Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav08:congruence_closure_theorem [2009/05/05 23:23]
vkuncak
sav08:congruence_closure_theorem [2009/05/06 00:25] (current)
vkuncak
Line 13: Line 13:
 **Proof:** **Proof:**
  
-The equivalence of first two statements ++|follows from the construction of [[Herbrand Universe for Equality]].++  ​+The equivalence of first two statements ++|follows from the construction of [[Herbrand Universe for Equality]]. We also directly show this special case.++  ​
  
 The equivalence of last two statements follows by definition. The equivalence of last two statements follows by definition.
 
sav08/congruence_closure_theorem.txt · Last modified: 2009/05/06 00:25 by vkuncak
 
© EPFL 2018 - Legal notice