MAYBE Time: 22.405217 TRS: { mark cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} DP: DP: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2), mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# f X -> mark# X, mark# f X -> f# mark X, mark# f X -> active# f mark X, mark# g X -> mark# X, mark# g X -> g# mark X, mark# g X -> active# g mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, mark# s X -> s# mark X, mark# 0() -> active# 0(), mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2), mark# sel(X1, X2) -> sel#(mark X1, mark X2), cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2), f# mark X -> f# X, f# active X -> f# X, g# mark X -> g# X, g# active X -> g# X, active# f X -> mark# cons(X, f g X), active# f X -> cons#(X, f g X), active# f X -> f# g X, active# f X -> g# X, active# g s X -> mark# s s g X, active# g s X -> g# X, active# g s X -> s# g X, active# g s X -> s# s g X, active# g 0() -> mark# s 0(), active# g 0() -> s# 0(), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), active# sel(s X, cons(Y, Z)) -> sel#(X, Z), active# sel(0(), cons(X, Y)) -> mark# X, s# mark X -> s# X, s# active X -> s# X, 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)} TRS: { mark cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} EDG: { (mark# g X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# g X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# g X -> mark# X, mark# sel(X1, X2) -> mark# X2) (mark# g X -> mark# X, mark# sel(X1, X2) -> mark# X1) (mark# g X -> mark# X, mark# 0() -> active# 0()) (mark# g X -> mark# X, mark# s X -> s# mark X) (mark# g X -> mark# X, mark# s X -> active# s mark X) (mark# g X -> mark# X, mark# s X -> mark# X) (mark# g X -> mark# X, mark# g X -> active# g mark X) (mark# g X -> mark# X, mark# g X -> g# mark X) (mark# g X -> mark# X, mark# g X -> mark# X) (mark# g X -> mark# X, mark# f X -> active# f mark X) (mark# g X -> mark# X, mark# f X -> f# mark X) (mark# g X -> mark# X, mark# f X -> mark# X) (mark# g X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# g X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# g X -> mark# X, mark# cons(X1, X2) -> mark# X1) (f# mark X -> f# X, f# active X -> f# X) (f# mark X -> f# X, f# mark X -> f# X) (g# mark X -> g# X, g# active X -> g# X) (g# mark X -> g# X, g# mark X -> g# X) (active# f X -> g# X, g# active X -> g# X) (active# f X -> g# X, g# mark X -> g# X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X2) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X1) (active# sel(0(), cons(X, Y)) -> mark# X, mark# 0() -> active# 0()) (active# sel(0(), cons(X, Y)) -> mark# X, mark# s X -> s# mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# s X -> active# s mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# s X -> mark# X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# g X -> active# g mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# g X -> g# mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# g X -> mark# X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# f X -> active# f mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# f X -> f# mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# f X -> mark# X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# cons(X1, X2) -> mark# X1) (s# active X -> s# X, s# active X -> s# X) (s# active X -> s# X, s# mark X -> s# X) (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# sel(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (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# s X -> mark# X) (mark# sel(X1, X2) -> mark# X1, mark# g X -> active# g mark X) (mark# sel(X1, X2) -> mark# X1, mark# g X -> g# mark X) (mark# sel(X1, X2) -> mark# X1, mark# g X -> mark# X) (mark# sel(X1, X2) -> mark# X1, mark# f X -> active# f mark X) (mark# sel(X1, X2) -> mark# X1, mark# f X -> f# mark X) (mark# sel(X1, X2) -> mark# X1, mark# f X -> mark# X) (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# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(0(), cons(X, Y)) -> mark# X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (sel#(X1, mark X2) -> sel#(X1, X2), sel#(active X1, 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#(X1, active X2) -> sel#(X1, X2)) (sel#(X1, mark X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2)) (sel#(mark X1, X2) -> sel#(X1, X2), sel#(active X1, 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#(X1, active X2) -> sel#(X1, X2)) (sel#(mark X1, X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(active X1, X2) -> sel#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(mark X1, X2) -> sel#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(X1, active X2) -> sel#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(X1, mark X2) -> sel#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> mark# X2) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> mark# X1) (mark# g X -> active# g mark X, active# g 0() -> s# 0()) (mark# g X -> active# g mark X, active# g 0() -> mark# s 0()) (mark# g X -> active# g mark X, active# g s X -> s# s g X) (mark# g X -> active# g mark X, active# g s X -> s# g X) (mark# g X -> active# g mark X, active# g s X -> g# X) (mark# g X -> active# g mark X, active# g s X -> mark# s s g X) (mark# f X -> f# mark X, f# active X -> f# X) (mark# f X -> f# mark X, f# mark X -> f# X) (mark# s X -> s# mark X, s# active X -> s# X) (mark# s X -> s# mark X, s# mark X -> s# X) (mark# g X -> g# mark X, g# mark X -> g# X) (mark# g X -> g# mark X, g# active X -> g# X) (active# g 0() -> mark# s 0(), mark# s X -> mark# X) (active# g 0() -> mark# s 0(), mark# s X -> active# s mark X) (active# g 0() -> mark# s 0(), mark# s X -> s# mark X) (mark# f X -> active# f mark X, active# f X -> mark# cons(X, f g X)) (mark# f X -> active# f mark X, active# f X -> cons#(X, f g X)) (mark# f X -> active# f mark X, active# f X -> f# g X) (mark# f X -> active# f mark X, active# f X -> g# X) (active# g s X -> mark# s s g X, mark# s X -> mark# X) (active# g s X -> mark# s s g X, mark# s X -> active# s mark X) (active# g s X -> mark# s s g X, mark# s X -> s# mark X) (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(X1, mark 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#(mark X1, X2) -> sel#(X1, X2)) (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(active X1, X2) -> sel#(X1, X2)) (sel#(active X1, X2) -> sel#(X1, X2), sel#(X1, mark 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#(mark X1, X2) -> sel#(X1, X2)) (sel#(active X1, X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2)) (sel#(X1, active X2) -> sel#(X1, X2), sel#(X1, mark 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#(mark X1, X2) -> sel#(X1, X2)) (sel#(X1, active X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (active# f X -> mark# cons(X, f g X), mark# cons(X1, X2) -> mark# X1) (active# f X -> mark# cons(X, f g X), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# f X -> mark# cons(X, f g X), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# f X -> cons#(X, f g X), cons#(mark X1, X2) -> cons#(X1, X2)) (active# f X -> cons#(X, f g X), cons#(active X1, X2) -> cons#(X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# f X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# f X -> f# mark X) (mark# sel(X1, X2) -> mark# X2, mark# f X -> active# f mark X) (mark# sel(X1, X2) -> mark# X2, mark# g X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# g X -> g# mark X) (mark# sel(X1, X2) -> mark# X2, mark# g X -> active# g mark X) (mark# sel(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# sel(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# sel(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (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) -> active# sel(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# f X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# f X -> f# mark X) (mark# cons(X1, X2) -> mark# X1, mark# f X -> active# f mark X) (mark# cons(X1, X2) -> mark# X1, mark# g X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# g X -> g# mark X) (mark# cons(X1, X2) -> mark# X1, mark# g X -> active# g mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (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) -> active# sel(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (s# mark X -> s# X, s# mark X -> s# X) (s# mark X -> s# X, s# active X -> s# X) (active# g s X -> g# X, g# mark X -> g# X) (active# g s X -> g# X, g# active X -> g# X) (g# active X -> g# X, g# mark X -> g# X) (g# active X -> g# X, g# active X -> g# X) (f# active X -> f# X, f# mark X -> f# X) (f# active X -> f# X, f# active X -> f# X) (mark# s X -> mark# X, mark# cons(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# f X -> mark# X) (mark# s X -> mark# X, mark# f X -> f# mark X) (mark# s X -> mark# X, mark# f X -> active# f mark X) (mark# s X -> mark# X, mark# g X -> mark# X) (mark# s X -> mark# X, mark# g X -> g# mark X) (mark# s X -> mark# X, mark# g X -> active# g mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (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# 0() -> active# 0()) (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X2) (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# f X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# f X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# f X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# f X -> mark# X, mark# f X -> mark# X) (mark# f X -> mark# X, mark# f X -> f# mark X) (mark# f X -> mark# X, mark# f X -> active# f mark X) (mark# f X -> mark# X, mark# g X -> mark# X) (mark# f X -> mark# X, mark# g X -> g# mark X) (mark# f X -> mark# X, mark# g X -> active# g mark X) (mark# f X -> mark# X, mark# s X -> mark# X) (mark# f X -> mark# X, mark# s X -> active# s mark X) (mark# f X -> mark# X, mark# s X -> s# mark X) (mark# f X -> mark# X, mark# 0() -> active# 0()) (mark# f X -> mark# X, mark# sel(X1, X2) -> mark# X1) (mark# f X -> mark# X, mark# sel(X1, X2) -> mark# X2) (mark# f X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# f X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) } STATUS: arrows: 0.889979 SCCS (6): Scc: { mark# cons(X1, X2) -> mark# X1, mark# f X -> mark# X, mark# f X -> active# f mark X, mark# g X -> mark# X, mark# g X -> active# g mark X, mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# f X -> mark# cons(X, f g X), active# g s X -> mark# s s g X, active# g 0() -> mark# s 0(), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), active# sel(0(), cons(X, Y)) -> mark# X} 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: { s# mark X -> s# X, s# active X -> s# X} Scc: { g# mark X -> g# X, g# active X -> g# X} Scc: { f# mark X -> f# X, f# active X -> f# X} 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 (14): Strict: { mark# cons(X1, X2) -> mark# X1, mark# f X -> mark# X, mark# f X -> active# f mark X, mark# g X -> mark# X, mark# g X -> active# g mark X, mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# f X -> mark# cons(X, f g X), active# g s X -> mark# s s g X, active# g 0() -> mark# s 0(), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), active# sel(0(), cons(X, Y)) -> mark# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} Fail 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 cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [sel](x0, x1) = 0, [mark](x0) = x0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [s](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: 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 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 1 + 0X + 0Y >= 0 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 1 + 0X + 0Y + 0Z >= 0 + 0X + 0Z active g 0() -> mark s 0() 1 >= 0 active g s X -> mark s s g X 1 + 0X >= 0 + 0X active f X -> mark cons(X, f g X) 1 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X cons(active X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(mark X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, active X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, mark X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark sel(X1, X2) -> active sel(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark 0() -> active 0() 0 >= 1 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark cons(X1, X2) -> active cons(mark X1, 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 cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1 + 1, [sel](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [f](x0) = 0, [g](x0) = x0 + 1, [active](x0) = x0, [s](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: sel(active X1, X2) -> sel(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 sel(mark X1, X2) -> sel(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 sel(X1, active X2) -> sel(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 sel(X1, mark X2) -> sel(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X active sel(0(), cons(X, Y)) -> mark X 2 + 1X + 1Y >= 1 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 2 + 1X + 1Y + 1Z >= 1 + 1X + 1Z active g 0() -> mark s 0() 2 >= 3 active g s X -> mark s s g X 2 + 1X >= 4 + 1X active f X -> mark cons(X, f g X) 0 + 0X >= 2 + 1X g active X -> g X 1 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X 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 mark sel(X1, X2) -> active sel(mark X1, mark X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 mark 0() -> active 0() 2 >= 1 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark g X -> active g mark X 2 + 1X >= 2 + 1X mark f X -> active f mark X 1 + 0X >= 0 + 0X mark cons(X1, X2) -> active cons(mark X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 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 cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [sel](x0, x1) = 0, [mark](x0) = x0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [s](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: 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 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 1 + 0X + 0Y >= 0 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 1 + 0X + 0Y + 0Z >= 0 + 0X + 0Z active g 0() -> mark s 0() 1 >= 0 active g s X -> mark s s g X 1 + 0X >= 0 + 0X active f X -> mark cons(X, f g X) 1 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X cons(active X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(mark X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, active X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, mark X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark sel(X1, X2) -> active sel(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark 0() -> active 0() 0 >= 1 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark cons(X1, X2) -> active cons(mark X1, 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 cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1 + 1, [sel](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [s](x0) = 0, [0] = 1, [sel#](x0, x1) = x0 Strict: sel#(X1, mark X2) -> sel#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: sel(active X1, X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(mark X1, X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(X1, active X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(X1, mark X2) -> sel(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 2 + 1X + 1Y >= 1 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 2 + 0X + 1Y + 1Z >= 2 + 0X + 1Z active g 0() -> mark s 0() 2 >= 1 active g s X -> mark s s g X 1 + 0X >= 1 + 0X active f X -> mark cons(X, f g X) 1 + 1X >= 4 + 2X g active X -> g X 1 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 1 + 1X >= 1 + 1X f mark X -> f X 2 + 1X >= 1 + 1X 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 mark sel(X1, X2) -> active sel(mark X1, mark X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 mark 0() -> active 0() 2 >= 1 mark s X -> active s mark X 1 + 0X >= 0 + 0X mark g X -> active g mark X 2 + 1X >= 2 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark cons(X1, X2) -> active cons(mark X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed SCC (2): Strict: { s# mark X -> s# X, s# active X -> s# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [sel](x0, x1) = 0, [mark](x0) = x0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [s](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: 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 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 1 + 0X + 0Y >= 0 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 1 + 0X + 0Y + 0Z >= 0 + 0X + 0Z active g 0() -> mark s 0() 1 >= 0 active g s X -> mark s s g X 1 + 0X >= 0 + 0X active f X -> mark cons(X, f g X) 1 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X cons(active X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(mark X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, active X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, mark X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark sel(X1, X2) -> active sel(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark 0() -> active 0() 0 >= 1 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark cons(X1, X2) -> active cons(mark X1, 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 cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1 + 1, [sel](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [s](x0) = 0, [0] = 1, [s#](x0) = x0 Strict: s# mark X -> s# X 1 + 1X >= 0 + 1X Weak: sel(active X1, X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(mark X1, X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(X1, active X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(X1, mark X2) -> sel(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 2 + 1X + 1Y >= 1 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 2 + 0X + 1Y + 1Z >= 2 + 0X + 1Z active g 0() -> mark s 0() 2 >= 1 active g s X -> mark s s g X 1 + 0X >= 1 + 0X active f X -> mark cons(X, f g X) 1 + 1X >= 4 + 2X g active X -> g X 1 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 1 + 1X >= 1 + 1X f mark X -> f X 2 + 1X >= 1 + 1X 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 mark sel(X1, X2) -> active sel(mark X1, mark X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 mark 0() -> active 0() 2 >= 1 mark s X -> active s mark X 1 + 0X >= 0 + 0X mark g X -> active g mark X 2 + 1X >= 2 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark cons(X1, X2) -> active cons(mark X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed SCC (2): Strict: { g# mark X -> g# X, g# active X -> g# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [sel](x0, x1) = 0, [mark](x0) = x0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [s](x0) = 0, [0] = 0, [g#](x0) = x0 Strict: g# active X -> g# X 1 + 1X >= 0 + 1X g# mark X -> g# X 0 + 1X >= 0 + 1X Weak: 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 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 1 + 0X + 0Y >= 0 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 1 + 0X + 0Y + 0Z >= 0 + 0X + 0Z active g 0() -> mark s 0() 1 >= 0 active g s X -> mark s s g X 1 + 0X >= 0 + 0X active f X -> mark cons(X, f g X) 1 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X cons(active X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(mark X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, active X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, mark X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark sel(X1, X2) -> active sel(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark 0() -> active 0() 0 >= 1 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark cons(X1, X2) -> active cons(mark X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 SCCS (1): Scc: {g# mark X -> g# X} SCC (1): Strict: {g# mark X -> g# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1 + 1, [sel](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [s](x0) = 0, [0] = 1, [g#](x0) = x0 Strict: g# mark X -> g# X 1 + 1X >= 0 + 1X Weak: sel(active X1, X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(mark X1, X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(X1, active X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(X1, mark X2) -> sel(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 2 + 1X + 1Y >= 1 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 2 + 0X + 1Y + 1Z >= 2 + 0X + 1Z active g 0() -> mark s 0() 2 >= 1 active g s X -> mark s s g X 1 + 0X >= 1 + 0X active f X -> mark cons(X, f g X) 1 + 1X >= 4 + 2X g active X -> g X 1 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 1 + 1X >= 1 + 1X f mark X -> f X 2 + 1X >= 1 + 1X 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 mark sel(X1, X2) -> active sel(mark X1, mark X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 mark 0() -> active 0() 2 >= 1 mark s X -> active s mark X 1 + 0X >= 0 + 0X mark g X -> active g mark X 2 + 1X >= 2 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark cons(X1, X2) -> active cons(mark X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed SCC (2): Strict: { f# mark X -> f# X, f# active X -> f# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [sel](x0, x1) = 0, [mark](x0) = x0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [s](x0) = 0, [0] = 0, [f#](x0) = x0 Strict: f# active X -> f# X 1 + 1X >= 0 + 1X f# mark X -> f# X 0 + 1X >= 0 + 1X Weak: 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 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 1 + 0X + 0Y >= 0 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 1 + 0X + 0Y + 0Z >= 0 + 0X + 0Z active g 0() -> mark s 0() 1 >= 0 active g s X -> mark s s g X 1 + 0X >= 0 + 0X active f X -> mark cons(X, f g X) 1 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X cons(active X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(mark X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, active X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, mark X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark sel(X1, X2) -> active sel(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark 0() -> active 0() 0 >= 1 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark cons(X1, X2) -> active cons(mark X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 SCCS (1): Scc: {f# mark X -> f# X} SCC (1): Strict: {f# mark X -> f# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1 + 1, [sel](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [s](x0) = 0, [0] = 1, [f#](x0) = x0 Strict: f# mark X -> f# X 1 + 1X >= 0 + 1X Weak: sel(active X1, X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(mark X1, X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(X1, active X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(X1, mark X2) -> sel(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 2 + 1X + 1Y >= 1 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 2 + 0X + 1Y + 1Z >= 2 + 0X + 1Z active g 0() -> mark s 0() 2 >= 1 active g s X -> mark s s g X 1 + 0X >= 1 + 0X active f X -> mark cons(X, f g X) 1 + 1X >= 4 + 2X g active X -> g X 1 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 1 + 1X >= 1 + 1X f mark X -> f X 2 + 1X >= 1 + 1X 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 mark sel(X1, X2) -> active sel(mark X1, mark X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 mark 0() -> active 0() 2 >= 1 mark s X -> active s mark X 1 + 0X >= 0 + 0X mark g X -> active g mark X 2 + 1X >= 2 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark cons(X1, X2) -> active cons(mark X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 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 cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [sel](x0, x1) = 0, [mark](x0) = x0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [s](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: 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 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 1 + 0X + 0Y >= 0 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 1 + 0X + 0Y + 0Z >= 0 + 0X + 0Z active g 0() -> mark s 0() 1 >= 0 active g s X -> mark s s g X 1 + 0X >= 0 + 0X active f X -> mark cons(X, f g X) 1 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X cons(active X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(mark X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, active X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, mark X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark sel(X1, X2) -> active sel(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark 0() -> active 0() 0 >= 1 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark cons(X1, X2) -> active cons(mark X1, 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 cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1 + 1, [sel](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [f](x0) = 0, [g](x0) = x0 + 1, [active](x0) = x0, [s](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: sel(active X1, X2) -> sel(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 sel(mark X1, X2) -> sel(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 sel(X1, active X2) -> sel(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 sel(X1, mark X2) -> sel(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X active sel(0(), cons(X, Y)) -> mark X 2 + 1X + 1Y >= 1 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 2 + 1X + 1Y + 1Z >= 1 + 1X + 1Z active g 0() -> mark s 0() 2 >= 3 active g s X -> mark s s g X 2 + 1X >= 4 + 1X active f X -> mark cons(X, f g X) 0 + 0X >= 2 + 1X g active X -> g X 1 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X 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 mark sel(X1, X2) -> active sel(mark X1, mark X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 mark 0() -> active 0() 2 >= 1 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark g X -> active g mark X 2 + 1X >= 2 + 1X mark f X -> active f mark X 1 + 0X >= 0 + 0X mark cons(X1, X2) -> active cons(mark X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 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 cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [sel](x0, x1) = 0, [mark](x0) = x0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [s](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: 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 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 1 + 0X + 0Y >= 0 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 1 + 0X + 0Y + 0Z >= 0 + 0X + 0Z active g 0() -> mark s 0() 1 >= 0 active g s X -> mark s s g X 1 + 0X >= 0 + 0X active f X -> mark cons(X, f g X) 1 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X cons(active X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(mark X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, active X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 cons(X1, mark X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark sel(X1, X2) -> active sel(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark 0() -> active 0() 0 >= 1 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark cons(X1, X2) -> active cons(mark X1, 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 cons(X1, X2) -> active cons(mark X1, X2), mark f X -> active f mark X, mark g X -> active g mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark sel(X1, X2) -> active sel(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f X -> mark cons(X, f g X), active g s X -> mark s s g X, active g 0() -> mark s 0(), active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active sel(0(), cons(X, Y)) -> mark X, s mark X -> s X, s active X -> s X, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1 + 1, [sel](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [s](x0) = 0, [0] = 1, [cons#](x0, x1) = x0 Strict: cons#(X1, mark X2) -> cons#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: sel(active X1, X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(mark X1, X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(X1, active X2) -> sel(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 sel(X1, mark X2) -> sel(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X active sel(0(), cons(X, Y)) -> mark X 2 + 1X + 1Y >= 1 + 1X active sel(s X, cons(Y, Z)) -> mark sel(X, Z) 2 + 0X + 1Y + 1Z >= 2 + 0X + 1Z active g 0() -> mark s 0() 2 >= 1 active g s X -> mark s s g X 1 + 0X >= 1 + 0X active f X -> mark cons(X, f g X) 1 + 1X >= 4 + 2X g active X -> g X 1 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 1 + 1X >= 1 + 1X f mark X -> f X 2 + 1X >= 1 + 1X 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 mark sel(X1, X2) -> active sel(mark X1, mark X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 mark 0() -> active 0() 2 >= 1 mark s X -> active s mark X 1 + 0X >= 0 + 0X mark g X -> active g mark X 2 + 1X >= 2 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark cons(X1, X2) -> active cons(mark X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed