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