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

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

Constrained HORPO yields:

  lessthan#(arrow(X, Y), arrow(U, V)) (>) lessthan#(U, X)
  lessthan#(arrow(X, Y), arrow(U, V)) (>) lessthan#(Y, V)
  lessthan(arrow(X, Y), arrow(U, V)) (>=) and(lessthan(U, X), lessthan(Y, V))

We do this using the following settings:

* Precedence and status (for non-mentioned symbols the precedence is irrelevant and the status is Lex):

  lessthan   (status: Mul_2) >
  arrow      (status: Lex)   >
  and        (status: Lex)   >
  lessthan#  (status: Mul_2)

* Well-founded theory orderings:

  [>]_{Bool} = {(true,false)}
  [>]_{Int}  = {(x,y) | x < 1000 /\ x < y }

* Filter:

  and disregards argument(s) 1 2 

All dependency pairs were removed.