(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
        
)