This is an old revision of the document!

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.