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) minus#(x, y) => min#(x, y)
      (2) minus#(x, y) => cond#(min(x, y) = y, x, y)
      (3) cond#(true, x, y) => minus#(x, y + 1)
      (4) min#(u, v) => if#(u < v, u, v)

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

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