We start the process with the following equations:

  E1: (• , taildown(f, x, y, a) ≈ recdown(g, x, y, a) , •)

We apply INDUCT to E1, which causes taildown(f, x, y, a) ≈ recdown(g, x, y, a) to be added to the set H of induction hypotheses.

This yields E2: (taildown(f, x, y, a) , taildown(f, x, y, a) ≈ recdown(g, x, y, a) , recdown(g, x, y, a))

We apply CASE on the constraint x ≤ y.

This yields the following new equations:

  E3: (taildown(f, x, y, a) , taildown(f, x, y, a) ≈ recdown(g, x, y, a) | x ≤ y , recdown(g, x, y, a))
  E4: (taildown(f, x, y, a) , taildown(f, x, y, a) ≈ recdown(g, x, y, a) | ¬(x ≤ y) , recdown(g, x, y, a))

We apply SIMPLIFICATION to E4 with rule R3 and substitution [F := f, a := a, i := y, x := x].

This yields E5: (taildown(f, x, y, a) , a ≈ recdown(g, x, y, a) | ¬(x ≤ y) , recdown(g, x, y, a))

We apply SIMPLIFICATION to E5 with rule R7 and substitution [F := g, i := y, x := x, z := a].

This yields E6: (taildown(f, x, y, a) , a ≈ a | ¬(x ≤ y) , recdown(g, x, y, a))

We apply DELETION to E6 because both sides are equal.  Thus, we may remove this equation from the proof state.

We apply SIMPLIFICATION to E3 with rule R4 and substitution [F := f, a := a, i := y, x := x].

This yields E7: (taildown(f, x, y, a) , taildown(f, x, y - 1, f(a, y)) ≈ recdown(g, x, y, a) | x ≤ y , recdown(g, x, y, a))

We use ALTER to add y1 = y - 1 to the constraint, and then use CALC at position l3.

This yields E8: (taildown(f, x, y, a) , taildown(f, x, y1, f(a, y)) ≈ recdown(g, x, y, a) | x ≤ y ∧ y1 = y - 1 , recdown(g, x, y, a))

We apply SIMPLIFICATION to E8 with rule R8 and substitution [F := g, i := y, x := x, z := a].

This yields E9: (taildown(f, x, y, a) , taildown(f, x, y1, f(a, y)) ≈ g(y, recdown(g, x, y - 1, a)) | x ≤ y ∧ y1 = y - 1 , recdown(g, x, y, a))

We use CALC at position r2.3.

This yields E10: (taildown(f, x, y, a) , taildown(f, x, y1, f(a, y)) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ y1 = y - 1 , recdown(g, x, y, a))

We apply HYPOTHESIS to E10 with induction hypothesis H1 and substitution [a := f(a, y), x := x, y := y1].  To this end, we impose the requirement that taildown(f, x, y, a) ≻ recdown(g, x, y1, f(a, y)) | x ≤ y ∧ y1 = y - 1.

This yields E11: (taildown(f, x, y, a) , recdown(g, x, y1, f(a, y)) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ y1 = y - 1 , recdown(g, x, y, a))

We apply GENERALISE to replace the constraint of E11 by x ≤ y.

This yields E12: (taildown(f, x, y, a) , recdown(g, x, y1, f(a, y)) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y , recdown(g, x, y, a))

We apply INDUCT to E12, which causes recdown(g, x, y1, f(a, y)) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y to be added to the set H of induction hypotheses.

This yields E13: (recdown(g, x, y1, f(a, y)) , recdown(g, x, y1, f(a, y)) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y , g(y, recdown(g, x, y1, a)))

We apply CASE on the constraint x ≤ y1.

This yields the following new equations:

  E14: (recdown(g, x, y1, f(a, y)) , recdown(g, x, y1, f(a, y)) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x ≤ y1 , g(y, recdown(g, x, y1, a)))
  E15: (recdown(g, x, y1, f(a, y)) , recdown(g, x, y1, f(a, y)) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ ¬(x ≤ y1) , g(y, recdown(g, x, y1, a)))

We apply SIMPLIFICATION to E15 with rule R7 and substitution [F := g, i := y1, x := x, z := f(a, y)].

