Differences
This shows you the differences between two versions of the page.
|
sav08:partial_congruences [2008/04/23 07:45] vkuncak |
sav08:partial_congruences [2015/04/21 17:30] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Partial Congruences ====== | ||
| - | Instead of a congruence on the (typically infinite) set of all ground terms we will compute congruences on a given finite set of ground terms. We call these congruences partial congruences; they are simply congruences on a subset of the original set. | ||
| - | |||
| - | **Theorem:** Let $T$ be a set of ground terms and $s$ a congruence on $T$. Then $CC(s) \cap T^2 = s$ where $CC(s)$ denotes the congruence closure of $s$. | ||
| - | |||
| - | **Proof:** | ||
| - | |||
| - | Show that C^i(s) \cap T^2 = s$ for each $i \ge 0$. | ||
| - | |||
| - | **Proof End.** | ||