(STRATEGY
    INNERMOST)

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