Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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