Changes between Version 5 and Version 6 of TypeFunctionsSynTC
 Timestamp:
 Dec 5, 2006 7:52:28 AM (10 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSynTC
v5 v6 426 426 The literate implication constraints generated out of the 427 427 program text may look as follows 428 {{{ a=T Int implies ( a= S Int implies ...) 428 {{{ 429 a=T Int implies ( a= S Int implies ...) 429 430 }}} 430 431 431 432 The above can be simplified to 432 {{{ (a=T Int /\ a = S Int) implies ...}}} 433 {{{ 434 (a=T Int /\ a = S Int) implies ... 435 }}} 433 436 Before we proceed with the completion method, we first 434 437 need to apply some closure rules (eg. transitivity, left, right etc) 435 438 Hence, from the above we generatet 436 {{{a=T Int /\ a = S Int /\ 439 {{{ 440 a=T Int /\ a = S Int /\ 437 441 T Int = a /\ S Int = a /\  symmetry 438 442 T Int = S Int /\ S Int = T Int  transitivity 439 443 }}} 440 444 We omit the trival (reflexive) equations 441 {{{ T Int = T Int /\ S Int = S Int }}} 445 {{{ 446 T Int = T Int /\ S Int = S Int 447 }}}