We consider termination of the MSTRS with no additional rule schemes:

  Signature: a :: o
             b :: o
             f :: o -> o -> o
             h :: o -> o

  Rules: f(x, x) -> x
         f(a, y) -> f(y, b)

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) f#(a, y) => f#(y, b)

***** We apply the Reduction Pair [with HORPO] Processor on D1 = (P1, R, i, c).

Constrained HORPO yields:

  f#(a, y) (>) f#(y, b)
  f(x, x) (>=) x
  f(a, y) (>=) f(y, b)

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:

    a   { }
  > b   { }
  = f#  { 1 2 }
  = f   { 1 2 }

* Well-founded theory orderings:

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

All dependency pairs were removed.

Processor output: { }.