R
↳Dependency Pair Analysis
DBL(s(X)) -> DBL(X)
DBLS(cons(X, Y)) -> DBL(X)
DBLS(cons(X, Y)) -> DBLS(Y)
SEL(s(X), cons(Y, Z)) -> SEL(X, Z)
INDX(cons(X, Y), Z) -> SEL(X, Z)
INDX(cons(X, Y), Z) -> INDX(Y, Z)
FROM(X) -> FROM(s(X))
DBL1(s(X)) -> DBL1(X)
SEL1(s(X), cons(Y, Z)) -> SEL1(X, Z)
QUOTE(s(X)) -> QUOTE(X)
QUOTE(dbl(X)) -> DBL1(X)
QUOTE(sel(X, Y)) -> SEL1(X, Y)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
→DP Problem 5
↳Remaining
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
→DP Problem 8
↳Remaining
DBL(s(X)) -> DBL(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBL(s(X)) -> DBL(X)
POL(s(x1)) = 1 + x1 POL(DBL(x1)) = x1
DBL(x1) -> DBL(x1)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 9
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
→DP Problem 5
↳Remaining
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
→DP Problem 8
↳Remaining
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
→DP Problem 5
↳Remaining
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
→DP Problem 8
↳Remaining
SEL(s(X), cons(Y, Z)) -> SEL(X, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
SEL(s(X), cons(Y, Z)) -> SEL(X, Z)
POL(SEL(x1, x2)) = x1 + x2 POL(cons(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1
SEL(x1, x2) -> SEL(x1, x2)
s(x1) -> s(x1)
cons(x1, x2) -> cons(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 10
↳Dependency Graph
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
→DP Problem 5
↳Remaining
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
→DP Problem 8
↳Remaining
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
→DP Problem 5
↳Remaining Obligation(s)
→DP Problem 6
↳Remaining Obligation(s)
→DP Problem 7
↳Remaining Obligation(s)
→DP Problem 8
↳Remaining Obligation(s)
FROM(X) -> FROM(s(X))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBL1(s(X)) -> DBL1(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
SEL1(s(X), cons(Y, Z)) -> SEL1(X, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBLS(cons(X, Y)) -> DBLS(Y)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
INDX(cons(X, Y), Z) -> INDX(Y, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
QUOTE(s(X)) -> QUOTE(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
→DP Problem 5
↳Remaining Obligation(s)
→DP Problem 6
↳Remaining Obligation(s)
→DP Problem 7
↳Remaining Obligation(s)
→DP Problem 8
↳Remaining Obligation(s)
FROM(X) -> FROM(s(X))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBL1(s(X)) -> DBL1(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
SEL1(s(X), cons(Y, Z)) -> SEL1(X, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBLS(cons(X, Y)) -> DBLS(Y)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
INDX(cons(X, Y), Z) -> INDX(Y, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
QUOTE(s(X)) -> QUOTE(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
→DP Problem 5
↳Remaining Obligation(s)
→DP Problem 6
↳Remaining Obligation(s)
→DP Problem 7
↳Remaining Obligation(s)
→DP Problem 8
↳Remaining Obligation(s)
FROM(X) -> FROM(s(X))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBL1(s(X)) -> DBL1(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
SEL1(s(X), cons(Y, Z)) -> SEL1(X, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBLS(cons(X, Y)) -> DBLS(Y)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
INDX(cons(X, Y), Z) -> INDX(Y, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
QUOTE(s(X)) -> QUOTE(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
→DP Problem 5
↳Remaining Obligation(s)
→DP Problem 6
↳Remaining Obligation(s)
→DP Problem 7
↳Remaining Obligation(s)
→DP Problem 8
↳Remaining Obligation(s)
FROM(X) -> FROM(s(X))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBL1(s(X)) -> DBL1(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
SEL1(s(X), cons(Y, Z)) -> SEL1(X, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBLS(cons(X, Y)) -> DBLS(Y)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
INDX(cons(X, Y), Z) -> INDX(Y, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
QUOTE(s(X)) -> QUOTE(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
→DP Problem 5
↳Remaining Obligation(s)
→DP Problem 6
↳Remaining Obligation(s)
→DP Problem 7
↳Remaining Obligation(s)
→DP Problem 8
↳Remaining Obligation(s)
FROM(X) -> FROM(s(X))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBL1(s(X)) -> DBL1(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
SEL1(s(X), cons(Y, Z)) -> SEL1(X, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBLS(cons(X, Y)) -> DBLS(Y)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
INDX(cons(X, Y), Z) -> INDX(Y, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
QUOTE(s(X)) -> QUOTE(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
→DP Problem 5
↳Remaining Obligation(s)
→DP Problem 6
↳Remaining Obligation(s)
→DP Problem 7
↳Remaining Obligation(s)
→DP Problem 8
↳Remaining Obligation(s)
FROM(X) -> FROM(s(X))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBL1(s(X)) -> DBL1(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
SEL1(s(X), cons(Y, Z)) -> SEL1(X, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
DBLS(cons(X, Y)) -> DBLS(Y)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
INDX(cons(X, Y), Z) -> INDX(Y, Z)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost
QUOTE(s(X)) -> QUOTE(X)
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, Z)
indx(nil, X) -> nil
indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
from(X) -> cons(X, from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0, cons(X, Y)) -> X
sel1(s(X), cons(Y, Z)) -> sel1(X, Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X, Y)) -> sel1(X, Y)
innermost