Remark
=========================================================================
The proof uses the following lemma 

recup(helper, x, y - 1, y) [=] recup(helper, x, y, 1) | x <= y

which does not follow from an existing lemma generation technique.

However, considering the conceptual structure of recup and that
helper is actually (reverse) multiplication: we have a neutral element 
1 (i.e. helper(1, x) = helper(x, 1)=x for all x), so this is a reasonable
lemma to suggest. 

For example, by similar reasoning we could propose a lemma 
recup([+], x, y - 1, y) [=] recup([+], x, y, 0) | x <= y
in a + related example. 
=========================================================================


We start the process with the following equations:

  E1: (• , factTU(x) ≈ factRU(x) | x ≥ 1 , •)

We apply POSTULATE to add the lemma equation u(x, i, a) ≈ tailup([*], i, x, a) to the current proof state.

This yields E2: (• , u(x, i, a) ≈ tailup([*], i, x, a) , •)

We apply INDUCT to E2, which causes u(x, i, a) ≈ tailup([*], i, x, a) to be added to the set H of induction hypotheses.

This yields E3: (u(x, i, a) , u(x, i, a) ≈ tailup([*], i, x, a) , tailup([*], i, x, a))

We apply CASE on the constraint x ≥ i.

This yields the following new equations:

  E4: (u(x, i, a) , u(x, i, a) ≈ tailup([*], i, x, a) | x ≥ i , tailup([*], i, x, a))
  E5: (u(x, i, a) , u(x, i, a) ≈ tailup([*], i, x, a) | ¬(x ≥ i) , tailup([*], i, x, a))

We apply SIMPLIFICATION to E5 with rule R2 and substitution [a := a, i := i, x := x].

This yields E6: (u(x, i, a) , a ≈ tailup([*], i, x, a) | ¬(x ≥ i) , tailup([*], i, x, a))

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

This yields E7: (u(x, i, a) , a ≈ a | ¬(x ≥ i) , tailup([*], i, x, a))

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

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

This yields E8: (u(x, i, a) , u(x, i + 1, i * a) ≈ tailup([*], i, x, a) | x ≥ i , tailup([*], i, x, a))

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

This yields E9: (u(x, i, a) , u(x, i1, i * a) ≈ tailup([*], i, x, a) | x ≥ i ∧ i1 = i + 1 , tailup([*], i, x, a))

We use ALTER to add a1 = i * a to the constraint, and then use CALC at position l3.

This yields E10: (u(x, i, a) , u(x, i1, a1) ≈ tailup([*], i, x, a) | x ≥ i ∧ i1 = i + 1 ∧ a1 = i * a , tailup([*], i, x, a))

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

This yields E11: (u(x, i, a) , u(x, i1, a1) ≈ tailup([*], i + 1, x, i * a) | x ≥ i ∧ i1 = i + 1 ∧ a1 = i * a , tailup([*], i, x, a))

We use CALC at position r2.

This yields E12: (u(x, i, a) , u(x, i1, a1) ≈ tailup([*], i1, x, i * a) | x ≥ i ∧ i1 = i + 1 ∧ a1 = i * a , tailup([*], i, x, a))

We use CALC at position r4.

This yields E13: (u(x, i, a) , u(x, i1, a1) ≈ tailup([*], i1, x, a1) | x ≥ i ∧ i1 = i + 1 ∧ a1 = i * a , tailup([*], i, x, a))

We apply HDELETE to E13 with induction hypothesis H2 and substitution [a := a1, i := i1, x := x].

We apply POSTULATE to add the lemma equation U(i, x) ≈ recup(helper, i, x - 1, x) to the current proof state.

This yields E14: (• , U(i, x) ≈ recup(helper, i, x - 1, x) , •)

We use CALC at the only position where it is possible.

This yields E15: (• , U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 , •)

We apply INDUCT to E15, which causes U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 to be added to the set H of induction hypotheses.

This yields E16: (U(i, x) , U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 , recup(helper, i, x1, x))

We apply CASE on the constraint i ≤ x - 1.

