Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U12: {1}
isNat: empty set
U13: {1}
U21: {1}
U22: {1}
U31: {1}
U32: {1}
U33: {1}
U41: {1}
U51: {1}
s: {1}
plus: {1, 2}
U61: {1}
0: empty set
U71: {1}
x: {1, 2}
and: {1}
isNatKind: empty set


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U12: {1}
isNat: empty set
U13: {1}
U21: {1}
U22: {1}
U31: {1}
U32: {1}
U33: {1}
U41: {1}
U51: {1}
s: {1}
plus: {1, 2}
U61: {1}
0: empty set
U71: {1}
x: {1, 2}
and: {1}
isNatKind: empty set

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U22, U33, s, plus, U61, x, U131, U221, U331, PLUS, X, U611} are replacing on all positions.
For all symbols f in {U11, U12, U21, U31, U32, U41, U51, U71, and, U121, U111, U211, U321, U311, U511, U711, AND, U411} we have µ(f) = {1}.
The symbols in {isNat, isNatKind, ISNAT, ISNATKIND, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

U111(tt, V1, V2) → U121(isNat(V1), V2)
U111(tt, V1, V2) → ISNAT(V1)
U121(tt, V2) → U131(isNat(V2))
U121(tt, V2) → ISNAT(V2)
U211(tt, V1) → U221(isNat(V1))
U211(tt, V1) → ISNAT(V1)
U311(tt, V1, V2) → U321(isNat(V1), V2)
U311(tt, V1, V2) → ISNAT(V1)
U321(tt, V2) → U331(isNat(V2))
U321(tt, V2) → ISNAT(V2)
U511(tt, M, N) → PLUS(N, M)
U711(tt, M, N) → PLUS(x(N, M), N)
U711(tt, M, N) → X(N, M)
ISNAT(plus(V1, V2)) → U111(and(isNatKind(V1), isNatKind(V2)), V1, V2)
ISNAT(plus(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
ISNAT(plus(V1, V2)) → ISNATKIND(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
ISNAT(s(V1)) → ISNATKIND(V1)
ISNAT(x(V1, V2)) → U311(and(isNatKind(V1), isNatKind(V2)), V1, V2)
ISNAT(x(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
ISNAT(x(V1, V2)) → ISNATKIND(V1)
ISNATKIND(plus(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
ISNATKIND(plus(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
ISNATKIND(x(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
ISNATKIND(x(V1, V2)) → ISNATKIND(V1)
PLUS(N, 0) → U411(and(isNat(N), isNatKind(N)), N)
PLUS(N, 0) → AND(isNat(N), isNatKind(N))
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → U511(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)
X(N, 0) → U611(and(isNat(N), isNatKind(N)))
X(N, 0) → AND(isNat(N), isNatKind(N))
X(N, 0) → ISNAT(N)
X(N, s(M)) → U711(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)

The collapsing dependency pairs are DPc:

U411(tt, N) → N
U511(tt, M, N) → N
U511(tt, M, N) → M
U711(tt, M, N) → N
U711(tt, M, N) → M
AND(tt, X) → X


The hidden terms of R are:

isNatKind(V2)

Every hiding context is built from:

and on positions {1}

Hence, the new unhiding pairs DPu are :

U411(tt, N) → U(N)
U511(tt, M, N) → U(N)
U511(tt, M, N) → U(M)
U711(tt, M, N) → U(N)
U711(tt, M, N) → U(M)
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatKind(V2)) → ISNATKIND(V2)

The TRS R consists of the following rules:

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)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 4 SCCs with 26 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U22, U33, s, plus, U61, x} are replacing on all positions.
For all symbols f in {U11, U12, U21, U31, U32, U41, U51, U71, and, AND} we have µ(f) = {1}.
The symbols in {isNat, isNatKind, U, ISNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
U(isNatKind(V2)) → ISNATKIND(V2)
ISNATKIND(plus(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
AND(tt, X) → U(X)
ISNATKIND(plus(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
ISNATKIND(x(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
ISNATKIND(x(V1, V2)) → ISNATKIND(V1)

The TRS R consists of the following rules:

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)

Q is empty.

Using the order
Recursive path order with status [2].
Quasi-Precedence:
[x2, U713] > [plus2, U513] > [and2, s1] > U1 > ISNATKIND1
[x2, U713] > [plus2, U513] > [and2, s1] > isNatKind1 > ISNATKIND1
[x2, U713] > [plus2, U513] > [and2, s1] > U212 > isNat1 > ISNATKIND1
[x2, U713] > [plus2, U513] > [and2, s1] > U212 > U221 > ISNATKIND1
[x2, U713] > [plus2, U513] > AND2 > U1 > ISNATKIND1
[x2, U713] > [plus2, U513] > U412 > ISNATKIND1
[x2, U713] > [plus2, U513] > U113 > U122 > isNat1 > ISNATKIND1
[x2, U713] > [plus2, U513] > U113 > U122 > U131 > ISNATKIND1
[x2, U713] > U313 > U322 > isNat1 > ISNATKIND1
[x2, U713] > U313 > U322 > U331 > ISNATKIND1
[x2, U713] > U611 > [tt, 0] > U1 > ISNATKIND1
[x2, U713] > U611 > [tt, 0] > isNatKind1 > ISNATKIND1
[x2, U713] > U611 > [tt, 0] > U412 > ISNATKIND1
[x2, U713] > U611 > [tt, 0] > U122 > isNat1 > ISNATKIND1
[x2, U713] > U611 > [tt, 0] > U122 > U131 > ISNATKIND1
[x2, U713] > U611 > [tt, 0] > U221 > ISNATKIND1
[x2, U713] > U611 > [tt, 0] > U322 > isNat1 > ISNATKIND1
[x2, U713] > U611 > [tt, 0] > U322 > U331 > ISNATKIND1

Status:
plus2: [2,1]
U611: multiset
ISNATKIND1: multiset
U322: multiset
U113: multiset
x2: [1,2]
U122: multiset
and2: multiset
isNatKind1: multiset
0: multiset
U212: [1,2]
U313: multiset
U221: multiset
tt: multiset
U1: multiset
AND2: multiset
U412: [2,1]
U131: multiset
s1: [1]
U331: multiset
isNat1: multiset
U513: [2,3,1]
U713: [3,2,1]


the following usable rules

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))
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)
U41(tt, N) → N
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)
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
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)
U61(tt) → 0
U71(tt, M, N) → plus(x(N, M), N)
U31(tt, V1, V2) → U32(isNat(V1), V2)
U32(tt, V2) → U33(isNat(V2))
U33(tt) → tt
U51(tt, M, N) → s(plus(N, M))

could all be oriented weakly.
Furthermore, the pairs

U(and(x_0, x_1)) → U(x_0)
U(isNatKind(V2)) → ISNATKIND(V2)
ISNATKIND(plus(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
AND(tt, X) → U(X)
ISNATKIND(plus(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
ISNATKIND(x(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
ISNATKIND(x(V1, V2)) → ISNATKIND(V1)

could be oriented strictly and thus removed.
All pairs have been removed.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSDPReductionPairProof
              ↳ QCSDP
                ↳ PIsEmptyProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U22, U33, s, plus, U61, x} are replacing on all positions.
For all symbols f in {U11, U12, U21, U31, U32, U41, U51, U71, and} we have µ(f) = {1}.
The symbols in {isNat, isNatKind} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

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)

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U22, U33, s, plus, U61, x} are replacing on all positions.
For all symbols f in {U11, U12, U21, U31, U32, U41, U51, U71, and, U121, U111, U211, U311, U321} we have µ(f) = {1}.
The symbols in {isNat, isNatKind, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

U121(tt, V2) → ISNAT(V2)
ISNAT(plus(V1, V2)) → U111(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U111(tt, V1, V2) → U121(isNat(V1), V2)
U111(tt, V1, V2) → ISNAT(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U211(tt, V1) → ISNAT(V1)
ISNAT(x(V1, V2)) → U311(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U311(tt, V1, V2) → U321(isNat(V1), V2)
U321(tt, V2) → ISNAT(V2)
U311(tt, V1, V2) → ISNAT(V1)

The TRS R consists of the following rules:

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)

Q is empty.

Using the order
Recursive path order with status [2].
Quasi-Precedence:
[x2, U713] > [plus2, U513] > U11^13 > [U12^12, ISNAT1]
[x2, U713] > [plus2, U513] > U11^13 > isNat1
[x2, U713] > [plus2, U513] > [and2, s1] > isNatKind1 > tt > [U12^12, ISNAT1]
[x2, U713] > [plus2, U513] > [and2, s1] > isNatKind1 > tt > U221
[x2, U713] > [plus2, U513] > [and2, s1] > isNatKind1 > tt > U322 > isNat1
[x2, U713] > [plus2, U513] > [and2, s1] > isNatKind1 > tt > U322 > U331
[x2, U713] > [plus2, U513] > [and2, s1] > U21^12 > [U12^12, ISNAT1]
[x2, U713] > [plus2, U513] > [and2, s1] > U212 > isNat1
[x2, U713] > [plus2, U513] > [and2, s1] > U212 > U221
[x2, U713] > [plus2, U513] > [0, U412, U611] > isNatKind1 > tt > [U12^12, ISNAT1]
[x2, U713] > [plus2, U513] > [0, U412, U611] > isNatKind1 > tt > U221
[x2, U713] > [plus2, U513] > [0, U412, U611] > isNatKind1 > tt > U322 > isNat1
[x2, U713] > [plus2, U513] > [0, U412, U611] > isNatKind1 > tt > U322 > U331
[x2, U713] > [plus2, U513] > U113 > U122 > U131 > tt > [U12^12, ISNAT1]
[x2, U713] > [plus2, U513] > U113 > U122 > U131 > tt > U221
[x2, U713] > [plus2, U513] > U113 > U122 > U131 > tt > U322 > isNat1
[x2, U713] > [plus2, U513] > U113 > U122 > U131 > tt > U322 > U331
[x2, U713] > U31^13 > isNat1
[x2, U713] > U31^13 > U32^12 > [U12^12, ISNAT1]
[x2, U713] > U313 > U322 > isNat1
[x2, U713] > U313 > U322 > U331

Status:
U12^12: multiset
U322: multiset
U21^12: multiset
U122: multiset
x2: [1,2]
and2: multiset
U212: multiset
U313: multiset
tt: multiset
s1: [1]
isNat1: multiset
U513: [3,2,1]
plus2: [1,2]
U611: multiset
U31^13: multiset
U11^13: multiset
U113: multiset
U32^12: multiset
isNatKind1: multiset
0: multiset
ISNAT1: multiset
U221: [1]
U412: multiset
U131: [1]
U331: [1]
U713: [3,2,1]


the following usable rules

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)
U41(tt, N) → 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)
U11(tt, V1, V2) → U12(isNat(V1), V2)
U12(tt, V2) → U13(isNat(V2))
U13(tt) → tt
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))
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)
U61(tt) → 0
U71(tt, M, N) → plus(x(N, M), N)
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
U51(tt, M, N) → s(plus(N, M))

could all be oriented weakly.
Furthermore, the pairs

U121(tt, V2) → ISNAT(V2)
ISNAT(plus(V1, V2)) → U111(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U111(tt, V1, V2) → U121(isNat(V1), V2)
U111(tt, V1, V2) → ISNAT(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U211(tt, V1) → ISNAT(V1)
ISNAT(x(V1, V2)) → U311(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U311(tt, V1, V2) → U321(isNat(V1), V2)
U321(tt, V2) → ISNAT(V2)
U311(tt, V1, V2) → ISNAT(V1)

could be oriented strictly and thus removed.
All pairs have been removed.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPReductionPairProof
              ↳ QCSDP
                ↳ PIsEmptyProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U22, U33, s, plus, U61, x} are replacing on all positions.
For all symbols f in {U11, U12, U21, U31, U32, U41, U51, U71, and} we have µ(f) = {1}.
The symbols in {isNat, isNatKind} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

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)

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U22, U33, s, plus, U61, x, PLUS} are replacing on all positions.
For all symbols f in {U11, U12, U21, U31, U32, U41, U51, U71, and, U511} we have µ(f) = {1}.
The symbols in {isNat, isNatKind} are not replacing on any position.

The TRS P consists of the following rules:

PLUS(N, s(M)) → U511(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
U511(tt, M, N) → PLUS(N, M)

The TRS R consists of the following rules:

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)

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


PLUS(N, s(M)) → U511(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
The remaining pairs can at least be oriented weakly.

U511(tt, M, N) → PLUS(N, M)
Used ordering: Combined order from the following AFS and order.
U511(x1, x2, x3)  =  x2
PLUS(x1, x2)  =  x2

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U22, U33, s, plus, U61, x, PLUS} are replacing on all positions.
For all symbols f in {U11, U12, U21, U31, U32, U41, U51, U71, and, U511} we have µ(f) = {1}.
The symbols in {isNat, isNatKind} are not replacing on any position.

The TRS P consists of the following rules:

U511(tt, M, N) → PLUS(N, M)

The TRS R consists of the following rules:

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)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U22, U33, s, plus, U61, x, X} are replacing on all positions.
For all symbols f in {U11, U12, U21, U31, U32, U41, U51, U71, and, U711} we have µ(f) = {1}.
The symbols in {isNat, isNatKind} are not replacing on any position.

The TRS P consists of the following rules:

U711(tt, M, N) → X(N, M)
X(N, s(M)) → U711(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)

The TRS R consists of the following rules:

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)

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


X(N, s(M)) → U711(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
The remaining pairs can at least be oriented weakly.

U711(tt, M, N) → X(N, M)
Used ordering: Combined order from the following AFS and order.
X(x1, x2)  =  x2
U711(x1, x2, x3)  =  x2

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U13, U22, U33, s, plus, U61, x, X} are replacing on all positions.
For all symbols f in {U11, U12, U21, U31, U32, U41, U51, U71, and, U711} we have µ(f) = {1}.
The symbols in {isNat, isNatKind} are not replacing on any position.

The TRS P consists of the following rules:

U711(tt, M, N) → X(N, M)

The TRS R consists of the following rules:

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)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.