Differences
This shows you the differences between two versions of the page.
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] 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. |