(STRATEGY
    INNERMOST)

(VAR
    m n x y)
(DATATYPES
    A = µX.< cons(X, X), s(X), 0, nil >)
(SIGNATURES
    sum :: [A x A] -> A
    weight :: [A] -> A)
(RULES
    sum(cons(s(n),x),cons(m,y)) ->
      sum(cons(n,x),cons(s(m),y))
    sum(cons(0(),x),y) -> sum(x,y)
    sum(nil(),y) -> y
    weight(cons(n,cons(m,x))) ->
      weight(sum(cons(n,cons(m,x))
                ,cons(0(),x)))
    weight(cons(n,nil())) -> n)