YES Termination Proof using AProVETerm Rewriting System R:
[M, N, V1, V2]
U101(tt, M, N) -> U102(isNatKind(M), M, N)
U102(tt, M, N) -> U103(isNat(N), M, N)
U103(tt, M, N) -> U104(isNatKind(N), M, N)
U104(tt, M, N) -> plus(x(N, M), N)
U11(tt, V1, V2) -> U12(isNatKind(V1), V1, V2)
U12(tt, V1, V2) -> U13(isNatKind(V2), V1, V2)
U13(tt, V1, V2) -> U14(isNatKind(V2), V1, V2)
U14(tt, V1, V2) -> U15(isNat(V1), V2)
U15(tt, V2) -> U16(isNat(V2))
U16(tt) -> tt
U21(tt, V1) -> U22(isNatKind(V1), V1)
U22(tt, V1) -> U23(isNat(V1))
U23(tt) -> tt
U31(tt, V1, V2) -> U32(isNatKind(V1), V1, V2)
U32(tt, V1, V2) -> U33(isNatKind(V2), V1, V2)
U33(tt, V1, V2) -> U34(isNatKind(V2), V1, V2)
U34(tt, V1, V2) -> U35(isNat(V1), V2)
U35(tt, V2) -> U36(isNat(V2))
U36(tt) -> tt
U41(tt, V2) -> U42(isNatKind(V2))
U42(tt) -> tt
U51(tt) -> tt
U61(tt, V2) -> U62(isNatKind(V2))
U62(tt) -> tt
U71(tt, N) -> U72(isNatKind(N), N)
U72(tt, N) -> N
U81(tt, M, N) -> U82(isNatKind(M), M, N)
U82(tt, M, N) -> U83(isNat(N), M, N)
U83(tt, M, N) -> U84(isNatKind(N), M, N)
U84(tt, M, N) -> s(plus(N, M))
U91(tt, N) -> U92(isNatKind(N))
U92(tt) -> 0
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(isNatKind(V1), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(isNatKind(V1), V1, V2)
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> U41(isNatKind(V1), V2)
isNatKind(s(V1)) -> U51(isNatKind(V1))
isNatKind(x(V1, V2)) -> U61(isNatKind(V1), V2)
plus(N, 0) -> U71(isNat(N), N)
plus(N, s(M)) -> U81(isNat(M), M, N)
x(N, 0) -> U91(isNat(N), N)
x(N, s(M)) -> U101(isNat(M), M, N)

Termination of R to be shown. 



   TRS
     ↳CSR to TRS Transformation




Trivial-Transformation successful.
Replacement map:
U71(1, 2)
U16(1)
U103(1, 2, 3)
x(1, 2)
U42(1)
U91(1, 2)
U11(1, 2, 3)
U33(1, 2, 3)
U84(1, 2, 3)
U14(1, 2, 3)
U51(1)
U62(1)
U36(1)
U101(1, 2, 3)
U21(1, 2)
U72(1, 2)
U13(1, 2, 3)
U35(1, 2)
U82(1, 2, 3)
plus(1, 2)
U31(1, 2, 3)
U34(1, 2, 3)
U92(1)
U12(1, 2, 3)
U23(1)
U15(1, 2)
U102(1, 2, 3)
U22(1, 2)
U81(1, 2, 3)
isNat(1)
U41(1, 2)
U32(1, 2, 3)
U61(1, 2)
s(1)
U83(1, 2, 3)
U104(1, 2, 3)
isNatKind(1)

Old CSR:

U101(tt, M, N) -> U102(isNatKind(M), M, N)
U102(tt, M, N) -> U103(isNat(N), M, N)
U103(tt, M, N) -> U104(isNatKind(N), M, N)
U104(tt, M, N) -> plus(x(N, M), N)
U11(tt, V1, V2) -> U12(isNatKind(V1), V1, V2)
U12(tt, V1, V2) -> U13(isNatKind(V2), V1, V2)
U13(tt, V1, V2) -> U14(isNatKind(V2), V1, V2)
U14(tt, V1, V2) -> U15(isNat(V1), V2)
U15(tt, V2) -> U16(isNat(V2))
U16(tt) -> tt
U21(tt, V1) -> U22(isNatKind(V1), V1)
U22(tt, V1) -> U23(isNat(V1))
U23(tt) -> tt
U31(tt, V1, V2) -> U32(isNatKind(V1), V1, V2)
U32(tt, V1, V2) -> U33(isNatKind(V2), V1, V2)
U33(tt, V1, V2) -> U34(isNatKind(V2), V1, V2)
U34(tt, V1, V2) -> U35(isNat(V1), V2)
U35(tt, V2) -> U36(isNat(V2))
U36(tt) -> tt
U41(tt, V2) -> U42(isNatKind(V2))
U42(tt) -> tt
U51(tt) -> tt
U61(tt, V2) -> U62(isNatKind(V2))
U62(tt) -> tt
U71(tt, N) -> U72(isNatKind(N), N)
U72(tt, N) -> N
U81(tt, M, N) -> U82(isNatKind(M), M, N)
U82(tt, M, N) -> U83(isNat(N), M, N)
U83(tt, M, N) -> U84(isNatKind(N), M, N)
U84(tt, M, N) -> s(plus(N, M))
U91(tt, N) -> U92(isNatKind(N))
U92(tt) -> 0
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(isNatKind(V1), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(isNatKind(V1), V1, V2)
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> U41(isNatKind(V1), V2)
isNatKind(s(V1)) -> U51(isNatKind(V1))
isNatKind(x(V1, V2)) -> U61(isNatKind(V1), V2)
plus(N, 0) -> U71(isNat(N), N)
plus(N, s(M)) -> U81(isNat(M), M, N)
x(N, 0) -> U91(isNat(N), N)
x(N, s(M)) -> U101(isNat(M), M, N)

new TRS:

U101(tt, M, N) -> U102(isNatKind(M), M, N)
U102(tt, M, N) -> U103(isNat(N), M, N)
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> U41(isNatKind(V1), V2)
isNatKind(s(V1)) -> U51(isNatKind(V1))
isNatKind(x(V1, V2)) -> U61(isNatKind(V1), V2)
U103(tt, M, N) -> U104(isNatKind(N), M, N)
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(isNatKind(V1), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(isNatKind(V1), V1, V2)
U104(tt, M, N) -> plus(x(N, M), N)
plus(N, 0) -> U71(isNat(N), N)
plus(N, s(M)) -> U81(isNat(M), M, N)
x(N, 0) -> U91(isNat(N), N)
x(N, s(M)) -> U101(isNat(M), M, N)
U11(tt, V1, V2) -> U12(isNatKind(V1), V1, V2)
U12(tt, V1, V2) -> U13(isNatKind(V2), V1, V2)
U13(tt, V1, V2) -> U14(isNatKind(V2), V1, V2)
U14(tt, V1, V2) -> U15(isNat(V1), V2)
U15(tt, V2) -> U16(isNat(V2))
U16(tt) -> tt
U21(tt, V1) -> U22(isNatKind(V1), V1)
U22(tt, V1) -> U23(isNat(V1))
U23(tt) -> tt
U31(tt, V1, V2) -> U32(isNatKind(V1), V1, V2)
U32(tt, V1, V2) -> U33(isNatKind(V2), V1, V2)
U33(tt, V1, V2) -> U34(isNatKind(V2), V1, V2)
U34(tt, V1, V2) -> U35(isNat(V1), V2)
U35(tt, V2) -> U36(isNat(V2))
U36(tt) -> tt
U41(tt, V2) -> U42(isNatKind(V2))
U42(tt) -> tt
U51(tt) -> tt
U61(tt, V2) -> U62(isNatKind(V2))
U62(tt) -> tt
U71(tt, N) -> U72(isNatKind(N), N)
U72(tt, N) -> N
U81(tt, M, N) -> U82(isNatKind(M), M, N)
U82(tt, M, N) -> U83(isNat(N), M, N)
U83(tt, M, N) -> U84(isNatKind(N), M, N)
U84(tt, M, N) -> s(plus(N, M))
U91(tt, N) -> U92(isNatKind(N))
U92(tt) -> 0



   TRS
     ↳CSRtoTRS
       →TRS1
         ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

U101'(tt, M, N) -> U102'(isNatKind(M), M, N)
U101'(tt, M, N) -> ISNATKIND(M)
U102'(tt, M, N) -> U103'(isNat(N), M, N)
U102'(tt, M, N) -> ISNAT(N)
ISNATKIND(plus(V1, V2)) -> U41'(isNatKind(V1), V2)
ISNATKIND(plus(V1, V2)) -> ISNATKIND(V1)
ISNATKIND(s(V1)) -> U51'(isNatKind(V1))
ISNATKIND(s(V1)) -> ISNATKIND(V1)
ISNATKIND(x(V1, V2)) -> U61'(isNatKind(V1), V2)
ISNATKIND(x(V1, V2)) -> ISNATKIND(V1)
U103'(tt, M, N) -> U104'(isNatKind(N), M, N)
U103'(tt, M, N) -> ISNATKIND(N)
ISNAT(plus(V1, V2)) -> U11'(isNatKind(V1), V1, V2)
ISNAT(plus(V1, V2)) -> ISNATKIND(V1)
ISNAT(s(V1)) -> U21'(isNatKind(V1), V1)
ISNAT(s(V1)) -> ISNATKIND(V1)
ISNAT(x(V1, V2)) -> U31'(isNatKind(V1), V1, V2)
ISNAT(x(V1, V2)) -> ISNATKIND(V1)
U104'(tt, M, N) -> PLUS(x(N, M), N)
U104'(tt, M, N) -> X(N, M)
PLUS(N, 0) -> U71'(isNat(N), N)
PLUS(N, 0) -> ISNAT(N)
PLUS(N, s(M)) -> U81'(isNat(M), M, N)
PLUS(N, s(M)) -> ISNAT(M)
X(N, 0) -> U91'(isNat(N), N)
X(N, 0) -> ISNAT(N)
X(N, s(M)) -> U101'(isNat(M), M, N)
X(N, s(M)) -> ISNAT(M)
U11'(tt, V1, V2) -> U12'(isNatKind(V1), V1, V2)
U11'(tt, V1, V2) -> ISNATKIND(V1)
U12'(tt, V1, V2) -> U13'(isNatKind(V2), V1, V2)
U12'(tt, V1, V2) -> ISNATKIND(V2)
U13'(tt, V1, V2) -> U14'(isNatKind(V2), V1, V2)
U13'(tt, V1, V2) -> ISNATKIND(V2)
U14'(tt, V1, V2) -> U15'(isNat(V1), V2)
U14'(tt, V1, V2) -> ISNAT(V1)
U15'(tt, V2) -> U16'(isNat(V2))
U15'(tt, V2) -> ISNAT(V2)
U21'(tt, V1) -> U22'(isNatKind(V1), V1)
U21'(tt, V1) -> ISNATKIND(V1)
U22'(tt, V1) -> U23'(isNat(V1))
U22'(tt, V1) -> ISNAT(V1)
U31'(tt, V1, V2) -> U32'(isNatKind(V1), V1, V2)
U31'(tt, V1, V2) -> ISNATKIND(V1)
U32'(tt, V1, V2) -> U33'(isNatKind(V2), V1, V2)
U32'(tt, V1, V2) -> ISNATKIND(V2)
U33'(tt, V1, V2) -> U34'(isNatKind(V2), V1, V2)
U33'(tt, V1, V2) -> ISNATKIND(V2)
U34'(tt, V1, V2) -> U35'(isNat(V1), V2)
U34'(tt, V1, V2) -> ISNAT(V1)
U35'(tt, V2) -> U36'(isNat(V2))
U35'(tt, V2) -> ISNAT(V2)
U41'(tt, V2) -> U42'(isNatKind(V2))
U41'(tt, V2) -> ISNATKIND(V2)
U61'(tt, V2) -> U62'(isNatKind(V2))
U61'(tt, V2) -> ISNATKIND(V2)
U71'(tt, N) -> U72'(isNatKind(N), N)
U71'(tt, N) -> ISNATKIND(N)
U81'(tt, M, N) -> U82'(isNatKind(M), M, N)
U81'(tt, M, N) -> ISNATKIND(M)
U82'(tt, M, N) -> U83'(isNat(N), M, N)
U82'(tt, M, N) -> ISNAT(N)
U83'(tt, M, N) -> U84'(isNatKind(N), M, N)
U83'(tt, M, N) -> ISNATKIND(N)
U84'(tt, M, N) -> PLUS(N, M)
U91'(tt, N) -> U92'(isNatKind(N))
U91'(tt, N) -> ISNATKIND(N)

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(V1)
U61'(tt, V2) -> ISNATKIND(V2)
ISNATKIND(x(V1, V2)) -> U61'(isNatKind(V1), V2)
ISNATKIND(s(V1)) -> ISNATKIND(V1)
ISNATKIND(plus(V1, V2)) -> ISNATKIND(V1)
U41'(tt, V2) -> ISNATKIND(V2)
ISNATKIND(plus(V1, V2)) -> U41'(isNatKind(V1), V2)


Rules:


U101(tt, M, N) -> U102(isNatKind(M), M, N)
U102(tt, M, N) -> U103(isNat(N), M, N)
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> U41(isNatKind(V1), V2)
isNatKind(s(V1)) -> U51(isNatKind(V1))
isNatKind(x(V1, V2)) -> U61(isNatKind(V1), V2)
U103(tt, M, N) -> U104(isNatKind(N), M, N)
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(isNatKind(V1), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(isNatKind(V1), V1, V2)
U104(tt, M, N) -> plus(x(N, M), N)
plus(N, 0) -> U71(isNat(N), N)
plus(N, s(M)) -> U81(isNat(M), M, N)
x(N, 0) -> U91(isNat(N), N)
x(N, s(M)) -> U101(isNat(M), M, N)
U11(tt, V1, V2) -> U12(isNatKind(V1), V1, V2)
U12(tt, V1, V2) -> U13(isNatKind(V2), V1, V2)
U13(tt, V1, V2) -> U14(isNatKind(V2), V1, V2)
U14(tt, V1, V2) -> U15(isNat(V1), V2)
U15(tt, V2) -> U16(isNat(V2))
U16(tt) -> tt
U21(tt, V1) -> U22(isNatKind(V1), V1)
U22(tt, V1) -> U23(isNat(V1))
U23(tt) -> tt
U31(tt, V1, V2) -> U32(isNatKind(V1), V1, V2)
U32(tt, V1, V2) -> U33(isNatKind(V2), V1, V2)
U33(tt, V1, V2) -> U34(isNatKind(V2), V1, V2)
U34(tt, V1, V2) -> U35(isNat(V1), V2)
U35(tt, V2) -> U36(isNat(V2))
U36(tt) -> tt
U41(tt, V2) -> U42(isNatKind(V2))
U42(tt) -> tt
U51(tt) -> tt
U61(tt, V2) -> U62(isNatKind(V2))
U62(tt) -> tt
U71(tt, N) -> U72(isNatKind(N), N)
U72(tt, N) -> N
U81(tt, M, N) -> U82(isNatKind(M), M, N)
U82(tt, M, N) -> U83(isNat(N), M, N)
U83(tt, M, N) -> U84(isNatKind(N), M, N)
U84(tt, M, N) -> s(plus(N, M))
U91(tt, N) -> U92(isNatKind(N))
U92(tt) -> 0





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

which lead(s) to this/these maximal multigraph(s):
{5, 4, 1} , {5, 4, 1}
1>1
{3} , {2}
1>1
{7} , {6}
1>1
{2} , {3}
2>2
{6} , {7}
2>2
{5, 4, 1} , {2}
1>1
{7} , {5, 4, 1}
1>1
{3} , {5, 4, 1}
1>1
{5, 4, 1} , {6}
1>1
{3} , {6}
1>1
{7} , {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
             ↳Size-Change Principle
           →DP Problem 3
             ↳SCP
           →DP Problem 4
             ↳SCP


Dependency Pairs:

U14'(tt, V1, V2) -> ISNAT(V1)
U34'(tt, V1, V2) -> ISNAT(V1)
U35'(tt, V2) -> ISNAT(V2)
U34'(tt, V1, V2) -> U35'(isNat(V1), V2)
U33'(tt, V1, V2) -> U34'(isNatKind(V2), V1, V2)
U32'(tt, V1, V2) -> U33'(isNatKind(V2), V1, V2)
U31'(tt, V1, V2) -> U32'(isNatKind(V1), V1, V2)
ISNAT(x(V1, V2)) -> U31'(isNatKind(V1), V1, V2)
U22'(tt, V1) -> ISNAT(V1)
U21'(tt, V1) -> U22'(isNatKind(V1), V1)
ISNAT(s(V1)) -> U21'(isNatKind(V1), V1)
U15'(tt, V2) -> ISNAT(V2)
U14'(tt, V1, V2) -> U15'(isNat(V1), V2)
U13'(tt, V1, V2) -> U14'(isNatKind(V2), V1, V2)
U12'(tt, V1, V2) -> U13'(isNatKind(V2), V1, V2)
U11'(tt, V1, V2) -> U12'(isNatKind(V1), V1, V2)
ISNAT(plus(V1, V2)) -> U11'(isNatKind(V1), V1, V2)


Rules:


U101(tt, M, N) -> U102(isNatKind(M), M, N)
U102(tt, M, N) -> U103(isNat(N), M, N)
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> U41(isNatKind(V1), V2)
isNatKind(s(V1)) -> U51(isNatKind(V1))
isNatKind(x(V1, V2)) -> U61(isNatKind(V1), V2)
U103(tt, M, N) -> U104(isNatKind(N), M, N)
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(isNatKind(V1), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(isNatKind(V1), V1, V2)
U104(tt, M, N) -> plus(x(N, M), N)
plus(N, 0) -> U71(isNat(N), N)
plus(N, s(M)) -> U81(isNat(M), M, N)
x(N, 0) -> U91(isNat(N), N)
x(N, s(M)) -> U101(isNat(M), M, N)
U11(tt, V1, V2) -> U12(isNatKind(V1), V1, V2)
U12(tt, V1, V2) -> U13(isNatKind(V2), V1, V2)
U13(tt, V1, V2) -> U14(isNatKind(V2), V1, V2)
U14(tt, V1, V2) -> U15(isNat(V1), V2)
U15(tt, V2) -> U16(isNat(V2))
U16(tt) -> tt
U21(tt, V1) -> U22(isNatKind(V1), V1)
U22(tt, V1) -> U23(isNat(V1))
U23(tt) -> tt
U31(tt, V1, V2) -> U32(isNatKind(V1), V1, V2)
U32(tt, V1, V2) -> U33(isNatKind(V2), V1, V2)
U33(tt, V1, V2) -> U34(isNatKind(V2), V1, V2)
U34(tt, V1, V2) -> U35(isNat(V1), V2)
U35(tt, V2) -> U36(isNat(V2))
U36(tt) -> tt
U41(tt, V2) -> U42(isNatKind(V2))
U42(tt) -> tt
U51(tt) -> tt
U61(tt, V2) -> U62(isNatKind(V2))
U62(tt) -> tt
U71(tt, N) -> U72(isNatKind(N), N)
U72(tt, N) -> N
U81(tt, M, N) -> U82(isNatKind(M), M, N)
U82(tt, M, N) -> U83(isNat(N), M, N)
U83(tt, M, N) -> U84(isNatKind(N), M, N)
U84(tt, M, N) -> s(plus(N, M))
U91(tt, N) -> U92(isNatKind(N))
U92(tt) -> 0





We number the DPs as follows:
  1. U14'(tt, V1, V2) -> ISNAT(V1)
  2. U34'(tt, V1, V2) -> ISNAT(V1)
  3. U35'(tt, V2) -> ISNAT(V2)
  4. U34'(tt, V1, V2) -> U35'(isNat(V1), V2)
  5. U33'(tt, V1, V2) -> U34'(isNatKind(V2), V1, V2)
  6. U32'(tt, V1, V2) -> U33'(isNatKind(V2), V1, V2)
  7. U31'(tt, V1, V2) -> U32'(isNatKind(V1), V1, V2)
  8. ISNAT(x(V1, V2)) -> U31'(isNatKind(V1), V1, V2)
  9. U22'(tt, V1) -> ISNAT(V1)
  10. U21'(tt, V1) -> U22'(isNatKind(V1), V1)
  11. ISNAT(s(V1)) -> U21'(isNatKind(V1), V1)
  12. U15'(tt, V2) -> ISNAT(V2)
  13. U14'(tt, V1, V2) -> U15'(isNat(V1), V2)
  14. U13'(tt, V1, V2) -> U14'(isNatKind(V2), V1, V2)
  15. U12'(tt, V1, V2) -> U13'(isNatKind(V2), V1, V2)
  16. U11'(tt, V1, V2) -> U12'(isNatKind(V1), V1, V2)
  17. ISNAT(plus(V1, V2)) -> U11'(isNatKind(V1), V1, V2)
and get the following Size-Change Graph(s):
{1} , {1}
2=1
{2} , {2}
2=1
{3} , {3}
2=1
{4} , {4}
3=2
{5} , {5}
2=2
3=3
{6} , {6}
2=2
3=3
{7} , {7}
2=2
3=3
{8} , {8}
1>2
1>3
{9} , {9}
2=1
{10} , {10}
2=2
{11} , {11}
1>2
{12} , {12}
2=1
{13} , {13}
3=2
{14} , {14}
2=2
3=3
{15} , {15}
2=2
3=3
{16} , {16}
2=2
3=3
{17} , {17}
1>2
1>3

which lead(s) to this/these maximal multigraph(s):
{10} , {11}
2>2
{11} , {9}
1>1
{9} , {10}
2>2
{15} , {16}
2>2
2>3
{7} , {8}
2>2
2>3
{8} , {2}
1>1
{16} , {17}
2>2
2>3
{2} , {5}
2>2
2>3
{17} , {1}
1>1
{6} , {7}
2>2
2>3
{5} , {6}
2>2
2>3
{1} , {14}
2>2
2>3
{14} , {15}
2>2
2>3
{7} , {8}
3>2
3>3
{6} , {7}
3>2
3>3
{15} , {16}
3>2
3>3
{14} , {15}
3>2
3>3
{13} , {14}
3>2
3>3
{12} , {13}
2>2
{16} , {17}
3>2
3>3
{8} , {3}
1>1
{17} , {12}
1>1
{4} , {5}
3>2
3>3
{5} , {6}
3>2
3>3
{3} , {4}
2>2
{8} , {9}
1>1
{11} , {2}
1>1
{11} , {1}
1>1
{17} , {9}
1>1
{11} , {3}
1>1
{11} , {12}
1>1
{17} , {2}
1>1
{8} , {1}
1>1
{17} , {3}
1>1
{8} , {12}
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:

U84'(tt, M, N) -> PLUS(N, M)
U83'(tt, M, N) -> U84'(isNatKind(N), M, N)
U82'(tt, M, N) -> U83'(isNat(N), M, N)
U81'(tt, M, N) -> U82'(isNatKind(M), M, N)
PLUS(N, s(M)) -> U81'(isNat(M), M, N)


Rules:


U101(tt, M, N) -> U102(isNatKind(M), M, N)
U102(tt, M, N) -> U103(isNat(N), M, N)
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> U41(isNatKind(V1), V2)
isNatKind(s(V1)) -> U51(isNatKind(V1))
isNatKind(x(V1, V2)) -> U61(isNatKind(V1), V2)
U103(tt, M, N) -> U104(isNatKind(N), M, N)
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(isNatKind(V1), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(isNatKind(V1), V1, V2)
U104(tt, M, N) -> plus(x(N, M), N)
plus(N, 0) -> U71(isNat(N), N)
plus(N, s(M)) -> U81(isNat(M), M, N)
x(N, 0) -> U91(isNat(N), N)
x(N, s(M)) -> U101(isNat(M), M, N)
U11(tt, V1, V2) -> U12(isNatKind(V1), V1, V2)
U12(tt, V1, V2) -> U13(isNatKind(V2), V1, V2)
U13(tt, V1, V2) -> U14(isNatKind(V2), V1, V2)
U14(tt, V1, V2) -> U15(isNat(V1), V2)
U15(tt, V2) -> U16(isNat(V2))
U16(tt) -> tt
U21(tt, V1) -> U22(isNatKind(V1), V1)
U22(tt, V1) -> U23(isNat(V1))
U23(tt) -> tt
U31(tt, V1, V2) -> U32(isNatKind(V1), V1, V2)
U32(tt, V1, V2) -> U33(isNatKind(V2), V1, V2)
U33(tt, V1, V2) -> U34(isNatKind(V2), V1, V2)
U34(tt, V1, V2) -> U35(isNat(V1), V2)
U35(tt, V2) -> U36(isNat(V2))
U36(tt) -> tt
U41(tt, V2) -> U42(isNatKind(V2))
U42(tt) -> tt
U51(tt) -> tt
U61(tt, V2) -> U62(isNatKind(V2))
U62(tt) -> tt
U71(tt, N) -> U72(isNatKind(N), N)
U72(tt, N) -> N
U81(tt, M, N) -> U82(isNatKind(M), M, N)
U82(tt, M, N) -> U83(isNat(N), M, N)
U83(tt, M, N) -> U84(isNatKind(N), M, N)
U84(tt, M, N) -> s(plus(N, M))
U91(tt, N) -> U92(isNatKind(N))
U92(tt) -> 0





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

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

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)) -> U101'(isNat(M), M, N)
U104'(tt, M, N) -> X(N, M)
U103'(tt, M, N) -> U104'(isNatKind(N), M, N)
U102'(tt, M, N) -> U103'(isNat(N), M, N)
U101'(tt, M, N) -> U102'(isNatKind(M), M, N)


Rules:


U101(tt, M, N) -> U102(isNatKind(M), M, N)
U102(tt, M, N) -> U103(isNat(N), M, N)
isNatKind(0) -> tt
isNatKind(plus(V1, V2)) -> U41(isNatKind(V1), V2)
isNatKind(s(V1)) -> U51(isNatKind(V1))
isNatKind(x(V1, V2)) -> U61(isNatKind(V1), V2)
U103(tt, M, N) -> U104(isNatKind(N), M, N)
isNat(0) -> tt
isNat(plus(V1, V2)) -> U11(isNatKind(V1), V1, V2)
isNat(s(V1)) -> U21(isNatKind(V1), V1)
isNat(x(V1, V2)) -> U31(isNatKind(V1), V1, V2)
U104(tt, M, N) -> plus(x(N, M), N)
plus(N, 0) -> U71(isNat(N), N)
plus(N, s(M)) -> U81(isNat(M), M, N)
x(N, 0) -> U91(isNat(N), N)
x(N, s(M)) -> U101(isNat(M), M, N)
U11(tt, V1, V2) -> U12(isNatKind(V1), V1, V2)
U12(tt, V1, V2) -> U13(isNatKind(V2), V1, V2)
U13(tt, V1, V2) -> U14(isNatKind(V2), V1, V2)
U14(tt, V1, V2) -> U15(isNat(V1), V2)
U15(tt, V2) -> U16(isNat(V2))
U16(tt) -> tt
U21(tt, V1) -> U22(isNatKind(V1), V1)
U22(tt, V1) -> U23(isNat(V1))
U23(tt) -> tt
U31(tt, V1, V2) -> U32(isNatKind(V1), V1, V2)
U32(tt, V1, V2) -> U33(isNatKind(V2), V1, V2)
U33(tt, V1, V2) -> U34(isNatKind(V2), V1, V2)
U34(tt, V1, V2) -> U35(isNat(V1), V2)
U35(tt, V2) -> U36(isNat(V2))
U36(tt) -> tt
U41(tt, V2) -> U42(isNatKind(V2))
U42(tt) -> tt
U51(tt) -> tt
U61(tt, V2) -> U62(isNatKind(V2))
U62(tt) -> tt
U71(tt, N) -> U72(isNatKind(N), N)
U72(tt, N) -> N
U81(tt, M, N) -> U82(isNatKind(M), M, N)
U82(tt, M, N) -> U83(isNat(N), M, N)
U83(tt, M, N) -> U84(isNatKind(N), M, N)
U84(tt, M, N) -> s(plus(N, M))
U91(tt, N) -> U92(isNatKind(N))
U92(tt) -> 0





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

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

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:
1:50 minutes