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) b10#(sv14_14, sv23_37, sv24_38) => b14#(sv14_14, sv23_37, sv24_38)
      (2) Cond_b14#(true, sv14_14, sv23_37, sv24_38) => b15#(sv14_14, sv23_37, sv24_38)
      (3) b14#(sv14_14, sv23_37, sv24_38) => Cond_b14#(sv23_37 >= sv14_14 /\ 1@z < sv14_14 /\ 0@z < sv24_38 /\ 1@z < sv23_37, sv14_14, sv23_37, sv24_38)
      (4) b15#(sv14_14, sv23_37, sv24_38) => b10#(sv14_14, sv23_37 - sv14_14, sv24_38 + 1@z)

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

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