This yields the following new equations:

  E17: (U(i, x) , U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ i ≤ x - 1 , recup(helper, i, x1, x))
  E18: (U(i, x) , U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ ¬(i ≤ x - 1) , recup(helper, i, x1, x))

We apply SIMPLIFICATION to E18 with rule R5 and substitution [i := i, x := x].

This yields E19: (U(i, x) , x ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ ¬(i ≤ x - 1) , recup(helper, i, x1, x))

We apply SIMPLIFICATION to E19 with rule R9 and substitution [F := helper, a := x, i := i, y := x1].

This yields E20: (U(i, x) , x ≈ x | x1 = x - 1 ∧ ¬(i ≤ x - 1) , recup(helper, i, x1, x))

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

We apply SIMPLIFICATION to E17 with rule R6 and substitution [i := i, x := x].

This yields E21: (U(i, x) , i * U(i + 1, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ i ≤ x - 1 , recup(helper, i, x1, x))

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

This yields E22: (U(i, x) , i * U(i1, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ i ≤ x - 1 ∧ i1 = i + 1 , recup(helper, i, x1, x))

We apply SIMPLIFICATION to E22 with rule R10 and substitution [F := helper, a := x, i := i, y := x1].

This yields E23: (U(i, x) , i * U(i1, x) ≈ helper(recup(helper, i + 1, x1, x), i) | x1 = x - 1 ∧ i ≤ x - 1 ∧ i1 = i + 1 , recup(helper, i, x1, x))

We use CALC at position r1.2.

This yields E24: (U(i, x) , i * U(i1, x) ≈ helper(recup(helper, i1, x1, x), i) | x1 = x - 1 ∧ i ≤ x - 1 ∧ i1 = i + 1 , recup(helper, i, x1, x))

We apply SIMPLIFICATION to E24 with rule R11 and substitution [x := recup(helper, i1, x1, x), y := i].

This yields E25: (U(i, x) , i * U(i1, x) ≈ i * recup(helper, i1, x1, x) | x1 = x - 1 ∧ i ≤ x - 1 ∧ i1 = i + 1 , recup(helper, i, x1, x))

We apply HDELETE to E25 with induction hypothesis H15 and substitution [i := i1, x := x, x1 := x1].

We apply POSTULATE to add the lemma equation tailup([*], x, y, a) ≈ recup(helper, x, y, a) to the current proof state.

This yields E26: (• , tailup([*], x, y, a) ≈ recup(helper, x, y, a) , •)

We apply INDUCT to E26, which causes tailup([*], x, y, a) ≈ recup(helper, x, y, a) to be added to the set H of induction hypotheses.

This yields E27: (tailup([*], x, y, a) , tailup([*], x, y, a) ≈ recup(helper, x, y, a) , recup(helper, x, y, a))

We apply CASE on the constraint x ≤ y.

This yields the following new equations:

  E28: (tailup([*], x, y, a) , tailup([*], x, y, a) ≈ recup(helper, x, y, a) | x ≤ y , recup(helper, x, y, a))
  E29: (tailup([*], x, y, a) , tailup([*], x, y, a) ≈ recup(helper, x, y, a) | ¬(x ≤ y) , recup(helper, x, y, a))

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

This yields E30: (tailup([*], x, y, a) , a ≈ recup(helper, x, y, a) | ¬(x ≤ y) , recup(helper, x, y, a))

We apply SIMPLIFICATION to E30 with rule R9 and substitution [F := helper, a := a, i := x, y := y].

This yields E31: (tailup([*], x, y, a) , a ≈ a | ¬(x ≤ y) , recup(helper, x, y, a))

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

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

This yields E32: (tailup([*], x, y, a) , tailup([*], x + 1, y, x * a) ≈ recup(helper, x, y, a) | x ≤ y , recup(helper, x, y, a))

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

This yields E33: (tailup([*], x, y, a) , tailup([*], x1, y, x * a) ≈ recup(helper, x, y, a) | x ≤ y ∧ x1 = x + 1 , recup(helper, x, y, a))

We use ALTER to add a1 = x * a to the constraint, and then use CALC at position l4.

This yields E34: (tailup([*], x, y, a) , tailup([*], x1, y, a1) ≈ recup(helper, x, y, a) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a , recup(helper, x, y, a))

We apply SIMPLIFICATION to E34 with rule R10 and substitution [F := helper, a := a, i := x, y := y].

This yields E35: (tailup([*], x, y, a) , tailup([*], x1, y, a1) ≈ helper(recup(helper, x + 1, y, a), x) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a , recup(helper, x, y, a))

We use CALC at position r1.2.

This yields E36: (tailup([*], x, y, a) , tailup([*], x1, y, a1) ≈ helper(recup(helper, x1, y, a), x) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a , recup(helper, x, y, a))

We apply SIMPLIFICATION to E36 with rule R11 and substitution [x := recup(helper, x1, y, a), y := x].

This yields E37: (tailup([*], x, y, a) , tailup([*], x1, y, a1) ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a , recup(helper, x, y, a))

We apply HYPOTHESIS to E37 with induction hypothesis H26 and substitution [a := a1, x := x1, y := y].  To this end, we impose the requirement that tailup([*], x, y, a) ≻ recup(helper, x1, y, a1) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a.

This yields E38: (tailup([*], x, y, a) , recup(helper, x1, y, a1) ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a , recup(helper, x, y, a))

We apply GENERALISE to replace the constraint of E38 by x ≤ y ∧ a1 = x * a.

This yields E39: (tailup([*], x, y, a) , recup(helper, x1, y, a1) ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ a1 = x * a , recup(helper, x, y, a))

We apply INDUCT to E39, which causes recup(helper, x1, y, a1) ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ a1 = x * a to be added to the set H of induction hypotheses.

This yields E40: (recup(helper, x1, y, a1) , recup(helper, x1, y, a1) ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ a1 = x * a , x * recup(helper, x1, y, a))

We apply CASE on the constraint x1 ≤ y.

This yields the following new equations:

  E41: (recup(helper, x1, y, a1) , recup(helper, x1, y, a1) ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ a1 = x * a ∧ x1 ≤ y , x * recup(helper, x1, y, a))
  E42: (recup(helper, x1, y, a1) , recup(helper, x1, y, a1) ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ a1 = x * a ∧ ¬(x1 ≤ y) , x * recup(helper, x1, y, a))

We apply SIMPLIFICATION to E42 with rule R9 and substitution [F := helper, a := a1, i := x1, y := y].

This yields E43: (recup(helper, x1, y, a1) , a1 ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ a1 = x * a ∧ ¬(x1 ≤ y) , x * recup(helper, x1, y, a))

We apply SIMPLIFICATION to E43 with rule R9 and substitution [F := helper, a := a, i := x1, y := y].

This yields E44: (recup(helper, x1, y, a1) , a1 ≈ x * a | x ≤ y ∧ a1 = x * a ∧ ¬(x1 ≤ y) , x * recup(helper, x1, y, a))

We use CALC at position r.

This yields E45: (recup(helper, x1, y, a1) , a1 ≈ a1 | x ≤ y ∧ a1 = x * a ∧ ¬(x1 ≤ y) , x * recup(helper, x1, y, a))

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

We apply SIMPLIFICATION to E41 with rule R10 and substitution [F := helper, a := a1, i := x1, y := y].

This yields E46: (recup(helper, x1, y, a1) , helper(recup(helper, x1 + 1, y, a1), x1) ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ a1 = x * a ∧ x1 ≤ y , x * recup(helper, x1, y, a))

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

This yields E47: (recup(helper, x1, y, a1) , helper(recup(helper, x2, y, a1), x1) ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ a1 = x * a ∧ x1 ≤ y ∧ x2 = x1 + 1 , x * recup(helper, x1, y, a))

We apply SIMPLIFICATION to E47 with rule R11 and substitution [x := recup(helper, x2, y, a1), y := x1].

This yields E48: (recup(helper, x1, y, a1) , x1 * recup(helper, x2, y, a1) ≈ x * recup(helper, x1, y, a) | x ≤ y ∧ a1 = x * a ∧ x1 ≤ y ∧ x2 = x1 + 1 , x * recup(helper, x1, y, a))

We apply SIMPLIFICATION to E48 with rule R10 and substitution [F := helper, a := a, i := x1, y := y].

This yields E49: (recup(helper, x1, y, a1) , x1 * recup(helper, x2, y, a1) ≈ x * helper(recup(helper, x1 + 1, y, a), x1) | x ≤ y ∧ a1 = x * a ∧ x1 ≤ y ∧ x2 = x1 + 1 , x * recup(helper, x1, y, a))

We use CALC at position r2.1.2.

This yields E50: (recup(helper, x1, y, a1) , x1 * recup(helper, x2, y, a1) ≈ x * helper(recup(helper, x2, y, a), x1) | x ≤ y ∧ a1 = x * a ∧ x1 ≤ y ∧ x2 = x1 + 1 , x * recup(helper, x1, y, a))

We apply SIMPLIFICATION to E50 with rule R11 and substitution [x := recup(helper, x2, y, a), y := x1].

This yields E51: (recup(helper, x1, y, a1) , x1 * recup(helper, x2, y, a1) ≈ x * (x1 * recup(helper, x2, y, a)) | x ≤ y ∧ a1 = x * a ∧ x1 ≤ y ∧ x2 = x1 + 1 , x * recup(helper, x1, y, a))

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

This yields E52: (recup(helper, x1, y, a1) , x1 * (x * recup(helper, x2, y, a)) ≈ x * (x1 * recup(helper, x2, y, a)) | x ≤ y ∧ a1 = x * a ∧ x1 ≤ y ∧ x2 = x1 + 1 , x * recup(helper, x1, y, a))

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

This yields E53: (• , x * (y * z) ≈ y * (x * z) , •)

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

This yields E54: (x * (y * z) , x * (y * z) ≈ y * (x * z) , y * (x * z))

We use ALTER to add i1 = y * z to the constraint, and then use CALC at position l2.

This yields E55: (x * (y * z) , x * i1 ≈ y * (x * z) | i1 = y * z , y * (x * z))

We use ALTER to add i2 = x * i1 to the constraint, and then use CALC at position l.

This yields E56: (x * (y * z) , i2 ≈ y * (x * z) | i1 = y * z ∧ i2 = x * i1 , y * (x * z))

We use ALTER to add i3 = x * z to the constraint, and then use CALC at position r2.

This yields E57: (x * (y * z) , i2 ≈ y * i3 | i1 = y * z ∧ i2 = x * i1 ∧ i3 = x * z , y * (x * z))

We use ALTER to add i4 = y * i3 to the constraint, and then use CALC at position r.

This yields E58: (x * (y * z) , i2 ≈ i4 | i1 = y * z ∧ i2 = x * i1 ∧ i3 = x * z ∧ i4 = y * i3 , y * (x * z))

We observe that i1 = y * z ∧ i2 = x * i1 ∧ i3 = x * z ∧ i4 = y * i3 ⊨ i2 = i4, and may therefore apply EQ-DELETION to remove E58 from the proof state.

We apply HDELETE to E52 with induction hypothesis H53 and substitution [x := x1, y := x, z := recup(helper, x2, y, a)].

We apply INDUCT to E1, which causes factTU(x) ≈ factRU(x) | x ≥ 1 to be added to the set H of induction hypotheses.

This yields E59: (factTU(x) , factTU(x) ≈ factRU(x) | x ≥ 1 , factRU(x))

We apply SIMPLIFICATION to E59 with rule R1 and substitution [x := x].

This yields E60: (factTU(x) , u(x, 1, 1) ≈ factRU(x) | x ≥ 1 , factRU(x))

We apply SIMPLIFICATION to E60 with rule R3 and substitution [a := 1, i := 1, x := x].

This yields E61: (factTU(x) , u(x, 1 + 1, 1 * 1) ≈ factRU(x) | x ≥ 1 , factRU(x))

We use CALC at position l2.

This yields E62: (factTU(x) , u(x, 2, 1 * 1) ≈ factRU(x) | x ≥ 1 , factRU(x))

We use CALC at position l3.

This yields E63: (factTU(x) , u(x, 2, 1) ≈ factRU(x) | x ≥ 1 , factRU(x))

We apply SIMPLIFICATION to E63 with rule R4 and substitution [x := x].

This yields E64: (factTU(x) , u(x, 2, 1) ≈ U(1, x) | x ≥ 1 , factRU(x))

We apply POSTULATE to add the lemma equation recup(helper, x, y - 1, y) ≈ recup(helper, x, y, 1) | x ≤ y to the current proof state.

This yields E65: (• , recup(helper, x, y - 1, y) ≈ recup(helper, x, y, 1) | x ≤ y , •)

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

This yields E66: (• , recup(helper, x, y1, y) ≈ recup(helper, x, y, 1) | x ≤ y ∧ y1 = y - 1 , •)

We apply INDUCT to E66, which causes recup(helper, x, y1, y) ≈ recup(helper, x, y, 1) | x ≤ y ∧ y1 = y - 1 to be added to the set H of induction hypotheses.

This yields E67: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ recup(helper, x, y, 1) | x ≤ y ∧ y1 = y - 1 , recup(helper, x, y, 1))

We apply SIMPLIFICATION to E67 with rule R10 and substitution [F := helper, a := 1, i := x, y := y].

This yields E68: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ helper(recup(helper, x + 1, y, 1), x) | x ≤ y ∧ y1 = y - 1 , recup(helper, x, y, 1))

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

