sum(sum(X0,s(X1)),X2) = sum(X1,s(X0)) sum(X0,s(X1)) = sum(X1,s(X0)) sum(0,X) = X sum(s(Y),X) = s(sum(Y,X))