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

YES Termination proof of ../tpdb/TRS/CSR_Maude/peanoSimple/MYNAT_complete-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, V1, V2) → U12(isNatKind(V1), V1, V2)
U12(tt, V1, V2) → U13(isNatKind(V2), V1, V2)
U13(tt, V1, V2) → U14(isNatKind(V2), V1, V2)
U14(tt, V1, V2) → U15(isNat(V1), V2)
U15(tt, V2) → U16(isNat(V2))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(V2))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(N), N)
U52(tt, N) → N
U61(tt, M, N) → U62(isNatKind(M), M, N)
U62(tt, M, N) → U63(isNat(N), M, N)
U63(tt, M, N) → U64(isNatKind(N), M, N)
U64(tt, M, N) → s(plus(N, M))
isNat(0) → tt
isNat(plus(V1, V2)) → U11(isNatKind(V1), V1, V2)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatKind(0) → tt
isNatKind(plus(V1, V2)) → U31(isNatKind(V1), V2)
isNatKind(s(V1)) → U41(isNatKind(V1))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U12: {1}
isNatKind: empty set
U13: {1}
U14: {1}
U15: {1}
isNat: empty set
U16: {1}
U21: {1}
U22: {1}
U23: {1}
U31: {1}
U32: {1}
U41: {1}
U51: {1}
U52: {1}
U61: {1}
U62: {1}
U63: {1}
U64: {1}
s: {1}
plus: {1, 2}
0: empty set

↳ CSR

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

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

U11(tt, V1, V2) → U12(isNatKind(V1), V1, V2)
U12(tt, V1, V2) → U13(isNatKind(V2), V1, V2)
U13(tt, V1, V2) → U14(isNatKind(V2), V1, V2)
U14(tt, V1, V2) → U15(isNat(V1), V2)
U15(tt, V2) → U16(isNat(V2))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(V2))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(N), N)
U52(tt, N) → N
U61(tt, M, N) → U62(isNatKind(M), M, N)
U62(tt, M, N) → U63(isNat(N), M, N)
U63(tt, M, N) → U64(isNatKind(N), M, N)
U64(tt, M, N) → s(plus(N, M))
isNat(0) → tt
isNat(plus(V1, V2)) → U11(isNatKind(V1), V1, V2)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatKind(0) → tt
isNatKind(plus(V1, V2)) → U31(isNatKind(V1), V2)
isNatKind(s(V1)) → U41(isNatKind(V1))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)

