Termination proof of /tmp/tmp7QS1rS/MYNAT

Termination of the following Term Rewriting System could be proven:

Context-sensitive 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

  ↳ CSDependencyPairsProof

Context-sensitive 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

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 {s, plus, U31, x, PLUS, X, U31¹} are replacing on all positions.
For all symbols f in {U11, U21, U41, and, U21¹, U41¹, AND, U11¹} we have µ(f) = {1}.
The symbols in {isNat, ISNAT, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

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

The collapsing dependency pairs are DP_c:

U11¹(tt, N) → N
U21¹(tt, M, N) → N
U21¹(tt, M, N) → M
U41¹(tt, M, N) → N
U41¹(tt, M, N) → M
AND(tt, X) → X

The hidden terms of R are:

isNat(V2)

Every hiding context is built from:none

Hence, the new unhiding pairs DP_u are :

U11¹(tt, N) → U(N)
U21¹(tt, M, N) → U(N)
U21¹(tt, M, N) → U(M)
U41¹(tt, M, N) → U(N)
U41¹(tt, M, N) → U(M)
AND(tt, X) → U(X)
U(isNat(V2)) → ISNAT(V2)

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)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 3 SCCs with 14 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

          ↳ QCSDP

          ↳ QCSDP

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

The TRS P consists of the following rules:

AND(tt, X) → U(X)
U(isNat(V2)) → ISNAT(V2)
ISNAT(plus(V1, V2)) → AND(isNat(V1), isNat(V2))
ISNAT(plus(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNAT(x(V1, V2)) → AND(isNat(V1), isNat(V2))
ISNAT(x(V1, V2)) → ISNAT(V1)

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)

Q is empty.

Using the order
Recursive path order with status [2].
Quasi-Precedence:

[x₂, U41₃] > [plus₂, U21₃] > [isNat₁, and₂] > tt > [AND₂, U₁] > s₁
[x₂, U41₃] > [plus₂, U21₃] > [isNat₁, and₂] > tt > 0 > s₁
[x₂, U41₃] > [plus₂, U21₃] > [isNat₁, and₂] > ISNAT₁ > [AND₂, U₁] > s₁
[x₂, U41₃] > [plus₂, U21₃] > U11₂ > s₁
[x₂, U41₃] > U31₁ > 0 > s₁

Status:

plus₂: [2,1]
U41₃: [2,3,1]
x₂: [2,1]
U11₂: multiset
and₂: [2,1]
0: multiset
ISNAT₁: multiset
tt: multiset
U31₁: multiset
U₁: multiset
AND₂: multiset
s₁: multiset
isNat₁: multiset
U21₃: [2,3,1]

the following usable rules

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)
U11(tt, N) → N
U21(tt, M, N) → s(plus(N, M))
and(tt, X) → X
x(N, 0) → U31(isNat(N))
x(N, s(M)) → U41(and(isNat(M), isNat(N)), M, N)
U31(tt) → 0
U41(tt, M, N) → plus(x(N, M), N)

could all be oriented weakly.
Furthermore, the pairs

AND(tt, X) → U(X)
U(isNat(V2)) → ISNAT(V2)
ISNAT(plus(V1, V2)) → AND(isNat(V1), isNat(V2))
ISNAT(plus(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNAT(x(V1, V2)) → AND(isNat(V1), isNat(V2))
ISNAT(x(V1, V2)) → ISNAT(V1)

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

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ PIsEmptyProof

          ↳ QCSDP

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, plus, U31, x} are replacing on all positions.
For all symbols f in {U11, U21, U41, and} we have µ(f) = {1}.
The symbols in {isNat} 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, 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)

Q is empty.

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

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, plus, U31, x, PLUS} are replacing on all positions.
For all symbols f in {U11, U21, U41, and, U21¹} we have µ(f) = {1}.
The symbols in {isNat} are not replacing on any position.

The TRS P consists of the following rules:

PLUS(N, s(M)) → U21¹(and(isNat(M), isNat(N)), M, N)
U21¹(tt, M, N) → PLUS(N, M)

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)

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

PLUS(N, s(M)) → U21¹(and(isNat(M), isNat(N)), M, N)

The remaining pairs can at least be oriented weakly.

U21¹(tt, M, N) → PLUS(N, M)

Used ordering: Combined order from the following AFS and order.
U21¹(x1, x2, x3) = x2
PLUS(x1, x2) = x2

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

          ↳ QCSDP

U21¹(tt, M, N) → PLUS(N, M)

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)

Q is empty.

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

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, plus, U31, x, X} are replacing on all positions.
For all symbols f in {U11, U21, U41, and, U41¹} we have µ(f) = {1}.
The symbols in {isNat} are not replacing on any position.

The TRS P consists of the following rules:

U41¹(tt, M, N) → X(N, M)
X(N, s(M)) → U41¹(and(isNat(M), isNat(N)), M, N)

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)

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

X(N, s(M)) → U41¹(and(isNat(M), isNat(N)), M, N)

The remaining pairs can at least be oriented weakly.

U41¹(tt, M, N) → X(N, M)

Used ordering: Combined order from the following AFS and order.
X(x1, x2) = x2
U41¹(x1, x2, x3) = x2

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

U41¹(tt, M, N) → X(N, M)

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)

Q is empty.

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