Remark 
=====================================================
The ordering requirements 

taildown([*], x, i, a) ≻ taildown(helper, x, i1, a1) | i ≥ x ∧ i1 = i - 1 ∧ a1 = a * i ∧ a2 = i * a
factTD(x) ≻ recup(helper, 1, x1, x2) | x ≥ 1 ∧ x1 = x - 1 ∧ x2 = 1 * x

are not actually needed: in the current version of Cora it is not yet possible to apply H54 and H26 with hdelete, so hypothesis was applied instead (causing the ordering requirements). 
=====================================================


We start the process with the following equations:

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

We apply POSTULATE to add the lemma equation d(i, a) ≈ taildown([*], 1, i, a) to the current proof state.

This yields E2: (• , d(i, a) ≈ taildown([*], 1, i, a) , •)

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

This yields E3: (d(i, a) , d(i, a) ≈ taildown([*], 1, i, a) , taildown([*], 1, i, a))

We apply CASE on the constraint i ≥ 1.

This yields the following new equations:

  E4: (d(i, a) , d(i, a) ≈ taildown([*], 1, i, a) | i ≥ 1 , taildown([*], 1, i, a))
  E5: (d(i, a) , d(i, a) ≈ taildown([*], 1, i, a) | ¬(i ≥ 1) , taildown([*], 1, i, a))

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

This yields E6: (d(i, a) , a ≈ taildown([*], 1, i, a) | ¬(i ≥ 1) , taildown([*], 1, i, a))

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

This yields E7: (d(i, a) , a ≈ a | ¬(i ≥ 1) , taildown([*], 1, i, 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, x := i].

This yields E8: (d(i, a) , d(i - 1, a * i) ≈ taildown([*], 1, i, a) | i ≥ 1 , taildown([*], 1, i, a))

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

This yields E9: (d(i, a) , d(i1, a * i) ≈ taildown([*], 1, i, a) | i ≥ 1 ∧ i1 = i - 1 , taildown([*], 1, i, a))

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

This yields E10: (d(i, a) , d(i1, a1) ≈ taildown([*], 1, i, a) | i ≥ 1 ∧ i1 = i - 1 ∧ a1 = a * i , taildown([*], 1, i, a))

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

This yields E11: (d(i, a) , d(i1, a1) ≈ taildown([*], 1, i - 1, a * i) | i ≥ 1 ∧ i1 = i - 1 ∧ a1 = a * i , taildown([*], 1, i, a))

We use CALC at position r3.

This yields E12: (d(i, a) , d(i1, a1) ≈ taildown([*], 1, i1, a * i) | i ≥ 1 ∧ i1 = i - 1 ∧ a1 = a * i , taildown([*], 1, i, a))

We use CALC at position r4.

This yields E13: (d(i, a) , d(i1, a1) ≈ taildown([*], 1, i1, a1) | i ≥ 1 ∧ i1 = i - 1 ∧ a1 = a * i , taildown([*], 1, i, a))

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

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 ALTER to add x1 = x - 1 to the constraint, and then use CALC at position r3.

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 taildown(F, x, i, z) ≈ recup(F, x, i, z) to the current proof state.

This yields E26: (• , taildown(F, x, i, z) ≈ recup(F, x, i, z) , •)

We apply INDUCT to E26, which causes taildown(F, x, i, z) ≈ recup(F, x, i, z) to be added to the set H of induction hypotheses.

This yields E27: (taildown(F, x, i, z) , taildown(F, x, i, z) ≈ recup(F, x, i, z) , recup(F, x, i, z))

We apply CASE on the constraint x ≤ i.

This yields the following new equations:

  E28: (taildown(F, x, i, z) , taildown(F, x, i, z) ≈ recup(F, x, i, z) | x ≤ i , recup(F, x, i, z))
  E29: (taildown(F, x, i, z) , taildown(F, x, i, z) ≈ recup(F, x, i, z) | ¬(x ≤ i) , recup(F, x, i, z))

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

This yields E30: (taildown(F, x, i, z) , z ≈ recup(F, x, i, z) | ¬(x ≤ i) , recup(F, x, i, z))

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

This yields E31: (taildown(F, x, i, z) , z ≈ z | ¬(x ≤ i) , recup(F, x, i, z))

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 := F, a := z, i := i, x := x].

