YES
Time: 1.080696
TRS:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
DP:
DP:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> mark# X1,
mark# fst(X1, X2) -> mark# X2,
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# fst(X1, X2) -> fst#(mark X1, mark X2),
mark# 0() -> active# 0(),
mark# cons(X1, X2) -> mark# X1,
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# cons(X1, X2) -> cons#(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> mark# X,
mark# from X -> active# from mark X,
mark# from X -> from# mark X,
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
mark# add(X1, X2) -> add#(mark X1, mark X2),
mark# len X -> mark# X,
mark# len X -> active# len mark X,
mark# len X -> len# mark X,
active# fst(0(), Z) -> mark# nil(),
active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)),
active# fst(s X, cons(Y, Z)) -> fst#(X, Z),
active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)),
active# from X -> mark# cons(X, from s X),
active# from X -> cons#(X, from s X),
active# from X -> s# X,
active# from X -> from# s X,
active# add(0(), X) -> mark# X,
active# add(s X, Y) -> mark# s add(X, Y),
active# add(s X, Y) -> s# add(X, Y),
active# add(s X, Y) -> add#(X, Y),
active# len nil() -> mark# 0(),
active# len cons(X, Z) -> mark# s len Z,
active# len cons(X, Z) -> s# len Z,
active# len cons(X, Z) -> len# Z,
fst#(X1, mark X2) -> fst#(X1, X2),
fst#(X1, active X2) -> fst#(X1, X2),
fst#(mark X1, X2) -> fst#(X1, X2),
fst#(active X1, X2) -> fst#(X1, X2),
cons#(X1, mark X2) -> cons#(X1, X2),
cons#(X1, active X2) -> cons#(X1, X2),
cons#(mark X1, X2) -> cons#(X1, X2),
cons#(active X1, X2) -> cons#(X1, X2),
s# mark X -> s# X,
s# active X -> s# X,
from# mark X -> from# X,
from# active X -> from# X,
add#(X1, mark X2) -> add#(X1, X2),
add#(X1, active X2) -> add#(X1, X2),
add#(mark X1, X2) -> add#(X1, X2),
add#(active X1, X2) -> add#(X1, X2),
len# mark X -> len# X,
len# active X -> len# X}
TRS:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
UR:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X,
a(x, y) -> x,
a(x, y) -> y}
EDG:
{
(mark# nil() -> active# nil(), active# len cons(X, Z) -> len# Z)
(mark# nil() -> active# nil(), active# len cons(X, Z) -> s# len Z)
(mark# nil() -> active# nil(), active# len cons(X, Z) -> mark# s len Z)
(mark# nil() -> active# nil(), active# len nil() -> mark# 0())
(mark# nil() -> active# nil(), active# add(s X, Y) -> add#(X, Y))
(mark# nil() -> active# nil(), active# add(s X, Y) -> s# add(X, Y))
(mark# nil() -> active# nil(), active# add(s X, Y) -> mark# s add(X, Y))
(mark# nil() -> active# nil(), active# add(0(), X) -> mark# X)
(mark# nil() -> active# nil(), active# from X -> from# s X)
(mark# nil() -> active# nil(), active# from X -> s# X)
(mark# nil() -> active# nil(), active# from X -> cons#(X, from s X))
(mark# nil() -> active# nil(), active# from X -> mark# cons(X, from s X))
(mark# nil() -> active# nil(), active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
(mark# nil() -> active# nil(), active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
(mark# nil() -> active# nil(), active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)))
(mark# nil() -> active# nil(), active# fst(0(), Z) -> mark# nil())
(active# fst(0(), Z) -> mark# nil(), mark# len X -> len# mark X)
(active# fst(0(), Z) -> mark# nil(), mark# len X -> active# len mark X)
(active# fst(0(), Z) -> mark# nil(), mark# len X -> mark# X)
(active# fst(0(), Z) -> mark# nil(), mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# fst(0(), Z) -> mark# nil(), mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# fst(0(), Z) -> mark# nil(), mark# add(X1, X2) -> mark# X2)
(active# fst(0(), Z) -> mark# nil(), mark# add(X1, X2) -> mark# X1)
(active# fst(0(), Z) -> mark# nil(), mark# from X -> from# mark X)
(active# fst(0(), Z) -> mark# nil(), mark# from X -> active# from mark X)
(active# fst(0(), Z) -> mark# nil(), mark# from X -> mark# X)
(active# fst(0(), Z) -> mark# nil(), mark# s X -> active# s X)
(active# fst(0(), Z) -> mark# nil(), mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# fst(0(), Z) -> mark# nil(), mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# fst(0(), Z) -> mark# nil(), mark# cons(X1, X2) -> mark# X1)
(active# fst(0(), Z) -> mark# nil(), mark# 0() -> active# 0())
(active# fst(0(), Z) -> mark# nil(), mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(active# fst(0(), Z) -> mark# nil(), mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(active# fst(0(), Z) -> mark# nil(), mark# fst(X1, X2) -> mark# X2)
(active# fst(0(), Z) -> mark# nil(), mark# fst(X1, X2) -> mark# X1)
(active# fst(0(), Z) -> mark# nil(), mark# nil() -> active# nil())
(mark# fst(X1, X2) -> fst#(mark X1, mark X2), fst#(active X1, X2) -> fst#(X1, X2))
(mark# fst(X1, X2) -> fst#(mark X1, mark X2), fst#(mark X1, X2) -> fst#(X1, X2))
(mark# fst(X1, X2) -> fst#(mark X1, mark X2), fst#(X1, active X2) -> fst#(X1, X2))
(mark# fst(X1, X2) -> fst#(mark X1, mark X2), fst#(X1, mark X2) -> fst#(X1, X2))
(active# len cons(X, Z) -> len# Z, len# active X -> len# X)
(active# len cons(X, Z) -> len# Z, len# mark X -> len# X)
(fst#(X1, active X2) -> fst#(X1, X2), fst#(active X1, X2) -> fst#(X1, X2))
(fst#(X1, active X2) -> fst#(X1, X2), fst#(mark X1, X2) -> fst#(X1, X2))
(fst#(X1, active X2) -> fst#(X1, X2), fst#(X1, active X2) -> fst#(X1, X2))
(fst#(X1, active X2) -> fst#(X1, X2), fst#(X1, mark X2) -> fst#(X1, X2))
(fst#(active X1, X2) -> fst#(X1, X2), fst#(active X1, X2) -> fst#(X1, X2))
(fst#(active X1, X2) -> fst#(X1, X2), fst#(mark X1, X2) -> fst#(X1, X2))
(fst#(active X1, X2) -> fst#(X1, X2), fst#(X1, active X2) -> fst#(X1, X2))
(fst#(active X1, X2) -> fst#(X1, X2), fst#(X1, mark X2) -> fst#(X1, X2))
(cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
(cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
(cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
(cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
(cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
(cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
(add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
(add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
(add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
(add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
(add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
(add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
(add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
(add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
(mark# fst(X1, X2) -> mark# X2, mark# len X -> len# mark X)
(mark# fst(X1, X2) -> mark# X2, mark# len X -> active# len mark X)
(mark# fst(X1, X2) -> mark# X2, mark# len X -> mark# X)
(mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2)
(mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
(mark# fst(X1, X2) -> mark# X2, mark# from X -> from# mark X)
(mark# fst(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
(mark# fst(X1, X2) -> mark# X2, mark# from X -> mark# X)
(mark# fst(X1, X2) -> mark# X2, mark# s X -> active# s X)
(mark# fst(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# fst(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# fst(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
(mark# fst(X1, X2) -> mark# X2, mark# 0() -> active# 0())
(mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X2)
(mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X1)
(mark# fst(X1, X2) -> mark# X2, mark# nil() -> active# nil())
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# len X -> len# mark X)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# len X -> active# len mark X)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# len X -> mark# X)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# add(X1, X2) -> mark# X2)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# add(X1, X2) -> mark# X1)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# from X -> from# mark X)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# from X -> active# from mark X)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# from X -> mark# X)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# s X -> active# s X)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# cons(X1, X2) -> mark# X1)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# 0() -> active# 0())
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# fst(X1, X2) -> mark# X2)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# fst(X1, X2) -> mark# X1)
(active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)), mark# nil() -> active# nil())
(active# add(s X, Y) -> s# add(X, Y), s# active X -> s# X)
(active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X)
(mark# from X -> active# from mark X, active# len cons(X, Z) -> len# Z)
(mark# from X -> active# from mark X, active# len cons(X, Z) -> s# len Z)
(mark# from X -> active# from mark X, active# len cons(X, Z) -> mark# s len Z)
(mark# from X -> active# from mark X, active# len nil() -> mark# 0())
(mark# from X -> active# from mark X, active# add(s X, Y) -> add#(X, Y))
(mark# from X -> active# from mark X, active# add(s X, Y) -> s# add(X, Y))
(mark# from X -> active# from mark X, active# add(s X, Y) -> mark# s add(X, Y))
(mark# from X -> active# from mark X, active# add(0(), X) -> mark# X)
(mark# from X -> active# from mark X, active# from X -> from# s X)
(mark# from X -> active# from mark X, active# from X -> s# X)
(mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
(mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
(mark# from X -> active# from mark X, active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
(mark# from X -> active# from mark X, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
(mark# from X -> active# from mark X, active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)))
(mark# from X -> active# from mark X, active# fst(0(), Z) -> mark# nil())
(active# add(s X, Y) -> mark# s add(X, Y), mark# len X -> len# mark X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# len X -> active# len mark X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# len X -> mark# X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X2)
(active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X1)
(active# add(s X, Y) -> mark# s add(X, Y), mark# from X -> from# mark X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# from X -> active# from mark X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# from X -> mark# X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# add(s X, Y) -> mark# s add(X, Y), mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# add(s X, Y) -> mark# s add(X, Y), mark# cons(X1, X2) -> mark# X1)
(active# add(s X, Y) -> mark# s add(X, Y), mark# 0() -> active# 0())
(active# add(s X, Y) -> mark# s add(X, Y), mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(active# add(s X, Y) -> mark# s add(X, Y), mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(active# add(s X, Y) -> mark# s add(X, Y), mark# fst(X1, X2) -> mark# X2)
(active# add(s X, Y) -> mark# s add(X, Y), mark# fst(X1, X2) -> mark# X1)
(active# add(s X, Y) -> mark# s add(X, Y), mark# nil() -> active# nil())
(active# fst(s X, cons(Y, Z)) -> fst#(X, Z), fst#(active X1, X2) -> fst#(X1, X2))
(active# fst(s X, cons(Y, Z)) -> fst#(X, Z), fst#(mark X1, X2) -> fst#(X1, X2))
(active# fst(s X, cons(Y, Z)) -> fst#(X, Z), fst#(X1, active X2) -> fst#(X1, X2))
(active# fst(s X, cons(Y, Z)) -> fst#(X, Z), fst#(X1, mark X2) -> fst#(X1, X2))
(mark# from X -> mark# X, mark# len X -> len# mark X)
(mark# from X -> mark# X, mark# len X -> active# len mark X)
(mark# from X -> mark# X, mark# len X -> mark# X)
(mark# from X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# from X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# from X -> mark# X, mark# add(X1, X2) -> mark# X2)
(mark# from X -> mark# X, mark# add(X1, X2) -> mark# X1)
(mark# from X -> mark# X, mark# from X -> from# mark X)
(mark# from X -> mark# X, mark# from X -> active# from mark X)
(mark# from X -> mark# X, mark# from X -> mark# X)
(mark# from X -> mark# X, mark# s X -> active# s X)
(mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(mark# from X -> mark# X, mark# 0() -> active# 0())
(mark# from X -> mark# X, mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(mark# from X -> mark# X, mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(mark# from X -> mark# X, mark# fst(X1, X2) -> mark# X2)
(mark# from X -> mark# X, mark# fst(X1, X2) -> mark# X1)
(mark# from X -> mark# X, mark# nil() -> active# nil())
(active# from X -> s# X, s# active X -> s# X)
(active# from X -> s# X, s# mark X -> s# X)
(s# mark X -> s# X, s# active X -> s# X)
(s# mark X -> s# X, s# mark X -> s# X)
(from# mark X -> from# X, from# active X -> from# X)
(from# mark X -> from# X, from# mark X -> from# X)
(len# mark X -> len# X, len# active X -> len# X)
(len# mark X -> len# X, len# mark X -> len# X)
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# len cons(X, Z) -> len# Z)
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# len cons(X, Z) -> s# len Z)
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# len cons(X, Z) -> mark# s len Z)
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# len nil() -> mark# 0())
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# add(0(), X) -> mark# X)
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# from X -> from# s X)
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# from X -> s# X)
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# from X -> cons#(X, from s X))
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# from X -> mark# cons(X, from s X))
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)))
(mark# fst(X1, X2) -> active# fst(mark X1, mark X2), active# fst(0(), Z) -> mark# nil())
(active# from X -> mark# cons(X, from s X), mark# len X -> len# mark X)
(active# from X -> mark# cons(X, from s X), mark# len X -> active# len mark X)
(active# from X -> mark# cons(X, from s X), mark# len X -> mark# X)
(active# from X -> mark# cons(X, from s X), mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# from X -> mark# cons(X, from s X), mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# from X -> mark# cons(X, from s X), mark# add(X1, X2) -> mark# X2)
(active# from X -> mark# cons(X, from s X), mark# add(X1, X2) -> mark# X1)
(active# from X -> mark# cons(X, from s X), mark# from X -> from# mark X)
(active# from X -> mark# cons(X, from s X), mark# from X -> active# from mark X)
(active# from X -> mark# cons(X, from s X), mark# from X -> mark# X)
(active# from X -> mark# cons(X, from s X), mark# s X -> active# s X)
(active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
(active# from X -> mark# cons(X, from s X), mark# 0() -> active# 0())
(active# from X -> mark# cons(X, from s X), mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(active# from X -> mark# cons(X, from s X), mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(active# from X -> mark# cons(X, from s X), mark# fst(X1, X2) -> mark# X2)
(active# from X -> mark# cons(X, from s X), mark# fst(X1, X2) -> mark# X1)
(active# from X -> mark# cons(X, from s X), mark# nil() -> active# nil())
(mark# from X -> from# mark X, from# active X -> from# X)
(mark# from X -> from# mark X, from# mark X -> from# X)
(active# from X -> from# s X, from# active X -> from# X)
(active# from X -> from# s X, from# mark X -> from# X)
(mark# fst(X1, X2) -> mark# X1, mark# len X -> len# mark X)
(mark# fst(X1, X2) -> mark# X1, mark# len X -> active# len mark X)
(mark# fst(X1, X2) -> mark# X1, mark# len X -> mark# X)
(mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
(mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
(mark# fst(X1, X2) -> mark# X1, mark# from X -> from# mark X)
(mark# fst(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
(mark# fst(X1, X2) -> mark# X1, mark# from X -> mark# X)
(mark# fst(X1, X2) -> mark# X1, mark# s X -> active# s X)
(mark# fst(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# fst(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# fst(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# fst(X1, X2) -> mark# X1, mark# 0() -> active# 0())
(mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2)
(mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1)
(mark# fst(X1, X2) -> mark# X1, mark# nil() -> active# nil())
(mark# add(X1, X2) -> mark# X1, mark# len X -> len# mark X)
(mark# add(X1, X2) -> mark# X1, mark# len X -> active# len mark X)
(mark# add(X1, X2) -> mark# X1, mark# len X -> mark# X)
(mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
(mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
(mark# add(X1, X2) -> mark# X1, mark# from X -> from# mark X)
(mark# add(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
(mark# add(X1, X2) -> mark# X1, mark# from X -> mark# X)
(mark# add(X1, X2) -> mark# X1, mark# s X -> active# s X)
(mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0())
(mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2)
(mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1)
(mark# add(X1, X2) -> mark# X1, mark# nil() -> active# nil())
(mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
(mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1)
(mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2)
(mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
(mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s X)
(mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
(mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
(mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
(mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
(mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# len X -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# len X -> active# len mark X)
(mark# cons(X1, X2) -> mark# X1, mark# len X -> len# mark X)
(active# len cons(X, Z) -> s# len Z, s# mark X -> s# X)
(active# len cons(X, Z) -> s# len Z, s# active X -> s# X)
(mark# len X -> len# mark X, len# mark X -> len# X)
(mark# len X -> len# mark X, len# active X -> len# X)
(mark# s X -> active# s X, active# fst(0(), Z) -> mark# nil())
(mark# s X -> active# s X, active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)))
(mark# s X -> active# s X, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
(mark# s X -> active# s X, active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
(mark# s X -> active# s X, active# from X -> mark# cons(X, from s X))
(mark# s X -> active# s X, active# from X -> cons#(X, from s X))
(mark# s X -> active# s X, active# from X -> s# X)
(mark# s X -> active# s X, active# from X -> from# s X)
(mark# s X -> active# s X, active# add(0(), X) -> mark# X)
(mark# s X -> active# s X, active# add(s X, Y) -> mark# s add(X, Y))
(mark# s X -> active# s X, active# add(s X, Y) -> s# add(X, Y))
(mark# s X -> active# s X, active# add(s X, Y) -> add#(X, Y))
(mark# s X -> active# s X, active# len nil() -> mark# 0())
(mark# s X -> active# s X, active# len cons(X, Z) -> mark# s len Z)
(mark# s X -> active# s X, active# len cons(X, Z) -> s# len Z)
(mark# s X -> active# s X, active# len cons(X, Z) -> len# Z)
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fst(0(), Z) -> mark# nil())
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# from X -> mark# cons(X, from s X))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# from X -> cons#(X, from s X))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# from X -> s# X)
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# from X -> from# s X)
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(0(), X) -> mark# X)
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# len nil() -> mark# 0())
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# len cons(X, Z) -> mark# s len Z)
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# len cons(X, Z) -> s# len Z)
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# len cons(X, Z) -> len# Z)
(len# active X -> len# X, len# mark X -> len# X)
(len# active X -> len# X, len# active X -> len# X)
(from# active X -> from# X, from# mark X -> from# X)
(from# active X -> from# X, from# active X -> from# X)
(s# active X -> s# X, s# mark X -> s# X)
(s# active X -> s# X, s# active X -> s# X)
(active# add(0(), X) -> mark# X, mark# nil() -> active# nil())
(active# add(0(), X) -> mark# X, mark# fst(X1, X2) -> mark# X1)
(active# add(0(), X) -> mark# X, mark# fst(X1, X2) -> mark# X2)
(active# add(0(), X) -> mark# X, mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(active# add(0(), X) -> mark# X, mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(active# add(0(), X) -> mark# X, mark# 0() -> active# 0())
(active# add(0(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
(active# add(0(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# add(0(), X) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# add(0(), X) -> mark# X, mark# s X -> active# s X)
(active# add(0(), X) -> mark# X, mark# from X -> mark# X)
(active# add(0(), X) -> mark# X, mark# from X -> active# from mark X)
(active# add(0(), X) -> mark# X, mark# from X -> from# mark X)
(active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1)
(active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2)
(active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# add(0(), X) -> mark# X, mark# len X -> mark# X)
(active# add(0(), X) -> mark# X, mark# len X -> active# len mark X)
(active# add(0(), X) -> mark# X, mark# len X -> len# mark X)
(mark# len X -> mark# X, mark# nil() -> active# nil())
(mark# len X -> mark# X, mark# fst(X1, X2) -> mark# X1)
(mark# len X -> mark# X, mark# fst(X1, X2) -> mark# X2)
(mark# len X -> mark# X, mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(mark# len X -> mark# X, mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(mark# len X -> mark# X, mark# 0() -> active# 0())
(mark# len X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(mark# len X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# len X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# len X -> mark# X, mark# s X -> active# s X)
(mark# len X -> mark# X, mark# from X -> mark# X)
(mark# len X -> mark# X, mark# from X -> active# from mark X)
(mark# len X -> mark# X, mark# from X -> from# mark X)
(mark# len X -> mark# X, mark# add(X1, X2) -> mark# X1)
(mark# len X -> mark# X, mark# add(X1, X2) -> mark# X2)
(mark# len X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# len X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# len X -> mark# X, mark# len X -> mark# X)
(mark# len X -> mark# X, mark# len X -> active# len mark X)
(mark# len X -> mark# X, mark# len X -> len# mark X)
(active# from X -> cons#(X, from s X), cons#(X1, mark X2) -> cons#(X1, X2))
(active# from X -> cons#(X, from s X), cons#(X1, active X2) -> cons#(X1, X2))
(active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
(active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
(active# len cons(X, Z) -> mark# s len Z, mark# nil() -> active# nil())
(active# len cons(X, Z) -> mark# s len Z, mark# fst(X1, X2) -> mark# X1)
(active# len cons(X, Z) -> mark# s len Z, mark# fst(X1, X2) -> mark# X2)
(active# len cons(X, Z) -> mark# s len Z, mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(active# len cons(X, Z) -> mark# s len Z, mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(active# len cons(X, Z) -> mark# s len Z, mark# 0() -> active# 0())
(active# len cons(X, Z) -> mark# s len Z, mark# cons(X1, X2) -> mark# X1)
(active# len cons(X, Z) -> mark# s len Z, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# len cons(X, Z) -> mark# s len Z, mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# len cons(X, Z) -> mark# s len Z, mark# s X -> active# s X)
(active# len cons(X, Z) -> mark# s len Z, mark# from X -> mark# X)
(active# len cons(X, Z) -> mark# s len Z, mark# from X -> active# from mark X)
(active# len cons(X, Z) -> mark# s len Z, mark# from X -> from# mark X)
(active# len cons(X, Z) -> mark# s len Z, mark# add(X1, X2) -> mark# X1)
(active# len cons(X, Z) -> mark# s len Z, mark# add(X1, X2) -> mark# X2)
(active# len cons(X, Z) -> mark# s len Z, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# len cons(X, Z) -> mark# s len Z, mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# len cons(X, Z) -> mark# s len Z, mark# len X -> mark# X)
(active# len cons(X, Z) -> mark# s len Z, mark# len X -> active# len mark X)
(active# len cons(X, Z) -> mark# s len Z, mark# len X -> len# mark X)
(mark# len X -> active# len mark X, active# fst(0(), Z) -> mark# nil())
(mark# len X -> active# len mark X, active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)))
(mark# len X -> active# len mark X, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
(mark# len X -> active# len mark X, active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
(mark# len X -> active# len mark X, active# from X -> mark# cons(X, from s X))
(mark# len X -> active# len mark X, active# from X -> cons#(X, from s X))
(mark# len X -> active# len mark X, active# from X -> s# X)
(mark# len X -> active# len mark X, active# from X -> from# s X)
(mark# len X -> active# len mark X, active# add(0(), X) -> mark# X)
(mark# len X -> active# len mark X, active# add(s X, Y) -> mark# s add(X, Y))
(mark# len X -> active# len mark X, active# add(s X, Y) -> s# add(X, Y))
(mark# len X -> active# len mark X, active# add(s X, Y) -> add#(X, Y))
(mark# len X -> active# len mark X, active# len nil() -> mark# 0())
(mark# len X -> active# len mark X, active# len cons(X, Z) -> mark# s len Z)
(mark# len X -> active# len mark X, active# len cons(X, Z) -> s# len Z)
(mark# len X -> active# len mark X, active# len cons(X, Z) -> len# Z)
(active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)), cons#(X1, mark X2) -> cons#(X1, X2))
(active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)), cons#(X1, active X2) -> cons#(X1, X2))
(active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)), cons#(mark X1, X2) -> cons#(X1, X2))
(active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)), cons#(active X1, X2) -> cons#(X1, X2))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fst(0(), Z) -> mark# nil())
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> mark# cons(X, from s X))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> cons#(X, from s X))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> s# X)
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> from# s X)
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# add(0(), X) -> mark# X)
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# add(s X, Y) -> mark# s add(X, Y))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# add(s X, Y) -> s# add(X, Y))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# add(s X, Y) -> add#(X, Y))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# len nil() -> mark# 0())
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# len cons(X, Z) -> mark# s len Z)
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# len cons(X, Z) -> s# len Z)
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# len cons(X, Z) -> len# Z)
(mark# add(X1, X2) -> mark# X2, mark# nil() -> active# nil())
(mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X1)
(mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X2)
(mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X2, mark# 0() -> active# 0())
(mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
(mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# add(X1, X2) -> mark# X2, mark# s X -> active# s X)
(mark# add(X1, X2) -> mark# X2, mark# from X -> mark# X)
(mark# add(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
(mark# add(X1, X2) -> mark# X2, mark# from X -> from# mark X)
(mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
(mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2)
(mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X2, mark# len X -> mark# X)
(mark# add(X1, X2) -> mark# X2, mark# len X -> active# len mark X)
(mark# add(X1, X2) -> mark# X2, mark# len X -> len# mark X)
(active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2))
(active# add(s X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2))
(active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2))
(active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2))
(add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
(add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
(add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
(add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
(add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
(add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2))
(add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
(add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
(cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
(cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
(cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
(fst#(mark X1, X2) -> fst#(X1, X2), fst#(X1, mark X2) -> fst#(X1, X2))
(fst#(mark X1, X2) -> fst#(X1, X2), fst#(X1, active X2) -> fst#(X1, X2))
(fst#(mark X1, X2) -> fst#(X1, X2), fst#(mark X1, X2) -> fst#(X1, X2))
(fst#(mark X1, X2) -> fst#(X1, X2), fst#(active X1, X2) -> fst#(X1, X2))
(fst#(X1, mark X2) -> fst#(X1, X2), fst#(X1, mark X2) -> fst#(X1, X2))
(fst#(X1, mark X2) -> fst#(X1, X2), fst#(X1, active X2) -> fst#(X1, X2))
(fst#(X1, mark X2) -> fst#(X1, X2), fst#(mark X1, X2) -> fst#(X1, X2))
(fst#(X1, mark X2) -> fst#(X1, X2), fst#(active X1, X2) -> fst#(X1, X2))
(mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(X1, X2))
(mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, active X2) -> add#(X1, X2))
(mark# add(X1, X2) -> add#(mark X1, mark X2), add#(mark X1, X2) -> add#(X1, X2))
(mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, X2) -> add#(X1, X2))
(active# len nil() -> mark# 0(), mark# nil() -> active# nil())
(active# len nil() -> mark# 0(), mark# fst(X1, X2) -> mark# X1)
(active# len nil() -> mark# 0(), mark# fst(X1, X2) -> mark# X2)
(active# len nil() -> mark# 0(), mark# fst(X1, X2) -> active# fst(mark X1, mark X2))
(active# len nil() -> mark# 0(), mark# fst(X1, X2) -> fst#(mark X1, mark X2))
(active# len nil() -> mark# 0(), mark# 0() -> active# 0())
(active# len nil() -> mark# 0(), mark# cons(X1, X2) -> mark# X1)
(active# len nil() -> mark# 0(), mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# len nil() -> mark# 0(), mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# len nil() -> mark# 0(), mark# s X -> active# s X)
(active# len nil() -> mark# 0(), mark# from X -> mark# X)
(active# len nil() -> mark# 0(), mark# from X -> active# from mark X)
(active# len nil() -> mark# 0(), mark# from X -> from# mark X)
(active# len nil() -> mark# 0(), mark# add(X1, X2) -> mark# X1)
(active# len nil() -> mark# 0(), mark# add(X1, X2) -> mark# X2)
(active# len nil() -> mark# 0(), mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# len nil() -> mark# 0(), mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# len nil() -> mark# 0(), mark# len X -> mark# X)
(active# len nil() -> mark# 0(), mark# len X -> active# len mark X)
(active# len nil() -> mark# 0(), mark# len X -> len# mark X)
(mark# 0() -> active# 0(), active# fst(0(), Z) -> mark# nil())
(mark# 0() -> active# 0(), active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)))
(mark# 0() -> active# 0(), active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
(mark# 0() -> active# 0(), active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
(mark# 0() -> active# 0(), active# from X -> mark# cons(X, from s X))
(mark# 0() -> active# 0(), active# from X -> cons#(X, from s X))
(mark# 0() -> active# 0(), active# from X -> s# X)
(mark# 0() -> active# 0(), active# from X -> from# s X)
(mark# 0() -> active# 0(), active# add(0(), X) -> mark# X)
(mark# 0() -> active# 0(), active# add(s X, Y) -> mark# s add(X, Y))
(mark# 0() -> active# 0(), active# add(s X, Y) -> s# add(X, Y))
(mark# 0() -> active# 0(), active# add(s X, Y) -> add#(X, Y))
(mark# 0() -> active# 0(), active# len nil() -> mark# 0())
(mark# 0() -> active# 0(), active# len cons(X, Z) -> mark# s len Z)
(mark# 0() -> active# 0(), active# len cons(X, Z) -> s# len Z)
(mark# 0() -> active# 0(), active# len cons(X, Z) -> len# Z)
(mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
(mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
(mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
}
STATUS:
arrows: 0.825103
SCCS (7):
Scc:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> mark# X1,
mark# fst(X1, X2) -> mark# X2,
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# 0() -> active# 0(),
mark# cons(X1, X2) -> mark# X1,
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> mark# X,
mark# from X -> active# from mark X,
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
mark# len X -> mark# X,
mark# len X -> active# len mark X,
active# fst(0(), Z) -> mark# nil(),
active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)),
active# from X -> mark# cons(X, from s X),
active# add(0(), X) -> mark# X,
active# add(s X, Y) -> mark# s add(X, Y),
active# len nil() -> mark# 0(),
active# len cons(X, Z) -> mark# s len Z}
Scc:
{ len# mark X -> len# X,
len# active X -> len# X}
Scc:
{ add#(X1, mark X2) -> add#(X1, X2),
add#(X1, active X2) -> add#(X1, X2),
add#(mark X1, X2) -> add#(X1, X2),
add#(active X1, X2) -> add#(X1, X2)}
Scc:
{ from# mark X -> from# X,
from# active X -> from# X}
Scc:
{ s# mark X -> s# X,
s# active X -> s# X}
Scc:
{ fst#(X1, mark X2) -> fst#(X1, X2),
fst#(X1, active X2) -> fst#(X1, X2),
fst#(mark X1, X2) -> fst#(X1, X2),
fst#(active X1, X2) -> fst#(X1, X2)}
Scc:
{ cons#(X1, mark X2) -> cons#(X1, X2),
cons#(X1, active X2) -> cons#(X1, X2),
cons#(mark X1, X2) -> cons#(X1, X2),
cons#(active X1, X2) -> cons#(X1, X2)}
SCC (22):
Strict:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> mark# X1,
mark# fst(X1, X2) -> mark# X2,
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# 0() -> active# 0(),
mark# cons(X1, X2) -> mark# X1,
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> mark# X,
mark# from X -> active# from mark X,
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
mark# len X -> mark# X,
mark# len X -> active# len mark X,
active# fst(0(), Z) -> mark# nil(),
active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z)),
active# from X -> mark# cons(X, from s X),
active# add(0(), X) -> mark# X,
active# add(s X, Y) -> mark# s add(X, Y),
active# len nil() -> mark# 0(),
active# len cons(X, Z) -> mark# s len Z}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0 + x1 + 1,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = x0 + x1,
[mark](x0) = x0,
[active](x0) = x0,
[s](x0) = 0,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 1,
[0] = 0,
[mark#](x0) = x0,
[active#](x0) = x0
Strict:
active# len cons(X, Z) -> mark# s len Z
2 + 0Z + 1X >= 0 + 0Z
active# len nil() -> mark# 0()
2 >= 0
active# add(s X, Y) -> mark# s add(X, Y)
0 + 1Y + 0X >= 0 + 0Y + 0X
active# add(0(), X) -> mark# X
0 + 1X >= 0 + 1X
active# from X -> mark# cons(X, from s X)
1 + 1X >= 1 + 1X
active# fst(s X, cons(Y, Z)) -> mark# cons(Y, fst(X, Z))
2 + 0Z + 1Y + 0X >= 1 + 0Z + 1Y + 0X
active# fst(0(), Z) -> mark# nil()
1 + 1Z >= 1
mark# len X -> active# len mark X
1 + 1X >= 1 + 1X
mark# len X -> mark# X
1 + 1X >= 0 + 1X
mark# add(X1, X2) -> active# add(mark X1, mark X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
mark# add(X1, X2) -> mark# X2
0 + 1X1 + 1X2 >= 0 + 1X2
mark# add(X1, X2) -> mark# X1
0 + 1X1 + 1X2 >= 0 + 1X1
mark# from X -> active# from mark X
1 + 1X >= 1 + 1X
mark# from X -> mark# X
1 + 1X >= 0 + 1X
mark# s X -> active# s X
0 + 0X >= 0 + 0X
mark# cons(X1, X2) -> active# cons(mark X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
mark# cons(X1, X2) -> mark# X1
1 + 1X1 + 0X2 >= 0 + 1X1
mark# 0() -> active# 0()
0 >= 0
mark# fst(X1, X2) -> active# fst(mark X1, mark X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
mark# fst(X1, X2) -> mark# X2
1 + 1X1 + 1X2 >= 0 + 1X2
mark# fst(X1, X2) -> mark# X1
1 + 1X1 + 1X2 >= 0 + 1X1
mark# nil() -> active# nil()
1 >= 1
Weak:
len active X -> len X
1 + 1X >= 1 + 1X
len mark X -> len X
1 + 1X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
add(mark X1, X2) -> add(X1, X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
add(X1, active X2) -> add(X1, X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
add(X1, mark X2) -> add(X1, X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
from active X -> from X
1 + 1X >= 1 + 1X
from mark X -> from X
1 + 1X >= 1 + 1X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
fst(X1, active X2) -> fst(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
active len cons(X, Z) -> mark s len Z
2 + 0Z + 1X >= 0 + 0Z
active len nil() -> mark 0()
2 >= 0
active add(s X, Y) -> mark s add(X, Y)
0 + 1Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
0 + 1X >= 0 + 1X
active from X -> mark cons(X, from s X)
1 + 1X >= 1 + 1X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 1Y + 0X >= 1 + 0Z + 1Y + 0X
active fst(0(), Z) -> mark nil()
1 + 1Z >= 1
mark len X -> active len mark X
1 + 1X >= 1 + 1X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
mark from X -> active from mark X
1 + 1X >= 1 + 1X
mark s X -> active s X
0 + 0X >= 0 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
mark 0() -> active 0()
0 >= 0
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
mark nil() -> active nil()
1 >= 1
SCCS (1):
Scc:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# 0() -> active# 0(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> active# from mark X,
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
mark# len X -> active# len mark X,
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X),
active# add(0(), X) -> mark# X,
active# add(s X, Y) -> mark# s add(X, Y)}
SCC (14):
Strict:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# 0() -> active# 0(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> active# from mark X,
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
mark# len X -> active# len mark X,
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X),
active# add(0(), X) -> mark# X,
active# add(s X, Y) -> mark# s add(X, Y)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = x0 + x1 + 1,
[mark](x0) = x0,
[active](x0) = x0,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 0,
[0] = 0,
[mark#](x0) = x0,
[active#](x0) = x0
Strict:
active# add(s X, Y) -> mark# s add(X, Y)
1 + 1Y + 0X >= 0 + 0Y + 0X
active# add(0(), X) -> mark# X
1 + 1X >= 0 + 1X
active# from X -> mark# cons(X, from s X)
0 + 0X >= 0 + 0X
active# fst(0(), Z) -> mark# nil()
0 + 0Z >= 0
mark# len X -> active# len mark X
0 + 0X >= 0 + 0X
mark# add(X1, X2) -> active# add(mark X1, mark X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
mark# add(X1, X2) -> mark# X2
1 + 1X1 + 1X2 >= 0 + 1X2
mark# add(X1, X2) -> mark# X1
1 + 1X1 + 1X2 >= 0 + 1X1
mark# from X -> active# from mark X
0 + 0X >= 0 + 0X
mark# s X -> active# s X
0 + 0X >= 0 + 0X
mark# cons(X1, X2) -> active# cons(mark X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# 0() -> active# 0()
0 >= 0
mark# fst(X1, X2) -> active# fst(mark X1, mark X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# nil() -> active# nil()
0 >= 0
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
add(mark X1, X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
add(X1, active X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
0 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
0 >= 0
active add(s X, Y) -> mark s add(X, Y)
1 + 1Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
1 + 1X >= 0 + 1X
active from X -> mark cons(X, from s X)
0 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
0 + 0Z + 0Y + 0X >= 0 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
0 + 0Z >= 0
mark len X -> active len mark X
0 + 0X >= 0 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
mark from X -> active from mark X
0 + 0X >= 0 + 0X
mark s X -> active s X
0 + 0X >= 0 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark 0() -> active 0()
0 >= 0
mark fst(X1, X2) -> active fst(mark X1, mark X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark nil() -> active nil()
0 >= 0
SCCS (1):
Scc:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# 0() -> active# 0(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> active# from mark X,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
mark# len X -> active# len mark X,
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
SCC (10):
Strict:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# 0() -> active# 0(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> active# from mark X,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
mark# len X -> active# len mark X,
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = 0,
[mark](x0) = 0,
[active](x0) = 0,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 1,
[nil] = 0,
[0] = 0,
[mark#](x0) = x0 + 1,
[active#](x0) = 1
Strict:
active# from X -> mark# cons(X, from s X)
1 + 0X >= 1 + 0X
active# fst(0(), Z) -> mark# nil()
1 + 0Z >= 1
mark# len X -> active# len mark X
2 + 0X >= 1 + 0X
mark# add(X1, X2) -> active# add(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# from X -> active# from mark X
1 + 0X >= 1 + 0X
mark# s X -> active# s X
1 + 0X >= 1 + 0X
mark# cons(X1, X2) -> active# cons(mark X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# 0() -> active# 0()
1 >= 1
mark# fst(X1, X2) -> active# fst(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# nil() -> active# nil()
1 >= 1
Weak:
len active X -> len X
1 + 0X >= 1 + 0X
len mark X -> len X
1 + 0X >= 1 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
0 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
0 >= 0
active add(s X, Y) -> mark s add(X, Y)
0 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
0 + 0X >= 0 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
0 + 0Z + 0Y + 0X >= 0 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
0 + 0Z >= 0
mark len X -> active len mark X
0 + 0X >= 0 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 0 + 0X
mark s X -> active s X
0 + 0X >= 0 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark 0() -> active 0()
0 >= 0
mark fst(X1, X2) -> active fst(mark X1, mark X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark nil() -> active nil()
0 >= 0
SCCS (1):
Scc:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# 0() -> active# 0(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> active# from mark X,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
SCC (9):
Strict:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# 0() -> active# 0(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> active# from mark X,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = 0,
[mark](x0) = 0,
[active](x0) = 0,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 0,
[0] = 1,
[mark#](x0) = x0 + 1,
[active#](x0) = 1
Strict:
active# from X -> mark# cons(X, from s X)
1 + 0X >= 1 + 0X
active# fst(0(), Z) -> mark# nil()
1 + 0Z >= 1
mark# add(X1, X2) -> active# add(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# from X -> active# from mark X
1 + 0X >= 1 + 0X
mark# s X -> active# s X
1 + 0X >= 1 + 0X
mark# cons(X1, X2) -> active# cons(mark X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# 0() -> active# 0()
2 >= 1
mark# fst(X1, X2) -> active# fst(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# nil() -> active# nil()
1 >= 1
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
0 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
0 >= 0
active add(s X, Y) -> mark s add(X, Y)
0 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
0 + 0X >= 0 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
0 + 0Z + 0Y + 0X >= 0 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
0 + 0Z >= 0
mark len X -> active len mark X
0 + 0X >= 0 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 0 + 0X
mark s X -> active s X
0 + 0X >= 0 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark 0() -> active 0()
0 >= 0
mark fst(X1, X2) -> active fst(mark X1, mark X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark nil() -> active nil()
0 >= 0
SCCS (1):
Scc:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> active# from mark X,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
SCC (8):
Strict:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# s X -> active# s X,
mark# from X -> active# from mark X,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = x0,
[mark](x0) = 1,
[active](x0) = 0,
[s](x0) = x0 + 1,
[from](x0) = 0,
[len](x0) = x0 + 1,
[nil] = 0,
[0] = 0,
[mark#](x0) = x0 + 1,
[active#](x0) = 1
Strict:
active# from X -> mark# cons(X, from s X)
1 + 0X >= 1 + 0X
active# fst(0(), Z) -> mark# nil()
1 + 0Z >= 1
mark# add(X1, X2) -> active# add(mark X1, mark X2)
1 + 1X1 + 0X2 >= 1 + 0X1 + 0X2
mark# from X -> active# from mark X
1 + 0X >= 1 + 0X
mark# s X -> active# s X
2 + 1X >= 1 + 0X
mark# cons(X1, X2) -> active# cons(mark X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# fst(X1, X2) -> active# fst(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# nil() -> active# nil()
1 >= 1
Weak:
len active X -> len X
1 + 0X >= 1 + 1X
len mark X -> len X
2 + 0X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
1 + 0X >= 1 + 1X
s mark X -> s X
2 + 0X >= 1 + 1X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
0 + 0Z + 0X >= 1 + 0Z
active len nil() -> mark 0()
0 >= 1
active add(s X, Y) -> mark s add(X, Y)
0 + 0Y + 0X >= 1 + 0Y + 0X
active add(0(), X) -> mark X
0 + 0X >= 1 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 1 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
0 + 0Z + 0Y + 0X >= 1 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
0 + 0Z >= 1
mark len X -> active len mark X
1 + 0X >= 0 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark from X -> active from mark X
1 + 0X >= 0 + 0X
mark s X -> active s X
1 + 0X >= 0 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark 0() -> active 0()
1 >= 0
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark nil() -> active nil()
1 >= 0
SCCS (1):
Scc:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# from X -> active# from mark X,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
SCC (7):
Strict:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# from X -> active# from mark X,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = x0 + x1,
[mark](x0) = x0 + 1,
[active](x0) = 0,
[s](x0) = x0 + 1,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 0,
[0] = 0,
[mark#](x0) = x0,
[active#](x0) = 0
Strict:
active# from X -> mark# cons(X, from s X)
0 + 0X >= 0 + 0X
active# fst(0(), Z) -> mark# nil()
0 + 0Z >= 0
mark# add(X1, X2) -> active# add(mark X1, mark X2)
0 + 1X1 + 1X2 >= 0 + 0X1 + 0X2
mark# from X -> active# from mark X
1 + 1X >= 0 + 0X
mark# cons(X1, X2) -> active# cons(mark X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# fst(X1, X2) -> active# fst(mark X1, mark X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# nil() -> active# nil()
0 >= 0
Weak:
len active X -> len X
1 + 0X >= 1 + 1X
len mark X -> len X
2 + 1X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 1X2 >= 0 + 1X1 + 1X2
add(mark X1, X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
add(X1, active X2) -> add(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 1X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
from active X -> from X
1 + 0X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
0 + 0Z + 0X >= 3 + 1Z
active len nil() -> mark 0()
0 >= 1
active add(s X, Y) -> mark s add(X, Y)
0 + 0Y + 0X >= 2 + 1Y + 1X
active add(0(), X) -> mark X
0 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
0 + 0X >= 1 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
0 + 0Z + 0Y + 0X >= 1 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
0 + 0Z >= 1
mark len X -> active len mark X
2 + 1X >= 0 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
1 + 1X1 + 1X2 >= 0 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 0 + 0X
mark s X -> active s X
2 + 1X >= 0 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark 0() -> active 0()
1 >= 0
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark nil() -> active nil()
1 >= 0
SCCS (1):
Scc:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
SCC (6):
Strict:
{ mark# nil() -> active# nil(),
mark# fst(X1, X2) -> active# fst(mark X1, mark X2),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 1,
[cons](x0, x1) = 0,
[add](x0, x1) = x0 + x1,
[mark](x0) = x0 + 1,
[active](x0) = 0,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 0,
[0] = 0,
[mark#](x0) = x0,
[active#](x0) = 0
Strict:
active# from X -> mark# cons(X, from s X)
0 + 0X >= 0 + 0X
active# fst(0(), Z) -> mark# nil()
0 + 0Z >= 0
mark# add(X1, X2) -> active# add(mark X1, mark X2)
0 + 1X1 + 1X2 >= 0 + 0X1 + 0X2
mark# cons(X1, X2) -> active# cons(mark X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# fst(X1, X2) -> active# fst(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# nil() -> active# nil()
0 >= 0
Weak:
len active X -> len X
1 + 0X >= 1 + 1X
len mark X -> len X
2 + 1X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 1X2 >= 0 + 1X1 + 1X2
add(mark X1, X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
add(X1, active X2) -> add(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 1X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
from active X -> from X
1 + 0X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
0 + 0Z + 0X >= 2 + 0Z
active len nil() -> mark 0()
0 >= 1
active add(s X, Y) -> mark s add(X, Y)
0 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
0 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
0 + 0X >= 1 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
0 + 0Z + 0Y + 0X >= 1 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
0 + 0Z >= 1
mark len X -> active len mark X
2 + 1X >= 0 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
1 + 1X1 + 1X2 >= 0 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 0 + 0X
mark s X -> active s X
2 + 0X >= 0 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark 0() -> active 0()
1 >= 0
mark fst(X1, X2) -> active fst(mark X1, mark X2)
2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark nil() -> active nil()
1 >= 0
SCCS (1):
Scc:
{ mark# nil() -> active# nil(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
SCC (5):
Strict:
{ mark# nil() -> active# nil(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# fst(0(), Z) -> mark# nil(),
active# from X -> mark# cons(X, from s X)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0 + 1,
[cons](x0, x1) = 0,
[add](x0, x1) = 0,
[mark](x0) = x0 + 1,
[active](x0) = 1,
[s](x0) = 1,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 0,
[0] = 1,
[mark#](x0) = 0,
[active#](x0) = x0
Strict:
active# from X -> mark# cons(X, from s X)
0 + 0X >= 0 + 0X
active# fst(0(), Z) -> mark# nil()
2 + 0Z >= 0
mark# add(X1, X2) -> active# add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# cons(X1, X2) -> active# cons(mark X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# nil() -> active# nil()
0 >= 0
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
2 + 0X1 + 0X2 >= 1 + 1X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 2 + 0Z
active len nil() -> mark 0()
1 >= 2
active add(s X, Y) -> mark s add(X, Y)
1 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
1 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
1 + 0X >= 1 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
1 + 0Z + 0Y + 0X >= 1 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
1 + 0Z >= 1
mark len X -> active len mark X
1 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
1 + 0X >= 1 + 0X
mark s X -> active s X
2 + 0X >= 1 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark 0() -> active 0()
2 >= 1
mark fst(X1, X2) -> active fst(mark X1, mark X2)
2 + 1X1 + 0X2 >= 1 + 0X1 + 0X2
mark nil() -> active nil()
1 >= 1
SCCS (1):
Scc:
{ mark# nil() -> active# nil(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# from X -> mark# cons(X, from s X)}
SCC (4):
Strict:
{ mark# nil() -> active# nil(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# from X -> mark# cons(X, from s X)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0 + 1,
[cons](x0, x1) = 0,
[add](x0, x1) = x0 + 1,
[mark](x0) = 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 0,
[0] = 1,
[mark#](x0) = x0,
[active#](x0) = 0
Strict:
active# from X -> mark# cons(X, from s X)
0 + 0X >= 0 + 0X
mark# add(X1, X2) -> active# add(mark X1, mark X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
mark# cons(X1, X2) -> active# cons(mark X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# nil() -> active# nil()
0 >= 0
Weak:
len active X -> len X
2 + 1X >= 1 + 1X
len mark X -> len X
2 + 0X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
add(X1, active X2) -> add(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
add(X1, mark X2) -> add(X1, X2)
2 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 0X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
2 + 0X1 + 0X2 >= 1 + 1X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
active len cons(X, Z) -> mark s len Z
2 + 0Z + 0X >= 1 + 0Z
active len nil() -> mark 0()
2 >= 1
active add(s X, Y) -> mark s add(X, Y)
2 + 1Y + 0X >= 1 + 0Y + 0X
active add(0(), X) -> mark X
2 + 1X >= 1 + 0X
active from X -> mark cons(X, from s X)
2 + 1X >= 1 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
3 + 0Z + 0Y + 0X >= 1 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
3 + 0Z >= 1
mark len X -> active len mark X
1 + 0X >= 3 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
1 + 0X1 + 0X2 >= 3 + 0X1 + 0X2
mark from X -> active from mark X
1 + 0X >= 3 + 0X
mark s X -> active s X
1 + 0X >= 2 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark 0() -> active 0()
1 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 0X2 >= 3 + 0X1 + 0X2
mark nil() -> active nil()
1 >= 1
SCCS (1):
Scc:
{ mark# nil() -> active# nil(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
active# from X -> mark# cons(X, from s X)}
SCC (3):
Strict:
{ mark# nil() -> active# nil(),
mark# cons(X1, X2) -> active# cons(mark X1, X2),
active# from X -> mark# cons(X, from s X)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = x0,
[mark](x0) = 0,
[active](x0) = x0 + 1,
[s](x0) = x0 + 1,
[from](x0) = 0,
[len](x0) = x0,
[nil] = 1,
[0] = 1,
[mark#](x0) = x0,
[active#](x0) = 0
Strict:
active# from X -> mark# cons(X, from s X)
0 + 0X >= 0 + 0X
mark# cons(X1, X2) -> active# cons(mark X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# nil() -> active# nil()
1 >= 0
Weak:
len active X -> len X
1 + 1X >= 0 + 1X
len mark X -> len X
0 + 0X >= 0 + 1X
add(active X1, X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
2 + 1X >= 1 + 1X
s mark X -> s X
1 + 0X >= 1 + 1X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
2 >= 0
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 1X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 0 + 0X
active from X -> mark cons(X, from s X)
1 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
1 + 0Z + 0Y + 0X >= 0 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
1 + 0Z >= 0
mark len X -> active len mark X
0 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 1 + 0X
mark s X -> active s X
0 + 0X >= 2 + 1X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark 0() -> active 0()
0 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark nil() -> active nil()
0 >= 2
SCCS (1):
Scc:
{mark# cons(X1, X2) -> active# cons(mark X1, X2),
active# from X -> mark# cons(X, from s X)}
SCC (2):
Strict:
{mark# cons(X1, X2) -> active# cons(mark X1, X2),
active# from X -> mark# cons(X, from s X)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 1,
[cons](x0, x1) = 0,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = x0 + 1,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 1,
[0] = 1,
[mark#](x0) = 0,
[active#](x0) = x0
Strict:
active# from X -> mark# cons(X, from s X)
1 + 1X >= 0 + 0X
mark# cons(X1, X2) -> active# cons(mark X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
Weak:
len active X -> len X
2 + 1X >= 1 + 1X
len mark X -> len X
2 + 1X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
2 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
2 + 0Z + 0X >= 3 + 1Z
active len nil() -> mark 0()
3 >= 2
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 0X >= 3 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
2 + 1X >= 1 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 0Y + 0X >= 1 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
2 + 0Z >= 2
mark len X -> active len mark X
2 + 1X >= 3 + 1X
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 3 + 1X
mark s X -> active s X
2 + 1X >= 2 + 1X
mark cons(X1, X2) -> active cons(mark X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark 0() -> active 0()
2 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark nil() -> active nil()
2 >= 2
SCCS (0):
SCC (2):
Strict:
{ len# mark X -> len# X,
len# active X -> len# X}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0 + 1,
[cons](x0, x1) = x0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[len#](x0) = x0
Strict:
len# active X -> len# X
1 + 1X >= 0 + 1X
len# mark X -> len# X
0 + 1X >= 0 + 1X
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(active X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, active X2) -> fst(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
1 >= 1
active add(s X, Y) -> mark s add(X, Y)
1 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active from X -> mark cons(X, from s X)
1 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 1Z + 0Y + 0X >= 1 + 1Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
2 + 1Z >= 1
mark len X -> active len mark X
0 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 1 + 0X
mark s X -> active s X
0 + 0X >= 1 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
mark 0() -> active 0()
1 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark nil() -> active nil()
1 >= 2
SCCS (1):
Scc:
{len# mark X -> len# X}
SCC (1):
Strict:
{len# mark X -> len# X}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 1,
[0] = 1,
[len#](x0) = x0
Strict:
len# mark X -> len# X
1 + 1X >= 0 + 1X
Weak:
len active X -> len X
2 + 1X >= 1 + 1X
len mark X -> len X
2 + 1X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
active len cons(X, Z) -> mark s len Z
3 + 0Z + 1X >= 2 + 0Z
active len nil() -> mark 0()
3 >= 2
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
2 + 1X >= 2 + 1X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 0Y + 0X >= 2 + 0Z + 1Y + 0X
active fst(0(), Z) -> mark nil()
2 + 0Z >= 2
mark len X -> active len mark X
2 + 1X >= 3 + 1X
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 3 + 1X
mark s X -> active s X
2 + 0X >= 2 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 3 + 1X1 + 0X2
mark 0() -> active 0()
2 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark nil() -> active nil()
2 >= 2
Qed
SCC (4):
Strict:
{ add#(X1, mark X2) -> add#(X1, X2),
add#(X1, active X2) -> add#(X1, X2),
add#(mark X1, X2) -> add#(X1, X2),
add#(active X1, X2) -> add#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[add#](x0, x1) = x0
Strict:
add#(active X1, X2) -> add#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
add#(mark X1, X2) -> add#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
add#(X1, active X2) -> add#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
add#(X1, mark X2) -> add#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
1 >= 1
active add(s X, Y) -> mark s add(X, Y)
1 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active from X -> mark cons(X, from s X)
1 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
1 + 0Z + 0Y + 0X >= 0 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
1 + 0Z >= 1
mark len X -> active len mark X
0 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 1 + 0X
mark s X -> active s X
0 + 0X >= 1 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark 0() -> active 0()
1 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark nil() -> active nil()
1 >= 2
SCCS (1):
Scc:
{ add#(X1, mark X2) -> add#(X1, X2),
add#(X1, active X2) -> add#(X1, X2),
add#(mark X1, X2) -> add#(X1, X2)}
SCC (3):
Strict:
{ add#(X1, mark X2) -> add#(X1, X2),
add#(X1, active X2) -> add#(X1, X2),
add#(mark X1, X2) -> add#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[add#](x0, x1) = x0
Strict:
add#(mark X1, X2) -> add#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
add#(X1, active X2) -> add#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
add#(X1, mark X2) -> add#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(X1, active X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 2 + 0Z
active len nil() -> mark 0()
1 >= 2
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
2 + 1X >= 2 + 1X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 1Y + 0X >= 2 + 0Z + 1Y + 0X
active fst(0(), Z) -> mark nil()
1 + 1Z >= 2
mark len X -> active len mark X
1 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 3 + 1X
mark s X -> active s X
2 + 0X >= 2 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 3 + 1X1 + 0X2
mark 0() -> active 0()
2 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark nil() -> active nil()
2 >= 2
SCCS (1):
Scc:
{ add#(X1, mark X2) -> add#(X1, X2),
add#(X1, active X2) -> add#(X1, X2)}
SCC (2):
Strict:
{ add#(X1, mark X2) -> add#(X1, X2),
add#(X1, active X2) -> add#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0 + 1,
[cons](x0, x1) = x0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[add#](x0, x1) = x0
Strict:
add#(X1, active X2) -> add#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
add#(X1, mark X2) -> add#(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(active X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, active X2) -> fst(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
1 >= 1
active add(s X, Y) -> mark s add(X, Y)
1 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active from X -> mark cons(X, from s X)
1 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 1Z + 0Y + 0X >= 1 + 1Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
2 + 1Z >= 1
mark len X -> active len mark X
0 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 1 + 0X
mark s X -> active s X
0 + 0X >= 1 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
mark 0() -> active 0()
1 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark nil() -> active nil()
1 >= 2
SCCS (1):
Scc:
{add#(X1, mark X2) -> add#(X1, X2)}
SCC (1):
Strict:
{add#(X1, mark X2) -> add#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 1,
[0] = 1,
[add#](x0, x1) = x0
Strict:
add#(X1, mark X2) -> add#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
len active X -> len X
2 + 1X >= 1 + 1X
len mark X -> len X
2 + 1X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
active len cons(X, Z) -> mark s len Z
3 + 0Z + 1X >= 2 + 0Z
active len nil() -> mark 0()
3 >= 2
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
2 + 1X >= 2 + 1X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 0Y + 0X >= 2 + 0Z + 1Y + 0X
active fst(0(), Z) -> mark nil()
2 + 0Z >= 2
mark len X -> active len mark X
2 + 1X >= 3 + 1X
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 3 + 1X
mark s X -> active s X
2 + 0X >= 2 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 3 + 1X1 + 0X2
mark 0() -> active 0()
2 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark nil() -> active nil()
2 >= 2
Qed
SCC (2):
Strict:
{ from# mark X -> from# X,
from# active X -> from# X}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0 + 1,
[cons](x0, x1) = x0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[from#](x0) = x0
Strict:
from# active X -> from# X
1 + 1X >= 0 + 1X
from# mark X -> from# X
0 + 1X >= 0 + 1X
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(active X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, active X2) -> fst(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
1 >= 1
active add(s X, Y) -> mark s add(X, Y)
1 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active from X -> mark cons(X, from s X)
1 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 1Z + 0Y + 0X >= 1 + 1Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
2 + 1Z >= 1
mark len X -> active len mark X
0 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 1 + 0X
mark s X -> active s X
0 + 0X >= 1 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
mark 0() -> active 0()
1 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark nil() -> active nil()
1 >= 2
SCCS (1):
Scc:
{from# mark X -> from# X}
SCC (1):
Strict:
{from# mark X -> from# X}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 1,
[0] = 1,
[from#](x0) = x0
Strict:
from# mark X -> from# X
1 + 1X >= 0 + 1X
Weak:
len active X -> len X
2 + 1X >= 1 + 1X
len mark X -> len X
2 + 1X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
active len cons(X, Z) -> mark s len Z
3 + 0Z + 1X >= 2 + 0Z
active len nil() -> mark 0()
3 >= 2
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
2 + 1X >= 2 + 1X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 0Y + 0X >= 2 + 0Z + 1Y + 0X
active fst(0(), Z) -> mark nil()
2 + 0Z >= 2
mark len X -> active len mark X
2 + 1X >= 3 + 1X
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 3 + 1X
mark s X -> active s X
2 + 0X >= 2 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 3 + 1X1 + 0X2
mark 0() -> active 0()
2 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark nil() -> active nil()
2 >= 2
Qed
SCC (2):
Strict:
{ s# mark X -> s# X,
s# active X -> s# X}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0 + 1,
[cons](x0, x1) = x0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[s#](x0) = x0
Strict:
s# active X -> s# X
1 + 1X >= 0 + 1X
s# mark X -> s# X
0 + 1X >= 0 + 1X
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(active X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, active X2) -> fst(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
1 >= 1
active add(s X, Y) -> mark s add(X, Y)
1 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active from X -> mark cons(X, from s X)
1 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 1Z + 0Y + 0X >= 1 + 1Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
2 + 1Z >= 1
mark len X -> active len mark X
0 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 1 + 0X
mark s X -> active s X
0 + 0X >= 1 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
mark 0() -> active 0()
1 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark nil() -> active nil()
1 >= 2
SCCS (1):
Scc:
{s# mark X -> s# X}
SCC (1):
Strict:
{s# mark X -> s# X}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 1,
[0] = 1,
[s#](x0) = x0
Strict:
s# mark X -> s# X
1 + 1X >= 0 + 1X
Weak:
len active X -> len X
2 + 1X >= 1 + 1X
len mark X -> len X
2 + 1X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
active len cons(X, Z) -> mark s len Z
3 + 0Z + 1X >= 2 + 0Z
active len nil() -> mark 0()
3 >= 2
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
2 + 1X >= 2 + 1X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 0Y + 0X >= 2 + 0Z + 1Y + 0X
active fst(0(), Z) -> mark nil()
2 + 0Z >= 2
mark len X -> active len mark X
2 + 1X >= 3 + 1X
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 3 + 1X
mark s X -> active s X
2 + 0X >= 2 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 3 + 1X1 + 0X2
mark 0() -> active 0()
2 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark nil() -> active nil()
2 >= 2
Qed
SCC (4):
Strict:
{ fst#(X1, mark X2) -> fst#(X1, X2),
fst#(X1, active X2) -> fst#(X1, X2),
fst#(mark X1, X2) -> fst#(X1, X2),
fst#(active X1, X2) -> fst#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[fst#](x0, x1) = x0
Strict:
fst#(active X1, X2) -> fst#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst#(mark X1, X2) -> fst#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst#(X1, active X2) -> fst#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst#(X1, mark X2) -> fst#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
1 >= 1
active add(s X, Y) -> mark s add(X, Y)
1 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active from X -> mark cons(X, from s X)
1 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
1 + 0Z + 0Y + 0X >= 0 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
1 + 0Z >= 1
mark len X -> active len mark X
0 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 1 + 0X
mark s X -> active s X
0 + 0X >= 1 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark 0() -> active 0()
1 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark nil() -> active nil()
1 >= 2
SCCS (1):
Scc:
{ fst#(X1, mark X2) -> fst#(X1, X2),
fst#(X1, active X2) -> fst#(X1, X2),
fst#(mark X1, X2) -> fst#(X1, X2)}
SCC (3):
Strict:
{ fst#(X1, mark X2) -> fst#(X1, X2),
fst#(X1, active X2) -> fst#(X1, X2),
fst#(mark X1, X2) -> fst#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[fst#](x0, x1) = x0
Strict:
fst#(mark X1, X2) -> fst#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst#(X1, active X2) -> fst#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst#(X1, mark X2) -> fst#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(X1, active X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 2 + 0Z
active len nil() -> mark 0()
1 >= 2
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
2 + 1X >= 2 + 1X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 1Y + 0X >= 2 + 0Z + 1Y + 0X
active fst(0(), Z) -> mark nil()
1 + 1Z >= 2
mark len X -> active len mark X
1 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 3 + 1X
mark s X -> active s X
2 + 0X >= 2 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 3 + 1X1 + 0X2
mark 0() -> active 0()
2 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark nil() -> active nil()
2 >= 2
SCCS (1):
Scc:
{ fst#(X1, mark X2) -> fst#(X1, X2),
fst#(X1, active X2) -> fst#(X1, X2)}
SCC (2):
Strict:
{ fst#(X1, mark X2) -> fst#(X1, X2),
fst#(X1, active X2) -> fst#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0 + 1,
[cons](x0, x1) = x0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[fst#](x0, x1) = x0
Strict:
fst#(X1, active X2) -> fst#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst#(X1, mark X2) -> fst#(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(active X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, active X2) -> fst(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
1 >= 1
active add(s X, Y) -> mark s add(X, Y)
1 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active from X -> mark cons(X, from s X)
1 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 1Z + 0Y + 0X >= 1 + 1Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
2 + 1Z >= 1
mark len X -> active len mark X
0 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 1 + 0X
mark s X -> active s X
0 + 0X >= 1 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
mark 0() -> active 0()
1 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark nil() -> active nil()
1 >= 2
SCCS (1):
Scc:
{fst#(X1, mark X2) -> fst#(X1, X2)}
SCC (1):
Strict:
{fst#(X1, mark X2) -> fst#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 1,
[0] = 1,
[fst#](x0, x1) = x0
Strict:
fst#(X1, mark X2) -> fst#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
len active X -> len X
2 + 1X >= 1 + 1X
len mark X -> len X
2 + 1X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
active len cons(X, Z) -> mark s len Z
3 + 0Z + 1X >= 2 + 0Z
active len nil() -> mark 0()
3 >= 2
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
2 + 1X >= 2 + 1X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 0Y + 0X >= 2 + 0Z + 1Y + 0X
active fst(0(), Z) -> mark nil()
2 + 0Z >= 2
mark len X -> active len mark X
2 + 1X >= 3 + 1X
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 3 + 1X
mark s X -> active s X
2 + 0X >= 2 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 3 + 1X1 + 0X2
mark 0() -> active 0()
2 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark nil() -> active nil()
2 >= 2
Qed
SCC (4):
Strict:
{ cons#(X1, mark X2) -> cons#(X1, X2),
cons#(X1, active X2) -> cons#(X1, X2),
cons#(mark X1, X2) -> cons#(X1, X2),
cons#(active X1, X2) -> cons#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[cons#](x0, x1) = x0
Strict:
cons#(active X1, X2) -> cons#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
cons#(mark X1, X2) -> cons#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
cons#(X1, active X2) -> cons#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
cons#(X1, mark X2) -> cons#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
1 >= 1
active add(s X, Y) -> mark s add(X, Y)
1 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active from X -> mark cons(X, from s X)
1 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
1 + 0Z + 0Y + 0X >= 0 + 0Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
1 + 0Z >= 1
mark len X -> active len mark X
0 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 1 + 0X
mark s X -> active s X
0 + 0X >= 1 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark 0() -> active 0()
1 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark nil() -> active nil()
1 >= 2
SCCS (1):
Scc:
{ cons#(X1, mark X2) -> cons#(X1, X2),
cons#(X1, active X2) -> cons#(X1, X2),
cons#(mark X1, X2) -> cons#(X1, X2)}
SCC (3):
Strict:
{ cons#(X1, mark X2) -> cons#(X1, X2),
cons#(X1, active X2) -> cons#(X1, X2),
cons#(mark X1, X2) -> cons#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[cons#](x0, x1) = x0
Strict:
cons#(mark X1, X2) -> cons#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
cons#(X1, active X2) -> cons#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
cons#(X1, mark X2) -> cons#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(mark X1, X2) -> fst(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(X1, active X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 2 + 0Z
active len nil() -> mark 0()
1 >= 2
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
2 + 1X >= 2 + 1X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 1Y + 0X >= 2 + 0Z + 1Y + 0X
active fst(0(), Z) -> mark nil()
1 + 1Z >= 2
mark len X -> active len mark X
1 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 3 + 1X
mark s X -> active s X
2 + 0X >= 2 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 3 + 1X1 + 0X2
mark 0() -> active 0()
2 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark nil() -> active nil()
2 >= 2
SCCS (1):
Scc:
{ cons#(X1, mark X2) -> cons#(X1, X2),
cons#(X1, active X2) -> cons#(X1, X2)}
SCC (2):
Strict:
{ cons#(X1, mark X2) -> cons#(X1, X2),
cons#(X1, active X2) -> cons#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0 + 1,
[cons](x0, x1) = x0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = 0,
[from](x0) = 0,
[len](x0) = 0,
[nil] = 1,
[0] = 1,
[cons#](x0, x1) = x0
Strict:
cons#(X1, active X2) -> cons#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons#(X1, mark X2) -> cons#(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
len active X -> len X
0 + 0X >= 0 + 0X
len mark X -> len X
0 + 0X >= 0 + 0X
add(active X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
from active X -> from X
0 + 0X >= 0 + 0X
from mark X -> from X
0 + 0X >= 0 + 0X
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
cons(active X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fst(active X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, active X2) -> fst(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fst(X1, mark X2) -> fst(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active len cons(X, Z) -> mark s len Z
1 + 0Z + 0X >= 0 + 0Z
active len nil() -> mark 0()
1 >= 1
active add(s X, Y) -> mark s add(X, Y)
1 + 0Y + 0X >= 0 + 0Y + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active from X -> mark cons(X, from s X)
1 + 0X >= 0 + 0X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 1Z + 0Y + 0X >= 1 + 1Z + 0Y + 0X
active fst(0(), Z) -> mark nil()
2 + 1Z >= 1
mark len X -> active len mark X
0 + 0X >= 1 + 0X
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark from X -> active from mark X
0 + 0X >= 1 + 0X
mark s X -> active s X
0 + 0X >= 1 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
mark 0() -> active 0()
1 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark nil() -> active nil()
1 >= 2
SCCS (1):
Scc:
{cons#(X1, mark X2) -> cons#(X1, X2)}
SCC (1):
Strict:
{cons#(X1, mark X2) -> cons#(X1, X2)}
Weak:
{ mark nil() -> active nil(),
mark fst(X1, X2) -> active fst(mark X1, mark X2),
mark 0() -> active 0(),
mark cons(X1, X2) -> active cons(mark X1, X2),
mark s X -> active s X,
mark from X -> active from mark X,
mark add(X1, X2) -> active add(mark X1, mark X2),
mark len X -> active len mark X,
active fst(0(), Z) -> mark nil(),
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
active from X -> mark cons(X, from s X),
active add(0(), X) -> mark X,
active add(s X, Y) -> mark s add(X, Y),
active len nil() -> mark 0(),
active len cons(X, Z) -> mark s len Z,
fst(X1, mark X2) -> fst(X1, X2),
fst(X1, active X2) -> fst(X1, X2),
fst(mark X1, X2) -> fst(X1, X2),
fst(active X1, X2) -> fst(X1, X2),
cons(X1, mark X2) -> cons(X1, X2),
cons(X1, active X2) -> cons(X1, X2),
cons(mark X1, X2) -> cons(X1, X2),
cons(active X1, X2) -> cons(X1, X2),
s mark X -> s X,
s active X -> s X,
from mark X -> from X,
from active X -> from X,
add(X1, mark X2) -> add(X1, X2),
add(X1, active X2) -> add(X1, X2),
add(mark X1, X2) -> add(X1, X2),
add(active X1, X2) -> add(X1, X2),
len mark X -> len X,
len active X -> len X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[fst](x0, x1) = x0,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0 + 1,
[len](x0) = x0 + 1,
[nil] = 1,
[0] = 1,
[cons#](x0, x1) = x0
Strict:
cons#(X1, mark X2) -> cons#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
len active X -> len X
2 + 1X >= 1 + 1X
len mark X -> len X
2 + 1X >= 1 + 1X
add(active X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
from active X -> from X
2 + 1X >= 1 + 1X
from mark X -> from X
2 + 1X >= 1 + 1X
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
cons(active X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(X1, mark X2) -> cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
fst(active X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(mark X1, X2) -> fst(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, active X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fst(X1, mark X2) -> fst(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
active len cons(X, Z) -> mark s len Z
3 + 0Z + 1X >= 2 + 0Z
active len nil() -> mark 0()
3 >= 2
active add(s X, Y) -> mark s add(X, Y)
2 + 0Y + 0X >= 2 + 0Y + 0X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active from X -> mark cons(X, from s X)
2 + 1X >= 2 + 1X
active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z))
2 + 0Z + 0Y + 0X >= 2 + 0Z + 1Y + 0X
active fst(0(), Z) -> mark nil()
2 + 0Z >= 2
mark len X -> active len mark X
2 + 1X >= 3 + 1X
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2
mark from X -> active from mark X
2 + 1X >= 3 + 1X
mark s X -> active s X
2 + 0X >= 2 + 0X
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 3 + 1X1 + 0X2
mark 0() -> active 0()
2 >= 2
mark fst(X1, X2) -> active fst(mark X1, mark X2)
1 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark nil() -> active nil()
2 >= 2
Qed