(STRATEGY
    INNERMOST)

(VAR
    x x' xs xs' y ys)
(DATATYPES
    A = µX.< Cons(X, X), Nil, S(X), 0, True, False >)
(SIGNATURES
    merge :: [A x A] -> A
    goal :: [A x A] -> A
    <= :: [A x A] -> A
    merge[Ite] :: [A x A x A] -> A)
(RULES
    merge(Cons(x,xs),Nil()) ->
      Cons(x,xs)
    merge(Cons(x',xs')
         ,Cons(x,xs)) -> merge[Ite](<=(x'
                                      ,x)
                                   ,Cons(x',xs')
                                   ,Cons(x,xs))
    merge(Nil(),ys) -> ys
    goal(xs,ys) -> merge(xs,ys)
    <=(S(x),S(y)) ->= <=(x,y)
    <=(0(),y) ->= True()
    <=(S(x),0()) ->= False()
    merge[Ite](False()
              ,xs'
              ,Cons(x,xs)) ->= Cons(x
                                   ,merge(xs',xs))
    merge[Ite](True()
              ,Cons(x,xs)
              ,ys) ->= Cons(x,merge(xs,ys)))