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

  Signature: cons    :: t -> f -> f
             heightf :: f -> N
             heightt :: t -> N
             leaf    :: t
             max     :: N -> N -> N
             nil     :: f
             node    :: f -> t
             s       :: N -> N
             z       :: N

  Rules: heightf(nil) -> z
         heightf(cons(X, Y)) -> max(heightt(X), heightf(Y))
         heightt(leaf) -> z
         heightt(node(U)) -> s(heightf(U))

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, f, c), where:

  P1. (1) heightf#(cons(X, Y)) => heightt#(X)
      (2) heightf#(cons(X, Y)) => heightf#(Y)
      (3) heightt#(node(U)) => heightf#(U)

***** We apply the Subterm Criterion Processor on D1 = (P1, R, f, c).

We use the following projection function:

  nu(heightf#) = 1
  nu(heightt#) = 1

We thus have:

  (1) cons(X, Y) |>| X
  (2) cons(X, Y) |>| Y
  (3) node(U)    |>| U

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

Processor output: { }.