The system is accessible function passing by a sort ordering that equates all sorts.

We start by computing the following initial DP problem:

  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 P1.

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

  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 Integer Function Processor on P2.

We use the following integer mapping:

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

We thus have:

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

We may remove the strictly oriented DPs, which yields:

  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
      (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

***** We apply the Theory Arguments Processor on P3.

We use the following theory arguments function:

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

This yields the following new DP problems:

  P4. (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 }

  P5. (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

***** We apply the Theory Arguments Processor on P4.

We use the following theory arguments function:

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

This yields the following new DP problems:

  P6. (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 }

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

***** We apply the Graph Processor on P5.

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

  P8. (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 P6.

We use the following integer mapping:

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

We thus have:

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

We may remove the strictly oriented DPs, which yields:

  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 P7.

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

***** We apply the Integer Function Processor on P8.

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.

***** We apply the Graph Processor on P9.

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

  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 P10.

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.