YES Termination proof of ../tpdb/TRS/CSR_Maude/peanoSimple/MYNAT_nokinds-noand.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, V2) → U12(isNat(V2))
U12(tt) → tt
U21(tt) → tt
U31(tt, N) → N
U41(tt, M, N) → U42(isNat(N), M, N)
U42(tt, M, N) → s(plus(N, M))
isNat(0) → tt
isNat(plus(V1, V2)) → U11(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
plus(N, 0) → U31(isNat(N), N)
plus(N, s(M)) → U41(isNat(M), M, N)

The replacement map contains the following entries:

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


↳ CSR
  ↳ Zantema-Transformation

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

U11(tt, V2) → U12(isNat(V2))
U12(tt) → tt
U21(tt) → tt
U31(tt, N) → N
U41(tt, M, N) → U42(isNat(N), M, N)
U42(tt, M, N) → s(plus(N, M))
isNat(0) → tt
isNat(plus(V1, V2)) → U11(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
plus(N, 0) → U31(isNat(N), N)
plus(N, s(M)) → U41(isNat(M), M, N)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U12: {1}
isNat: empty set
U21: {1}
U31: {1}
U41: {1}
U42: {1}
s: {1}
plus: {1, 2}
0: 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, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → U42(isNat(a(N)), a(M), a(N))
U42(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
plus(N, 0) → U31(isNat(N), N)
plus(N, s(M)) → U41(isNat(M), M, N)
a(x) → x
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

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:

U111(tt, V2) → ISNAT(a(V2))
ISNAT(plusInact(V1, V2)) → A(V1)
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, 0) → ISNAT(N)
U411(tt, M, N) → ISNAT(a(N))
PLUS(N, s(M)) → ISNAT(M)
U421(tt, M, N) → PLUS(a(N), a(M))
U111(tt, V2) → U121(isNat(a(V2)))
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U421(tt, M, N) → A(M)
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))
U111(tt, V2) → A(V2)
PLUS(N, s(M)) → U411(isNat(M), M, N)
A(0Inact) → 01
U421(tt, M, N) → S(plus(a(N), a(M)))
U311(tt, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(sInact(V1)) → A(V1)
A(sInact(x1)) → S(x1)
ISNAT(sInact(V1)) → U211(isNat(a(V1)))
U411(tt, M, N) → A(M)
U421(tt, M, N) → A(N)
PLUS(N, 0) → U311(isNat(N), N)
U411(tt, M, N) → U421(isNat(a(N)), a(M), a(N))
U411(tt, M, N) → A(N)

The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → U42(isNat(a(N)), a(M), a(N))
U42(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
plus(N, 0) → U31(isNat(N), N)
plus(N, s(M)) → U41(isNat(M), M, N)
a(x) → x
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

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:

U111(tt, V2) → ISNAT(a(V2))
ISNAT(plusInact(V1, V2)) → A(V1)
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, 0) → ISNAT(N)
U411(tt, M, N) → ISNAT(a(N))
PLUS(N, s(M)) → ISNAT(M)
U421(tt, M, N) → PLUS(a(N), a(M))
U111(tt, V2) → U121(isNat(a(V2)))
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U421(tt, M, N) → A(M)
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))
U111(tt, V2) → A(V2)
PLUS(N, s(M)) → U411(isNat(M), M, N)
A(0Inact) → 01
U421(tt, M, N) → S(plus(a(N), a(M)))
U311(tt, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(sInact(V1)) → A(V1)
A(sInact(x1)) → S(x1)
ISNAT(sInact(V1)) → U211(isNat(a(V1)))
U411(tt, M, N) → A(M)
U421(tt, M, N) → A(N)
PLUS(N, 0) → U311(isNat(N), N)
U411(tt, M, N) → U421(isNat(a(N)), a(M), a(N))
U411(tt, M, N) → A(N)

The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → U42(isNat(a(N)), a(M), a(N))
U42(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
plus(N, 0) → U31(isNat(N), N)
plus(N, s(M)) → U41(isNat(M), M, N)
a(x) → x
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

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:

U311(tt, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V2)
U111(tt, V2) → ISNAT(a(V2))
ISNAT(sInact(V1)) → A(V1)
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
PLUS(N, 0) → ISNAT(N)
ISNAT(sInact(V1)) → ISNAT(a(V1))
U411(tt, M, N) → A(M)
U411(tt, M, N) → ISNAT(a(N))
PLUS(N, s(M)) → ISNAT(M)
U421(tt, M, N) → PLUS(a(N), a(M))
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U421(tt, M, N) → A(M)
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))
U421(tt, M, N) → A(N)
PLUS(N, 0) → U311(isNat(N), N)
U111(tt, V2) → A(V2)
U411(tt, M, N) → U421(isNat(a(N)), a(M), a(N))
U411(tt, M, N) → A(N)
PLUS(N, s(M)) → U411(isNat(M), M, N)

