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)
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
↳ CSDependencyPairsProof
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)
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
Using Improved CS-DPs we result in the following initial Q-CSDP problem.
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
U111(tt, V1, V2) → U121(isNat(V1), V2)
U111(tt, V1, V2) → ISNAT(V1)
U121(tt, V2) → U131(isNat(V2))
U121(tt, V2) → ISNAT(V2)
U211(tt, V1) → U221(isNat(V1))
U211(tt, V1) → ISNAT(V1)
U411(tt, M, N) → PLUS(N, M)
ISNAT(plus(V1, V2)) → U111(and(isNatKind(V1), isNatKind(V2)), V1, V2)
ISNAT(plus(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
ISNAT(plus(V1, V2)) → ISNATKIND(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
ISNAT(s(V1)) → ISNATKIND(V1)
ISNATKIND(plus(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
ISNATKIND(plus(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
PLUS(N, 0) → U311(and(isNat(N), isNatKind(N)), N)
PLUS(N, 0) → AND(isNat(N), isNatKind(N))
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → U411(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
PLUS(N, s(M)) → AND(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
PLUS(N, s(M)) → AND(isNat(M), isNatKind(M))
PLUS(N, s(M)) → ISNAT(M)
U311(tt, N) → N
U411(tt, M, N) → N
U411(tt, M, N) → M
AND(tt, X) → X
isNatKind(V2)
and on positions {1}
U311(tt, N) → U(N)
U411(tt, M, N) → U(N)
U411(tt, M, N) → U(M)
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatKind(V2)) → ISNATKIND(V2)
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)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDPReductionPairProof
↳ QCSDP
↳ QCSDP
U(and(x_0, x_1)) → U(x_0)
U(isNatKind(V2)) → ISNATKIND(V2)
ISNATKIND(plus(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
AND(tt, X) → U(X)
ISNATKIND(plus(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
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)
POL(0) = 1
POL(AND(x1, x2)) = x1 + x2
POL(ISNATKIND(x1)) = x1
POL(U(x1)) = x1
POL(U11(x1, x2, x3)) = 1
POL(U12(x1, x2)) = 1
POL(U13(x1)) = 1
POL(U21(x1, x2)) = 1
POL(U22(x1)) = 1
POL(U31(x1, x2)) = x2
POL(U41(x1, x2, x3)) = x2 + x3
POL(and(x1, x2)) = x1 + x2
POL(isNat(x1)) = 1
POL(isNatKind(x1)) = x1
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(tt) = 1
and(tt, X) → X
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)
U31(tt, N) → N
isNat(0) → tt
isNat(plus(V1, V2)) → U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
isNat(s(V1)) → U21(isNatKind(V1), V1)
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
U41(tt, M, N) → s(plus(N, M))
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatKind(V2)) → ISNATKIND(V2)
ISNATKIND(plus(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
ISNATKIND(plus(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDPReductionPairProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ QCSDP
↳ QCSDP
U(and(x_0, x_1)) → U(x_0)
U(isNatKind(V2)) → ISNATKIND(V2)
ISNATKIND(plus(V1, V2)) → AND(isNatKind(V1), isNatKind(V2))
ISNATKIND(plus(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
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)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDPReductionPairProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDPSubtermProof
↳ QCSDP
↳ QCSDP
↳ QCSDP
ISNATKIND(plus(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
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 following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ISNATKIND(plus(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDPReductionPairProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDPSubtermProof
↳ QCSDP
↳ PIsEmptyProof
↳ QCSDP
↳ QCSDP
↳ QCSDP
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)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDPReductionPairProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDP
↳ QCSDPSubtermProof
↳ QCSDP
↳ QCSDP
U(and(x_0, x_1)) → U(x_0)
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 following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U(and(x_0, x_1)) → U(x_0)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDPReductionPairProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDP
↳ QCSDPSubtermProof
↳ QCSDP
↳ PIsEmptyProof
↳ QCSDP
↳ QCSDP
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)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDP
↳ QCSDPReductionPairProof
↳ QCSDPReductionPairProof
↳ QCSDP
U121(tt, V2) → ISNAT(V2)
ISNAT(plus(V1, V2)) → U111(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U111(tt, V1, V2) → U121(isNat(V1), V2)
U111(tt, V1, V2) → ISNAT(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U211(tt, V1) → ISNAT(V1)
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)
POL( plus(x1, x2) ) = x1 + x2 + 1
POL( U121(x1, x2) ) = 2x2 + 1
POL( U31(x1, x2) ) = x2
POL( U41(x1, ..., x3) ) = x2 + x3 + 2
POL( U111(x1, ..., x3) ) = 2x2 + 2x3 + 1
POL( U11(x1, ..., x3) ) = 2x2 + x3 + 1
POL( U211(x1, x2) ) = 2x2 + 1
POL( U12(x1, x2) ) = max{0, -1}
POL( isNatKind(x1) ) = max{0, -1}
POL( and(x1, x2) ) = 2x2
POL( 0 ) = 0
POL( U21(x1, x2) ) = max{0, -1}
POL( ISNAT(x1) ) = 2x1 + 1
POL( U22(x1) ) = max{0, -1}
POL( tt ) = 0
POL( U13(x1) ) = 0
POL( s(x1) ) = x1 + 1
POL( isNat(x1) ) = max{0, 2x1 - 1}
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)
U31(tt, N) → N
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)
U11(tt, V1, V2) → U12(isNat(V1), V2)
U12(tt, V2) → U13(isNat(V2))
U13(tt) → tt
isNatKind(0) → tt
isNatKind(plus(V1, V2)) → and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) → isNatKind(V1)
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U41(tt, M, N) → s(plus(N, M))
ISNAT(plus(V1, V2)) → U111(and(isNatKind(V1), isNatKind(V2)), V1, V2)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U121(tt, V2) → ISNAT(V2)
U111(tt, V1, V2) → U121(isNat(V1), V2)
U111(tt, V1, V2) → ISNAT(V1)
U211(tt, V1) → ISNAT(V1)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDP
↳ QCSDPReductionPairProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ QCSDPReductionPairProof
↳ QCSDP
U121(tt, V2) → ISNAT(V2)
U111(tt, V1, V2) → U121(isNat(V1), V2)
U111(tt, V1, V2) → ISNAT(V1)
U211(tt, V1) → ISNAT(V1)
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)
POL(0) = 1
POL(ISNAT(x1)) = x1
POL(U11(x1, x2, x3)) = x3
POL(U111(x1, x2, x3)) = x2 + x3
POL(U12(x1, x2)) = x2
POL(U121(x1, x2)) = x1 + x2
POL(U13(x1)) = x1
POL(U21(x1, x2)) = x2
POL(U211(x1, x2)) = x2
POL(U22(x1)) = x1
POL(U31(x1, x2)) = x2
POL(U41(x1, x2, x3)) = x2 + x3
POL(and(x1, x2)) = x2
POL(isNat(x1)) = x1
POL(isNatKind(x1)) = 1
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(tt) = 1
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)
U31(tt, N) → N
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)
U11(tt, V1, V2) → U12(isNat(V1), V2)
U12(tt, V2) → U13(isNat(V2))
U13(tt) → tt
isNatKind(0) → tt
isNatKind(plus(V1, V2)) → and(isNatKind(V1), isNatKind(V2))
isNatKind(s(V1)) → isNatKind(V1)
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U41(tt, M, N) → s(plus(N, M))
U121(tt, V2) → ISNAT(V2)
ISNAT(plus(V1, V2)) → U111(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U111(tt, V1, V2) → U121(isNat(V1), V2)
U111(tt, V1, V2) → ISNAT(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U211(tt, V1) → ISNAT(V1)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDP
↳ QCSDPReductionPairProof
↳ QCSDPReductionPairProof
↳ QCSDP
↳ QCSDP
ISNAT(plus(V1, V2)) → U111(and(isNatKind(V1), isNatKind(V2)), V1, V2)
U111(tt, V1, V2) → U121(isNat(V1), V2)
U111(tt, V1, V2) → ISNAT(V1)
ISNAT(s(V1)) → U211(isNatKind(V1), V1)
U211(tt, V1) → ISNAT(V1)
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)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDP
↳ QCSDP
↳ QCSDPSubtermProof
PLUS(N, s(M)) → U411(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
U411(tt, M, N) → PLUS(N, M)
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 following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(N, s(M)) → U411(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
Used ordering: Combined order from the following AFS and order.
U411(tt, M, N) → PLUS(N, M)
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ AND
↳ QCSDP
↳ QCSDP
↳ QCSDP
↳ QCSDPSubtermProof
↳ QCSDP
↳ QCSDependencyGraphProof
U411(tt, M, N) → PLUS(N, M)
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)