(STRATEGY
    INNERMOST)

(VAR
    a x xs y)
(DATATYPES
    A = µX.< Cons(X, X), S(X), 0, Nil, True, False >)
(SIGNATURES
    foldl :: [A x A] -> A
    foldr :: [A x A] -> A
    notEmpty :: [A] -> A
    op :: [A x A] -> A
    fold :: [A x A] -> A)
(RULES
    foldl(x,Cons(S(0()),xs)) ->
      foldl(S(x),xs)
    foldl(S(0()),Cons(x,xs)) ->
      foldl(S(x),xs)
    foldr(a,Cons(x,xs)) -> op(x
                             ,foldr(a,xs))
    foldr(a,Nil()) -> a
    foldl(a,Nil()) -> a
    notEmpty(Cons(x,xs)) -> True()
    notEmpty(Nil()) -> False()
    op(x,S(0())) -> S(x)
    op(S(0()),y) -> S(y)
    fold(a,xs) -> Cons(foldl(a,xs)
                      ,Cons(foldr(a,xs),Nil())))