Termination proof of ../tpdb/TRS/CSR_Maude/peanoSimple/MYNAT

YES Termination proof of ../tpdb/TRS/CSR_Maude/peanoSimple/MYNAT_complete.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, 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, N) → N
U41(tt, M, N) → s(plus(N, M))
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)
isNatKind(0) → tt
isNatKind(plus(V1, V2)) → and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) → isNatKind(V1)
plus(N, 0) → U31(and(isNat(N), isNatKind(N)), N)
plus(N, s(M)) → U41(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}
U41: {1}
s: {1}
plus: {1, 2}
and: {1}
0: empty set
isNatKind: empty set

↳ CSR

  ↳ Zantema-Transformation

Q restricted 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, N) → N
U41(tt, M, N) → s(plus(N, M))
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)
isNatKind(0) → tt
isNatKind(plus(V1, V2)) → and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) → isNatKind(V1)
plus(N, 0) → U31(and(isNat(N), isNatKind(N)), N)
plus(N, s(M)) → U41(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}
U41: {1}
s: {1}
plus: {1, 2}
and: {1}
0: empty set
isNatKind: 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, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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:

ISNATKIND(sInact(V1)) → A(V1)
A(isNatKindInact(x1)) → ISNATKIND(x1)
PLUS(N, s(M)) → U41¹(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
U41¹(tt, M, N) → S(plus(a(N), a(M)))
U11¹(tt, V1, V2) → ISNAT(a(V1))
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → AND(isNat(M), isNatKindInact(M))
ISNATKIND(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
U11¹(tt, V1, V2) → U12¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
U12¹(tt, V2) → A(V2)
A(andInact(x1, x2)) → AND(x1, x2)
U21¹(tt, V1) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
U21¹(tt, V1) → U22¹(isNat(a(V1)))
AND(tt, X) → A(X)
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
A(0Inact) → 0¹
U31¹(tt, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
A(sInact(x1)) → S(x1)
U21¹(tt, V1) → A(V1)
U11¹(tt, V1, V2) → A(V1)
ISNAT(sInact(V1)) → A(V1)
U12¹(tt, V2) → ISNAT(a(V2))
PLUS(N, 0) → AND(isNat(N), isNatKindInact(N))
U41¹(tt, M, N) → A(M)
U41¹(tt, M, N) → PLUS(a(N), a(M))
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
PLUS(N, s(M)) → AND(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N)))
ISNATKIND(plusInact(V1, V2)) → A(V2)
PLUS(N, 0) → U31¹(and(isNat(N), isNatKindInact(N)), N)
U12¹(tt, V2) → U13¹(isNat(a(V2)))
U11¹(tt, V1, V2) → A(V2)
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
ISNATKIND(plusInact(V1, V2)) → A(V1)
PLUS(N, s(M)) → ISNAT(N)
U41¹(tt, M, N) → A(N)
ISNAT(plusInact(V1, V2)) → U11¹(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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:

ISNATKIND(sInact(V1)) → A(V1)
A(isNatKindInact(x1)) → ISNATKIND(x1)
PLUS(N, s(M)) → U41¹(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
U41¹(tt, M, N) → S(plus(a(N), a(M)))
U11¹(tt, V1, V2) → ISNAT(a(V1))
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → AND(isNat(M), isNatKindInact(M))
ISNATKIND(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
U11¹(tt, V1, V2) → U12¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
U12¹(tt, V2) → A(V2)
A(andInact(x1, x2)) → AND(x1, x2)
U21¹(tt, V1) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
U21¹(tt, V1) → U22¹(isNat(a(V1)))
AND(tt, X) → A(X)
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
A(0Inact) → 0¹
U31¹(tt, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
A(sInact(x1)) → S(x1)
U21¹(tt, V1) → A(V1)
U11¹(tt, V1, V2) → A(V1)
ISNAT(sInact(V1)) → A(V1)
U12¹(tt, V2) → ISNAT(a(V2))
PLUS(N, 0) → AND(isNat(N), isNatKindInact(N))
U41¹(tt, M, N) → A(M)
U41¹(tt, M, N) → PLUS(a(N), a(M))
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
PLUS(N, s(M)) → AND(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N)))
ISNATKIND(plusInact(V1, V2)) → A(V2)
PLUS(N, 0) → U31¹(and(isNat(N), isNatKindInact(N)), N)
U12¹(tt, V2) → U13¹(isNat(a(V2)))
U11¹(tt, V1, V2) → A(V2)
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
ISNATKIND(plusInact(V1, V2)) → A(V1)
PLUS(N, s(M)) → ISNAT(N)
U41¹(tt, M, N) → A(N)
ISNAT(plusInact(V1, V2)) → U11¹(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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:

ISNATKIND(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U41¹(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
A(isNatKindInact(x1)) → ISNATKIND(x1)
U11¹(tt, V1, V2) → ISNAT(a(V1))
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → AND(isNat(M), isNatKindInact(M))
ISNATKIND(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
U11¹(tt, V1, V2) → U12¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
U12¹(tt, V2) → A(V2)
A(andInact(x1, x2)) → AND(x1, x2)
U21¹(tt, V1) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
AND(tt, X) → A(X)
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
U31¹(tt, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
U11¹(tt, V1, V2) → A(V1)
U21¹(tt, V1) → A(V1)
ISNAT(sInact(V1)) → A(V1)
U12¹(tt, V2) → ISNAT(a(V2))
PLUS(N, 0) → AND(isNat(N), isNatKindInact(N))
U41¹(tt, M, N) → A(M)
U41¹(tt, M, N) → PLUS(a(N), a(M))
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
PLUS(N, s(M)) → AND(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N)))
ISNATKIND(plusInact(V1, V2)) → A(V2)
PLUS(N, 0) → U31¹(and(isNat(N), isNatKindInact(N)), N)
U11¹(tt, V1, V2) → A(V2)
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
ISNATKIND(plusInact(V1, V2)) → A(V1)
PLUS(N, s(M)) → ISNAT(N)
U41¹(tt, M, N) → A(N)
ISNAT(plusInact(V1, V2)) → U11¹(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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.

PLUS(N, 0) → ISNAT(N)
PLUS(N, 0) → AND(isNat(N), isNatKindInact(N))
PLUS(N, 0) → U31¹(and(isNat(N), isNatKindInact(N)), N)

The remaining pairs can at least be oriented weakly.

ISNATKIND(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U41¹(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
A(isNatKindInact(x1)) → ISNATKIND(x1)
U11¹(tt, V1, V2) → ISNAT(a(V1))
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
PLUS(N, s(M)) → AND(isNat(M), isNatKindInact(M))
ISNATKIND(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
U11¹(tt, V1, V2) → U12¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
U12¹(tt, V2) → A(V2)
A(andInact(x1, x2)) → AND(x1, x2)
U21¹(tt, V1) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
AND(tt, X) → A(X)
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
U31¹(tt, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
U11¹(tt, V1, V2) → A(V1)
U21¹(tt, V1) → A(V1)
ISNAT(sInact(V1)) → A(V1)
U12¹(tt, V2) → ISNAT(a(V2))
U41¹(tt, M, N) → A(M)
U41¹(tt, M, N) → PLUS(a(N), a(M))
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
PLUS(N, s(M)) → AND(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N)))
ISNATKIND(plusInact(V1, V2)) → A(V2)
U11¹(tt, V1, V2) → A(V2)
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
ISNATKIND(plusInact(V1, V2)) → A(V1)
PLUS(N, s(M)) → ISNAT(N)
U41¹(tt, M, N) → A(N)
ISNAT(plusInact(V1, V2)) → U11¹(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(0Inact) = 1
POL(A(x₁)) = x₁
POL(AND(x₁, x₂)) = x₂
POL(ISNAT(x₁)) = x₁
POL(ISNATKIND(x₁)) = x₁
POL(PLUS(x₁, x₂)) = x₁ + x₂
POL(U11(x₁, x₂, x₃)) = 0
POL(U11¹(x₁, x₂, x₃)) = x₂ + x₃
POL(U12(x₁, x₂)) = 0
POL(U12¹(x₁, x₂)) = x₂
POL(U13(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U21¹(x₁, x₂)) = x₂
POL(U22(x₁)) = 0
POL(U31(x₁, x₂)) = 1 + x₂
POL(U31¹(x₁, x₂)) = x₂
POL(U41(x₁, x₂, x₃)) = x₂ + x₃
POL(U41¹(x₁, x₂, x₃)) = x₂ + x₃
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₂
POL(andInact(x₁, x₂)) = x₂
POL(isNat(x₁)) = 0
POL(isNatKind(x₁)) = x₁
POL(isNatKindInact(x₁)) = x₁
POL(plus(x₁, x₂)) = x₁ + x₂
POL(plusInact(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = x₁
POL(sInact(x₁)) = x₁
POL(tt) = 0

The following usable rules [17] were oriented:

isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
U13(tt) → tt
and(x1, x2) → andInact(x1, x2)
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
U12(tt, V2) → U13(isNat(a(V2)))
isNatKind(0Inact) → tt
U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
plus(x1, x2) → plusInact(x1, x2)
U21(tt, V1) → U22(isNat(a(V1)))
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(0Inact) → 0
s(x1) → sInact(x1)
U41(tt, M, N) → s(plus(a(N), a(M)))
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
and(tt, X) → a(X)
isNatKind(sInact(V1)) → isNatKind(a(V1))
a(andInact(x1, x2)) → and(x1, x2)
U31(tt, N) → a(N)
a(isNatKindInact(x1)) → isNatKind(x1)
a(plusInact(x1, x2)) → plus(x1, x2)
a(sInact(x1)) → s(x1)
isNatKind(x1) → isNatKindInact(x1)
U22(tt) → tt
0 → 0Inact
a(x) → x

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

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

ISNATKIND(sInact(V1)) → A(V1)
A(isNatKindInact(x1)) → ISNATKIND(x1)
PLUS(N, s(M)) → U41¹(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
U11¹(tt, V1, V2) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → A(V1)
A(plusInact(x1, x2)) → PLUS(x1, x2)
PLUS(N, s(M)) → AND(isNat(M), isNatKindInact(M))
ISNATKIND(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
U11¹(tt, V1, V2) → U12¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
U12¹(tt, V2) → A(V2)
A(andInact(x1, x2)) → AND(x1, x2)
U21¹(tt, V1) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
AND(tt, X) → A(X)
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
U31¹(tt, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
U11¹(tt, V1, V2) → A(V1)
U21¹(tt, V1) → A(V1)
ISNAT(sInact(V1)) → A(V1)
U12¹(tt, V2) → ISNAT(a(V2))
U41¹(tt, M, N) → A(M)
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
U41¹(tt, M, N) → PLUS(a(N), a(M))
PLUS(N, s(M)) → AND(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N)))
ISNATKIND(plusInact(V1, V2)) → A(V2)
U11¹(tt, V1, V2) → A(V2)
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
ISNATKIND(plusInact(V1, V2)) → A(V1)
PLUS(N, s(M)) → ISNAT(N)
U41¹(tt, M, N) → A(N)
ISNAT(plusInact(V1, V2)) → U11¹(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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 1 less node.

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

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

ISNATKIND(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U41¹(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
A(isNatKindInact(x1)) → ISNATKIND(x1)
U11¹(tt, V1, V2) → ISNAT(a(V1))
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
PLUS(N, s(M)) → AND(isNat(M), isNatKindInact(M))
ISNATKIND(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
U11¹(tt, V1, V2) → U12¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
U12¹(tt, V2) → A(V2)
A(andInact(x1, x2)) → AND(x1, x2)
U21¹(tt, V1) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
AND(tt, X) → A(X)
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
U11¹(tt, V1, V2) → A(V1)
U21¹(tt, V1) → A(V1)
ISNAT(sInact(V1)) → A(V1)
U12¹(tt, V2) → ISNAT(a(V2))
U41¹(tt, M, N) → A(M)
U41¹(tt, M, N) → PLUS(a(N), a(M))
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
PLUS(N, s(M)) → AND(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N)))
ISNATKIND(plusInact(V1, V2)) → A(V2)
U11¹(tt, V1, V2) → A(V2)
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
ISNATKIND(plusInact(V1, V2)) → A(V1)
PLUS(N, s(M)) → ISNAT(N)
U41¹(tt, M, N) → A(N)
ISNAT(plusInact(V1, V2)) → U11¹(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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.

U11¹(tt, V1, V2) → ISNAT(a(V1))
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
PLUS(N, s(M)) → AND(isNat(M), isNatKindInact(M))
ISNATKIND(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
U11¹(tt, V1, V2) → U12¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
U12¹(tt, V2) → A(V2)
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
ISNAT(plusInact(V1, V2)) → A(V2)
ISNAT(plusInact(V1, V2)) → AND(isNatKind(a(V1)), isNatKindInact(a(V2)))
U11¹(tt, V1, V2) → A(V1)
U21¹(tt, V1) → A(V1)
ISNAT(sInact(V1)) → A(V1)
U12¹(tt, V2) → ISNAT(a(V2))
U41¹(tt, M, N) → A(M)
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
PLUS(N, s(M)) → AND(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N)))
ISNATKIND(plusInact(V1, V2)) → A(V2)
U11¹(tt, V1, V2) → A(V2)
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
ISNATKIND(plusInact(V1, V2)) → A(V1)
PLUS(N, s(M)) → ISNAT(N)
U41¹(tt, M, N) → A(N)
ISNAT(plusInact(V1, V2)) → U11¹(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))

The remaining pairs can at least be oriented weakly.

ISNATKIND(sInact(V1)) → A(V1)
PLUS(N, s(M)) → U41¹(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
A(isNatKindInact(x1)) → ISNATKIND(x1)
A(andInact(x1, x2)) → AND(x1, x2)
U21¹(tt, V1) → ISNAT(a(V1))
AND(tt, X) → A(X)
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
U41¹(tt, M, N) → PLUS(a(N), a(M))

Used ordering: Combined order from the following AFS and order.
ISNATKIND(x1) = x1
sInact(x1) = x1
A(x1) = x1
PLUS(x1, x2) = PLUS(x1, x2)
s(x1) = x1
U41¹(x1, x2, x3) = U41¹(x2, x3)
and(x1, x2) = x2
isNat(x1) = x1
isNatKindInact(x1) = x1
andInact(x1, x2) = x2
U11¹(x1, x2, x3) = U11¹(x1, x2, x3)
tt = tt
ISNAT(x1) = ISNAT(x1)
a(x1) = x1
plusInact(x1, x2) = plusInact(x1, x2)
AND(x1, x2) = x2
isNatKind(x1) = x1
U12¹(x1, x2) = U12¹(x2)
U21¹(x1, x2) = U21¹(x2)
U11(x1, x2, x3) = x2
U13(x1) = U13
U21(x1, x2) = x1
U12(x1, x2) = x1
0Inact = 0Inact
plus(x1, x2) = plus(x1, x2)
U22(x1) = U22
U41(x1, x2, x3) = U41(x2, x3)
0 = 0
U31(x1, x2) = U31(x1, x2)

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

[tt, U13, 0Inact, U22, 0] > U31₂
[plusInact₂, plus₂, U41_2] > [U11^1₃, U12^1_1] > [PLUS₂, U41^1₂, ISNAT₁, U21^1_1]
[plusInact₂, plus₂, U41_2] > U31₂

Status:

U21^1₁: multiset
U41₂: multiset
U11^1₃: multiset
U41^1₂: multiset
0: multiset
0Inact: multiset
PLUS₂: multiset
ISNAT₁: multiset
tt: multiset
U13: multiset
U22: multiset
U31₂: multiset
plus₂: multiset
U12^1₁: multiset
plusInact₂: multiset

The following usable rules [17] were oriented:

isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
U13(tt) → tt
and(x1, x2) → andInact(x1, x2)
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
U12(tt, V2) → U13(isNat(a(V2)))
isNatKind(0Inact) → tt
U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
plus(x1, x2) → plusInact(x1, x2)
isNat(0Inact) → tt
U21(tt, V1) → U22(isNat(a(V1)))
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(0Inact) → 0
s(x1) → sInact(x1)
U41(tt, M, N) → s(plus(a(N), a(M)))
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
and(tt, X) → a(X)
isNatKind(sInact(V1)) → isNatKind(a(V1))
a(andInact(x1, x2)) → and(x1, x2)
U31(tt, N) → a(N)
a(isNatKindInact(x1)) → isNatKind(x1)
a(plusInact(x1, x2)) → plus(x1, x2)
a(sInact(x1)) → s(x1)
isNatKind(x1) → isNatKindInact(x1)
U22(tt) → tt
0 → 0Inact
a(x) → x

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

ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
ISNATKIND(sInact(V1)) → A(V1)
A(isNatKindInact(x1)) → ISNATKIND(x1)
PLUS(N, s(M)) → U41¹(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
A(andInact(x1, x2)) → AND(x1, x2)
U21¹(tt, V1) → ISNAT(a(V1))
U41¹(tt, M, N) → PLUS(a(N), a(M))
AND(tt, X) → A(X)

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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 3 SCCs.

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                              ↳ QDP

                              ↳ QDP

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

ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
U21¹(tt, V1) → ISNAT(a(V1))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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)) → U21¹(isNatKind(a(V1)), a(V1))

The remaining pairs can at least be oriented weakly.

U21¹(tt, V1) → ISNAT(a(V1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(ISNAT(x₁)) = x₁
POL(U11(x₁, x₂, x₃)) = x₃
POL(U12(x₁, x₂)) = x₂
POL(U13(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U21¹(x₁, x₂)) = x₂
POL(U22(x₁)) = 0
POL(U31(x₁, x₂)) = x₂
POL(U41(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₂
POL(andInact(x₁, x₂)) = x₂
POL(isNat(x₁)) = 1 + x₁
POL(isNatKind(x₁)) = 0
POL(isNatKindInact(x₁)) = 0
POL(plus(x₁, x₂)) = x₁ + x₂
POL(plusInact(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = 1 + x₁
POL(sInact(x₁)) = 1 + x₁
POL(tt) = 0

The following usable rules [17] were oriented:

a(0Inact) → 0
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
U13(tt) → tt
and(x1, x2) → andInact(x1, x2)
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
s(x1) → sInact(x1)
U41(tt, M, N) → s(plus(a(N), a(M)))
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
and(tt, X) → a(X)
isNatKind(sInact(V1)) → isNatKind(a(V1))
a(andInact(x1, x2)) → and(x1, x2)
U31(tt, N) → a(N)
a(isNatKindInact(x1)) → isNatKind(x1)
a(plusInact(x1, x2)) → plus(x1, x2)
U12(tt, V2) → U13(isNat(a(V2)))
a(sInact(x1)) → s(x1)
isNatKind(0Inact) → tt
isNatKind(x1) → isNatKindInact(x1)
U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U22(tt) → tt
plus(x1, x2) → plusInact(x1, x2)
0 → 0Inact
U21(tt, V1) → U22(isNat(a(V1)))
a(x) → x

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                              ↳ QDP

                              ↳ QDP

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

U21¹(tt, V1) → ISNAT(a(V1))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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.

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPOrderProof

                              ↳ QDP

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

PLUS(N, s(M)) → U41¹(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
U41¹(tt, M, N) → PLUS(a(N), a(M))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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.

PLUS(N, s(M)) → U41¹(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)

The remaining pairs can at least be oriented weakly.

U41¹(tt, M, N) → PLUS(a(N), a(M))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(PLUS(x₁, x₂)) = x₂
POL(U11(x₁, x₂, x₃)) = 1
POL(U12(x₁, x₂)) = 1
POL(U13(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U22(x₁)) = 0
POL(U31(x₁, x₂)) = x₂
POL(U41(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U41¹(x₁, x₂, x₃)) = x₂
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₂
POL(andInact(x₁, x₂)) = x₂
POL(isNat(x₁)) = 1
POL(isNatKind(x₁)) = 0
POL(isNatKindInact(x₁)) = 0
POL(plus(x₁, x₂)) = x₁ + x₂
POL(plusInact(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = 1 + x₁
POL(sInact(x₁)) = 1 + x₁
POL(tt) = 0

The following usable rules [17] were oriented:

a(0Inact) → 0
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
U13(tt) → tt
and(x1, x2) → andInact(x1, x2)
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
s(x1) → sInact(x1)
U41(tt, M, N) → s(plus(a(N), a(M)))
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
and(tt, X) → a(X)
isNatKind(sInact(V1)) → isNatKind(a(V1))
a(andInact(x1, x2)) → and(x1, x2)
U31(tt, N) → a(N)
a(isNatKindInact(x1)) → isNatKind(x1)
a(plusInact(x1, x2)) → plus(x1, x2)
U12(tt, V2) → U13(isNat(a(V2)))
a(sInact(x1)) → s(x1)
isNatKind(0Inact) → tt
isNatKind(x1) → isNatKindInact(x1)
U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U22(tt) → tt
plus(x1, x2) → plusInact(x1, x2)
0 → 0Inact
U21(tt, V1) → U22(isNat(a(V1)))
a(x) → x

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                              ↳ QDP

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

U41¹(tt, M, N) → PLUS(a(N), a(M))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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.

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPOrderProof

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

ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
ISNATKIND(sInact(V1)) → A(V1)
A(isNatKindInact(x1)) → ISNATKIND(x1)
A(andInact(x1, x2)) → AND(x1, x2)
AND(tt, X) → A(X)

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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.

ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
ISNATKIND(sInact(V1)) → A(V1)

The remaining pairs can at least be oriented weakly.

A(isNatKindInact(x1)) → ISNATKIND(x1)
A(andInact(x1, x2)) → AND(x1, x2)
AND(tt, X) → A(X)

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(0Inact) = 1
POL(A(x₁)) = x₁
POL(AND(x₁, x₂)) = x₂
POL(ISNATKIND(x₁)) = x₁
POL(U11(x₁, x₂, x₃)) = 0
POL(U12(x₁, x₂)) = 0
POL(U13(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U22(x₁)) = 0
POL(U31(x₁, x₂)) = x₂
POL(U41(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(a(x₁)) = x₁
POL(and(x₁, x₂)) = x₂
POL(andInact(x₁, x₂)) = x₂
POL(isNat(x₁)) = 0
POL(isNatKind(x₁)) = x₁
POL(isNatKindInact(x₁)) = x₁
POL(plus(x₁, x₂)) = x₁ + x₂
POL(plusInact(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = 1 + x₁
POL(sInact(x₁)) = 1 + x₁
POL(tt) = 0

The following usable rules [17] were oriented:

a(0Inact) → 0
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
U13(tt) → tt
and(x1, x2) → andInact(x1, x2)
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
s(x1) → sInact(x1)
U41(tt, M, N) → s(plus(a(N), a(M)))
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
and(tt, X) → a(X)
isNatKind(sInact(V1)) → isNatKind(a(V1))
a(andInact(x1, x2)) → and(x1, x2)
U31(tt, N) → a(N)
a(isNatKindInact(x1)) → isNatKind(x1)
a(plusInact(x1, x2)) → plus(x1, x2)
U12(tt, V2) → U13(isNat(a(V2)))
a(sInact(x1)) → s(x1)
isNatKind(0Inact) → tt
isNatKind(x1) → isNatKindInact(x1)
U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U22(tt) → tt
plus(x1, x2) → plusInact(x1, x2)
0 → 0Inact
U21(tt, V1) → U22(isNat(a(V1)))
a(x) → x

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ DependencyGraphProof

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

A(isNatKindInact(x1)) → ISNATKIND(x1)
A(andInact(x1, x2)) → AND(x1, x2)
AND(tt, X) → A(X)

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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 1 less node.

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ UsableRulesProof

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

A(andInact(x1, x2)) → AND(x1, x2)
AND(tt, X) → A(X)

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNat(a(V1)), a(V2))
U12(tt, V2) → U13(isNat(a(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(a(V1)))
U22(tt) → tt
U31(tt, N) → a(N)
U41(tt, M, N) → s(plus(a(N), a(M)))
and(tt, X) → a(X)
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(and(isNatKind(a(V1)), isNatKindInact(a(V2))), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → and(isNatKind(a(V1)), isNatKindInact(a(V2)))
isNatKind(sInact(V1)) → isNatKind(a(V1))
plus(N, 0) → U31(and(isNat(N), isNatKindInact(N)), N)
plus(N, s(M)) → U41(and(and(isNat(M), isNatKindInact(M)), andInact(isNat(N), isNatKindInact(N))), M, N)
a(x) → x
isNatKind(x1) → isNatKindInact(x1)
a(isNatKindInact(x1)) → isNatKind(x1)
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)
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 can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ UsableRulesProof

                                          ↳ QDP

                                            ↳ QDPSizeChangeProof

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

A(andInact(x1, x2)) → AND(x1, x2)
AND(tt, X) → A(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

AND(tt, X) → A(X)
The graph contains the following edges 2 >= 1
A(andInact(x1, x2)) → AND(x1, x2)
The graph contains the following edges 1 > 1, 1 > 2