We start the process with the following equations:

  E1: (• , factTU(x) ≈ factRD(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 i ≤ x.

This yields the following new equations:

  E4: (u(x, i, a) , u(x, i, a) ≈ tailup([*], i, x, a) | i ≤ x , tailup([*], i, x, a))
  E5: (u(x, i, a) , u(x, i, a) ≈ tailup([*], i, x, a) | ¬(i ≤ x) , 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) | ¬(i ≤ x) , tailup([*], i, x, a))

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

This yields E7: (u(x, i, a) , a ≈ a | ¬(i ≤ x) , 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) | i ≤ x , 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) | i ≤ x ∧ 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) | i ≤ x ∧ i1 = i + 1 ∧ a1 = i * a , tailup([*], i, x, a))

We apply SIMPLIFICATION to E10 with rule R7 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) | i ≤ x ∧ 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) | i ≤ x ∧ 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) | i ≤ x ∧ 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 factRD(i) ≈ recdown([*], 2, i, 1) to the current proof state.

This yields E14: (• , factRD(i) ≈ recdown([*], 2, i, 1) , •)

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

This yields E15: (factRD(i) , factRD(i) ≈ recdown([*], 2, i, 1) , recdown([*], 2, i, 1))

We apply CASE on the constraint i > 1.

This yields the following new equations:

  E16: (factRD(i) , factRD(i) ≈ recdown([*], 2, i, 1) | i > 1 , recdown([*], 2, i, 1))
  E17: (factRD(i) , factRD(i) ≈ recdown([*], 2, i, 1) | ¬(i > 1) , recdown([*], 2, i, 1))

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

This yields E18: (factRD(i) , 1 ≈ recdown([*], 2, i, 1) | ¬(i > 1) , recdown([*], 2, i, 1))

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

This yields E19: (factRD(i) , 1 ≈ 1 | ¬(i > 1) , recdown([*], 2, i, 1))

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 R5 and substitution [x := i].

This yields E20: (factRD(i) , i * factRD(i - 1) ≈ recdown([*], 2, i, 1) | i > 1 , recdown([*], 2, i, 1))

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

This yields E21: (factRD(i) , i * factRD(i1) ≈ recdown([*], 2, i, 1) | i > 1 ∧ i1 = i - 1 , recdown([*], 2, i, 1))

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

This yields E22: (factRD(i) , i * factRD(i1) ≈ i * recdown([*], 2, i - 1, 1) | i > 1 ∧ i1 = i - 1 , recdown([*], 2, i, 1))

We use CALC at position r2.3.

This yields E23: (factRD(i) , i * factRD(i1) ≈ i * recdown([*], 2, i1, 1) | i > 1 ∧ i1 = i - 1 , recdown([*], 2, i, 1))

We apply HDELETE to E23 with induction hypothesis H14 and substitution [i := i1].

We apply POSTULATE to add the lemma equation tailup(F, i, y, z) ≈ recdown(F, i, y, z) to the current proof state.

This yields E24: (• , tailup(F, i, y, z) ≈ recdown(F, i, y, z) , •)

We apply INDUCT to E24, which causes tailup(F, i, y, z) ≈ recdown(F, i, y, z) to be added to the set H of induction hypotheses.

This yields E25: (tailup(F, i, y, z) , tailup(F, i, y, z) ≈ recdown(F, i, y, z) , recdown(F, i, y, z))

We apply CASE on the constraint i ≤ y.

This yields the following new equations:

  E26: (tailup(F, i, y, z) , tailup(F, i, y, z) ≈ recdown(F, i, y, z) | i ≤ y , recdown(F, i, y, z))
  E27: (tailup(F, i, y, z) , tailup(F, i, y, z) ≈ recdown(F, i, y, z) | ¬(i ≤ y) , recdown(F, i, y, z))

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

This yields E28: (tailup(F, i, y, z) , z ≈ recdown(F, i, y, z) | ¬(i ≤ y) , recdown(F, i, y, z))

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

