We consider universal computability of the LCTRS with only rule scheme Calc:

  Signature: eval_1 :: Int -> Int -> Int -> Int -> o -> o
             eval_2 :: Int -> Int -> Int -> Int -> o -> o
             eval_3 :: Int -> Int -> Int -> Int -> o -> o
             eval_4 :: Int -> Int -> Int -> Int -> o -> o

  Rules: eval_1(i, j, l, r, n) -> eval_2(i, j, l - 1, r, n) | l >= 2
         eval_1(i, j, l, r, n) -> eval_2(i, j, l, r - 1, n) | 2 > l
         eval_2(i, j, l, r, n) -> eval_3(l, 2 * l, l, r, n) | r >= 2
         eval_3(i, j, l, r, n) -> eval_4(i, j, l, r, n) | r >= j /\ r - 1 >= j
         eval_3(i, j, l, r, n) -> eval_4(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j
         eval_3(i, j, l, r, n) -> eval_3(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1
         eval_3(i, j, l, r, n) -> eval_3(j + 1, 2 * j + 2, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1
         eval_3(i, j, l, r, n) -> eval_4(i, j, l, r, n) | r >= j /\ j > r - 1
         eval_3(i, j, l, r, n) -> eval_3(j, 2 * j, l, r, n) | r >= j /\ j > r - 1 /\ j >= 1
         eval_4(i, j, l, r, n) -> eval_2(i, j, l - 1, r, n) | l >= 2 /\ l >= 1 /\ r >= 2
         eval_4(i, j, l, r, n) -> eval_2(i, j, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2

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_?, f, c), where:

  P1. (1)  eval_1#(i, j, l, r, n) => eval_2#(i, j, l - 1, r, n) | l >= 2
      (2)  eval_1#(i, j, l, r, n) => eval_2#(i, j, l, r - 1, n) | 2 > l
      (3)  eval_2#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r, n) | r >= 2
      (4)  eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ r - 1 >= j
      (5)  eval_3#(i, j, l, r, n) => eval_4#(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j
      (6)  eval_3#(i, j, l, r, n) => eval_3#(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1
      (7)  eval_3#(i, j, l, r, n) => eval_3#(j + 1, 2 * j + 2, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1
      (8)  eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ j > r - 1
      (9)  eval_3#(i, j, l, r, n) => eval_3#(j, 2 * j, l, r, n) | r >= j /\ j > r - 1 /\ j >= 1
      (10) eval_4#(i, j, l, r, n) => eval_2#(i, j, l - 1, r, n) | l >= 2 /\ l >= 1 /\ r >= 2
      (11) eval_4#(i, j, l, r, n) => eval_2#(i, j, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2

***** We apply the Graph Processor on D1 = (P1, R UNION R_?, f, c).

We compute a graph approximation with the following edges:

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

There is only one SCC, so all DPs not inside the SCC can be removed.

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

  P2. (1) eval_2#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r, n) | r >= 2
      (2) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ r - 1 >= j
      (3) eval_3#(i, j, l, r, n) => eval_4#(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j
      (4) eval_3#(i, j, l, r, n) => eval_3#(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1
      (5) eval_3#(i, j, l, r, n) => eval_3#(j + 1, 2 * j + 2, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1
      (6) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ j > r - 1
      (7) eval_4#(i, j, l, r, n) => eval_2#(i, j, l - 1, r, n) | l >= 2 /\ l >= 1 /\ r >= 2
      (8) eval_4#(i, j, l, r, n) => eval_2#(i, j, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2

***** We apply the Theory Arguments Processor on D2 = (P2, R UNION R_?, f, c).

We use the following theory arguments function:

  eval_3# : [1, 2, 3, 4]

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

  P3. (1) eval_2#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r, n) | r >= 2
      (2) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ r - 1 >= j { i, j, l, r }
      (3) eval_3#(i, j, l, r, n) => eval_4#(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j { i, j, l, r }
      (4) eval_3#(i, j, l, r, n) => eval_3#(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 { i, j, l, r }
      (5) eval_3#(i, j, l, r, n) => eval_3#(j + 1, 2 * j + 2, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 { i, j, l, r }
      (6) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ j > r - 1 { i, j, l, r }
      (7) eval_4#(i, j, l, r, n) => eval_2#(i, j, l - 1, r, n) | l >= 2 /\ l >= 1 /\ r >= 2 { i, j, l, r }
      (8) eval_4#(i, j, l, r, n) => eval_2#(i, j, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2 { i, j, l, r }

  P4. (1) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ r - 1 >= j
      (2) eval_3#(i, j, l, r, n) => eval_4#(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j
      (3) eval_3#(i, j, l, r, n) => eval_3#(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1
      (4) eval_3#(i, j, l, r, n) => eval_3#(j + 1, 2 * j + 2, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1
      (5) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ j > r - 1
      (6) eval_4#(i, j, l, r, n) => eval_2#(i, j, l - 1, r, n) | l >= 2 /\ l >= 1 /\ r >= 2
      (7) eval_4#(i, j, l, r, n) => eval_2#(i, j, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2

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

We use the following theory arguments function:

  eval_3# : [1, 2, 3, 4]

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

  P5. (1) eval_2#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r, n) | r >= 2 { i, j, l, r }
      (2) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ r - 1 >= j { i, j, l, r }
      (3) eval_3#(i, j, l, r, n) => eval_4#(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j { i, j, l, r }
      (4) eval_3#(i, j, l, r, n) => eval_3#(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 { i, j, l, r }
      (5) eval_3#(i, j, l, r, n) => eval_3#(j + 1, 2 * j + 2, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 { i, j, l, r }
      (6) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ j > r - 1 { i, j, l, r }
      (7) eval_4#(i, j, l, r, n) => eval_2#(i, j, l - 1, r, n) | l >= 2 /\ l >= 1 /\ r >= 2 { i, j, l, r }
      (8) eval_4#(i, j, l, r, n) => eval_2#(i, j, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2 { i, j, l, r }

  P6. (1) eval_2#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r, n) | r >= 2

***** We apply the Graph Processor on D4 = (P4, R UNION R_?, f, c).

We compute a graph approximation with the following edges:

  1: 6 7 
  2: 6 7 
  3: 1 2 3 4 5 
  4: 1 2 3 4 5 
  5: 6 7 
  6:
  7:

There is only one SCC, so all DPs not inside the SCC can be removed.

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

  P7. (1) eval_3#(i, j, l, r, n) => eval_3#(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1
      (2) eval_3#(i, j, l, r, n) => eval_3#(j + 1, 2 * j + 2, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1

***** We apply the Integer Function Processor on D5 = (P5, R UNION R_?, f, c).

We use the following integer mapping:

  J(eval_2#) = arg_3
  J(eval_3#) = arg_3
  J(eval_4#) = arg_3

We thus have:

  (1) r >= 2                         |= l >= l
  (2) r >= j /\ r - 1 >= j           |= l >= l
  (3) r >= j /\ r - 1 >= j           |= l >= l
  (4) r >= j /\ r - 1 >= j /\ j >= 1 |= l >= l
  (5) r >= j /\ r - 1 >= j /\ j >= 1 |= l >= l
  (6) r >= j /\ j > r - 1            |= l >= l
  (7) l >= 2 /\ l >= 1 /\ r >= 2     |= l >  l - 1 (and l >= 0)
  (8) 2 > l /\ l >= 1 /\ r >= 2      |= l >= l

We may remove the strictly oriented DPs, which yields:

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

  P8. (1) eval_2#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r, n) | r >= 2 { i, j, l, r }
      (2) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ r - 1 >= j { i, j, l, r }
      (3) eval_3#(i, j, l, r, n) => eval_4#(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j { i, j, l, r }
      (4) eval_3#(i, j, l, r, n) => eval_3#(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 { i, j, l, r }
      (5) eval_3#(i, j, l, r, n) => eval_3#(j + 1, 2 * j + 2, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 { i, j, l, r }
      (6) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ j > r - 1 { i, j, l, r }
      (7) eval_4#(i, j, l, r, n) => eval_2#(i, j, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2 { i, j, l, r }

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

We compute a graph approximation with the following edges:

  1:

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

Processor output: { }.

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

We use the following integer mapping:

  J(eval_3#) = arg_4 - 1 - arg_2

We thus have:

  (1) r >= j /\ r - 1 >= j /\ j >= 1 |= r - 1 - j > r - 1 - 2 * j       (and r - 1 - j >= 0)
  (2) r >= j /\ r - 1 >= j /\ j >= 1 |= r - 1 - j > r - 1 - (2 * j + 2) (and r - 1 - j >= 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 D8 = (P8, R UNION R_?, f, c).

We use the following integer mapping:

  J(eval_2#) = arg_4 - 1
  J(eval_3#) = arg_4 - 1
  J(eval_4#) = arg_4 - 1

We thus have:

  (1) r >= 2                         |= r - 1 >= r - 1
  (2) r >= j /\ r - 1 >= j           |= r - 1 >= r - 1
  (3) r >= j /\ r - 1 >= j           |= r - 1 >= r - 1
  (4) r >= j /\ r - 1 >= j /\ j >= 1 |= r - 1 >= r - 1
  (5) r >= j /\ r - 1 >= j /\ j >= 1 |= r - 1 >= r - 1
  (6) r >= j /\ j > r - 1            |= r - 1 >= r - 1
  (7) 2 > l /\ l >= 1 /\ r >= 2      |= r - 1 >  r - 1 - 1 (and r - 1 >= 0)

We may remove the strictly oriented DPs, which yields:

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

  P9. (1) eval_2#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r, n) | r >= 2 { i, j, l, r }
      (2) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ r - 1 >= j { i, j, l, r }
      (3) eval_3#(i, j, l, r, n) => eval_4#(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j { i, j, l, r }
      (4) eval_3#(i, j, l, r, n) => eval_3#(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 { i, j, l, r }
      (5) eval_3#(i, j, l, r, n) => eval_3#(j + 1, 2 * j + 2, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 { i, j, l, r }
      (6) eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ j > r - 1 { i, j, l, r }

***** We apply the Graph Processor on D9 = (P9, R UNION R_?, f, c).

We compute a graph approximation with the following edges:

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

There is only one SCC, so all DPs not inside the SCC can be removed.

Processor output: { D10 = (P10, R UNION R_?, f, c) }, where:

  P10. (1) eval_3#(i, j, l, r, n) => eval_3#(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 { i, j, l, r }
       (2) eval_3#(i, j, l, r, n) => eval_3#(j + 1, 2 * j + 2, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 { i, j, l, r }

***** We apply the Integer Function Processor on D10 = (P10, R UNION R_?, f, c).

We use the following integer mapping:

  J(eval_3#) = arg_4 - 1 - arg_2

We thus have:

  (1) r >= j /\ r - 1 >= j /\ j >= 1 |= r - 1 - j > r - 1 - 2 * j       (and r - 1 - j >= 0)
  (2) r >= j /\ r - 1 >= j /\ j >= 1 |= r - 1 - j > r - 1 - (2 * j + 2) (and r - 1 - j >= 0)

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

Processor output: { }.