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