YES Termination proof of ../tpdb/TRS/CSR_Maude/peanoSimple/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))
and(tt, X) → X
isNat(0) → tt
isNat(plus(V1, V2)) → and(isNat(V1), isNat(V2))
isNat(s(V1)) → isNat(V1)
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(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}
and: {1}
isNat: empty set
0: 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))
and(tt, X) → X
isNat(0) → tt
isNat(plus(V1, V2)) → and(isNat(V1), isNat(V2))
isNat(s(V1)) → isNat(V1)
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(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}
and: {1}
isNat: empty set
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, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
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))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(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))
A(0Inact) → 01
A(isNatInact(x1)) → ISNAT(x1)
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
A(sInact(x1)) → S(x1)
ISNAT(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U211(and(isNat(M), isNatInact(N)), M, N)
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
PLUS(N, 0) → ISNAT(N)
ISNAT(sInact(V1)) → ISNAT(a(V1))
U211(tt, M, N) → S(plus(a(N), a(M)))
PLUS(N, s(M)) → ISNAT(M)
U211(tt, M, N) → PLUS(a(N), a(M))
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U111(tt, N) → A(N)
U211(tt, M, N) → A(N)
PLUS(N, 0) → U111(isNat(N), N)
U211(tt, M, N) → A(M)
AND(tt, X) → A(X)

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
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))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(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))
A(0Inact) → 01
A(isNatInact(x1)) → ISNAT(x1)
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
A(sInact(x1)) → S(x1)
ISNAT(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U211(and(isNat(M), isNatInact(N)), M, N)
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
PLUS(N, 0) → ISNAT(N)
ISNAT(sInact(V1)) → ISNAT(a(V1))
U211(tt, M, N) → S(plus(a(N), a(M)))
PLUS(N, s(M)) → ISNAT(M)
U211(tt, M, N) → PLUS(a(N), a(M))
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U111(tt, N) → A(N)
U211(tt, M, N) → A(N)
PLUS(N, 0) → U111(isNat(N), N)
U211(tt, M, N) → A(M)
AND(tt, X) → A(X)

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
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))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(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 3 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))
A(isNatInact(x1)) → ISNAT(x1)
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
ISNAT(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U211(and(isNat(M), isNatInact(N)), M, N)
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
PLUS(N, 0) → ISNAT(N)
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, s(M)) → ISNAT(M)
U211(tt, M, N) → PLUS(a(N), a(M))
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U111(tt, N) → A(N)
U211(tt, M, N) → A(N)
PLUS(N, 0) → U111(isNat(N), N)
U211(tt, M, N) → A(M)
AND(tt, X) → A(X)

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
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))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(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))
ISNAT(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U211(and(isNat(M), isNatInact(N)), M, N)
PLUS(N, 0) → ISNAT(N)
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, s(M)) → ISNAT(M)
PLUS(N, 0) → U111(isNat(N), N)
AND(tt, X) → A(X)
The remaining pairs can at least be oriented weakly.

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

POL(0) = 1   
POL(0Inact) = 1   
POL(A(x1)) = 1 + x1   
POL(AND(x1, x2)) = 1 + x1 + x2   
POL(ISNAT(x1)) = 1 + x1   
POL(PLUS(x1, x2)) = 1 + x1 + x2   
POL(U11(x1, x2)) = 1 + x2   
POL(U111(x1, x2)) = 1 + x2   
POL(U21(x1, x2, x3)) = 1 + x2 + x3   
POL(U211(x1, x2, x3)) = 1 + x2 + x3   
POL(a(x1)) = x1   
POL(and(x1, x2)) = x2   
POL(isNat(x1)) = x1   
POL(isNatInact(x1)) = x1   
POL(plus(x1, x2)) = x1 + x2   
POL(plusInact(x1, x2)) = x1 + x2   
POL(s(x1)) = 1 + x1   
POL(sInact(x1)) = 1 + x1   
POL(tt) = 1   

The following usable rules [17] were oriented:

0 → 0Inact
isNat(x1) → isNatInact(x1)
U21(tt, M, N) → s(plus(a(N), a(M)))
a(0Inact) → 0
a(isNatInact(x1)) → isNat(x1)
and(tt, X) → a(X)
plus(N, 0) → U11(isNat(N), N)
U11(tt, N) → a(N)
isNat(sInact(V1)) → isNat(a(V1))
a(plusInact(x1, x2)) → plus(x1, x2)
isNat(plusInact(V1, V2)) → and(isNat(a(V1)), isNatInact(a(V2)))
plus(x1, x2) → plusInact(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
a(x) → x
isNat(0Inact) → tt
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))
ISNAT(plusInact(V1, V2)) → A(V2)
A(isNatInact(x1)) → ISNAT(x1)
ISNAT(plusInact(V1, V2)) → AND(isNat(a(V1)), isNatInact(a(V2)))
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → A(V1)
A(plusInact(x1, x2)) → PLUS(x1, x2)
U111(tt, N) → A(N)
U211(tt, M, N) → A(N)
U211(tt, M, N) → A(M)

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
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))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(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 6 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)) → A(V2)
A(isNatInact(x1)) → ISNAT(x1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → A(V1)

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
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))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(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.


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

A(isNatInact(x1)) → ISNAT(x1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
Used ordering: Polynomial interpretation [25]:

POL(0) = 1   
POL(0Inact) = 1   
POL(A(x1)) = x1   
POL(ISNAT(x1)) = 1 + x1   
POL(U11(x1, x2)) = x2   
POL(U21(x1, x2, x3)) = x2 + x3   
POL(a(x1)) = x1   
POL(and(x1, x2)) = x2   
POL(isNat(x1)) = 1 + x1   
POL(isNatInact(x1)) = 1 + x1   
POL(plus(x1, x2)) = x1 + x2   
POL(plusInact(x1, x2)) = x1 + x2   
POL(s(x1)) = x1   
POL(sInact(x1)) = x1   
POL(tt) = 0   

The following usable rules [17] were oriented:

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



↳ 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:

A(isNatInact(x1)) → ISNAT(x1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
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))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(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 1 less node.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof
                ↳ 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))

The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
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))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(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.


ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(0Inact) = 0   
POL(ISNAT(x1)) = x1   
POL(U11(x1, x2)) = 1 + x2   
POL(U21(x1, x2, x3)) = x3   
POL(a(x1)) = x1   
POL(and(x1, x2)) = x2   
POL(isNat(x1)) = 0   
POL(isNatInact(x1)) = 0   
POL(plus(x1, x2)) = 1 + x1   
POL(plusInact(x1, x2)) = 1 + x1   
POL(s(x1)) = 0   
POL(sInact(x1)) = 0   
POL(tt) = 0   

The following usable rules [17] were oriented:

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



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

Q DP problem:
P is empty.
The TRS R consists of the following rules:

U11(tt, N) → a(N)
U21(tt, M, N) → s(plus(a(N), a(M)))
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))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), isNatInact(N)), M, N)
a(x) → x
isNat(x1) → isNatInact(x1)
a(isNatInact(x1)) → isNat(x1)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.