We start the process with the following equations:

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

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

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

We apply CASE on the constraint x ≤ y.

This yields the following new equations:

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

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

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

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

This yields E6: (tailup(f, x, y, a) , a ≈ a | ¬(x ≤ y) , taildown(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 R2 and substitution [F := f, a := a, i := x, y := y].

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

We use ALTER to add x1 = x + 1 to the constraint, and then use CALC at position l2.

This yields E8: (tailup(f, x, y, a) , tailup(f, x1, y, f(x, a)) ≈ taildown(g, x, y, a) | x ≤ y ∧ x1 = x + 1 , taildown(g, x, y, a))

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

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

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

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

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

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

We apply INDUCT to E11, which causes taildown(g, x1, y, f(x, a)) ≈ taildown(g, x, y1, g(a, y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 to be added to the set H of induction hypotheses.

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

We apply CASE on the constraint x1 ≤ y.

This yields the following new equations:

  E13: (taildown(g, x1, y, f(x, a)) , taildown(g, x1, y, f(x, a)) ≈ taildown(g, x, y1, g(a, y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y , taildown(g, x, y1, g(a, y)))
  E14: (taildown(g, x1, y, f(x, a)) , taildown(g, x1, y, f(x, a)) ≈ taildown(g, x, y1, g(a, y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) , taildown(g, x, y1, g(a, y)))

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

This yields E15: (taildown(g, x1, y, f(x, a)) , f(x, a) ≈ taildown(g, x, y1, g(a, y)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) , taildown(g, x, y1, g(a, y)))

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

This yields E16: (taildown(g, x1, y, f(x, a)) , f(x, a) ≈ g(a, y) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y) , taildown(g, x, y1, g(a, y)))

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

This yields E17: (• , f(x, a) ≈ g(a, y) | x = y , •)

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

This yields E18: (f(x, a) , f(x, a) ≈ g(a, y) | x = y , g(a, y))

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

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

We apply SIMPLIFICATION to E13 with rule R4 and substitution [F := g, a := f(x, a), i := y, x := x1].

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

We use CALC at position l3.

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

We apply SIMPLIFICATION to E20 with rule R4 and substitution [F := g, a := g(a, y), i := y1, x := x].

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

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

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

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

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

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

This yields E24: (g(f(x, y), z) , g(f(x, y), z) ≈ f(x, g(y, z)) , f(x, g(y, z)))

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

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

This yields E25: (taildown(g, x1, y, f(x, a)) , taildown(g, x1, y1, f(x, g(a, y))) ≈ taildown(g, x, y2, g(g(a, y), y1)) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y ∧ y2 = y1 - 1 , taildown(g, x, y1, g(a, y)))

We apply HDELETE to E25 with induction hypothesis H11 and substitution [a := g(a, y), x := x, x1 := x1, y := y1, y1 := y2].