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_?, i, 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_?, i, 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_?, i, 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 Chaining Processor Processor on D2 = (P2, R UNION R_?, i, c).

We chain DPs according to the following mapping:


  eval_4#(i, j, l, r, n) => eval_3#(l - 1, 2 * (l - 1), l - 1, r, n) | l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2  is obtained by chaining  eval_4#(i, j, l, r, n) => eval_2#(i, j, l - 1, r, n) | l >= 2 /\ l >= 1 /\ r >= 2 and eval_2#(i', j', l', r', n') => eval_3#(l', 2 * l', l', r', n') | r' >= 2
  eval_4#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2 /\ r - 1 >= 2         is obtained by chaining  eval_4#(i, j, l, r, n) => eval_2#(i, j, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2  and eval_2#(i', j', l', r', n') => eval_3#(l', 2 * l', l', r', n') | r' >= 2


The following DPs were deleted:

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

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


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

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

  P3. (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_3#(l - 1, 2 * (l - 1), l - 1, r, n) | l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2
      (7) eval_4#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2 /\ r - 1 >= 2

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

We chain DPs according to the following mapping:


  eval_3#(i, j, l, r, n) => eval_3#(l - 1, 2 * (l - 1), l - 1, r, n) | r >= j /\ r - 1 >= j /\ (l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2)  is obtained by chaining  eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ r - 1 >= j     and eval_4#(i', j', l', r', n') => eval_3#(l' - 1, 2 * (l' - 1), l' - 1, r', n') | l' >= 2 /\ l' >= 1 /\ r' >= 2 /\ r' >= 2
  eval_3#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r - 1, n) | r >= j /\ r - 1 >= j /\ (2 > l /\ l >= 1 /\ r >= 2 /\ r - 1 >= 2)         is obtained by chaining  eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ r - 1 >= j     and eval_4#(i', j', l', r', n') => eval_3#(l', 2 * l', l', r' - 1, n') | 2 > l' /\ l' >= 1 /\ r' >= 2 /\ r' - 1 >= 2
  eval_3#(i, j, l, r, n) => eval_3#(l - 1, 2 * (l - 1), l - 1, r, n) | r >= j /\ r - 1 >= j /\ (l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2)  is obtained by chaining  eval_3#(i, j, l, r, n) => eval_4#(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j and eval_4#(i', j', l', r', n') => eval_3#(l' - 1, 2 * (l' - 1), l' - 1, r', n') | l' >= 2 /\ l' >= 1 /\ r' >= 2 /\ r' >= 2
  eval_3#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r - 1, n) | r >= j /\ r - 1 >= j /\ (2 > l /\ l >= 1 /\ r >= 2 /\ r - 1 >= 2)         is obtained by chaining  eval_3#(i, j, l, r, n) => eval_4#(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j and eval_4#(i', j', l', r', n') => eval_3#(l', 2 * l', l', r' - 1, n') | 2 > l' /\ l' >= 1 /\ r' >= 2 /\ r' - 1 >= 2
  eval_3#(i, j, l, r, n) => eval_3#(l - 1, 2 * (l - 1), l - 1, r, n) | r >= j /\ j > r - 1 /\ (l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2)   is obtained by chaining  eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ j > r - 1      and eval_4#(i', j', l', r', n') => eval_3#(l' - 1, 2 * (l' - 1), l' - 1, r', n') | l' >= 2 /\ l' >= 1 /\ r' >= 2 /\ r' >= 2
  eval_3#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r - 1, n) | r >= j /\ j > r - 1 /\ (2 > l /\ l >= 1 /\ r >= 2 /\ r - 1 >= 2)          is obtained by chaining  eval_3#(i, j, l, r, n) => eval_4#(i, j, l, r, n) | r >= j /\ j > r - 1      and eval_4#(i', j', l', r', n') => eval_3#(l', 2 * l', l', r' - 1, n') | 2 > l' /\ l' >= 1 /\ r' >= 2 /\ r' - 1 >= 2


The following DPs were deleted:

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_4#(i, j, l, r, n) | r >= j /\ j > r - 1

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

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


By chaining, we added 6 DPs and removed 5 DPs.

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

  P4. (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
      (3) eval_3#(i, j, l, r, n) => eval_3#(l - 1, 2 * (l - 1), l - 1, r, n) | r >= j /\ r - 1 >= j /\ (l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2)
      (4) eval_3#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r - 1, n) | r >= j /\ r - 1 >= j /\ (2 > l /\ l >= 1 /\ r >= 2 /\ r - 1 >= 2)
      (5) eval_3#(i, j, l, r, n) => eval_3#(l - 1, 2 * (l - 1), l - 1, r, n) | r >= j /\ r - 1 >= j /\ (l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2)
      (6) eval_3#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r - 1, n) | r >= j /\ r - 1 >= j /\ (2 > l /\ l >= 1 /\ r >= 2 /\ r - 1 >= 2)
      (7) eval_3#(i, j, l, r, n) => eval_3#(l - 1, 2 * (l - 1), l - 1, r, n) | r >= j /\ j > r - 1 /\ (l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2)
      (8) eval_3#(i, j, l, r, n) => eval_3#(l, 2 * l, l, r - 1, n) | r >= j /\ j > r - 1 /\ (2 > l /\ l >= 1 /\ r >= 2 /\ r - 1 >= 2)

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

We use the following integer mapping:

  J(eval_3#) = arg_4 - 1 - 2

We thus have:

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

We may remove the strictly oriented DPs, which yields:

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

  P5. (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
      (3) eval_3#(i, j, l, r, n) => eval_3#(l - 1, 2 * (l - 1), l - 1, r, n) | r >= j /\ r - 1 >= j /\ (l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2)
      (4) eval_3#(i, j, l, r, n) => eval_3#(l - 1, 2 * (l - 1), l - 1, r, n) | r >= j /\ r - 1 >= j /\ (l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2)
      (5) eval_3#(i, j, l, r, n) => eval_3#(l - 1, 2 * (l - 1), l - 1, r, n) | r >= j /\ j > r - 1 /\ (l >= 2 /\ l >= 1 /\ r >= 2 /\ r >= 2)

***** We apply the Usable Rules Processor on D5 = (P5, R UNION R_?, i, c).

We obtain 0 usable rules (out of 11 rules in the input problem).

Processor output: { D6 = (P5, {}, i, c) }.

***** No progress could be made on DP problem D6 = (P5, {}, i, c).