This yields E69: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ helper(recup(helper, x1, y, 1), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 , recup(helper, x, y, 1))

We apply SIMPLIFICATION to E69 with rule R11 and substitution [x := recup(helper, x1, y, 1), y := x].

This yields E70: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 , recup(helper, x, y, 1))

We apply CASE on the constraint x ≤ y1.

This yields the following new equations:

  E71: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , recup(helper, x, y, 1))
  E72: (recup(helper, x, y1, y) , recup(helper, x, y1, y) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) , recup(helper, x, y, 1))

We apply SIMPLIFICATION to E72 with rule R9 and substitution [F := helper, a := y, i := x, y := y1].

This yields E73: (recup(helper, x, y1, y) , y ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) , recup(helper, x, y, 1))

We apply SIMPLIFICATION to E73 with rule R9 and substitution [F := helper, a := 1, i := x1, y := y].

This yields E74: (recup(helper, x, y1, y) , y ≈ x * 1 | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) , recup(helper, x, y, 1))

We use ALTER to add x2 = x * 1 to the constraint, and then use CALC at position r.

This yields E75: (recup(helper, x, y1, y) , y ≈ x2 | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) ∧ x2 = x * 1 , recup(helper, x, y, 1))

We observe that x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) ∧ x2 = x * 1 ⊨ y = x2, and may therefore apply EQ-DELETION to remove E75 from the proof state.

