YES Termination proof of ../tpdb/TRS/CSR_Maude/my-nat/MYNAT_nokinds.trs
Termination of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt, N) → N
U21(tt, M, N) → s(plus(N, M))
U31(tt) → 0
U41(tt, M, N) → plus(x(N, M), N)
and(tt, X) → X
isNat(0) → tt
isNat(plus(V1, V2)) → and(isNat(V1), isNat(V2))
isNat(s(V1)) → isNat(V1)
isNat(x(V1, V2)) → and(isNat(V1), isNat(V2))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNat(N)), M, N)
x(N, 0) → U31(isNat(N))
x(N, s(M)) → U41(and(isNat(M), isNat(N)), M, N)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U21: {1}
s: {1}
plus: {1, 2}
U31: {1}
0: empty set
U41: {1}
x: {1, 2}
and: {1}
isNat: empty set


↳ CSR
  ↳ Zantema-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt, N) → N
U21(tt, M, N) → s(plus(N, M))
U31(tt) → 0
U41(tt, M, N) → plus(x(N, M), N)
and(tt, X) → X
isNat(0) → tt
isNat(plus(V1, V2)) → and(isNat(V1), isNat(V2))
isNat(s(V1)) → isNat(V1)
isNat(x(V1, V2)) → and(isNat(V1), isNat(V2))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNat(N)), M, N)
x(N, 0) → U31(isNat(N))
x(N, s(M)) → U41(and(isNat(M), isNat(N)), M, N)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U21: {1}
s: {1}
plus: {1, 2}
U31: {1}
0: empty set
U41: {1}
x: {1, 2}
and: {1}
isNat: empty set

