Changes between Version 7 and Version 8 of TypeFunctionsSynTC
 Timestamp:
 Dec 7, 2006 8:07:59 PM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSynTC
v7 v8 119 119 To solve {{{(C implies t1=t2)}}} with respect to Ax 120 120 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. 124 123 125 124 … … 188 187 To solve {{{(C implies t1=t2)}}} with respect to Ax 189 188 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. 195 193 196 194