YES Termination Proof using AProVETerm Rewriting System R:
[X, N, M]
and(tt, X) -> X
plus(N, 0) -> N
plus(N, s(M)) -> s(plus(N, M))
x(N, 0) -> 0
x(N, s(M)) -> plus(x(N, 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:
and(1, 2)
plus(1, 2)
x(1, 2)
s(1)

Old CSR:

and(tt, X) -> X
plus(N, 0) -> N
plus(N, s(M)) -> s(plus(N, M))
x(N, 0) -> 0
x(N, s(M)) -> plus(x(N, M), N)

new TRS:

and(tt, X) -> a(X)
plus(N, 0) -> N
plus(N, s(M)) -> s(plus(N, M))
x(N, 0) -> 0
x(N, s(M)) -> plus(x(N, 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:

PLUS(N, s(M)) -> PLUS(N, M)
X(N, s(M)) -> PLUS(x(N, M), N)
X(N, s(M)) -> X(N, M)

Furthermore, R contains two SCCs. 


   R
     ↳OrthoCSR
       →TRS1
         ↳CSRtoTRS
           →TRS2
             ↳OC
             ...
               →DP Problem 1
                 ↳Usable Rules (Innermost)


Dependency Pair:

PLUS(N, s(M)) -> PLUS(N, M)


Rules:


and(tt, X) -> a(X)
plus(N, 0) -> N
plus(N, s(M)) -> s(plus(N, M))
x(N, 0) -> 0
x(N, s(M)) -> plus(x(N, M), N)


Strategy:

innermost




As we are in the innermost case, we can delete all 5 non-usable-rules.


   R
     ↳OrthoCSR
       →TRS1
         ↳CSRtoTRS
           →TRS2
             ↳OC
             ...
               →DP Problem 3
                 ↳Size-Change Principle


Dependency Pair:

PLUS(N, s(M)) -> PLUS(N, M)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. PLUS(N, s(M)) -> PLUS(N, M)
and get the following Size-Change Graph(s):
{1} , {1}
1=1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1=1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems. 


   R
     ↳OrthoCSR
       →TRS1
         ↳CSRtoTRS
           →TRS2
             ↳OC
             ...
               →DP Problem 2
                 ↳Usable Rules (Innermost)


Dependency Pair:

X(N, s(M)) -> X(N, M)


Rules:


and(tt, X) -> a(X)
plus(N, 0) -> N
plus(N, s(M)) -> s(plus(N, M))
x(N, 0) -> 0
x(N, s(M)) -> plus(x(N, M), N)


Strategy:

innermost




As we are in the innermost case, we can delete all 5 non-usable-rules.


   R
     ↳OrthoCSR
       →TRS1
         ↳CSRtoTRS
           →TRS2
             ↳OC
             ...
               →DP Problem 4
                 ↳Size-Change Principle


Dependency Pair:

X(N, s(M)) -> X(N, M)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. X(N, s(M)) -> X(N, M)
and get the following Size-Change Graph(s):
{1} , {1}
1=1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1=1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems.

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