(STRATEGY
    INNERMOST)

(VAR
    w x y z)
(DATATYPES
    A = µX.< c(X, X), s(X), 0 >)
(SIGNATURES
    h :: [A x A x A] -> A
    t :: [A] -> A)
(RULES
    h(c(x,y),c(s(z),z),t(w)) -> h(z
                                 ,c(y,x)
                                 ,t(t(c(x,c(y,t(w))))))
    h(x,c(y,z),t(w)) -> h(c(s(y),x)
                         ,z
                         ,t(c(t(w),w)))
    h(c(s(x),c(s(0()),y)),z,t(x)) ->
      h(y
       ,c(s(0()),c(x,z))
       ,t(t(c(x,s(x)))))
    t(t(x)) -> t(c(t(x),x))
    t(x) -> x
    t(x) -> c(0()
             ,c(0(),c(0(),c(0(),c(0(),x))))))