(STRATEGY
    INNERMOST)

(VAR
    x xs y)
(DATATYPES
    A = µX.< 0, s(X), nil, cons(X, X), true, false >)
(SIGNATURES
    double :: [A] -> A
    del :: [A x A] -> A
    if :: [A x A x A x A] -> A
    eq :: [A x A] -> A
    first :: [A] -> A
    doublelist :: [A] -> A)
(RULES
    double(0()) -> 0()
    double(s(x)) -> s(s(double(x)))
    del(x,nil()) -> nil()
    del(x,cons(y,xs)) -> if(eq(x,y)
                           ,x
                           ,y
                           ,xs)
    if(true(),x,y,xs) -> xs
    if(false(),x,y,xs) -> cons(y
                              ,del(x,xs))
    eq(0(),0()) -> true()
    eq(0(),s(y)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    first(nil()) -> 0()
    first(cons(x,xs)) -> x
    doublelist(nil()) -> nil()
    doublelist(cons(x,xs)) ->
      cons(double(x)
          ,doublelist(del(first(cons(x
                                    ,xs))
                         ,cons(x,xs)))))