(COMMENT 
)

(VAR k l x y z )
(RULES
a(h,h,h,x) -> s(x)
a(l,x,s(y),h) -> a(l,x,y,s(h))
a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
a(l,s(x),h,z) -> a(l,x,z,z)
a(s(l),h,h,z) -> a(l,z,h,z)
+(x, h) -> x 
+(h, x) -> x 
+(s(x), s(y)) -> s(s(+(x,y)))
+(+(x,y),z) -> +(x,+(y,z))
s(h) -> 1
app(nil, k) -> k
app(l, nil) -> l
app(cons(x,l), k) -> cons(x, app(l, k))
sum(cons(x,nil)) -> cons(x,nil)
sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h,h),l))


)