(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< nil, g(X, X), true, false, or(X, X), =(X, X), not(X), max'(X, X), u >)
(SIGNATURES
    f :: [A x A] -> A
    ++ :: [A x A] -> A
    null :: [A] -> A
    mem :: [A x A] -> A
    max :: [A] -> A)
(RULES
    f(x,nil()) -> g(nil(),x)
    f(x,g(y,z)) -> g(f(x,y),z)
    ++(x,nil()) -> x
    ++(x,g(y,z)) -> g(++(x,y),z)
    null(nil()) -> true()
    null(g(x,y)) -> false()
    mem(nil(),y) -> false()
    mem(g(x,y),z) -> or(=(y,z)
                       ,mem(x,z))
    mem(x,max(x)) -> not(null(x))
    max(g(g(nil(),x),y)) -> max'(x
                                ,y)
    max(g(g(g(x,y),z),u())) ->
      max'(max(g(g(x,y),z)),u()))