(STRATEGY
    INNERMOST)

(VAR
    u v x y)
(DATATYPES
    A = µX.< true, s(X), 0, false >)
(SIGNATURES
    f :: [A x A x A] -> A
    gt :: [A x A] -> A)
(RULES
    f(true(),x,y) -> f(gt(x,y)
                      ,s(x)
                      ,s(s(y)))
    gt(0(),v) -> false()
    gt(s(u),0()) -> true()
    gt(s(u),s(v)) -> gt(u,v))