MAYBE Time: 0.074571 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# 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.871282 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} Open 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} Open 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} Open 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} Open 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} Open 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} Open 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} Open 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} Open