(VAR M N )
(STRATEGY CONTEXTSENSITIVE
        (U11 1) 
        (tt ) 
        (U12 1) 
        (s 1) 
        (plus 1 2) 
        (U21 1) 
        (U22 1) 
        (x 1 2) 
        (0 ) 
)
(RULES 
        U11(tt, M, N) -> U12(tt, M, N)
        U12(tt, M, N) -> s(plus(N, M))
        U21(tt, M, N) -> U22(tt, M, N)
        U22(tt, M, N) -> plus(x(N, M), 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)
        
)