(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< *(X, X), u >)
(SIGNATURES
    + :: [A x A] -> A)
(RULES
    +(*(x,y),*(x,z)) -> *(x,+(y,z))
    +(+(x,y),z) -> +(x,+(y,z))
    +(*(x,y),+(*(x,z),u())) -> +(*(x
                                  ,+(y,z))
                                ,u()))