We start the process with the following equations:

  E1: (• , taildown(F, x, y, z) ≈ recup(F, x, y, z) , •)

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

This yields E2: (taildown(F, x, y, z) , taildown(F, x, y, z) ≈ recup(F, x, y, z) , recup(F, x, y, z))

We apply CASE on the constraint x ≤ y.

This yields the following new equations:

  E3: (taildown(F, x, y, z) , taildown(F, x, y, z) ≈ recup(F, x, y, z) | x ≤ y , recup(F, x, y, z))
  E4: (taildown(F, x, y, z) , taildown(F, x, y, z) ≈ recup(F, x, y, z) | ¬(x ≤ y) , recup(F, x, y, z))

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

This yields E5: (taildown(F, x, y, z) , z ≈ recup(F, x, y, z) | ¬(x ≤ y) , recup(F, x, y, z))

We apply SIMPLIFICATION to E5 with rule R5 and substitution [F := F, i := x, y := y, z := z].

This yields E6: (taildown(F, x, y, z) , z ≈ z | ¬(x ≤ y) , recup(F, x, y, z))

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

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

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

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

This yields E8: (taildown(F, x, y, z) , taildown(F, x, y1, F(z, y)) ≈ recup(F, x, y, z) | x ≤ y ∧ y1 = y - 1 , recup(F, x, y, z))

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

This yields E9: (taildown(F, x, y, z) , taildown(F, x, y1, F(z, y)) ≈ F(recup(F, x + 1, y, z), x) | x ≤ y ∧ y1 = y - 1 , recup(F, x, y, z))

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

This yields E10: (taildown(F, x, y, z) , taildown(F, x, y1, F(z, y)) ≈ F(recup(F, x1, y, z), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 , recup(F, x, y, z))

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

This yields E11: (taildown(F, x, y, z) , recup(F, x, y1, F(z, y)) ≈ F(recup(F, x1, y, z), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 , recup(F, x, y, z))

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

This yields E12: (recup(F, x, y1, F(z, y)) , recup(F, x, y1, F(z, y)) ≈ F(recup(F, x1, y, z), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 , F(recup(F, x1, y, z), x))

We apply CASE on the constraint x ≤ y1.

This yields the following new equations:

  E13: (recup(F, x, y1, F(z, y)) , recup(F, x, y1, F(z, y)) ≈ F(recup(F, x1, y, z), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , F(recup(F, x1, y, z), x))
  E14: (recup(F, x, y1, F(z, y)) , recup(F, x, y1, F(z, y)) ≈ F(recup(F, x1, y, z), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) , F(recup(F, x1, y, z), x))

We apply SIMPLIFICATION to E14 with rule R5 and substitution [F := F, i := x, y := y1, z := F(z, y)].

This yields E15: (recup(F, x, y1, F(z, y)) , F(z, y) ≈ F(recup(F, x1, y, z), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) , F(recup(F, x1, y, z), x))

We apply SIMPLIFICATION to E15 with rule R5 and substitution [F := F, i := x1, y := y, z := z].

This yields E16: (recup(F, x, y1, F(z, y)) , F(z, y) ≈ F(z, x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ ¬(x ≤ y1) , F(recup(F, x1, y, z), x))

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

We apply SIMPLIFICATION to E13 with rule R6 and substitution [F := F, i := x, y := y1, z := F(z, y)].

This yields E17: (recup(F, x, y1, F(z, y)) , F(recup(F, x + 1, y1, F(z, y)), x) ≈ F(recup(F, x1, y, z), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , F(recup(F, x1, y, z), x))

We use CALC at position l1.2.

This yields E18: (recup(F, x, y1, F(z, y)) , F(recup(F, x1, y1, F(z, y)), x) ≈ F(recup(F, x1, y, z), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , F(recup(F, x1, y, z), x))

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

This yields E19: (recup(F, x, y1, F(z, y)) , F(recup(F, x1, y1, F(z, y)), x) ≈ F(F(recup(F, x1 + 1, y, z), x1), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 , F(recup(F, x1, y, z), x))

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

This yields E20: (recup(F, x, y1, F(z, y)) , F(recup(F, x1, y1, F(z, y)), x) ≈ F(F(recup(F, x2, y, z), x1), x) | x ≤ y ∧ y1 = y - 1 ∧ x1 = x + 1 ∧ x ≤ y1 ∧ x2 = x1 + 1 , F(recup(F, x1, y, z), x))

We apply HDELETE to E20 with induction hypothesis H11 and substitution [F := F, x := x1, x1 := x2, y := y, y1 := y1, z := z].

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: f        :: Int → Int → Int
             g        :: Int → Int → Int
             recdown  :: (Int → Int → Int) → Int → Int → Int → Int
             recup    :: (Int → Int → Int) → Int → Int → Int → Int
             taildown :: (Int → Int → Int) → Int → Int → Int → Int
             tailup   :: (Int → Int → Int) → Int → Int → Int → Int

  Rules: 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
         recup(F, i, y, z) → z | i > y
         recup(F, i, y, z) → F(recup(F, i + 1, y, z), i) | i ≤ y
         recdown(F, x, i, z) → z | i < x
         recdown(F, x, i, z) → F(i, recdown(F, x, i - 1, z)) | i ≥ x
         f(x, y) → x | x > 100000
         g(x, y) → x | x > 100000
         taildown(F, x__1, y__1, z) → recup(F, x__1, y__2, F(z, y__1)) | x__1 ≤ y__1 ∧ y__2 = y__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) tailup#(F, i, y, a) ➡ tailup#(F, i + 1, y, F(i, a)) | i ≤ y
      (2) taildown#(F, x, i, a) ➡ taildown#(F, x, i - 1, F(a, i)) | i ≥ x
      (3) recup#(F, i, y, z) ➡ recup#(F, i + 1, y, z) | i ≤ y
      (4) recdown#(F, x, i, z) ➡ recdown#(F, x, i - 1, z) | i ≥ x
      (5) taildown#(F, x__1, y__1, z) ➡ recup#(F, x__1, y__2, F(z, y__1)) | x__1 ≤ y__1 ∧ y__2 = y__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: 1 
  2: 2 5 
  3: 3 
  4: 4 
  5: 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) tailup#(F, i, y, a) ➡ tailup#(F, i + 1, y, F(i, a)) | i ≤ y

  P3. (1) recup#(F, i, y, z) ➡ recup#(F, i + 1, y, z) | i ≤ y

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

  P5. (1) recdown#(F, x, i, z) ➡ recdown#(F, x, i - 1, z) | i ≥ x

***** We apply the Integer Function Processor on D2 = (P2, 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 D3 = (P3, 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 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(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: { }.