# LARA

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 be a set of ground terms and a congruence on . Then where denotes the congruence closure of .

Proof:

Show for all .

Proof End.

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: $\begin{array}{l}  \forall x_1,\ldots,x_n,y_1,\ldots,y_n. \bigwedge_{i=1}^n (x_i,y_i) \in r\ \land \ f(x_1,\ldots,x_n) \in T \land f(y_1,\ldots,y_n) \in T \rightarrow \\ (f(x_1,\ldots,x_n),f(y_1,\ldots,y_n)) \in r$