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 /\ i = i /\ j = j /\ r = r
         eval_1(i, j, l, r, n) -> eval_2(i, j, l, r - 1, n) | 2 > l /\ i = i /\ j = j /\ r = r
         eval_2(i, j, l, r, n) -> eval_3(l, 2 * l, l, r, n) | r >= 2 /\ i = i /\ j = j /\ l = l
         eval_3(i, j, l, r, n) -> eval_4(i, j, l, r, n) | r >= j /\ r - 1 >= j /\ i = i /\ l = l
         eval_3(i, j, l, r, n) -> eval_4(i, j + 1, l, r, n) | r >= j /\ r - 1 >= j /\ i = i /\ l = l
         eval_3(i, j, l, r, n) -> eval_3(j, 2 * j, l, r, n) | r >= j /\ r - 1 >= j /\ j >= 1 /\ i = i /\ l = l
         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 = i /\ l = l
         eval_3(i, j, l, r, n) -> eval_4(i, j, l, r, n) | r >= j /\ j > r - 1 /\ i = i /\ l = l
         eval_3(i, j, l, r, n) -> eval_3(j, 2 * j, l, r, n) | r >= j /\ j > r - 1 /\ j >= 1 /\ i = i /\ l = l
         eval_4(i, j, l, r, n) -> eval_2(i, j, l - 1, r, n) | l >= 2 /\ l >= 1 /\ r >= 2 /\ i = i /\ j = j
         eval_4(i, j, l, r, n) -> eval_2(i, j, l, r - 1, n) | 2 > l /\ l >= 1 /\ r >= 2 /\ i = i /\ j = j

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

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

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


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 /\ i = i /\ j = j

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

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


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

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


The following DPs were deleted:

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

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

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

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

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


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

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

We use the following integer mapping:

  J(eval_3#) = arg_3 - 1

We thus have:

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

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

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

We use the following integer mapping:

  J(eval_3#) = arg_4

We thus have:

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

We may remove the strictly oriented DPs, which yields:

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

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

***** We apply the Integer Function Processor on D6 = (P6, R UNION R_?, i, 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 /\ i = i /\ l = l |= r - 1 - j > r - 1 - 2 * j       (and r - 1 - j >= 0)
  (2) r >= j /\ r - 1 >= j /\ j >= 1 /\ i = i /\ l = l |= 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: { }.