(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< .(X, X), true, false, nil, u, v, and(X, X) >)
(SIGNATURES
    del :: [A] -> A
    f :: [A x A x A x A] -> A
    = :: [A x A] -> A)
(RULES
    del(.(x,.(y,z))) -> f(=(x,y)
                         ,x
                         ,y
                         ,z)
    f(true(),x,y,z) -> del(.(y,z))
    f(false(),x,y,z) -> .(x
                         ,del(.(y,z)))
    =(nil(),nil()) -> true()
    =(.(x,y),nil()) -> false()
    =(nil(),.(y,z)) -> false()
    =(.(x,y),.(u(),v())) -> and(=(x
                                 ,u())
                               ,=(y,v())))