Changes between Version 7 and Version 8 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 7, 2006 8:07:59 PM (9 years ago)
Author:
chak
Comment:

wiki formatting

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v7 v8  
    119119To solve  {{{(C implies t1=t2)}}} with respect to Ax
    120120
    121 1. We interpret Ax /\ C as a rewrite system (from left to right).
    122 
    123 2. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent.
     121 1. We interpret Ax /\ C as a rewrite system (from left to right).
     122 2. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent.
    124123
    125124
     
    188187To solve  {{{(C implies t1=t2)}}} with respect to Ax
    189188
    190 1. a. We interpret Ax /\ C as a rewrite system (from left to right)       and
    191 
    192    b. perform completion until the rewrite system is confluent.
    193 
    194 2. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent.
     189 1. First:
     190   1. We interpret Ax /\ C as a rewrite system (from left to right)   and
     191   2. perform completion until the rewrite system is confluent.
     192 2. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent.
    195193
    196194