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) eval#(i, j, k) => eval#(j, i + 1, k - 1) | i <= 100 /\ j <= k

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

Constrained HORPO yields:

  eval#(i, j, k) (>) eval#(j, i + 1, k - 1) | i <= 100 /\ j <= k
  eval(i, j, k) (>=) eval(j, i + 1, k - 1) | i <= 100 /\ j <= k

We do this using the following settings:

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

  eval   (status: Mul_2) >
  eval#  (status: Mul_2) >
  +      (status: Lex)   >
  -      (status: Lex)

* Well-founded theory orderings:

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

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

All dependency pairs were removed.