This yields E32: (taildown(F, x, i, z) , taildown(F, x, i - 1, F(z, i)) ≈ recup(F, x, i, z) | x ≤ i , recup(F, x, i, z))

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

This yields E33: (taildown(F, x, i, z) , taildown(F, x, i1, F(z, i)) ≈ recup(F, x, i, z) | x ≤ i ∧ i1 = i - 1 , recup(F, x, i, z))

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

This yields E34: (taildown(F, x, i, z) , taildown(F, x, i1, F(z, i)) ≈ F(recup(F, x + 1, i, z), x) | x ≤ i ∧ i1 = i - 1 , recup(F, x, i, z))

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

This yields E35: (taildown(F, x, i, z) , taildown(F, x, i1, F(z, i)) ≈ F(recup(F, x1, i, z), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 , recup(F, x, i, z))

We apply HYPOTHESIS to E35 with induction hypothesis H26 and substitution [F := F, i := i1, x := x, z := F(z, i)].  To this end, we impose the requirement that taildown(F, x, i, z) ≻ recup(F, x, i1, F(z, i)) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1.

This yields E36: (taildown(F, x, i, z) , recup(F, x, i1, F(z, i)) ≈ F(recup(F, x1, i, z), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 , recup(F, x, i, z))

We apply INDUCT to E36, which causes recup(F, x, i1, F(z, i)) ≈ F(recup(F, x1, i, z), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 to be added to the set H of induction hypotheses.

This yields E37: (recup(F, x, i1, F(z, i)) , recup(F, x, i1, F(z, i)) ≈ F(recup(F, x1, i, z), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 , F(recup(F, x1, i, z), x))

We apply CASE on the constraint x ≤ i1.

This yields the following new equations:

  E38: (recup(F, x, i1, F(z, i)) , recup(F, x, i1, F(z, i)) ≈ F(recup(F, x1, i, z), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 ∧ x ≤ i1 , F(recup(F, x1, i, z), x))
  E39: (recup(F, x, i1, F(z, i)) , recup(F, x, i1, F(z, i)) ≈ F(recup(F, x1, i, z), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ i1) , F(recup(F, x1, i, z), x))

We apply SIMPLIFICATION to E39 with rule R9 and substitution [F := F, a := F(z, i), i := x, y := i1].

This yields E40: (recup(F, x, i1, F(z, i)) , F(z, i) ≈ F(recup(F, x1, i, z), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ i1) , F(recup(F, x1, i, z), x))

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

This yields E41: (recup(F, x, i1, F(z, i)) , F(z, i) ≈ F(z, x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ i1) , F(recup(F, x1, i, z), x))

We observe that x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ i1) ⊨ i = x, and may therefore apply EQ-DELETION to remove E41 from the proof state.

We apply SIMPLIFICATION to E38 with rule R10 and substitution [F := F, a := F(z, i), i := x, y := i1].

This yields E42: (recup(F, x, i1, F(z, i)) , F(recup(F, x + 1, i1, F(z, i)), x) ≈ F(recup(F, x1, i, z), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 ∧ x ≤ i1 , F(recup(F, x1, i, z), x))

We use CALC at position l1.2.

This yields E43: (recup(F, x, i1, F(z, i)) , F(recup(F, x1, i1, F(z, i)), x) ≈ F(recup(F, x1, i, z), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 ∧ x ≤ i1 , F(recup(F, x1, i, z), x))

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

This yields E44: (recup(F, x, i1, F(z, i)) , F(recup(F, x1, i1, F(z, i)), x) ≈ F(F(recup(F, x1 + 1, i, z), x1), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 ∧ x ≤ i1 , F(recup(F, x1, i, z), x))

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

This yields E45: (recup(F, x, i1, F(z, i)) , F(recup(F, x1, i1, F(z, i)), x) ≈ F(F(recup(F, x2, i, z), x1), x) | x ≤ i ∧ i1 = i - 1 ∧ x1 = x + 1 ∧ x ≤ i1 ∧ x2 = x1 + 1 , F(recup(F, x1, i, z), x))

We apply HDELETE to E45 with induction hypothesis H36 and substitution [F := F, i := i, i1 := i1, x := x1, x1 := x2, z := z].

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

This yields E46: (factTD(x) , factTD(x) ≈ factRU(x) | x ≥ 1 , factRU(x))

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

This yields E47: (factTD(x) , d(x, 1) ≈ factRU(x) | x ≥ 1 , factRU(x))

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

This yields E48: (factTD(x) , d(x - 1, 1 * x) ≈ factRU(x) | x ≥ 1 , factRU(x))

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

This yields E49: (factTD(x) , d(x1, 1 * x) ≈ factRU(x) | x ≥ 1 ∧ x1 = x - 1 , factRU(x))

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

This yields E50: (factTD(x) , d(x1, x2) ≈ factRU(x) | x ≥ 1 ∧ x1 = x - 1 ∧ x2 = 1 * x , factRU(x))

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

This yields E51: (factTD(x) , d(x1, x2) ≈ U(1, x) | x ≥ 1 ∧ x1 = x - 1 ∧ x2 = 1 * x , factRU(x))

We apply HYPOTHESIS to E51 with induction hypothesis H2 and substitution [a := x2, i := x1].  To this end, we impose the requirement that factTD(x) ≻ taildown([*], 1, x1, x2) | x ≥ 1 ∧ x1 = x - 1 ∧ x2 = 1 * x.

This yields E52: (factTD(x) , taildown([*], 1, x1, x2) ≈ U(1, x) | x ≥ 1 ∧ x1 = x - 1 ∧ x2 = 1 * x , factRU(x))

We apply HYPOTHESIS to E52 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 ∧ x2 = 1 * x.

This yields E53: (factTD(x) , taildown([*], 1, x1, x2) ≈ recup(helper, 1, x1, x) | x ≥ 1 ∧ x1 = x - 1 ∧ x2 = 1 * x , factRU(x))

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

This yields E54: (• , taildown([*], x, i, a) ≈ taildown(helper, x, i, a) , •)

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

This yields E55: (taildown([*], x, i, a) , taildown([*], x, i, a) ≈ taildown(helper, x, i, a) , taildown(helper, x, i, a))

We apply CASE on the constraint i ≥ x.

This yields the following new equations:

  E56: (taildown([*], x, i, a) , taildown([*], x, i, a) ≈ taildown(helper, x, i, a) | i ≥ x , taildown(helper, x, i, a))
  E57: (taildown([*], x, i, a) , taildown([*], x, i, a) ≈ taildown(helper, x, i, a) | ¬(i ≥ x) , taildown(helper, x, i, a))

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

This yields E58: (taildown([*], x, i, a) , a ≈ taildown(helper, x, i, a) | ¬(i ≥ x) , taildown(helper, x, i, a))

We apply SIMPLIFICATION to E58 with rule R7 and substitution [F := helper, a := a, i := i, x := x].

This yields E59: (taildown([*], x, i, a) , a ≈ a | ¬(i ≥ x) , taildown(helper, x, i, a))

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

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

This yields E60: (taildown([*], x, i, a) , taildown([*], x, i - 1, a * i) ≈ taildown(helper, x, i, a) | i ≥ x , taildown(helper, x, i, a))

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

This yields E61: (taildown([*], x, i, a) , taildown([*], x, i1, a * i) ≈ taildown(helper, x, i, a) | i ≥ x ∧ i1 = i - 1 , taildown(helper, x, i, a))

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

This yields E62: (taildown([*], x, i, a) , taildown([*], x, i1, a1) ≈ taildown(helper, x, i, a) | i ≥ x ∧ i1 = i - 1 ∧ a1 = a * i , taildown(helper, x, i, a))

We apply SIMPLIFICATION to E62 with rule R8 and substitution [F := helper, a := a, i := i, x := x].

This yields E63: (taildown([*], x, i, a) , taildown([*], x, i1, a1) ≈ taildown(helper, x, i - 1, helper(a, i)) | i ≥ x ∧ i1 = i - 1 ∧ a1 = a * i , taildown(helper, x, i, a))

We use CALC at position r3.

This yields E64: (taildown([*], x, i, a) , taildown([*], x, i1, a1) ≈ taildown(helper, x, i1, helper(a, i)) | i ≥ x ∧ i1 = i - 1 ∧ a1 = a * i , taildown(helper, x, i, a))

We apply SIMPLIFICATION to E64 with rule R11 and substitution [x := a, y := i].

This yields E65: (taildown([*], x, i, a) , taildown([*], x, i1, a1) ≈ taildown(helper, x, i1, i * a) | i ≥ x ∧ i1 = i - 1 ∧ a1 = a * i , taildown(helper, x, i, a))

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

This yields E66: (taildown([*], x, i, a) , taildown([*], x, i1, a1) ≈ taildown(helper, x, i1, a2) | i ≥ x ∧ i1 = i - 1 ∧ a1 = a * i ∧ a2 = i * a , taildown(helper, x, i, a))

We apply HYPOTHESIS to E66 with induction hypothesis H54 and substitution [a := a1, i := i1, x := x].  To this end, we impose the requirement that taildown([*], x, i, a) ≻ taildown(helper, x, i1, a1) | i ≥ x ∧ i1 = i - 1 ∧ a1 = a * i ∧ a2 = i * a.

This yields E67: (taildown([*], x, i, a) , taildown(helper, x, i1, a1) ≈ taildown(helper, x, i1, a2) | i ≥ x ∧ i1 = i - 1 ∧ a1 = a * i ∧ a2 = i * a , taildown(helper, x, i, a))

We observe that i ≥ x ∧ i1 = i - 1 ∧ a1 = a * i ∧ a2 = i * a ⊨ a1 = a2, and may therefore apply EQ-DELETION to remove E67 from the proof state.

We apply HYPOTHESIS to E53 with induction hypothesis H54 and substitution [a := x2, i := x1, x := 1].  To this end, we impose the requirement that factTD(x) ≻ taildown(helper, 1, x1, x2) | x ≥ 1 ∧ x1 = x - 1 ∧ x2 = 1 * x.

This yields E68: (factTD(x) , taildown(helper, 1, x1, x2) ≈ recup(helper, 1, x1, x) | x ≥ 1 ∧ x1 = x - 1 ∧ x2 = 1 * x , factRU(x))

We apply HYPOTHESIS to E68 with induction hypothesis H26 and substitution [F := helper, i := x1, x := 1, z := x2].  To this end, we impose the requirement that factTD(x) ≻ recup(helper, 1, x1, x2) | x ≥ 1 ∧ x1 = x - 1 ∧ x2 = 1 * x.

This yields E69: (factTD(x) , recup(helper, 1, x1, x2) ≈ recup(helper, 1, x1, x) | x ≥ 1 ∧ x1 = x - 1 ∧ x2 = 1 * x , factRU(x))

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

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
             d        :: Int → Int → Int
             factRU   :: Int → Int
             factTD   :: Int → Int
             helper   :: Int → Int → Int
             recup    :: (Int → Int → Int) → Int → Int → Int → Int
             taildown :: (Int → Int → Int) → Int → Int → Int → Int

  Rules: factTD(x) → d(x, 1)
         d(x, a) → a | x ≤ 0
         d(x, a) → d(x - 1, a * x) | x > 0
         factRU(x) → U(1, x)
         U(i, x) → x | i > x - 1
         U(i, x) → i * U(i + 1, x) | i ≤ x - 1
         taildown(F, x, i, a) → a | i < x
         taildown(F, x, i, a) → taildown(F, x, i - 1, F(a, i)) | i ≥ x
         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
         taildown(F, x__1, i__1, z) → recup(F, x__1, i__2, F(z, i__1)) | x__1 ≤ i__1 ∧ i__2 = i__1 - 1 ∧ x__2 = x__1 + 1
         factTD(x__1) → taildown([*], 1, x__2, x__3) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__1
         factRU(x__1) → recup(helper, 1, x__2, x__1) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__1
         taildown([*], x, i__1, a__1) → taildown(helper, x, i__2, a__2) | i__1 ≥ x ∧ i__2 = i__1 - 1 ∧ a__2 = a__1 * i__1 ∧ a__3 = i__1 * a__1
         factTD(x__1) → taildown(helper, 1, x__2, x__3) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__1
         factTD(x__1) → recup(helper, 1, x__2, x__3) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__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)  factTD#(x) ➡ d#(x, 1) | true
      (2)  d#(x, a) ➡ d#(x - 1, a * x) | x > 0
      (3)  factRU#(x) ➡ U#(1, x) | true
      (4)  U#(i, x) ➡ U#(i + 1, x) | i ≤ x - 1
      (5)  taildown#(F, x, i, a) ➡ taildown#(F, x, i - 1, F(a, i)) | i ≥ x
      (6)  recup#(F, i, y, a) ➡ recup#(F, i + 1, y, a) | i ≤ y
      (7)  taildown#(F, x__1, i__1, z) ➡ recup#(F, x__1, i__2, F(z, i__1)) | x__1 ≤ i__1 ∧ i__2 = i__1 - 1 ∧ x__2 = x__1 + 1
      (8)  factTD#(x__1) ➡ taildown#([*], 1, x__2, x__3) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__1
      (9)  factRU#(x__1) ➡ helper#(fresh1, fresh2) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__1
      (10) factRU#(x__1) ➡ recup#(helper, 1, x__2, x__1) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__1
      (11) taildown#([*], x, i__1, a__1) ➡ helper#(fresh1, fresh2) | i__1 ≥ x ∧ i__2 = i__1 - 1 ∧ a__2 = a__1 * i__1 ∧ a__3 = i__1 * a__1
      (12) taildown#([*], x, i__1, a__1) ➡ taildown#(helper, x, i__2, a__2) | i__1 ≥ x ∧ i__2 = i__1 - 1 ∧ a__2 = a__1 * i__1 ∧ a__3 = i__1 * a__1
      (13) factTD#(x__1) ➡ helper#(fresh1, fresh2) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__1
      (14) factTD#(x__1) ➡ taildown#(helper, 1, x__2, x__3) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__1
      (15) factTD#(x__1) ➡ helper#(fresh1, fresh2) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__1
      (16) factTD#(x__1) ➡ recup#(helper, 1, x__2, x__3) | x__1 ≥ 1 ∧ x__2 = x__1 - 1 ∧ x__3 = 1 * x__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 11 12 
  6:  6 
  7:  6 
  8:  5 7 11 12 
  9:
  10: 6 
  11:
  12: 5 7 
  13:
  14: 5 7 
  15:
  16: 6 

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) d#(x, a) ➡ d#(x - 1, a * x) | x > 0

  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

  P5. (1) taildown#(F, x, i, a) ➡ taildown#(F, x, i - 1, F(a, i)) | i ≥ x
      (2) taildown#([*], x, i__1, a__1) ➡ taildown#(helper, x, i__2, a__2) | i__1 ≥ x ∧ i__2 = i__1 - 1 ∧ a__2 = a__1 * i__1 ∧ a__3 = i__1 * a__1

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

We use the following integer mapping:

  J(d#) = arg_1

We thus have:

  (1) x > 0 ⊨ x > x - 1 (and x ≥ 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 Integer Function Processor on D4 = (P4, 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: { }.

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

We use the following integer mapping:

  J(taildown#) = arg_3 - arg_2

We thus have:

  (1) i ≥ x                                                                ⊨ i - x    > i - 1 - x (and i - x ≥ 0)
  (2) i__1 ≥ x ∧ i__2 = i__1 - 1 ∧ a__2 = a__1 * i__1 ∧ a__3 = i__1 * a__1 ⊨ i__1 - x > i__2 - x  (and i__1 - x ≥ 0)

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

Processor output: { }.