The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → U42(isNat(a(N)), a(M), a(N))
U42(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
plus(N, 0) → U31(isNat(N), N)
plus(N, s(M)) → U41(isNat(M), M, N)
a(x) → x
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

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.


ISNAT(sInact(V1)) → A(V1)
PLUS(N, 0) → ISNAT(N)
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, s(M)) → ISNAT(M)
PLUS(N, 0) → U311(isNat(N), N)
PLUS(N, s(M)) → U411(isNat(M), M, N)
The remaining pairs can at least be oriented weakly.

U311(tt, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V2)
U111(tt, V2) → ISNAT(a(V2))
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
U411(tt, M, N) → A(M)
U411(tt, M, N) → ISNAT(a(N))
U421(tt, M, N) → PLUS(a(N), a(M))
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U421(tt, M, N) → A(M)
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))
U421(tt, M, N) → A(N)
U111(tt, V2) → A(V2)
U411(tt, M, N) → U421(isNat(a(N)), a(M), a(N))
U411(tt, M, N) → A(N)
Used ordering: Polynomial interpretation [25]:

POL(0) = 1   
POL(0Inact) = 1   
POL(A(x1)) = x1   
POL(ISNAT(x1)) = x1   
POL(PLUS(x1, x2)) = x1 + x2   
POL(U11(x1, x2)) = 0   
POL(U111(x1, x2)) = x2   
POL(U12(x1)) = 0   
POL(U21(x1)) = 0   
POL(U31(x1, x2)) = 1 + x2   
POL(U311(x1, x2)) = x2   
POL(U41(x1, x2, x3)) = 1 + x2 + x3   
POL(U411(x1, x2, x3)) = x2 + x3   
POL(U42(x1, x2, x3)) = 1 + x2 + x3   
POL(U421(x1, x2, x3)) = x2 + x3   
POL(a(x1)) = x1   
POL(isNat(x1)) = 0   
POL(plus(x1, x2)) = x1 + x2   
POL(plusInact(x1, x2)) = x1 + x2   
POL(s(x1)) = 1 + x1   
POL(sInact(x1)) = 1 + x1   
POL(tt) = 0   

The following usable rules [17] were oriented:

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



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

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

U311(tt, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V2)
U111(tt, V2) → ISNAT(a(V2))
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
U411(tt, M, N) → A(M)
U411(tt, M, N) → ISNAT(a(N))
U421(tt, M, N) → PLUS(a(N), a(M))
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U421(tt, M, N) → A(M)
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))
U421(tt, M, N) → A(N)
U111(tt, V2) → A(V2)
U411(tt, M, N) → U421(isNat(a(N)), a(M), a(N))
U411(tt, M, N) → A(N)

The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → U42(isNat(a(N)), a(M), a(N))
U42(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
plus(N, 0) → U31(isNat(N), N)
plus(N, s(M)) → U41(isNat(M), M, N)
a(x) → x
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

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 12 less nodes.

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

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

ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U111(tt, V2) → ISNAT(a(V2))
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))

The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → U42(isNat(a(N)), a(M), a(N))
U42(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
plus(N, 0) → U31(isNat(N), N)
plus(N, s(M)) → U41(isNat(M), M, N)
a(x) → x
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

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.


ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))
The remaining pairs can at least be oriented weakly.

U111(tt, V2) → ISNAT(a(V2))
Used ordering: Polynomial interpretation [25]:

POL(0) = 1   
POL(0Inact) = 1   
POL(ISNAT(x1)) = 1 + x1   
POL(U11(x1, x2)) = 1 + x2   
POL(U111(x1, x2)) = 1 + x2   
POL(U12(x1)) = 0   
POL(U21(x1)) = 0   
POL(U31(x1, x2)) = 1 + x2   
POL(U41(x1, x2, x3)) = 1 + x3   
POL(U42(x1, x2, x3)) = 1 + x3   
POL(a(x1)) = x1   
POL(isNat(x1)) = 1 + x1   
POL(plus(x1, x2)) = 1 + x1 + x2   
POL(plusInact(x1, x2)) = 1 + x1 + x2   
POL(s(x1)) = 0   
POL(sInact(x1)) = 0   
POL(tt) = 0   

The following usable rules [17] were oriented:

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



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

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

U111(tt, V2) → ISNAT(a(V2))

The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → U42(isNat(a(N)), a(M), a(N))
U42(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
plus(N, 0) → U31(isNat(N), N)
plus(N, s(M)) → U41(isNat(M), M, N)
a(x) → x
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

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 1 less node.