(STRATEGY
    INNERMOST)

(VAR
    x x' xs xs' y)
(DATATYPES
    A = µX.< Cons(X, X), Nil, False, True >)
(SIGNATURES
    lt0 :: [A x A] -> A
    g :: [A x A] -> A
    f :: [A x A] -> A
    number42 :: [] -> 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(Cons(x',xs'),Cons(x,xs)) ->
      lt0(xs',xs)
    g(x,Nil()) -> Cons(Nil()
                      ,Cons(Nil()
                           ,Cons(Nil()
                                ,Cons(Nil()
                                     ,Cons(Nil()
                                          ,Cons(Nil()
                                               ,Cons(Nil()
                                                    ,Cons(Nil()
                                                         ,Cons(Nil()
                                                              ,Cons(Nil()
                                                                   ,Cons(Nil()
                                                                        ,Cons(Nil()
                                                                             ,Cons(Nil()
                                                                                  ,Cons(Nil()
                                                                                       ,Cons(Nil()
                                                                                            ,Cons(Nil()
                                                                                                 ,Cons(Nil()
                                                                                                      ,Cons(Nil()
                                                                                                           ,Cons(Nil()
                                                                                                                ,Cons(Nil()
                                                                                                                     ,Cons(Nil()
                                                                                                                          ,Cons(Nil()
                                                                                                                               ,Cons(Nil()
                                                                                                                                    ,Cons(Nil()
                                                                                                                                         ,Cons(Nil()
                                                                                                                                              ,Cons(Nil()
                                                                                                                                                   ,Cons(Nil()
                                                                                                                                                        ,Cons(Nil()
                                                                                                                                                             ,Cons(Nil()
                                                                                                                                                                  ,Cons(Nil()
                                                                                                                                                                       ,Cons(Nil()
                                                                                                                                                                            ,Cons(Nil()
                                                                                                                                                                                 ,Cons(Nil()
                                                                                                                                                                                      ,Cons(Nil()
                                                                                                                                                                                           ,Cons(Nil()
                                                                                                                                                                                                ,Cons(Nil()
                                                                                                                                                                                                     ,Cons(Nil()
                                                                                                                                                                                                          ,Cons(Nil()
                                                                                                                                                                                                               ,Cons(Nil()
                                                                                                                                                                                                                    ,Cons(Nil()
                                                                                                                                                                                                                         ,Cons(Nil()
                                                                                                                                                                                                                              ,Cons(Nil()
                                                                                                                                                                                                                                   ,Nil()))))))))))))))))))))))))))))))))))))))))))
    f(x,Nil()) -> Cons(Nil()
                      ,Cons(Nil()
                           ,Cons(Nil()
                                ,Cons(Nil()
                                     ,Cons(Nil()
                                          ,Cons(Nil()
                                               ,Cons(Nil()
                                                    ,Cons(Nil()
                                                         ,Cons(Nil()
                                                              ,Cons(Nil()
                                                                   ,Cons(Nil()
                                                                        ,Cons(Nil()
                                                                             ,Cons(Nil()
                                                                                  ,Cons(Nil()
                                                                                       ,Cons(Nil()
                                                                                            ,Cons(Nil()
                                                                                                 ,Cons(Nil()
                                                                                                      ,Cons(Nil()
                                                                                                           ,Cons(Nil()
                                                                                                                ,Cons(Nil()
                                                                                                                     ,Cons(Nil()
                                                                                                                          ,Cons(Nil()
                                                                                                                               ,Cons(Nil()
                                                                                                                                    ,Cons(Nil()
                                                                                                                                         ,Cons(Nil()
                                                                                                                                              ,Cons(Nil()
                                                                                                                                                   ,Cons(Nil()
                                                                                                                                                        ,Cons(Nil()
                                                                                                                                                             ,Cons(Nil()
                                                                                                                                                                  ,Cons(Nil()
                                                                                                                                                                       ,Cons(Nil()
                                                                                                                                                                            ,Cons(Nil()
                                                                                                                                                                                 ,Cons(Nil()
                                                                                                                                                                                      ,Cons(Nil()
                                                                                                                                                                                           ,Cons(Nil()
                                                                                                                                                                                                ,Cons(Nil()
                                                                                                                                                                                                     ,Cons(Nil()
                                                                                                                                                                                                          ,Cons(Nil()
                                                                                                                                                                                                               ,Cons(Nil()
                                                                                                                                                                                                                    ,Cons(Nil()
                                                                                                                                                                                                                         ,Cons(Nil()
                                                                                                                                                                                                                              ,Cons(Nil()
                                                                                                                                                                                                                                   ,Nil()))))))))))))))))))))))))))))))))))))))))))
    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(f[Ite][False][Ite](lt0(x
                              ,Cons(Nil(),Nil()))
                          ,x
                          ,Cons(x',xs))
       ,f[Ite][False][Ite](lt0(x
                              ,Cons(Nil(),Nil()))
                          ,x
                          ,Cons(x',xs)))
    number42() -> Cons(Nil()
                      ,Cons(Nil()
                           ,Cons(Nil()
                                ,Cons(Nil()
                                     ,Cons(Nil()
                                          ,Cons(Nil()
                                               ,Cons(Nil()
                                                    ,Cons(Nil()
                                                         ,Cons(Nil()
                                                              ,Cons(Nil()
                                                                   ,Cons(Nil()
                                                                        ,Cons(Nil()
                                                                             ,Cons(Nil()
                                                                                  ,Cons(Nil()
                                                                                       ,Cons(Nil()
                                                                                            ,Cons(Nil()
                                                                                                 ,Cons(Nil()
                                                                                                      ,Cons(Nil()
                                                                                                           ,Cons(Nil()
                                                                                                                ,Cons(Nil()
                                                                                                                     ,Cons(Nil()
                                                                                                                          ,Cons(Nil()
                                                                                                                               ,Cons(Nil()
                                                                                                                                    ,Cons(Nil()
                                                                                                                                         ,Cons(Nil()
                                                                                                                                              ,Cons(Nil()
                                                                                                                                                   ,Cons(Nil()
                                                                                                                                                        ,Cons(Nil()
                                                                                                                                                             ,Cons(Nil()
                                                                                                                                                                  ,Cons(Nil()
                                                                                                                                                                       ,Cons(Nil()
                                                                                                                                                                            ,Cons(Nil()
                                                                                                                                                                                 ,Cons(Nil()
                                                                                                                                                                                      ,Cons(Nil()
                                                                                                                                                                                           ,Cons(Nil()
                                                                                                                                                                                                ,Cons(Nil()
                                                                                                                                                                                                     ,Cons(Nil()
                                                                                                                                                                                                          ,Cons(Nil()
                                                                                                                                                                                                               ,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) ->= xs
    f[Ite][False][Ite](True()
                      ,x'
                      ,Cons(x,xs)) ->= xs
    f[Ite][False][Ite](False()
                      ,x
                      ,y) ->= Cons(Cons(Nil(),Nil())
                                  ,y)
    f[Ite][False][Ite](True()
                      ,x
                      ,y) ->= x)