We consider termination of the LCTRS with only rule scheme Calc:

  Signature: eval_0  :: Int -> o -> o -> Int -> o
             eval_1  :: Int -> Int -> Int -> Int -> o
             eval_11 :: Int -> Int -> Int -> Int -> o
             eval_2  :: Int -> Int -> Int -> Int -> o
             eval_3  :: Int -> Int -> Int -> Int -> o
             eval_5  :: Int -> Int -> Int -> Int -> o
             eval_7  :: Int -> Int -> Int -> Int -> o
             eval_9  :: Int -> Int -> Int -> Int -> o

  Rules: eval_0(x, y1, y2, z) -> eval_1(x, x, 1, z)
         eval_1(x, y1, y2, z) -> eval_2(x, y1, y2, y1 - 10) | y1 > 100
         eval_1(x, y1, y2, z) -> eval_3(x, y1, y2, z) | y1 <= 100
         eval_3(x, y1, y2, z) -> eval_3(x, y1 + 11, y2 + 1, z) | y1 <= 100
         eval_3(x, y1, y2, z) -> eval_5(x, y1, y2, z) | y1 > 100
         eval_5(x, y1, y2, z) -> eval_7(x, y1 - 10, y2 - 1, z) | y2 > 1
         eval_7(x, y1, y2, z) -> eval_5(x, y1, y2, y1 - 10) | y1 > 100 /\ y2 = 1
         eval_7(x, y1, y2, z) -> eval_9(x, y1, y2, z) | y1 <= 100 \/ not (y2 = 1)
         eval_9(x, y1, y2, z) -> eval_11(x, y1 - 10, y2 - 1, z) | y1 > 100
         eval_9(x, y1, y2, z) -> eval_11(x, y1, y2, z) | y1 <= 100
         eval_11(x, y1, y2, z) -> eval_5(x, y1 + 11, y2 + 1, z)

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)  eval_0#(x, y1, y2, z) => eval_1#(x, x, 1, z)
      (2)  eval_1#(x, y1, y2, z) => eval_3#(x, y1, y2, z) | y1 <= 100
      (3)  eval_3#(x, y1, y2, z) => eval_3#(x, y1 + 11, y2 + 1, z) | y1 <= 100
      (4)  eval_3#(x, y1, y2, z) => eval_5#(x, y1, y2, z) | y1 > 100
      (5)  eval_5#(x, y1, y2, z) => eval_7#(x, y1 - 10, y2 - 1, z) | y2 > 1
      (6)  eval_7#(x, y1, y2, z) => eval_5#(x, y1, y2, y1 - 10) | y1 > 100 /\ y2 = 1
      (7)  eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | y1 <= 100 \/ not (y2 = 1)
      (8)  eval_9#(x, y1, y2, z) => eval_11#(x, y1 - 10, y2 - 1, z) | y1 > 100
      (9)  eval_9#(x, y1, y2, z) => eval_11#(x, y1, y2, z) | y1 <= 100
      (10) eval_11#(x, y1, y2, z) => eval_5#(x, y1 + 11, y2 + 1, z)

***** We apply the Constraint Modification Processor on D1 = (P1, R, f, c).

We replace eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | y1 <= 100 \/ not (y2 = 1) by:

  eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | y1 <= 100 { y1, y2 }
  eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | not (y2 = 1) { y1, y2 }

Processor output: { D2 = (P2, R, f, c) }, where:

  P2. (1)  eval_0#(x, y1, y2, z) => eval_1#(x, x, 1, z)
      (2)  eval_1#(x, y1, y2, z) => eval_3#(x, y1, y2, z) | y1 <= 100
      (3)  eval_3#(x, y1, y2, z) => eval_3#(x, y1 + 11, y2 + 1, z) | y1 <= 100
      (4)  eval_3#(x, y1, y2, z) => eval_5#(x, y1, y2, z) | y1 > 100
      (5)  eval_5#(x, y1, y2, z) => eval_7#(x, y1 - 10, y2 - 1, z) | y2 > 1
      (6)  eval_7#(x, y1, y2, z) => eval_5#(x, y1, y2, y1 - 10) | y1 > 100 /\ y2 = 1
      (7)  eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | y1 <= 100 { y1, y2 }
      (8)  eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | not (y2 = 1) { y1, y2 }
      (9)  eval_9#(x, y1, y2, z) => eval_11#(x, y1 - 10, y2 - 1, z) | y1 > 100
      (10) eval_9#(x, y1, y2, z) => eval_11#(x, y1, y2, z) | y1 <= 100
      (11) eval_11#(x, y1, y2, z) => eval_5#(x, y1 + 11, y2 + 1, z)

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

