But in many other cases, proving the congruence property involves assuming that two terms are related by R and then showing that two other terms are related by R. In such cases, after applying quantifier and implication elimination, we will have assumed a ground equation
(*) t R t' = true ,which is often not directly usable for proving that the other two terms are related by R.
However, R is usually defined by some equations of the form
(+) (where T0, T0' are terms of hidden sort, and the term pairs T1, T1', etc. each have the same visible sort. Then we can expand an instance t R t', as in (*), into a set of equations of the form:X) T0 R T0' = T1 == T1' and T2 == T2' and ....... ,
t1 = t1' t2 = t2' ....... ,where the pairs t', t1' etc. are substitution instances of T', T1', etc. These consequences of (*) should be placed among the hypotheses of the proof, and are often essential for checking the congruence property.
This rule of inference, which we call relation expansion, is actually a general result of equational logic, not specific to hidden algebra. Its soundness is proved as follows: an instance t R t' of T0 R T0' can only be true when each conjunct on the rightside of the equation (+) is true; because each conjunct relates two terms by ==, truth of the conjunct implies that its two terms can be proved equal.
It is also possible that R has been defined recursively, so that there is a conjunct of the form Ti R Ti' on the rightside of (+). In this case, relation expansion of (*) produces an equation of the form
ti R ti' = true .
Kumo has a general inference rule that converts (some) first order formulae to equations that can be used as rewrite rules; this inference rule is general enough to include relation expansion as a special case.