We consider universal computability 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) | x = x /\ z = z
         eval_1(x, y1, y2, z) -> eval_2(x, y1, y2, y1 - 10) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z
         eval_1(x, y1, y2, z) -> eval_3(x, y1, y2, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z
         eval_3(x, y1, y2, z) -> eval_3(x, y1 + 11, y2 + 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z
         eval_3(x, y1, y2, z) -> eval_5(x, y1, y2, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z
         eval_5(x, y1, y2, z) -> eval_7(x, y1 - 10, y2 - 1, z) | y2 > 1 /\ x = x /\ y1 = y1 /\ z = z
         eval_7(x, y1, y2, z) -> eval_5(x, y1, y2, y1 - 10) | y1 > 100 /\ y2 = 1 /\ x = x /\ z = z
         eval_7(x, y1, y2, z) -> eval_9(x, y1, y2, z) | (y1 <= 100 \/ not (y2 = 1)) /\ x = x /\ z = z
         eval_9(x, y1, y2, z) -> eval_11(x, y1 - 10, y2 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z
         eval_9(x, y1, y2, z) -> eval_11(x, y1, y2, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z
         eval_11(x, y1, y2, z) -> eval_5(x, y1 + 11, y2 + 1, z) | x = x /\ y1 = y1 /\ y2 = y2 /\ z = 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 UNION R_?, i, c), where:

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

***** We apply the Constraint Modification Processor on D1 = (P1, R UNION R_?, i, c).

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

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

Processor output: { D2 = (P2, R UNION R_?, i, c) }, where:

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

***** We apply the Graph Processor on D2 = (P2, R UNION R_?, i, 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 UNION R_?, i, c) ; D4 = (P4, R UNION R_?, i, c) }, where:

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

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

***** We apply the Chaining Processor Processor on D3 = (P3, R UNION R_?, i, c).

We chain DPs according to the following mapping:


  eval_9#(x, y1, y2, z) => eval_5#(x, y1 - 10 + 11, y2 - 1 + 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z)  is obtained by chaining  eval_9#(x, y1, y2, z) => eval_11#(x, y1 - 10, y2 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z and eval_11#(x', y1', y2', z') => eval_5#(x', y1' + 11, y2' + 1, z') | x' = x' /\ y1' = y1' /\ y2' = y2' /\ z' = z'
  eval_9#(x, y1, y2, z) => eval_5#(x, y1 + 11, y2 + 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z)                            is obtained by chaining  eval_9#(x, y1, y2, z) => eval_11#(x, y1, y2, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z         and eval_11#(x', y1', y2', z') => eval_5#(x', y1' + 11, y2' + 1, z') | x' = x' /\ y1' = y1' /\ y2' = y2' /\ z' = z'


The following DPs were deleted:

eval_9#(x, y1, y2, z) => eval_11#(x, y1 - 10, y2 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z

eval_9#(x, y1, y2, z) => eval_11#(x, y1, y2, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z

eval_11#(x, y1, y2, z) => eval_5#(x, y1 + 11, y2 + 1, z) | x = x /\ y1 = y1 /\ y2 = y2 /\ z = z


By chaining, we added 2 DPs and removed 3 DPs.

Processor output: { D5 = (P5, R UNION R_?, i, c) }, where:

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

***** We apply the Integer Function Processor on D4 = (P4, R UNION R_?, i, c).

We use the following integer mapping:

  J(eval_3#) = 100 - arg_2

We thus have:

  (1) y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z |= 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 Chaining Processor Processor on D5 = (P5, R UNION R_?, i, c).

We chain DPs according to the following mapping:


  eval_9#(x, y1, y2, z) => eval_7#(x, y1 - 10 + 11 - 10, y2 - 1 + 1 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) /\ (y2 - 1 + 1 > 1 /\ x = x /\ y1 - 10 + 11 = y1 - 10 + 11 /\ z = z)  is obtained by chaining  eval_9#(x, y1, y2, z) => eval_5#(x, y1 - 10 + 11, y2 - 1 + 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) and eval_5#(x', y1', y2', z') => eval_7#(x', y1' - 10, y2' - 1, z') | y2' > 1 /\ x' = x' /\ y1' = y1' /\ z' = z'
  eval_9#(x, y1, y2, z) => eval_7#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z)                                          is obtained by chaining  eval_9#(x, y1, y2, z) => eval_5#(x, y1 + 11, y2 + 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z)                           and eval_5#(x', y1', y2', z') => eval_7#(x', y1' - 10, y2' - 1, z') | y2' > 1 /\ x' = x' /\ y1' = y1' /\ z' = z'


The following DPs were deleted:

eval_9#(x, y1, y2, z) => eval_5#(x, y1 - 10 + 11, y2 - 1 + 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z)

eval_9#(x, y1, y2, z) => eval_5#(x, y1 + 11, y2 + 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z)

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


By chaining, we added 2 DPs and removed 3 DPs.

Processor output: { D6 = (P6, R UNION R_?, i, c) }, where:

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

***** We apply the Chaining Processor Processor on D6 = (P6, R UNION R_?, i, c).

We chain DPs according to the following mapping:


  eval_9#(x, y1, y2, z) => eval_9#(x, y1 - 10 + 11 - 10, y2 - 1 + 1 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) /\ (y2 - 1 + 1 > 1 /\ x = x /\ y1 - 10 + 11 = y1 - 10 + 11 /\ z = z) /\ (y1 - 10 + 11 - 10 <= 100 /\ x = x /\ z = z)  is obtained by chaining  eval_9#(x, y1, y2, z) => eval_7#(x, y1 - 10 + 11 - 10, y2 - 1 + 1 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) /\ (y2 - 1 + 1 > 1 /\ x = x /\ y1 - 10 + 11 = y1 - 10 + 11 /\ z = z) and eval_7#(x', y1', y2', z') => eval_9#(x', y1', y2', z') | y1' <= 100 /\ x' = x' /\ z' = z' { x', y1', y2', z' }
  eval_9#(x, y1, y2, z) => eval_9#(x, y1 - 10 + 11 - 10, y2 - 1 + 1 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) /\ (y2 - 1 + 1 > 1 /\ x = x /\ y1 - 10 + 11 = y1 - 10 + 11 /\ z = z) /\ (not (y2 - 1 + 1 - 1 = 1) /\ x = x /\ z = z)  is obtained by chaining  eval_9#(x, y1, y2, z) => eval_7#(x, y1 - 10 + 11 - 10, y2 - 1 + 1 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) /\ (y2 - 1 + 1 > 1 /\ x = x /\ y1 - 10 + 11 = y1 - 10 + 11 /\ z = z) and eval_7#(x', y1', y2', z') => eval_9#(x', y1', y2', z') | not (y2' = 1) /\ x' = x' /\ z' = z' { x', y1', y2', z' }
  eval_9#(x, y1, y2, z) => eval_9#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (y1 + 11 - 10 <= 100 /\ x = x /\ z = z)                                               is obtained by chaining  eval_9#(x, y1, y2, z) => eval_7#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z)                                         and eval_7#(x', y1', y2', z') => eval_9#(x', y1', y2', z') | y1' <= 100 /\ x' = x' /\ z' = z' { x', y1', y2', z' }
  eval_9#(x, y1, y2, z) => eval_9#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (not (y2 + 1 - 1 = 1) /\ x = x /\ z = z)                                              is obtained by chaining  eval_9#(x, y1, y2, z) => eval_7#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z)                                         and eval_7#(x', y1', y2', z') => eval_9#(x', y1', y2', z') | not (y2' = 1) /\ x' = x' /\ z' = z' { x', y1', y2', z' }


The following DPs were deleted:

eval_9#(x, y1, y2, z) => eval_7#(x, y1 - 10 + 11 - 10, y2 - 1 + 1 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) /\ (y2 - 1 + 1 > 1 /\ x = x /\ y1 - 10 + 11 = y1 - 10 + 11 /\ z = z)

eval_9#(x, y1, y2, z) => eval_7#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z)

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

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


By chaining, we added 4 DPs and removed 4 DPs.

Processor output: { D7 = (P7, R UNION R_?, i, c) }, where:

  P7. (1) eval_9#(x, y1, y2, z) => eval_9#(x, y1 - 10 + 11 - 10, y2 - 1 + 1 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) /\ (y2 - 1 + 1 > 1 /\ x = x /\ y1 - 10 + 11 = y1 - 10 + 11 /\ z = z) /\ (y1 - 10 + 11 - 10 <= 100 /\ x = x /\ z = z)
      (2) eval_9#(x, y1, y2, z) => eval_9#(x, y1 - 10 + 11 - 10, y2 - 1 + 1 - 1, z) | y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) /\ (y2 - 1 + 1 > 1 /\ x = x /\ y1 - 10 + 11 = y1 - 10 + 11 /\ z = z) /\ (not (y2 - 1 + 1 - 1 = 1) /\ x = x /\ z = z)
      (3) eval_9#(x, y1, y2, z) => eval_9#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (y1 + 11 - 10 <= 100 /\ x = x /\ z = z)
      (4) eval_9#(x, y1, y2, z) => eval_9#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (not (y2 + 1 - 1 = 1) /\ x = x /\ z = z)

***** We apply the Integer Function Processor on D7 = (P7, R UNION R_?, i, c).

We use the following integer mapping:

  J(eval_9#) = arg_3 - 1 + 1 - 1

We thus have:

  (1) y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) /\ (y2 - 1 + 1 > 1 /\ x = x /\ y1 - 10 + 11 = y1 - 10 + 11 /\ z = z) /\ (y1 - 10 + 11 - 10 <= 100 /\ x = x /\ z = z) |= y2 - 1 + 1 - 1 >  y2 - 1 + 1 - 1 - 1 + 1 - 1 (and y2 - 1 + 1 - 1 >= 0)
  (2) y1 > 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 - 10 = y1 - 10 /\ y2 - 1 = y2 - 1 /\ z = z) /\ (y2 - 1 + 1 > 1 /\ x = x /\ y1 - 10 + 11 = y1 - 10 + 11 /\ z = z) /\ (not (y2 - 1 + 1 - 1 = 1) /\ x = x /\ z = z) |= y2 - 1 + 1 - 1 >  y2 - 1 + 1 - 1 - 1 + 1 - 1 (and y2 - 1 + 1 - 1 >= 0)
  (3) y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (y1 + 11 - 10 <= 100 /\ x = x /\ z = z)                                     |= y2 - 1 + 1 - 1 >= y2 + 1 - 1 - 1 + 1 - 1
  (4) y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (not (y2 + 1 - 1 = 1) /\ x = x /\ z = z)                                    |= y2 - 1 + 1 - 1 >= y2 + 1 - 1 - 1 + 1 - 1

We may remove the strictly oriented DPs, which yields:

Processor output: { D8 = (P8, R UNION R_?, i, c) }, where:

  P8. (1) eval_9#(x, y1, y2, z) => eval_9#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (y1 + 11 - 10 <= 100 /\ x = x /\ z = z)
      (2) eval_9#(x, y1, y2, z) => eval_9#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (not (y2 + 1 - 1 = 1) /\ x = x /\ z = z)

***** We apply the Integer Function Processor on D8 = (P8, R UNION R_?, i, c).

We use the following integer mapping:

  J(eval_9#) = 100 - (arg_2 + 11 - 10)

We thus have:

  (1) y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (y1 + 11 - 10 <= 100 /\ x = x /\ z = z)  |= 100 - (y1 + 11 - 10) >  100 - (y1 + 11 - 10 + 11 - 10) (and 100 - (y1 + 11 - 10) >= 0)
  (2) y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (not (y2 + 1 - 1 = 1) /\ x = x /\ z = z) |= 100 - (y1 + 11 - 10) >= 100 - (y1 + 11 - 10 + 11 - 10)

We may remove the strictly oriented DPs, which yields:

Processor output: { D9 = (P9, R UNION R_?, i, c) }, where:

  P9. (1) eval_9#(x, y1, y2, z) => eval_9#(x, y1 + 11 - 10, y2 + 1 - 1, z) | y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (not (y2 + 1 - 1 = 1) /\ x = x /\ z = z)

***** We apply the Integer Function Processor on D9 = (P9, R UNION R_?, i, c).

We use the following integer mapping:

  J(eval_9#) = 100 - arg_2

We thus have:

  (1) y1 <= 100 /\ x = x /\ y2 = y2 /\ z = z /\ (x = x /\ y1 = y1 /\ y2 = y2 /\ z = z) /\ (y2 + 1 > 1 /\ x = x /\ y1 + 11 = y1 + 11 /\ z = z) /\ (not (y2 + 1 - 1 = 1) /\ x = x /\ z = z) |= 100 - y1 > 100 - (y1 + 11 - 10) (and 100 - y1 >= 0)

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

Processor output: { }.