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 PisEmptyProof (⇔)
↳19 TRUE
↳20 QDP
↳21 QDPOrderProof (⇔)
↳22 QDP
↳23 QDPOrderProof (⇔)
↳24 QDP
↳25 PisEmptyProof (⇔)
↳26 TRUE
↳27 QDP
↳28 QDPOrderProof (⇔)
↳29 QDP
↳30 QDPOrderProof (⇔)
↳31 QDP
↳32 PisEmptyProof (⇔)
↳33 TRUE
↳34 QDP
↳35 QDPOrderProof (⇔)
↳36 QDP
↳37 QDPOrderProof (⇔)
↳38 QDP
↳39 PisEmptyProof (⇔)
↳40 TRUE
↳41 QDP
↳42 QDPOrderProof (⇔)
↳43 QDP
↳44 QDPOrderProof (⇔)
↳45 QDP
↳46 PisEmptyProof (⇔)
↳47 TRUE
↳48 QDP
↳49 QDPOrderProof (⇔)
↳50 QDP
↳51 QDPOrderProof (⇔)
↳52 QDP
↳53 PisEmptyProof (⇔)
↳54 TRUE
↳55 QDP
↳56 QDPOrderProof (⇔)
↳57 QDP
↳58 QDPOrderProof (⇔)
↳59 QDP
↳60 PisEmptyProof (⇔)
↳61 TRUE
↳62 QDP
↳63 QDPOrderProof (⇔)
↳64 QDP
↳65 QDPOrderProof (⇔)
↳66 QDP
↳67 PisEmptyProof (⇔)
↳68 TRUE
↳69 QDP
↳70 QDPOrderProof (⇔)
↳71 QDP
↳72 QDPOrderProof (⇔)
↳73 QDP
↳74 PisEmptyProof (⇔)
↳75 TRUE
↳76 QDP
↳77 QDPOrderProof (⇔)
↳78 QDP
↳79 QDPOrderProof (⇔)
↳80 QDP
↳81 QDPOrderProof (⇔)
↳82 QDP
↳83 QDPOrderProof (⇔)
↳84 QDP
↳85 PisEmptyProof (⇔)
↳86 TRUE
↳87 QDP
↳88 QDPOrderProof (⇔)
↳89 QDP
↳90 QDPOrderProof (⇔)
↳91 QDP
↳92 QDPOrderProof (⇔)
↳93 QDP
↳94 PisEmptyProof (⇔)
↳95 TRUE
↳96 QDP
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(dbl(s(X))) → S(s(dbl(X)))
ACTIVE(dbl(s(X))) → S(dbl(X))
ACTIVE(dbl(s(X))) → DBL(X)
ACTIVE(dbls(cons(X, Y))) → CONS(dbl(X), dbls(Y))
ACTIVE(dbls(cons(X, Y))) → DBL(X)
ACTIVE(dbls(cons(X, Y))) → DBLS(Y)
ACTIVE(sel(s(X), cons(Y, Z))) → SEL(X, Z)
ACTIVE(indx(cons(X, Y), Z)) → CONS(sel(X, Z), indx(Y, Z))
ACTIVE(indx(cons(X, Y), Z)) → SEL(X, Z)
ACTIVE(indx(cons(X, Y), Z)) → INDX(Y, Z)
ACTIVE(from(X)) → CONS(X, from(s(X)))
ACTIVE(from(X)) → FROM(s(X))
ACTIVE(from(X)) → S(X)
ACTIVE(dbl1(s(X))) → S1(s1(dbl1(X)))
ACTIVE(dbl1(s(X))) → S1(dbl1(X))
ACTIVE(dbl1(s(X))) → DBL1(X)
ACTIVE(sel1(s(X), cons(Y, Z))) → SEL1(X, Z)
ACTIVE(quote(s(X))) → S1(quote(X))
ACTIVE(quote(s(X))) → QUOTE(X)
ACTIVE(quote(dbl(X))) → DBL1(X)
ACTIVE(quote(sel(X, Y))) → SEL1(X, Y)
ACTIVE(dbl(X)) → DBL(active(X))
ACTIVE(dbl(X)) → ACTIVE(X)
ACTIVE(dbls(X)) → DBLS(active(X))
ACTIVE(dbls(X)) → ACTIVE(X)
ACTIVE(sel(X1, X2)) → SEL(active(X1), X2)
ACTIVE(sel(X1, X2)) → ACTIVE(X1)
ACTIVE(sel(X1, X2)) → SEL(X1, active(X2))
ACTIVE(sel(X1, X2)) → ACTIVE(X2)
ACTIVE(indx(X1, X2)) → INDX(active(X1), X2)
ACTIVE(indx(X1, X2)) → ACTIVE(X1)
ACTIVE(dbl1(X)) → DBL1(active(X))
ACTIVE(dbl1(X)) → ACTIVE(X)
ACTIVE(s1(X)) → S1(active(X))
ACTIVE(s1(X)) → ACTIVE(X)
ACTIVE(sel1(X1, X2)) → SEL1(active(X1), X2)
ACTIVE(sel1(X1, X2)) → ACTIVE(X1)
ACTIVE(sel1(X1, X2)) → SEL1(X1, active(X2))
ACTIVE(sel1(X1, X2)) → ACTIVE(X2)
ACTIVE(quote(X)) → QUOTE(active(X))
ACTIVE(quote(X)) → ACTIVE(X)
DBL(mark(X)) → DBL(X)
DBLS(mark(X)) → DBLS(X)
SEL(mark(X1), X2) → SEL(X1, X2)
SEL(X1, mark(X2)) → SEL(X1, X2)
INDX(mark(X1), X2) → INDX(X1, X2)
DBL1(mark(X)) → DBL1(X)
S1(mark(X)) → S1(X)
SEL1(mark(X1), X2) → SEL1(X1, X2)
SEL1(X1, mark(X2)) → SEL1(X1, X2)
QUOTE(mark(X)) → QUOTE(X)
PROPER(dbl(X)) → DBL(proper(X))
PROPER(dbl(X)) → PROPER(X)
PROPER(s(X)) → S(proper(X))
PROPER(s(X)) → PROPER(X)
PROPER(dbls(X)) → DBLS(proper(X))
PROPER(dbls(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(sel(X1, X2)) → SEL(proper(X1), proper(X2))
PROPER(sel(X1, X2)) → PROPER(X1)
PROPER(sel(X1, X2)) → PROPER(X2)
PROPER(indx(X1, X2)) → INDX(proper(X1), proper(X2))
PROPER(indx(X1, X2)) → PROPER(X1)
PROPER(indx(X1, X2)) → PROPER(X2)
PROPER(from(X)) → FROM(proper(X))
PROPER(from(X)) → PROPER(X)
PROPER(dbl1(X)) → DBL1(proper(X))
PROPER(dbl1(X)) → PROPER(X)
PROPER(s1(X)) → S1(proper(X))
PROPER(s1(X)) → PROPER(X)
PROPER(sel1(X1, X2)) → SEL1(proper(X1), proper(X2))
PROPER(sel1(X1, X2)) → PROPER(X1)
PROPER(sel1(X1, X2)) → PROPER(X2)
PROPER(quote(X)) → QUOTE(proper(X))
PROPER(quote(X)) → PROPER(X)
DBL(ok(X)) → DBL(X)
S(ok(X)) → S(X)
DBLS(ok(X)) → DBLS(X)
CONS(ok(X1), ok(X2)) → CONS(X1, X2)
SEL(ok(X1), ok(X2)) → SEL(X1, X2)
INDX(ok(X1), ok(X2)) → INDX(X1, X2)
FROM(ok(X)) → FROM(X)
DBL1(ok(X)) → DBL1(X)
S1(ok(X)) → S1(X)
SEL1(ok(X1), ok(X2)) → SEL1(X1, X2)
QUOTE(ok(X)) → QUOTE(X)
TOP(mark(X)) → TOP(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(ok(X)) → TOP(active(X))
TOP(ok(X)) → ACTIVE(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
FROM(ok(X)) → FROM(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
FROM(ok(X)) → FROM(X)
[0, 01] > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
nil > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
top > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
ok1: [1]
active1: [1]
dbl1: [1]
0: []
mark: []
s1: [1]
dbls1: [1]
nil: []
sel1: [1]
indx1: [1]
from1: [1]
dbl11: [1]
01: []
s11: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
CONS(ok(X1), ok(X2)) → CONS(X1, X2)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > nil > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > cons1 > dbl1 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > from1 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > 01 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
top > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
CONS1: [1]
ok1: [1]
dbl1: [1]
0: []
mark: []
dbls1: [1]
nil: []
cons1: [1]
sel1: [1]
indx1: [1]
from1: [1]
01: []
sel11: [1]
quote1: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
S(ok(X)) → S(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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)
[0, 01] > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
nil > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
top > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
ok1: [1]
active1: [1]
dbl1: [1]
0: []
mark: []
s1: [1]
dbls1: [1]
nil: []
sel1: [1]
indx1: [1]
from1: [1]
dbl11: [1]
01: []
s11: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
QUOTE(ok(X)) → QUOTE(X)
QUOTE(mark(X)) → QUOTE(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
QUOTE(mark(X)) → QUOTE(X)
active1 > [0, 01] > [mark1, dbl1, dbls1, s11]
active1 > nil > [mark1, dbl1, dbls1, s11]
active1 > [cons2, indx2, proper1] > sel2 > sel12 > [mark1, dbl1, dbls1, s11]
top > [cons2, indx2, proper1] > sel2 > sel12 > [mark1, dbl1, dbls1, s11]
mark1: [1]
active1: [1]
dbl1: [1]
0: []
dbls1: [1]
nil: []
cons2: [1,2]
sel2: [2,1]
indx2: [2,1]
01: []
s11: [1]
sel12: [1,2]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
QUOTE(ok(X)) → QUOTE(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
QUOTE(ok(X)) → QUOTE(X)
[0, 01] > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
nil > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
top > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
ok1: [1]
active1: [1]
dbl1: [1]
0: []
mark: []
s1: [1]
dbls1: [1]
nil: []
sel1: [1]
indx1: [1]
from1: [1]
dbl11: [1]
01: []
s11: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
SEL1(X1, mark(X2)) → SEL1(X1, X2)
SEL1(mark(X1), X2) → SEL1(X1, X2)
SEL1(ok(X1), ok(X2)) → SEL1(X1, X2)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
SEL1(X1, mark(X2)) → SEL1(X1, X2)
SEL1(mark(X1), X2) → SEL1(X1, X2)
[active1, dbl11] > [0, 01] > [SEL12, mark1]
[active1, dbl11] > indx2 > nil > [SEL12, mark1]
[active1, dbl11] > indx2 > cons2 > [dbl1, dbls1] > [SEL12, mark1]
[active1, dbl11] > indx2 > cons2 > sel2 > [SEL12, mark1]
[active1, dbl11] > sel12 > [SEL12, mark1]
SEL12: [2,1]
mark1: [1]
active1: [1]
dbl1: [1]
0: []
dbls1: [1]
nil: []
cons2: [2,1]
sel2: [2,1]
indx2: [2,1]
dbl11: [1]
01: []
sel12: [1,2]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
SEL1(ok(X1), ok(X2)) → SEL1(X1, X2)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
SEL1(ok(X1), ok(X2)) → SEL1(X1, X2)
SEL11 > [ok1, 0, mark, dbls1, nil, sel1, indx1, sel11, quote1]
01 > [ok1, 0, mark, dbls1, nil, sel1, indx1, sel11, quote1]
proper1 > cons1 > dbl1 > [ok1, 0, mark, dbls1, nil, sel1, indx1, sel11, quote1]
proper1 > from1 > [ok1, 0, mark, dbls1, nil, sel1, indx1, sel11, quote1]
top > [ok1, 0, mark, dbls1, nil, sel1, indx1, sel11, quote1]
SEL11: [1]
ok1: [1]
dbl1: [1]
0: []
mark: []
dbls1: [1]
nil: []
cons1: [1]
sel1: [1]
indx1: [1]
from1: [1]
01: []
sel11: [1]
quote1: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
S1(ok(X)) → S1(X)
S1(mark(X)) → S1(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
S1(mark(X)) → S1(X)
active1 > [0, 01] > [mark1, dbl1, dbls1, s11]
active1 > nil > [mark1, dbl1, dbls1, s11]
active1 > [cons2, indx2, proper1] > sel2 > sel12 > [mark1, dbl1, dbls1, s11]
top > [cons2, indx2, proper1] > sel2 > sel12 > [mark1, dbl1, dbls1, s11]
mark1: [1]
active1: [1]
dbl1: [1]
0: []
dbls1: [1]
nil: []
cons2: [1,2]
sel2: [2,1]
indx2: [2,1]
01: []
s11: [1]
sel12: [1,2]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
S1(ok(X)) → S1(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
S1(ok(X)) → S1(X)
[0, 01] > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
nil > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
top > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
ok1: [1]
active1: [1]
dbl1: [1]
0: []
mark: []
s1: [1]
dbls1: [1]
nil: []
sel1: [1]
indx1: [1]
from1: [1]
dbl11: [1]
01: []
s11: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
DBL1(ok(X)) → DBL1(X)
DBL1(mark(X)) → DBL1(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
DBL1(mark(X)) → DBL1(X)
active1 > [0, 01] > [mark1, dbl1, dbls1, s11]
active1 > nil > [mark1, dbl1, dbls1, s11]
active1 > [cons2, indx2, proper1] > sel2 > sel12 > [mark1, dbl1, dbls1, s11]
top > [cons2, indx2, proper1] > sel2 > sel12 > [mark1, dbl1, dbls1, s11]
mark1: [1]
active1: [1]
dbl1: [1]
0: []
dbls1: [1]
nil: []
cons2: [1,2]
sel2: [2,1]
indx2: [2,1]
01: []
s11: [1]
sel12: [1,2]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
DBL1(ok(X)) → DBL1(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
DBL1(ok(X)) → DBL1(X)
[0, 01] > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
nil > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
top > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
ok1: [1]
active1: [1]
dbl1: [1]
0: []
mark: []
s1: [1]
dbls1: [1]
nil: []
sel1: [1]
indx1: [1]
from1: [1]
dbl11: [1]
01: []
s11: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
INDX(ok(X1), ok(X2)) → INDX(X1, X2)
INDX(mark(X1), X2) → INDX(X1, X2)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
INDX(mark(X1), X2) → INDX(X1, X2)
top > proper1 > [active1, dbls1, sel12] > nil > [mark1, 0] > INDX1
top > proper1 > [active1, dbls1, sel12] > nil > [mark1, 0] > 01
top > proper1 > [active1, dbls1, sel12] > sel2 > [mark1, 0] > INDX1
top > proper1 > [active1, dbls1, sel12] > sel2 > [mark1, 0] > 01
top > proper1 > [active1, dbls1, sel12] > indx2 > [mark1, 0] > INDX1
top > proper1 > [active1, dbls1, sel12] > indx2 > [mark1, 0] > 01
top > proper1 > [active1, dbls1, sel12] > indx2 > cons2
top > proper1 > [active1, dbls1, sel12] > from1 > [mark1, 0] > INDX1
top > proper1 > [active1, dbls1, sel12] > from1 > [mark1, 0] > 01
top > proper1 > [active1, dbls1, sel12] > from1 > cons2
INDX1: [1]
mark1: [1]
active1: [1]
0: []
dbls1: [1]
nil: []
cons2: [2,1]
sel2: [2,1]
indx2: [1,2]
from1: [1]
01: []
sel12: [2,1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
INDX(ok(X1), ok(X2)) → INDX(X1, X2)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
INDX(ok(X1), ok(X2)) → INDX(X1, X2)
INDX1 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > nil > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > cons1 > dbl1 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > from1 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > 01 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
top > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
INDX1: [1]
ok1: [1]
dbl1: [1]
0: []
mark: []
dbls1: [1]
nil: []
cons1: [1]
sel1: [1]
indx1: [1]
from1: [1]
01: []
sel11: [1]
quote1: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(mark(X1), X2) → SEL(X1, X2)
SEL(ok(X1), ok(X2)) → SEL(X1, X2)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
SEL(X1, mark(X2)) → SEL(X1, X2)
SEL(mark(X1), X2) → SEL(X1, X2)
active1 > [0, 01] > [mark1, dbls1, nil]
active1 > [s1, sel12] > sel2 > [mark1, dbls1, nil]
active1 > indx2 > cons2 > sel2 > [mark1, dbls1, nil]
active1 > s11 > [mark1, dbls1, nil]
SEL2: [2,1]
mark1: [1]
active1: [1]
0: []
s1: [1]
dbls1: [1]
nil: []
cons2: [2,1]
sel2: [2,1]
indx2: [2,1]
01: []
s11: [1]
sel12: [2,1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
SEL(ok(X1), ok(X2)) → SEL(X1, X2)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
SEL(ok(X1), ok(X2)) → SEL(X1, X2)
SEL1 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > nil > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > cons1 > dbl1 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > from1 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
proper1 > 01 > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
top > [ok1, 0, mark, dbls1, sel1, indx1, sel11, quote1]
SEL1: [1]
ok1: [1]
dbl1: [1]
0: []
mark: []
dbls1: [1]
nil: []
cons1: [1]
sel1: [1]
indx1: [1]
from1: [1]
01: []
sel11: [1]
quote1: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
DBLS(ok(X)) → DBLS(X)
DBLS(mark(X)) → DBLS(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
DBLS(mark(X)) → DBLS(X)
active1 > [0, 01] > [mark1, dbl1, dbls1, s11]
active1 > nil > [mark1, dbl1, dbls1, s11]
active1 > [cons2, indx2, proper1] > sel2 > sel12 > [mark1, dbl1, dbls1, s11]
top > [cons2, indx2, proper1] > sel2 > sel12 > [mark1, dbl1, dbls1, s11]
mark1: [1]
active1: [1]
dbl1: [1]
0: []
dbls1: [1]
nil: []
cons2: [1,2]
sel2: [2,1]
indx2: [2,1]
01: []
s11: [1]
sel12: [1,2]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
DBLS(ok(X)) → DBLS(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
DBLS(ok(X)) → DBLS(X)
[0, 01] > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
nil > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
top > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
ok1: [1]
active1: [1]
dbl1: [1]
0: []
mark: []
s1: [1]
dbls1: [1]
nil: []
sel1: [1]
indx1: [1]
from1: [1]
dbl11: [1]
01: []
s11: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
DBL(ok(X)) → DBL(X)
DBL(mark(X)) → DBL(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
DBL(mark(X)) → DBL(X)
active1 > [0, 01] > [mark1, dbl1, dbls1, s11]
active1 > nil > [mark1, dbl1, dbls1, s11]
active1 > [cons2, indx2, proper1] > sel2 > sel12 > [mark1, dbl1, dbls1, s11]
top > [cons2, indx2, proper1] > sel2 > sel12 > [mark1, dbl1, dbls1, s11]
mark1: [1]
active1: [1]
dbl1: [1]
0: []
dbls1: [1]
nil: []
cons2: [1,2]
sel2: [2,1]
indx2: [2,1]
01: []
s11: [1]
sel12: [1,2]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
DBL(ok(X)) → DBL(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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.
DBL(ok(X)) → DBL(X)
[0, 01] > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
nil > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
top > [ok1, active1, dbl1, mark, s1, dbls1, sel1, indx1, from1, dbl11, s11, proper1]
ok1: [1]
active1: [1]
dbl1: [1]
0: []
mark: []
s1: [1]
dbls1: [1]
nil: []
sel1: [1]
indx1: [1]
from1: [1]
dbl11: [1]
01: []
s11: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(s(X)) → PROPER(X)
PROPER(dbl(X)) → PROPER(X)
PROPER(dbls(X)) → PROPER(X)
PROPER(cons(X1, X2)) → PROPER(X1)
PROPER(cons(X1, X2)) → PROPER(X2)
PROPER(sel(X1, X2)) → PROPER(X1)
PROPER(sel(X1, X2)) → PROPER(X2)
PROPER(indx(X1, X2)) → PROPER(X1)
PROPER(indx(X1, X2)) → PROPER(X2)
PROPER(from(X)) → PROPER(X)
PROPER(dbl1(X)) → PROPER(X)
PROPER(s1(X)) → PROPER(X)
PROPER(sel1(X1, X2)) → PROPER(X1)
PROPER(sel1(X1, X2)) → PROPER(X2)
PROPER(quote(X)) → PROPER(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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(s(X)) → PROPER(X)
PROPER(cons(X1, X2)) → PROPER(X1)
PROPER(cons(X1, X2)) → PROPER(X2)
PROPER(sel(X1, X2)) → PROPER(X1)
PROPER(sel(X1, X2)) → PROPER(X2)
PROPER(indx(X1, X2)) → PROPER(X1)
PROPER(indx(X1, X2)) → PROPER(X2)
PROPER(sel1(X1, X2)) → PROPER(X1)
PROPER(sel1(X1, X2)) → PROPER(X2)
PROPER1 > [s1, cons2, sel2, nil]
top > active1 > [indx2, sel12, 0, proper1] > [s1, cons2, sel2, nil]
top > active1 > 01 > [s1, cons2, sel2, nil]
PROPER1: [1]
s1: [1]
cons2: [1,2]
sel2: [1,2]
indx2: [1,2]
sel12: [1,2]
active1: [1]
0: []
nil: []
01: []
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(dbl(X)) → PROPER(X)
PROPER(dbls(X)) → PROPER(X)
PROPER(from(X)) → PROPER(X)
PROPER(dbl1(X)) → PROPER(X)
PROPER(s1(X)) → PROPER(X)
PROPER(quote(X)) → PROPER(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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(dbl(X)) → PROPER(X)
PROPER(dbls(X)) → PROPER(X)
PROPER(from(X)) → PROPER(X)
PROPER(dbl1(X)) → PROPER(X)
PROPER1 > [dbl11, mark1]
0 > 01 > [dbl11, mark1]
top > [active1, nil, indx2, sel12] > dbl1 > [dbl11, mark1]
top > [active1, nil, indx2, sel12] > [dbls1, cons2, sel2] > [dbl11, mark1]
top > [active1, nil, indx2, sel12] > from1 > [dbl11, mark1]
PROPER1: [1]
dbl1: [1]
dbls1: [1]
from1: [1]
dbl11: [1]
active1: [1]
0: []
mark1: [1]
nil: []
cons2: [2,1]
sel2: [1,2]
indx2: [1,2]
01: []
sel12: [1,2]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(s1(X)) → PROPER(X)
PROPER(quote(X)) → PROPER(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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(quote(X)) → PROPER(X)
PROPER1 > [mark1, s1, dbl11]
active1 > [quote1, dbl1, sel2, indx2, from1, proper1] > cons2 > dbls1 > nil > [mark1, s1, dbl11]
active1 > [quote1, dbl1, sel2, indx2, from1, proper1] > cons2 > sel12 > [mark1, s1, dbl11]
active1 > 01 > [mark1, s1, dbl11]
0 > 01 > [mark1, s1, dbl11]
top > [mark1, s1, dbl11]
PROPER1: [1]
quote1: [1]
active1: [1]
dbl1: [1]
0: []
mark1: [1]
s1: [1]
dbls1: [1]
nil: []
cons2: [1,2]
sel2: [1,2]
indx2: [2,1]
from1: [1]
dbl11: [1]
01: []
sel12: [1,2]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(s1(X)) → PROPER(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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(s1(X)) → PROPER(X)
PROPER1 > cons2
[dbl, s, dbls1, from1, proper1] > [0, mark, indx, sel11, quote] > s11 > cons2
[dbl, s, dbls1, from1, proper1] > [0, mark, indx, sel11, quote] > nil > cons2
[dbl, s, dbls1, from1, proper1] > [0, mark, indx, sel11, quote] > sel2 > cons2
[dbl, s, dbls1, from1, proper1] > [0, mark, indx, sel11, quote] > top > cons2
[dbl, s, dbls1, from1, proper1] > 01 > cons2
PROPER1: [1]
s11: [1]
dbl: []
0: []
mark: []
s: []
dbls1: [1]
nil: []
cons2: [1,2]
sel2: [1,2]
indx: []
from1: [1]
01: []
sel11: [1]
quote: []
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(dbls(X)) → ACTIVE(X)
ACTIVE(dbl(X)) → ACTIVE(X)
ACTIVE(sel(X1, X2)) → ACTIVE(X1)
ACTIVE(sel(X1, X2)) → ACTIVE(X2)
ACTIVE(indx(X1, X2)) → ACTIVE(X1)
ACTIVE(dbl1(X)) → ACTIVE(X)
ACTIVE(s1(X)) → ACTIVE(X)
ACTIVE(sel1(X1, X2)) → ACTIVE(X1)
ACTIVE(sel1(X1, X2)) → ACTIVE(X2)
ACTIVE(quote(X)) → ACTIVE(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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(dbls(X)) → ACTIVE(X)
ACTIVE(sel(X1, X2)) → ACTIVE(X1)
ACTIVE(sel(X1, X2)) → ACTIVE(X2)
ACTIVE(indx(X1, X2)) → ACTIVE(X1)
ACTIVE(dbl1(X)) → ACTIVE(X)
ACTIVE(s1(X)) → ACTIVE(X)
ACTIVE(sel1(X1, X2)) → ACTIVE(X1)
ACTIVE(sel1(X1, X2)) → ACTIVE(X2)
0 > 01
top > [sel2, indx2, dbl11, sel12, active1, from1, proper1] > dbls1 > cons2
top > [sel2, indx2, dbl11, sel12, active1, from1, proper1] > s11
top > [sel2, indx2, dbl11, sel12, active1, from1, proper1] > nil
top > [sel2, indx2, dbl11, sel12, active1, from1, proper1] > 01
ACTIVE1: [1]
dbls1: [1]
sel2: [1,2]
indx2: [2,1]
dbl11: [1]
s11: [1]
sel12: [1,2]
active1: [1]
0: []
nil: []
cons2: [2,1]
from1: [1]
01: []
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(dbl(X)) → ACTIVE(X)
ACTIVE(quote(X)) → ACTIVE(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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(dbl(X)) → ACTIVE(X)
[dbl1, active1, indx] > [s1, from] > s1 > [0, mark, 01]
[dbl1, active1, indx] > [s1, from] > sel1 > [0, mark, 01]
[dbl1, active1, indx] > nil > [0, mark, 01]
[dbl1, active1, indx] > cons1 > sel1 > [0, mark, 01]
top > [0, mark, 01]
dbl1: [1]
active1: [1]
0: []
mark: []
s1: [1]
nil: []
cons1: [1]
indx: []
from: []
01: []
s1: []
sel1: []
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(quote(X)) → ACTIVE(X)
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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(quote(X)) → ACTIVE(X)
0 > 01 > [ACTIVE1, quote1, mark, s1, nil, cons2, from, dbl11, sel11, proper1]
dbls > active1 > dbl > [ACTIVE1, quote1, mark, s1, nil, cons2, from, dbl11, sel11, proper1]
dbls > active1 > indx > [ACTIVE1, quote1, mark, s1, nil, cons2, from, dbl11, sel11, proper1]
dbls > active1 > 01 > [ACTIVE1, quote1, mark, s1, nil, cons2, from, dbl11, sel11, proper1]
top > [ACTIVE1, quote1, mark, s1, nil, cons2, from, dbl11, sel11, proper1]
ACTIVE1: [1]
quote1: [1]
active1: [1]
dbl: []
0: []
mark: []
s1: [1]
dbls: []
nil: []
cons2: [1,2]
indx: []
from: []
dbl11: [1]
01: []
sel11: [1]
proper1: [1]
top: []
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(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(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(dbls(nil)) → mark(nil)
active(dbls(cons(X, Y))) → mark(cons(dbl(X), dbls(Y)))
active(sel(0, cons(X, Y))) → mark(X)
active(sel(s(X), cons(Y, Z))) → mark(sel(X, Z))
active(indx(nil, X)) → mark(nil)
active(indx(cons(X, Y), Z)) → mark(cons(sel(X, Z), indx(Y, Z)))
active(from(X)) → mark(cons(X, from(s(X))))
active(dbl1(0)) → mark(01)
active(dbl1(s(X))) → mark(s1(s1(dbl1(X))))
active(sel1(0, cons(X, Y))) → mark(X)
active(sel1(s(X), cons(Y, Z))) → mark(sel1(X, Z))
active(quote(0)) → mark(01)
active(quote(s(X))) → mark(s1(quote(X)))
active(quote(dbl(X))) → mark(dbl1(X))
active(quote(sel(X, Y))) → mark(sel1(X, Y))
active(dbl(X)) → dbl(active(X))
active(dbls(X)) → dbls(active(X))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
active(indx(X1, X2)) → indx(active(X1), X2)
active(dbl1(X)) → dbl1(active(X))
active(s1(X)) → s1(active(X))
active(sel1(X1, X2)) → sel1(active(X1), X2)
active(sel1(X1, X2)) → sel1(X1, active(X2))
active(quote(X)) → quote(active(X))
dbl(mark(X)) → mark(dbl(X))
dbls(mark(X)) → mark(dbls(X))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
indx(mark(X1), X2) → mark(indx(X1, X2))
dbl1(mark(X)) → mark(dbl1(X))
s1(mark(X)) → mark(s1(X))
sel1(mark(X1), X2) → mark(sel1(X1, X2))
sel1(X1, mark(X2)) → mark(sel1(X1, X2))
quote(mark(X)) → mark(quote(X))
proper(dbl(X)) → dbl(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(dbls(X)) → dbls(proper(X))
proper(nil) → ok(nil)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
proper(indx(X1, X2)) → indx(proper(X1), proper(X2))
proper(from(X)) → from(proper(X))
proper(dbl1(X)) → dbl1(proper(X))
proper(01) → ok(01)
proper(s1(X)) → s1(proper(X))
proper(sel1(X1, X2)) → sel1(proper(X1), proper(X2))
proper(quote(X)) → quote(proper(X))
dbl(ok(X)) → ok(dbl(X))
s(ok(X)) → ok(s(X))
dbls(ok(X)) → ok(dbls(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
indx(ok(X1), ok(X2)) → ok(indx(X1, X2))
from(ok(X)) → ok(from(X))
dbl1(ok(X)) → ok(dbl1(X))
s1(ok(X)) → ok(s1(X))
sel1(ok(X1), ok(X2)) → ok(sel1(X1, X2))
quote(ok(X)) → ok(quote(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))