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

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

Constrained HORPO yields:

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

We do this using the following settings:

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

  f      (status: Mul_2) >
  a      (status: Lex)   >
  f#     (status: Mul_2) >
  b = g  (status: Lex)

* Well-founded theory orderings:

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

* Filter:

  f  disregards argument(s) 3 
  f# disregards argument(s) 3 
  g  disregards argument(s) 1 

All dependency pairs were removed.