We apply SIMPLIFICATION to E71 with rule R10 and substitution [F := helper, a := y, i := x, y := y1].

This yields E76: (recup(helper, x, y1, y) , helper(recup(helper, x + 1, y1, y), x) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , recup(helper, x, y, 1))

We use CALC at position l1.2.

This yields E77: (recup(helper, x, y1, y) , helper(recup(helper, x1, y1, y), x) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , recup(helper, x, y, 1))

We apply SIMPLIFICATION to E77 with rule R11 and substitution [x := recup(helper, x1, y1, y), y := x].

This yields E78: (recup(helper, x, y1, y) , x * recup(helper, x1, y1, y) ≈ x * recup(helper, x1, y, 1) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , recup(helper, x, y, 1))

We apply HDELETE to E78 with induction hypothesis H66 and substitution [x := x1, y := y, y1 := y1].

We apply HYPOTHESIS to E64 with induction hypothesis H2 and substitution [a := 1, i := 2, x := x].  To this end, we impose the requirement that factTU(x) ≻ tailup([*], 2, x, 1) | x ≥ 1.

This yields E79: (factTU(x) , tailup([*], 2, x, 1) ≈ U(1, x) | x ≥ 1 , factRU(x))

We apply ALTER to add x1 = x - 1 to the constraint of E79.