The replacement map contains the following entries:

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U22(tt, V1) → U23(isNat(a(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(a(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U64(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

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:

U12¹(tt, V1, V2) → ISNATKIND(a(V2))
U62¹(tt, M, N) → A(N)
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
U62¹(tt, M, N) → A(M)
PLUS(N, 0) → ISNAT(N)
U14¹(tt, V1, V2) → A(V2)
U14¹(tt, V1, V2) → U15¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
ISNAT(plusInact(V1, V2)) → U11¹(isNatKind(a(V1)), a(V1), a(V2))
U31¹(tt, V2) → ISNATKIND(a(V2))
U62¹(tt, M, N) → U63¹(isNat(a(N)), a(M), a(N))
U51¹(tt, N) → ISNATKIND(a(N))
U11¹(tt, V1, V2) → ISNATKIND(a(V1))
U31¹(tt, V2) → A(V2)
U61¹(tt, M, N) → A(N)
U13¹(tt, V1, V2) → ISNATKIND(a(V2))
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
U15¹(tt, V2) → A(V2)
U22¹(tt, V1) → ISNAT(a(V1))
U13¹(tt, V1, V2) → A(V2)
A(sInact(x1)) → S(x1)
ISNAT(sInact(V1)) → A(V1)
U21¹(tt, V1) → A(V1)
U11¹(tt, V1, V2) → A(V1)
U63¹(tt, M, N) → A(N)
ISNATKIND(plusInact(V1, V2)) → U31¹(isNatKind(a(V1)), a(V2))
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
U11¹(tt, V1, V2) → U12¹(isNatKind(a(V1)), a(V1), a(V2))
U61¹(tt, M, N) → U62¹(isNatKind(a(M)), a(M), a(N))
U52¹(tt, N) → A(N)
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
U64¹(tt, M, N) → PLUS(a(N), a(M))
PLUS(N, s(M)) → U61¹(isNat(M), M, N)
ISNATKIND(plusInact(V1, V2)) → A(V1)
U14¹(tt, V1, V2) → A(V1)
ISNATKIND(sInact(V1)) → A(V1)
U12¹(tt, V1, V2) → A(V1)
U51¹(tt, N) → U52¹(isNatKind(a(N)), a(N))
U61¹(tt, M, N) → ISNATKIND(a(M))
U51¹(tt, N) → A(N)
U63¹(tt, M, N) → A(M)
U12¹(tt, V1, V2) → U13¹(isNatKind(a(V2)), a(V1), a(V2))
U13¹(tt, V1, V2) → U14¹(isNatKind(a(V2)), a(V1), a(V2))
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
U13¹(tt, V1, V2) → A(V1)
U63¹(tt, M, N) → U64¹(isNatKind(a(N)), a(M), a(N))
U14¹(tt, V1, V2) → ISNAT(a(V1))
U63¹(tt, M, N) → ISNATKIND(a(N))
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
A(0Inact) → 0¹
U22¹(tt, V1) → A(V1)
U22¹(tt, V1) → U23¹(isNat(a(V1)))
PLUS(N, 0) → U51¹(isNat(N), N)
U15¹(tt, V2) → ISNAT(a(V2))
ISNAT(plusInact(V1, V2)) → A(V2)
U21¹(tt, V1) → U22¹(isNatKind(a(V1)), a(V1))
U64¹(tt, M, N) → A(M)
U15¹(tt, V2) → U16¹(isNat(a(V2)))
U64¹(tt, M, N) → S(plus(a(N), a(M)))
U61¹(tt, M, N) → A(M)
U31¹(tt, V2) → U32¹(isNatKind(a(V2)))
ISNATKIND(plusInact(V1, V2)) → A(V2)
U64¹(tt, M, N) → A(N)
U11¹(tt, V1, V2) → A(V2)
U62¹(tt, M, N) → ISNAT(a(N))
ISNATKIND(sInact(V1)) → U41¹(isNatKind(a(V1)))
U12¹(tt, V1, V2) → A(V2)
U21¹(tt, V1) → ISNATKIND(a(V1))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U22(tt, V1) → U23(isNat(a(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(a(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U64(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

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

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

U12¹(tt, V1, V2) → ISNATKIND(a(V2))
U62¹(tt, M, N) → A(N)
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
U62¹(tt, M, N) → A(M)
PLUS(N, 0) → ISNAT(N)
U14¹(tt, V1, V2) → A(V2)
U14¹(tt, V1, V2) → U15¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
ISNAT(plusInact(V1, V2)) → U11¹(isNatKind(a(V1)), a(V1), a(V2))
U31¹(tt, V2) → ISNATKIND(a(V2))
U62¹(tt, M, N) → U63¹(isNat(a(N)), a(M), a(N))
U51¹(tt, N) → ISNATKIND(a(N))
U11¹(tt, V1, V2) → ISNATKIND(a(V1))
U31¹(tt, V2) → A(V2)
U61¹(tt, M, N) → A(N)
U13¹(tt, V1, V2) → ISNATKIND(a(V2))
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
U15¹(tt, V2) → A(V2)
U22¹(tt, V1) → ISNAT(a(V1))
U13¹(tt, V1, V2) → A(V2)
A(sInact(x1)) → S(x1)
ISNAT(sInact(V1)) → A(V1)
U21¹(tt, V1) → A(V1)
U11¹(tt, V1, V2) → A(V1)
U63¹(tt, M, N) → A(N)
ISNATKIND(plusInact(V1, V2)) → U31¹(isNatKind(a(V1)), a(V2))
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
U11¹(tt, V1, V2) → U12¹(isNatKind(a(V1)), a(V1), a(V2))
U61¹(tt, M, N) → U62¹(isNatKind(a(M)), a(M), a(N))
U52¹(tt, N) → A(N)
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
U64¹(tt, M, N) → PLUS(a(N), a(M))
PLUS(N, s(M)) → U61¹(isNat(M), M, N)
ISNATKIND(plusInact(V1, V2)) → A(V1)
U14¹(tt, V1, V2) → A(V1)
ISNATKIND(sInact(V1)) → A(V1)
U12¹(tt, V1, V2) → A(V1)
U51¹(tt, N) → U52¹(isNatKind(a(N)), a(N))
U61¹(tt, M, N) → ISNATKIND(a(M))
U51¹(tt, N) → A(N)
U63¹(tt, M, N) → A(M)
U12¹(tt, V1, V2) → U13¹(isNatKind(a(V2)), a(V1), a(V2))
U13¹(tt, V1, V2) → U14¹(isNatKind(a(V2)), a(V1), a(V2))
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
U13¹(tt, V1, V2) → A(V1)
U63¹(tt, M, N) → U64¹(isNatKind(a(N)), a(M), a(N))
U14¹(tt, V1, V2) → ISNAT(a(V1))
U63¹(tt, M, N) → ISNATKIND(a(N))
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
A(0Inact) → 0¹
U22¹(tt, V1) → A(V1)
U22¹(tt, V1) → U23¹(isNat(a(V1)))
PLUS(N, 0) → U51¹(isNat(N), N)
U15¹(tt, V2) → ISNAT(a(V2))
ISNAT(plusInact(V1, V2)) → A(V2)
U21¹(tt, V1) → U22¹(isNatKind(a(V1)), a(V1))
U64¹(tt, M, N) → A(M)
U15¹(tt, V2) → U16¹(isNat(a(V2)))
U64¹(tt, M, N) → S(plus(a(N), a(M)))
U61¹(tt, M, N) → A(M)
U31¹(tt, V2) → U32¹(isNatKind(a(V2)))
ISNATKIND(plusInact(V1, V2)) → A(V2)
U64¹(tt, M, N) → A(N)
U11¹(tt, V1, V2) → A(V2)
U62¹(tt, M, N) → ISNAT(a(N))
ISNATKIND(sInact(V1)) → U41¹(isNatKind(a(V1)))
U12¹(tt, V1, V2) → A(V2)
U21¹(tt, V1) → ISNATKIND(a(V1))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U22(tt, V1) → U23(isNat(a(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(a(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U64(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

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

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

U12¹(tt, V1, V2) → ISNATKIND(a(V2))
U62¹(tt, M, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V1)
A(plusInact(x1, x2)) → PLUS(x1, x2)
U62¹(tt, M, N) → A(M)
U14¹(tt, V1, V2) → A(V2)
PLUS(N, 0) → ISNAT(N)
U14¹(tt, V1, V2) → U15¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
ISNAT(plusInact(V1, V2)) → U11¹(isNatKind(a(V1)), a(V1), a(V2))
U31¹(tt, V2) → ISNATKIND(a(V2))
U62¹(tt, M, N) → U63¹(isNat(a(N)), a(M), a(N))
U51¹(tt, N) → ISNATKIND(a(N))
U11¹(tt, V1, V2) → ISNATKIND(a(V1))
U31¹(tt, V2) → A(V2)
U61¹(tt, M, N) → A(N)
U13¹(tt, V1, V2) → ISNATKIND(a(V2))
U15¹(tt, V2) → A(V2)
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
U13¹(tt, V1, V2) → A(V2)
U22¹(tt, V1) → ISNAT(a(V1))
U11¹(tt, V1, V2) → A(V1)
ISNAT(sInact(V1)) → A(V1)
U21¹(tt, V1) → A(V1)
U63¹(tt, M, N) → A(N)
ISNATKIND(plusInact(V1, V2)) → U31¹(isNatKind(a(V1)), a(V2))
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
U11¹(tt, V1, V2) → U12¹(isNatKind(a(V1)), a(V1), a(V2))
U61¹(tt, M, N) → U62¹(isNatKind(a(M)), a(M), a(N))
U52¹(tt, N) → A(N)
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
U64¹(tt, M, N) → PLUS(a(N), a(M))
PLUS(N, s(M)) → U61¹(isNat(M), M, N)
ISNATKIND(plusInact(V1, V2)) → A(V1)
U14¹(tt, V1, V2) → A(V1)
ISNATKIND(sInact(V1)) → A(V1)
U12¹(tt, V1, V2) → A(V1)
U51¹(tt, N) → U52¹(isNatKind(a(N)), a(N))
U61¹(tt, M, N) → ISNATKIND(a(M))
U51¹(tt, N) → A(N)
U63¹(tt, M, N) → A(M)
U12¹(tt, V1, V2) → U13¹(isNatKind(a(V2)), a(V1), a(V2))
U13¹(tt, V1, V2) → U14¹(isNatKind(a(V2)), a(V1), a(V2))
U13¹(tt, V1, V2) → A(V1)
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
U63¹(tt, M, N) → U64¹(isNatKind(a(N)), a(M), a(N))
U14¹(tt, V1, V2) → ISNAT(a(V1))
U63¹(tt, M, N) → ISNATKIND(a(N))
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
U22¹(tt, V1) → A(V1)
U15¹(tt, V2) → ISNAT(a(V2))
PLUS(N, 0) → U51¹(isNat(N), N)
ISNAT(plusInact(V1, V2)) → A(V2)
U21¹(tt, V1) → U22¹(isNatKind(a(V1)), a(V1))
U64¹(tt, M, N) → A(M)
U61¹(tt, M, N) → A(M)
ISNATKIND(plusInact(V1, V2)) → A(V2)
U64¹(tt, M, N) → A(N)
U11¹(tt, V1, V2) → A(V2)
U62¹(tt, M, N) → ISNAT(a(N))
U12¹(tt, V1, V2) → A(V2)
U21¹(tt, V1) → ISNATKIND(a(V1))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U22(tt, V1) → U23(isNat(a(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(a(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U64(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

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.

U12¹(tt, V1, V2) → ISNATKIND(a(V2))
U62¹(tt, M, N) → A(N)
ISNAT(plusInact(V1, V2)) → A(V1)
U62¹(tt, M, N) → A(M)
U14¹(tt, V1, V2) → A(V2)
U51¹(tt, N) → ISNATKIND(a(N))
U11¹(tt, V1, V2) → ISNATKIND(a(V1))
U61¹(tt, M, N) → A(N)
U13¹(tt, V1, V2) → ISNATKIND(a(V2))
U15¹(tt, V2) → A(V2)
ISNAT(sInact(V1)) → U21¹(isNatKind(a(V1)), a(V1))
U13¹(tt, V1, V2) → A(V2)
U11¹(tt, V1, V2) → A(V1)
ISNAT(sInact(V1)) → A(V1)
U21¹(tt, V1) → A(V1)
U63¹(tt, M, N) → A(N)
ISNAT(sInact(V1)) → ISNATKIND(a(V1))
U52¹(tt, N) → A(N)
U14¹(tt, V1, V2) → A(V1)
ISNATKIND(sInact(V1)) → A(V1)
U12¹(tt, V1, V2) → A(V1)
U61¹(tt, M, N) → ISNATKIND(a(M))
U51¹(tt, N) → A(N)
U63¹(tt, M, N) → A(M)
U13¹(tt, V1, V2) → A(V1)
ISNAT(plusInact(V1, V2)) → ISNATKIND(a(V1))
U63¹(tt, M, N) → U64¹(isNatKind(a(N)), a(M), a(N))
U63¹(tt, M, N) → ISNATKIND(a(N))
ISNATKIND(sInact(V1)) → ISNATKIND(a(V1))
U22¹(tt, V1) → A(V1)
ISNAT(plusInact(V1, V2)) → A(V2)
U61¹(tt, M, N) → A(M)
U11¹(tt, V1, V2) → A(V2)
U12¹(tt, V1, V2) → A(V2)
U21¹(tt, V1) → ISNATKIND(a(V1))

The remaining pairs can at least be oriented weakly.

A(plusInact(x1, x2)) → PLUS(x1, x2)
PLUS(N, 0) → ISNAT(N)
U14¹(tt, V1, V2) → U15¹(isNat(a(V1)), a(V2))
PLUS(N, s(M)) → ISNAT(M)
ISNAT(plusInact(V1, V2)) → U11¹(isNatKind(a(V1)), a(V1), a(V2))
U31¹(tt, V2) → ISNATKIND(a(V2))
U62¹(tt, M, N) → U63¹(isNat(a(N)), a(M), a(N))
U31¹(tt, V2) → A(V2)
U22¹(tt, V1) → ISNAT(a(V1))
ISNATKIND(plusInact(V1, V2)) → U31¹(isNatKind(a(V1)), a(V2))
U11¹(tt, V1, V2) → U12¹(isNatKind(a(V1)), a(V1), a(V2))
U61¹(tt, M, N) → U62¹(isNatKind(a(M)), a(M), a(N))
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
U64¹(tt, M, N) → PLUS(a(N), a(M))
PLUS(N, s(M)) → U61¹(isNat(M), M, N)
ISNATKIND(plusInact(V1, V2)) → A(V1)
U51¹(tt, N) → U52¹(isNatKind(a(N)), a(N))
U12¹(tt, V1, V2) → U13¹(isNatKind(a(V2)), a(V1), a(V2))
U13¹(tt, V1, V2) → U14¹(isNatKind(a(V2)), a(V1), a(V2))
U14¹(tt, V1, V2) → ISNAT(a(V1))
U15¹(tt, V2) → ISNAT(a(V2))
PLUS(N, 0) → U51¹(isNat(N), N)
U21¹(tt, V1) → U22¹(isNatKind(a(V1)), a(V1))
U64¹(tt, M, N) → A(M)
ISNATKIND(plusInact(V1, V2)) → A(V2)
U64¹(tt, M, N) → A(N)
U62¹(tt, M, N) → ISNAT(a(N))

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(0Inact) = 1
POL(A(x₁)) = x₁
POL(ISNAT(x₁)) = 1 + x₁
POL(ISNATKIND(x₁)) = x₁
POL(PLUS(x₁, x₂)) = x₁ + x₂
POL(U11(x₁, x₂, x₃)) = 0
POL(U11¹(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U12(x₁, x₂, x₃)) = 0
POL(U12¹(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U13(x₁, x₂, x₃)) = 0
POL(U13¹(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U14(x₁, x₂, x₃)) = 0
POL(U14¹(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U15(x₁, x₂)) = 0
POL(U15¹(x₁, x₂)) = 1 + x₂
POL(U16(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U21¹(x₁, x₂)) = 1 + x₂
POL(U22(x₁, x₂)) = 0
POL(U22¹(x₁, x₂)) = 1 + x₂
POL(U23(x₁)) = 0
POL(U31(x₁, x₂)) = x₂
POL(U31¹(x₁, x₂)) = x₂
POL(U32(x₁)) = 0
POL(U41(x₁)) = 1
POL(U51(x₁, x₂)) = 1 + x₂
POL(U51¹(x₁, x₂)) = 1 + x₂
POL(U52(x₁, x₂)) = 1 + x₂
POL(U52¹(x₁, x₂)) = 1 + x₂
POL(U61(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U61¹(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U62(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U62¹(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U63(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U63¹(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U64(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U64¹(x₁, x₂, x₃)) = x₂ + x₃
POL(a(x₁)) = x₁
POL(isNat(x₁)) = 0
POL(isNatKind(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:

U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
s(x1) → sInact(x1)
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
a(sInact(x1)) → s(x1)
plus(x1, x2) → plusInact(x1, x2)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U64(tt, M, N) → s(plus(a(N), a(M)))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
0 → 0Inact
plus(N, 0) → U51(isNat(N), N)
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
a(plusInact(x1, x2)) → plus(x1, x2)
a(0Inact) → 0
U23(tt) → tt
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
U22(tt, V1) → U23(isNat(a(V1)))
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U31(tt, V2) → U32(isNatKind(a(V2)))
U15(tt, V2) → U16(isNat(a(V2)))
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
U41(tt) → tt
a(x) → x
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
U16(tt) → tt
plus(N, s(M)) → U61(isNat(M), M, N)
U32(tt) → tt

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

U51¹(tt, N) → U52¹(isNatKind(a(N)), a(N))
A(plusInact(x1, x2)) → PLUS(x1, x2)
U14¹(tt, V1, V2) → U15¹(isNat(a(V1)), a(V2))
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → ISNAT(M)
ISNAT(plusInact(V1, V2)) → U11¹(isNatKind(a(V1)), a(V1), a(V2))
U31¹(tt, V2) → ISNATKIND(a(V2))
U12¹(tt, V1, V2) → U13¹(isNatKind(a(V2)), a(V1), a(V2))
U13¹(tt, V1, V2) → U14¹(isNatKind(a(V2)), a(V1), a(V2))
U62¹(tt, M, N) → U63¹(isNat(a(N)), a(M), a(N))
U14¹(tt, V1, V2) → ISNAT(a(V1))
U31¹(tt, V2) → A(V2)
U15¹(tt, V2) → ISNAT(a(V2))
PLUS(N, 0) → U51¹(isNat(N), N)
U22¹(tt, V1) → ISNAT(a(V1))
U21¹(tt, V1) → U22¹(isNatKind(a(V1)), a(V1))
U64¹(tt, M, N) → A(M)
ISNATKIND(plusInact(V1, V2)) → U31¹(isNatKind(a(V1)), a(V2))
U11¹(tt, V1, V2) → U12¹(isNatKind(a(V1)), a(V1), a(V2))
U64¹(tt, M, N) → A(N)
U61¹(tt, M, N) → U62¹(isNatKind(a(M)), a(M), a(N))
ISNATKIND(plusInact(V1, V2)) → A(V2)
U62¹(tt, M, N) → ISNAT(a(N))
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
U64¹(tt, M, N) → PLUS(a(N), a(M))
PLUS(N, s(M)) → U61¹(isNat(M), M, N)
ISNATKIND(plusInact(V1, V2)) → A(V1)

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U22(tt, V1) → U23(isNat(a(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(a(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U64(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

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

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ QDPOrderProof

                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

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

U15¹(tt, V2) → ISNAT(a(V2))
ISNAT(plusInact(V1, V2)) → U11¹(isNatKind(a(V1)), a(V1), a(V2))
U12¹(tt, V1, V2) → U13¹(isNatKind(a(V2)), a(V1), a(V2))
U13¹(tt, V1, V2) → U14¹(isNatKind(a(V2)), a(V1), a(V2))
U14¹(tt, V1, V2) → U15¹(isNat(a(V1)), a(V2))
U14¹(tt, V1, V2) → ISNAT(a(V1))
U11¹(tt, V1, V2) → U12¹(isNatKind(a(V1)), a(V1), a(V2))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U22(tt, V1) → U23(isNat(a(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(a(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U64(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

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) → U12¹(isNatKind(a(V1)), a(V1), a(V2))

The remaining pairs can at least be oriented weakly.

U15¹(tt, V2) → ISNAT(a(V2))
ISNAT(plusInact(V1, V2)) → U11¹(isNatKind(a(V1)), a(V1), a(V2))
U12¹(tt, V1, V2) → U13¹(isNatKind(a(V2)), a(V1), a(V2))
U13¹(tt, V1, V2) → U14¹(isNatKind(a(V2)), a(V1), a(V2))
U14¹(tt, V1, V2) → U15¹(isNat(a(V1)), a(V2))
U14¹(tt, V1, V2) → ISNAT(a(V1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(0Inact) = 0
POL(ISNAT(x₁)) = 1 + x₁
POL(U11(x₁, x₂, x₃)) = 1
POL(U11¹(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(U12(x₁, x₂, x₃)) = 1
POL(U12¹(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U13(x₁, x₂, x₃)) = 1
POL(U13¹(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U14(x₁, x₂, x₃)) = 1
POL(U14¹(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U15(x₁, x₂)) = x₁
POL(U15¹(x₁, x₂)) = 1 + x₂
POL(U16(x₁)) = 1
POL(U21(x₁, x₂)) = 1
POL(U22(x₁, x₂)) = 1
POL(U23(x₁)) = x₁
POL(U31(x₁, x₂)) = 1
POL(U32(x₁)) = 1
POL(U41(x₁)) = 1
POL(U51(x₁, x₂)) = 1 + x₂
POL(U52(x₁, x₂)) = x₂
POL(U61(x₁, x₂, x₃)) = x₃
POL(U62(x₁, x₂, x₃)) = 0
POL(U63(x₁, x₂, x₃)) = 0
POL(U64(x₁, x₂, x₃)) = 0
POL(a(x₁)) = x₁
POL(isNat(x₁)) = 1
POL(isNatKind(x₁)) = 1
POL(plus(x₁, x₂)) = 1 + x₁ + x₂
POL(plusInact(x₁, x₂)) = 1 + x₁ + x₂
POL(s(x₁)) = 0
POL(sInact(x₁)) = 0
POL(tt) = 1

The following usable rules [17] were oriented:

U23(tt) → tt
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
U22(tt, V1) → U23(isNat(a(V1)))
s(x1) → sInact(x1)
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
isNatKind(0Inact) → tt
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U31(tt, V2) → U32(isNatKind(a(V2)))
a(sInact(x1)) → s(x1)
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
plus(x1, x2) → plusInact(x1, x2)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
isNat(0Inact) → tt
U41(tt) → tt
a(x) → x
U64(tt, M, N) → s(plus(a(N), a(M)))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
0 → 0Inact
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
a(0Inact) → 0
plus(N, 0) → U51(isNat(N), N)
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
a(plusInact(x1, x2)) → plus(x1, x2)
U16(tt) → tt
plus(N, s(M)) → U61(isNat(M), M, N)
U32(tt) → tt

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                      ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

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

U15¹(tt, V2) → ISNAT(a(V2))
ISNAT(plusInact(V1, V2)) → U11¹(isNatKind(a(V1)), a(V1), a(V2))
U12¹(tt, V1, V2) → U13¹(isNatKind(a(V2)), a(V1), a(V2))
U13¹(tt, V1, V2) → U14¹(isNatKind(a(V2)), a(V1), a(V2))
U14¹(tt, V1, V2) → U15¹(isNat(a(V1)), a(V2))
U14¹(tt, V1, V2) → ISNAT(a(V1))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U22(tt, V1) → U23(isNat(a(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(a(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U64(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

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

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPOrderProof

  ↳ Incomplete Giesl Middeldorp-Transformation

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

U31¹(tt, V2) → ISNATKIND(a(V2))
ISNATKIND(plusInact(V1, V2)) → ISNATKIND(a(V1))
ISNATKIND(plusInact(V1, V2)) → U31¹(isNatKind(a(V1)), a(V2))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U22(tt, V1) → U23(isNat(a(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(a(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U64(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

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(plusInact(V1, V2)) → ISNATKIND(a(V1))
ISNATKIND(plusInact(V1, V2)) → U31¹(isNatKind(a(V1)), a(V2))

The remaining pairs can at least be oriented weakly.

U31¹(tt, V2) → ISNATKIND(a(V2))

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(0Inact) = 1
POL(ISNATKIND(x₁)) = x₁
POL(U11(x₁, x₂, x₃)) = x₃
POL(U12(x₁, x₂, x₃)) = 0
POL(U13(x₁, x₂, x₃)) = 0
POL(U14(x₁, x₂, x₃)) = 0
POL(U15(x₁, x₂)) = 0
POL(U16(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U22(x₁, x₂)) = 0
POL(U23(x₁)) = 0
POL(U31(x₁, x₂)) = 0
POL(U31¹(x₁, x₂)) = x₂
POL(U32(x₁)) = 0
POL(U41(x₁)) = 0
POL(U51(x₁, x₂)) = 1 + x₂
POL(U52(x₁, x₂)) = x₂
POL(U61(x₁, x₂, x₃)) = 1 + x₃
POL(U62(x₁, x₂, x₃)) = x₃
POL(U63(x₁, x₂, x₃)) = x₃
POL(U64(x₁, x₂, x₃)) = 0
POL(a(x₁)) = x₁
POL(isNat(x₁)) = 1 + x₁
POL(isNatKind(x₁)) = 0
POL(plus(x₁, x₂)) = 1 + x₁ + x₂
POL(plusInact(x₁, x₂)) = 1 + x₁ + x₂
POL(s(x₁)) = 0
POL(sInact(x₁)) = 0
POL(tt) = 0

The following usable rules [17] were oriented:

U23(tt) → tt
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
U22(tt, V1) → U23(isNat(a(V1)))
s(x1) → sInact(x1)
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U31(tt, V2) → U32(isNatKind(a(V2)))
a(sInact(x1)) → s(x1)
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
plus(x1, x2) → plusInact(x1, x2)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U41(tt) → tt
a(x) → x
U64(tt, M, N) → s(plus(a(N), a(M)))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
0 → 0Inact
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
plus(N, 0) → U51(isNat(N), N)
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
a(plusInact(x1, x2)) → plus(x1, x2)
a(0Inact) → 0
U16(tt) → tt
plus(N, s(M)) → U61(isNat(M), M, N)
U32(tt) → tt

↳ CSR

  ↳ Zantema-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

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

U31¹(tt, V2) → ISNATKIND(a(V2))

The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNatKind(a(V1)), a(V1), a(V2))
U12(tt, V1, V2) → U13(isNatKind(a(V2)), a(V1), a(V2))
U13(tt, V1, V2) → U14(isNatKind(a(V2)), a(V1), a(V2))
U14(tt, V1, V2) → U15(isNat(a(V1)), a(V2))
U15(tt, V2) → U16(isNat(a(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(a(V1)), a(V1))
U22(tt, V1) → U23(isNat(a(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(a(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(a(N)), a(N))
U52(tt, N) → a(N)
U61(tt, M, N) → U62(isNatKind(a(M)), a(M), a(N))
U62(tt, M, N) → U63(isNat(a(N)), a(M), a(N))
U63(tt, M, N) → U64(isNatKind(a(N)), a(M), a(N))
U64(tt, M, N) → s(plus(a(N), a(M)))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNatKind(a(V1)), a(V1), a(V2))
isNat(sInact(V1)) → U21(isNatKind(a(V1)), a(V1))
isNatKind(0Inact) → tt
isNatKind(plusInact(V1, V2)) → U31(isNatKind(a(V1)), a(V2))
isNatKind(sInact(V1)) → U41(isNatKind(a(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Incomplete Giesl Middeldorp [11] to transform the context-sensitive TRS to an usual TRS.

↳ CSR

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

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

mark(U11(x1, x2, x3)) → U11Active(mark(x1), x2, x3)
U11Active(x1, x2, x3) → U11(x1, x2, x3)
mark(U12(x1, x2, x3)) → U12Active(mark(x1), x2, x3)
U12Active(x1, x2, x3) → U12(x1, x2, x3)
mark(U13(x1, x2, x3)) → U13Active(mark(x1), x2, x3)
U13Active(x1, x2, x3) → U13(x1, x2, x3)
mark(U14(x1, x2, x3)) → U14Active(mark(x1), x2, x3)
U14Active(x1, x2, x3) → U14(x1, x2, x3)
mark(U15(x1, x2)) → U15Active(mark(x1), x2)
U15Active(x1, x2) → U15(x1, x2)
mark(U16(x1)) → U16Active(mark(x1))
U16Active(x1) → U16(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1, x2)) → U22Active(mark(x1), x2)
U22Active(x1, x2) → U22(x1, x2)
mark(U23(x1)) → U23Active(mark(x1))
U23Active(x1) → U23(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1)) → U41Active(mark(x1))
U41Active(x1) → U41(x1)
mark(U51(x1, x2)) → U51Active(mark(x1), x2)
U51Active(x1, x2) → U51(x1, x2)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U61(x1, x2, x3)) → U61Active(mark(x1), x2, x3)
U61Active(x1, x2, x3) → U61(x1, x2, x3)
mark(U62(x1, x2, x3)) → U62Active(mark(x1), x2, x3)
U62Active(x1, x2, x3) → U62(x1, x2, x3)
mark(U63(x1, x2, x3)) → U63Active(mark(x1), x2, x3)
U63Active(x1, x2, x3) → U63(x1, x2, x3)
mark(U64(x1, x2, x3)) → U64Active(mark(x1), x2, x3)
U64Active(x1, x2, x3) → U64(x1, x2, x3)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(plus(x1, x2)) → plusActive(mark(x1), mark(x2))
plusActive(x1, x2) → plus(x1, x2)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(0) → 0
U11Active(tt, V1, V2) → U12Active(isNatKindActive(V1), V1, V2)
U12Active(tt, V1, V2) → U13Active(isNatKindActive(V2), V1, V2)
U13Active(tt, V1, V2) → U14Active(isNatKindActive(V2), V1, V2)
U14Active(tt, V1, V2) → U15Active(isNatActive(V1), V2)
U15Active(tt, V2) → U16Active(isNatActive(V2))
U16Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatKindActive(V1), V1)
U22Active(tt, V1) → U23Active(isNatActive(V1))
U23Active(tt) → tt
U31Active(tt, V2) → U32Active(isNatKindActive(V2))
U32Active(tt) → tt
U41Active(tt) → tt
U51Active(tt, N) → U52Active(isNatKindActive(N), N)
U52Active(tt, N) → mark(N)
U61Active(tt, M, N) → U62Active(isNatKindActive(M), M, N)
U62Active(tt, M, N) → U63Active(isNatActive(N), M, N)
U63Active(tt, M, N) → U64Active(isNatKindActive(N), M, N)
U64Active(tt, M, N) → s(plusActive(mark(N), mark(M)))
isNatActive(0) → tt
isNatActive(plus(V1, V2)) → U11Active(isNatKindActive(V1), V1, V2)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatKindActive(0) → tt
isNatKindActive(plus(V1, V2)) → U31Active(isNatKindActive(V1), V2)
isNatKindActive(s(V1)) → U41Active(isNatKindActive(V1))
plusActive(N, 0) → U51Active(isNatActive(N), N)
plusActive(N, s(M)) → U61Active(isNatActive(M), M, N)

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:

U12ACTIVE(tt, V1, V2) → U13ACTIVE(isNatKindActive(V2), V1, V2)
ISNATKINDACTIVE(plus(V1, V2)) → ISNATKINDACTIVE(V1)
U11ACTIVE(tt, V1, V2) → ISNATKINDACTIVE(V1)
U61ACTIVE(tt, M, N) → U62ACTIVE(isNatKindActive(M), M, N)
MARK(U63(x1, x2, x3)) → U63ACTIVE(mark(x1), x2, x3)
MARK(U32(x1)) → U32ACTIVE(mark(x1))
U13ACTIVE(tt, V1, V2) → ISNATKINDACTIVE(V2)
MARK(plus(x1, x2)) → MARK(x2)
U21ACTIVE(tt, V1) → U22ACTIVE(isNatKindActive(V1), V1)
MARK(U31(x1, x2)) → U31ACTIVE(mark(x1), x2)
MARK(U11(x1, x2, x3)) → MARK(x1)
MARK(U14(x1, x2, x3)) → U14ACTIVE(mark(x1), x2, x3)
MARK(U11(x1, x2, x3)) → U11ACTIVE(mark(x1), x2, x3)
PLUSACTIVE(N, s(M)) → ISNATACTIVE(M)
MARK(U22(x1, x2)) → MARK(x1)
U22ACTIVE(tt, V1) → U23ACTIVE(isNatActive(V1))
MARK(U52(x1, x2)) → MARK(x1)
MARK(U23(x1)) → U23ACTIVE(mark(x1))
MARK(U21(x1, x2)) → MARK(x1)
MARK(U22(x1, x2)) → U22ACTIVE(mark(x1), x2)
U31ACTIVE(tt, V2) → U32ACTIVE(isNatKindActive(V2))
MARK(U51(x1, x2)) → MARK(x1)
U64ACTIVE(tt, M, N) → PLUSACTIVE(mark(N), mark(M))
U14ACTIVE(tt, V1, V2) → U15ACTIVE(isNatActive(V1), V2)
MARK(U64(x1, x2, x3)) → MARK(x1)
U14ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(U16(x1)) → MARK(x1)
MARK(U61(x1, x2, x3)) → MARK(x1)
ISNATKINDACTIVE(plus(V1, V2)) → U31ACTIVE(isNatKindActive(V1), V2)
U63ACTIVE(tt, M, N) → ISNATKINDACTIVE(N)
MARK(U13(x1, x2, x3)) → MARK(x1)
MARK(U41(x1)) → MARK(x1)
U63ACTIVE(tt, M, N) → U64ACTIVE(isNatKindActive(N), M, N)
MARK(U51(x1, x2)) → U51ACTIVE(mark(x1), x2)
MARK(s(x1)) → MARK(x1)
MARK(isNatKind(x1)) → ISNATKINDACTIVE(x1)
U64ACTIVE(tt, M, N) → MARK(M)
MARK(U31(x1, x2)) → MARK(x1)
PLUSACTIVE(N, s(M)) → U61ACTIVE(isNatActive(M), M, N)
ISNATACTIVE(plus(V1, V2)) → ISNATKINDACTIVE(V1)
U15ACTIVE(tt, V2) → ISNATACTIVE(V2)
MARK(U61(x1, x2, x3)) → U61ACTIVE(mark(x1), x2, x3)
MARK(isNat(x1)) → ISNATACTIVE(x1)
U61ACTIVE(tt, M, N) → ISNATKINDACTIVE(M)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)
MARK(plus(x1, x2)) → MARK(x1)
MARK(U12(x1, x2, x3)) → MARK(x1)
U64ACTIVE(tt, M, N) → MARK(N)
U21ACTIVE(tt, V1) → ISNATKINDACTIVE(V1)
U11ACTIVE(tt, V1, V2) → U12ACTIVE(isNatKindActive(V1), V1, V2)
MARK(U14(x1, x2, x3)) → MARK(x1)
MARK(plus(x1, x2)) → PLUSACTIVE(mark(x1), mark(x2))
PLUSACTIVE(N, 0) → ISNATACTIVE(N)
MARK(U41(x1)) → U41ACTIVE(mark(x1))
MARK(U64(x1, x2, x3)) → U64ACTIVE(mark(x1), x2, x3)
ISNATKINDACTIVE(s(V1)) → U41ACTIVE(isNatKindActive(V1))
MARK(U62(x1, x2, x3)) → MARK(x1)
U12ACTIVE(tt, V1, V2) → ISNATKINDACTIVE(V2)
PLUSACTIVE(N, 0) → U51ACTIVE(isNatActive(N), N)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
MARK(U23(x1)) → MARK(x1)
U51ACTIVE(tt, N) → U52ACTIVE(isNatKindActive(N), N)
ISNATACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
MARK(U15(x1, x2)) → MARK(x1)
MARK(U63(x1, x2, x3)) → MARK(x1)
MARK(U15(x1, x2)) → U15ACTIVE(mark(x1), x2)
U62ACTIVE(tt, M, N) → U63ACTIVE(isNatActive(N), M, N)
U51ACTIVE(tt, N) → ISNATKINDACTIVE(N)
U22ACTIVE(tt, V1) → ISNATACTIVE(V1)
U52ACTIVE(tt, N) → MARK(N)
MARK(U32(x1)) → MARK(x1)
U15ACTIVE(tt, V2) → U16ACTIVE(isNatActive(V2))
U31ACTIVE(tt, V2) → ISNATKINDACTIVE(V2)
MARK(U21(x1, x2)) → U21ACTIVE(mark(x1), x2)
MARK(U13(x1, x2, x3)) → U13ACTIVE(mark(x1), x2, x3)
U13ACTIVE(tt, V1, V2) → U14ACTIVE(isNatKindActive(V2), V1, V2)
ISNATACTIVE(plus(V1, V2)) → U11ACTIVE(isNatKindActive(V1), V1, V2)
MARK(U16(x1)) → U16ACTIVE(mark(x1))
MARK(U62(x1, x2, x3)) → U62ACTIVE(mark(x1), x2, x3)
U62ACTIVE(tt, M, N) → ISNATACTIVE(N)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
MARK(U12(x1, x2, x3)) → U12ACTIVE(mark(x1), x2, x3)

The TRS R consists of the following rules:

mark(U11(x1, x2, x3)) → U11Active(mark(x1), x2, x3)
U11Active(x1, x2, x3) → U11(x1, x2, x3)
mark(U12(x1, x2, x3)) → U12Active(mark(x1), x2, x3)
U12Active(x1, x2, x3) → U12(x1, x2, x3)
mark(U13(x1, x2, x3)) → U13Active(mark(x1), x2, x3)
U13Active(x1, x2, x3) → U13(x1, x2, x3)
mark(U14(x1, x2, x3)) → U14Active(mark(x1), x2, x3)
U14Active(x1, x2, x3) → U14(x1, x2, x3)
mark(U15(x1, x2)) → U15Active(mark(x1), x2)
U15Active(x1, x2) → U15(x1, x2)
mark(U16(x1)) → U16Active(mark(x1))
U16Active(x1) → U16(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1, x2)) → U22Active(mark(x1), x2)
U22Active(x1, x2) → U22(x1, x2)
mark(U23(x1)) → U23Active(mark(x1))
U23Active(x1) → U23(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1)) → U41Active(mark(x1))
U41Active(x1) → U41(x1)
mark(U51(x1, x2)) → U51Active(mark(x1), x2)
U51Active(x1, x2) → U51(x1, x2)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U61(x1, x2, x3)) → U61Active(mark(x1), x2, x3)
U61Active(x1, x2, x3) → U61(x1, x2, x3)
mark(U62(x1, x2, x3)) → U62Active(mark(x1), x2, x3)
U62Active(x1, x2, x3) → U62(x1, x2, x3)
mark(U63(x1, x2, x3)) → U63Active(mark(x1), x2, x3)
U63Active(x1, x2, x3) → U63(x1, x2, x3)
mark(U64(x1, x2, x3)) → U64Active(mark(x1), x2, x3)
U64Active(x1, x2, x3) → U64(x1, x2, x3)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(plus(x1, x2)) → plusActive(mark(x1), mark(x2))
plusActive(x1, x2) → plus(x1, x2)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(0) → 0
U11Active(tt, V1, V2) → U12Active(isNatKindActive(V1), V1, V2)
U12Active(tt, V1, V2) → U13Active(isNatKindActive(V2), V1, V2)
U13Active(tt, V1, V2) → U14Active(isNatKindActive(V2), V1, V2)
U14Active(tt, V1, V2) → U15Active(isNatActive(V1), V2)
U15Active(tt, V2) → U16Active(isNatActive(V2))
U16Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatKindActive(V1), V1)
U22Active(tt, V1) → U23Active(isNatActive(V1))
U23Active(tt) → tt
U31Active(tt, V2) → U32Active(isNatKindActive(V2))
U32Active(tt) → tt
U41Active(tt) → tt
U51Active(tt, N) → U52Active(isNatKindActive(N), N)
U52Active(tt, N) → mark(N)
U61Active(tt, M, N) → U62Active(isNatKindActive(M), M, N)
U62Active(tt, M, N) → U63Active(isNatActive(N), M, N)
U63Active(tt, M, N) → U64Active(isNatKindActive(N), M, N)
U64Active(tt, M, N) → s(plusActive(mark(N), mark(M)))
isNatActive(0) → tt
isNatActive(plus(V1, V2)) → U11Active(isNatKindActive(V1), V1, V2)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatKindActive(0) → tt
isNatKindActive(plus(V1, V2)) → U31Active(isNatKindActive(V1), V2)
isNatKindActive(s(V1)) → U41Active(isNatKindActive(V1))
plusActive(N, 0) → U51Active(isNatActive(N), N)
plusActive(N, s(M)) → U61Active(isNatActive(M), M, N)

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

↳ CSR

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

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

U12ACTIVE(tt, V1, V2) → U13ACTIVE(isNatKindActive(V2), V1, V2)
ISNATKINDACTIVE(plus(V1, V2)) → ISNATKINDACTIVE(V1)
U11ACTIVE(tt, V1, V2) → ISNATKINDACTIVE(V1)
U61ACTIVE(tt, M, N) → U62ACTIVE(isNatKindActive(M), M, N)
MARK(U63(x1, x2, x3)) → U63ACTIVE(mark(x1), x2, x3)
MARK(U32(x1)) → U32ACTIVE(mark(x1))
U13ACTIVE(tt, V1, V2) → ISNATKINDACTIVE(V2)
MARK(plus(x1, x2)) → MARK(x2)
U21ACTIVE(tt, V1) → U22ACTIVE(isNatKindActive(V1), V1)
MARK(U31(x1, x2)) → U31ACTIVE(mark(x1), x2)
MARK(U11(x1, x2, x3)) → MARK(x1)
MARK(U14(x1, x2, x3)) → U14ACTIVE(mark(x1), x2, x3)
MARK(U11(x1, x2, x3)) → U11ACTIVE(mark(x1), x2, x3)
PLUSACTIVE(N, s(M)) → ISNATACTIVE(M)
MARK(U22(x1, x2)) → MARK(x1)
U22ACTIVE(tt, V1) → U23ACTIVE(isNatActive(V1))
MARK(U52(x1, x2)) → MARK(x1)
MARK(U23(x1)) → U23ACTIVE(mark(x1))
MARK(U21(x1, x2)) → MARK(x1)
MARK(U22(x1, x2)) → U22ACTIVE(mark(x1), x2)
U31ACTIVE(tt, V2) → U32ACTIVE(isNatKindActive(V2))
MARK(U51(x1, x2)) → MARK(x1)
U64ACTIVE(tt, M, N) → PLUSACTIVE(mark(N), mark(M))
U14ACTIVE(tt, V1, V2) → U15ACTIVE(isNatActive(V1), V2)
MARK(U64(x1, x2, x3)) → MARK(x1)
U14ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(U16(x1)) → MARK(x1)
MARK(U61(x1, x2, x3)) → MARK(x1)
ISNATKINDACTIVE(plus(V1, V2)) → U31ACTIVE(isNatKindActive(V1), V2)
U63ACTIVE(tt, M, N) → ISNATKINDACTIVE(N)
MARK(U13(x1, x2, x3)) → MARK(x1)
MARK(U41(x1)) → MARK(x1)
U63ACTIVE(tt, M, N) → U64ACTIVE(isNatKindActive(N), M, N)
MARK(U51(x1, x2)) → U51ACTIVE(mark(x1), x2)
MARK(s(x1)) → MARK(x1)
MARK(isNatKind(x1)) → ISNATKINDACTIVE(x1)
U64ACTIVE(tt, M, N) → MARK(M)
MARK(U31(x1, x2)) → MARK(x1)
PLUSACTIVE(N, s(M)) → U61ACTIVE(isNatActive(M), M, N)
ISNATACTIVE(plus(V1, V2)) → ISNATKINDACTIVE(V1)
U15ACTIVE(tt, V2) → ISNATACTIVE(V2)
MARK(U61(x1, x2, x3)) → U61ACTIVE(mark(x1), x2, x3)
MARK(isNat(x1)) → ISNATACTIVE(x1)
U61ACTIVE(tt, M, N) → ISNATKINDACTIVE(M)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)
MARK(plus(x1, x2)) → MARK(x1)
MARK(U12(x1, x2, x3)) → MARK(x1)
U64ACTIVE(tt, M, N) → MARK(N)
U21ACTIVE(tt, V1) → ISNATKINDACTIVE(V1)
U11ACTIVE(tt, V1, V2) → U12ACTIVE(isNatKindActive(V1), V1, V2)
MARK(U14(x1, x2, x3)) → MARK(x1)
MARK(plus(x1, x2)) → PLUSACTIVE(mark(x1), mark(x2))
PLUSACTIVE(N, 0) → ISNATACTIVE(N)
MARK(U41(x1)) → U41ACTIVE(mark(x1))
MARK(U64(x1, x2, x3)) → U64ACTIVE(mark(x1), x2, x3)
ISNATKINDACTIVE(s(V1)) → U41ACTIVE(isNatKindActive(V1))
MARK(U62(x1, x2, x3)) → MARK(x1)
U12ACTIVE(tt, V1, V2) → ISNATKINDACTIVE(V2)
PLUSACTIVE(N, 0) → U51ACTIVE(isNatActive(N), N)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
MARK(U23(x1)) → MARK(x1)
U51ACTIVE(tt, N) → U52ACTIVE(isNatKindActive(N), N)
ISNATACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
MARK(U15(x1, x2)) → MARK(x1)
MARK(U63(x1, x2, x3)) → MARK(x1)
MARK(U15(x1, x2)) → U15ACTIVE(mark(x1), x2)
U62ACTIVE(tt, M, N) → U63ACTIVE(isNatActive(N), M, N)
U51ACTIVE(tt, N) → ISNATKINDACTIVE(N)
U22ACTIVE(tt, V1) → ISNATACTIVE(V1)
U52ACTIVE(tt, N) → MARK(N)
MARK(U32(x1)) → MARK(x1)
U15ACTIVE(tt, V2) → U16ACTIVE(isNatActive(V2))
U31ACTIVE(tt, V2) → ISNATKINDACTIVE(V2)
MARK(U21(x1, x2)) → U21ACTIVE(mark(x1), x2)
MARK(U13(x1, x2, x3)) → U13ACTIVE(mark(x1), x2, x3)
U13ACTIVE(tt, V1, V2) → U14ACTIVE(isNatKindActive(V2), V1, V2)
ISNATACTIVE(plus(V1, V2)) → U11ACTIVE(isNatKindActive(V1), V1, V2)
MARK(U16(x1)) → U16ACTIVE(mark(x1))
MARK(U62(x1, x2, x3)) → U62ACTIVE(mark(x1), x2, x3)
U62ACTIVE(tt, M, N) → ISNATACTIVE(N)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
MARK(U12(x1, x2, x3)) → U12ACTIVE(mark(x1), x2, x3)

The TRS R consists of the following rules:

mark(U11(x1, x2, x3)) → U11Active(mark(x1), x2, x3)
U11Active(x1, x2, x3) → U11(x1, x2, x3)
mark(U12(x1, x2, x3)) → U12Active(mark(x1), x2, x3)
U12Active(x1, x2, x3) → U12(x1, x2, x3)
mark(U13(x1, x2, x3)) → U13Active(mark(x1), x2, x3)
U13Active(x1, x2, x3) → U13(x1, x2, x3)
mark(U14(x1, x2, x3)) → U14Active(mark(x1), x2, x3)
U14Active(x1, x2, x3) → U14(x1, x2, x3)
mark(U15(x1, x2)) → U15Active(mark(x1), x2)
U15Active(x1, x2) → U15(x1, x2)
mark(U16(x1)) → U16Active(mark(x1))
U16Active(x1) → U16(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1, x2)) → U22Active(mark(x1), x2)
U22Active(x1, x2) → U22(x1, x2)
mark(U23(x1)) → U23Active(mark(x1))
U23Active(x1) → U23(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1)) → U41Active(mark(x1))
U41Active(x1) → U41(x1)
mark(U51(x1, x2)) → U51Active(mark(x1), x2)
U51Active(x1, x2) → U51(x1, x2)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U61(x1, x2, x3)) → U61Active(mark(x1), x2, x3)
U61Active(x1, x2, x3) → U61(x1, x2, x3)
mark(U62(x1, x2, x3)) → U62Active(mark(x1), x2, x3)
U62Active(x1, x2, x3) → U62(x1, x2, x3)
mark(U63(x1, x2, x3)) → U63Active(mark(x1), x2, x3)
U63Active(x1, x2, x3) → U63(x1, x2, x3)
mark(U64(x1, x2, x3)) → U64Active(mark(x1), x2, x3)
U64Active(x1, x2, x3) → U64(x1, x2, x3)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(plus(x1, x2)) → plusActive(mark(x1), mark(x2))
plusActive(x1, x2) → plus(x1, x2)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(0) → 0
U11Active(tt, V1, V2) → U12Active(isNatKindActive(V1), V1, V2)
U12Active(tt, V1, V2) → U13Active(isNatKindActive(V2), V1, V2)
U13Active(tt, V1, V2) → U14Active(isNatKindActive(V2), V1, V2)
U14Active(tt, V1, V2) → U15Active(isNatActive(V1), V2)
U15Active(tt, V2) → U16Active(isNatActive(V2))
U16Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatKindActive(V1), V1)
U22Active(tt, V1) → U23Active(isNatActive(V1))
U23Active(tt) → tt
U31Active(tt, V2) → U32Active(isNatKindActive(V2))
U32Active(tt) → tt
U41Active(tt) → tt
U51Active(tt, N) → U52Active(isNatKindActive(N), N)
U52Active(tt, N) → mark(N)
U61Active(tt, M, N) → U62Active(isNatKindActive(M), M, N)
U62Active(tt, M, N) → U63Active(isNatActive(N), M, N)
U63Active(tt, M, N) → U64Active(isNatKindActive(N), M, N)
U64Active(tt, M, N) → s(plusActive(mark(N), mark(M)))
isNatActive(0) → tt
isNatActive(plus(V1, V2)) → U11Active(isNatKindActive(V1), V1, V2)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatKindActive(0) → tt
isNatKindActive(plus(V1, V2)) → U31Active(isNatKindActive(V1), V2)
isNatKindActive(s(V1)) → U41Active(isNatKindActive(V1))
plusActive(N, 0) → U51Active(isNatActive(N), N)
plusActive(N, s(M)) → U61Active(isNatActive(M), M, N)

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 with 30 less nodes.

↳ CSR

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

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

ISNATKINDACTIVE(plus(V1, V2)) → ISNATKINDACTIVE(V1)
U31ACTIVE(tt, V2) → ISNATKINDACTIVE(V2)
ISNATKINDACTIVE(plus(V1, V2)) → U31ACTIVE(isNatKindActive(V1), V2)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)

The TRS R consists of the following rules:

mark(U11(x1, x2, x3)) → U11Active(mark(x1), x2, x3)
U11Active(x1, x2, x3) → U11(x1, x2, x3)
mark(U12(x1, x2, x3)) → U12Active(mark(x1), x2, x3)
U12Active(x1, x2, x3) → U12(x1, x2, x3)
mark(U13(x1, x2, x3)) → U13Active(mark(x1), x2, x3)
U13Active(x1, x2, x3) → U13(x1, x2, x3)
mark(U14(x1, x2, x3)) → U14Active(mark(x1), x2, x3)
U14Active(x1, x2, x3) → U14(x1, x2, x3)
mark(U15(x1, x2)) → U15Active(mark(x1), x2)
U15Active(x1, x2) → U15(x1, x2)
mark(U16(x1)) → U16Active(mark(x1))
U16Active(x1) → U16(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1, x2)) → U22Active(mark(x1), x2)
U22Active(x1, x2) → U22(x1, x2)
mark(U23(x1)) → U23Active(mark(x1))
U23Active(x1) → U23(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1)) → U41Active(mark(x1))
U41Active(x1) → U41(x1)
mark(U51(x1, x2)) → U51Active(mark(x1), x2)
U51Active(x1, x2) → U51(x1, x2)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U61(x1, x2, x3)) → U61Active(mark(x1), x2, x3)
U61Active(x1, x2, x3) → U61(x1, x2, x3)
mark(U62(x1, x2, x3)) → U62Active(mark(x1), x2, x3)
U62Active(x1, x2, x3) → U62(x1, x2, x3)
mark(U63(x1, x2, x3)) → U63Active(mark(x1), x2, x3)
U63Active(x1, x2, x3) → U63(x1, x2, x3)
mark(U64(x1, x2, x3)) → U64Active(mark(x1), x2, x3)
U64Active(x1, x2, x3) → U64(x1, x2, x3)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(plus(x1, x2)) → plusActive(mark(x1), mark(x2))
plusActive(x1, x2) → plus(x1, x2)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(0) → 0
U11Active(tt, V1, V2) → U12Active(isNatKindActive(V1), V1, V2)
U12Active(tt, V1, V2) → U13Active(isNatKindActive(V2), V1, V2)
U13Active(tt, V1, V2) → U14Active(isNatKindActive(V2), V1, V2)
U14Active(tt, V1, V2) → U15Active(isNatActive(V1), V2)
U15Active(tt, V2) → U16Active(isNatActive(V2))
U16Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatKindActive(V1), V1)
U22Active(tt, V1) → U23Active(isNatActive(V1))
U23Active(tt) → tt
U31Active(tt, V2) → U32Active(isNatKindActive(V2))
U32Active(tt) → tt
U41Active(tt) → tt
U51Active(tt, N) → U52Active(isNatKindActive(N), N)
U52Active(tt, N) → mark(N)
U61Active(tt, M, N) → U62Active(isNatKindActive(M), M, N)
U62Active(tt, M, N) → U63Active(isNatActive(N), M, N)
U63Active(tt, M, N) → U64Active(isNatKindActive(N), M, N)
U64Active(tt, M, N) → s(plusActive(mark(N), mark(M)))
isNatActive(0) → tt
isNatActive(plus(V1, V2)) → U11Active(isNatKindActive(V1), V1, V2)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatKindActive(0) → tt
isNatKindActive(plus(V1, V2)) → U31Active(isNatKindActive(V1), V2)
isNatKindActive(s(V1)) → U41Active(isNatKindActive(V1))
plusActive(N, 0) → U51Active(isNatActive(N), N)
plusActive(N, s(M)) → U61Active(isNatActive(M), M, N)

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

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

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

ISNATKINDACTIVE(plus(V1, V2)) → ISNATKINDACTIVE(V1)
U31ACTIVE(tt, V2) → ISNATKINDACTIVE(V2)
ISNATKINDACTIVE(plus(V1, V2)) → U31ACTIVE(isNatKindActive(V1), V2)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)

The TRS R consists of the following rules:

isNatKindActive(x1) → isNatKind(x1)
isNatKindActive(0) → tt
isNatKindActive(plus(V1, V2)) → U31Active(isNatKindActive(V1), V2)
isNatKindActive(s(V1)) → U41Active(isNatKindActive(V1))
U41Active(x1) → U41(x1)
U41Active(tt) → tt
U31Active(x1, x2) → U31(x1, x2)
U31Active(tt, V2) → U32Active(isNatKindActive(V2))
U32Active(x1) → U32(x1)
U32Active(tt) → tt

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:

ISNATKINDACTIVE(plus(V1, V2)) → U31ACTIVE(isNatKindActive(V1), V2)
The graph contains the following edges 1 > 2
U31ACTIVE(tt, V2) → ISNATKINDACTIVE(V2)
The graph contains the following edges 2 >= 1
ISNATKINDACTIVE(plus(V1, V2)) → ISNATKINDACTIVE(V1)
The graph contains the following edges 1 > 1
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
The graph contains the following edges 1 > 1

↳ CSR

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

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

U12ACTIVE(tt, V1, V2) → U13ACTIVE(isNatKindActive(V2), V1, V2)
U21ACTIVE(tt, V1) → U22ACTIVE(isNatKindActive(V1), V1)
U14ACTIVE(tt, V1, V2) → U15ACTIVE(isNatActive(V1), V2)
U22ACTIVE(tt, V1) → ISNATACTIVE(V1)
U14ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
U13ACTIVE(tt, V1, V2) → U14ACTIVE(isNatKindActive(V2), V1, V2)
U11ACTIVE(tt, V1, V2) → U12ACTIVE(isNatKindActive(V1), V1, V2)
ISNATACTIVE(plus(V1, V2)) → U11ACTIVE(isNatKindActive(V1), V1, V2)
U15ACTIVE(tt, V2) → ISNATACTIVE(V2)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)

The TRS R consists of the following rules:

mark(U11(x1, x2, x3)) → U11Active(mark(x1), x2, x3)
U11Active(x1, x2, x3) → U11(x1, x2, x3)
mark(U12(x1, x2, x3)) → U12Active(mark(x1), x2, x3)
U12Active(x1, x2, x3) → U12(x1, x2, x3)
mark(U13(x1, x2, x3)) → U13Active(mark(x1), x2, x3)
U13Active(x1, x2, x3) → U13(x1, x2, x3)
mark(U14(x1, x2, x3)) → U14Active(mark(x1), x2, x3)
U14Active(x1, x2, x3) → U14(x1, x2, x3)
mark(U15(x1, x2)) → U15Active(mark(x1), x2)
U15Active(x1, x2) → U15(x1, x2)
mark(U16(x1)) → U16Active(mark(x1))
U16Active(x1) → U16(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1, x2)) → U22Active(mark(x1), x2)
U22Active(x1, x2) → U22(x1, x2)
mark(U23(x1)) → U23Active(mark(x1))
U23Active(x1) → U23(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1)) → U41Active(mark(x1))
U41Active(x1) → U41(x1)
mark(U51(x1, x2)) → U51Active(mark(x1), x2)
U51Active(x1, x2) → U51(x1, x2)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U61(x1, x2, x3)) → U61Active(mark(x1), x2, x3)
U61Active(x1, x2, x3) → U61(x1, x2, x3)
mark(U62(x1, x2, x3)) → U62Active(mark(x1), x2, x3)
U62Active(x1, x2, x3) → U62(x1, x2, x3)
mark(U63(x1, x2, x3)) → U63Active(mark(x1), x2, x3)
U63Active(x1, x2, x3) → U63(x1, x2, x3)
mark(U64(x1, x2, x3)) → U64Active(mark(x1), x2, x3)
U64Active(x1, x2, x3) → U64(x1, x2, x3)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(plus(x1, x2)) → plusActive(mark(x1), mark(x2))
plusActive(x1, x2) → plus(x1, x2)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(0) → 0
U11Active(tt, V1, V2) → U12Active(isNatKindActive(V1), V1, V2)
U12Active(tt, V1, V2) → U13Active(isNatKindActive(V2), V1, V2)
U13Active(tt, V1, V2) → U14Active(isNatKindActive(V2), V1, V2)
U14Active(tt, V1, V2) → U15Active(isNatActive(V1), V2)
U15Active(tt, V2) → U16Active(isNatActive(V2))
U16Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatKindActive(V1), V1)
U22Active(tt, V1) → U23Active(isNatActive(V1))
U23Active(tt) → tt
U31Active(tt, V2) → U32Active(isNatKindActive(V2))
U32Active(tt) → tt
U41Active(tt) → tt
U51Active(tt, N) → U52Active(isNatKindActive(N), N)
U52Active(tt, N) → mark(N)
U61Active(tt, M, N) → U62Active(isNatKindActive(M), M, N)
U62Active(tt, M, N) → U63Active(isNatActive(N), M, N)
U63Active(tt, M, N) → U64Active(isNatKindActive(N), M, N)
U64Active(tt, M, N) → s(plusActive(mark(N), mark(M)))
isNatActive(0) → tt
isNatActive(plus(V1, V2)) → U11Active(isNatKindActive(V1), V1, V2)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatKindActive(0) → tt
isNatKindActive(plus(V1, V2)) → U31Active(isNatKindActive(V1), V2)
isNatKindActive(s(V1)) → U41Active(isNatKindActive(V1))
plusActive(N, 0) → U51Active(isNatActive(N), N)
plusActive(N, s(M)) → U61Active(isNatActive(M), M, N)

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

U13ACTIVE(tt, V1, V2) → U14ACTIVE(isNatKindActive(V2), V1, V2)
The graph contains the following edges 2 >= 2, 3 >= 3
U11ACTIVE(tt, V1, V2) → U12ACTIVE(isNatKindActive(V1), V1, V2)
The graph contains the following edges 2 >= 2, 3 >= 3
U12ACTIVE(tt, V1, V2) → U13ACTIVE(isNatKindActive(V2), V1, V2)
The graph contains the following edges 2 >= 2, 3 >= 3
U15ACTIVE(tt, V2) → ISNATACTIVE(V2)
The graph contains the following edges 2 >= 1
U14ACTIVE(tt, V1, V2) → U15ACTIVE(isNatActive(V1), V2)
The graph contains the following edges 3 >= 2
U14ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
The graph contains the following edges 2 >= 1
U22ACTIVE(tt, V1) → ISNATACTIVE(V1)
The graph contains the following edges 2 >= 1
U21ACTIVE(tt, V1) → U22ACTIVE(isNatKindActive(V1), V1)
The graph contains the following edges 2 >= 2
ISNATACTIVE(plus(V1, V2)) → U11ACTIVE(isNatKindActive(V1), V1, V2)
The graph contains the following edges 1 > 2, 1 > 3
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
The graph contains the following edges 1 > 2

↳ CSR

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

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

MARK(U12(x1, x2, x3)) → MARK(x1)
U64ACTIVE(tt, M, N) → MARK(N)
U61ACTIVE(tt, M, N) → U62ACTIVE(isNatKindActive(M), M, N)
MARK(plus(x1, x2)) → PLUSACTIVE(mark(x1), mark(x2))
MARK(U63(x1, x2, x3)) → U63ACTIVE(mark(x1), x2, x3)
MARK(U14(x1, x2, x3)) → MARK(x1)
MARK(plus(x1, x2)) → MARK(x2)
MARK(U64(x1, x2, x3)) → U64ACTIVE(mark(x1), x2, x3)
MARK(U11(x1, x2, x3)) → MARK(x1)
MARK(U22(x1, x2)) → MARK(x1)
MARK(U62(x1, x2, x3)) → MARK(x1)
MARK(U52(x1, x2)) → MARK(x1)
MARK(U21(x1, x2)) → MARK(x1)
PLUSACTIVE(N, 0) → U51ACTIVE(isNatActive(N), N)
MARK(U23(x1)) → MARK(x1)
U51ACTIVE(tt, N) → U52ACTIVE(isNatKindActive(N), N)
MARK(U51(x1, x2)) → MARK(x1)
U64ACTIVE(tt, M, N) → PLUSACTIVE(mark(N), mark(M))
MARK(U64(x1, x2, x3)) → MARK(x1)
MARK(U63(x1, x2, x3)) → MARK(x1)
MARK(U61(x1, x2, x3)) → MARK(x1)
MARK(U16(x1)) → MARK(x1)
MARK(U15(x1, x2)) → MARK(x1)
MARK(U13(x1, x2, x3)) → MARK(x1)
MARK(U41(x1)) → MARK(x1)
U63ACTIVE(tt, M, N) → U64ACTIVE(isNatKindActive(N), M, N)
U62ACTIVE(tt, M, N) → U63ACTIVE(isNatActive(N), M, N)
MARK(U51(x1, x2)) → U51ACTIVE(mark(x1), x2)
MARK(s(x1)) → MARK(x1)
U52ACTIVE(tt, N) → MARK(N)
MARK(U32(x1)) → MARK(x1)
U64ACTIVE(tt, M, N) → MARK(M)
MARK(U31(x1, x2)) → MARK(x1)
PLUSACTIVE(N, s(M)) → U61ACTIVE(isNatActive(M), M, N)
MARK(U62(x1, x2, x3)) → U62ACTIVE(mark(x1), x2, x3)
MARK(U61(x1, x2, x3)) → U61ACTIVE(mark(x1), x2, x3)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)
MARK(plus(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(U11(x1, x2, x3)) → U11Active(mark(x1), x2, x3)
U11Active(x1, x2, x3) → U11(x1, x2, x3)
mark(U12(x1, x2, x3)) → U12Active(mark(x1), x2, x3)
U12Active(x1, x2, x3) → U12(x1, x2, x3)
mark(U13(x1, x2, x3)) → U13Active(mark(x1), x2, x3)
U13Active(x1, x2, x3) → U13(x1, x2, x3)
mark(U14(x1, x2, x3)) → U14Active(mark(x1), x2, x3)
U14Active(x1, x2, x3) → U14(x1, x2, x3)
mark(U15(x1, x2)) → U15Active(mark(x1), x2)
U15Active(x1, x2) → U15(x1, x2)
mark(U16(x1)) → U16Active(mark(x1))
U16Active(x1) → U16(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1, x2)) → U22Active(mark(x1), x2)
U22Active(x1, x2) → U22(x1, x2)
mark(U23(x1)) → U23Active(mark(x1))
U23Active(x1) → U23(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1)) → U41Active(mark(x1))
U41Active(x1) → U41(x1)
mark(U51(x1, x2)) → U51Active(mark(x1), x2)
U51Active(x1, x2) → U51(x1, x2)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U61(x1, x2, x3)) → U61Active(mark(x1), x2, x3)
U61Active(x1, x2, x3) → U61(x1, x2, x3)
mark(U62(x1, x2, x3)) → U62Active(mark(x1), x2, x3)
U62Active(x1, x2, x3) → U62(x1, x2, x3)
mark(U63(x1, x2, x3)) → U63Active(mark(x1), x2, x3)
U63Active(x1, x2, x3) → U63(x1, x2, x3)
mark(U64(x1, x2, x3)) → U64Active(mark(x1), x2, x3)
U64Active(x1, x2, x3) → U64(x1, x2, x3)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(plus(x1, x2)) → plusActive(mark(x1), mark(x2))
plusActive(x1, x2) → plus(x1, x2)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(0) → 0
U11Active(tt, V1, V2) → U12Active(isNatKindActive(V1), V1, V2)
U12Active(tt, V1, V2) → U13Active(isNatKindActive(V2), V1, V2)
U13Active(tt, V1, V2) → U14Active(isNatKindActive(V2), V1, V2)
U14Active(tt, V1, V2) → U15Active(isNatActive(V1), V2)
U15Active(tt, V2) → U16Active(isNatActive(V2))
U16Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatKindActive(V1), V1)
U22Active(tt, V1) → U23Active(isNatActive(V1))
U23Active(tt) → tt
U31Active(tt, V2) → U32Active(isNatKindActive(V2))
U32Active(tt) → tt
U41Active(tt) → tt
U51Active(tt, N) → U52Active(isNatKindActive(N), N)
U52Active(tt, N) → mark(N)
U61Active(tt, M, N) → U62Active(isNatKindActive(M), M, N)
U62Active(tt, M, N) → U63Active(isNatActive(N), M, N)
U63Active(tt, M, N) → U64Active(isNatKindActive(N), M, N)
U64Active(tt, M, N) → s(plusActive(mark(N), mark(M)))
isNatActive(0) → tt
isNatActive(plus(V1, V2)) → U11Active(isNatKindActive(V1), V1, V2)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatKindActive(0) → tt
isNatKindActive(plus(V1, V2)) → U31Active(isNatKindActive(V1), V2)
isNatKindActive(s(V1)) → U41Active(isNatKindActive(V1))
plusActive(N, 0) → U51Active(isNatActive(N), N)
plusActive(N, s(M)) → U61Active(isNatActive(M), M, N)

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.

U61ACTIVE(tt, M, N) → U62ACTIVE(isNatKindActive(M), M, N)
U51ACTIVE(tt, N) → U52ACTIVE(isNatKindActive(N), N)
MARK(s(x1)) → MARK(x1)
MARK(U62(x1, x2, x3)) → U62ACTIVE(mark(x1), x2, x3)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)

The remaining pairs can at least be oriented weakly.

MARK(U12(x1, x2, x3)) → MARK(x1)
U64ACTIVE(tt, M, N) → MARK(N)
MARK(plus(x1, x2)) → PLUSACTIVE(mark(x1), mark(x2))
MARK(U63(x1, x2, x3)) → U63ACTIVE(mark(x1), x2, x3)
MARK(U14(x1, x2, x3)) → MARK(x1)
MARK(plus(x1, x2)) → MARK(x2)
MARK(U64(x1, x2, x3)) → U64ACTIVE(mark(x1), x2, x3)
MARK(U11(x1, x2, x3)) → MARK(x1)
MARK(U22(x1, x2)) → MARK(x1)
MARK(U62(x1, x2, x3)) → MARK(x1)
MARK(U52(x1, x2)) → MARK(x1)
MARK(U21(x1, x2)) → MARK(x1)
PLUSACTIVE(N, 0) → U51ACTIVE(isNatActive(N), N)
MARK(U23(x1)) → MARK(x1)
MARK(U51(x1, x2)) → MARK(x1)
U64ACTIVE(tt, M, N) → PLUSACTIVE(mark(N), mark(M))
MARK(U64(x1, x2, x3)) → MARK(x1)
MARK(U63(x1, x2, x3)) → MARK(x1)
MARK(U61(x1, x2, x3)) → MARK(x1)
MARK(U16(x1)) → MARK(x1)
MARK(U15(x1, x2)) → MARK(x1)
MARK(U13(x1, x2, x3)) → MARK(x1)
MARK(U41(x1)) → MARK(x1)
U63ACTIVE(tt, M, N) → U64ACTIVE(isNatKindActive(N), M, N)
U62ACTIVE(tt, M, N) → U63ACTIVE(isNatActive(N), M, N)
MARK(U51(x1, x2)) → U51ACTIVE(mark(x1), x2)
U52ACTIVE(tt, N) → MARK(N)
MARK(U32(x1)) → MARK(x1)
U64ACTIVE(tt, M, N) → MARK(M)
MARK(U31(x1, x2)) → MARK(x1)
PLUSACTIVE(N, s(M)) → U61ACTIVE(isNatActive(M), M, N)
MARK(U61(x1, x2, x3)) → U61ACTIVE(mark(x1), x2, x3)
MARK(plus(x1, x2)) → MARK(x1)

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(MARK(x₁)) = 1 + x₁
POL(PLUSACTIVE(x₁, x₂)) = 1 + x₁ + x₂
POL(U11(x₁, x₂, x₃)) = x₁
POL(U11Active(x₁, x₂, x₃)) = x₁
POL(U12(x₁, x₂, x₃)) = x₁
POL(U12Active(x₁, x₂, x₃)) = x₁
POL(U13(x₁, x₂, x₃)) = x₁
POL(U13Active(x₁, x₂, x₃)) = x₁
POL(U14(x₁, x₂, x₃)) = x₁
POL(U14Active(x₁, x₂, x₃)) = x₁
POL(U15(x₁, x₂)) = x₁
POL(U15Active(x₁, x₂)) = x₁
POL(U16(x₁)) = x₁
POL(U16Active(x₁)) = x₁
POL(U21(x₁, x₂)) = x₁
POL(U21Active(x₁, x₂)) = x₁
POL(U22(x₁, x₂)) = x₁
POL(U22Active(x₁, x₂)) = x₁
POL(U23(x₁)) = x₁
POL(U23Active(x₁)) = x₁
POL(U31(x₁, x₂)) = x₁
POL(U31Active(x₁, x₂)) = x₁
POL(U32(x₁)) = x₁
POL(U32Active(x₁)) = x₁
POL(U41(x₁)) = x₁
POL(U41Active(x₁)) = x₁
POL(U51(x₁, x₂)) = x₁ + x₂
POL(U51ACTIVE(x₁, x₂)) = 1 + x₁ + x₂
POL(U51Active(x₁, x₂)) = x₁ + x₂
POL(U52(x₁, x₂)) = x₁ + x₂
POL(U52ACTIVE(x₁, x₂)) = x₁ + x₂
POL(U52Active(x₁, x₂)) = x₁ + x₂
POL(U61(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U61ACTIVE(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(U61Active(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U62(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U62ACTIVE(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U62Active(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U63(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U63ACTIVE(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U63Active(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U64(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U64ACTIVE(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U64Active(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(isNat(x₁)) = 1
POL(isNatActive(x₁)) = 1
POL(isNatKind(x₁)) = 1
POL(isNatKindActive(x₁)) = 1
POL(mark(x₁)) = x₁
POL(plus(x₁, x₂)) = x₁ + x₂
POL(plusActive(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = 1 + x₁
POL(tt) = 1

The following usable rules [17] were oriented:

U62Active(tt, M, N) → U63Active(isNatActive(N), M, N)
U32Active(tt) → tt
mark(U61(x1, x2, x3)) → U61Active(mark(x1), x2, x3)
mark(U14(x1, x2, x3)) → U14Active(mark(x1), x2, x3)
U14Active(tt, V1, V2) → U15Active(isNatActive(V1), V2)
mark(U23(x1)) → U23Active(mark(x1))
U16Active(x1) → U16(x1)
U52Active(x1, x2) → U52(x1, x2)
U13Active(tt, V1, V2) → U14Active(isNatKindActive(V2), V1, V2)
U12Active(tt, V1, V2) → U13Active(isNatKindActive(V2), V1, V2)
mark(U62(x1, x2, x3)) → U62Active(mark(x1), x2, x3)
U51Active(x1, x2) → U51(x1, x2)
mark(0) → 0
U11Active(x1, x2, x3) → U11(x1, x2, x3)
U63Active(x1, x2, x3) → U63(x1, x2, x3)
mark(U12(x1, x2, x3)) → U12Active(mark(x1), x2, x3)
mark(U64(x1, x2, x3)) → U64Active(mark(x1), x2, x3)
isNatKindActive(0) → tt
U41Active(x1) → U41(x1)
U14Active(x1, x2, x3) → U14(x1, x2, x3)
U61Active(tt, M, N) → U62Active(isNatKindActive(M), M, N)
isNatActive(plus(V1, V2)) → U11Active(isNatKindActive(V1), V1, V2)
U64Active(x1, x2, x3) → U64(x1, x2, x3)
U51Active(tt, N) → U52Active(isNatKindActive(N), N)
plusActive(N, 0) → U51Active(isNatActive(N), N)
mark(plus(x1, x2)) → plusActive(mark(x1), mark(x2))
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
mark(U51(x1, x2)) → U51Active(mark(x1), x2)
U52Active(tt, N) → mark(N)
mark(U13(x1, x2, x3)) → U13Active(mark(x1), x2, x3)
U23Active(tt) → tt
U11Active(tt, V1, V2) → U12Active(isNatKindActive(V1), V1, V2)
U31Active(tt, V2) → U32Active(isNatKindActive(V2))
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U13Active(x1, x2, x3) → U13(x1, x2, x3)
U61Active(x1, x2, x3) → U61(x1, x2, x3)
mark(isNatKind(x1)) → isNatKindActive(x1)
plusActive(N, s(M)) → U61Active(isNatActive(M), M, N)
U15Active(tt, V2) → U16Active(isNatActive(V2))
U31Active(x1, x2) → U31(x1, x2)
U12Active(x1, x2, x3) → U12(x1, x2, x3)
isNatActive(0) → tt
U22Active(tt, V1) → U23Active(isNatActive(V1))
mark(U32(x1)) → U32Active(mark(x1))
isNatKindActive(x1) → isNatKind(x1)
isNatKindActive(plus(V1, V2)) → U31Active(isNatKindActive(V1), V2)
plusActive(x1, x2) → plus(x1, x2)
mark(U15(x1, x2)) → U15Active(mark(x1), x2)
mark(isNat(x1)) → isNatActive(x1)
U15Active(x1, x2) → U15(x1, x2)
mark(U41(x1)) → U41Active(mark(x1))
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
U16Active(tt) → tt
mark(s(x1)) → s(mark(x1))
U23Active(x1) → U23(x1)
U21Active(tt, V1) → U22Active(isNatKindActive(V1), V1)
mark(U63(x1, x2, x3)) → U63Active(mark(x1), x2, x3)
mark(tt) → tt
mark(U16(x1)) → U16Active(mark(x1))
U22Active(x1, x2) → U22(x1, x2)
mark(U11(x1, x2, x3)) → U11Active(mark(x1), x2, x3)
U41Active(tt) → tt
U62Active(x1, x2, x3) → U62(x1, x2, x3)
U32Active(x1) → U32(x1)
isNatKindActive(s(V1)) → U41Active(isNatKindActive(V1))
mark(U22(x1, x2)) → U22Active(mark(x1), x2)
U64Active(tt, M, N) → s(plusActive(mark(N), mark(M)))
isNatActive(x1) → isNat(x1)
U63Active(tt, M, N) → U64Active(isNatKindActive(N), M, N)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)

↳ CSR

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ DependencyGraphProof

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

MARK(U12(x1, x2, x3)) → MARK(x1)
U64ACTIVE(tt, M, N) → MARK(N)
MARK(U14(x1, x2, x3)) → MARK(x1)
MARK(U63(x1, x2, x3)) → U63ACTIVE(mark(x1), x2, x3)
MARK(plus(x1, x2)) → PLUSACTIVE(mark(x1), mark(x2))
MARK(U64(x1, x2, x3)) → U64ACTIVE(mark(x1), x2, x3)
MARK(plus(x1, x2)) → MARK(x2)
MARK(U11(x1, x2, x3)) → MARK(x1)
MARK(U22(x1, x2)) → MARK(x1)
MARK(U52(x1, x2)) → MARK(x1)
MARK(U62(x1, x2, x3)) → MARK(x1)
MARK(U21(x1, x2)) → MARK(x1)
PLUSACTIVE(N, 0) → U51ACTIVE(isNatActive(N), N)
MARK(U23(x1)) → MARK(x1)
MARK(U51(x1, x2)) → MARK(x1)
U64ACTIVE(tt, M, N) → PLUSACTIVE(mark(N), mark(M))
MARK(U64(x1, x2, x3)) → MARK(x1)
MARK(U63(x1, x2, x3)) → MARK(x1)
MARK(U61(x1, x2, x3)) → MARK(x1)
MARK(U16(x1)) → MARK(x1)
MARK(U15(x1, x2)) → MARK(x1)
MARK(U13(x1, x2, x3)) → MARK(x1)
MARK(U41(x1)) → MARK(x1)
U63ACTIVE(tt, M, N) → U64ACTIVE(isNatKindActive(N), M, N)
U62ACTIVE(tt, M, N) → U63ACTIVE(isNatActive(N), M, N)
MARK(U51(x1, x2)) → U51ACTIVE(mark(x1), x2)
U52ACTIVE(tt, N) → MARK(N)
MARK(U32(x1)) → MARK(x1)
MARK(U31(x1, x2)) → MARK(x1)
U64ACTIVE(tt, M, N) → MARK(M)
PLUSACTIVE(N, s(M)) → U61ACTIVE(isNatActive(M), M, N)
MARK(U61(x1, x2, x3)) → U61ACTIVE(mark(x1), x2, x3)
MARK(plus(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(U11(x1, x2, x3)) → U11Active(mark(x1), x2, x3)
U11Active(x1, x2, x3) → U11(x1, x2, x3)
mark(U12(x1, x2, x3)) → U12Active(mark(x1), x2, x3)
U12Active(x1, x2, x3) → U12(x1, x2, x3)
mark(U13(x1, x2, x3)) → U13Active(mark(x1), x2, x3)
U13Active(x1, x2, x3) → U13(x1, x2, x3)
mark(U14(x1, x2, x3)) → U14Active(mark(x1), x2, x3)
U14Active(x1, x2, x3) → U14(x1, x2, x3)
mark(U15(x1, x2)) → U15Active(mark(x1), x2)
U15Active(x1, x2) → U15(x1, x2)
mark(U16(x1)) → U16Active(mark(x1))
U16Active(x1) → U16(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1, x2)) → U22Active(mark(x1), x2)
U22Active(x1, x2) → U22(x1, x2)
mark(U23(x1)) → U23Active(mark(x1))
U23Active(x1) → U23(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1)) → U41Active(mark(x1))
U41Active(x1) → U41(x1)
mark(U51(x1, x2)) → U51Active(mark(x1), x2)
U51Active(x1, x2) → U51(x1, x2)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U61(x1, x2, x3)) → U61Active(mark(x1), x2, x3)
U61Active(x1, x2, x3) → U61(x1, x2, x3)
mark(U62(x1, x2, x3)) → U62Active(mark(x1), x2, x3)
U62Active(x1, x2, x3) → U62(x1, x2, x3)
mark(U63(x1, x2, x3)) → U63Active(mark(x1), x2, x3)
U63Active(x1, x2, x3) → U63(x1, x2, x3)
mark(U64(x1, x2, x3)) → U64Active(mark(x1), x2, x3)
U64Active(x1, x2, x3) → U64(x1, x2, x3)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(plus(x1, x2)) → plusActive(mark(x1), mark(x2))
plusActive(x1, x2) → plus(x1, x2)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(0) → 0
U11Active(tt, V1, V2) → U12Active(isNatKindActive(V1), V1, V2)
U12Active(tt, V1, V2) → U13Active(isNatKindActive(V2), V1, V2)
U13Active(tt, V1, V2) → U14Active(isNatKindActive(V2), V1, V2)
U14Active(tt, V1, V2) → U15Active(isNatActive(V1), V2)
U15Active(tt, V2) → U16Active(isNatActive(V2))
U16Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatKindActive(V1), V1)
U22Active(tt, V1) → U23Active(isNatActive(V1))
U23Active(tt) → tt
U31Active(tt, V2) → U32Active(isNatKindActive(V2))
U32Active(tt) → tt
U41Active(tt) → tt
U51Active(tt, N) → U52Active(isNatKindActive(N), N)
U52Active(tt, N) → mark(N)
U61Active(tt, M, N) → U62Active(isNatKindActive(M), M, N)
U62Active(tt, M, N) → U63Active(isNatActive(N), M, N)
U63Active(tt, M, N) → U64Active(isNatKindActive(N), M, N)
U64Active(tt, M, N) → s(plusActive(mark(N), mark(M)))
isNatActive(0) → tt
isNatActive(plus(V1, V2)) → U11Active(isNatKindActive(V1), V1, V2)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatKindActive(0) → tt
isNatKindActive(plus(V1, V2)) → U31Active(isNatKindActive(V1), V2)
isNatKindActive(s(V1)) → U41Active(isNatKindActive(V1))
plusActive(N, 0) → U51Active(isNatActive(N), N)
plusActive(N, s(M)) → U61Active(isNatActive(M), M, N)

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

↳ CSR

  ↳ Zantema-Transformation

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

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

MARK(U12(x1, x2, x3)) → MARK(x1)
U64ACTIVE(tt, M, N) → MARK(N)
MARK(U14(x1, x2, x3)) → MARK(x1)
MARK(U63(x1, x2, x3)) → U63ACTIVE(mark(x1), x2, x3)
MARK(U64(x1, x2, x3)) → U64ACTIVE(mark(x1), x2, x3)
MARK(plus(x1, x2)) → MARK(x2)
MARK(U11(x1, x2, x3)) → MARK(x1)
MARK(U22(x1, x2)) → MARK(x1)
MARK(U52(x1, x2)) → MARK(x1)
MARK(U62(x1, x2, x3)) → MARK(x1)
MARK(U21(x1, x2)) → MARK(x1)
MARK(U23(x1)) → MARK(x1)
MARK(U51(x1, x2)) → MARK(x1)
MARK(U64(x1, x2, x3)) → MARK(x1)
MARK(U16(x1)) → MARK(x1)
MARK(U15(x1, x2)) → MARK(x1)
MARK(U61(x1, x2, x3)) → MARK(x1)
MARK(U63(x1, x2, x3)) → MARK(x1)
MARK(U13(x1, x2, x3)) → MARK(x1)
MARK(U41(x1)) → MARK(x1)
U63ACTIVE(tt, M, N) → U64ACTIVE(isNatKindActive(N), M, N)
MARK(U32(x1)) → MARK(x1)
MARK(U31(x1, x2)) → MARK(x1)
U64ACTIVE(tt, M, N) → MARK(M)
MARK(plus(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(U11(x1, x2, x3)) → U11Active(mark(x1), x2, x3)
U11Active(x1, x2, x3) → U11(x1, x2, x3)
mark(U12(x1, x2, x3)) → U12Active(mark(x1), x2, x3)
U12Active(x1, x2, x3) → U12(x1, x2, x3)
mark(U13(x1, x2, x3)) → U13Active(mark(x1), x2, x3)
U13Active(x1, x2, x3) → U13(x1, x2, x3)
mark(U14(x1, x2, x3)) → U14Active(mark(x1), x2, x3)
U14Active(x1, x2, x3) → U14(x1, x2, x3)
mark(U15(x1, x2)) → U15Active(mark(x1), x2)
U15Active(x1, x2) → U15(x1, x2)
mark(U16(x1)) → U16Active(mark(x1))
U16Active(x1) → U16(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1, x2)) → U22Active(mark(x1), x2)
U22Active(x1, x2) → U22(x1, x2)
mark(U23(x1)) → U23Active(mark(x1))
U23Active(x1) → U23(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1)) → U41Active(mark(x1))
U41Active(x1) → U41(x1)
mark(U51(x1, x2)) → U51Active(mark(x1), x2)
U51Active(x1, x2) → U51(x1, x2)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U61(x1, x2, x3)) → U61Active(mark(x1), x2, x3)
U61Active(x1, x2, x3) → U61(x1, x2, x3)
mark(U62(x1, x2, x3)) → U62Active(mark(x1), x2, x3)
U62Active(x1, x2, x3) → U62(x1, x2, x3)
mark(U63(x1, x2, x3)) → U63Active(mark(x1), x2, x3)
U63Active(x1, x2, x3) → U63(x1, x2, x3)
mark(U64(x1, x2, x3)) → U64Active(mark(x1), x2, x3)
U64Active(x1, x2, x3) → U64(x1, x2, x3)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(plus(x1, x2)) → plusActive(mark(x1), mark(x2))
plusActive(x1, x2) → plus(x1, x2)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(0) → 0
U11Active(tt, V1, V2) → U12Active(isNatKindActive(V1), V1, V2)
U12Active(tt, V1, V2) → U13Active(isNatKindActive(V2), V1, V2)
U13Active(tt, V1, V2) → U14Active(isNatKindActive(V2), V1, V2)
U14Active(tt, V1, V2) → U15Active(isNatActive(V1), V2)
U15Active(tt, V2) → U16Active(isNatActive(V2))
U16Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatKindActive(V1), V1)
U22Active(tt, V1) → U23Active(isNatActive(V1))
U23Active(tt) → tt
U31Active(tt, V2) → U32Active(isNatKindActive(V2))
U32Active(tt) → tt
U41Active(tt) → tt
U51Active(tt, N) → U52Active(isNatKindActive(N), N)
U52Active(tt, N) → mark(N)
U61Active(tt, M, N) → U62Active(isNatKindActive(M), M, N)
U62Active(tt, M, N) → U63Active(isNatActive(N), M, N)
U63Active(tt, M, N) → U64Active(isNatKindActive(N), M, N)
U64Active(tt, M, N) → s(plusActive(mark(N), mark(M)))
isNatActive(0) → tt
isNatActive(plus(V1, V2)) → U11Active(isNatKindActive(V1), V1, V2)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatKindActive(0) → tt
isNatKindActive(plus(V1, V2)) → U31Active(isNatKindActive(V1), V2)
isNatKindActive(s(V1)) → U41Active(isNatKindActive(V1))
plusActive(N, 0) → U51Active(isNatActive(N), N)
plusActive(N, s(M)) → U61Active(isNatActive(M), M, N)

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

U63ACTIVE(tt, M, N) → U64ACTIVE(isNatKindActive(N), M, N)
The graph contains the following edges 2 >= 2, 3 >= 3
MARK(U63(x1, x2, x3)) → U63ACTIVE(mark(x1), x2, x3)
The graph contains the following edges 1 > 2, 1 > 3
MARK(U64(x1, x2, x3)) → U64ACTIVE(mark(x1), x2, x3)
The graph contains the following edges 1 > 2, 1 > 3
MARK(U11(x1, x2, x3)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U12(x1, x2, x3)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U13(x1, x2, x3)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U14(x1, x2, x3)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U15(x1, x2)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U16(x1)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U21(x1, x2)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U22(x1, x2)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U23(x1)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U31(x1, x2)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U32(x1)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U41(x1)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U51(x1, x2)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U52(x1, x2)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U61(x1, x2, x3)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U62(x1, x2, x3)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U63(x1, x2, x3)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(U64(x1, x2, x3)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(plus(x1, x2)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(plus(x1, x2)) → MARK(x2)
The graph contains the following edges 1 > 1
U64ACTIVE(tt, M, N) → MARK(N)
The graph contains the following edges 3 >= 1
U64ACTIVE(tt, M, N) → MARK(M)
The graph contains the following edges 2 >= 1