This yields E29: (tailup(F, i, y, z) , z ≈ z | ¬(i ≤ y) , recdown(F, i, y, z))

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

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

This yields E30: (tailup(F, i, y, z) , tailup(F, i + 1, y, F(i, z)) ≈ recdown(F, i, y, z) | i ≤ y , recdown(F, i, y, z))

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

This yields E31: (tailup(F, i, y, z) , tailup(F, i1, y, F(i, z)) ≈ recdown(F, i, y, z) | i ≤ y ∧ i1 = i + 1 , recdown(F, i, y, z))

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

This yields E32: (tailup(F, i, y, z) , tailup(F, i1, y, F(i, z)) ≈ F(y, recdown(F, i, y - 1, z)) | i ≤ y ∧ i1 = i + 1 , recdown(F, i, y, z))

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

This yields E33: (tailup(F, i, y, z) , tailup(F, i1, y, F(i, z)) ≈ F(y, recdown(F, i, y1, z)) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 , recdown(F, i, y, z))

We apply HYPOTHESIS to E33 with induction hypothesis H24 and substitution [F := F, i := i1, y := y, z := F(i, z)].  To this end, we impose the requirement that tailup(F, i, y, z) ≻ recdown(F, i1, y, F(i, z)) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1.

This yields E34: (tailup(F, i, y, z) , recdown(F, i1, y, F(i, z)) ≈ F(y, recdown(F, i, y1, z)) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 , recdown(F, i, y, z))

We apply INDUCT to E34, which causes recdown(F, i1, y, F(i, z)) ≈ F(y, recdown(F, i, y1, z)) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 to be added to the set H of induction hypotheses.

This yields E35: (recdown(F, i1, y, F(i, z)) , recdown(F, i1, y, F(i, z)) ≈ F(y, recdown(F, i, y1, z)) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 , F(y, recdown(F, i, y1, z)))

We apply CASE on the constraint i1 ≤ y.

This yields the following new equations:

  E36: (recdown(F, i1, y, F(i, z)) , recdown(F, i1, y, F(i, z)) ≈ F(y, recdown(F, i, y1, z)) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 ∧ i1 ≤ y , F(y, recdown(F, i, y1, z)))
  E37: (recdown(F, i1, y, F(i, z)) , recdown(F, i1, y, F(i, z)) ≈ F(y, recdown(F, i, y1, z)) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 ∧ ¬(i1 ≤ y) , F(y, recdown(F, i, y1, z)))

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

This yields E38: (recdown(F, i1, y, F(i, z)) , F(i, z) ≈ F(y, recdown(F, i, y1, z)) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 ∧ ¬(i1 ≤ y) , F(y, recdown(F, i, y1, z)))

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

This yields E39: (recdown(F, i1, y, F(i, z)) , F(i, z) ≈ F(y, z) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 ∧ ¬(i1 ≤ y) , F(y, recdown(F, i, y1, z)))

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

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

This yields E40: (recdown(F, i1, y, F(i, z)) , F(y, recdown(F, i1, y - 1, F(i, z))) ≈ F(y, recdown(F, i, y1, z)) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 ∧ i1 ≤ y , F(y, recdown(F, i, y1, z)))

We use CALC at position l2.3.

This yields E41: (recdown(F, i1, y, F(i, z)) , F(y, recdown(F, i1, y1, F(i, z))) ≈ F(y, recdown(F, i, y1, z)) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 ∧ i1 ≤ y , F(y, recdown(F, i, y1, z)))

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

This yields E42: (recdown(F, i1, y, F(i, z)) , F(y, recdown(F, i1, y1, F(i, z))) ≈ F(y, F(y1, recdown(F, i, y1 - 1, z))) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 ∧ i1 ≤ y , F(y, recdown(F, i, y1, z)))

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

