We consider universal computability of the STRS with no additional rule schemes:

  Signature: and      :: c -> c -> c
             arrow    :: t -> t -> t
             lessthan :: t -> t -> c

  Rules: lessthan(arrow(X, Y), arrow(U, V)) -> and(lessthan(U, X), lessthan(Y, V))

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) lessthan#(arrow(X, Y), arrow(U, V)) => lessthan#(U, X)
      (2) lessthan#(arrow(X, Y), arrow(U, V)) => lessthan#(Y, V)

***** No progress could be made on DP problem D1 = (P1, R UNION R_?, i, c).