This yields E80: (factTU(x) , tailup([*], 2, x, 1) ≈ U(1, x) | x ≥ 1 ∧ x1 = x - 1 , factRU(x))

We apply HYPOTHESIS to E80 with induction hypothesis H15 and substitution [i := 1, x := x, x1 := x1].  To this end, we impose the requirement that factRU(x) ≻ recup(helper, 1, x1, x) | x ≥ 1 ∧ x1 = x - 1.

This yields E81: (factTU(x) , tailup([*], 2, x, 1) ≈ recup(helper, 1, x1, x) | x ≥ 1 ∧ x1 = x - 1 , factRU(x))

We apply HYPOTHESIS to E81 with induction hypothesis H66 and substitution [x := 1, y := x, y1 := x1].  To this end, we impose the requirement that factRU(x) ≻ recup(helper, 1, x, 1) | x ≥ 1 ∧ x1 = x - 1.

This yields E82: (factTU(x) , tailup([*], 2, x, 1) ≈ recup(helper, 1, x, 1) | x ≥ 1 ∧ x1 = x - 1 , factRU(x))

We apply SIMPLIFICATION to E82 with rule R10 and substitution [F := helper, a := 1, i := 1, y := x].

This yields E83: (factTU(x) , tailup([*], 2, x, 1) ≈ helper(recup(helper, 1 + 1, x, 1), 1) | x ≥ 1 ∧ x1 = x - 1 , factRU(x))

