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