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

***** We apply the Constraint Modification Processor on P1.

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

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

This yields:

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

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

Considering the 2 SCCs, this DP problem is split into the following new problems.

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

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

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

We use the following theory arguments function:

  eval_11# : [1, 2, 3, 4]
  eval_5#  : [1, 2, 3, 4]
  eval_7#  : [1, 2, 3, 4]
  eval_9#  : [1, 2, 3, 4]

This yields the following new DP problems:

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

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

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

We use the following integer mapping:

  J(eval_3#) = 100 - arg_2

We thus have:

  (1) y1 <= 100 |= 100 - y1 > 100 - (y1 + 11) (and 100 - y1 >= 0)

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

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

We use the following theory arguments function:

  eval_11# : [1, 2, 3, 4]
  eval_5#  : [1, 2, 3, 4]
  eval_7#  : [1, 2, 3, 4]
  eval_9#  : [1, 2, 3, 4]

This yields the following new DP problems:

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

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

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

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

***** No progress could be made on DP problem P7.