(VAR N M) (RULES U11(tt) -> U12(tt) U12(tt) -> s(plus(N,M)) U21(tt) -> U22(tt) U22(tt) -> plus(x(N,M),N) plus(N,0) -> N plus(N,s(M)) -> U11(tt) x(N,0) -> 0 x(N,s(M)) -> U21(tt) )