We show that R  is a hidden -congruence.
We show
(I1,I2 : Nat A1,A2 : Arr)
(I1 || A1) R (I2 || A2)   implies   top(I1 || A1)  R  top(I2 || A2) ,
with the following steps:
  1. Use quantifier elimination to introduce new constants i1, i2 of sort Nat, and a1, a2 of sort Arr.
  2. Use implication elimination to assume (i1 || a1) R (i2 || a2) .
  3. Use case analysis, i1 = 0 or i1 = s(j) for some j of sort Nat .
    3A.  In case i1 = 0 :
    3A1.  Use relation expansion to add i2 = 0 to the hypotheses.
    3A2.  Show by reduction that
    top(i1 || a1)  R  top(i2 || a2) = true .
    3B.  in case i1 = s(j) :
    3B1.  Use relation expansion to add the following equations to the hypotheses:
    • i2 = s j
    • a2[j] = a1[j]
    • (j || a1) R (j || a2) = true .
    3B2. show by reduction that
    top(i1 || a1)  R  top(i2 || a2) = true .

18 Jun 1997 >