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) h#(F, G, s(Y)) => if#(F(Y), Y, 0)
      (2) h#(F, G, s(Y)) => h#(F, G, if(F(Y), Y, 0))

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

There is only one SCC, so all DPs not inside the SCC can be removed:

  P2. (1) h#(F, G, s(Y)) => h#(F, G, if(F(Y), Y, 0))

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

Constrained HORPO yields:

  h#(F, G, s(Y)) (>) h#(F, G, if(F(Y), Y, 0))
  if(true, X, Y) (>=) X
  if(false, X, Y) (>=) Y
  h(F, G, 0) (>=) 0
  h(F, G, s(Y)) (>=) G(h(F, G, if(F(Y), Y, 0)))

We do this using the following settings:

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

  h# = s  (status: Lex) >
  0       (status: Lex) >
  h = if  (status: Lex)

* Well-founded theory orderings:

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

* Filter:

  h# disregards argument(s) 2 
  if disregards argument(s) 1 

All dependency pairs were removed.