We use CALC at position r1.2.

This yields E84: (factTU(x) , tailup([*], 2, x, 1) ≈ helper(recup(helper, 2, x, 1), 1) | x ≥ 1 ∧ x1 = x - 1 , factRU(x))

We apply SIMPLIFICATION to E84 with rule R11 and substitution [x := recup(helper, 2, x, 1), y := 1].

This yields E85: (factTU(x) , tailup([*], 2, x, 1) ≈ 1 * recup(helper, 2, x, 1) | x ≥ 1 ∧ x1 = x - 1 , factRU(x))

We apply POSTULATE to add the lemma equation 1 * x ≈ x to the current proof state.

This yields E86: (• , 1 * x ≈ x , •)

We apply INDUCT to E86, which causes 1 * x ≈ x to be added to the set H of induction hypotheses.

This yields E87: (1 * x , 1 * x ≈ x , x)

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

This yields E88: (1 * x , x1 ≈ x | x1 = 1 * x , x)

We observe that x1 = 1 * x ⊨ x1 = x, and may therefore apply EQ-DELETION to remove E88 from the proof state.

We apply HYPOTHESIS to E85 with induction hypothesis H86 and substitution [x := recup(helper, 2, x, 1)].  To this end, we impose the requirement that factRU(x) ≻ recup(helper, 2, x, 1) | x ≥ 1 ∧ x1 = x - 1.

This yields E89: (factTU(x) , tailup([*], 2, x, 1) ≈ recup(helper, 2, x, 1) | x ≥ 1 ∧ x1 = x - 1 , factRU(x))

We apply HDELETE to E89 with induction hypothesis H26 and substitution [a := 1, x := 2, y := x].

All equations have been removed, so the proof is complete: the original equations are inductive theorems.  The existence of a suitable bounding pair is guaranteed by the termination of the corresponding term rewriting systems, as is demonstrated below.

