We consider termination 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, 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)

***** We apply the Usable Rules Processor on D1 = (P1, R, i, c).

We obtain 0 usable rules (out of 1 rules in the input problem).

Processor output: { D2 = (P1, {}, i, c) }.

***** We apply the Usable rules with respect to HORPO Processor on D2 = (P1, {}, i, c).

Constrained HORPO yields:

  lessthan#2(arrow2(X, Y), arrow2(U, V)) (>) lessthan#2(U, X)
  lessthan#2(arrow2(X, Y), arrow2(U, V)) (>) lessthan#2(Y, V)

We do this using the following settings:

* Monotonicity requirements: this is a strongly monotonic reduction pair (all arguments of function symbols were regarded).

* Precedence and permutation:

    arrow2      { 2 }   1
  = lessthan#2  { 1 2 }

* Well-founded theory orderings:

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

Processor output: { }.