MAYBE Time: 0.674851 TRS: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} DP: DP: { cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2), incr# mark X -> incr# X, incr# ok X -> incr# X, active# cons(X1, X2) -> cons#(active X1, X2), active# cons(X1, X2) -> active# X1, active# incr X -> incr# active X, active# incr X -> active# X, active# incr cons(X, XS) -> cons#(s X, incr XS), active# incr cons(X, XS) -> incr# XS, active# incr cons(X, XS) -> s# X, active# nats() -> cons#(0(), incr nats()), active# nats() -> incr# nats(), active# odds() -> incr# pairs(), active# pairs() -> cons#(0(), incr odds()), active# pairs() -> incr# odds(), active# s X -> active# X, active# s X -> s# active X, active# head X -> active# X, active# head X -> head# active X, active# tail X -> active# X, active# tail X -> tail# active X, s# mark X -> s# X, s# ok X -> s# X, head# mark X -> head# X, head# ok X -> head# X, tail# mark X -> tail# X, tail# ok X -> tail# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2), proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# incr X -> incr# proper X, proper# incr X -> proper# X, proper# s X -> s# proper X, proper# s X -> proper# X, proper# head X -> head# proper X, proper# head X -> proper# X, proper# tail X -> tail# proper X, proper# tail X -> proper# X, top# mark X -> proper# X, top# mark X -> top# proper X, top# ok X -> active# X, top# ok X -> top# active X} TRS: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} UR: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X} EDG: { (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2)) (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2)) (incr# ok X -> incr# X, incr# ok X -> incr# X) (incr# ok X -> incr# X, incr# mark X -> incr# X) (active# incr cons(X, XS) -> s# X, s# ok X -> s# X) (active# incr cons(X, XS) -> s# X, s# mark X -> s# X) (active# head X -> active# X, active# tail X -> tail# active X) (active# head X -> active# X, active# tail X -> active# X) (active# head X -> active# X, active# head X -> head# active X) (active# head X -> active# X, active# head X -> active# X) (active# head X -> active# X, active# s X -> s# active X) (active# head X -> active# X, active# s X -> active# X) (active# head X -> active# X, active# pairs() -> incr# odds()) (active# head X -> active# X, active# pairs() -> cons#(0(), incr odds())) (active# head X -> active# X, active# odds() -> incr# pairs()) (active# head X -> active# X, active# nats() -> incr# nats()) (active# head X -> active# X, active# nats() -> cons#(0(), incr nats())) (active# head X -> active# X, active# incr cons(X, XS) -> s# X) (active# head X -> active# X, active# incr cons(X, XS) -> incr# XS) (active# head X -> active# X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (active# head X -> active# X, active# incr X -> active# X) (active# head X -> active# X, active# incr X -> incr# active X) (active# head X -> active# X, active# cons(X1, X2) -> active# X1) (active# head X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2)) (s# mark X -> s# X, s# ok X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (head# mark X -> head# X, head# ok X -> head# X) (head# mark X -> head# X, head# mark X -> head# X) (tail# mark X -> tail# X, tail# ok X -> tail# X) (tail# mark X -> tail# X, tail# mark X -> tail# X) (proper# incr X -> proper# X, proper# tail X -> proper# X) (proper# incr X -> proper# X, proper# tail X -> tail# proper X) (proper# incr X -> proper# X, proper# head X -> proper# X) (proper# incr X -> proper# X, proper# head X -> head# proper X) (proper# incr X -> proper# X, proper# s X -> proper# X) (proper# incr X -> proper# X, proper# s X -> s# proper X) (proper# incr X -> proper# X, proper# incr X -> proper# X) (proper# incr X -> proper# X, proper# incr X -> incr# proper X) (proper# incr X -> proper# X, proper# cons(X1, X2) -> proper# X2) (proper# incr X -> proper# X, proper# cons(X1, X2) -> proper# X1) (proper# incr X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# head X -> proper# X, proper# tail X -> proper# X) (proper# head X -> proper# X, proper# tail X -> tail# proper X) (proper# head X -> proper# X, proper# head X -> proper# X) (proper# head X -> proper# X, proper# head X -> head# proper X) (proper# head X -> proper# X, proper# s X -> proper# X) (proper# head X -> proper# X, proper# s X -> s# proper X) (proper# head X -> proper# X, proper# incr X -> proper# X) (proper# head X -> proper# X, proper# incr X -> incr# proper X) (proper# head X -> proper# X, proper# cons(X1, X2) -> proper# X2) (proper# head X -> proper# X, proper# cons(X1, X2) -> proper# X1) (proper# head X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (top# mark X -> proper# X, proper# tail X -> proper# X) (top# mark X -> proper# X, proper# tail X -> tail# proper X) (top# mark X -> proper# X, proper# head X -> proper# X) (top# mark X -> proper# X, proper# head X -> head# proper X) (top# mark X -> proper# X, proper# s X -> proper# X) (top# mark X -> proper# X, proper# s X -> s# proper X) (top# mark X -> proper# X, proper# incr X -> proper# X) (top# mark X -> proper# X, proper# incr X -> incr# proper X) (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2) (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1) (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2)) (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (active# incr X -> incr# active X, incr# ok X -> incr# X) (active# incr X -> incr# active X, incr# mark X -> incr# X) (active# head X -> head# active X, head# ok X -> head# X) (active# head X -> head# active X, head# mark X -> head# X) (proper# incr X -> incr# proper X, incr# ok X -> incr# X) (proper# incr X -> incr# proper X, incr# mark X -> incr# X) (proper# head X -> head# proper X, head# ok X -> head# X) (proper# head X -> head# proper X, head# mark X -> head# X) (top# mark X -> top# proper X, top# ok X -> top# active X) (top# mark X -> top# proper X, top# ok X -> active# X) (top# mark X -> top# proper X, top# mark X -> top# proper X) (top# mark X -> top# proper X, top# mark X -> proper# X) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (active# cons(X1, X2) -> active# X1, active# tail X -> tail# active X) (active# cons(X1, X2) -> active# X1, active# tail X -> active# X) (active# cons(X1, X2) -> active# X1, active# head X -> head# active X) (active# cons(X1, X2) -> active# X1, active# head X -> active# X) (active# cons(X1, X2) -> active# X1, active# s X -> s# active X) (active# cons(X1, X2) -> active# X1, active# s X -> active# X) (active# cons(X1, X2) -> active# X1, active# pairs() -> incr# odds()) (active# cons(X1, X2) -> active# X1, active# pairs() -> cons#(0(), incr odds())) (active# cons(X1, X2) -> active# X1, active# odds() -> incr# pairs()) (active# cons(X1, X2) -> active# X1, active# nats() -> incr# nats()) (active# cons(X1, X2) -> active# X1, active# nats() -> cons#(0(), incr nats())) (active# cons(X1, X2) -> active# X1, active# incr cons(X, XS) -> s# X) (active# cons(X1, X2) -> active# X1, active# incr cons(X, XS) -> incr# XS) (active# cons(X1, X2) -> active# X1, active# incr cons(X, XS) -> cons#(s X, incr XS)) (active# cons(X1, X2) -> active# X1, active# incr X -> active# X) (active# cons(X1, X2) -> active# X1, active# incr X -> incr# active X) (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1) (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2)) (active# incr cons(X, XS) -> incr# XS, incr# mark X -> incr# X) (active# incr cons(X, XS) -> incr# XS, incr# ok X -> incr# X) (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X1, proper# incr X -> incr# proper X) (proper# cons(X1, X2) -> proper# X1, proper# incr X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X) (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# head X -> head# proper X) (proper# cons(X1, X2) -> proper# X1, proper# head X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# tail X -> tail# proper X) (proper# cons(X1, X2) -> proper# X1, proper# tail X -> proper# X) (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2)) (top# ok X -> top# active X, top# mark X -> proper# X) (top# ok X -> top# active X, top# mark X -> top# proper X) (top# ok X -> top# active X, top# ok X -> active# X) (top# ok X -> top# active X, top# ok X -> top# active X) (proper# tail X -> tail# proper X, tail# mark X -> tail# X) (proper# tail X -> tail# proper X, tail# ok X -> tail# X) (proper# s X -> s# proper X, s# mark X -> s# X) (proper# s X -> s# proper X, s# ok X -> s# X) (active# tail X -> tail# active X, tail# mark X -> tail# X) (active# tail X -> tail# active X, tail# ok X -> tail# X) (active# s X -> s# active X, s# mark X -> s# X) (active# s X -> s# active X, s# ok X -> s# X) (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X2, proper# incr X -> incr# proper X) (proper# cons(X1, X2) -> proper# X2, proper# incr X -> proper# X) (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X) (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X) (proper# cons(X1, X2) -> proper# X2, proper# head X -> head# proper X) (proper# cons(X1, X2) -> proper# X2, proper# head X -> proper# X) (proper# cons(X1, X2) -> proper# X2, proper# tail X -> tail# proper X) (proper# cons(X1, X2) -> proper# X2, proper# tail X -> proper# X) (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2)) (top# ok X -> active# X, active# cons(X1, X2) -> active# X1) (top# ok X -> active# X, active# incr X -> incr# active X) (top# ok X -> active# X, active# incr X -> active# X) (top# ok X -> active# X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (top# ok X -> active# X, active# incr cons(X, XS) -> incr# XS) (top# ok X -> active# X, active# incr cons(X, XS) -> s# X) (top# ok X -> active# X, active# nats() -> cons#(0(), incr nats())) (top# ok X -> active# X, active# nats() -> incr# nats()) (top# ok X -> active# X, active# odds() -> incr# pairs()) (top# ok X -> active# X, active# pairs() -> cons#(0(), incr odds())) (top# ok X -> active# X, active# pairs() -> incr# odds()) (top# ok X -> active# X, active# s X -> active# X) (top# ok X -> active# X, active# s X -> s# active X) (top# ok X -> active# X, active# head X -> active# X) (top# ok X -> active# X, active# head X -> head# active X) (top# ok X -> active# X, active# tail X -> active# X) (top# ok X -> active# X, active# tail X -> tail# active X) (proper# tail X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# tail X -> proper# X, proper# cons(X1, X2) -> proper# X1) (proper# tail X -> proper# X, proper# cons(X1, X2) -> proper# X2) (proper# tail X -> proper# X, proper# incr X -> incr# proper X) (proper# tail X -> proper# X, proper# incr X -> proper# X) (proper# tail X -> proper# X, proper# s X -> s# proper X) (proper# tail X -> proper# X, proper# s X -> proper# X) (proper# tail X -> proper# X, proper# head X -> head# proper X) (proper# tail X -> proper# X, proper# head X -> proper# X) (proper# tail X -> proper# X, proper# tail X -> tail# proper X) (proper# tail X -> proper# X, proper# tail X -> proper# X) (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1) (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2) (proper# s X -> proper# X, proper# incr X -> incr# proper X) (proper# s X -> proper# X, proper# incr X -> proper# X) (proper# s X -> proper# X, proper# s X -> s# proper X) (proper# s X -> proper# X, proper# s X -> proper# X) (proper# s X -> proper# X, proper# head X -> head# proper X) (proper# s X -> proper# X, proper# head X -> proper# X) (proper# s X -> proper# X, proper# tail X -> tail# proper X) (proper# s X -> proper# X, proper# tail X -> proper# X) (tail# ok X -> tail# X, tail# mark X -> tail# X) (tail# ok X -> tail# X, tail# ok X -> tail# X) (head# ok X -> head# X, head# mark X -> head# X) (head# ok X -> head# X, head# ok X -> head# X) (s# ok X -> s# X, s# mark X -> s# X) (s# ok X -> s# X, s# ok X -> s# X) (active# tail X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2)) (active# tail X -> active# X, active# cons(X1, X2) -> active# X1) (active# tail X -> active# X, active# incr X -> incr# active X) (active# tail X -> active# X, active# incr X -> active# X) (active# tail X -> active# X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (active# tail X -> active# X, active# incr cons(X, XS) -> incr# XS) (active# tail X -> active# X, active# incr cons(X, XS) -> s# X) (active# tail X -> active# X, active# nats() -> cons#(0(), incr nats())) (active# tail X -> active# X, active# nats() -> incr# nats()) (active# tail X -> active# X, active# odds() -> incr# pairs()) (active# tail X -> active# X, active# pairs() -> cons#(0(), incr odds())) (active# tail X -> active# X, active# pairs() -> incr# odds()) (active# tail X -> active# X, active# s X -> active# X) (active# tail X -> active# X, active# s X -> s# active X) (active# tail X -> active# X, active# head X -> active# X) (active# tail X -> active# X, active# head X -> head# active X) (active# tail X -> active# X, active# tail X -> active# X) (active# tail X -> active# X, active# tail X -> tail# active X) (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2)) (active# s X -> active# X, active# cons(X1, X2) -> active# X1) (active# s X -> active# X, active# incr X -> incr# active X) (active# s X -> active# X, active# incr X -> active# X) (active# s X -> active# X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (active# s X -> active# X, active# incr cons(X, XS) -> incr# XS) (active# s X -> active# X, active# incr cons(X, XS) -> s# X) (active# s X -> active# X, active# nats() -> cons#(0(), incr nats())) (active# s X -> active# X, active# nats() -> incr# nats()) (active# s X -> active# X, active# odds() -> incr# pairs()) (active# s X -> active# X, active# pairs() -> cons#(0(), incr odds())) (active# s X -> active# X, active# pairs() -> incr# odds()) (active# s X -> active# X, active# s X -> active# X) (active# s X -> active# X, active# s X -> s# active X) (active# s X -> active# X, active# head X -> active# X) (active# s X -> active# X, active# head X -> head# active X) (active# s X -> active# X, active# tail X -> active# X) (active# s X -> active# X, active# tail X -> tail# active X) (active# incr X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2)) (active# incr X -> active# X, active# cons(X1, X2) -> active# X1) (active# incr X -> active# X, active# incr X -> incr# active X) (active# incr X -> active# X, active# incr X -> active# X) (active# incr X -> active# X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (active# incr X -> active# X, active# incr cons(X, XS) -> incr# XS) (active# incr X -> active# X, active# incr cons(X, XS) -> s# X) (active# incr X -> active# X, active# nats() -> cons#(0(), incr nats())) (active# incr X -> active# X, active# nats() -> incr# nats()) (active# incr X -> active# X, active# odds() -> incr# pairs()) (active# incr X -> active# X, active# pairs() -> cons#(0(), incr odds())) (active# incr X -> active# X, active# pairs() -> incr# odds()) (active# incr X -> active# X, active# s X -> active# X) (active# incr X -> active# X, active# s X -> s# active X) (active# incr X -> active# X, active# head X -> active# X) (active# incr X -> active# X, active# head X -> head# active X) (active# incr X -> active# X, active# tail X -> active# X) (active# incr X -> active# X, active# tail X -> tail# active X) (incr# mark X -> incr# X, incr# mark X -> incr# X) (incr# mark X -> incr# X, incr# ok X -> incr# X) (active# incr cons(X, XS) -> cons#(s X, incr XS), cons#(mark X1, X2) -> cons#(X1, X2)) (active# incr cons(X, XS) -> cons#(s X, incr XS), cons#(ok X1, ok X2) -> cons#(X1, X2)) } STATUS: arrows: 0.870741 SCCS (8): Scc: {top# mark X -> top# proper X, top# ok X -> top# active X} Scc: {proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# incr X -> proper# X, proper# s X -> proper# X, proper# head X -> proper# X, proper# tail X -> proper# X} Scc: {active# cons(X1, X2) -> active# X1, active# incr X -> active# X, active# s X -> active# X, active# head X -> active# X, active# tail X -> active# X} Scc: {tail# mark X -> tail# X, tail# ok X -> tail# X} Scc: {head# mark X -> head# X, head# ok X -> head# X} Scc: {s# mark X -> s# X, s# ok X -> s# X} Scc: {incr# mark X -> incr# X, incr# ok X -> incr# X} Scc: { cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2)} SCC (2): Strict: {top# mark X -> top# proper X, top# ok X -> top# active X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} Fail SCC (6): Strict: {proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# incr X -> proper# X, proper# s X -> proper# X, proper# head X -> proper# X, proper# tail X -> proper# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [mark](x0) = 0, [incr](x0) = x0, [active](x0) = 0, [s](x0) = x0, [head](x0) = x0, [tail](x0) = x0 + 1, [ok](x0) = x0 + 1, [proper](x0) = 0, [top](x0) = 0, [0] = 0, [nats] = 0, [odds] = 0, [pairs] = 0, [proper#](x0) = x0 Strict: proper# tail X -> proper# X 1 + 1X >= 0 + 1X proper# head X -> proper# X 0 + 1X >= 0 + 1X proper# s X -> proper# X 0 + 1X >= 0 + 1X proper# incr X -> proper# X 0 + 1X >= 0 + 1X proper# cons(X1, X2) -> proper# X2 0 + 1X1 + 1X2 >= 0 + 1X2 proper# cons(X1, X2) -> proper# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 0 + 0X >= 1 + 0X proper head X -> head proper X 0 + 0X >= 0 + 0X proper s X -> s proper X 0 + 0X >= 0 + 0X proper pairs() -> ok pairs() 0 >= 1 proper odds() -> ok odds() 0 >= 1 proper nats() -> ok nats() 0 >= 1 proper incr X -> incr proper X 0 + 0X >= 0 + 0X proper 0() -> ok 0() 0 >= 1 proper cons(X1, X2) -> cons(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 tail ok X -> ok tail X 2 + 1X >= 2 + 1X tail mark X -> mark tail X 1 + 0X >= 0 + 0X head ok X -> ok head X 1 + 1X >= 1 + 1X head mark X -> mark head X 0 + 0X >= 0 + 0X s ok X -> ok s X 1 + 1X >= 1 + 1X s mark X -> mark s X 0 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 0XS active tail X -> tail active X 0 + 0X >= 1 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 0X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 0 + 0X >= 0 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 0 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 0 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 incr ok X -> ok incr X 1 + 1X >= 1 + 1X incr mark X -> mark incr X 0 + 0X >= 0 + 0X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# incr X -> proper# X, proper# s X -> proper# X, proper# head X -> proper# X} SCC (5): Strict: {proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# incr X -> proper# X, proper# s X -> proper# X, proper# head X -> proper# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [mark](x0) = 0, [incr](x0) = x0, [active](x0) = 0, [s](x0) = x0, [head](x0) = x0 + 1, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = 0, [top](x0) = 0, [0] = 0, [nats] = 0, [odds] = 1, [pairs] = 0, [proper#](x0) = x0 Strict: proper# head X -> proper# X 1 + 1X >= 0 + 1X proper# s X -> proper# X 0 + 1X >= 0 + 1X proper# incr X -> proper# X 0 + 1X >= 0 + 1X proper# cons(X1, X2) -> proper# X2 0 + 1X1 + 1X2 >= 0 + 1X2 proper# cons(X1, X2) -> proper# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 0 + 0X >= 0 + 0X proper head X -> head proper X 0 + 0X >= 1 + 0X proper s X -> s proper X 0 + 0X >= 0 + 0X proper pairs() -> ok pairs() 0 >= 1 proper odds() -> ok odds() 0 >= 2 proper nats() -> ok nats() 0 >= 1 proper incr X -> incr proper X 0 + 0X >= 0 + 0X proper 0() -> ok 0() 0 >= 1 proper cons(X1, X2) -> cons(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 0 + 0X head ok X -> ok head X 2 + 1X >= 2 + 1X head mark X -> mark head X 1 + 0X >= 0 + 0X s ok X -> ok s X 1 + 1X >= 1 + 1X s mark X -> mark s X 0 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 0XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 0X active head X -> head active X 0 + 0X >= 1 + 0X active s X -> s active X 0 + 0X >= 0 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 0 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 0 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 incr ok X -> ok incr X 1 + 1X >= 1 + 1X incr mark X -> mark incr X 0 + 0X >= 0 + 0X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# incr X -> proper# X, proper# s X -> proper# X} SCC (4): Strict: {proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# incr X -> proper# X, proper# s X -> proper# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [mark](x0) = 0, [incr](x0) = x0, [active](x0) = 0, [s](x0) = x0 + 1, [head](x0) = 0, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = 0, [0] = 0, [nats] = 0, [odds] = 0, [pairs] = 0, [proper#](x0) = x0 Strict: proper# s X -> proper# X 1 + 1X >= 0 + 1X proper# incr X -> proper# X 0 + 1X >= 0 + 1X proper# cons(X1, X2) -> proper# X2 0 + 1X1 + 1X2 >= 0 + 1X2 proper# cons(X1, X2) -> proper# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 1 + 0X >= 0 + 0X proper head X -> head proper X 1 + 0X >= 0 + 0X proper s X -> s proper X 2 + 1X >= 2 + 1X proper pairs() -> ok pairs() 1 >= 1 proper odds() -> ok odds() 1 >= 1 proper nats() -> ok nats() 1 >= 1 proper incr X -> incr proper X 1 + 1X >= 1 + 1X proper 0() -> ok 0() 1 >= 1 proper cons(X1, X2) -> cons(proper X1, proper X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 0 + 0X head ok X -> ok head X 0 + 0X >= 1 + 0X head mark X -> mark head X 0 + 0X >= 0 + 0X s ok X -> ok s X 2 + 1X >= 2 + 1X s mark X -> mark s X 1 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 0XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 0X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 0 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 0 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 0 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 incr ok X -> ok incr X 1 + 1X >= 1 + 1X incr mark X -> mark incr X 0 + 0X >= 0 + 0X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# incr X -> proper# X} SCC (3): Strict: {proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# incr X -> proper# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [mark](x0) = 0, [incr](x0) = x0 + 1, [active](x0) = 0, [s](x0) = 1, [head](x0) = 0, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = 0, [0] = 0, [nats] = 1, [odds] = 1, [pairs] = 1, [proper#](x0) = x0 Strict: proper# incr X -> proper# X 1 + 1X >= 0 + 1X proper# cons(X1, X2) -> proper# X2 0 + 1X1 + 1X2 >= 0 + 1X2 proper# cons(X1, X2) -> proper# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 1 + 0X >= 0 + 0X proper head X -> head proper X 1 + 0X >= 0 + 0X proper s X -> s proper X 2 + 0X >= 1 + 0X proper pairs() -> ok pairs() 2 >= 2 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 1 >= 1 proper cons(X1, X2) -> cons(proper X1, proper X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 0 + 0X head ok X -> ok head X 0 + 0X >= 1 + 0X head mark X -> mark head X 0 + 0X >= 0 + 0X s ok X -> ok s X 1 + 0X >= 2 + 0X s mark X -> mark s X 1 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 0XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 0X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 0 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 0 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 1 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 1 + 0X >= 0 + 0X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2} SCC (2): Strict: {proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1 + 1, [mark](x0) = x0 + 1, [incr](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [head](x0) = 0, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = 0, [top](x0) = x0, [0] = 1, [nats] = 0, [odds] = 0, [pairs] = 1, [proper#](x0) = x0 + 1 Strict: proper# cons(X1, X2) -> proper# X2 2 + 1X1 + 1X2 >= 1 + 1X2 proper# cons(X1, X2) -> proper# X1 2 + 1X1 + 1X2 >= 1 + 1X1 Weak: top ok X -> top active X 1 + 1X >= 0 + 1X top mark X -> top proper X 1 + 1X >= 0 + 0X proper tail X -> tail proper X 0 + 0X >= 0 + 0X proper head X -> head proper X 0 + 0X >= 0 + 0X proper s X -> s proper X 0 + 0X >= 1 + 0X proper pairs() -> ok pairs() 0 >= 2 proper odds() -> ok odds() 0 >= 1 proper nats() -> ok nats() 0 >= 1 proper incr X -> incr proper X 0 + 0X >= 1 + 0X proper 0() -> ok 0() 0 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 1 + 0X head ok X -> ok head X 0 + 0X >= 1 + 0X head mark X -> mark head X 0 + 0X >= 1 + 0X s ok X -> ok s X 2 + 1X >= 2 + 1X s mark X -> mark s X 2 + 1X >= 2 + 1X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 1 + 1XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 1 + 1X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 1 + 1X >= 1 + 1X active pairs() -> mark cons(0(), incr odds()) 1 >= 4 active odds() -> mark incr pairs() 0 >= 3 active nats() -> mark cons(0(), incr nats()) 0 >= 4 active incr cons(X, XS) -> mark cons(s X, incr XS) 2 + 1X + 1XS >= 4 + 1X + 1XS active incr X -> incr active X 1 + 1X >= 1 + 1X active cons(X1, X2) -> cons(active X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 2 + 1X >= 2 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 3 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 cons(mark X1, X2) -> mark cons(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed SCC (5): Strict: {active# cons(X1, X2) -> active# X1, active# incr X -> active# X, active# s X -> active# X, active# head X -> active# X, active# tail X -> active# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [mark](x0) = 0, [incr](x0) = x0, [active](x0) = 0, [s](x0) = x0, [head](x0) = x0, [tail](x0) = x0 + 1, [ok](x0) = x0 + 1, [proper](x0) = 0, [top](x0) = 0, [0] = 0, [nats] = 0, [odds] = 0, [pairs] = 0, [active#](x0) = x0 Strict: active# tail X -> active# X 1 + 1X >= 0 + 1X active# head X -> active# X 0 + 1X >= 0 + 1X active# s X -> active# X 0 + 1X >= 0 + 1X active# incr X -> active# X 0 + 1X >= 0 + 1X active# cons(X1, X2) -> active# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 0 + 0X >= 1 + 0X proper head X -> head proper X 0 + 0X >= 0 + 0X proper s X -> s proper X 0 + 0X >= 0 + 0X proper pairs() -> ok pairs() 0 >= 1 proper odds() -> ok odds() 0 >= 1 proper nats() -> ok nats() 0 >= 1 proper incr X -> incr proper X 0 + 0X >= 0 + 0X proper 0() -> ok 0() 0 >= 1 proper cons(X1, X2) -> cons(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 tail ok X -> ok tail X 2 + 1X >= 2 + 1X tail mark X -> mark tail X 1 + 0X >= 0 + 0X head ok X -> ok head X 1 + 1X >= 1 + 1X head mark X -> mark head X 0 + 0X >= 0 + 0X s ok X -> ok s X 1 + 1X >= 1 + 1X s mark X -> mark s X 0 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 0XS active tail X -> tail active X 0 + 0X >= 1 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 0X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 0 + 0X >= 0 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 0 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 0 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 incr ok X -> ok incr X 1 + 1X >= 1 + 1X incr mark X -> mark incr X 0 + 0X >= 0 + 0X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {active# cons(X1, X2) -> active# X1, active# incr X -> active# X, active# s X -> active# X, active# head X -> active# X} SCC (4): Strict: {active# cons(X1, X2) -> active# X1, active# incr X -> active# X, active# s X -> active# X, active# head X -> active# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [mark](x0) = 0, [incr](x0) = x0, [active](x0) = 0, [s](x0) = x0, [head](x0) = x0 + 1, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = 0, [top](x0) = 0, [0] = 0, [nats] = 0, [odds] = 0, [pairs] = 0, [active#](x0) = x0 Strict: active# head X -> active# X 1 + 1X >= 0 + 1X active# s X -> active# X 0 + 1X >= 0 + 1X active# incr X -> active# X 0 + 1X >= 0 + 1X active# cons(X1, X2) -> active# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 0 + 0X >= 0 + 0X proper head X -> head proper X 0 + 0X >= 1 + 0X proper s X -> s proper X 0 + 0X >= 0 + 0X proper pairs() -> ok pairs() 0 >= 1 proper odds() -> ok odds() 0 >= 1 proper nats() -> ok nats() 0 >= 1 proper incr X -> incr proper X 0 + 0X >= 0 + 0X proper 0() -> ok 0() 0 >= 1 proper cons(X1, X2) -> cons(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 0 + 0X head ok X -> ok head X 2 + 1X >= 2 + 1X head mark X -> mark head X 1 + 0X >= 0 + 0X s ok X -> ok s X 1 + 1X >= 1 + 1X s mark X -> mark s X 0 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 0XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 0X active head X -> head active X 0 + 0X >= 1 + 0X active s X -> s active X 0 + 0X >= 0 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 0 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 0 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 incr ok X -> ok incr X 1 + 1X >= 1 + 1X incr mark X -> mark incr X 0 + 0X >= 0 + 0X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {active# cons(X1, X2) -> active# X1, active# incr X -> active# X, active# s X -> active# X} SCC (3): Strict: {active# cons(X1, X2) -> active# X1, active# incr X -> active# X, active# s X -> active# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [mark](x0) = 0, [incr](x0) = x0, [active](x0) = 0, [s](x0) = x0 + 1, [head](x0) = 0, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = 0, [0] = 0, [nats] = 0, [odds] = 0, [pairs] = 0, [active#](x0) = x0 Strict: active# s X -> active# X 1 + 1X >= 0 + 1X active# incr X -> active# X 0 + 1X >= 0 + 1X active# cons(X1, X2) -> active# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 1 + 0X >= 0 + 0X proper head X -> head proper X 1 + 0X >= 0 + 0X proper s X -> s proper X 2 + 1X >= 2 + 1X proper pairs() -> ok pairs() 1 >= 1 proper odds() -> ok odds() 1 >= 1 proper nats() -> ok nats() 1 >= 1 proper incr X -> incr proper X 1 + 1X >= 1 + 1X proper 0() -> ok 0() 1 >= 1 proper cons(X1, X2) -> cons(proper X1, proper X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 0 + 0X head ok X -> ok head X 0 + 0X >= 1 + 0X head mark X -> mark head X 0 + 0X >= 0 + 0X s ok X -> ok s X 2 + 1X >= 2 + 1X s mark X -> mark s X 1 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 0XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 0X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 0 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 0 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 0 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 incr ok X -> ok incr X 1 + 1X >= 1 + 1X incr mark X -> mark incr X 0 + 0X >= 0 + 0X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {active# cons(X1, X2) -> active# X1, active# incr X -> active# X} SCC (2): Strict: {active# cons(X1, X2) -> active# X1, active# incr X -> active# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [mark](x0) = 0, [incr](x0) = x0 + 1, [active](x0) = 0, [s](x0) = 1, [head](x0) = 0, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = 0, [0] = 0, [nats] = 1, [odds] = 1, [pairs] = 1, [active#](x0) = x0 Strict: active# incr X -> active# X 1 + 1X >= 0 + 1X active# cons(X1, X2) -> active# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 1 + 0X >= 0 + 0X proper head X -> head proper X 1 + 0X >= 0 + 0X proper s X -> s proper X 2 + 0X >= 1 + 0X proper pairs() -> ok pairs() 2 >= 2 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 1 >= 1 proper cons(X1, X2) -> cons(proper X1, proper X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 0 + 0X head ok X -> ok head X 0 + 0X >= 1 + 0X head mark X -> mark head X 0 + 0X >= 0 + 0X s ok X -> ok s X 1 + 0X >= 2 + 0X s mark X -> mark s X 1 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 0XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 0X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 0 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 0 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 1 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 1 + 0X >= 0 + 0X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {active# cons(X1, X2) -> active# X1} SCC (1): Strict: {active# cons(X1, X2) -> active# X1} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [incr](x0) = x0 + 1, [active](x0) = x0 + 1, [s](x0) = 1, [head](x0) = x0 + 1, [tail](x0) = x0 + 1, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = x0 + 1, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 1, [active#](x0) = x0 Strict: active# cons(X1, X2) -> active# X1 1 + 1X1 + 0X2 >= 0 + 1X1 Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper tail X -> tail proper X 2 + 1X >= 2 + 1X proper head X -> head proper X 2 + 1X >= 2 + 1X proper s X -> s proper X 2 + 0X >= 1 + 0X proper pairs() -> ok pairs() 2 >= 2 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 tail ok X -> ok tail X 2 + 1X >= 2 + 1X tail mark X -> mark tail X 2 + 1X >= 2 + 1X head ok X -> ok head X 2 + 1X >= 2 + 1X head mark X -> mark head X 2 + 1X >= 2 + 1X s ok X -> ok s X 1 + 0X >= 2 + 0X s mark X -> mark s X 1 + 0X >= 2 + 0X active tail cons(X, XS) -> mark XS 3 + 1X + 0XS >= 1 + 1XS active tail X -> tail active X 2 + 1X >= 2 + 1X active head cons(X, XS) -> mark X 3 + 1X + 0XS >= 1 + 1X active head X -> head active X 2 + 1X >= 2 + 1X active s X -> s active X 2 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 2 >= 3 active odds() -> mark incr pairs() 2 >= 3 active nats() -> mark cons(0(), incr nats()) 2 >= 3 active incr cons(X, XS) -> mark cons(s X, incr XS) 3 + 1X + 0XS >= 3 + 0X + 0XS active incr X -> incr active X 2 + 1X >= 2 + 1X active cons(X1, X2) -> cons(active X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 2 + 1X >= 2 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 Qed SCC (2): Strict: {tail# mark X -> tail# X, tail# ok X -> tail# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [mark](x0) = x0, [incr](x0) = x0 + 1, [active](x0) = 0, [s](x0) = 0, [head](x0) = 0, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = 0, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 0, [tail#](x0) = x0 Strict: tail# ok X -> tail# X 1 + 1X >= 0 + 1X tail# mark X -> tail# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 1 + 0X >= 0 + 0X proper head X -> head proper X 1 + 0X >= 0 + 0X proper s X -> s proper X 1 + 0X >= 0 + 0X proper pairs() -> ok pairs() 1 >= 1 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 0 + 0X head ok X -> ok head X 0 + 0X >= 1 + 0X head mark X -> mark head X 0 + 0X >= 0 + 0X s ok X -> ok s X 0 + 0X >= 1 + 0X s mark X -> mark s X 0 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 1XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 1X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 0 + 0X >= 0 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 1 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 1 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 1 + 1X >= 1 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {tail# mark X -> tail# X} SCC (1): Strict: {tail# mark X -> tail# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [incr](x0) = x0 + 1, [active](x0) = x0 + 1, [s](x0) = 1, [head](x0) = x0 + 1, [tail](x0) = x0 + 1, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = x0 + 1, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 1, [tail#](x0) = x0 Strict: tail# mark X -> tail# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper tail X -> tail proper X 2 + 1X >= 2 + 1X proper head X -> head proper X 2 + 1X >= 2 + 1X proper s X -> s proper X 2 + 0X >= 1 + 0X proper pairs() -> ok pairs() 2 >= 2 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 tail ok X -> ok tail X 2 + 1X >= 2 + 1X tail mark X -> mark tail X 2 + 1X >= 2 + 1X head ok X -> ok head X 2 + 1X >= 2 + 1X head mark X -> mark head X 2 + 1X >= 2 + 1X s ok X -> ok s X 1 + 0X >= 2 + 0X s mark X -> mark s X 1 + 0X >= 2 + 0X active tail cons(X, XS) -> mark XS 3 + 1X + 0XS >= 1 + 1XS active tail X -> tail active X 2 + 1X >= 2 + 1X active head cons(X, XS) -> mark X 3 + 1X + 0XS >= 1 + 1X active head X -> head active X 2 + 1X >= 2 + 1X active s X -> s active X 2 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 2 >= 3 active odds() -> mark incr pairs() 2 >= 3 active nats() -> mark cons(0(), incr nats()) 2 >= 3 active incr cons(X, XS) -> mark cons(s X, incr XS) 3 + 1X + 0XS >= 3 + 0X + 0XS active incr X -> incr active X 2 + 1X >= 2 + 1X active cons(X1, X2) -> cons(active X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 2 + 1X >= 2 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 Qed SCC (2): Strict: {head# mark X -> head# X, head# ok X -> head# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [mark](x0) = x0, [incr](x0) = x0 + 1, [active](x0) = 0, [s](x0) = 0, [head](x0) = 0, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = 0, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 0, [head#](x0) = x0 Strict: head# ok X -> head# X 1 + 1X >= 0 + 1X head# mark X -> head# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 1 + 0X >= 0 + 0X proper head X -> head proper X 1 + 0X >= 0 + 0X proper s X -> s proper X 1 + 0X >= 0 + 0X proper pairs() -> ok pairs() 1 >= 1 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 0 + 0X head ok X -> ok head X 0 + 0X >= 1 + 0X head mark X -> mark head X 0 + 0X >= 0 + 0X s ok X -> ok s X 0 + 0X >= 1 + 0X s mark X -> mark s X 0 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 1XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 1X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 0 + 0X >= 0 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 1 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 1 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 1 + 1X >= 1 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {head# mark X -> head# X} SCC (1): Strict: {head# mark X -> head# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [incr](x0) = x0 + 1, [active](x0) = x0 + 1, [s](x0) = 1, [head](x0) = x0 + 1, [tail](x0) = x0 + 1, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = x0 + 1, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 1, [head#](x0) = x0 Strict: head# mark X -> head# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper tail X -> tail proper X 2 + 1X >= 2 + 1X proper head X -> head proper X 2 + 1X >= 2 + 1X proper s X -> s proper X 2 + 0X >= 1 + 0X proper pairs() -> ok pairs() 2 >= 2 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 tail ok X -> ok tail X 2 + 1X >= 2 + 1X tail mark X -> mark tail X 2 + 1X >= 2 + 1X head ok X -> ok head X 2 + 1X >= 2 + 1X head mark X -> mark head X 2 + 1X >= 2 + 1X s ok X -> ok s X 1 + 0X >= 2 + 0X s mark X -> mark s X 1 + 0X >= 2 + 0X active tail cons(X, XS) -> mark XS 3 + 1X + 0XS >= 1 + 1XS active tail X -> tail active X 2 + 1X >= 2 + 1X active head cons(X, XS) -> mark X 3 + 1X + 0XS >= 1 + 1X active head X -> head active X 2 + 1X >= 2 + 1X active s X -> s active X 2 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 2 >= 3 active odds() -> mark incr pairs() 2 >= 3 active nats() -> mark cons(0(), incr nats()) 2 >= 3 active incr cons(X, XS) -> mark cons(s X, incr XS) 3 + 1X + 0XS >= 3 + 0X + 0XS active incr X -> incr active X 2 + 1X >= 2 + 1X active cons(X1, X2) -> cons(active X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 2 + 1X >= 2 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 Qed SCC (2): Strict: {s# mark X -> s# X, s# ok X -> s# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [mark](x0) = x0, [incr](x0) = x0 + 1, [active](x0) = 0, [s](x0) = 0, [head](x0) = 0, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = 0, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 0, [s#](x0) = x0 Strict: s# ok X -> s# X 1 + 1X >= 0 + 1X s# mark X -> s# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 1 + 0X >= 0 + 0X proper head X -> head proper X 1 + 0X >= 0 + 0X proper s X -> s proper X 1 + 0X >= 0 + 0X proper pairs() -> ok pairs() 1 >= 1 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 0 + 0X head ok X -> ok head X 0 + 0X >= 1 + 0X head mark X -> mark head X 0 + 0X >= 0 + 0X s ok X -> ok s X 0 + 0X >= 1 + 0X s mark X -> mark s X 0 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 1XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 1X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 0 + 0X >= 0 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 1 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 1 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 1 + 1X >= 1 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {s# mark X -> s# X} SCC (1): Strict: {s# mark X -> s# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [incr](x0) = x0 + 1, [active](x0) = x0 + 1, [s](x0) = 1, [head](x0) = x0 + 1, [tail](x0) = x0 + 1, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = x0 + 1, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 1, [s#](x0) = x0 Strict: s# mark X -> s# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper tail X -> tail proper X 2 + 1X >= 2 + 1X proper head X -> head proper X 2 + 1X >= 2 + 1X proper s X -> s proper X 2 + 0X >= 1 + 0X proper pairs() -> ok pairs() 2 >= 2 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 tail ok X -> ok tail X 2 + 1X >= 2 + 1X tail mark X -> mark tail X 2 + 1X >= 2 + 1X head ok X -> ok head X 2 + 1X >= 2 + 1X head mark X -> mark head X 2 + 1X >= 2 + 1X s ok X -> ok s X 1 + 0X >= 2 + 0X s mark X -> mark s X 1 + 0X >= 2 + 0X active tail cons(X, XS) -> mark XS 3 + 1X + 0XS >= 1 + 1XS active tail X -> tail active X 2 + 1X >= 2 + 1X active head cons(X, XS) -> mark X 3 + 1X + 0XS >= 1 + 1X active head X -> head active X 2 + 1X >= 2 + 1X active s X -> s active X 2 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 2 >= 3 active odds() -> mark incr pairs() 2 >= 3 active nats() -> mark cons(0(), incr nats()) 2 >= 3 active incr cons(X, XS) -> mark cons(s X, incr XS) 3 + 1X + 0XS >= 3 + 0X + 0XS active incr X -> incr active X 2 + 1X >= 2 + 1X active cons(X1, X2) -> cons(active X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 2 + 1X >= 2 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 Qed SCC (2): Strict: {incr# mark X -> incr# X, incr# ok X -> incr# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [mark](x0) = x0, [incr](x0) = x0 + 1, [active](x0) = 0, [s](x0) = 0, [head](x0) = 0, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = 0, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 0, [incr#](x0) = x0 Strict: incr# ok X -> incr# X 1 + 1X >= 0 + 1X incr# mark X -> incr# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 1 + 0X >= 0 + 0X proper head X -> head proper X 1 + 0X >= 0 + 0X proper s X -> s proper X 1 + 0X >= 0 + 0X proper pairs() -> ok pairs() 1 >= 1 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 0 + 0X head ok X -> ok head X 0 + 0X >= 1 + 0X head mark X -> mark head X 0 + 0X >= 0 + 0X s ok X -> ok s X 0 + 0X >= 1 + 0X s mark X -> mark s X 0 + 0X >= 0 + 0X active tail cons(X, XS) -> mark XS 0 + 0X + 0XS >= 0 + 1XS active tail X -> tail active X 0 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 0 + 0X + 0XS >= 0 + 1X active head X -> head active X 0 + 0X >= 0 + 0X active s X -> s active X 0 + 0X >= 0 + 0X active pairs() -> mark cons(0(), incr odds()) 0 >= 0 active odds() -> mark incr pairs() 0 >= 1 active nats() -> mark cons(0(), incr nats()) 0 >= 0 active incr cons(X, XS) -> mark cons(s X, incr XS) 0 + 0X + 0XS >= 0 + 0X + 0XS active incr X -> incr active X 0 + 0X >= 1 + 0X active cons(X1, X2) -> cons(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 1 + 1X >= 1 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {incr# mark X -> incr# X} SCC (1): Strict: {incr# mark X -> incr# X} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [incr](x0) = x0 + 1, [active](x0) = x0 + 1, [s](x0) = 1, [head](x0) = x0 + 1, [tail](x0) = x0 + 1, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = x0 + 1, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 1, [incr#](x0) = x0 Strict: incr# mark X -> incr# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper tail X -> tail proper X 2 + 1X >= 2 + 1X proper head X -> head proper X 2 + 1X >= 2 + 1X proper s X -> s proper X 2 + 0X >= 1 + 0X proper pairs() -> ok pairs() 2 >= 2 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 tail ok X -> ok tail X 2 + 1X >= 2 + 1X tail mark X -> mark tail X 2 + 1X >= 2 + 1X head ok X -> ok head X 2 + 1X >= 2 + 1X head mark X -> mark head X 2 + 1X >= 2 + 1X s ok X -> ok s X 1 + 0X >= 2 + 0X s mark X -> mark s X 1 + 0X >= 2 + 0X active tail cons(X, XS) -> mark XS 3 + 1X + 0XS >= 1 + 1XS active tail X -> tail active X 2 + 1X >= 2 + 1X active head cons(X, XS) -> mark X 3 + 1X + 0XS >= 1 + 1X active head X -> head active X 2 + 1X >= 2 + 1X active s X -> s active X 2 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 2 >= 3 active odds() -> mark incr pairs() 2 >= 3 active nats() -> mark cons(0(), incr nats()) 2 >= 3 active incr cons(X, XS) -> mark cons(s X, incr XS) 3 + 1X + 0XS >= 3 + 0X + 0XS active incr X -> incr active X 2 + 1X >= 2 + 1X active cons(X1, X2) -> cons(active X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 2 + 1X >= 2 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 Qed SCC (2): Strict: { cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2)} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [incr](x0) = x0 + 1, [active](x0) = x0 + 1, [s](x0) = 1, [head](x0) = x0 + 1, [tail](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = 0, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 1, [cons#](x0, x1) = x0 Strict: cons#(ok X1, ok X2) -> cons#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 cons#(mark X1, X2) -> cons#(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper tail X -> tail proper X 1 + 0X >= 0 + 0X proper head X -> head proper X 2 + 1X >= 2 + 1X proper s X -> s proper X 2 + 0X >= 1 + 0X proper pairs() -> ok pairs() 2 >= 2 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 tail ok X -> ok tail X 0 + 0X >= 1 + 0X tail mark X -> mark tail X 0 + 0X >= 1 + 0X head ok X -> ok head X 2 + 1X >= 2 + 1X head mark X -> mark head X 2 + 1X >= 2 + 1X s ok X -> ok s X 1 + 0X >= 2 + 0X s mark X -> mark s X 1 + 0X >= 2 + 0X active tail cons(X, XS) -> mark XS 1 + 0X + 0XS >= 1 + 1XS active tail X -> tail active X 1 + 0X >= 0 + 0X active head cons(X, XS) -> mark X 3 + 1X + 0XS >= 1 + 1X active head X -> head active X 2 + 1X >= 2 + 1X active s X -> s active X 2 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 2 >= 3 active odds() -> mark incr pairs() 2 >= 3 active nats() -> mark cons(0(), incr nats()) 2 >= 3 active incr cons(X, XS) -> mark cons(s X, incr XS) 3 + 1X + 0XS >= 3 + 0X + 0XS active incr X -> incr active X 2 + 1X >= 2 + 1X active cons(X1, X2) -> cons(active X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 2 + 1X >= 2 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 SCCS (1): Scc: {cons#(mark X1, X2) -> cons#(X1, X2)} SCC (1): Strict: {cons#(mark X1, X2) -> cons#(X1, X2)} Weak: { cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), incr mark X -> mark incr X, incr ok X -> ok incr X, active cons(X1, X2) -> cons(active X1, X2), active incr X -> incr active X, active incr cons(X, XS) -> mark cons(s X, incr XS), active nats() -> mark cons(0(), incr nats()), active odds() -> mark incr pairs(), active pairs() -> mark cons(0(), incr odds()), active s X -> s active X, active head X -> head active X, active head cons(X, XS) -> mark X, active tail X -> tail active X, active tail cons(X, XS) -> mark XS, s mark X -> mark s X, s ok X -> ok s X, head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, proper cons(X1, X2) -> cons(proper X1, proper X2), proper 0() -> ok 0(), proper incr X -> incr proper X, proper nats() -> ok nats(), proper odds() -> ok odds(), proper pairs() -> ok pairs(), proper s X -> s proper X, proper head X -> head proper X, proper tail X -> tail proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [incr](x0) = x0 + 1, [active](x0) = x0 + 1, [s](x0) = 1, [head](x0) = x0 + 1, [tail](x0) = x0 + 1, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [top](x0) = x0 + 1, [0] = 1, [nats] = 1, [odds] = 1, [pairs] = 1, [cons#](x0, x1) = x0 Strict: cons#(mark X1, X2) -> cons#(X1, X2) 1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper tail X -> tail proper X 2 + 1X >= 2 + 1X proper head X -> head proper X 2 + 1X >= 2 + 1X proper s X -> s proper X 2 + 0X >= 1 + 0X proper pairs() -> ok pairs() 2 >= 2 proper odds() -> ok odds() 2 >= 2 proper nats() -> ok nats() 2 >= 2 proper incr X -> incr proper X 2 + 1X >= 2 + 1X proper 0() -> ok 0() 2 >= 2 proper cons(X1, X2) -> cons(proper X1, proper X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 tail ok X -> ok tail X 2 + 1X >= 2 + 1X tail mark X -> mark tail X 2 + 1X >= 2 + 1X head ok X -> ok head X 2 + 1X >= 2 + 1X head mark X -> mark head X 2 + 1X >= 2 + 1X s ok X -> ok s X 1 + 0X >= 2 + 0X s mark X -> mark s X 1 + 0X >= 2 + 0X active tail cons(X, XS) -> mark XS 3 + 1X + 0XS >= 1 + 1XS active tail X -> tail active X 2 + 1X >= 2 + 1X active head cons(X, XS) -> mark X 3 + 1X + 0XS >= 1 + 1X active head X -> head active X 2 + 1X >= 2 + 1X active s X -> s active X 2 + 0X >= 1 + 0X active pairs() -> mark cons(0(), incr odds()) 2 >= 3 active odds() -> mark incr pairs() 2 >= 3 active nats() -> mark cons(0(), incr nats()) 2 >= 3 active incr cons(X, XS) -> mark cons(s X, incr XS) 3 + 1X + 0XS >= 3 + 0X + 0XS active incr X -> incr active X 2 + 1X >= 2 + 1X active cons(X1, X2) -> cons(active X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 incr ok X -> ok incr X 2 + 1X >= 2 + 1X incr mark X -> mark incr X 2 + 1X >= 2 + 1X cons(ok X1, ok X2) -> ok cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 cons(mark X1, X2) -> mark cons(X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 Qed