(STRATEGY
    INNERMOST)

(VAR
    n x x' xs xs' y)
(DATATYPES
    A = µX.< Nil, Cons(X, X), True, False >)
(SIGNATURES
    lt0 :: [A x A] -> A
    g :: [A x A] -> A
    f :: [A x A] -> A
    notEmpty :: [A] -> A
    number4 :: [A] -> A
    goal :: [A x A] -> A
    g[Ite][False][Ite] :: [A x A x A] -> A
    f[Ite][False][Ite] :: [A x A x A] -> A)
(RULES
    lt0(Nil(),Cons(x',xs)) -> True()
    lt0(Cons(x',xs'),Cons(x,xs)) ->
      lt0(xs',xs)
    g(x,Nil()) -> Cons(Nil()
                      ,Cons(Nil()
                           ,Cons(Nil(),Cons(Nil(),Nil()))))
    f(x,Nil()) -> Cons(Nil()
                      ,Cons(Nil()
                           ,Cons(Nil(),Cons(Nil(),Nil()))))
    notEmpty(Cons(x,xs)) -> True()
    notEmpty(Nil()) -> False()
    lt0(x,Nil()) -> False()
    g(x,Cons(x',xs)) ->
      g[Ite][False][Ite](lt0(x
                            ,Cons(Nil(),Nil()))
                        ,x
                        ,Cons(x',xs))
    f(x,Cons(x',xs)) ->
      f[Ite][False][Ite](lt0(x
                            ,Cons(Nil(),Nil()))
                        ,x
                        ,Cons(x',xs))
    number4(n) -> Cons(Nil()
                      ,Cons(Nil()
                           ,Cons(Nil(),Cons(Nil(),Nil()))))
    goal(x,y) -> Cons(f(x,y)
                     ,Cons(g(x,y),Nil()))
    g[Ite][False][Ite](False()
                      ,Cons(x,xs)
                      ,y) ->= g(xs
                               ,Cons(Cons(Nil(),Nil()),y))
    g[Ite][False][Ite](True()
                      ,x'
                      ,Cons(x,xs)) ->= g(x',xs)
    f[Ite][False][Ite](False()
                      ,Cons(x,xs)
                      ,y) ->= f(xs
                               ,Cons(Cons(Nil(),Nil()),y))
    f[Ite][False][Ite](True()
                      ,x'
                      ,Cons(x,xs)) ->= f(x',xs))