We compute a graph approximation with the following edges:

  1:  2 
  2:  3 
  3:  3 4 
  4:  5 
  5:  6 7 8 
  6:
  7:  10 
  8:  9 10 
  9:  11 
  10: 11 
  11: 5 

There are 2 SCCs.

Processor output: { D3 = (P3, R, f, c) ; D4 = (P4, R, f, c) }, where:

  P3. (1) eval_5#(x, y1, y2, z) => eval_7#(x, y1 - 10, y2 - 1, z) | y2 > 1
      (2) eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | y1 <= 100 { y1, y2 }
      (3) eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | not (y2 = 1) { y1, y2 }
      (4) eval_9#(x, y1, y2, z) => eval_11#(x, y1 - 10, y2 - 1, z) | y1 > 100
      (5) eval_9#(x, y1, y2, z) => eval_11#(x, y1, y2, z) | y1 <= 100
      (6) eval_11#(x, y1, y2, z) => eval_5#(x, y1 + 11, y2 + 1, z)

  P4. (1) eval_3#(x, y1, y2, z) => eval_3#(x, y1 + 11, y2 + 1, z) | y1 <= 100

***** We apply the Theory Arguments Processor on D3 = (P3, R, f, c).

We use the following theory arguments function:

  eval_11# : [1, 2, 3, 4]
  eval_5#  : [1, 2, 3, 4]
  eval_7#  : [1, 2, 3, 4]
  eval_9#  : [1, 2, 3, 4]

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

  P5. (1) eval_5#(x, y1, y2, z) => eval_7#(x, y1 - 10, y2 - 1, z) | y2 > 1
      (2) eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | y1 <= 100 { x, y1, y2, z }
      (3) eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | not (y2 = 1) { x, y1, y2, z }
      (4) eval_9#(x, y1, y2, z) => eval_11#(x, y1 - 10, y2 - 1, z) | y1 > 100 { x, y1, y2, z }
      (5) eval_9#(x, y1, y2, z) => eval_11#(x, y1, y2, z) | y1 <= 100 { x, y1, y2, z }
      (6) eval_11#(x, y1, y2, z) => eval_5#(x, y1 + 11, y2 + 1, z) { x, y1, y2, z }

  P6. (1) eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | y1 <= 100 { y1, y2 }
      (2) eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | not (y2 = 1) { y1, y2 }
      (3) eval_9#(x, y1, y2, z) => eval_11#(x, y1 - 10, y2 - 1, z) | y1 > 100
      (4) eval_9#(x, y1, y2, z) => eval_11#(x, y1, y2, z) | y1 <= 100
      (5) eval_11#(x, y1, y2, z) => eval_5#(x, y1 + 11, y2 + 1, z)

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

We use the following integer mapping:

  J(eval_3#) = 100 - arg_2

We thus have:

  (1) y1 <= 100 |= 100 - y1 > 100 - (y1 + 11) (and 100 - y1 >= 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 D5 = (P5, R, f, c).

We use the following theory arguments function:

  eval_11# : [1, 2, 3, 4]
  eval_5#  : [1, 2, 3, 4]
  eval_7#  : [1, 2, 3, 4]
  eval_9#  : [1, 2, 3, 4]

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

  P7. (1) eval_5#(x, y1, y2, z) => eval_7#(x, y1 - 10, y2 - 1, z) | y2 > 1 { x, y1, y2, z }
      (2) eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | y1 <= 100 { x, y1, y2, z }
      (3) eval_7#(x, y1, y2, z) => eval_9#(x, y1, y2, z) | not (y2 = 1) { x, y1, y2, z }
      (4) eval_9#(x, y1, y2, z) => eval_11#(x, y1 - 10, y2 - 1, z) | y1 > 100 { x, y1, y2, z }
      (5) eval_9#(x, y1, y2, z) => eval_11#(x, y1, y2, z) | y1 <= 100 { x, y1, y2, z }
      (6) eval_11#(x, y1, y2, z) => eval_5#(x, y1 + 11, y2 + 1, z) { x, y1, y2, z }

  P8. (1) eval_5#(x, y1, y2, z) => eval_7#(x, y1 - 10, y2 - 1, z) | y2 > 1

***** We apply the Graph Processor on D6 = (P6, R, f, c).

We compute a graph approximation with the following edges:

  1: 4 
  2: 3 4 
  3: 5 
  4: 5 
  5:

As there are no SCCs, this DP problem is removed.

Processor output: { }.

***** No progress could be made on DP problem D7 = (P7, R, f, c).