We consider termination of the LCSTRS with only rule scheme Calc:

  Signature: U      :: Int → Int → Int
             factRU :: Int → Int
             factTU :: Int → Int
             helper :: Int → Int → Int
             recup  :: (Int → Int → Int) → Int → Int → Int → Int
             tailup :: (Int → Int → Int) → Int → Int → Int → Int
             u      :: Int → Int → Int → Int

  Rules: factTU(x) → u(x, 1, 1)
         u(x, i, a) → a | i > x
         u(x, i, a) → u(x, i + 1, i * a) | i ≤ x
         factRU(x) → U(1, x)
         U(i, x) → x | i > x - 1
         U(i, x) → i * U(i + 1, x) | i ≤ x - 1
         tailup(F, i, y, a) → a | i > y
         tailup(F, i, y, a) → tailup(F, i + 1, y, F(i, a)) | i ≤ y
         recup(F, i, y, a) → a | i > y
         recup(F, i, y, a) → F(recup(F, i + 1, y, a), i) | i ≤ y
         helper(x, y) → y * x
         tailup([*], x__1, y, a__1) → recup(helper, x__2, y, a__2) | x__1 ≤ y ∧ x__2 = x__1 + 1 ∧ a__2 = x__1 * a__1
         recup(helper, x__2, y, a__2) → x__2 * (x__1 * recup(helper, x__3, y, a__1)) | x__1 ≤ y ∧ a__2 = x__1 * a__1 ∧ x__2 ≤ y ∧ x__3 = x__2 + 1
         factTU(x) → tailup([*], 2, x, 1) | x ≥ 1
         factRU(x__1) → recup(helper, 1, x__2, x__1) | x__1 ≥ 1 ∧ x__2 = x__1 - 1
         factRU(x__1) → recup(helper, 1, x__1, 1) | x__1 ≥ 1 ∧ x__2 = x__1 - 1
         factRU(x__1) → recup(helper, 2, x__1, 1) | x__1 ≥ 1 ∧ x__2 = x__1 - 1

The system is accessible function passing by a sort ordering that equates all sorts.

We start by computing the initial DP problem D1 = (P1, R, f, c), where:

  P1. (1)  factTU#(x) ➡ u#(x, 1, 1) | true
      (2)  u#(x, i, a) ➡ u#(x, i + 1, i * a) | i ≤ x
      (3)  factRU#(x) ➡ U#(1, x) | true
      (4)  U#(i, x) ➡ U#(i + 1, x) | i ≤ x - 1
      (5)  tailup#(F, i, y, a) ➡ tailup#(F, i + 1, y, F(i, a)) | i ≤ y
      (6)  recup#(F, i, y, a) ➡ recup#(F, i + 1, y, a) | i ≤ y
      (7)  tailup#([*], x__1, y, a__1) ➡ helper#(fresh1, fresh2) | x__1 ≤ y ∧ x__2 = x__1 + 1 ∧ a__2 = x__1 * a__1
      (8)  tailup#([*], x__1, y, a__1) ➡ recup#(helper, x__2, y, a__2) | x__1 ≤ y ∧ x__2 = x__1 + 1 ∧ a__2 = x__1 * a__1
      (9)  recup#(helper, x__2, y, a__2) ➡ helper#(fresh1, fresh2) | x__1 ≤ y ∧ a__2 = x__1 * a__1 ∧ x__2 ≤ y ∧ x__3 = x__2 + 1
      (10) recup#(helper, x__2, y, a__2) ➡ recup#(helper, x__3, y, a__1) | x__1 ≤ y ∧ a__2 = x__1 * a__1 ∧ x__2 ≤ y ∧ x__3 = x__2 + 1
      (11) factTU#(x) ➡ tailup#([*], 2, x, 1) | x ≥ 1
      (12) factRU#(x__1) ➡ helper#(fresh1, fresh2) | x__1 ≥ 1 ∧ x__2 = x__1 - 1
      (13) factRU#(x__1) ➡ recup#(helper, 1, x__2, x__1) | x__1 ≥ 1 ∧ x__2 = x__1 - 1
      (14) factRU#(x__1) ➡ helper#(fresh1, fresh2) | x__1 ≥ 1 ∧ x__2 = x__1 - 1
      (15) factRU#(x__1) ➡ recup#(helper, 1, x__1, 1) | x__1 ≥ 1 ∧ x__2 = x__1 - 1
      (16) factRU#(x__1) ➡ helper#(fresh1, fresh2) | x__1 ≥ 1 ∧ x__2 = x__1 - 1
      (17) factRU#(x__1) ➡ recup#(helper, 2, x__1, 1) | x__1 ≥ 1 ∧ x__2 = x__1 - 1

