YES Termination Proof using AProVETerm Rewriting System R:
[M, N]
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)

Termination of R to be shown. 



   R
     ↳Orthogonal Check



This CSR is orthogonal, so it is sufficient to show innermost termination. 


   R
     ↳OrthoCSR
       →TRS1
         ↳CSR to TRS Transformation




Zantema-Transformation successful.
Replacement map:
plus(1, 2)
x(1, 2)
U12(1, 2, 3)
U21(1, 2, 3)
s(1)
U11(1, 2, 3)
U22(1, 2, 3)

Old CSR:

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)

new TRS:

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



   R
     ↳OrthoCSR
       →TRS1
         ↳CSRtoTRS
           →TRS2
             ↳Overlay and local confluence Check



The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost. 


   R
     ↳OrthoCSR
       →TRS1
         ↳CSRtoTRS
           →TRS2
             ↳OC
             ...
               →TRS3
                 ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

U11'(tt, M, N) -> U12'(tt, a(M), a(N))
U12'(tt, M, N) -> PLUS(a(N), a(M))
PLUS(N, s(M)) -> U11'(tt, M, N)
U21'(tt, M, N) -> U22'(tt, a(M), a(N))
U22'(tt, M, N) -> PLUS(x(a(N), a(M)), a(N))
U22'(tt, M, N) -> X(a(N), a(M))
X(N, s(M)) -> U21'(tt, M, N)

R contains no SCCs.

Termination of R successfully shown.
Duration:
0:03 minutes