This yields E16: (recdown(g, x, y1, f(a, y)) , f(a, y) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ ¬(x ≤ y1) , g(y, recdown(g, x, y1, a)))

We apply SIMPLIFICATION to E16 with rule R7 and substitution [F := g, i := y1, x := x, z := a].

This yields E17: (recdown(g, x, y1, f(a, y)) , f(a, y) ≈ g(y, a) | x ≤ y ∧ ¬(x ≤ y1) , g(y, recdown(g, x, y1, a)))

We apply POSTULATE to add the lemma equation f(x, y) ≈ g(y, x) to the current proof state.

This yields E18: (• , f(x, y) ≈ g(y, x) , •)

We apply INDUCT to E18, which causes f(x, y) ≈ g(y, x) to be added to the set H of induction hypotheses.

This yields E19: (f(x, y) , f(x, y) ≈ g(y, x) , g(y, x))

We apply SKIP, which does not change the existing equations, but does allow us to focus on a different one.

We apply HDELETE to E17 with induction hypothesis H18 and substitution [x := a, y := y].

We apply SIMPLIFICATION to E14 with rule R8 and substitution [F := g, i := y1, x := x, z := f(a, y)].

This yields E20: (recdown(g, x, y1, f(a, y)) , g(y1, recdown(g, x, y1 - 1, f(a, y))) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x ≤ y1 , g(y, recdown(g, x, y1, a)))

We use ALTER to add y2 = y1 - 1 to the constraint, and then use CALC at position l2.3.

This yields E21: (recdown(g, x, y1, f(a, y)) , g(y1, recdown(g, x, y2, f(a, y))) ≈ g(y, recdown(g, x, y1, a)) | x ≤ y ∧ x ≤ y1 ∧ y2 = y1 - 1 , g(y, recdown(g, x, y1, a)))

We apply SIMPLIFICATION to E21 with rule R8 and substitution [F := g, i := y1, x := x, z := a].

This yields E22: (recdown(g, x, y1, f(a, y)) , g(y1, recdown(g, x, y2, f(a, y))) ≈ g(y, g(y1, recdown(g, x, y1 - 1, a))) | x ≤ y ∧ x ≤ y1 ∧ y2 = y1 - 1 , g(y, recdown(g, x, y1, a)))

We use CALC at position r2.2.3.

This yields E23: (recdown(g, x, y1, f(a, y)) , g(y1, recdown(g, x, y2, f(a, y))) ≈ g(y, g(y1, recdown(g, x, y2, a))) | x ≤ y ∧ x ≤ y1 ∧ y2 = y1 - 1 , g(y, recdown(g, x, y1, a)))

We apply HYPOTHESIS to E23 with induction hypothesis H12 and substitution [a := a, x := x, y := y, y1 := y2].  To this end, we impose the requirement that recdown(g, x, y1, f(a, y)) ≻ g(y1, g(y, recdown(g, x, y2, a))) | x ≤ y ∧ x ≤ y1 ∧ y2 = y1 - 1.

This yields E24: (recdown(g, x, y1, f(a, y)) , g(y1, g(y, recdown(g, x, y2, a))) ≈ g(y, g(y1, recdown(g, x, y2, a))) | x ≤ y ∧ x ≤ y1 ∧ y2 = y1 - 1 , g(y, recdown(g, x, y1, a)))

We apply POSTULATE to add the lemma equation g(x, g(y, z)) ≈ g(y, g(x, z)) to the current proof state.

This yields E25: (• , g(x, g(y, z)) ≈ g(y, g(x, z)) , •)

We apply INDUCT to E25, which causes g(x, g(y, z)) ≈ g(y, g(x, z)) to be added to the set H of induction hypotheses.

This yields E26: (g(x, g(y, z)) , g(x, g(y, z)) ≈ g(y, g(x, z)) , g(y, g(x, z)))

We apply SKIP, which does not change the existing equations, but does allow us to focus on a different one.

We apply HDELETE to E24 with induction hypothesis H25 and substitution [x := y1, y := y, z := recdown(g, x, y2, a)].