(STRATEGY
    INNERMOST)

(VAR
    x y)
(DATATYPES
    A = µX.< c(X), 0 >)
(SIGNATURES
    b :: [A x A] -> A
    a :: [A x A] -> A)
(RULES
    b(x,y) -> c(a(c(y),a(0(),x)))
    a(y,x) -> y
    a(y,c(b(a(0(),x),0()))) ->
      b(a(c(b(0(),y)),x),0()))