0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 QDPOrderProof (⇔)
↳6 QDP
↳7 DependencyGraphProof (⇔)
↳8 AND
↳9 QDP
↳10 QDPOrderProof (⇔)
↳11 QDP
↳12 DependencyGraphProof (⇔)
↳13 TRUE
↳14 QDP
↳15 QDPOrderProof (⇔)
↳16 QDP
↳17 DependencyGraphProof (⇔)
↳18 AND
↳19 QDP
↳20 QDPOrderProof (⇔)
↳21 QDP
↳22 PisEmptyProof (⇔)
↳23 TRUE
↳24 QDP
↳25 QDPOrderProof (⇔)
↳26 QDP
↳27 PisEmptyProof (⇔)
↳28 TRUE
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
U111(tt, N) → ACTIVATE(N)
U211(tt, M, N) → S(plus(activate(N), activate(M)))
U211(tt, M, N) → PLUS(activate(N), activate(M))
U211(tt, M, N) → ACTIVATE(N)
U211(tt, M, N) → ACTIVATE(M)
AND(tt, X) → ACTIVATE(X)
ISNAT(n__plus(V1, V2)) → AND(isNat(activate(V1)), n__isNat(activate(V2)))
ISNAT(n__plus(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__plus(V1, V2)) → ACTIVATE(V1)
ISNAT(n__plus(V1, V2)) → ACTIVATE(V2)
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
PLUS(N, 0) → U111(isNat(N), N)
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → U211(and(isNat(M), n__isNat(N)), M, N)
PLUS(N, s(M)) → AND(isNat(M), n__isNat(N))
PLUS(N, s(M)) → ISNAT(M)
ACTIVATE(n__0) → 01
ACTIVATE(n__plus(X1, X2)) → PLUS(activate(X1), activate(X2))
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__isNat(X)) → ISNAT(X)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__s(X)) → ACTIVATE(X)
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
ACTIVATE(n__plus(X1, X2)) → PLUS(activate(X1), activate(X2))
PLUS(N, 0) → U111(isNat(N), N)
U111(tt, N) → ACTIVATE(N)
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__isNat(X)) → ISNAT(X)
ISNAT(n__plus(V1, V2)) → AND(isNat(activate(V1)), n__isNat(activate(V2)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ISNAT(n__plus(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__plus(V1, V2)) → ACTIVATE(V1)
ISNAT(n__plus(V1, V2)) → ACTIVATE(V2)
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → U211(and(isNat(M), n__isNat(N)), M, N)
U211(tt, M, N) → PLUS(activate(N), activate(M))
PLUS(N, s(M)) → AND(isNat(M), n__isNat(N))
PLUS(N, s(M)) → ISNAT(M)
U211(tt, M, N) → ACTIVATE(N)
U211(tt, M, N) → ACTIVATE(M)
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__plus(X1, X2)) → PLUS(activate(X1), activate(X2))
PLUS(N, 0) → U111(isNat(N), N)
U111(tt, N) → ACTIVATE(N)
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X2)
ISNAT(n__plus(V1, V2)) → AND(isNat(activate(V1)), n__isNat(activate(V2)))
ISNAT(n__plus(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__plus(V1, V2)) → ACTIVATE(V1)
ISNAT(n__plus(V1, V2)) → ACTIVATE(V2)
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → AND(isNat(M), n__isNat(N))
PLUS(N, s(M)) → ISNAT(M)
U211(tt, M, N) → ACTIVATE(N)
U211(tt, M, N) → ACTIVATE(M)
[nplus2, U212, plus2] > [PLUS2, U11^11, U21^12] > U111
[0, n0] > [PLUS2, U11^11, U21^12] > U111
[0, n0] > tt > U111
nplus2: multiset
PLUS2: multiset
0: multiset
U11^11: multiset
tt: multiset
U21^12: multiset
U111: [1]
U212: multiset
plus2: multiset
n0: multiset
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
ACTIVATE(n__isNat(X)) → ISNAT(X)
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
PLUS(N, s(M)) → U211(and(isNat(M), n__isNat(N)), M, N)
U211(tt, M, N) → PLUS(activate(N), activate(M))
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
U211(tt, M, N) → PLUS(activate(N), activate(M))
PLUS(N, s(M)) → U211(and(isNat(M), n__isNat(N)), M, N)
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U211(tt, M, N) → PLUS(activate(N), activate(M))
[U213, plus2, nplus2] > [U21^11, tt, s1, and1, isNat1, nisNat1, U111, ns1]
[n0, 0] > [U21^11, tt, s1, and1, isNat1, nisNat1, U111, ns1]
U21^11: multiset
tt: multiset
s1: multiset
and1: multiset
isNat1: multiset
nisNat1: multiset
U111: multiset
U213: [2,3,1]
plus2: [2,1]
n0: multiset
nplus2: [2,1]
ns1: multiset
0: multiset
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
PLUS(N, s(M)) → U211(and(isNat(M), n__isNat(N)), M, N)
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__isNat(X)) → ISNAT(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__isNat(X)) → ISNAT(X)
[n0, 0] > [ISNAT1, ACTIVATE1, nisNat1, U111, tt, U212, plus2, and1, isNat1, nplus2]
ISNAT1: [1]
ACTIVATE1: [1]
nisNat1: multiset
U111: multiset
tt: multiset
U212: multiset
plus2: multiset
and1: multiset
isNat1: multiset
n0: multiset
nplus2: multiset
0: multiset
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
ACTIVATE(n__s(X)) → ACTIVATE(X)
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__s(X)) → ACTIVATE(X)
[U213, plus2, nplus2] > [ns1, s1] > [U111, tt, and1, isNat1, nisNat1]
[n0, 0] > [U111, tt, and1, isNat1, nisNat1]
ns1: multiset
U111: multiset
tt: multiset
U213: [3,2,1]
s1: multiset
plus2: [1,2]
and1: multiset
isNat1: multiset
n0: multiset
nplus2: [1,2]
nisNat1: multiset
0: multiset
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
ISNAT(n__s(V1)) → ISNAT(activate(V1))
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ISNAT(n__s(V1)) → ISNAT(activate(V1))
[U213, plus2, nplus2] > [ns1, s1] > [U111, tt, and1, isNat1, nisNat1]
[n0, 0] > [U111, tt, and1, isNat1, nisNat1]
ns1: multiset
U111: multiset
tt: multiset
U213: [3,2,1]
s1: multiset
plus2: [1,2]
and1: multiset
isNat1: multiset
n0: multiset
nplus2: [1,2]
nisNat1: multiset
0: multiset
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X