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

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

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

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

***** 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 an argument wiltering [with HORPO] Processor on D2 = (P1, {}, i, c).

Constrained HORPO yields:

  f#3(x, a0, y) (>) f#3(b0, x, g1(y))

We do this using the following settings:

* Disregarded arguments:

  g1 1 

* Precedence and permutation:

    a0   { }
  > b0   { }
  = f#3  { 1 2 } _ 3
  = g1   { }

* Well-founded theory orderings:

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

Processor output: { }.