MAYBE
Time: 0.869897
TRS:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
DP:
DP:
{ mark# sel(X1, X2) -> mark# X1,
mark# sel(X1, X2) -> mark# X2,
mark# sel(X1, X2) -> sel#(mark X1, mark X2),
mark# sel(X1, X2) -> active# sel(mark X1, mark X2),
mark# fib1(X1, X2) -> mark# X1,
mark# fib1(X1, X2) -> mark# X2,
mark# fib1(X1, X2) -> fib1#(mark X1, mark X2),
mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2),
mark# s X -> mark# X,
mark# s X -> s# mark X,
mark# s X -> active# s mark X,
mark# 0() -> active# 0(),
mark# fib X -> mark# X,
mark# fib X -> active# fib mark X,
mark# fib X -> fib# mark X,
mark# cons(X1, X2) -> mark# X1,
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# cons(X1, X2) -> cons#(mark X1, X2),
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),
sel#(X1, mark X2) -> sel#(X1, X2),
sel#(X1, active X2) -> sel#(X1, X2),
sel#(mark X1, X2) -> sel#(X1, X2),
sel#(active X1, X2) -> sel#(X1, X2),
fib1#(X1, mark X2) -> fib1#(X1, X2),
fib1#(X1, active X2) -> fib1#(X1, X2),
fib1#(mark X1, X2) -> fib1#(X1, X2),
fib1#(active X1, X2) -> fib1#(X1, X2),
s# mark X -> s# X,
s# active X -> s# X,
active# sel(s N, cons(X, XS)) -> mark# sel(N, XS),
active# sel(s N, cons(X, XS)) -> sel#(N, XS),
active# sel(0(), cons(X, XS)) -> mark# X,
active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))),
active# fib1(X, Y) -> fib1#(Y, add(X, Y)),
active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))),
active# fib1(X, Y) -> add#(X, Y),
active# fib N -> mark# sel(N, fib1(s 0(), s 0())),
active# fib N -> sel#(N, fib1(s 0(), s 0())),
active# fib N -> fib1#(s 0(), s 0()),
active# fib N -> s# 0(),
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# add(0(), X) -> mark# X,
fib# mark X -> fib# X,
fib# active X -> fib# X,
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),
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)}
TRS:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
UR:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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),
a(x, y) -> x,
a(x, y) -> y}
EDG:
{
(mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(active X1, X2) -> sel#(X1, X2))
(mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(mark X1, X2) -> sel#(X1, X2))
(mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(X1, active X2) -> sel#(X1, X2))
(mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(X1, mark X2) -> sel#(X1, X2))
(mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, 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#(X1, active X2) -> add#(X1, X2))
(mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(X1, X2))
(sel#(X1, active X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2))
(sel#(X1, active X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
(sel#(X1, active X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2))
(sel#(X1, active X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
(sel#(active X1, X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2))
(sel#(active X1, X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
(sel#(active X1, X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2))
(sel#(active X1, X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
(fib1#(X1, active X2) -> fib1#(X1, X2), fib1#(active X1, X2) -> fib1#(X1, X2))
(fib1#(X1, active X2) -> fib1#(X1, X2), fib1#(mark X1, X2) -> fib1#(X1, X2))
(fib1#(X1, active X2) -> fib1#(X1, X2), fib1#(X1, active X2) -> fib1#(X1, X2))
(fib1#(X1, active X2) -> fib1#(X1, X2), fib1#(X1, mark X2) -> fib1#(X1, X2))
(fib1#(active X1, X2) -> fib1#(X1, X2), fib1#(active X1, X2) -> fib1#(X1, X2))
(fib1#(active X1, X2) -> fib1#(X1, X2), fib1#(mark X1, X2) -> fib1#(X1, X2))
(fib1#(active X1, X2) -> fib1#(X1, X2), fib1#(X1, active X2) -> fib1#(X1, X2))
(fib1#(active X1, X2) -> fib1#(X1, X2), fib1#(X1, mark X2) -> fib1#(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# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# add(0(), X) -> mark# X)
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# fib N -> s# 0())
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# fib N -> fib1#(s 0(), s 0()))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# fib N -> sel#(N, fib1(s 0(), s 0())))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# fib N -> mark# sel(N, fib1(s 0(), s 0())))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# fib1(X, Y) -> add#(X, Y))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# sel(0(), cons(X, XS)) -> mark# X)
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> sel#(N, XS))
(mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS))
(mark# fib X -> active# fib mark X, active# add(0(), X) -> mark# X)
(mark# fib X -> active# fib mark X, active# add(s X, Y) -> add#(X, Y))
(mark# fib X -> active# fib mark X, active# add(s X, Y) -> s# add(X, Y))
(mark# fib X -> active# fib mark X, active# add(s X, Y) -> mark# s add(X, Y))
(mark# fib X -> active# fib mark X, active# fib N -> s# 0())
(mark# fib X -> active# fib mark X, active# fib N -> fib1#(s 0(), s 0()))
(mark# fib X -> active# fib mark X, active# fib N -> sel#(N, fib1(s 0(), s 0())))
(mark# fib X -> active# fib mark X, active# fib N -> mark# sel(N, fib1(s 0(), s 0())))
(mark# fib X -> active# fib mark X, active# fib1(X, Y) -> add#(X, Y))
(mark# fib X -> active# fib mark X, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
(mark# fib X -> active# fib mark X, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
(mark# fib X -> active# fib mark X, active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))))
(mark# fib X -> active# fib mark X, active# sel(0(), cons(X, XS)) -> mark# X)
(mark# fib X -> active# fib mark X, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
(mark# fib X -> active# fib mark X, active# sel(s N, cons(X, XS)) -> mark# sel(N, XS))
(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# 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# fib X -> fib# mark X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# fib X -> active# fib mark X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# fib X -> mark# X)
(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# s X -> active# s mark X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> s# mark X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> mark# X)
(active# add(s X, Y) -> mark# s add(X, Y), mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(active# add(s X, Y) -> mark# s add(X, Y), mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(active# add(s X, Y) -> mark# s add(X, Y), mark# fib1(X1, X2) -> mark# X2)
(active# add(s X, Y) -> mark# s add(X, Y), mark# fib1(X1, X2) -> mark# X1)
(active# add(s X, Y) -> mark# s add(X, Y), mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(active# add(s X, Y) -> mark# s add(X, Y), mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(active# add(s X, Y) -> mark# s add(X, Y), mark# sel(X1, X2) -> mark# X2)
(active# add(s X, Y) -> mark# s add(X, Y), mark# sel(X1, X2) -> mark# X1)
(mark# fib1(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2)
(mark# fib1(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
(mark# fib1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# fib1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# fib1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
(mark# fib1(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
(mark# fib1(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
(mark# fib1(X1, X2) -> mark# X2, mark# fib X -> mark# X)
(mark# fib1(X1, X2) -> mark# X2, mark# 0() -> active# 0())
(mark# fib1(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
(mark# fib1(X1, X2) -> mark# X2, mark# s X -> s# mark X)
(mark# fib1(X1, X2) -> mark# X2, mark# s X -> mark# X)
(mark# fib1(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X2)
(mark# fib1(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
(mark# fib1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
(mark# fib1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
(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) -> 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) -> mark# s add(X, Y))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fib N -> s# 0())
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fib N -> fib1#(s 0(), s 0()))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fib N -> sel#(N, fib1(s 0(), s 0())))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fib N -> mark# sel(N, fib1(s 0(), s 0())))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fib1(X, Y) -> add#(X, Y))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sel(0(), cons(X, XS)) -> mark# X)
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sel(s N, cons(X, XS)) -> sel#(N, XS))
(mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS))
(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# fib1(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
(mark# fib1(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
(mark# fib1(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# fib1(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# fib1(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# fib1(X1, X2) -> mark# X1, mark# fib X -> fib# mark X)
(mark# fib1(X1, X2) -> mark# X1, mark# fib X -> active# fib mark X)
(mark# fib1(X1, X2) -> mark# X1, mark# fib X -> mark# X)
(mark# fib1(X1, X2) -> mark# X1, mark# 0() -> active# 0())
(mark# fib1(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
(mark# fib1(X1, X2) -> mark# X1, mark# s X -> s# mark X)
(mark# fib1(X1, X2) -> mark# X1, mark# s X -> mark# X)
(mark# fib1(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> mark# X2)
(mark# fib1(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> mark# X1)
(mark# fib1(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(mark# fib1(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
(mark# fib1(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
(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# 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# fib X -> fib# mark X)
(mark# add(X1, X2) -> mark# X1, mark# fib X -> active# fib mark X)
(mark# add(X1, X2) -> mark# X1, mark# fib X -> mark# X)
(mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0())
(mark# add(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
(mark# add(X1, X2) -> mark# X1, mark# s X -> s# mark X)
(mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X)
(mark# add(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> mark# X2)
(mark# add(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> mark# X1)
(mark# add(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
(mark# add(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# add(X1, X2) -> mark# X2)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# add(X1, X2) -> mark# X1)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# cons(X1, X2) -> mark# X1)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# fib X -> fib# mark X)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# fib X -> active# fib mark X)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# fib X -> mark# X)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# 0() -> active# 0())
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# s X -> active# s mark X)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# s X -> s# mark X)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# s X -> mark# X)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# fib1(X1, X2) -> mark# X2)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# fib1(X1, X2) -> mark# X1)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# sel(X1, X2) -> mark# X2)
(active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# sel(X1, X2) -> mark# X1)
(active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))), cons#(active X1, X2) -> cons#(X1, X2))
(active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))), cons#(mark X1, X2) -> cons#(X1, X2))
(active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))), cons#(X1, active X2) -> cons#(X1, X2))
(active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))), cons#(X1, mark X2) -> cons#(X1, X2))
(active# fib1(X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2))
(active# fib1(X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2))
(active# fib1(X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2))
(active# fib1(X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2))
(mark# s X -> s# mark X, s# active X -> s# X)
(mark# s X -> s# mark X, s# mark X -> s# X)
(active# fib1(X, Y) -> fib1#(Y, add(X, Y)), fib1#(active X1, X2) -> fib1#(X1, X2))
(active# fib1(X, Y) -> fib1#(Y, add(X, Y)), fib1#(mark X1, X2) -> fib1#(X1, X2))
(active# fib1(X, Y) -> fib1#(Y, add(X, Y)), fib1#(X1, active X2) -> fib1#(X1, X2))
(active# fib1(X, Y) -> fib1#(Y, add(X, Y)), fib1#(X1, mark X2) -> fib1#(X1, X2))
(mark# s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2)
(mark# s X -> mark# X, mark# add(X1, X2) -> mark# X1)
(mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(mark# s X -> mark# X, mark# fib X -> fib# mark X)
(mark# s X -> mark# X, mark# fib X -> active# fib mark X)
(mark# s X -> mark# X, mark# fib X -> mark# X)
(mark# s X -> mark# X, mark# 0() -> active# 0())
(mark# s X -> mark# X, mark# s X -> active# s mark X)
(mark# s X -> mark# X, mark# s X -> s# mark X)
(mark# s X -> mark# X, mark# s X -> mark# X)
(mark# s X -> mark# X, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(mark# s X -> mark# X, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(mark# s X -> mark# X, mark# fib1(X1, X2) -> mark# X2)
(mark# s X -> mark# X, mark# fib1(X1, X2) -> mark# X1)
(mark# s X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(mark# s X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X2)
(mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X1)
(s# mark X -> s# X, s# active X -> s# X)
(s# mark X -> s# X, s# mark X -> s# X)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# sel(0(), cons(X, XS)) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# sel(0(), cons(X, XS)) -> mark# X, mark# add(X1, X2) -> mark# X2)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# add(X1, X2) -> mark# X1)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# sel(0(), cons(X, XS)) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# sel(0(), cons(X, XS)) -> mark# X, mark# cons(X1, X2) -> mark# X1)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# fib X -> fib# mark X)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# fib X -> active# fib mark X)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# fib X -> mark# X)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# 0() -> active# 0())
(active# sel(0(), cons(X, XS)) -> mark# X, mark# s X -> active# s mark X)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# s X -> s# mark X)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# s X -> mark# X)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(active# sel(0(), cons(X, XS)) -> mark# X, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(active# sel(0(), cons(X, XS)) -> mark# X, mark# fib1(X1, X2) -> mark# X2)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# fib1(X1, X2) -> mark# X1)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(active# sel(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(active# sel(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
(active# sel(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
(fib# mark X -> fib# X, fib# active X -> fib# X)
(fib# mark X -> fib# X, fib# mark X -> fib# X)
(fib# active X -> fib# X, fib# mark X -> fib# X)
(fib# active X -> fib# X, fib# active X -> fib# X)
(active# add(0(), X) -> mark# X, mark# sel(X1, X2) -> mark# X1)
(active# add(0(), X) -> mark# X, mark# sel(X1, X2) -> mark# X2)
(active# add(0(), X) -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(active# add(0(), X) -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(active# add(0(), X) -> mark# X, mark# fib1(X1, X2) -> mark# X1)
(active# add(0(), X) -> mark# X, mark# fib1(X1, X2) -> mark# X2)
(active# add(0(), X) -> mark# X, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(active# add(0(), X) -> mark# X, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(active# add(0(), X) -> mark# X, mark# s X -> mark# X)
(active# add(0(), X) -> mark# X, mark# s X -> s# mark X)
(active# add(0(), X) -> mark# X, mark# s X -> active# s mark X)
(active# add(0(), X) -> mark# X, mark# 0() -> active# 0())
(active# add(0(), X) -> mark# X, mark# fib X -> mark# X)
(active# add(0(), X) -> mark# X, mark# fib X -> active# fib mark X)
(active# add(0(), X) -> mark# X, mark# fib X -> fib# mark X)
(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# 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))
(s# active X -> s# X, s# mark X -> s# X)
(s# active X -> s# X, s# active X -> s# X)
(mark# fib X -> mark# X, mark# sel(X1, X2) -> mark# X1)
(mark# fib X -> mark# X, mark# sel(X1, X2) -> mark# X2)
(mark# fib X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(mark# fib X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(mark# fib X -> mark# X, mark# fib1(X1, X2) -> mark# X1)
(mark# fib X -> mark# X, mark# fib1(X1, X2) -> mark# X2)
(mark# fib X -> mark# X, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(mark# fib X -> mark# X, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(mark# fib X -> mark# X, mark# s X -> mark# X)
(mark# fib X -> mark# X, mark# s X -> s# mark X)
(mark# fib X -> mark# X, mark# s X -> active# s mark X)
(mark# fib X -> mark# X, mark# 0() -> active# 0())
(mark# fib X -> mark# X, mark# fib X -> mark# X)
(mark# fib X -> mark# X, mark# fib X -> active# fib mark X)
(mark# fib X -> mark# X, mark# fib X -> fib# mark X)
(mark# fib X -> mark# X, mark# cons(X1, X2) -> mark# X1)
(mark# fib X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# fib X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# fib X -> mark# X, mark# add(X1, X2) -> mark# X1)
(mark# fib X -> mark# X, mark# add(X1, X2) -> mark# X2)
(mark# fib X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# fib X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# fib X -> fib# mark X, fib# mark X -> fib# X)
(mark# fib X -> fib# mark X, fib# active X -> fib# 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))
(active# fib N -> sel#(N, fib1(s 0(), s 0())), sel#(mark X1, X2) -> sel#(X1, X2))
(active# fib N -> sel#(N, fib1(s 0(), s 0())), sel#(active X1, X2) -> sel#(X1, X2))
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# sel(X1, X2) -> mark# X1)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# sel(X1, X2) -> mark# X2)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# fib1(X1, X2) -> mark# X1)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# fib1(X1, X2) -> mark# X2)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# s X -> mark# X)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# s X -> s# mark X)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# s X -> active# s mark X)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# 0() -> active# 0())
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# fib X -> mark# X)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# fib X -> active# fib mark X)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# fib X -> fib# mark X)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# cons(X1, X2) -> mark# X1)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# add(X1, X2) -> mark# X1)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# add(X1, X2) -> mark# X2)
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# sel(s N, cons(X, XS)) -> sel#(N, XS), sel#(X1, mark X2) -> sel#(X1, X2))
(active# sel(s N, cons(X, XS)) -> sel#(N, XS), sel#(X1, active X2) -> sel#(X1, X2))
(active# sel(s N, cons(X, XS)) -> sel#(N, XS), sel#(mark X1, X2) -> sel#(X1, X2))
(active# sel(s N, cons(X, XS)) -> sel#(N, XS), sel#(active X1, X2) -> sel#(X1, X2))
(mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
(mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
(mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> mark# X1)
(mark# cons(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> mark# X2)
(mark# cons(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
(mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
(mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
(mark# cons(X1, X2) -> mark# X1, mark# fib X -> mark# X)
(mark# cons(X1, X2) -> mark# X1, mark# fib X -> active# fib mark X)
(mark# cons(X1, X2) -> mark# X1, mark# fib X -> fib# mark X)
(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# 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# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
(mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
(mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(mark# sel(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> mark# X1)
(mark# sel(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> mark# X2)
(mark# sel(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(mark# sel(X1, X2) -> mark# X1, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(mark# sel(X1, X2) -> mark# X1, mark# s X -> mark# X)
(mark# sel(X1, X2) -> mark# X1, mark# s X -> s# mark X)
(mark# sel(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
(mark# sel(X1, X2) -> mark# X1, mark# 0() -> active# 0())
(mark# sel(X1, X2) -> mark# X1, mark# fib X -> mark# X)
(mark# sel(X1, X2) -> mark# X1, mark# fib X -> active# fib mark X)
(mark# sel(X1, X2) -> mark# X1, mark# fib X -> fib# mark X)
(mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
(mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# sel(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1)
(mark# sel(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2)
(mark# sel(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# sel(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2))
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# sel(X1, X2) -> mark# X1)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# sel(X1, X2) -> mark# X2)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# fib1(X1, X2) -> mark# X1)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# fib1(X1, X2) -> mark# X2)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# s X -> mark# X)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# s X -> s# mark X)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# s X -> active# s mark X)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# 0() -> active# 0())
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# fib X -> mark# X)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# fib X -> active# fib mark X)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# fib X -> fib# mark X)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# cons(X1, X2) -> mark# X1)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# cons(X1, X2) -> active# cons(mark X1, X2))
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# cons(X1, X2) -> cons#(mark X1, X2))
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# add(X1, X2) -> mark# X1)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# add(X1, X2) -> mark# X2)
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# add(X1, X2) -> active# add(mark X1, mark X2))
(active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
(mark# add(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
(mark# add(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
(mark# add(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X2)
(mark# add(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X)
(mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X)
(mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
(mark# add(X1, X2) -> mark# X2, mark# 0() -> active# 0())
(mark# add(X1, X2) -> mark# X2, mark# fib X -> mark# X)
(mark# add(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
(mark# add(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
(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# 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# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
(mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
(mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
(mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
(mark# sel(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
(mark# sel(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X2)
(mark# sel(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> fib1#(mark X1, mark X2))
(mark# sel(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2))
(mark# sel(X1, X2) -> mark# X2, mark# s X -> mark# X)
(mark# sel(X1, X2) -> mark# X2, mark# s X -> s# mark X)
(mark# sel(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
(mark# sel(X1, X2) -> mark# X2, mark# 0() -> active# 0())
(mark# sel(X1, X2) -> mark# X2, mark# fib X -> mark# X)
(mark# sel(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
(mark# sel(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
(mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
(mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
(mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
(mark# sel(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
(mark# sel(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2)
(mark# sel(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2))
(mark# sel(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> sel#(N, XS))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# sel(0(), cons(X, XS)) -> mark# X)
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fib1(X, Y) -> add#(X, Y))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fib N -> mark# sel(N, fib1(s 0(), s 0())))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fib N -> sel#(N, fib1(s 0(), s 0())))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fib N -> fib1#(s 0(), s 0()))
(mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fib N -> s# 0())
(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# add(0(), X) -> mark# X)
(mark# s X -> active# s mark X, active# sel(s N, cons(X, XS)) -> mark# sel(N, XS))
(mark# s X -> active# s mark X, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
(mark# s X -> active# s mark X, active# sel(0(), cons(X, XS)) -> mark# X)
(mark# s X -> active# s mark X, active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))))
(mark# s X -> active# s mark X, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
(mark# s X -> active# s mark X, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
(mark# s X -> active# s mark X, active# fib1(X, Y) -> add#(X, Y))
(mark# s X -> active# s mark X, active# fib N -> mark# sel(N, fib1(s 0(), s 0())))
(mark# s X -> active# s mark X, active# fib N -> sel#(N, fib1(s 0(), s 0())))
(mark# s X -> active# s mark X, active# fib N -> fib1#(s 0(), s 0()))
(mark# s X -> active# s mark X, active# fib N -> s# 0())
(mark# s X -> active# s mark X, active# add(s X, Y) -> mark# s add(X, Y))
(mark# s X -> active# s mark X, active# add(s X, Y) -> s# add(X, Y))
(mark# s X -> active# s mark X, active# add(s X, Y) -> add#(X, Y))
(mark# s X -> active# s mark X, active# add(0(), X) -> mark# X)
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> sel#(N, XS))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(0(), cons(X, XS)) -> mark# X)
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# fib1(X, Y) -> add#(X, Y))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# fib N -> mark# sel(N, fib1(s 0(), s 0())))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# fib N -> sel#(N, fib1(s 0(), s 0())))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# fib N -> fib1#(s 0(), s 0()))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# fib N -> s# 0())
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y))
(mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# add(0(), X) -> mark# X)
(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))
(fib1#(mark X1, X2) -> fib1#(X1, X2), fib1#(X1, mark X2) -> fib1#(X1, X2))
(fib1#(mark X1, X2) -> fib1#(X1, X2), fib1#(X1, active X2) -> fib1#(X1, X2))
(fib1#(mark X1, X2) -> fib1#(X1, X2), fib1#(mark X1, X2) -> fib1#(X1, X2))
(fib1#(mark X1, X2) -> fib1#(X1, X2), fib1#(active X1, X2) -> fib1#(X1, X2))
(fib1#(X1, mark X2) -> fib1#(X1, X2), fib1#(X1, mark X2) -> fib1#(X1, X2))
(fib1#(X1, mark X2) -> fib1#(X1, X2), fib1#(X1, active X2) -> fib1#(X1, X2))
(fib1#(X1, mark X2) -> fib1#(X1, X2), fib1#(mark X1, X2) -> fib1#(X1, X2))
(fib1#(X1, mark X2) -> fib1#(X1, X2), fib1#(active X1, X2) -> fib1#(X1, X2))
(sel#(mark X1, X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
(sel#(mark X1, X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2))
(sel#(mark X1, X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
(sel#(mark X1, X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2))
(sel#(X1, mark X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
(sel#(X1, mark X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2))
(sel#(X1, mark X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
(sel#(X1, mark X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2))
(mark# fib1(X1, X2) -> fib1#(mark X1, mark X2), fib1#(X1, mark X2) -> fib1#(X1, X2))
(mark# fib1(X1, X2) -> fib1#(mark X1, mark X2), fib1#(X1, active X2) -> fib1#(X1, X2))
(mark# fib1(X1, X2) -> fib1#(mark X1, mark X2), fib1#(mark X1, X2) -> fib1#(X1, X2))
(mark# fib1(X1, X2) -> fib1#(mark X1, mark X2), fib1#(active X1, X2) -> fib1#(X1, X2))
(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.835026
SCCS (7):
Scc:
{ mark# sel(X1, X2) -> mark# X1,
mark# sel(X1, X2) -> mark# X2,
mark# sel(X1, X2) -> active# sel(mark X1, mark X2),
mark# fib1(X1, X2) -> mark# X1,
mark# fib1(X1, X2) -> mark# X2,
mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2),
mark# s X -> mark# X,
mark# s X -> active# s mark X,
mark# fib X -> mark# X,
mark# fib X -> active# fib mark X,
mark# cons(X1, X2) -> mark# X1,
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# sel(s N, cons(X, XS)) -> mark# sel(N, XS),
active# sel(0(), cons(X, XS)) -> mark# X,
active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))),
active# fib N -> mark# sel(N, fib1(s 0(), s 0())),
active# add(s X, Y) -> mark# s add(X, Y),
active# add(0(), X) -> mark# X}
Scc:
{ fib# mark X -> fib# X,
fib# active X -> fib# X}
Scc:
{ s# mark X -> s# X,
s# active X -> s# 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:
{ fib1#(X1, mark X2) -> fib1#(X1, X2),
fib1#(X1, active X2) -> fib1#(X1, X2),
fib1#(mark X1, X2) -> fib1#(X1, X2),
fib1#(active X1, X2) -> fib1#(X1, X2)}
Scc:
{ sel#(X1, mark X2) -> sel#(X1, X2),
sel#(X1, active X2) -> sel#(X1, X2),
sel#(mark X1, X2) -> sel#(X1, X2),
sel#(active X1, X2) -> sel#(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 (21):
Strict:
{ mark# sel(X1, X2) -> mark# X1,
mark# sel(X1, X2) -> mark# X2,
mark# sel(X1, X2) -> active# sel(mark X1, mark X2),
mark# fib1(X1, X2) -> mark# X1,
mark# fib1(X1, X2) -> mark# X2,
mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2),
mark# s X -> mark# X,
mark# s X -> active# s mark X,
mark# fib X -> mark# X,
mark# fib X -> active# fib mark X,
mark# cons(X1, X2) -> mark# X1,
mark# cons(X1, X2) -> active# cons(mark X1, X2),
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# sel(s N, cons(X, XS)) -> mark# sel(N, XS),
active# sel(0(), cons(X, XS)) -> mark# X,
active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))),
active# fib N -> mark# sel(N, fib1(s 0(), s 0())),
active# add(s X, Y) -> mark# s add(X, Y),
active# add(0(), X) -> mark# X}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 1,
[fib1](x0, x1) = 1,
[cons](x0, x1) = 0,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[s](x0) = 1,
[active](x0) = 0,
[fib](x0) = 1,
[0] = 1,
[mark#](x0) = 1,
[active#](x0) = x0
Strict:
active# add(0(), X) -> mark# X
1 + 0X >= 1 + 0X
active# add(s X, Y) -> mark# s add(X, Y)
1 + 0X + 0Y >= 1 + 0X + 0Y
active# fib N -> mark# sel(N, fib1(s 0(), s 0()))
1 + 0N >= 1 + 0N
active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 1 + 0X + 0Y
active# sel(0(), cons(X, XS)) -> mark# X
1 + 0X + 0XS >= 1 + 0X
active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)
1 + 0N + 0X + 0XS >= 1 + 0N + 0XS
mark# add(X1, X2) -> active# add(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# add(X1, X2) -> mark# X2
1 + 0X1 + 0X2 >= 1 + 0X2
mark# add(X1, X2) -> mark# X1
1 + 0X1 + 0X2 >= 1 + 0X1
mark# cons(X1, X2) -> active# cons(mark X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark# cons(X1, X2) -> mark# X1
1 + 0X1 + 0X2 >= 1 + 0X1
mark# fib X -> active# fib mark X
1 + 0X >= 1 + 0X
mark# fib X -> mark# X
1 + 0X >= 1 + 0X
mark# s X -> active# s mark X
1 + 0X >= 1 + 0X
mark# s X -> mark# X
1 + 0X >= 1 + 0X
mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# fib1(X1, X2) -> mark# X2
1 + 0X1 + 0X2 >= 1 + 0X2
mark# fib1(X1, X2) -> mark# X1
1 + 0X1 + 0X2 >= 1 + 0X1
mark# sel(X1, X2) -> active# sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# sel(X1, X2) -> mark# X2
1 + 0X1 + 0X2 >= 1 + 0X2
mark# sel(X1, X2) -> mark# X1
1 + 0X1 + 0X2 >= 1 + 0X1
Weak:
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
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
fib active X -> fib X
1 + 0X >= 1 + 0X
fib mark X -> fib X
1 + 0X >= 1 + 0X
active add(0(), X) -> mark X
0 + 0X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
0 + 0X + 0Y >= 2 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
0 + 0N >= 2 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
0 + 0X + 0Y >= 1 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 2 + 0N + 0XS
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark fib X -> active fib mark X
2 + 0X >= 0 + 0X
mark 0() -> active 0()
2 >= 0
mark s X -> active s mark X
2 + 0X >= 0 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{ mark# sel(X1, X2) -> mark# X1,
mark# sel(X1, X2) -> mark# X2,
mark# sel(X1, X2) -> active# sel(mark X1, mark X2),
mark# fib1(X1, X2) -> mark# X1,
mark# fib1(X1, X2) -> mark# X2,
mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2),
mark# s X -> mark# X,
mark# s X -> active# s mark X,
mark# fib X -> mark# X,
mark# fib X -> active# fib mark X,
mark# cons(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# sel(s N, cons(X, XS)) -> mark# sel(N, XS),
active# sel(0(), cons(X, XS)) -> mark# X,
active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))),
active# fib N -> mark# sel(N, fib1(s 0(), s 0())),
active# add(s X, Y) -> mark# s add(X, Y),
active# add(0(), X) -> mark# X}
SCC (20):
Strict:
{ mark# sel(X1, X2) -> mark# X1,
mark# sel(X1, X2) -> mark# X2,
mark# sel(X1, X2) -> active# sel(mark X1, mark X2),
mark# fib1(X1, X2) -> mark# X1,
mark# fib1(X1, X2) -> mark# X2,
mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2),
mark# s X -> mark# X,
mark# s X -> active# s mark X,
mark# fib X -> mark# X,
mark# fib X -> active# fib mark X,
mark# cons(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# sel(s N, cons(X, XS)) -> mark# sel(N, XS),
active# sel(0(), cons(X, XS)) -> mark# X,
active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))),
active# fib N -> mark# sel(N, fib1(s 0(), s 0())),
active# add(s X, Y) -> mark# s add(X, Y),
active# add(0(), X) -> mark# X}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 1,
[fib1](x0, x1) = 1,
[cons](x0, x1) = 0,
[add](x0, x1) = 1,
[mark](x0) = x0 + 1,
[s](x0) = 0,
[active](x0) = 0,
[fib](x0) = 1,
[0] = 1,
[mark#](x0) = 1,
[active#](x0) = x0
Strict:
active# add(0(), X) -> mark# X
1 + 0X >= 1 + 0X
active# add(s X, Y) -> mark# s add(X, Y)
1 + 0X + 0Y >= 1 + 0X + 0Y
active# fib N -> mark# sel(N, fib1(s 0(), s 0()))
1 + 0N >= 1 + 0N
active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 1 + 0X + 0Y
active# sel(0(), cons(X, XS)) -> mark# X
1 + 0X + 0XS >= 1 + 0X
active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)
1 + 0N + 0X + 0XS >= 1 + 0N + 0XS
mark# add(X1, X2) -> active# add(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# add(X1, X2) -> mark# X2
1 + 0X1 + 0X2 >= 1 + 0X2
mark# add(X1, X2) -> mark# X1
1 + 0X1 + 0X2 >= 1 + 0X1
mark# cons(X1, X2) -> mark# X1
1 + 0X1 + 0X2 >= 1 + 0X1
mark# fib X -> active# fib mark X
1 + 0X >= 1 + 0X
mark# fib X -> mark# X
1 + 0X >= 1 + 0X
mark# s X -> active# s mark X
1 + 0X >= 0 + 0X
mark# s X -> mark# X
1 + 0X >= 1 + 0X
mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# fib1(X1, X2) -> mark# X2
1 + 0X1 + 0X2 >= 1 + 0X2
mark# fib1(X1, X2) -> mark# X1
1 + 0X1 + 0X2 >= 1 + 0X1
mark# sel(X1, X2) -> active# sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark# sel(X1, X2) -> mark# X2
1 + 0X1 + 0X2 >= 1 + 0X2
mark# sel(X1, X2) -> mark# X1
1 + 0X1 + 0X2 >= 1 + 0X1
Weak:
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
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
fib active X -> fib X
1 + 0X >= 1 + 0X
fib mark X -> fib X
1 + 0X >= 1 + 0X
active add(0(), X) -> mark X
0 + 0X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
0 + 0X + 0Y >= 1 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
0 + 0N >= 2 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
0 + 0X + 0Y >= 1 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 2 + 0N + 0XS
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark fib X -> active fib mark X
2 + 0X >= 0 + 0X
mark 0() -> active 0()
2 >= 0
mark s X -> active s mark X
1 + 0X >= 0 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{ mark# sel(X1, X2) -> mark# X1,
mark# sel(X1, X2) -> mark# X2,
mark# sel(X1, X2) -> active# sel(mark X1, mark X2),
mark# fib1(X1, X2) -> mark# X1,
mark# fib1(X1, X2) -> mark# X2,
mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2),
mark# s X -> mark# X,
mark# fib X -> mark# X,
mark# fib X -> active# fib mark X,
mark# cons(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# sel(s N, cons(X, XS)) -> mark# sel(N, XS),
active# sel(0(), cons(X, XS)) -> mark# X,
active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))),
active# fib N -> mark# sel(N, fib1(s 0(), s 0())),
active# add(s X, Y) -> mark# s add(X, Y),
active# add(0(), X) -> mark# X}
SCC (19):
Strict:
{ mark# sel(X1, X2) -> mark# X1,
mark# sel(X1, X2) -> mark# X2,
mark# sel(X1, X2) -> active# sel(mark X1, mark X2),
mark# fib1(X1, X2) -> mark# X1,
mark# fib1(X1, X2) -> mark# X2,
mark# fib1(X1, X2) -> active# fib1(mark X1, mark X2),
mark# s X -> mark# X,
mark# fib X -> mark# X,
mark# fib X -> active# fib mark X,
mark# cons(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X1,
mark# add(X1, X2) -> mark# X2,
mark# add(X1, X2) -> active# add(mark X1, mark X2),
active# sel(s N, cons(X, XS)) -> mark# sel(N, XS),
active# sel(0(), cons(X, XS)) -> mark# X,
active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))),
active# fib N -> mark# sel(N, fib1(s 0(), s 0())),
active# add(s X, Y) -> mark# s add(X, Y),
active# add(0(), X) -> mark# X}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
Fail
SCC (2):
Strict:
{ fib# mark X -> fib# X,
fib# active X -> fib# X}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = x0,
[mark](x0) = x0,
[s](x0) = 1,
[active](x0) = x0 + 1,
[fib](x0) = 0,
[0] = 0,
[fib#](x0) = x0
Strict:
fib# active X -> fib# X
1 + 1X >= 0 + 1X
fib# mark X -> fib# X
0 + 1X >= 0 + 1X
Weak:
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
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
fib active X -> fib X
0 + 0X >= 0 + 0X
fib mark X -> fib X
0 + 0X >= 0 + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 0X + 0Y >= 1 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 0N >= 0 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 0 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
1 + 0X + 0XS >= 0 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
1 + 0N + 0X + 0XS >= 0 + 0N + 0XS
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark fib X -> active fib mark X
0 + 0X >= 1 + 0X
mark 0() -> active 0()
0 >= 1
mark s X -> active s mark X
1 + 0X >= 2 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
SCCS (1):
Scc:
{fib# mark X -> fib# X}
SCC (1):
Strict:
{fib# mark X -> fib# X}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1 + 1,
[add](x0, x1) = x0 + 1,
[mark](x0) = x0 + 1,
[s](x0) = x0 + 1,
[active](x0) = x0,
[fib](x0) = x0 + 1,
[0] = 1,
[fib#](x0) = x0
Strict:
fib# mark X -> fib# X
1 + 1X >= 0 + 1X
Weak:
add(active X1, X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(active X1, X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
fib active X -> fib X
1 + 1X >= 1 + 1X
fib mark X -> fib X
2 + 1X >= 1 + 1X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 1X + 0Y >= 3 + 1X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 1N >= 1 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 1Y >= 4 + 2X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 1 + 0N + 0XS
s active X -> s X
1 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, mark X2) -> fib1(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
mark fib X -> active fib mark X
2 + 1X >= 2 + 1X
mark 0() -> active 0()
2 >= 1
mark s X -> active s mark X
2 + 1X >= 2 + 1X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
Qed
SCC (2):
Strict:
{ s# mark X -> s# X,
s# active X -> s# X}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = x0,
[mark](x0) = x0,
[s](x0) = 1,
[active](x0) = x0 + 1,
[fib](x0) = 0,
[0] = 0,
[s#](x0) = x0
Strict:
s# active X -> s# X
1 + 1X >= 0 + 1X
s# mark X -> s# X
0 + 1X >= 0 + 1X
Weak:
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
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
fib active X -> fib X
0 + 0X >= 0 + 0X
fib mark X -> fib X
0 + 0X >= 0 + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 0X + 0Y >= 1 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 0N >= 0 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 0 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
1 + 0X + 0XS >= 0 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
1 + 0N + 0X + 0XS >= 0 + 0N + 0XS
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark fib X -> active fib mark X
0 + 0X >= 1 + 0X
mark 0() -> active 0()
0 >= 1
mark s X -> active s mark X
1 + 0X >= 2 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
SCCS (1):
Scc:
{s# mark X -> s# X}
SCC (1):
Strict:
{s# mark X -> s# X}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1 + 1,
[add](x0, x1) = x0 + 1,
[mark](x0) = x0 + 1,
[s](x0) = x0 + 1,
[active](x0) = x0,
[fib](x0) = x0 + 1,
[0] = 1,
[s#](x0) = x0
Strict:
s# mark X -> s# X
1 + 1X >= 0 + 1X
Weak:
add(active X1, X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(active X1, X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
fib active X -> fib X
1 + 1X >= 1 + 1X
fib mark X -> fib X
2 + 1X >= 1 + 1X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 1X + 0Y >= 3 + 1X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 1N >= 1 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 1Y >= 4 + 2X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 1 + 0N + 0XS
s active X -> s X
1 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, mark X2) -> fib1(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
mark fib X -> active fib mark X
2 + 1X >= 2 + 1X
mark 0() -> active 0()
2 >= 1
mark s X -> active s mark X
2 + 1X >= 2 + 1X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
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 sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[s](x0) = 0,
[active](x0) = x0 + 1,
[fib](x0) = 0,
[0] = 0,
[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:
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
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
fib active X -> fib X
0 + 0X >= 0 + 0X
fib mark X -> fib X
0 + 0X >= 0 + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active add(s X, Y) -> mark s add(X, Y)
1 + 0X + 0Y >= 0 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 0N >= 0 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 0 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
1 + 0X + 0XS >= 0 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
1 + 0N + 0X + 0XS >= 0 + 0N + 0XS
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark fib X -> active fib mark X
0 + 0X >= 1 + 0X
mark 0() -> active 0()
0 >= 1
mark s X -> active s mark X
0 + 0X >= 1 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
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 sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = x0 + x1,
[mark](x0) = x0 + 1,
[s](x0) = x0 + 1,
[active](x0) = x0,
[fib](x0) = x0 + 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:
add(active X1, X2) -> add(X1, X2)
0 + 1X1 + 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 + 1X2 >= 0 + 1X1 + 1X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
cons(active X1, X2) -> cons(X1, X2)
1 + 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
fib active X -> fib X
1 + 1X >= 1 + 1X
fib mark X -> fib X
2 + 1X >= 1 + 1X
active add(0(), X) -> mark X
1 + 1X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
1 + 1X + 1Y >= 2 + 1X + 1Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 1N >= 1 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 1Y >= 2 + 1X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 1 + 0N + 0XS
s active X -> s X
1 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, mark X2) -> fib1(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark fib X -> active fib mark X
2 + 1X >= 2 + 1X
mark 0() -> active 0()
2 >= 1
mark s X -> active s mark X
2 + 1X >= 2 + 1X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
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 sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = x0,
[mark](x0) = x0,
[s](x0) = 1,
[active](x0) = x0 + 1,
[fib](x0) = 0,
[0] = 0,
[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:
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
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
fib active X -> fib X
0 + 0X >= 0 + 0X
fib mark X -> fib X
0 + 0X >= 0 + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 0X + 0Y >= 1 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 0N >= 0 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 0 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
1 + 0X + 0XS >= 0 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
1 + 0N + 0X + 0XS >= 0 + 0N + 0XS
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark fib X -> active fib mark X
0 + 0X >= 1 + 0X
mark 0() -> active 0()
0 >= 1
mark s X -> active s mark X
1 + 0X >= 2 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
SCCS (1):
Scc:
{add#(X1, mark X2) -> add#(X1, X2)}
SCC (1):
Strict:
{add#(X1, mark X2) -> add#(X1, X2)}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1 + 1,
[add](x0, x1) = x0 + 1,
[mark](x0) = x0 + 1,
[s](x0) = x0 + 1,
[active](x0) = x0,
[fib](x0) = x0 + 1,
[0] = 1,
[add#](x0, x1) = x0
Strict:
add#(X1, mark X2) -> add#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
add(active X1, X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(active X1, X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
fib active X -> fib X
1 + 1X >= 1 + 1X
fib mark X -> fib X
2 + 1X >= 1 + 1X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 1X + 0Y >= 3 + 1X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 1N >= 1 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 1Y >= 4 + 2X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 1 + 0N + 0XS
s active X -> s X
1 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, mark X2) -> fib1(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
mark fib X -> active fib mark X
2 + 1X >= 2 + 1X
mark 0() -> active 0()
2 >= 1
mark s X -> active s mark X
2 + 1X >= 2 + 1X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
Qed
SCC (4):
Strict:
{ fib1#(X1, mark X2) -> fib1#(X1, X2),
fib1#(X1, active X2) -> fib1#(X1, X2),
fib1#(mark X1, X2) -> fib1#(X1, X2),
fib1#(active X1, X2) -> fib1#(X1, X2)}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[s](x0) = 0,
[active](x0) = x0 + 1,
[fib](x0) = 0,
[0] = 0,
[fib1#](x0, x1) = x0
Strict:
fib1#(active X1, X2) -> fib1#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fib1#(mark X1, X2) -> fib1#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fib1#(X1, active X2) -> fib1#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fib1#(X1, mark X2) -> fib1#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
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
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
fib active X -> fib X
0 + 0X >= 0 + 0X
fib mark X -> fib X
0 + 0X >= 0 + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active add(s X, Y) -> mark s add(X, Y)
1 + 0X + 0Y >= 0 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 0N >= 0 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 0 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
1 + 0X + 0XS >= 0 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
1 + 0N + 0X + 0XS >= 0 + 0N + 0XS
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark fib X -> active fib mark X
0 + 0X >= 1 + 0X
mark 0() -> active 0()
0 >= 1
mark s X -> active s mark X
0 + 0X >= 1 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
SCCS (1):
Scc:
{ fib1#(X1, mark X2) -> fib1#(X1, X2),
fib1#(X1, active X2) -> fib1#(X1, X2),
fib1#(mark X1, X2) -> fib1#(X1, X2)}
SCC (3):
Strict:
{ fib1#(X1, mark X2) -> fib1#(X1, X2),
fib1#(X1, active X2) -> fib1#(X1, X2),
fib1#(mark X1, X2) -> fib1#(X1, X2)}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = x0 + x1,
[mark](x0) = x0 + 1,
[s](x0) = x0 + 1,
[active](x0) = x0,
[fib](x0) = x0 + 1,
[0] = 1,
[fib1#](x0, x1) = x0
Strict:
fib1#(mark X1, X2) -> fib1#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fib1#(X1, active X2) -> fib1#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
fib1#(X1, mark X2) -> fib1#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
add(active X1, X2) -> add(X1, X2)
0 + 1X1 + 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 + 1X2 >= 0 + 1X1 + 1X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
cons(active X1, X2) -> cons(X1, X2)
1 + 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
fib active X -> fib X
1 + 1X >= 1 + 1X
fib mark X -> fib X
2 + 1X >= 1 + 1X
active add(0(), X) -> mark X
1 + 1X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
1 + 1X + 1Y >= 2 + 1X + 1Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 1N >= 1 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 1Y >= 2 + 1X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 1 + 0N + 0XS
s active X -> s X
1 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, mark X2) -> fib1(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark fib X -> active fib mark X
2 + 1X >= 2 + 1X
mark 0() -> active 0()
2 >= 1
mark s X -> active s mark X
2 + 1X >= 2 + 1X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{ fib1#(X1, mark X2) -> fib1#(X1, X2),
fib1#(X1, active X2) -> fib1#(X1, X2)}
SCC (2):
Strict:
{ fib1#(X1, mark X2) -> fib1#(X1, X2),
fib1#(X1, active X2) -> fib1#(X1, X2)}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = x0,
[mark](x0) = x0,
[s](x0) = 1,
[active](x0) = x0 + 1,
[fib](x0) = 0,
[0] = 0,
[fib1#](x0, x1) = x0
Strict:
fib1#(X1, active X2) -> fib1#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
fib1#(X1, mark X2) -> fib1#(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
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
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
fib active X -> fib X
0 + 0X >= 0 + 0X
fib mark X -> fib X
0 + 0X >= 0 + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 0X + 0Y >= 1 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 0N >= 0 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 0 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
1 + 0X + 0XS >= 0 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
1 + 0N + 0X + 0XS >= 0 + 0N + 0XS
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark fib X -> active fib mark X
0 + 0X >= 1 + 0X
mark 0() -> active 0()
0 >= 1
mark s X -> active s mark X
1 + 0X >= 2 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
SCCS (1):
Scc:
{fib1#(X1, mark X2) -> fib1#(X1, X2)}
SCC (1):
Strict:
{fib1#(X1, mark X2) -> fib1#(X1, X2)}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1 + 1,
[add](x0, x1) = x0 + 1,
[mark](x0) = x0 + 1,
[s](x0) = x0 + 1,
[active](x0) = x0,
[fib](x0) = x0 + 1,
[0] = 1,
[fib1#](x0, x1) = x0
Strict:
fib1#(X1, mark X2) -> fib1#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
add(active X1, X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(active X1, X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
fib active X -> fib X
1 + 1X >= 1 + 1X
fib mark X -> fib X
2 + 1X >= 1 + 1X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 1X + 0Y >= 3 + 1X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 1N >= 1 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 1Y >= 4 + 2X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 1 + 0N + 0XS
s active X -> s X
1 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, mark X2) -> fib1(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
mark fib X -> active fib mark X
2 + 1X >= 2 + 1X
mark 0() -> active 0()
2 >= 1
mark s X -> active s mark X
2 + 1X >= 2 + 1X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
Qed
SCC (4):
Strict:
{ sel#(X1, mark X2) -> sel#(X1, X2),
sel#(X1, active X2) -> sel#(X1, X2),
sel#(mark X1, X2) -> sel#(X1, X2),
sel#(active X1, X2) -> sel#(X1, X2)}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[s](x0) = 0,
[active](x0) = x0 + 1,
[fib](x0) = 0,
[0] = 0,
[sel#](x0, x1) = x0
Strict:
sel#(active X1, X2) -> sel#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
sel#(mark X1, X2) -> sel#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
sel#(X1, active X2) -> sel#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
sel#(X1, mark X2) -> sel#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
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
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
fib active X -> fib X
0 + 0X >= 0 + 0X
fib mark X -> fib X
0 + 0X >= 0 + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active add(s X, Y) -> mark s add(X, Y)
1 + 0X + 0Y >= 0 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 0N >= 0 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 0 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
1 + 0X + 0XS >= 0 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
1 + 0N + 0X + 0XS >= 0 + 0N + 0XS
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark fib X -> active fib mark X
0 + 0X >= 1 + 0X
mark 0() -> active 0()
0 >= 1
mark s X -> active s mark X
0 + 0X >= 1 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
SCCS (1):
Scc:
{ sel#(X1, mark X2) -> sel#(X1, X2),
sel#(X1, active X2) -> sel#(X1, X2),
sel#(mark X1, X2) -> sel#(X1, X2)}
SCC (3):
Strict:
{ sel#(X1, mark X2) -> sel#(X1, X2),
sel#(X1, active X2) -> sel#(X1, X2),
sel#(mark X1, X2) -> sel#(X1, X2)}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = x0 + x1,
[mark](x0) = x0 + 1,
[s](x0) = x0 + 1,
[active](x0) = x0,
[fib](x0) = x0 + 1,
[0] = 1,
[sel#](x0, x1) = x0
Strict:
sel#(mark X1, X2) -> sel#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
sel#(X1, active X2) -> sel#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
sel#(X1, mark X2) -> sel#(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
add(active X1, X2) -> add(X1, X2)
0 + 1X1 + 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 + 1X2 >= 0 + 1X1 + 1X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
cons(active X1, X2) -> cons(X1, X2)
1 + 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
fib active X -> fib X
1 + 1X >= 1 + 1X
fib mark X -> fib X
2 + 1X >= 1 + 1X
active add(0(), X) -> mark X
1 + 1X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
1 + 1X + 1Y >= 2 + 1X + 1Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 1N >= 1 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 1Y >= 2 + 1X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 1 + 0N + 0XS
s active X -> s X
1 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, mark X2) -> fib1(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark fib X -> active fib mark X
2 + 1X >= 2 + 1X
mark 0() -> active 0()
2 >= 1
mark s X -> active s mark X
2 + 1X >= 2 + 1X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{ sel#(X1, mark X2) -> sel#(X1, X2),
sel#(X1, active X2) -> sel#(X1, X2)}
SCC (2):
Strict:
{ sel#(X1, mark X2) -> sel#(X1, X2),
sel#(X1, active X2) -> sel#(X1, X2)}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = x0,
[mark](x0) = x0,
[s](x0) = 1,
[active](x0) = x0 + 1,
[fib](x0) = 0,
[0] = 0,
[sel#](x0, x1) = x0
Strict:
sel#(X1, active X2) -> sel#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
sel#(X1, mark X2) -> sel#(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
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
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
fib active X -> fib X
0 + 0X >= 0 + 0X
fib mark X -> fib X
0 + 0X >= 0 + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 0X + 0Y >= 1 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 0N >= 0 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 0 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
1 + 0X + 0XS >= 0 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
1 + 0N + 0X + 0XS >= 0 + 0N + 0XS
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark fib X -> active fib mark X
0 + 0X >= 1 + 0X
mark 0() -> active 0()
0 >= 1
mark s X -> active s mark X
1 + 0X >= 2 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
SCCS (1):
Scc:
{sel#(X1, mark X2) -> sel#(X1, X2)}
SCC (1):
Strict:
{sel#(X1, mark X2) -> sel#(X1, X2)}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1 + 1,
[add](x0, x1) = x0 + 1,
[mark](x0) = x0 + 1,
[s](x0) = x0 + 1,
[active](x0) = x0,
[fib](x0) = x0 + 1,
[0] = 1,
[sel#](x0, x1) = x0
Strict:
sel#(X1, mark X2) -> sel#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
add(active X1, X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(active X1, X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
fib active X -> fib X
1 + 1X >= 1 + 1X
fib mark X -> fib X
2 + 1X >= 1 + 1X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 1X + 0Y >= 3 + 1X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 1N >= 1 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 1Y >= 4 + 2X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 1 + 0N + 0XS
s active X -> s X
1 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, mark X2) -> fib1(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
mark fib X -> active fib mark X
2 + 1X >= 2 + 1X
mark 0() -> active 0()
2 >= 1
mark s X -> active s mark X
2 + 1X >= 2 + 1X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
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 sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = 0,
[mark](x0) = x0,
[s](x0) = 0,
[active](x0) = x0 + 1,
[fib](x0) = 0,
[0] = 0,
[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:
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
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
fib active X -> fib X
0 + 0X >= 0 + 0X
fib mark X -> fib X
0 + 0X >= 0 + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active add(s X, Y) -> mark s add(X, Y)
1 + 0X + 0Y >= 0 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 0N >= 0 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 0 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
1 + 0X + 0XS >= 0 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
1 + 0N + 0X + 0XS >= 0 + 0N + 0XS
s active X -> s X
0 + 0X >= 0 + 0X
s mark X -> s X
0 + 0X >= 0 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark fib X -> active fib mark X
0 + 0X >= 1 + 0X
mark 0() -> active 0()
0 >= 1
mark s X -> active s mark X
0 + 0X >= 1 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
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 sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + 1,
[add](x0, x1) = x0 + x1,
[mark](x0) = x0 + 1,
[s](x0) = x0 + 1,
[active](x0) = x0,
[fib](x0) = x0 + 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:
add(active X1, X2) -> add(X1, X2)
0 + 1X1 + 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 + 1X2 >= 0 + 1X1 + 1X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
cons(active X1, X2) -> cons(X1, X2)
1 + 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
fib active X -> fib X
1 + 1X >= 1 + 1X
fib mark X -> fib X
2 + 1X >= 1 + 1X
active add(0(), X) -> mark X
1 + 1X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
1 + 1X + 1Y >= 2 + 1X + 1Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 1N >= 1 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 1Y >= 2 + 1X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 1 + 0N + 0XS
s active X -> s X
1 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, mark X2) -> fib1(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark fib X -> active fib mark X
2 + 1X >= 2 + 1X
mark 0() -> active 0()
2 >= 1
mark s X -> active s mark X
2 + 1X >= 2 + 1X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
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 sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = 0,
[cons](x0, x1) = 0,
[add](x0, x1) = x0,
[mark](x0) = x0,
[s](x0) = 1,
[active](x0) = x0 + 1,
[fib](x0) = 0,
[0] = 0,
[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:
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
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
fib active X -> fib X
0 + 0X >= 0 + 0X
fib mark X -> fib X
0 + 0X >= 0 + 0X
active add(0(), X) -> mark X
1 + 0X >= 0 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 0X + 0Y >= 1 + 0X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 0N >= 0 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 0Y >= 0 + 0X + 0Y
active sel(0(), cons(X, XS)) -> mark X
1 + 0X + 0XS >= 0 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
1 + 0N + 0X + 0XS >= 0 + 0N + 0XS
s active X -> s X
1 + 0X >= 1 + 0X
s mark X -> s X
1 + 0X >= 1 + 0X
fib1(active X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(mark X1, X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, active X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
fib1(X1, mark X2) -> fib1(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
0 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark fib X -> active fib mark X
0 + 0X >= 1 + 0X
mark 0() -> active 0()
0 >= 1
mark s X -> active s mark X
1 + 0X >= 2 + 0X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
SCCS (1):
Scc:
{cons#(X1, mark X2) -> cons#(X1, X2)}
SCC (1):
Strict:
{cons#(X1, mark X2) -> cons#(X1, X2)}
Weak:
{ mark sel(X1, X2) -> active sel(mark X1, mark X2),
mark fib1(X1, X2) -> active fib1(mark X1, mark X2),
mark s X -> active s mark X,
mark 0() -> active 0(),
mark fib X -> active fib mark X,
mark cons(X1, X2) -> active cons(mark X1, X2),
mark add(X1, X2) -> active add(mark X1, mark X2),
sel(X1, mark X2) -> sel(X1, X2),
sel(X1, active X2) -> sel(X1, X2),
sel(mark X1, X2) -> sel(X1, X2),
sel(active X1, X2) -> sel(X1, X2),
fib1(X1, mark X2) -> fib1(X1, X2),
fib1(X1, active X2) -> fib1(X1, X2),
fib1(mark X1, X2) -> fib1(X1, X2),
fib1(active X1, X2) -> fib1(X1, X2),
s mark X -> s X,
s active X -> s X,
active sel(s N, cons(X, XS)) -> mark sel(N, XS),
active sel(0(), cons(X, XS)) -> mark X,
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y))),
active fib N -> mark sel(N, fib1(s 0(), s 0())),
active add(s X, Y) -> mark s add(X, Y),
active add(0(), X) -> mark X,
fib mark X -> fib X,
fib active X -> fib X,
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),
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)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[sel](x0, x1) = 0,
[fib1](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1 + 1,
[add](x0, x1) = x0 + 1,
[mark](x0) = x0 + 1,
[s](x0) = x0 + 1,
[active](x0) = x0,
[fib](x0) = x0 + 1,
[0] = 1,
[cons#](x0, x1) = x0
Strict:
cons#(X1, mark X2) -> cons#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
add(active X1, X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(mark X1, X2) -> add(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, active X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
add(X1, mark X2) -> add(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(active X1, X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(mark X1, X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, active X2) -> cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(X1, mark X2) -> cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
fib active X -> fib X
1 + 1X >= 1 + 1X
fib mark X -> fib X
2 + 1X >= 1 + 1X
active add(0(), X) -> mark X
2 + 0X >= 1 + 1X
active add(s X, Y) -> mark s add(X, Y)
2 + 1X + 0Y >= 3 + 1X + 0Y
active fib N -> mark sel(N, fib1(s 0(), s 0()))
1 + 1N >= 1 + 0N
active fib1(X, Y) -> mark cons(X, fib1(Y, add(X, Y)))
1 + 0X + 1Y >= 4 + 2X + 0Y
active sel(0(), cons(X, XS)) -> mark X
0 + 0X + 0XS >= 1 + 1X
active sel(s N, cons(X, XS)) -> mark sel(N, XS)
0 + 0N + 0X + 0XS >= 1 + 0N + 0XS
s active X -> s X
1 + 1X >= 1 + 1X
s mark X -> s X
2 + 1X >= 1 + 1X
fib1(active X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(mark X1, X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, active X2) -> fib1(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
fib1(X1, mark X2) -> fib1(X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
sel(active X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(mark X1, X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, active X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
sel(X1, mark X2) -> sel(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
mark add(X1, X2) -> active add(mark X1, mark X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
mark cons(X1, X2) -> active cons(mark X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
mark fib X -> active fib mark X
2 + 1X >= 2 + 1X
mark 0() -> active 0()
2 >= 1
mark s X -> active s mark X
2 + 1X >= 2 + 1X
mark fib1(X1, X2) -> active fib1(mark X1, mark X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
mark sel(X1, X2) -> active sel(mark X1, mark X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
Qed