(STRATEGY
    INNERMOST)

(VAR
    x xs y ys)
(DATATYPES
    A = µX.< Cons(X, X), S, Nil >)
(SIGNATURES
    mul0 :: [A x A] -> A
    add0 :: [A x A] -> A
    goal :: [A x A] -> A)
(RULES
    mul0(Cons(x,xs),y) ->
      add0(mul0(xs,y),y)
    add0(Cons(x,xs),y) -> add0(xs
                              ,Cons(S(),y))
    mul0(Nil(),y) -> Nil()
    add0(Nil(),y) -> y
    goal(xs,ys) -> mul0(xs,ys))