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

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 d(i, a) ≈ taildown([*], 1, i, a) to the current proof state.

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

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

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

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

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

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

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

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

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

This yields E23: (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 E24: (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 E25: (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 E25 with induction hypothesis H14 and substitution [a := a1, i := i1].

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

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

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

This yields E27: (tailup([*], x, y, a) , tailup([*], x, y, a) ≈ taildown([*], x, y, a) , taildown([*], 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) ≈ taildown([*], x, y, a) | x ≤ y , taildown([*], x, y, a))
  E29: (tailup([*], x, y, a) , tailup([*], x, y, a) ≈ taildown([*], x, y, a) | ¬(x ≤ y) , taildown([*], 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 ≈ taildown([*], x, y, a) | ¬(x ≤ y) , taildown([*], x, y, a))

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

This yields E31: (tailup([*], x, y, a) , a ≈ a | ¬(x ≤ y) , taildown([*], 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) ≈ taildown([*], x, y, a) | x ≤ y , taildown([*], 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) ≈ taildown([*], x, y, a) | x ≤ y ∧ x1 = x + 1 , taildown([*], 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) ≈ taildown([*], x, y, a) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a , taildown([*], x, y, a))

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

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

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

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

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

This yields E37: (tailup([*], x, y, a) , tailup([*], x1, y, a1) ≈ taildown([*], x, y1, a2) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y , taildown([*], 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) ≻ taildown([*], x1, y, a1) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y.

This yields E38: (tailup([*], x, y, a) , taildown([*], x1, y, a1) ≈ taildown([*], x, y1, a2) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y , taildown([*], x, y, a))

We apply INDUCT to E38, which causes taildown([*], x1, y, a1) ≈ taildown([*], x, y1, a2) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y to be added to the set H of induction hypotheses.

This yields E39: (taildown([*], x1, y, a1) , taildown([*], x1, y, a1) ≈ taildown([*], x, y1, a2) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y , taildown([*], x, y1, a2))

We apply CASE on the constraint x1 ≤ y.

This yields the following new equations:

  E40: (taildown([*], x1, y, a1) , taildown([*], x1, y, a1) ≈ taildown([*], x, y1, a2) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y ∧ x1 ≤ y , taildown([*], x, y1, a2))
  E41: (taildown([*], x1, y, a1) , taildown([*], x1, y, a1) ≈ taildown([*], x, y1, a2) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y ∧ ¬(x1 ≤ y) , taildown([*], x, y1, a2))

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

This yields E42: (taildown([*], x1, y, a1) , a1 ≈ taildown([*], x, y1, a2) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y ∧ ¬(x1 ≤ y) , taildown([*], x, y1, a2))

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

This yields E43: (taildown([*], x1, y, a1) , a1 ≈ a2 | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y ∧ ¬(x1 ≤ y) , taildown([*], x, y1, a2))

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

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

This yields E44: (taildown([*], x1, y, a1) , taildown([*], x1, y - 1, a1 * y) ≈ taildown([*], x, y1, a2) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y ∧ x1 ≤ y , taildown([*], x, y1, a2))

We use CALC at position l3.

This yields E45: (taildown([*], x1, y, a1) , taildown([*], x1, y1, a1 * y) ≈ taildown([*], x, y1, a2) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y ∧ x1 ≤ y , taildown([*], x, y1, a2))

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

This yields E46: (taildown([*], x1, y, a1) , taildown([*], x1, y1, a3) ≈ taildown([*], x, y1, a2) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y ∧ x1 ≤ y ∧ a3 = a1 * y , taildown([*], x, y1, a2))

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

This yields E47: (taildown([*], x1, y, a1) , taildown([*], x1, y1, a3) ≈ taildown([*], x, y1 - 1, a2 * y1) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y ∧ x1 ≤ y ∧ a3 = a1 * y , taildown([*], x, y1, a2))

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

This yields E48: (taildown([*], x1, y, a1) , taildown([*], x1, y1, a3) ≈ taildown([*], x, y2, a2 * y1) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y ∧ x1 ≤ y ∧ a3 = a1 * y ∧ y2 = y1 - 1 , taildown([*], x, y1, a2))

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

This yields E49: (taildown([*], x1, y, a1) , taildown([*], x1, y1, a3) ≈ taildown([*], x, y2, a4) | x ≤ y ∧ x1 = x + 1 ∧ a1 = x * a ∧ y1 = y - 1 ∧ a2 = a * y ∧ x1 ≤ y ∧ a3 = a1 * y ∧ y2 = y1 - 1 ∧ a4 = a2 * y1 , taildown([*], x, y1, a2))

We apply HDELETE to E49 with induction hypothesis H38 and substitution [a := a2, a1 := a3, a2 := a4, x := x, x1 := x1, y := y1, y1 := y2].

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

This yields E50: (factTU(x) , factTU(x) ≈ factTD(x) , factTD(x))

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

This yields E51: (factTU(x) , u(x, 1, 1) ≈ factTD(x) , factTD(x))

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

This yields E52: (factTU(x) , u(x, 1, 1) ≈ d(x, 1) , factTD(x))

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

This yields E53: (factTU(x) , tailup([*], 1, x, 1) ≈ d(x, 1) , factTD(x))

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

This yields E54: (factTU(x) , tailup([*], 1, x, 1) ≈ taildown([*], 1, x, 1) , factTD(x))

We apply HDELETE to E54 with induction hypothesis H26 and substitution [a := 1, x := 1, 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: d        :: Int → Int → Int
             factTD   :: Int → Int
             factTU   :: Int → Int
             taildown :: (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
         factTD(x) → d(x, 1)
         d(x, a) → a | x ≤ 0
         d(x, a) → d(x - 1, a * x) | x > 0
         tailup(F, i, y, a) → a | i > y
         tailup(F, i, y, a) → tailup(F, i + 1, y, F(i, a)) | i ≤ y
         taildown(F, x, i, a) → a | i < x
         taildown(F, x, i, a) → taildown(F, x, i - 1, F(a, i)) | i ≥ x
         tailup([*], x__1, y__1, a__1) → taildown([*], x__2, y__1, a__2) | x__1 ≤ y__1 ∧ x__2 = x__1 + 1 ∧ a__2 = x__1 * a__1 ∧ y__2 = y__1 - 1 ∧ a__3 = a__1 * y__1
         factTU(x) → tailup([*], 1, x, 1)
         factTD(x) → taildown([*], 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) factTD#(x) ➡ d#(x, 1) | true
      (4) d#(x, a) ➡ d#(x - 1, a * x) | x > 0
      (5) tailup#(F, i, y, a) ➡ tailup#(F, i + 1, y, F(i, a)) | i ≤ y
      (6) taildown#(F, x, i, a) ➡ taildown#(F, x, i - 1, F(a, i)) | i ≥ x
      (7) tailup#([*], x__1, y__1, a__1) ➡ taildown#([*], x__2, y__1, a__2) | x__1 ≤ y__1 ∧ x__2 = x__1 + 1 ∧ a__2 = x__1 * a__1 ∧ y__2 = y__1 - 1 ∧ a__3 = a__1 * y__1
      (8) factTU#(x) ➡ tailup#([*], 1, x, 1) | true
      (9) factTD#(x) ➡ taildown#([*], 1, x, 1) | true

***** 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 
  6: 6 
  7: 6 
  8: 5 7 
  9: 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) u#(x, i, a) ➡ u#(x, i + 1, i * a) | i ≤ x

  P3. (1) d#(x, a) ➡ d#(x - 1, a * x) | x > 0

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

  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(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 D4 = (P4, 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 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: { }.