Remark
=====================================================================================================
The poof uses the following lemma 

u(x, j, a) ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0

of which all equalities-invariants and the inequality-invariant i > 0 in the constraint can be 
generated by the heuristics of matrix invariants. The invariant x > i - 1 cannot be generated by a 
method being published yet. 
======================================================================================================


We start the process with the following equations:

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

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

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

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

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

We apply INDUCT to E3, 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 E4: (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:

  E5: (U(i, x) , U(i, x) ≈ recup(helper, i, x1, x) | x1 = x - 1 ∧ i ≤ x - 1 , recup(helper, i, x1, x))
  E6: (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 E6 with rule R5 and substitution [i := i, x := x].

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

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

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

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

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

This yields E9: (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 E10: (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 E10 with rule R10 and substitution [F := helper, a := x, i := i, y := x1].

This yields E11: (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 E12: (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 E12 with rule R11 and substitution [x := recup(helper, i1, x1, x), y := i].

This yields E13: (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 E13 with induction hypothesis H3 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 E14: (• , tailup([*], x, y, a) ≈ recup(helper, x, y, a) , •)

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

This yields E15: (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:

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

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

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

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

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

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

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

This yields E20: (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 E21: (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 E22: (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 E22 with rule R10 and substitution [F := helper, a := a, i := x, y := y].

This yields E23: (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 E24: (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 E24 with rule R11 and substitution [x := recup(helper, x1, y, a), y := x].

This yields E25: (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 E25 with induction hypothesis H14 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 E26: (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 E26 by x ≤ y ∧ a1 = x * a.

This yields E27: (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 E27, 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 E28: (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:

  E29: (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))
  E30: (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 E30 with rule R9 and substitution [F := helper, a := a1, i := x1, y := y].

This yields E31: (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 E31 with rule R9 and substitution [F := helper, a := a, i := x1, y := y].

This yields E32: (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 E33: (recup(helper, x1, y, a1) , a1 ≈ a1 | x ≤ y ∧ a1 = x * a ∧ ¬(x1 ≤ y) , x * recup(helper, x1, y, a))

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

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

This yields E34: (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 E35: (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 E35 with rule R11 and substitution [x := recup(helper, x2, y, a1), y := x1].

This yields E36: (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 E36 with rule R10 and substitution [F := helper, a := a, i := x1, y := y].

This yields E37: (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 E38: (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 E38 with rule R11 and substitution [x := recup(helper, x2, y, a), y := x1].

This yields E39: (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 E39 with induction hypothesis H27 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 E40: (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 E41: (• , x * (y * z) ≈ y * (x * z) , •)

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

This yields E42: (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 E43: (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 E44: (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 E45: (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 E46: (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 E46 from the proof state.

We apply HDELETE to E40 with induction hypothesis H41 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 E47: (factTU(x) , factTU(x) ≈ factRU(x) | x ≥ 1 , factRU(x))

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

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

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

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

We use CALC at position l2.

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

We use CALC at position l3.

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

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

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

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

This yields E53: (factTU(x) , u(x, 2, 1) ≈ U(1, x) | x ≥ 1 ∧ x1 = x - 1 , factRU(x))

We apply HYPOTHESIS to E53 with induction hypothesis H3 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 E54: (factTU(x) , u(x, 2, 1) ≈ recup(helper, 1, x1, x) | x ≥ 1 ∧ x1 = x - 1 , factRU(x))

We apply HYPOTHESIS to E54 with induction hypothesis H14^{-1} and substitution [a := x, x := 1, y := x1].  To this end, we impose the requirement that factRU(x) ≻ tailup([*], 1, x1, x) | x ≥ 1 ∧ x1 = x - 1.

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

We apply POSTULATE to add the lemma equation u(x, j, a) ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 to the current proof state.

This yields E56: (• , u(x, j, a) ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 , •)

We apply INDUCT to E56, which causes u(x, j, a) ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 to be added to the set H of induction hypotheses.

This yields E57: (u(x, j, a) , u(x, j, a) ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 , tailup([*], i, x1, b))

We apply CASE on the constraint j ≤ x.

This yields the following new equations:

  E58: (u(x, j, a) , u(x, j, a) ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ j ≤ x , tailup([*], i, x1, b))
  E59: (u(x, j, a) , u(x, j, a) ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ ¬(j ≤ x) , tailup([*], i, x1, b))

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

This yields E60: (u(x, j, a) , a ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ ¬(j ≤ x) , tailup([*], i, x1, b))

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

This yields E61: (u(x, j, a) , a ≈ b | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ ¬(j ≤ x) , tailup([*], i, x1, b))

We observe that x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ ¬(j ≤ x) ⊨ a = b, and may therefore apply EQ-DELETION to remove E61 from the proof state.

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

This yields E62: (u(x, j, a) , u(x, j + 1, j * a) ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ j ≤ x , tailup([*], i, x1, b))

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

This yields E63: (u(x, j, a) , u(x, j1, j * a) ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ j ≤ x ∧ j1 = j + 1 , tailup([*], i, x1, b))

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

This yields E64: (u(x, j, a) , u(x, j1, a1) ≈ tailup([*], i, x1, b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ j ≤ x ∧ j1 = j + 1 ∧ a1 = j * a , tailup([*], i, x1, b))

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

This yields E65: (u(x, j, a) , u(x, j1, a1) ≈ tailup([*], i + 1, x1, i * b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ j ≤ x ∧ j1 = j + 1 ∧ a1 = j * a , tailup([*], i, x1, b))

We use CALC at position r2.

This yields E66: (u(x, j, a) , u(x, j1, a1) ≈ tailup([*], j, x1, i * b) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ j ≤ x ∧ j1 = j + 1 ∧ a1 = j * a , tailup([*], i, x1, b))

We use ALTER to add a2 = i * b to the constraint, and then use CALC at position r4.

This yields E67: (u(x, j, a) , u(x, j1, a1) ≈ tailup([*], j, x1, a2) | x1 = x - 1 ∧ j = i + 1 ∧ b * i = a * x ∧ x > i - 1 ∧ i > 0 ∧ j ≤ x ∧ j1 = j + 1 ∧ a1 = j * a ∧ a2 = i * b , tailup([*], i, x1, b))

We apply HDELETE to E67 with induction hypothesis H56 and substitution [a := a1, b := a2, i := j, j := j1, x := x, x1 := x1].

We apply HDELETE to E55 with induction hypothesis H56 and substitution [a := 1, b := x, i := 1, j := 2, x := x, x1 := x1].

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
         factRU(x__1) → recup(helper, 1, x__2, x__1) | x__1 ≥ 1 ∧ x__2 = x__1 - 1
         factRU(x__1) → tailup([*], 1, x__2, x__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) factRU#(x__1) ➡ helper#(fresh1, fresh2) | x__1 ≥ 1 ∧ x__2 = x__1 - 1
      (12) factRU#(x__1) ➡ recup#(helper, 1, x__2, x__1) | x__1 ≥ 1 ∧ x__2 = x__1 - 1
      (13) factRU#(x__1) ➡ tailup#([*], 1, x__2, x__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:
  12: 6 9 10 
  13: 5 7 8 

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: { }.