We applied the Zantema [34] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
U31(tt) → 0
U41(tt, M, N) → plus(x(a(N), a(M)), a(N))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
isNat(sInact(V1)) → isNat(a(V1))
isNat(xInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
x(N, 0) → U31(isNat(N))
x(N, s(M)) → U41(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
a(xInact(x1, x2)) → x(x1, x2)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

PLUS(N, s(M)) → AND(isNat(M), isNatInact(N))
X(N, s(M)) → AND(isNat(M), isNatInact(N))
ISNAT(plusInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
A(plusInact(x1, x2)) → PLUS(x1, x2)
X(N, 0) → U311(isNat(N))
U411(tt, M, N) → PLUS(x(a(N), a(M)), a(N))
ISNAT(plusInact(V1, V2)) → A(V1)
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → ISNAT(M)
ISNAT(xInact(V1, V2)) → A(V1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
ISNAT(xInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
U411(tt, M, N) → X(a(N), a(M))
U111(tt, N) → A(N)
PLUS(N, 0) → U111(isNat(N), N)
AND(tt, X) → A(X)
U311(tt) → 01
ISNAT(xInact(V1, V2)) → A(V2)
A(0Inact) → 01
A(isNatInact(x1)) → ISNAT(x1)
ISNAT(plusInact(V1, V2)) → A(V2)
A(xInact(x1, x2)) → X(x1, x2)
A(sInact(x1)) → S(x1)
ISNAT(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U211(and(isNat(M), isNatInact(N)), M, N)
X(N, s(M)) → ISNAT(M)
U211(tt, M, N) → S(plus(a(N), a(M)))
U411(tt, M, N) → A(M)
X(N, 0) → ISNAT(N)
U211(tt, M, N) → PLUS(a(N), a(M))
ISNAT(xInact(V1, V2)) → ISNAT(a(V1))
U211(tt, M, N) → A(N)
U411(tt, M, N) → A(N)
U211(tt, M, N) → A(M)
X(N, s(M)) → U411(and(isNat(M), isNatInact(N)), M, N)

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
U31(tt) → 0
U41(tt, M, N) → plus(x(a(N), a(M)), a(N))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
isNat(sInact(V1)) → isNat(a(V1))
isNat(xInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
x(N, 0) → U31(isNat(N))
x(N, s(M)) → U41(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
a(xInact(x1, x2)) → x(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

PLUS(N, s(M)) → AND(isNat(M), isNatInact(N))
X(N, s(M)) → AND(isNat(M), isNatInact(N))
ISNAT(plusInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
A(plusInact(x1, x2)) → PLUS(x1, x2)
X(N, 0) → U311(isNat(N))
U411(tt, M, N) → PLUS(x(a(N), a(M)), a(N))
ISNAT(plusInact(V1, V2)) → A(V1)
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → ISNAT(M)
ISNAT(xInact(V1, V2)) → A(V1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
ISNAT(xInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
U411(tt, M, N) → X(a(N), a(M))
U111(tt, N) → A(N)
PLUS(N, 0) → U111(isNat(N), N)
AND(tt, X) → A(X)
U311(tt) → 01
ISNAT(xInact(V1, V2)) → A(V2)
A(0Inact) → 01
A(isNatInact(x1)) → ISNAT(x1)
ISNAT(plusInact(V1, V2)) → A(V2)
A(xInact(x1, x2)) → X(x1, x2)
A(sInact(x1)) → S(x1)
ISNAT(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U211(and(isNat(M), isNatInact(N)), M, N)
X(N, s(M)) → ISNAT(M)
U211(tt, M, N) → S(plus(a(N), a(M)))
U411(tt, M, N) → A(M)
X(N, 0) → ISNAT(N)
U211(tt, M, N) → PLUS(a(N), a(M))
ISNAT(xInact(V1, V2)) → ISNAT(a(V1))
U211(tt, M, N) → A(N)
U411(tt, M, N) → A(N)
U211(tt, M, N) → A(M)
X(N, s(M)) → U411(and(isNat(M), isNatInact(N)), M, N)

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
U31(tt) → 0
U41(tt, M, N) → plus(x(a(N), a(M)), a(N))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
isNat(sInact(V1)) → isNat(a(V1))
isNat(xInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
x(N, 0) → U31(isNat(N))
x(N, s(M)) → U41(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
a(xInact(x1, x2)) → x(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 5 less nodes.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

PLUS(N, s(M)) → AND(isNat(M), isNatInact(N))
X(N, s(M)) → AND(isNat(M), isNatInact(N))
ISNAT(plusInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
ISNAT(plusInact(V1, V2)) → A(V1)
A(plusInact(x1, x2)) → PLUS(x1, x2)
U411(tt, M, N) → PLUS(x(a(N), a(M)), a(N))
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → ISNAT(M)
ISNAT(xInact(V1, V2)) → A(V1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
ISNAT(xInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
U411(tt, M, N) → X(a(N), a(M))
U111(tt, N) → A(N)
PLUS(N, 0) → U111(isNat(N), N)
AND(tt, X) → A(X)
ISNAT(xInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → A(V2)
A(isNatInact(x1)) → ISNAT(x1)
ISNAT(sInact(V1)) → A(V1)
A(xInact(x1, x2)) → X(x1, x2)
PLUS(N, s(M)) → U211(and(isNat(M), isNatInact(N)), M, N)
X(N, s(M)) → ISNAT(M)
U411(tt, M, N) → A(M)
X(N, 0) → ISNAT(N)
U211(tt, M, N) → PLUS(a(N), a(M))
ISNAT(xInact(V1, V2)) → ISNAT(a(V1))
U211(tt, M, N) → A(N)
U411(tt, M, N) → A(N)
U211(tt, M, N) → A(M)
X(N, s(M)) → U411(and(isNat(M), isNatInact(N)), M, N)

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
U31(tt) → 0
U41(tt, M, N) → plus(x(a(N), a(M)), a(N))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
isNat(sInact(V1)) → isNat(a(V1))
isNat(xInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
x(N, 0) → U31(isNat(N))
x(N, s(M)) → U41(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
a(xInact(x1, x2)) → x(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


PLUS(N, s(M)) → AND(isNat(M), isNatInact(N))
X(N, s(M)) → AND(isNat(M), isNatInact(N))
ISNAT(plusInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
ISNAT(plusInact(V1, V2)) → A(V1)
A(plusInact(x1, x2)) → PLUS(x1, x2)
U411(tt, M, N) → PLUS(x(a(N), a(M)), a(N))
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → ISNAT(M)
ISNAT(xInact(V1, V2)) → A(V1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
ISNAT(xInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
U411(tt, M, N) → X(a(N), a(M))
PLUS(N, 0) → U111(isNat(N), N)
AND(tt, X) → A(X)
ISNAT(xInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → A(V2)
A(isNatInact(x1)) → ISNAT(x1)
ISNAT(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U211(and(isNat(M), isNatInact(N)), M, N)
X(N, s(M)) → ISNAT(M)
U411(tt, M, N) → A(M)
X(N, 0) → ISNAT(N)
ISNAT(xInact(V1, V2)) → ISNAT(a(V1))
U211(tt, M, N) → A(N)
U411(tt, M, N) → A(N)
U211(tt, M, N) → A(M)
X(N, s(M)) → U411(and(isNat(M), isNatInact(N)), M, N)
The remaining pairs can at least be oriented weakly.

U111(tt, N) → A(N)
A(xInact(x1, x2)) → X(x1, x2)
U211(tt, M, N) → PLUS(a(N), a(M))
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  PLUS(x1, x2)
s(x1)  =  s(x1)
AND(x1, x2)  =  AND(x2)
isNat(x1)  =  isNat(x1)
isNatInact(x1)  =  isNatInact(x1)
X(x1, x2)  =  X(x1, x2)
ISNAT(x1)  =  x1
plusInact(x1, x2)  =  plusInact(x1, x2)
a(x1)  =  x1
A(x1)  =  x1
U411(x1, x2, x3)  =  U411(x1, x2, x3)
tt  =  tt
x(x1, x2)  =  x(x1, x2)
sInact(x1)  =  sInact(x1)
0  =  0
xInact(x1, x2)  =  xInact(x1, x2)
U111(x1, x2)  =  x2
U211(x1, x2, x3)  =  U211(x2, x3)
and(x1, x2)  =  and(x1, x2)
0Inact  =  0Inact
U31(x1)  =  U31(x1)
plus(x1, x2)  =  plus(x1, x2)
U21(x1, x2, x3)  =  U21(x1, x2, x3)
U11(x1, x2)  =  x2
U41(x1, x2, x3)  =  U41(x1, x2, x3)

Recursive path order with status [2].
Quasi-Precedence:
[X2, U41^13, x2, xInact2, U413] > [plusInact2, plus2, U213] > [PLUS2, U21^12] > [s1, isNat1, isNatInact1, sInact1] > [tt, 0, 0Inact] > AND1
[X2, U41^13, x2, xInact2, U413] > [plusInact2, plus2, U213] > and2 > AND1
[X2, U41^13, x2, xInact2, U413] > U311 > [tt, 0, 0Inact] > AND1

Status:
xInact2: [2,1]
U213: [3,2,1]
U311: [1]
U41^13: [2,3,1]
0: multiset
0Inact: multiset
U413: [2,3,1]
PLUS2: multiset
x2: [2,1]
tt: multiset
isNat1: multiset
AND1: multiset
and2: multiset
plus2: [1,2]
X2: [2,1]
s1: multiset
sInact1: multiset
isNatInact1: multiset
U21^12: multiset
plusInact2: [1,2]


The following usable rules [17] were oriented:

0 → 0Inact
isNat(0Inact) → tt
a(x) → x
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
x(N, 0) → U31(isNat(N))
a(sInact(x1)) → s(x1)
isNat(x1) → isNatInact(x1)
plus(x1, x2) → plusInact(x1, x2)
U21(tt, M, N) → s(plus(a(N), a(M)))
U31(tt) → 0
s(x1) → sInact(x1)
a(isNatInact(x1)) → isNat(x1)
and(tt, X) → a(X)
plus(N, 0) → U11(isNat(N), N)
a(xInact(x1, x2)) → x(x1, x2)
isNat(sInact(V1)) → isNat(a(V1))
x(N, s(M)) → U41(and(isNat(M), isNatInact(N)), M, N)
U11(tt, N) → a(N)
isNat(xInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
U41(tt, M, N) → plus(x(a(N), a(M)), a(N))
a(plusInact(x1, x2)) → plus(x1, x2)
isNat(plusInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof
                ↳ QDP
                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U211(tt, M, N) → PLUS(a(N), a(M))
A(xInact(x1, x2)) → X(x1, x2)
U111(tt, N) → A(N)

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
U31(tt) → 0
U41(tt, M, N) → plus(x(a(N), a(M)), a(N))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
isNat(sInact(V1)) → isNat(a(V1))
isNat(xInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
x(N, 0) → U31(isNat(N))
x(N, s(M)) → U41(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
a(xInact(x1, x2)) → x(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 3 less nodes.