We start the process with the following equations:

  E1: (• , factTD(x) ≈ factRD(x) , •)

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 R6 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 R7 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 taildown([*], x, y, a) ≈ recdown([*], x, y, a) to the current proof state.

This yields E14: (• , taildown([*], x, y, a) ≈ recdown([*], x, y, a) , •)

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

This yields E15: (taildown([*], x, y, a) , taildown([*], x, y, a) ≈ recdown([*], x, y, a) , recdown([*], x, y, a))

We apply CASE on the constraint x ≤ y.

This yields the following new equations:

  E16: (taildown([*], x, y, a) , taildown([*], x, y, a) ≈ recdown([*], x, y, a) | x ≤ y , recdown([*], x, y, a))
  E17: (taildown([*], x, y, a) , taildown([*], x, y, a) ≈ recdown([*], x, y, a) | ¬(x ≤ y) , recdown([*], x, y, a))

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

This yields E18: (taildown([*], x, y, a) , a ≈ recdown([*], x, y, a) | ¬(x ≤ y) , recdown([*], x, y, a))

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

This yields E19: (taildown([*], x, y, a) , a ≈ a | ¬(x ≤ y) , recdown([*], 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 R7 and substitution [F := [*], a := a, i := y, x := x].

This yields E20: (taildown([*], x, y, a) , taildown([*], x, y - 1, a * y) ≈ recdown([*], x, y, a) | x ≤ y , recdown([*], x, y, a))

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

This yields E21: (taildown([*], x, y, a) , taildown([*], x, y1, a * y) ≈ recdown([*], x, y, a) | x ≤ y ∧ y1 = y - 1 , recdown([*], x, y, a))

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

This yields E22: (taildown([*], x, y, a) , taildown([*], x, y1, a1) ≈ recdown([*], x, y, a) | x ≤ y ∧ y1 = y - 1 ∧ a1 = a * y , recdown([*], x, y, a))

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

This yields E23: (taildown([*], x, y, a) , taildown([*], x, y1, a1) ≈ y * recdown([*], x, y - 1, a) | x ≤ y ∧ y1 = y - 1 ∧ a1 = a * y , recdown([*], x, y, a))

We use CALC at position r2.3.

This yields E24: (taildown([*], x, y, a) , taildown([*], x, y1, a1) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ y1 = y - 1 ∧ a1 = a * y , recdown([*], x, y, a))

We apply HYPOTHESIS to E24 with induction hypothesis H14 and substitution [a := a1, x := x, y := y1].  To this end, we impose the requirement that taildown([*], x, y, a) ≻ recdown([*], x, y1, a1) | x ≤ y ∧ y1 = y - 1 ∧ a1 = a * y.

This yields E25: (taildown([*], x, y, a) , recdown([*], x, y1, a1) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ y1 = y - 1 ∧ a1 = a * y , recdown([*], x, y, a))

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

This yields E26: (taildown([*], x, y, a) , recdown([*], x, y1, a1) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ a1 = a * y , recdown([*], x, y, a))

We apply INDUCT to E26, which causes recdown([*], x, y1, a1) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ a1 = a * y to be added to the set H of induction hypotheses.

This yields E27: (recdown([*], x, y1, a1) , recdown([*], x, y1, a1) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ a1 = a * y , y * recdown([*], x, y1, a))

We apply CASE on the constraint x ≤ y1.

This yields the following new equations:

  E28: (recdown([*], x, y1, a1) , recdown([*], x, y1, a1) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ a1 = a * y ∧ x ≤ y1 , y * recdown([*], x, y1, a))
  E29: (recdown([*], x, y1, a1) , recdown([*], x, y1, a1) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ a1 = a * y ∧ ¬(x ≤ y1) , y * recdown([*], x, y1, a))

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

This yields E30: (recdown([*], x, y1, a1) , a1 ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ a1 = a * y ∧ ¬(x ≤ y1) , y * recdown([*], x, y1, a))

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

This yields E31: (recdown([*], x, y1, a1) , a1 ≈ y * a | x ≤ y ∧ a1 = a * y ∧ ¬(x ≤ y1) , y * recdown([*], x, y1, a))

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

This yields E32: (recdown([*], x, y1, a1) , a1 ≈ i1 | x ≤ y ∧ a1 = a * y ∧ ¬(x ≤ y1) ∧ i1 = y * a , y * recdown([*], x, y1, a))

We observe that x ≤ y ∧ a1 = a * y ∧ ¬(x ≤ y1) ∧ i1 = y * a ⊨ a1 = i1, and may therefore apply EQ-DELETION to remove E32 from the proof state.

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

This yields E33: (recdown([*], x, y1, a1) , y1 * recdown([*], x, y1 - 1, a1) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ a1 = a * y ∧ x ≤ y1 , y * recdown([*], x, y1, a))

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

This yields E34: (recdown([*], x, y1, a1) , y1 * recdown([*], x, y2, a1) ≈ y * recdown([*], x, y1, a) | x ≤ y ∧ a1 = a * y ∧ x ≤ y1 ∧ y2 = y1 - 1 , y * recdown([*], x, y1, a))

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

This yields E35: (recdown([*], x, y1, a1) , y1 * recdown([*], x, y2, a1) ≈ y * (y1 * recdown([*], x, y1 - 1, a)) | x ≤ y ∧ a1 = a * y ∧ x ≤ y1 ∧ y2 = y1 - 1 , y * recdown([*], x, y1, a))

We use CALC at position r2.2.3.

This yields E36: (recdown([*], x, y1, a1) , y1 * recdown([*], x, y2, a1) ≈ y * (y1 * recdown([*], x, y2, a)) | x ≤ y ∧ a1 = a * y ∧ x ≤ y1 ∧ y2 = y1 - 1 , y * recdown([*], x, y1, a))

We apply HYPOTHESIS to E36 with induction hypothesis H26 and substitution [a := a, a1 := a1, x := x, y := y, y1 := y2].  To this end, we impose the requirement that recdown([*], x, y1, a1) ≻ y1 * (y * recdown([*], x, y2, a)) | x ≤ y ∧ a1 = a * y ∧ x ≤ y1 ∧ y2 = y1 - 1.

This yields E37: (recdown([*], x, y1, a1) , y1 * (y * recdown([*], x, y2, a)) ≈ y * (y1 * recdown([*], x, y2, a)) | x ≤ y ∧ a1 = a * y ∧ x ≤ y1 ∧ y2 = y1 - 1 , y * recdown([*], x, y1, a))

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

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

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

This yields E39: (x * (y * z) , x * (y * z) ≈ y * (x * z) , y * (x * 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 E37 with induction hypothesis H38 and substitution [x := y1, y := y, z := recdown([*], x, y2, a)].  To this end, we impose the requirement that recdown([*], x, y1, a1) ≻ y * (y1 * recdown([*], x, y2, a)) | x ≤ y ∧ a1 = a * y ∧ x ≤ y1 ∧ y2 = y1 - 1.

This yields E40: (recdown([*], x, y1, a1) , y * (y1 * recdown([*], x, y2, a)) ≈ y * (y1 * recdown([*], x, y2, a)) | x ≤ y ∧ a1 = a * y ∧ x ≤ y1 ∧ y2 = y1 - 1 , y * recdown([*], x, y1, a))

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

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

This yields E41: (factTD(x) , factTD(x) ≈ factRD(x) , factRD(x))

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

This yields E42: (factTD(x) , d(x, 1) ≈ factRD(x) , factRD(x))

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

This yields E43: (factTD(x) , taildown([*], 1, x, 1) ≈ factRD(x) , factRD(x))

We apply HYPOTHESIS to E43 with induction hypothesis H14 and substitution [a := 1, x := 1, y := x].  To this end, we impose the requirement that factTD(x) ≻ recdown([*], 1, x, 1).

This yields E44: (factTD(x) , recdown([*], 1, x, 1) ≈ factRD(x) , factRD(x))

We apply INDUCT to E44, which causes recdown([*], 1, x, 1) ≈ factRD(x) to be added to the set H of induction hypotheses.

This yields E45: (recdown([*], 1, x, 1) , recdown([*], 1, x, 1) ≈ factRD(x) , factRD(x))

We apply CASE on the constraint x > 1.

This yields the following new equations:

  E46: (recdown([*], 1, x, 1) , recdown([*], 1, x, 1) ≈ factRD(x) | x > 1 , factRD(x))
  E47: (recdown([*], 1, x, 1) , recdown([*], 1, x, 1) ≈ factRD(x) | ¬(x > 1) , factRD(x))

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

This yields E48: (recdown([*], 1, x, 1) , recdown([*], 1, x, 1) ≈ 1 | ¬(x > 1) , factRD(x))

We apply CASE on the constraint x = 1.

This yields the following new equations:

  E49: (recdown([*], 1, x, 1) , recdown([*], 1, x, 1) ≈ 1 | ¬(x > 1) ∧ x = 1 , factRD(x))
  E50: (recdown([*], 1, x, 1) , recdown([*], 1, x, 1) ≈ 1 | ¬(x > 1) ∧ ¬(x = 1) , factRD(x))

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

This yields E51: (recdown([*], 1, x, 1) , 1 ≈ 1 | ¬(x > 1) ∧ ¬(x = 1) , factRD(x))

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

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

This yields E52: (recdown([*], 1, x, 1) , x * recdown([*], 1, x - 1, 1) ≈ 1 | ¬(x > 1) ∧ x = 1 , factRD(x))

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

This yields E53: (recdown([*], 1, x, 1) , x * recdown([*], 1, x1, 1) ≈ 1 | ¬(x > 1) ∧ x = 1 ∧ x1 = x - 1 , factRD(x))

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

This yields E54: (recdown([*], 1, x, 1) , x * 1 ≈ 1 | ¬(x > 1) ∧ x = 1 ∧ x1 = x - 1 , factRD(x))

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

This yields E55: (recdown([*], 1, x, 1) , x2 ≈ 1 | ¬(x > 1) ∧ x = 1 ∧ x1 = x - 1 ∧ x2 = x * 1 , factRD(x))

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

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

This yields E56: (recdown([*], 1, x, 1) , x * recdown([*], 1, x - 1, 1) ≈ factRD(x) | x > 1 , factRD(x))

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

This yields E57: (recdown([*], 1, x, 1) , x * recdown([*], 1, x1, 1) ≈ factRD(x) | x > 1 ∧ x1 = x - 1 , factRD(x))

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

This yields E58: (recdown([*], 1, x, 1) , x * (x1 * recdown([*], 1, x1 - 1, 1)) ≈ factRD(x) | x > 1 ∧ x1 = x - 1 , factRD(x))

We use ALTER to add x2 = x1 - 1 to the constraint, and then use CALC at position l2.2.3.

This yields E59: (recdown([*], 1, x, 1) , x * (x1 * recdown([*], 1, x2, 1)) ≈ factRD(x) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 , factRD(x))

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

This yields E60: (recdown([*], 1, x, 1) , x * (x1 * recdown([*], 1, x2, 1)) ≈ x * factRD(x - 1) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 , factRD(x))

We use CALC at position r2.1.

This yields E61: (recdown([*], 1, x, 1) , x * (x1 * recdown([*], 1, x2, 1)) ≈ x * factRD(x1) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 , factRD(x))

We apply HYPOTHESIS to E61 with induction hypothesis H44 and substitution [x := x2].  To this end, we impose the requirement that recdown([*], 1, x, 1) ≻ x * (x1 * factRD(x2)) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1.

This yields E62: (recdown([*], 1, x, 1) , x * (x1 * factRD(x2)) ≈ x * factRD(x1) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 , factRD(x))

We apply INDUCT to E62, which causes x * (x1 * factRD(x2)) ≈ x * factRD(x1) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 to be added to the set H of induction hypotheses.

This yields E63: (x * (x1 * factRD(x2)) , x * (x1 * factRD(x2)) ≈ x * factRD(x1) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 , x * factRD(x1))

We apply CASE on the constraint x > 2.

This yields the following new equations:

  E64: (x * (x1 * factRD(x2)) , x * (x1 * factRD(x2)) ≈ x * factRD(x1) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 ∧ x > 2 , x * factRD(x1))
  E65: (x * (x1 * factRD(x2)) , x * (x1 * factRD(x2)) ≈ x * factRD(x1) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 ∧ ¬(x > 2) , x * factRD(x1))

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

This yields E66: (x * (x1 * factRD(x2)) , x * (x1 * 1) ≈ x * factRD(x1) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 ∧ ¬(x > 2) , x * factRD(x1))

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

This yields E67: (x * (x1 * factRD(x2)) , x * x3 ≈ x * factRD(x1) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 ∧ ¬(x > 2) ∧ x3 = x1 * 1 , x * factRD(x1))

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

This yields E68: (x * (x1 * factRD(x2)) , x4 ≈ x * factRD(x1) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 ∧ ¬(x > 2) ∧ x3 = x1 * 1 ∧ x4 = x * x3 , x * factRD(x1))

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

This yields E69: (x * (x1 * factRD(x2)) , x4 ≈ x * 1 | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 ∧ ¬(x > 2) ∧ x3 = x1 * 1 ∧ x4 = x * x3 , x * factRD(x1))

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

This yields E70: (x * (x1 * factRD(x2)) , x4 ≈ x5 | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 ∧ ¬(x > 2) ∧ x3 = x1 * 1 ∧ x4 = x * x3 ∧ x5 = x * 1 , x * factRD(x1))

We observe that x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 ∧ ¬(x > 2) ∧ x3 = x1 * 1 ∧ x4 = x * x3 ∧ x5 = x * 1 ⊨ x4 = x5, and may therefore apply EQ-DELETION to remove E70 from the proof state.

We apply SIMPLIFICATION to E64 with rule R5 and substitution [x := x1].

This yields E71: (x * (x1 * factRD(x2)) , x * (x1 * factRD(x2)) ≈ x * (x1 * factRD(x1 - 1)) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 ∧ x > 2 , x * factRD(x1))

We use CALC at position r2.2.1.

This yields E72: (x * (x1 * factRD(x2)) , x * (x1 * factRD(x2)) ≈ x * (x1 * factRD(x2)) | x > 1 ∧ x1 = x - 1 ∧ x2 = x1 - 1 ∧ x > 2 , x * factRD(x1))

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

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

This yields E73: (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 E74: (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 E75: (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 E76: (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 E76 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: d        :: Int → Int → Int
             factRD   :: Int → Int
             factTD   :: Int → Int
             recdown  :: (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
         factRD(x) → 1 | x ≤ 1
         factRD(x) → x * factRD(x - 1) | 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
         recdown(F, x, i, a) → a | i < x
         recdown(F, x, i, a) → F(i, recdown(F, x, i - 1, a)) | i ≥ x
         taildown([*], x, y__1, a__1) → recdown([*], x, y__2, a__2) | x ≤ y__1 ∧ y__2 = y__1 - 1 ∧ a__2 = a__1 * y__1
         recdown([*], x, y__2, a__2) → y__2 * (y__1 * recdown([*], x, y__3, a__1)) | x ≤ y__1 ∧ a__2 = a__1 * y__1 ∧ x ≤ y__2 ∧ y__3 = y__2 - 1
         recdown([*], x, y__2, a__2) → y__1 * (y__2 * recdown([*], x, y__3, a__1)) | x ≤ y__1 ∧ a__2 = a__1 * y__1 ∧ x ≤ y__2 ∧ y__3 = y__2 - 1
         factTD(x) → taildown([*], 1, x, 1)
         factTD(x) → recdown([*], 1, x, 1)
         recdown([*], 1, x__1, 1) → x__1 * (x__2 * factRD(x__3)) | x__1 > 1 ∧ x__2 = x__1 - 1 ∧ x__3 = x__2 - 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)  factRD#(x) ➡ factRD#(x - 1) | x > 1
      (4)  taildown#(F, x, i, a) ➡ taildown#(F, x, i - 1, F(a, i)) | i ≥ x
      (5)  recdown#(F, x, i, a) ➡ recdown#(F, x, i - 1, a) | i ≥ x
      (6)  taildown#([*], x, y__1, a__1) ➡ recdown#([*], x, y__2, a__2) | x ≤ y__1 ∧ y__2 = y__1 - 1 ∧ a__2 = a__1 * y__1
      (7)  recdown#([*], x, y__2, a__2) ➡ recdown#([*], x, y__3, a__1) | x ≤ y__1 ∧ a__2 = a__1 * y__1 ∧ x ≤ y__2 ∧ y__3 = y__2 - 1
      (8)  recdown#([*], x, y__2, a__2) ➡ recdown#([*], x, y__3, a__1) | x ≤ y__1 ∧ a__2 = a__1 * y__1 ∧ x ≤ y__2 ∧ y__3 = y__2 - 1
      (9)  factTD#(x) ➡ taildown#([*], 1, x, 1) | true
      (10) factTD#(x) ➡ recdown#([*], 1, x, 1) | true
      (11) recdown#([*], 1, x__1, 1) ➡ factRD#(x__3) | x__1 > 1 ∧ x__2 = x__1 - 1 ∧ x__3 = x__2 - 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:  3 
  4:  4 6 
  5:  5 7 8 11 
  6:  5 7 8 
  7:  5 7 8 11 
  8:  5 7 8 11 
  9:  4 6 
  10: 5 7 8 11 
  11: 3 

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) factRD#(x) ➡ factRD#(x - 1) | x > 1

  P4. (1) recdown#(F, x, i, a) ➡ recdown#(F, x, i - 1, a) | i ≥ x
      (2) recdown#([*], x, y__2, a__2) ➡ recdown#([*], x, y__3, a__1) | x ≤ y__1 ∧ a__2 = a__1 * y__1 ∧ x ≤ y__2 ∧ y__3 = y__2 - 1
      (3) recdown#([*], x, y__2, a__2) ➡ recdown#([*], x, y__3, a__1) | x ≤ y__1 ∧ a__2 = a__1 * y__1 ∧ x ≤ y__2 ∧ y__3 = y__2 - 1

  P5. (1) taildown#(F, x, i, a) ➡ taildown#(F, x, i - 1, F(a, i)) | i ≥ x

***** 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(factRD#) = arg_1

We thus have:

  (1) x > 1 ⊨ 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 Theory Arguments Processor on D4 = (P4, R, f, c).

We use the following theory arguments function:

  recdown# : [2, 3]

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

  P6. (1) recdown#(F, x, i, a) ➡ recdown#(F, x, i - 1, a) | i ≥ x { a }
      (2) recdown#([*], x, y__2, a__2) ➡ recdown#([*], x, y__3, a__1) | x ≤ y__1 ∧ a__2 = a__1 * y__1 ∧ x ≤ y__2 ∧ y__3 = y__2 - 1
      (3) recdown#([*], x, y__2, a__2) ➡ recdown#([*], x, y__3, a__1) | x ≤ y__1 ∧ a__2 = a__1 * y__1 ∧ x ≤ y__2 ∧ y__3 = y__2 - 1

  P7. (1) recdown#(F, x, i, a) ➡ recdown#(F, x, i - 1, a) | i ≥ x

***** 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)

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(recdown#) = arg_3 - arg_2

We thus have:

  (1) i ≥ x                                                      ⊨ i - x    > i - 1 - x (and i - x ≥ 0)
  (2) x ≤ y__1 ∧ a__2 = a__1 * y__1 ∧ x ≤ y__2 ∧ y__3 = y__2 - 1 ⊨ y__2 - x > y__3 - x  (and y__2 - x ≥ 0)
  (3) x ≤ y__1 ∧ a__2 = a__1 * y__1 ∧ x ≤ y__2 ∧ y__3 = y__2 - 1 ⊨ y__2 - x > y__3 - x  (and y__2 - 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 D7 = (P7, R, f, c).

We use the following integer mapping:

  J(recdown#) = arg_3 - arg_2

We thus have:

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

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

Processor output: { }.