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

We apply INDUCT to E1, which causes tailup(f, x, y, a) ≈ recup(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) ≈ recup(g, x, y, a) , recup(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) ≈ recup(g, x, y, a) | x ≤ y , recup(g, x, y, a))
  E4: (tailup(f, x, y, a) , tailup(f, x, y, a) ≈ recup(g, x, y, a) | ¬(x ≤ y) , recup(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 ≈ recup(g, x, y, a) | ¬(x ≤ y) , recup(g, x, y, a))

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

This yields E6: (tailup(f, x, y, a) , a ≈ a | ¬(x ≤ y) , recup(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)) ≈ recup(g, x, y, a) | x ≤ y , recup(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)) ≈ recup(g, x, y, a) | x ≤ y ∧ x1 = x + 1 , recup(g, x, y, a))

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

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

We use CALC at position r1.2.

This yields E10: (tailup(f, x, y, a) , tailup(f, x1, y, f(x, a)) ≈ g(recup(g, x1, y, a), x) | x ≤ y ∧ x1 = x + 1 , recup(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) ≻ recup(g, x1, y, f(x, a)) | x ≤ y ∧ x1 = x + 1.

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

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

This yields E12: (tailup(f, x, y, a) , recup(g, x1, y, f(x, a)) ≈ g(recup(g, x1, y, a), x) | x ≤ y , recup(g, x, y, a))

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

This yields E13: (recup(g, x1, y, f(x, a)) , recup(g, x1, y, f(x, a)) ≈ g(recup(g, x1, y, a), x) | x ≤ y , g(recup(g, x1, y, a), x))

We apply CASE on the constraint x1 ≤ y.

This yields the following new equations:

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

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

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

We apply SIMPLIFICATION to E16 with rule R5 and substitution [F := g, i := x1, y := y, z := a].

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

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 := x, y := a].

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

This yields E20: (recup(g, x1, y, f(x, a)) , g(recup(g, x1 + 1, y, f(x, a)), x1) ≈ g(recup(g, x1, y, a), x) | x ≤ y ∧ x1 ≤ y , g(recup(g, x1, y, a), x))

We use ALTER to add x2 = x1 + 1 to the constraint, and then use CALC at position l1.2.

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

We apply SIMPLIFICATION to E21 with rule R6 and substitution [F := g, i := x1, y := y, z := a].

This yields E22: (recup(g, x1, y, f(x, a)) , g(recup(g, x2, y, f(x, a)), x1) ≈ g(g(recup(g, x1 + 1, y, a), x1), x) | x ≤ y ∧ x1 ≤ y ∧ x2 = x1 + 1 , g(recup(g, x1, y, a), x))

We use CALC at position r1.1.2.

This yields E23: (recup(g, x1, y, f(x, a)) , g(recup(g, x2, y, f(x, a)), x1) ≈ g(g(recup(g, x2, y, a), x1), x) | x ≤ y ∧ x1 ≤ y ∧ x2 = x1 + 1 , g(recup(g, x1, y, a), x))

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

This yields E24: (recup(g, x1, y, f(x, a)) , g(g(recup(g, x2, y, a), x), x1) ≈ g(g(recup(g, x2, y, a), x1), x) | x ≤ y ∧ x1 ≤ y ∧ x2 = x1 + 1 , g(recup(g, x1, y, a), x))

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

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

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

This yields E26: (g(g(x, y), z) , g(g(x, y), z) ≈ g(g(x, z), y) , g(g(x, z), 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 E24 with induction hypothesis H25 and substitution [x := recup(g, x2, y, a), y := x, z := x1].