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 be a set of ground terms and a congruence on . Then where denotes the congruence closure of .
Show for all , by induction.
- : s = s
, by induction hypothesis . Thus . As adds only needed term for congruence, the added term are either not in or in not a congruence. By hypothesis is a congruence, so . Therefore .
When checking a formula we compute congruences on a finite set of terms that occur in the formula.
We apply the congruence condition only to terms that already exist in the set, using congruence condition: