YES Termination Proof using AProVETerm Rewriting System R:
[V1, V2, N, M, X]
U11(tt, V1, V2) -> U12(isNat(V1), V2)
U12(tt, V2) -> U13(isNat(V2))
U13(tt) -> tt
U21(tt, V1) -> U22(isNat(V1))
U22(tt) -> tt
U31(tt, V1, V2) -> U32(isNat(V1), V2)
U32(tt, V2) -> U33(isNat(V2))
U33(tt) -> tt
U41(tt, N) -> N
U51(tt, M, N) -> s(plus(N, M))
U61(tt) -> 0
U71(tt, M, N) -> plus(x(N, M), N)
and(tt, X) -> X
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) -> isNatKind(V1)
isNatKind(x(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
plus(N, 0) -> U41(and(isNat(N), isNatKind(N)), N)
plus(N, s(M)) -> U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
x(N, 0) -> U61(and(isNat(N), isNatKind(N)))
x(N, s(M)) -> U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)

Termination of R to be shown. 



   TRS
     ↳CSR to TRS Transformation




Trivial-Transformation successful.
Replacement map:
U71(1, 2, 3)
and(1, 2)
plus(1, 2)
U31(1, 2, 3)
x(1, 2)
U12(1, 2)
U11(1, 2, 3)
U22(1)
U33(1)
isNat(1)
U51(1, 2, 3)
U41(1, 2)
U32(1, 2)
U21(1, 2)
U13(1)
U61(1)
s(1)
isNatKind(1)

Old CSR:

U11(tt, V1, V2) -> U12(isNat(V1), V2)
U12(tt, V2) -> U13(isNat(V2))
U13(tt) -> tt
U21(tt, V1) -> U22(isNat(V1))
U22(tt) -> tt
U31(tt, V1, V2) -> U32(isNat(V1), V2)
U32(tt, V2) -> U33(isNat(V2))
U33(tt) -> tt
U41(tt, N) -> N
U51(tt, M, N) -> s(plus(N, M))
U61(tt) -> 0
U71(tt, M, N) -> plus(x(N, M), N)
and(tt, X) -> X
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) -> isNatKind(V1)
isNatKind(x(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
plus(N, 0) -> U41(and(isNat(N), isNatKind(N)), N)
plus(N, s(M)) -> U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
x(N, 0) -> U61(and(isNat(N), isNatKind(N)))
x(N, s(M)) -> U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)

new TRS:

U11(tt, V1, V2) -> U12(isNat(V1), V2)
U12(tt, V2) -> U13(isNat(V2))
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U13(tt) -> tt
U21(tt, V1) -> U22(isNat(V1))
U22(tt) -> tt
U31(tt, V1, V2) -> U32(isNat(V1), V2)
U32(tt, V2) -> U33(isNat(V2))
U33(tt) -> tt
U41(tt, N) -> N
U51(tt, M, N) -> s(plus(N, M))
plus(N, 0) -> U41(and(isNat(N), isNatKind(N)), N)
plus(N, s(M)) -> U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
U61(tt) -> 0
U71(tt, M, N) -> plus(x(N, M), N)
x(N, 0) -> U61(and(isNat(N), isNatKind(N)))
x(N, s(M)) -> U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
and(tt, X) -> X
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) -> isNatKind(V1)
isNatKind(x(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))



   TRS
     ↳CSRtoTRS
       →TRS1
         ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

U11'(tt, V1, V2) -> U12'(isNat(V1), V2)
U11'(tt, V1, V2) -> ISNAT(V1)
U12'(tt, V2) -> U13'(isNat(V2))
U12'(tt, V2) -> ISNAT(V2)
ISNAT(plus(V1, V2)) -> U11'(and(isNatKind(V1), isNatKind(V2)), V1, V2)
ISNAT(plus(V1, V2)) -> AND(isNatKind(V1), isNatKind(V2))
ISNAT(plus(V1, V2)) -> ISNATKIND(V1)
ISNAT(plus(V1, V2)) -> ISNATKIND(V2)
ISNAT(s(V1)) -> U21'(isNatKind(V1), V1)
ISNAT(s(V1)) -> ISNATKIND(V1)
ISNAT(x(V1, V2)) -> U31'(and(isNatKind(V1), isNatKind(V2)), V1, V2)
ISNAT(x(V1, V2)) -> AND(isNatKind(V1), isNatKind(V2))
ISNAT(x(V1, V2)) -> ISNATKIND(V1)
ISNAT(x(V1, V2)) -> ISNATKIND(V2)
U21'(tt, V1) -> U22'(isNat(V1))
U21'(tt, V1) -> ISNAT(V1)
U31'(tt, V1, V2) -> U32'(isNat(V1), V2)
U31'(tt, V1, V2) -> ISNAT(V1)
U32'(tt, V2) -> U33'(isNat(V2))
U32'(tt, V2) -> ISNAT(V2)
U51'(tt, M, N) -> PLUS(N, M)
PLUS(N, 0) -> U41'(and(isNat(N), isNatKind(N)), N)
PLUS(N, 0) -> AND(isNat(N), isNatKind(N))
PLUS(N, 0) -> ISNAT(N)
PLUS(N, 0) -> ISNATKIND(N)
PLUS(N, s(M)) -> U51'(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
PLUS(N, s(M)) -> AND(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
PLUS(N, s(M)) -> AND(isNat(M), isNatKind(M))
PLUS(N, s(M)) -> ISNAT(M)
PLUS(N, s(M)) -> ISNATKIND(M)
PLUS(N, s(M)) -> AND(isNat(N), isNatKind(N))
PLUS(N, s(M)) -> ISNAT(N)
PLUS(N, s(M)) -> ISNATKIND(N)
U71'(tt, M, N) -> PLUS(x(N, M), N)
U71'(tt, M, N) -> X(N, M)
X(N, 0) -> U61'(and(isNat(N), isNatKind(N)))
X(N, 0) -> AND(isNat(N), isNatKind(N))
X(N, 0) -> ISNAT(N)
X(N, 0) -> ISNATKIND(N)
X(N, s(M)) -> U71'(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
X(N, s(M)) -> AND(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
X(N, s(M)) -> AND(isNat(M), isNatKind(M))
X(N, s(M)) -> ISNAT(M)
X(N, s(M)) -> ISNATKIND(M)
X(N, s(M)) -> AND(isNat(N), isNatKind(N))
X(N, s(M)) -> ISNAT(N)
X(N, s(M)) -> ISNATKIND(N)
ISNATKIND(plus(V1, V2)) -> AND(isNatKind(V1), isNatKind(V2))
ISNATKIND(plus(V1, V2)) -> ISNATKIND(V1)
ISNATKIND(plus(V1, V2)) -> ISNATKIND(V2)
ISNATKIND(s(V1)) -> ISNATKIND(V1)
ISNATKIND(x(V1, V2)) -> AND(isNatKind(V1), isNatKind(V2))
ISNATKIND(x(V1, V2)) -> ISNATKIND(V1)
ISNATKIND(x(V1, V2)) -> ISNATKIND(V2)

Furthermore, R contains four SCCs. 


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳Size-Change Principle
           →DP Problem 2
             ↳SCP
           →DP Problem 3
             ↳SCP
           →DP Problem 4
             ↳SCP


Dependency Pairs:

ISNATKIND(x(V1, V2)) -> ISNATKIND(V2)
ISNATKIND(x(V1, V2)) -> ISNATKIND(V1)
ISNATKIND(s(V1)) -> ISNATKIND(V1)
ISNATKIND(plus(V1, V2)) -> ISNATKIND(V2)
ISNATKIND(plus(V1, V2)) -> ISNATKIND(V1)


Rules:


U11(tt, V1, V2) -> U12(isNat(V1), V2)
U12(tt, V2) -> U13(isNat(V2))
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U13(tt) -> tt
U21(tt, V1) -> U22(isNat(V1))
U22(tt) -> tt
U31(tt, V1, V2) -> U32(isNat(V1), V2)
U32(tt, V2) -> U33(isNat(V2))
U33(tt) -> tt
U41(tt, N) -> N
U51(tt, M, N) -> s(plus(N, M))
plus(N, 0) -> U41(and(isNat(N), isNatKind(N)), N)
plus(N, s(M)) -> U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
U61(tt) -> 0
U71(tt, M, N) -> plus(x(N, M), N)
x(N, 0) -> U61(and(isNat(N), isNatKind(N)))
x(N, s(M)) -> U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
and(tt, X) -> X
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) -> isNatKind(V1)
isNatKind(x(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))





We number the DPs as follows:
  1. ISNATKIND(x(V1, V2)) -> ISNATKIND(V2)
  2. ISNATKIND(x(V1, V2)) -> ISNATKIND(V1)
  3. ISNATKIND(s(V1)) -> ISNATKIND(V1)
  4. ISNATKIND(plus(V1, V2)) -> ISNATKIND(V2)
  5. ISNATKIND(plus(V1, V2)) -> ISNATKIND(V1)
and get the following Size-Change Graph(s):
{5, 4, 3, 2, 1} , {5, 4, 3, 2, 1}
1>1

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

DP: empty set
Oriented Rules: none

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

with Argument Filtering System:
plus(x1, x2) -> plus(x1, x2)
x(x1, x2) -> x(x1, x2)
s(x1) -> s(x1)

We obtain no new DP problems. 


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳Size-Change Principle
           →DP Problem 3
             ↳SCP
           →DP Problem 4
             ↳SCP


Dependency Pairs:

U31'(tt, V1, V2) -> ISNAT(V1)
U32'(tt, V2) -> ISNAT(V2)
U31'(tt, V1, V2) -> U32'(isNat(V1), V2)
ISNAT(x(V1, V2)) -> U31'(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U21'(tt, V1) -> ISNAT(V1)
ISNAT(s(V1)) -> U21'(isNatKind(V1), V1)
U11'(tt, V1, V2) -> ISNAT(V1)
ISNAT(plus(V1, V2)) -> U11'(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U12'(tt, V2) -> ISNAT(V2)
U11'(tt, V1, V2) -> U12'(isNat(V1), V2)


Rules:


U11(tt, V1, V2) -> U12(isNat(V1), V2)
U12(tt, V2) -> U13(isNat(V2))
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U13(tt) -> tt
U21(tt, V1) -> U22(isNat(V1))
U22(tt) -> tt
U31(tt, V1, V2) -> U32(isNat(V1), V2)
U32(tt, V2) -> U33(isNat(V2))
U33(tt) -> tt
U41(tt, N) -> N
U51(tt, M, N) -> s(plus(N, M))
plus(N, 0) -> U41(and(isNat(N), isNatKind(N)), N)
plus(N, s(M)) -> U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
U61(tt) -> 0
U71(tt, M, N) -> plus(x(N, M), N)
x(N, 0) -> U61(and(isNat(N), isNatKind(N)))
x(N, s(M)) -> U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
and(tt, X) -> X
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) -> isNatKind(V1)
isNatKind(x(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))





We number the DPs as follows:
  1. U31'(tt, V1, V2) -> ISNAT(V1)
  2. U32'(tt, V2) -> ISNAT(V2)
  3. U31'(tt, V1, V2) -> U32'(isNat(V1), V2)
  4. ISNAT(x(V1, V2)) -> U31'(and(isNatKind(V1), isNatKind(V2)), V1, V2)
  5. U21'(tt, V1) -> ISNAT(V1)
  6. ISNAT(s(V1)) -> U21'(isNatKind(V1), V1)
  7. U11'(tt, V1, V2) -> ISNAT(V1)
  8. ISNAT(plus(V1, V2)) -> U11'(and(isNatKind(V1), isNatKind(V2)), V1, V2)
  9. U12'(tt, V2) -> ISNAT(V2)
  10. U11'(tt, V1, V2) -> U12'(isNat(V1), V2)
and get the following Size-Change Graph(s):
{1} , {1}
2=1
{2} , {2}
2=1
{3} , {3}
3=2
{4} , {4}
1>2
1>3
{5} , {5}
2=1
{6} , {6}
1>2
{7} , {7}
2=1
{8} , {8}
1>2
1>3
{9} , {9}
2=1
{10} , {10}
3=2

which lead(s) to this/these maximal multigraph(s):
{1} , {4}
2>2
2>3
{7} , {8}
2>2
2>3
{5} , {6}
2>2
{6} , {5}
1>1
{4} , {1}
1>1
{8} , {7}
1>1
{4} , {2}
1>1
{2} , {3}
2>2
{8} , {9}
1>1
{9} , {10}
2>2
{3} , {4}
3>2
3>3
{10} , {8}
3>2
3>3
{4} , {7}
1>1
{6} , {7}
1>1
{4} , {5}
1>1
{8} , {1}
1>1
{8} , {5}
1>1
{6} , {1}
1>1
{8} , {2}
1>1
{6} , {9}
1>1
{4} , {9}
1>1
{6} , {2}
1>1

DP: empty set
Oriented Rules: none

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

with Argument Filtering System:
plus(x1, x2) -> plus(x1, x2)
x(x1, x2) -> x(x1, x2)
s(x1) -> s(x1)

We obtain no new DP problems. 


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳SCP
           →DP Problem 3
             ↳Size-Change Principle
           →DP Problem 4
             ↳SCP


Dependency Pairs:

PLUS(N, s(M)) -> U51'(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
U51'(tt, M, N) -> PLUS(N, M)


Rules:


U11(tt, V1, V2) -> U12(isNat(V1), V2)
U12(tt, V2) -> U13(isNat(V2))
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U13(tt) -> tt
U21(tt, V1) -> U22(isNat(V1))
U22(tt) -> tt
U31(tt, V1, V2) -> U32(isNat(V1), V2)
U32(tt, V2) -> U33(isNat(V2))
U33(tt) -> tt
U41(tt, N) -> N
U51(tt, M, N) -> s(plus(N, M))
plus(N, 0) -> U41(and(isNat(N), isNatKind(N)), N)
plus(N, s(M)) -> U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
U61(tt) -> 0
U71(tt, M, N) -> plus(x(N, M), N)
x(N, 0) -> U61(and(isNat(N), isNatKind(N)))
x(N, s(M)) -> U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
and(tt, X) -> X
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) -> isNatKind(V1)
isNatKind(x(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))





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

which lead(s) to this/these maximal multigraph(s):
{2} , {1}
2>2
3=3
{1} , {2}
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. 


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳SCP
           →DP Problem 3
             ↳SCP
           →DP Problem 4
             ↳Size-Change Principle


Dependency Pairs:

X(N, s(M)) -> U71'(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
U71'(tt, M, N) -> X(N, M)


Rules:


U11(tt, V1, V2) -> U12(isNat(V1), V2)
U12(tt, V2) -> U13(isNat(V2))
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U13(tt) -> tt
U21(tt, V1) -> U22(isNat(V1))
U22(tt) -> tt
U31(tt, V1, V2) -> U32(isNat(V1), V2)
U32(tt, V2) -> U33(isNat(V2))
U33(tt) -> tt
U41(tt, N) -> N
U51(tt, M, N) -> s(plus(N, M))
plus(N, 0) -> U41(and(isNat(N), isNatKind(N)), N)
plus(N, s(M)) -> U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
U61(tt) -> 0
U71(tt, M, N) -> plus(x(N, M), N)
x(N, 0) -> U61(and(isNat(N), isNatKind(N)))
x(N, s(M)) -> U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
and(tt, X) -> X
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) -> isNatKind(V1)
isNatKind(x(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))





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

which lead(s) to this/these maximal multigraph(s):
{2} , {1}
2>2
3=3
{1} , {2}
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:35 minutes