***** We apply the Graph Processor on D1 = (P1, R, f, c).

We compute a graph approximation with the following edges:

  1:  2 
  2:  2 
  3:  4 
  4:  4 
  5:  5 7 8 
  6:  6 9 10 
  7:
  8:  6 9 10 
  9:
  10: 6 9 10 
  11: 5 7 8 
  12:
  13: 6 9 10 
  14:
  15: 6 9 10 
  16:
  17: 6 9 10 

There are 4 SCCs.

Processor output: { D2 = (P2, R, f, c) ; D3 = (P3, R, f, c) ; D4 = (P4, R, f, c) ; D5 = (P5, R, f, c) }, where:

  P2. (1) u#(x, i, a) ➡ u#(x, i + 1, i * a) | i ≤ x

  P3. (1) U#(i, x) ➡ U#(i + 1, x) | i ≤ x - 1

  P4. (1) recup#(F, i, y, a) ➡ recup#(F, i + 1, y, a) | i ≤ y
      (2) recup#(helper, x__2, y, a__2) ➡ recup#(helper, x__3, y, a__1) | x__1 ≤ y ∧ a__2 = x__1 * a__1 ∧ x__2 ≤ y ∧ x__3 = x__2 + 1

  P5. (1) tailup#(F, i, y, a) ➡ tailup#(F, i + 1, y, F(i, a)) | i ≤ y

***** We apply the Integer Function Processor on D2 = (P2, R, f, c).

We use the following integer mapping:

  J(u#) = arg_1 - arg_2

We thus have:

  (1) i ≤ x ⊨ x - i > x - (i + 1) (and x - i ≥ 0)

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

Processor output: { }.

***** We apply the Integer Function Processor on D3 = (P3, R, f, c).

We use the following integer mapping:

  J(U#) = arg_2 - 1 - arg_1

We thus have:

  (1) i ≤ x - 1 ⊨ x - 1 - i > x - 1 - (i + 1) (and x - 1 - i ≥ 0)

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

Processor output: { }.

***** We apply the Theory Arguments Processor on D4 = (P4, R, f, c).

We use the following theory arguments function:

  recup# : [2, 3]

Processor output: { D6 = (P6, R, f, c) ; D7 = (P7, R, f, c) }, where:

  P6. (1) recup#(F, i, y, a) ➡ recup#(F, i + 1, y, a) | i ≤ y { a }
      (2) recup#(helper, x__2, y, a__2) ➡ recup#(helper, x__3, y, a__1) | x__1 ≤ y ∧ a__2 = x__1 * a__1 ∧ x__2 ≤ y ∧ x__3 = x__2 + 1

  P7. (1) recup#(F, i, y, a) ➡ recup#(F, i + 1, y, a) | i ≤ y

***** We apply the Integer Function Processor on D5 = (P5, R, f, c).

We use the following integer mapping:

  J(tailup#) = arg_3 - arg_2

We thus have:

  (1) i ≤ y ⊨ y - i > y - (i + 1) (and y - i ≥ 0)

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

Processor output: { }.

***** We apply the Integer Function Processor on D6 = (P6, R, f, c).

We use the following integer mapping:

  J(recup#) = arg_3 - arg_2

We thus have:

  (1) i ≤ y                                                      ⊨ y - i    > y - (i + 1) (and y - i ≥ 0)
  (2) x__1 ≤ y ∧ a__2 = x__1 * a__1 ∧ x__2 ≤ y ∧ x__3 = x__2 + 1 ⊨ y - x__2 > y - x__3    (and y - x__2 ≥ 0)

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

Processor output: { }.

***** We apply the Integer Function Processor on D7 = (P7, R, f, c).

We use the following integer mapping:

  J(recup#) = arg_3 - arg_2

We thus have:

  (1) i ≤ y ⊨ y - i > y - (i + 1) (and y - i ≥ 0)

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

Processor output: { }.