(STRATEGY
    INNERMOST)

(VAR
    p pp s ss x x' xs xs' y)
(DATATYPES
    A = µX.< Cons(X, X), Nil, False, True, S(X), 0 >)
(SIGNATURES
    loop :: [A x A x A x A] -> A
    match1 :: [A x A] -> A
    !EQ :: [A x A] -> A
    loop[Ite] :: [A x A x A x A x A] -> A)
(RULES
    loop(Cons(x,xs),Nil(),pp,ss) ->
      False()
    loop(Cons(x',xs')
        ,Cons(x,xs)
        ,pp
        ,ss) -> loop[Ite](!EQ(x',x)
                         ,Cons(x',xs')
                         ,Cons(x,xs)
                         ,pp
                         ,ss)
    loop(Nil(),s,pp,ss) -> True()
    match1(p,s) -> loop(p,s,p,s)
    !EQ(S(x),S(y)) ->= !EQ(x,y)
    !EQ(0(),S(y)) ->= False()
    !EQ(S(x),0()) ->= False()
    !EQ(0(),0()) ->= True()
    loop[Ite](False()
             ,p
             ,s
             ,pp
             ,Cons(x,xs)) ->= loop(pp
                                  ,xs
                                  ,pp
                                  ,xs)
    loop[Ite](True()
             ,Cons(x',xs')
             ,Cons(x,xs)
             ,pp
             ,ss) ->= loop(xs',xs,pp,ss))