(VAR x y b xs ys)
(RULES
isEmpty(cons(x,xs)) -> false
isEmpty(nil) -> true

isZero(0) -> true
isZero(s(x)) -> false

head(cons(x,xs)) -> x
tail(cons(x,xs)) -> xs
tail(nil) -> nil

p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0
p(0) -> 0

inc(s(x)) -> s(inc(x))
inc(0) -> s(0)

sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))
if(true, b, y, xs, ys, x) -> y
if(false, true, y, xs, ys, x) -> sumList(xs, y)
if(false, false, y, xs, ys, x) -> sumList(ys, x)

sum(xs) -> sumList(xs, 0)
)
(COMMENT
sum(xs) returns the sum of all elements in the list
)