MAYBE Time: 0.648487 TRS: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark incr X -> active incr mark X, mark nats() -> active nats(), mark odds() -> active odds(), mark pairs() -> active pairs(), mark s X -> active s mark X, mark head X -> active head mark X, mark tail X -> active tail mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), incr mark X -> incr X, incr active X -> incr 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 head cons(X, XS) -> mark X, active tail cons(X, XS) -> mark XS, s mark X -> s X, s active X -> s X, head mark X -> head X, head active X -> head X, tail mark X -> tail X, tail active X -> tail X} DP: DP: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2), mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# 0() -> active# 0(), mark# incr X -> mark# X, mark# incr X -> incr# mark X, mark# incr X -> active# incr mark X, mark# nats() -> active# nats(), mark# odds() -> active# odds(), mark# pairs() -> active# pairs(), mark# s X -> mark# X, mark# s X -> active# s mark X, mark# s X -> s# mark X, mark# head X -> mark# X, mark# head X -> active# head mark X, mark# head X -> head# mark X, mark# tail X -> mark# X, mark# tail X -> active# tail mark X, mark# tail X -> tail# mark X, cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2), incr# mark X -> incr# X, incr# active X -> incr# X, active# incr cons(X, XS) -> mark# cons(s X, incr XS), 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() -> mark# cons(0(), incr nats()), active# nats() -> cons#(0(), incr nats()), active# nats() -> incr# nats(), active# odds() -> mark# incr pairs(), active# odds() -> incr# pairs(), active# pairs() -> mark# cons(0(), incr odds()), active# pairs() -> cons#(0(), incr odds()), active# pairs() -> incr# odds(), active# head cons(X, XS) -> mark# X, active# tail cons(X, XS) -> mark# XS, s# mark X -> s# X, s# active X -> s# X, head# mark X -> head# X, head# active X -> head# X, tail# mark X -> tail# X, tail# active X -> tail# X} TRS: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark incr X -> active incr mark X, mark nats() -> active nats(), mark odds() -> active odds(), mark pairs() -> active pairs(), mark s X -> active s mark X, mark head X -> active head mark X, mark tail X -> active tail mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), incr mark X -> incr X, incr active X -> incr 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 head cons(X, XS) -> mark X, active tail cons(X, XS) -> mark XS, s mark X -> s X, s active X -> s X, head mark X -> head X, head active X -> head X, tail mark X -> tail X, tail active X -> tail X} UR: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark incr X -> active incr mark X, mark nats() -> active nats(), mark odds() -> active odds(), mark pairs() -> active pairs(), mark s X -> active s mark X, mark head X -> active head mark X, mark tail X -> active tail mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), incr mark X -> incr X, incr active X -> incr 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 head cons(X, XS) -> mark X, active tail cons(X, XS) -> mark XS, s mark X -> s X, s active X -> s X, head mark X -> head X, head active X -> head X, tail mark X -> tail X, tail active X -> tail X} EDG: { (mark# s X -> active# s mark X, active# tail cons(X, XS) -> mark# XS) (mark# s X -> active# s mark X, active# head cons(X, XS) -> mark# X) (mark# s X -> active# s mark X, active# pairs() -> incr# odds()) (mark# s X -> active# s mark X, active# pairs() -> cons#(0(), incr odds())) (mark# s X -> active# s mark X, active# pairs() -> mark# cons(0(), incr odds())) (mark# s X -> active# s mark X, active# odds() -> incr# pairs()) (mark# s X -> active# s mark X, active# odds() -> mark# incr pairs()) (mark# s X -> active# s mark X, active# nats() -> incr# nats()) (mark# s X -> active# s mark X, active# nats() -> cons#(0(), incr nats())) (mark# s X -> active# s mark X, active# nats() -> mark# cons(0(), incr nats())) (mark# s X -> active# s mark X, active# incr cons(X, XS) -> s# X) (mark# s X -> active# s mark X, active# incr cons(X, XS) -> incr# XS) (mark# s X -> active# s mark X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# s X -> active# s mark X, active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# tail X -> active# tail mark X, active# tail cons(X, XS) -> mark# XS) (mark# tail X -> active# tail mark X, active# head cons(X, XS) -> mark# X) (mark# tail X -> active# tail mark X, active# pairs() -> incr# odds()) (mark# tail X -> active# tail mark X, active# pairs() -> cons#(0(), incr odds())) (mark# tail X -> active# tail mark X, active# pairs() -> mark# cons(0(), incr odds())) (mark# tail X -> active# tail mark X, active# odds() -> incr# pairs()) (mark# tail X -> active# tail mark X, active# odds() -> mark# incr pairs()) (mark# tail X -> active# tail mark X, active# nats() -> incr# nats()) (mark# tail X -> active# tail mark X, active# nats() -> cons#(0(), incr nats())) (mark# tail X -> active# tail mark X, active# nats() -> mark# cons(0(), incr nats())) (mark# tail X -> active# tail mark X, active# incr cons(X, XS) -> s# X) (mark# tail X -> active# tail mark X, active# incr cons(X, XS) -> incr# XS) (mark# tail X -> active# tail mark X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# tail X -> active# tail mark X, active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# incr X -> mark# X, mark# tail X -> tail# mark X) (mark# incr X -> mark# X, mark# tail X -> active# tail mark X) (mark# incr X -> mark# X, mark# tail X -> mark# X) (mark# incr X -> mark# X, mark# head X -> head# mark X) (mark# incr X -> mark# X, mark# head X -> active# head mark X) (mark# incr X -> mark# X, mark# head X -> mark# X) (mark# incr X -> mark# X, mark# s X -> s# mark X) (mark# incr X -> mark# X, mark# s X -> active# s mark X) (mark# incr X -> mark# X, mark# s X -> mark# X) (mark# incr X -> mark# X, mark# pairs() -> active# pairs()) (mark# incr X -> mark# X, mark# odds() -> active# odds()) (mark# incr X -> mark# X, mark# nats() -> active# nats()) (mark# incr X -> mark# X, mark# incr X -> active# incr mark X) (mark# incr X -> mark# X, mark# incr X -> incr# mark X) (mark# incr X -> mark# X, mark# incr X -> mark# X) (mark# incr X -> mark# X, mark# 0() -> active# 0()) (mark# incr X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# incr X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# head X -> mark# X, mark# tail X -> tail# mark X) (mark# head X -> mark# X, mark# tail X -> active# tail mark X) (mark# head X -> mark# X, mark# tail X -> mark# X) (mark# head X -> mark# X, mark# head X -> head# mark X) (mark# head X -> mark# X, mark# head X -> active# head mark X) (mark# head X -> mark# X, mark# head X -> mark# X) (mark# head X -> mark# X, mark# s X -> s# mark X) (mark# head X -> mark# X, mark# s X -> active# s mark X) (mark# head X -> mark# X, mark# s X -> mark# X) (mark# head X -> mark# X, mark# pairs() -> active# pairs()) (mark# head X -> mark# X, mark# odds() -> active# odds()) (mark# head X -> mark# X, mark# nats() -> active# nats()) (mark# head X -> mark# X, mark# incr X -> active# incr mark X) (mark# head X -> mark# X, mark# incr X -> incr# mark X) (mark# head X -> mark# X, mark# incr X -> mark# X) (mark# head X -> mark# X, mark# 0() -> active# 0()) (mark# head X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# head X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1) (incr# mark X -> incr# X, incr# active X -> incr# X) (incr# mark X -> incr# X, incr# mark X -> incr# X) (active# incr cons(X, XS) -> s# X, s# active X -> s# X) (active# incr cons(X, XS) -> s# X, s# mark X -> s# X) (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (head# mark X -> head# X, head# active X -> head# X) (head# mark X -> head# X, head# mark X -> head# X) (tail# mark X -> tail# X, tail# active X -> tail# X) (tail# mark X -> tail# X, tail# mark X -> tail# X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# tail X -> tail# mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# tail X -> active# tail mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# tail X -> mark# X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# head X -> head# mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# head X -> active# head mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# head X -> mark# X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# s X -> s# mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# s X -> active# s mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# s X -> mark# X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# pairs() -> active# pairs()) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# odds() -> active# odds()) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# nats() -> active# nats()) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# incr X -> active# incr mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# incr X -> incr# mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# incr X -> mark# X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# 0() -> active# 0()) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> mark# X1) (active# pairs() -> mark# cons(0(), incr odds()), mark# tail X -> tail# mark X) (active# pairs() -> mark# cons(0(), incr odds()), mark# tail X -> active# tail mark X) (active# pairs() -> mark# cons(0(), incr odds()), mark# tail X -> mark# X) (active# pairs() -> mark# cons(0(), incr odds()), mark# head X -> head# mark X) (active# pairs() -> mark# cons(0(), incr odds()), mark# head X -> active# head mark X) (active# pairs() -> mark# cons(0(), incr odds()), mark# head X -> mark# X) (active# pairs() -> mark# cons(0(), incr odds()), mark# s X -> s# mark X) (active# pairs() -> mark# cons(0(), incr odds()), mark# s X -> active# s mark X) (active# pairs() -> mark# cons(0(), incr odds()), mark# s X -> mark# X) (active# pairs() -> mark# cons(0(), incr odds()), mark# pairs() -> active# pairs()) (active# pairs() -> mark# cons(0(), incr odds()), mark# odds() -> active# odds()) (active# pairs() -> mark# cons(0(), incr odds()), mark# nats() -> active# nats()) (active# pairs() -> mark# cons(0(), incr odds()), mark# incr X -> active# incr mark X) (active# pairs() -> mark# cons(0(), incr odds()), mark# incr X -> incr# mark X) (active# pairs() -> mark# cons(0(), incr odds()), mark# incr X -> mark# X) (active# pairs() -> mark# cons(0(), incr odds()), mark# 0() -> active# 0()) (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> mark# X1) (active# tail cons(X, XS) -> mark# XS, mark# tail X -> tail# mark X) (active# tail cons(X, XS) -> mark# XS, mark# tail X -> active# tail mark X) (active# tail cons(X, XS) -> mark# XS, mark# tail X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# head X -> head# mark X) (active# tail cons(X, XS) -> mark# XS, mark# head X -> active# head mark X) (active# tail cons(X, XS) -> mark# XS, mark# head X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# s X -> s# mark X) (active# tail cons(X, XS) -> mark# XS, mark# s X -> active# s mark X) (active# tail cons(X, XS) -> mark# XS, mark# s X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# pairs() -> active# pairs()) (active# tail cons(X, XS) -> mark# XS, mark# odds() -> active# odds()) (active# tail cons(X, XS) -> mark# XS, mark# nats() -> active# nats()) (active# tail cons(X, XS) -> mark# XS, mark# incr X -> active# incr mark X) (active# tail cons(X, XS) -> mark# XS, mark# incr X -> incr# mark X) (active# tail cons(X, XS) -> mark# XS, mark# incr X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# 0() -> active# 0()) (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# tail X -> tail# mark X) (mark# cons(X1, X2) -> mark# X1, mark# tail X -> active# tail mark X) (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# head X -> head# mark X) (mark# cons(X1, X2) -> mark# X1, mark# head X -> active# head mark X) (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# pairs() -> active# pairs()) (mark# cons(X1, X2) -> mark# X1, mark# odds() -> active# odds()) (mark# cons(X1, X2) -> mark# X1, mark# nats() -> active# nats()) (mark# cons(X1, X2) -> mark# X1, mark# incr X -> active# incr mark X) (mark# cons(X1, X2) -> mark# X1, mark# incr X -> incr# mark X) (mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# s X -> s# mark X, s# active X -> s# X) (mark# s X -> s# mark X, s# mark X -> s# X) (mark# tail X -> tail# mark X, tail# active X -> tail# X) (mark# tail X -> tail# mark X, tail# mark X -> tail# X) (active# nats() -> cons#(0(), incr nats()), cons#(active X1, X2) -> cons#(X1, X2)) (active# nats() -> cons#(0(), incr nats()), cons#(mark X1, X2) -> cons#(X1, X2)) (active# nats() -> cons#(0(), incr nats()), cons#(X1, active X2) -> cons#(X1, X2)) (active# nats() -> cons#(0(), incr nats()), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# 0() -> active# 0(), active# tail cons(X, XS) -> mark# XS) (mark# 0() -> active# 0(), active# head cons(X, XS) -> mark# X) (mark# 0() -> active# 0(), active# pairs() -> incr# odds()) (mark# 0() -> active# 0(), active# pairs() -> cons#(0(), incr odds())) (mark# 0() -> active# 0(), active# pairs() -> mark# cons(0(), incr odds())) (mark# 0() -> active# 0(), active# odds() -> incr# pairs()) (mark# 0() -> active# 0(), active# odds() -> mark# incr pairs()) (mark# 0() -> active# 0(), active# nats() -> incr# nats()) (mark# 0() -> active# 0(), active# nats() -> cons#(0(), incr nats())) (mark# 0() -> active# 0(), active# nats() -> mark# cons(0(), incr nats())) (mark# 0() -> active# 0(), active# incr cons(X, XS) -> s# X) (mark# 0() -> active# 0(), active# incr cons(X, XS) -> incr# XS) (mark# 0() -> active# 0(), active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# 0() -> active# 0(), active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# odds() -> active# odds(), active# tail cons(X, XS) -> mark# XS) (mark# odds() -> active# odds(), active# head cons(X, XS) -> mark# X) (mark# odds() -> active# odds(), active# pairs() -> incr# odds()) (mark# odds() -> active# odds(), active# pairs() -> cons#(0(), incr odds())) (mark# odds() -> active# odds(), active# pairs() -> mark# cons(0(), incr odds())) (mark# odds() -> active# odds(), active# odds() -> incr# pairs()) (mark# odds() -> active# odds(), active# odds() -> mark# incr pairs()) (mark# odds() -> active# odds(), active# nats() -> incr# nats()) (mark# odds() -> active# odds(), active# nats() -> cons#(0(), incr nats())) (mark# odds() -> active# odds(), active# nats() -> mark# cons(0(), incr nats())) (mark# odds() -> active# odds(), active# incr cons(X, XS) -> s# X) (mark# odds() -> active# odds(), active# incr cons(X, XS) -> incr# XS) (mark# odds() -> active# odds(), active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# odds() -> active# odds(), active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (active# nats() -> incr# nats(), incr# active X -> incr# X) (active# nats() -> incr# nats(), incr# mark X -> incr# X) (active# pairs() -> incr# odds(), incr# active X -> incr# X) (active# pairs() -> incr# odds(), incr# mark X -> incr# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, XS) -> incr# XS) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, XS) -> s# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# nats() -> mark# cons(0(), incr nats())) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# nats() -> cons#(0(), incr nats())) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# nats() -> incr# nats()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# odds() -> mark# incr pairs()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# odds() -> incr# pairs()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# pairs() -> mark# cons(0(), incr odds())) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# pairs() -> cons#(0(), incr odds())) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# pairs() -> incr# odds()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# head cons(X, XS) -> mark# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# tail cons(X, XS) -> mark# XS) (active# odds() -> incr# pairs(), incr# mark X -> incr# X) (active# odds() -> incr# pairs(), incr# active X -> incr# X) (mark# pairs() -> active# pairs(), active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# pairs() -> active# pairs(), active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# pairs() -> active# pairs(), active# incr cons(X, XS) -> incr# XS) (mark# pairs() -> active# pairs(), active# incr cons(X, XS) -> s# X) (mark# pairs() -> active# pairs(), active# nats() -> mark# cons(0(), incr nats())) (mark# pairs() -> active# pairs(), active# nats() -> cons#(0(), incr nats())) (mark# pairs() -> active# pairs(), active# nats() -> incr# nats()) (mark# pairs() -> active# pairs(), active# odds() -> mark# incr pairs()) (mark# pairs() -> active# pairs(), active# odds() -> incr# pairs()) (mark# pairs() -> active# pairs(), active# pairs() -> mark# cons(0(), incr odds())) (mark# pairs() -> active# pairs(), active# pairs() -> cons#(0(), incr odds())) (mark# pairs() -> active# pairs(), active# pairs() -> incr# odds()) (mark# pairs() -> active# pairs(), active# head cons(X, XS) -> mark# X) (mark# pairs() -> active# pairs(), active# tail cons(X, XS) -> mark# XS) (mark# nats() -> active# nats(), active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# nats() -> active# nats(), active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# nats() -> active# nats(), active# incr cons(X, XS) -> incr# XS) (mark# nats() -> active# nats(), active# incr cons(X, XS) -> s# X) (mark# nats() -> active# nats(), active# nats() -> mark# cons(0(), incr nats())) (mark# nats() -> active# nats(), active# nats() -> cons#(0(), incr nats())) (mark# nats() -> active# nats(), active# nats() -> incr# nats()) (mark# nats() -> active# nats(), active# odds() -> mark# incr pairs()) (mark# nats() -> active# nats(), active# odds() -> incr# pairs()) (mark# nats() -> active# nats(), active# pairs() -> mark# cons(0(), incr odds())) (mark# nats() -> active# nats(), active# pairs() -> cons#(0(), incr odds())) (mark# nats() -> active# nats(), active# pairs() -> incr# odds()) (mark# nats() -> active# nats(), active# head cons(X, XS) -> mark# X) (mark# nats() -> active# nats(), active# tail cons(X, XS) -> mark# XS) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (active# pairs() -> cons#(0(), incr odds()), cons#(X1, mark X2) -> cons#(X1, X2)) (active# pairs() -> cons#(0(), incr odds()), cons#(X1, active X2) -> cons#(X1, X2)) (active# pairs() -> cons#(0(), incr odds()), cons#(mark X1, X2) -> cons#(X1, X2)) (active# pairs() -> cons#(0(), incr odds()), cons#(active X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (mark# head X -> head# mark X, head# mark X -> head# X) (mark# head X -> head# mark X, head# active X -> head# X) (mark# incr X -> incr# mark X, incr# mark X -> incr# X) (mark# incr X -> incr# mark X, incr# active X -> incr# X) (active# incr cons(X, XS) -> cons#(s X, incr XS), cons#(X1, mark X2) -> cons#(X1, X2)) (active# incr cons(X, XS) -> cons#(s X, incr XS), cons#(X1, active X2) -> cons#(X1, X2)) (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#(active X1, X2) -> cons#(X1, X2)) (active# incr cons(X, XS) -> incr# XS, incr# mark X -> incr# X) (active# incr cons(X, XS) -> incr# XS, incr# active X -> incr# X) (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> mark# X1) (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# nats() -> mark# cons(0(), incr nats()), mark# 0() -> active# 0()) (active# nats() -> mark# cons(0(), incr nats()), mark# incr X -> mark# X) (active# nats() -> mark# cons(0(), incr nats()), mark# incr X -> incr# mark X) (active# nats() -> mark# cons(0(), incr nats()), mark# incr X -> active# incr mark X) (active# nats() -> mark# cons(0(), incr nats()), mark# nats() -> active# nats()) (active# nats() -> mark# cons(0(), incr nats()), mark# odds() -> active# odds()) (active# nats() -> mark# cons(0(), incr nats()), mark# pairs() -> active# pairs()) (active# nats() -> mark# cons(0(), incr nats()), mark# s X -> mark# X) (active# nats() -> mark# cons(0(), incr nats()), mark# s X -> active# s mark X) (active# nats() -> mark# cons(0(), incr nats()), mark# s X -> s# mark X) (active# nats() -> mark# cons(0(), incr nats()), mark# head X -> mark# X) (active# nats() -> mark# cons(0(), incr nats()), mark# head X -> active# head mark X) (active# nats() -> mark# cons(0(), incr nats()), mark# head X -> head# mark X) (active# nats() -> mark# cons(0(), incr nats()), mark# tail X -> mark# X) (active# nats() -> mark# cons(0(), incr nats()), mark# tail X -> active# tail mark X) (active# nats() -> mark# cons(0(), incr nats()), mark# tail X -> tail# mark X) (tail# active X -> tail# X, tail# mark X -> tail# X) (tail# active X -> tail# X, tail# active X -> tail# X) (head# active X -> head# X, head# mark X -> head# X) (head# active X -> head# X, head# active X -> head# X) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> mark# X1) (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# head cons(X, XS) -> mark# X, mark# 0() -> active# 0()) (active# head cons(X, XS) -> mark# X, mark# incr X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# incr X -> incr# mark X) (active# head cons(X, XS) -> mark# X, mark# incr X -> active# incr mark X) (active# head cons(X, XS) -> mark# X, mark# nats() -> active# nats()) (active# head cons(X, XS) -> mark# X, mark# odds() -> active# odds()) (active# head cons(X, XS) -> mark# X, mark# pairs() -> active# pairs()) (active# head cons(X, XS) -> mark# X, mark# s X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# s X -> active# s mark X) (active# head cons(X, XS) -> mark# X, mark# s X -> s# mark X) (active# head cons(X, XS) -> mark# X, mark# head X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# head X -> active# head mark X) (active# head cons(X, XS) -> mark# X, mark# head X -> head# mark X) (active# head cons(X, XS) -> mark# X, mark# tail X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# tail X -> active# tail mark X) (active# head cons(X, XS) -> mark# X, mark# tail X -> tail# mark X) (incr# active X -> incr# X, incr# mark X -> incr# X) (incr# active X -> incr# X, incr# active X -> incr# X) (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# tail X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# tail X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# tail X -> mark# X, mark# 0() -> active# 0()) (mark# tail X -> mark# X, mark# incr X -> mark# X) (mark# tail X -> mark# X, mark# incr X -> incr# mark X) (mark# tail X -> mark# X, mark# incr X -> active# incr mark X) (mark# tail X -> mark# X, mark# nats() -> active# nats()) (mark# tail X -> mark# X, mark# odds() -> active# odds()) (mark# tail X -> mark# X, mark# pairs() -> active# pairs()) (mark# tail X -> mark# X, mark# s X -> mark# X) (mark# tail X -> mark# X, mark# s X -> active# s mark X) (mark# tail X -> mark# X, mark# s X -> s# mark X) (mark# tail X -> mark# X, mark# head X -> mark# X) (mark# tail X -> mark# X, mark# head X -> active# head mark X) (mark# tail X -> mark# X, mark# head X -> head# mark X) (mark# tail X -> mark# X, mark# tail X -> mark# X) (mark# tail X -> mark# X, mark# tail X -> active# tail mark X) (mark# tail X -> mark# X, mark# tail X -> tail# mark X) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# s X -> mark# X, mark# 0() -> active# 0()) (mark# s X -> mark# X, mark# incr X -> mark# X) (mark# s X -> mark# X, mark# incr X -> incr# mark X) (mark# s X -> mark# X, mark# incr X -> active# incr mark X) (mark# s X -> mark# X, mark# nats() -> active# nats()) (mark# s X -> mark# X, mark# odds() -> active# odds()) (mark# s X -> mark# X, mark# pairs() -> active# pairs()) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# s X -> active# s mark X) (mark# s X -> mark# X, mark# s X -> s# mark X) (mark# s X -> mark# X, mark# head X -> mark# X) (mark# s X -> mark# X, mark# head X -> active# head mark X) (mark# s X -> mark# X, mark# head X -> head# mark X) (mark# s X -> mark# X, mark# tail X -> mark# X) (mark# s X -> mark# X, mark# tail X -> active# tail mark X) (mark# s X -> mark# X, mark# tail X -> tail# mark X) (active# odds() -> mark# incr pairs(), mark# cons(X1, X2) -> mark# X1) (active# odds() -> mark# incr pairs(), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# odds() -> mark# incr pairs(), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# odds() -> mark# incr pairs(), mark# 0() -> active# 0()) (active# odds() -> mark# incr pairs(), mark# incr X -> mark# X) (active# odds() -> mark# incr pairs(), mark# incr X -> incr# mark X) (active# odds() -> mark# incr pairs(), mark# incr X -> active# incr mark X) (active# odds() -> mark# incr pairs(), mark# nats() -> active# nats()) (active# odds() -> mark# incr pairs(), mark# odds() -> active# odds()) (active# odds() -> mark# incr pairs(), mark# pairs() -> active# pairs()) (active# odds() -> mark# incr pairs(), mark# s X -> mark# X) (active# odds() -> mark# incr pairs(), mark# s X -> active# s mark X) (active# odds() -> mark# incr pairs(), mark# s X -> s# mark X) (active# odds() -> mark# incr pairs(), mark# head X -> mark# X) (active# odds() -> mark# incr pairs(), mark# head X -> active# head mark X) (active# odds() -> mark# incr pairs(), mark# head X -> head# mark X) (active# odds() -> mark# incr pairs(), mark# tail X -> mark# X) (active# odds() -> mark# incr pairs(), mark# tail X -> active# tail mark X) (active# odds() -> mark# incr pairs(), mark# tail X -> tail# mark X) (mark# head X -> active# head mark X, active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# head X -> active# head mark X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# head X -> active# head mark X, active# incr cons(X, XS) -> incr# XS) (mark# head X -> active# head mark X, active# incr cons(X, XS) -> s# X) (mark# head X -> active# head mark X, active# nats() -> mark# cons(0(), incr nats())) (mark# head X -> active# head mark X, active# nats() -> cons#(0(), incr nats())) (mark# head X -> active# head mark X, active# nats() -> incr# nats()) (mark# head X -> active# head mark X, active# odds() -> mark# incr pairs()) (mark# head X -> active# head mark X, active# odds() -> incr# pairs()) (mark# head X -> active# head mark X, active# pairs() -> mark# cons(0(), incr odds())) (mark# head X -> active# head mark X, active# pairs() -> cons#(0(), incr odds())) (mark# head X -> active# head mark X, active# pairs() -> incr# odds()) (mark# head X -> active# head mark X, active# head cons(X, XS) -> mark# X) (mark# head X -> active# head mark X, active# tail cons(X, XS) -> mark# XS) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> incr# XS) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> s# X) (mark# incr X -> active# incr mark X, active# nats() -> mark# cons(0(), incr nats())) (mark# incr X -> active# incr mark X, active# nats() -> cons#(0(), incr nats())) (mark# incr X -> active# incr mark X, active# nats() -> incr# nats()) (mark# incr X -> active# incr mark X, active# odds() -> mark# incr pairs()) (mark# incr X -> active# incr mark X, active# odds() -> incr# pairs()) (mark# incr X -> active# incr mark X, active# pairs() -> mark# cons(0(), incr odds())) (mark# incr X -> active# incr mark X, active# pairs() -> cons#(0(), incr odds())) (mark# incr X -> active# incr mark X, active# pairs() -> incr# odds()) (mark# incr X -> active# incr mark X, active# head cons(X, XS) -> mark# X) (mark# incr X -> active# incr mark X, active# tail cons(X, XS) -> mark# XS) } EDG: { (mark# s X -> active# s mark X, active# tail cons(X, XS) -> mark# XS) (mark# s X -> active# s mark X, active# head cons(X, XS) -> mark# X) (mark# s X -> active# s mark X, active# incr cons(X, XS) -> s# X) (mark# s X -> active# s mark X, active# incr cons(X, XS) -> incr# XS) (mark# s X -> active# s mark X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# s X -> active# s mark X, active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# tail X -> active# tail mark X, active# tail cons(X, XS) -> mark# XS) (mark# tail X -> active# tail mark X, active# head cons(X, XS) -> mark# X) (mark# tail X -> active# tail mark X, active# incr cons(X, XS) -> s# X) (mark# tail X -> active# tail mark X, active# incr cons(X, XS) -> incr# XS) (mark# tail X -> active# tail mark X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# tail X -> active# tail mark X, active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# incr X -> mark# X, mark# tail X -> tail# mark X) (mark# incr X -> mark# X, mark# tail X -> active# tail mark X) (mark# incr X -> mark# X, mark# tail X -> mark# X) (mark# incr X -> mark# X, mark# head X -> head# mark X) (mark# incr X -> mark# X, mark# head X -> active# head mark X) (mark# incr X -> mark# X, mark# head X -> mark# X) (mark# incr X -> mark# X, mark# s X -> s# mark X) (mark# incr X -> mark# X, mark# s X -> active# s mark X) (mark# incr X -> mark# X, mark# s X -> mark# X) (mark# incr X -> mark# X, mark# pairs() -> active# pairs()) (mark# incr X -> mark# X, mark# odds() -> active# odds()) (mark# incr X -> mark# X, mark# nats() -> active# nats()) (mark# incr X -> mark# X, mark# incr X -> active# incr mark X) (mark# incr X -> mark# X, mark# incr X -> incr# mark X) (mark# incr X -> mark# X, mark# incr X -> mark# X) (mark# incr X -> mark# X, mark# 0() -> active# 0()) (mark# incr X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# incr X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# head X -> mark# X, mark# tail X -> tail# mark X) (mark# head X -> mark# X, mark# tail X -> active# tail mark X) (mark# head X -> mark# X, mark# tail X -> mark# X) (mark# head X -> mark# X, mark# head X -> head# mark X) (mark# head X -> mark# X, mark# head X -> active# head mark X) (mark# head X -> mark# X, mark# head X -> mark# X) (mark# head X -> mark# X, mark# s X -> s# mark X) (mark# head X -> mark# X, mark# s X -> active# s mark X) (mark# head X -> mark# X, mark# s X -> mark# X) (mark# head X -> mark# X, mark# pairs() -> active# pairs()) (mark# head X -> mark# X, mark# odds() -> active# odds()) (mark# head X -> mark# X, mark# nats() -> active# nats()) (mark# head X -> mark# X, mark# incr X -> active# incr mark X) (mark# head X -> mark# X, mark# incr X -> incr# mark X) (mark# head X -> mark# X, mark# incr X -> mark# X) (mark# head X -> mark# X, mark# 0() -> active# 0()) (mark# head X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# head X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1) (incr# mark X -> incr# X, incr# active X -> incr# X) (incr# mark X -> incr# X, incr# mark X -> incr# X) (active# incr cons(X, XS) -> s# X, s# active X -> s# X) (active# incr cons(X, XS) -> s# X, s# mark X -> s# X) (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (head# mark X -> head# X, head# active X -> head# X) (head# mark X -> head# X, head# mark X -> head# X) (tail# mark X -> tail# X, tail# active X -> tail# X) (tail# mark X -> tail# X, tail# mark X -> tail# X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# tail X -> tail# mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# tail X -> active# tail mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# tail X -> mark# X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# head X -> head# mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# head X -> active# head mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# head X -> mark# X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# s X -> s# mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# s X -> active# s mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# s X -> mark# X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# incr X -> active# incr mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# incr X -> incr# mark X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# incr X -> mark# X) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> mark# X1) (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> mark# X1) (active# tail cons(X, XS) -> mark# XS, mark# tail X -> tail# mark X) (active# tail cons(X, XS) -> mark# XS, mark# tail X -> active# tail mark X) (active# tail cons(X, XS) -> mark# XS, mark# tail X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# head X -> head# mark X) (active# tail cons(X, XS) -> mark# XS, mark# head X -> active# head mark X) (active# tail cons(X, XS) -> mark# XS, mark# head X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# s X -> s# mark X) (active# tail cons(X, XS) -> mark# XS, mark# s X -> active# s mark X) (active# tail cons(X, XS) -> mark# XS, mark# s X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# pairs() -> active# pairs()) (active# tail cons(X, XS) -> mark# XS, mark# odds() -> active# odds()) (active# tail cons(X, XS) -> mark# XS, mark# nats() -> active# nats()) (active# tail cons(X, XS) -> mark# XS, mark# incr X -> active# incr mark X) (active# tail cons(X, XS) -> mark# XS, mark# incr X -> incr# mark X) (active# tail cons(X, XS) -> mark# XS, mark# incr X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# 0() -> active# 0()) (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# tail X -> tail# mark X) (mark# cons(X1, X2) -> mark# X1, mark# tail X -> active# tail mark X) (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# head X -> head# mark X) (mark# cons(X1, X2) -> mark# X1, mark# head X -> active# head mark X) (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# pairs() -> active# pairs()) (mark# cons(X1, X2) -> mark# X1, mark# odds() -> active# odds()) (mark# cons(X1, X2) -> mark# X1, mark# nats() -> active# nats()) (mark# cons(X1, X2) -> mark# X1, mark# incr X -> active# incr mark X) (mark# cons(X1, X2) -> mark# X1, mark# incr X -> incr# mark X) (mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# s X -> s# mark X, s# active X -> s# X) (mark# s X -> s# mark X, s# mark X -> s# X) (mark# tail X -> tail# mark X, tail# active X -> tail# X) (mark# tail X -> tail# mark X, tail# mark X -> tail# X) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# odds() -> active# odds(), active# odds() -> incr# pairs()) (mark# odds() -> active# odds(), active# odds() -> mark# incr pairs()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, XS) -> incr# XS) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, XS) -> s# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# head cons(X, XS) -> mark# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# tail cons(X, XS) -> mark# XS) (mark# pairs() -> active# pairs(), active# pairs() -> mark# cons(0(), incr odds())) (mark# pairs() -> active# pairs(), active# pairs() -> cons#(0(), incr odds())) (mark# pairs() -> active# pairs(), active# pairs() -> incr# odds()) (mark# nats() -> active# nats(), active# nats() -> mark# cons(0(), incr nats())) (mark# nats() -> active# nats(), active# nats() -> cons#(0(), incr nats())) (mark# nats() -> active# nats(), active# nats() -> incr# nats()) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (mark# head X -> head# mark X, head# mark X -> head# X) (mark# head X -> head# mark X, head# active X -> head# X) (mark# incr X -> incr# mark X, incr# mark X -> incr# X) (mark# incr X -> incr# mark X, incr# active X -> incr# X) (active# incr cons(X, XS) -> cons#(s X, incr XS), cons#(X1, mark X2) -> cons#(X1, X2)) (active# incr cons(X, XS) -> cons#(s X, incr XS), cons#(X1, active X2) -> cons#(X1, X2)) (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#(active X1, X2) -> cons#(X1, X2)) (active# incr cons(X, XS) -> incr# XS, incr# mark X -> incr# X) (active# incr cons(X, XS) -> incr# XS, incr# active X -> incr# X) (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> mark# X1) (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (tail# active X -> tail# X, tail# mark X -> tail# X) (tail# active X -> tail# X, tail# active X -> tail# X) (head# active X -> head# X, head# mark X -> head# X) (head# active X -> head# X, head# active X -> head# X) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> mark# X1) (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# head cons(X, XS) -> mark# X, mark# 0() -> active# 0()) (active# head cons(X, XS) -> mark# X, mark# incr X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# incr X -> incr# mark X) (active# head cons(X, XS) -> mark# X, mark# incr X -> active# incr mark X) (active# head cons(X, XS) -> mark# X, mark# nats() -> active# nats()) (active# head cons(X, XS) -> mark# X, mark# odds() -> active# odds()) (active# head cons(X, XS) -> mark# X, mark# pairs() -> active# pairs()) (active# head cons(X, XS) -> mark# X, mark# s X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# s X -> active# s mark X) (active# head cons(X, XS) -> mark# X, mark# s X -> s# mark X) (active# head cons(X, XS) -> mark# X, mark# head X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# head X -> active# head mark X) (active# head cons(X, XS) -> mark# X, mark# head X -> head# mark X) (active# head cons(X, XS) -> mark# X, mark# tail X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# tail X -> active# tail mark X) (active# head cons(X, XS) -> mark# X, mark# tail X -> tail# mark X) (incr# active X -> incr# X, incr# mark X -> incr# X) (incr# active X -> incr# X, incr# active X -> incr# X) (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# tail X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# tail X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# tail X -> mark# X, mark# 0() -> active# 0()) (mark# tail X -> mark# X, mark# incr X -> mark# X) (mark# tail X -> mark# X, mark# incr X -> incr# mark X) (mark# tail X -> mark# X, mark# incr X -> active# incr mark X) (mark# tail X -> mark# X, mark# nats() -> active# nats()) (mark# tail X -> mark# X, mark# odds() -> active# odds()) (mark# tail X -> mark# X, mark# pairs() -> active# pairs()) (mark# tail X -> mark# X, mark# s X -> mark# X) (mark# tail X -> mark# X, mark# s X -> active# s mark X) (mark# tail X -> mark# X, mark# s X -> s# mark X) (mark# tail X -> mark# X, mark# head X -> mark# X) (mark# tail X -> mark# X, mark# head X -> active# head mark X) (mark# tail X -> mark# X, mark# head X -> head# mark X) (mark# tail X -> mark# X, mark# tail X -> mark# X) (mark# tail X -> mark# X, mark# tail X -> active# tail mark X) (mark# tail X -> mark# X, mark# tail X -> tail# mark X) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# s X -> mark# X, mark# 0() -> active# 0()) (mark# s X -> mark# X, mark# incr X -> mark# X) (mark# s X -> mark# X, mark# incr X -> incr# mark X) (mark# s X -> mark# X, mark# incr X -> active# incr mark X) (mark# s X -> mark# X, mark# nats() -> active# nats()) (mark# s X -> mark# X, mark# odds() -> active# odds()) (mark# s X -> mark# X, mark# pairs() -> active# pairs()) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# s X -> active# s mark X) (mark# s X -> mark# X, mark# s X -> s# mark X) (mark# s X -> mark# X, mark# head X -> mark# X) (mark# s X -> mark# X, mark# head X -> active# head mark X) (mark# s X -> mark# X, mark# head X -> head# mark X) (mark# s X -> mark# X, mark# tail X -> mark# X) (mark# s X -> mark# X, mark# tail X -> active# tail mark X) (mark# s X -> mark# X, mark# tail X -> tail# mark X) (active# odds() -> mark# incr pairs(), mark# incr X -> mark# X) (active# odds() -> mark# incr pairs(), mark# incr X -> incr# mark X) (active# odds() -> mark# incr pairs(), mark# incr X -> active# incr mark X) (mark# head X -> active# head mark X, active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# head X -> active# head mark X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# head X -> active# head mark X, active# incr cons(X, XS) -> incr# XS) (mark# head X -> active# head mark X, active# incr cons(X, XS) -> s# X) (mark# head X -> active# head mark X, active# head cons(X, XS) -> mark# X) (mark# head X -> active# head mark X, active# tail cons(X, XS) -> mark# XS) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> incr# XS) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> s# X) (mark# incr X -> active# incr mark X, active# head cons(X, XS) -> mark# X) (mark# incr X -> active# incr mark X, active# tail cons(X, XS) -> mark# XS) } EDG: { (mark# tail X -> active# tail mark X, active# tail cons(X, XS) -> mark# XS) (mark# incr X -> mark# X, mark# tail X -> tail# mark X) (mark# incr X -> mark# X, mark# tail X -> active# tail mark X) (mark# incr X -> mark# X, mark# tail X -> mark# X) (mark# incr X -> mark# X, mark# head X -> head# mark X) (mark# incr X -> mark# X, mark# head X -> active# head mark X) (mark# incr X -> mark# X, mark# head X -> mark# X) (mark# incr X -> mark# X, mark# s X -> s# mark X) (mark# incr X -> mark# X, mark# s X -> active# s mark X) (mark# incr X -> mark# X, mark# s X -> mark# X) (mark# incr X -> mark# X, mark# pairs() -> active# pairs()) (mark# incr X -> mark# X, mark# odds() -> active# odds()) (mark# incr X -> mark# X, mark# nats() -> active# nats()) (mark# incr X -> mark# X, mark# incr X -> active# incr mark X) (mark# incr X -> mark# X, mark# incr X -> incr# mark X) (mark# incr X -> mark# X, mark# incr X -> mark# X) (mark# incr X -> mark# X, mark# 0() -> active# 0()) (mark# incr X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# incr X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# head X -> mark# X, mark# tail X -> tail# mark X) (mark# head X -> mark# X, mark# tail X -> active# tail mark X) (mark# head X -> mark# X, mark# tail X -> mark# X) (mark# head X -> mark# X, mark# head X -> head# mark X) (mark# head X -> mark# X, mark# head X -> active# head mark X) (mark# head X -> mark# X, mark# head X -> mark# X) (mark# head X -> mark# X, mark# s X -> s# mark X) (mark# head X -> mark# X, mark# s X -> active# s mark X) (mark# head X -> mark# X, mark# s X -> mark# X) (mark# head X -> mark# X, mark# pairs() -> active# pairs()) (mark# head X -> mark# X, mark# odds() -> active# odds()) (mark# head X -> mark# X, mark# nats() -> active# nats()) (mark# head X -> mark# X, mark# incr X -> active# incr mark X) (mark# head X -> mark# X, mark# incr X -> incr# mark X) (mark# head X -> mark# X, mark# incr X -> mark# X) (mark# head X -> mark# X, mark# 0() -> active# 0()) (mark# head X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# head X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> mark# X1) (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> mark# X1) (active# tail cons(X, XS) -> mark# XS, mark# tail X -> tail# mark X) (active# tail cons(X, XS) -> mark# XS, mark# tail X -> active# tail mark X) (active# tail cons(X, XS) -> mark# XS, mark# tail X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# head X -> head# mark X) (active# tail cons(X, XS) -> mark# XS, mark# head X -> active# head mark X) (active# tail cons(X, XS) -> mark# XS, mark# head X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# s X -> s# mark X) (active# tail cons(X, XS) -> mark# XS, mark# s X -> active# s mark X) (active# tail cons(X, XS) -> mark# XS, mark# s X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# pairs() -> active# pairs()) (active# tail cons(X, XS) -> mark# XS, mark# odds() -> active# odds()) (active# tail cons(X, XS) -> mark# XS, mark# nats() -> active# nats()) (active# tail cons(X, XS) -> mark# XS, mark# incr X -> active# incr mark X) (active# tail cons(X, XS) -> mark# XS, mark# incr X -> incr# mark X) (active# tail cons(X, XS) -> mark# XS, mark# incr X -> mark# X) (active# tail cons(X, XS) -> mark# XS, mark# 0() -> active# 0()) (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# tail X -> tail# mark X) (mark# cons(X1, X2) -> mark# X1, mark# tail X -> active# tail mark X) (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# head X -> head# mark X) (mark# cons(X1, X2) -> mark# X1, mark# head X -> active# head mark X) (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# pairs() -> active# pairs()) (mark# cons(X1, X2) -> mark# X1, mark# odds() -> active# odds()) (mark# cons(X1, X2) -> mark# X1, mark# nats() -> active# nats()) (mark# cons(X1, X2) -> mark# X1, mark# incr X -> active# incr mark X) (mark# cons(X1, X2) -> mark# X1, mark# incr X -> incr# mark X) (mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# s X -> s# mark X, s# active X -> s# X) (mark# s X -> s# mark X, s# mark X -> s# X) (mark# tail X -> tail# mark X, tail# active X -> tail# X) (mark# tail X -> tail# mark X, tail# mark X -> tail# X) (mark# odds() -> active# odds(), active# odds() -> incr# pairs()) (mark# odds() -> active# odds(), active# odds() -> mark# incr pairs()) (mark# pairs() -> active# pairs(), active# pairs() -> mark# cons(0(), incr odds())) (mark# pairs() -> active# pairs(), active# pairs() -> cons#(0(), incr odds())) (mark# pairs() -> active# pairs(), active# pairs() -> incr# odds()) (mark# nats() -> active# nats(), active# nats() -> mark# cons(0(), incr nats())) (mark# nats() -> active# nats(), active# nats() -> cons#(0(), incr nats())) (mark# nats() -> active# nats(), active# nats() -> incr# nats()) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (mark# head X -> head# mark X, head# mark X -> head# X) (mark# head X -> head# mark X, head# active X -> head# X) (mark# incr X -> incr# mark X, incr# mark X -> incr# X) (mark# incr X -> incr# mark X, incr# active X -> incr# X) (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> mark# X1) (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> mark# X1) (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# head cons(X, XS) -> mark# X, mark# 0() -> active# 0()) (active# head cons(X, XS) -> mark# X, mark# incr X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# incr X -> incr# mark X) (active# head cons(X, XS) -> mark# X, mark# incr X -> active# incr mark X) (active# head cons(X, XS) -> mark# X, mark# nats() -> active# nats()) (active# head cons(X, XS) -> mark# X, mark# odds() -> active# odds()) (active# head cons(X, XS) -> mark# X, mark# pairs() -> active# pairs()) (active# head cons(X, XS) -> mark# X, mark# s X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# s X -> active# s mark X) (active# head cons(X, XS) -> mark# X, mark# s X -> s# mark X) (active# head cons(X, XS) -> mark# X, mark# head X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# head X -> active# head mark X) (active# head cons(X, XS) -> mark# X, mark# head X -> head# mark X) (active# head cons(X, XS) -> mark# X, mark# tail X -> mark# X) (active# head cons(X, XS) -> mark# X, mark# tail X -> active# tail mark X) (active# head cons(X, XS) -> mark# X, mark# tail X -> tail# mark X) (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# tail X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# tail X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# tail X -> mark# X, mark# 0() -> active# 0()) (mark# tail X -> mark# X, mark# incr X -> mark# X) (mark# tail X -> mark# X, mark# incr X -> incr# mark X) (mark# tail X -> mark# X, mark# incr X -> active# incr mark X) (mark# tail X -> mark# X, mark# nats() -> active# nats()) (mark# tail X -> mark# X, mark# odds() -> active# odds()) (mark# tail X -> mark# X, mark# pairs() -> active# pairs()) (mark# tail X -> mark# X, mark# s X -> mark# X) (mark# tail X -> mark# X, mark# s X -> active# s mark X) (mark# tail X -> mark# X, mark# s X -> s# mark X) (mark# tail X -> mark# X, mark# head X -> mark# X) (mark# tail X -> mark# X, mark# head X -> active# head mark X) (mark# tail X -> mark# X, mark# head X -> head# mark X) (mark# tail X -> mark# X, mark# tail X -> mark# X) (mark# tail X -> mark# X, mark# tail X -> active# tail mark X) (mark# tail X -> mark# X, mark# tail X -> tail# mark X) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# s X -> mark# X, mark# 0() -> active# 0()) (mark# s X -> mark# X, mark# incr X -> mark# X) (mark# s X -> mark# X, mark# incr X -> incr# mark X) (mark# s X -> mark# X, mark# incr X -> active# incr mark X) (mark# s X -> mark# X, mark# nats() -> active# nats()) (mark# s X -> mark# X, mark# odds() -> active# odds()) (mark# s X -> mark# X, mark# pairs() -> active# pairs()) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# s X -> active# s mark X) (mark# s X -> mark# X, mark# s X -> s# mark X) (mark# s X -> mark# X, mark# head X -> mark# X) (mark# s X -> mark# X, mark# head X -> active# head mark X) (mark# s X -> mark# X, mark# head X -> head# mark X) (mark# s X -> mark# X, mark# tail X -> mark# X) (mark# s X -> mark# X, mark# tail X -> active# tail mark X) (mark# s X -> mark# X, mark# tail X -> tail# mark X) (active# odds() -> mark# incr pairs(), mark# incr X -> mark# X) (active# odds() -> mark# incr pairs(), mark# incr X -> incr# mark X) (active# odds() -> mark# incr pairs(), mark# incr X -> active# incr mark X) (mark# head X -> active# head mark X, active# head cons(X, XS) -> mark# X) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> mark# cons(s X, incr XS)) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> cons#(s X, incr XS)) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> incr# XS) (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> s# X) } STATUS: arrows: 0.916543 SCCS (1): Scc: { mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X, mark# incr X -> active# incr mark X, mark# nats() -> active# nats(), mark# odds() -> active# odds(), mark# pairs() -> active# pairs(), mark# s X -> mark# X, mark# head X -> mark# X, mark# head X -> active# head mark X, mark# tail X -> mark# X, mark# tail X -> active# tail mark 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# head cons(X, XS) -> mark# X, active# tail cons(X, XS) -> mark# XS} SCC (17): Strict: { mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X, mark# incr X -> active# incr mark X, mark# nats() -> active# nats(), mark# odds() -> active# odds(), mark# pairs() -> active# pairs(), mark# s X -> mark# X, mark# head X -> mark# X, mark# head X -> active# head mark X, mark# tail X -> mark# X, mark# tail X -> active# tail mark 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# head cons(X, XS) -> mark# X, active# tail cons(X, XS) -> mark# XS} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark incr X -> active incr mark X, mark nats() -> active nats(), mark odds() -> active odds(), mark pairs() -> active pairs(), mark s X -> active s mark X, mark head X -> active head mark X, mark tail X -> active tail mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), incr mark X -> incr X, incr active X -> incr 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 head cons(X, XS) -> mark X, active tail cons(X, XS) -> mark XS, s mark X -> s X, s active X -> s X, head mark X -> head X, head active X -> head X, tail mark X -> tail X, tail active X -> tail X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [mark](x0) = x0, [incr](x0) = x0, [active](x0) = x0, [s](x0) = x0, [head](x0) = x0 + 1, [tail](x0) = x0, [0] = 0, [nats] = 0, [odds] = 0, [pairs] = 0, [mark#](x0) = x0, [active#](x0) = x0 Strict: active# tail cons(X, XS) -> mark# XS 0 + 1X + 1XS >= 0 + 1XS active# head cons(X, XS) -> mark# X 1 + 1X + 1XS >= 0 + 1X 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 + 1X + 1XS >= 0 + 1X + 1XS mark# tail X -> active# tail mark X 0 + 1X >= 0 + 1X mark# tail X -> mark# X 0 + 1X >= 0 + 1X mark# head X -> active# head mark X 1 + 1X >= 1 + 1X mark# head X -> mark# X 1 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# pairs() -> active# pairs() 0 >= 0 mark# odds() -> active# odds() 0 >= 0 mark# nats() -> active# nats() 0 >= 0 mark# incr X -> active# incr mark X 0 + 1X >= 0 + 1X mark# incr X -> mark# X 0 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: tail active X -> tail X 0 + 1X >= 0 + 1X tail mark X -> tail X 0 + 1X >= 0 + 1X head active X -> head X 1 + 1X >= 1 + 1X head mark X -> head X 1 + 1X >= 1 + 1X s active X -> s X 0 + 1X >= 0 + 1X s mark X -> s X 0 + 1X >= 0 + 1X active tail cons(X, XS) -> mark XS 0 + 1X + 1XS >= 0 + 1XS active head cons(X, XS) -> mark X 1 + 1X + 1XS >= 0 + 1X 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 + 1X + 1XS >= 0 + 1X + 1XS incr active X -> incr X 0 + 1X >= 0 + 1X incr mark X -> incr X 0 + 1X >= 0 + 1X cons(active X1, X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 cons(mark X1, X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 cons(X1, active X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 cons(X1, mark X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark tail X -> active tail mark X 0 + 1X >= 0 + 1X mark head X -> active head mark X 1 + 1X >= 1 + 1X mark s X -> active s mark X 0 + 1X >= 0 + 1X mark pairs() -> active pairs() 0 >= 0 mark odds() -> active odds() 0 >= 0 mark nats() -> active nats() 0 >= 0 mark incr X -> active incr mark X 0 + 1X >= 0 + 1X mark 0() -> active 0() 0 >= 0 mark cons(X1, X2) -> active cons(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 SCCS (1): Scc: { mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X, mark# incr X -> active# incr mark X, mark# nats() -> active# nats(), mark# odds() -> active# odds(), mark# pairs() -> active# pairs(), mark# s X -> mark# X, mark# tail X -> mark# X, mark# tail X -> active# tail mark 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# tail cons(X, XS) -> mark# XS} SCC (14): Strict: { mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X, mark# incr X -> active# incr mark X, mark# nats() -> active# nats(), mark# odds() -> active# odds(), mark# pairs() -> active# pairs(), mark# s X -> mark# X, mark# tail X -> mark# X, mark# tail X -> active# tail mark 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# tail cons(X, XS) -> mark# XS} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark incr X -> active incr mark X, mark nats() -> active nats(), mark odds() -> active odds(), mark pairs() -> active pairs(), mark s X -> active s mark X, mark head X -> active head mark X, mark tail X -> active tail mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), incr mark X -> incr X, incr active X -> incr 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 head cons(X, XS) -> mark X, active tail cons(X, XS) -> mark XS, s mark X -> s X, s active X -> s X, head mark X -> head X, head active X -> head X, tail mark X -> tail X, tail active X -> tail X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [mark](x0) = x0, [incr](x0) = x0, [active](x0) = x0, [s](x0) = x0, [head](x0) = x0, [tail](x0) = x0 + 1, [0] = 0, [nats] = 0, [odds] = 0, [pairs] = 0, [mark#](x0) = x0, [active#](x0) = x0 Strict: active# tail cons(X, XS) -> mark# XS 1 + 1X + 1XS >= 0 + 1XS 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 + 1X + 1XS >= 0 + 1X + 1XS mark# tail X -> active# tail mark X 1 + 1X >= 1 + 1X mark# tail X -> mark# X 1 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# pairs() -> active# pairs() 0 >= 0 mark# odds() -> active# odds() 0 >= 0 mark# nats() -> active# nats() 0 >= 0 mark# incr X -> active# incr mark X 0 + 1X >= 0 + 1X mark# incr X -> mark# X 0 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: tail active X -> tail X 1 + 1X >= 1 + 1X tail mark X -> tail X 1 + 1X >= 1 + 1X head active X -> head X 0 + 1X >= 0 + 1X head mark X -> head X 0 + 1X >= 0 + 1X s active X -> s X 0 + 1X >= 0 + 1X s mark X -> s X 0 + 1X >= 0 + 1X active tail cons(X, XS) -> mark XS 1 + 1X + 1XS >= 0 + 1XS active head cons(X, XS) -> mark X 0 + 1X + 1XS >= 0 + 1X 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 + 1X + 1XS >= 0 + 1X + 1XS incr active X -> incr X 0 + 1X >= 0 + 1X incr mark X -> incr X 0 + 1X >= 0 + 1X cons(active X1, X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 cons(mark X1, X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 cons(X1, active X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 cons(X1, mark X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark tail X -> active tail mark X 1 + 1X >= 1 + 1X mark head X -> active head mark X 0 + 1X >= 0 + 1X mark s X -> active s mark X 0 + 1X >= 0 + 1X mark pairs() -> active pairs() 0 >= 0 mark odds() -> active odds() 0 >= 0 mark nats() -> active nats() 0 >= 0 mark incr X -> active incr mark X 0 + 1X >= 0 + 1X mark 0() -> active 0() 0 >= 0 mark cons(X1, X2) -> active cons(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 SCCS (1): Scc: { mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X, mark# incr X -> active# incr mark X, mark# nats() -> active# nats(), mark# odds() -> active# odds(), mark# pairs() -> active# pairs(), mark# s X -> mark# 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())} SCC (11): Strict: { mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X, mark# incr X -> active# incr mark X, mark# nats() -> active# nats(), mark# odds() -> active# odds(), mark# pairs() -> active# pairs(), mark# s X -> mark# 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())} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark incr X -> active incr mark X, mark nats() -> active nats(), mark odds() -> active odds(), mark pairs() -> active pairs(), mark s X -> active s mark X, mark head X -> active head mark X, mark tail X -> active tail mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), incr mark X -> incr X, incr active X -> incr 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 head cons(X, XS) -> mark X, active tail cons(X, XS) -> mark XS, s mark X -> s X, s active X -> s X, head mark X -> head X, head active X -> head X, tail mark X -> tail X, tail active X -> tail X} Fail