0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 PisEmptyProof (⇔)
↳9 TRUE
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 PisEmptyProof (⇔)
↳14 TRUE
↳15 QDP
↳16 QDPOrderProof (⇔)
↳17 QDP
↳18 QDPOrderProof (⇔)
↳19 QDP
↳20 PisEmptyProof (⇔)
↳21 TRUE
↳22 QDP
↳23 QDPOrderProof (⇔)
↳24 QDP
↳25 QDPOrderProof (⇔)
↳26 QDP
↳27 PisEmptyProof (⇔)
↳28 TRUE
↳29 QDP
↳30 QDPOrderProof (⇔)
↳31 QDP
↳32 QDPOrderProof (⇔)
↳33 QDP
↳34 PisEmptyProof (⇔)
↳35 TRUE
↳36 QDP
↳37 QDPOrderProof (⇔)
↳38 QDP
↳39 QDPOrderProof (⇔)
↳40 QDP
↳41 PisEmptyProof (⇔)
↳42 TRUE
↳43 QDP
↳44 QDPOrderProof (⇔)
↳45 QDP
↳46 QDPOrderProof (⇔)
↳47 QDP
↳48 QDPOrderProof (⇔)
↳49 QDP
↳50 QDPOrderProof (⇔)
↳51 QDP
↳52 QDPOrderProof (⇔)
↳53 QDP
↳54 PisEmptyProof (⇔)
↳55 TRUE
↳56 QDP
↳57 QDPOrderProof (⇔)
↳58 QDP
↳59 QDPOrderProof (⇔)
↳60 QDP
↳61 QDPOrderProof (⇔)
↳62 QDP
↳63 QDPOrderProof (⇔)
↳64 QDP
↳65 PisEmptyProof (⇔)
↳66 TRUE
↳67 QDP
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(nats) → ADX(zeros)
ACTIVE(zeros) → CONS(0, zeros)
ACTIVE(incr(cons(X, Y))) → CONS(s(X), incr(Y))
ACTIVE(incr(cons(X, Y))) → S(X)
ACTIVE(incr(cons(X, Y))) → INCR(Y)
ACTIVE(adx(cons(X, Y))) → INCR(cons(X, adx(Y)))
ACTIVE(adx(cons(X, Y))) → CONS(X, adx(Y))
ACTIVE(adx(cons(X, Y))) → ADX(Y)
ACTIVE(adx(X)) → ADX(active(X))
ACTIVE(adx(X)) → ACTIVE(X)
ACTIVE(incr(X)) → INCR(active(X))
ACTIVE(incr(X)) → ACTIVE(X)
ACTIVE(hd(X)) → HD(active(X))
ACTIVE(hd(X)) → ACTIVE(X)
ACTIVE(tl(X)) → TL(active(X))
ACTIVE(tl(X)) → ACTIVE(X)
ADX(mark(X)) → ADX(X)
INCR(mark(X)) → INCR(X)
HD(mark(X)) → HD(X)
TL(mark(X)) → TL(X)
PROPER(adx(X)) → ADX(proper(X))
PROPER(adx(X)) → PROPER(X)
PROPER(cons(X1, X2)) → CONS(proper(X1), proper(X2))
PROPER(cons(X1, X2)) → PROPER(X1)
PROPER(cons(X1, X2)) → PROPER(X2)
PROPER(incr(X)) → INCR(proper(X))
PROPER(incr(X)) → PROPER(X)
PROPER(s(X)) → S(proper(X))
PROPER(s(X)) → PROPER(X)
PROPER(hd(X)) → HD(proper(X))
PROPER(hd(X)) → PROPER(X)
PROPER(tl(X)) → TL(proper(X))
PROPER(tl(X)) → PROPER(X)
ADX(ok(X)) → ADX(X)
CONS(ok(X1), ok(X2)) → CONS(X1, X2)
INCR(ok(X)) → INCR(X)
S(ok(X)) → S(X)
HD(ok(X)) → HD(X)
TL(ok(X)) → TL(X)
TOP(mark(X)) → TOP(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(ok(X)) → TOP(active(X))
TOP(ok(X)) → ACTIVE(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
S(ok(X)) → S(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(ok(X)) → S(X)
top > active > [nats, zeros, 0] > ok1 > mark
top > proper > [nats, zeros, 0] > ok1 > mark
ok1: [1]
active: multiset
nats: multiset
mark: []
zeros: multiset
0: multiset
proper: multiset
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
CONS(ok(X1), ok(X2)) → CONS(X1, X2)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CONS(ok(X1), ok(X2)) → CONS(X1, X2)
CONS1 > mark
[active1, proper, top] > ok1 > mark
[active1, proper, top] > [nats, zeros, 0] > mark
CONS1: [1]
ok1: [1]
active1: [1]
nats: multiset
mark: []
zeros: multiset
0: multiset
proper: multiset
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
TL(ok(X)) → TL(X)
TL(mark(X)) → TL(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TL(mark(X)) → TL(X)
active1 > zeros > [s, top]
active1 > 0 > [s, top]
active1 > incr1 > [TL1, mark1] > [s, top]
active1 > incr1 > cons2 > [s, top]
nats > [s, top]
TL1: multiset
mark1: multiset
active1: [1]
nats: multiset
zeros: multiset
cons2: [2,1]
0: multiset
incr1: multiset
s: []
top: multiset
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
TL(ok(X)) → TL(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TL(ok(X)) → TL(X)
top > active > [nats, zeros, 0] > ok1 > mark
top > proper > [nats, zeros, 0] > ok1 > mark
ok1: [1]
active: multiset
nats: multiset
mark: []
zeros: multiset
0: multiset
proper: multiset
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
HD(ok(X)) → HD(X)
HD(mark(X)) → HD(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HD(mark(X)) → HD(X)
active1 > zeros > [s, top]
active1 > 0 > [s, top]
active1 > incr1 > [HD1, mark1] > [s, top]
active1 > incr1 > cons2 > [s, top]
nats > [s, top]
HD1: multiset
mark1: multiset
active1: [1]
nats: multiset
zeros: multiset
cons2: [2,1]
0: multiset
incr1: multiset
s: []
top: multiset
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
HD(ok(X)) → HD(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HD(ok(X)) → HD(X)
top > active > [nats, zeros, 0] > ok1 > mark
top > proper > [nats, zeros, 0] > ok1 > mark
ok1: [1]
active: multiset
nats: multiset
mark: []
zeros: multiset
0: multiset
proper: multiset
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
INCR(ok(X)) → INCR(X)
INCR(mark(X)) → INCR(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
INCR(mark(X)) → INCR(X)
active1 > zeros > [s, top]
active1 > 0 > [s, top]
active1 > incr1 > [INCR1, mark1] > [s, top]
active1 > incr1 > cons2 > [s, top]
nats > [s, top]
INCR1: multiset
mark1: multiset
active1: [1]
nats: multiset
zeros: multiset
cons2: [2,1]
0: multiset
incr1: multiset
s: []
top: multiset
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
INCR(ok(X)) → INCR(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
INCR(ok(X)) → INCR(X)
top > active > [nats, zeros, 0] > ok1 > mark
top > proper > [nats, zeros, 0] > ok1 > mark
ok1: [1]
active: multiset
nats: multiset
mark: []
zeros: multiset
0: multiset
proper: multiset
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ADX(ok(X)) → ADX(X)
ADX(mark(X)) → ADX(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ADX(mark(X)) → ADX(X)
active1 > zeros > [s, top]
active1 > 0 > [s, top]
active1 > incr1 > [ADX1, mark1] > [s, top]
active1 > incr1 > cons2 > [s, top]
nats > [s, top]
ADX1: multiset
mark1: multiset
active1: [1]
nats: multiset
zeros: multiset
cons2: [2,1]
0: multiset
incr1: multiset
s: []
top: multiset
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ADX(ok(X)) → ADX(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ADX(ok(X)) → ADX(X)
top > active > [nats, zeros, 0] > ok1 > mark
top > proper > [nats, zeros, 0] > ok1 > mark
ok1: [1]
active: multiset
nats: multiset
mark: []
zeros: multiset
0: multiset
proper: multiset
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(cons(X1, X2)) → PROPER(X1)
PROPER(adx(X)) → PROPER(X)
PROPER(cons(X1, X2)) → PROPER(X2)
PROPER(incr(X)) → PROPER(X)
PROPER(s(X)) → PROPER(X)
PROPER(hd(X)) → PROPER(X)
PROPER(tl(X)) → PROPER(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(cons(X1, X2)) → PROPER(X1)
PROPER(cons(X1, X2)) → PROPER(X2)
PROPER(s(X)) → PROPER(X)
active > cons2 > PROPER1 > [s1, top]
active > cons2 > [nats, mark] > [s1, top]
zeros > cons2 > PROPER1 > [s1, top]
zeros > cons2 > [nats, mark] > [s1, top]
zeros > 0 > [s1, top]
PROPER1: multiset
cons2: multiset
s1: [1]
active: []
nats: multiset
mark: multiset
zeros: multiset
0: multiset
top: multiset
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(adx(X)) → PROPER(X)
PROPER(incr(X)) → PROPER(X)
PROPER(hd(X)) → PROPER(X)
PROPER(tl(X)) → PROPER(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(adx(X)) → PROPER(X)
PROPER1 > [s, top]
[adx1, active1] > zeros > [s, top]
[adx1, active1] > cons2 > [s, top]
[adx1, active1] > 0 > [s, top]
nats > zeros > [s, top]
PROPER1: [1]
adx1: multiset
active1: multiset
nats: multiset
zeros: multiset
cons2: multiset
0: multiset
s: []
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(incr(X)) → PROPER(X)
PROPER(hd(X)) → PROPER(X)
PROPER(tl(X)) → PROPER(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(hd(X)) → PROPER(X)
[nats, zeros] > mark > [PROPER1, hd1]
[nats, zeros] > ok > [PROPER1, hd1]
cons > mark > [PROPER1, hd1]
cons > s > ok > [PROPER1, hd1]
0 > ok > [PROPER1, hd1]
top > [PROPER1, hd1]
PROPER1: multiset
hd1: [1]
nats: multiset
mark: multiset
zeros: multiset
cons: []
0: multiset
s: []
ok: []
top: multiset
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(incr(X)) → PROPER(X)
PROPER(tl(X)) → PROPER(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(incr(X)) → PROPER(X)
PROPER1 > top
active1 > adx > [incr1, cons] > [mark, zeros] > top
active1 > 0 > top
active1 > hd1 > [mark, zeros] > top
nats > [mark, zeros] > top
PROPER1: [1]
incr1: [1]
active1: multiset
nats: multiset
mark: []
adx: []
zeros: multiset
cons: multiset
0: multiset
hd1: multiset
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(tl(X)) → PROPER(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(tl(X)) → PROPER(X)
PROPER1 > [nats, zeros, cons1, 0, ok]
hd > [tl1, active1, incr] > mark > [nats, zeros, cons1, 0, ok]
hd > [tl1, active1, incr] > s > [nats, zeros, cons1, 0, ok]
top > [nats, zeros, cons1, 0, ok]
PROPER1: multiset
tl1: [1]
active1: [1]
nats: multiset
mark: []
zeros: multiset
cons1: [1]
0: multiset
incr: multiset
s: []
hd: multiset
ok: multiset
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(incr(X)) → ACTIVE(X)
ACTIVE(adx(X)) → ACTIVE(X)
ACTIVE(hd(X)) → ACTIVE(X)
ACTIVE(tl(X)) → ACTIVE(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(incr(X)) → ACTIVE(X)
[ACTIVE1, incr1, proper1] > [zeros, 0] > [nats, ok] > [mark, top]
[ACTIVE1, incr1, proper1] > cons > [nats, ok] > [mark, top]
[ACTIVE1, incr1, proper1] > s > [nats, ok] > [mark, top]
ACTIVE1: multiset
incr1: [1]
nats: multiset
mark: []
zeros: multiset
cons: multiset
0: multiset
s: []
proper1: [1]
ok: multiset
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(adx(X)) → ACTIVE(X)
ACTIVE(hd(X)) → ACTIVE(X)
ACTIVE(tl(X)) → ACTIVE(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(adx(X)) → ACTIVE(X)
zeros > [nats, mark] > top > [adx1, active1] > ACTIVE1
cons2 > [nats, mark] > top > [adx1, active1] > ACTIVE1
0 > ACTIVE1
ACTIVE1: [1]
adx1: [1]
active1: [1]
nats: multiset
mark: []
zeros: multiset
cons2: [1,2]
0: multiset
top: multiset
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(hd(X)) → ACTIVE(X)
ACTIVE(tl(X)) → ACTIVE(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(hd(X)) → ACTIVE(X)
[hd1, active1] > ACTIVE1
[hd1, active1] > [nats, zeros] > cons
[hd1, active1] > [mark, adx, incr, top] > cons
[hd1, active1] > [mark, adx, incr, top] > s1
[hd1, active1] > 0
ACTIVE1: multiset
hd1: multiset
active1: multiset
nats: multiset
mark: []
adx: []
zeros: multiset
cons: multiset
0: multiset
incr: []
s1: [1]
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(tl(X)) → ACTIVE(X)
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(tl(X)) → ACTIVE(X)
ACTIVE1 > [nats, zeros, cons1, 0, ok]
hd > [tl1, active1, incr] > mark > [nats, zeros, cons1, 0, ok]
hd > [tl1, active1, incr] > s > [nats, zeros, cons1, 0, ok]
top > [nats, zeros, cons1, 0, ok]
ACTIVE1: multiset
tl1: [1]
active1: [1]
nats: multiset
mark: []
zeros: multiset
cons1: [1]
0: multiset
incr: multiset
s: []
hd: multiset
ok: multiset
top: []
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
TOP(ok(X)) → TOP(active(X))
TOP(mark(X)) → TOP(proper(X))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(incr(cons(X, Y))) → mark(cons(s(X), incr(Y)))
active(adx(cons(X, Y))) → mark(incr(cons(X, adx(Y))))
active(hd(cons(X, Y))) → mark(X)
active(tl(cons(X, Y))) → mark(Y)
active(adx(X)) → adx(active(X))
active(incr(X)) → incr(active(X))
active(hd(X)) → hd(active(X))
active(tl(X)) → tl(active(X))
adx(mark(X)) → mark(adx(X))
incr(mark(X)) → mark(incr(X))
hd(mark(X)) → mark(hd(X))
tl(mark(X)) → mark(tl(X))
proper(nats) → ok(nats)
proper(adx(X)) → adx(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(incr(X)) → incr(proper(X))
proper(s(X)) → s(proper(X))
proper(hd(X)) → hd(proper(X))
proper(tl(X)) → tl(proper(X))
adx(ok(X)) → ok(adx(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
incr(ok(X)) → ok(incr(X))
s(ok(X)) → ok(s(X))
hd(ok(X)) → ok(hd(X))
tl(ok(X)) → ok(tl(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))