This yields E43: (recdown(F, i1, y, F(i, z)) , F(y, recdown(F, i1, y1, F(i, z))) ≈ F(y, F(y1, recdown(F, i, y2, z))) | i ≤ y ∧ i1 = i + 1 ∧ y1 = y - 1 ∧ i1 ≤ y ∧ y2 = y1 - 1 , F(y, recdown(F, i, y1, z)))

We apply HDELETE to E43 with induction hypothesis H34 and substitution [F := F, i := i, i1 := i1, y := y1, y1 := y2, z := z].

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

This yields E44: (factTU(x) , factTU(x) ≈ factRD(x) | x ≥ 1 , factRD(x))

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

This yields E45: (factTU(x) , u(x, 1, 1) ≈ factRD(x) | x ≥ 1 , factRD(x))

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

This yields E46: (factTU(x) , u(x, 1 + 1, 1 * 1) ≈ factRD(x) | x ≥ 1 , factRD(x))

We use CALC at position l2.

This yields E47: (factTU(x) , u(x, 2, 1 * 1) ≈ factRD(x) | x ≥ 1 , factRD(x))

We use CALC at position l3.

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

We apply HYPOTHESIS to E48 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 E49: (factTU(x) , tailup([*], 2, x, 1) ≈ factRD(x) | x ≥ 1 , factRD(x))

We apply HYPOTHESIS to E49 with induction hypothesis H14 and substitution [i := x].  To this end, we impose the requirements that factRD(x) ≻ recdown([*], 2, x, 1) | x ≥ 1 and factTU(x) ≻ recdown([*], 2, x, 1) | x ≥ 1.

This yields E50: (factTU(x) , tailup([*], 2, x, 1) ≈ recdown([*], 2, x, 1) | x ≥ 1 , factRD(x))

We apply HDELETE to E50 with induction hypothesis H24 and substitution [F := [*], i := 2, y := x, z := 1].

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: factRD  :: Int → Int
             factTU  :: Int → Int
             recdown :: (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
         factRD(x) → 1 | x ≤ 1
         factRD(x) → x * factRD(x - 1) | 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
         recdown(F, x, i, a) → a | i < x
         recdown(F, x, i, a) → F(i, recdown(F, x, i - 1, a)) | i ≥ x
         tailup(F, i__1, y__1, z) → recdown(F, i__2, y__1, F(i__1, z)) | i__1 ≤ y__1 ∧ i__2 = i__1 + 1 ∧ y__2 = y__1 - 1
         factTU(x) → tailup([*], 2, x, 1) | x ≥ 1
         factRD(x) → recdown([*], 2, x, 1) | x ≥ 1
         factTU(x) → recdown([*], 2, x, 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) factTU#(x) ➡ u#(x, 1, 1) | true
      (2) u#(x, i, a) ➡ u#(x, i + 1, i * a) | i ≤ x
      (3) factRD#(x) ➡ factRD#(x - 1) | x > 1
      (4) tailup#(F, i, y, a) ➡ tailup#(F, i + 1, y, F(i, a)) | i ≤ y
      (5) recdown#(F, x, i, a) ➡ recdown#(F, x, i - 1, a) | i ≥ x
      (6) tailup#(F, i__1, y__1, z) ➡ recdown#(F, i__2, y__1, F(i__1, z)) | i__1 ≤ y__1 ∧ i__2 = i__1 + 1 ∧ y__2 = y__1 - 1
      (7) factTU#(x) ➡ tailup#([*], 2, x, 1) | x ≥ 1
      (8) factRD#(x) ➡ recdown#([*], 2, x, 1) | x ≥ 1
      (9) factTU#(x) ➡ recdown#([*], 2, x, 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: 3 8 
  4: 4 6 
  5: 5 
  6: 5 
  7: 4 6 
  8: 5 
  9: 5 

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) recdown#(F, x, i, a) ➡ recdown#(F, x, i - 1, a) | i ≥ x

  P4. (1) factRD#(x) ➡ factRD#(x - 1) | x > 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(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: { }.

***** We apply the Integer Function Processor on D4 = (P4, 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 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: { }.