MAYBE Time: 11.851083 TRS: { mark adx X -> active adx mark X, mark zeros() -> active zeros(), mark nats() -> active nats(), mark cons(X1, X2) -> active cons(X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark incr X -> active incr mark X, mark hd X -> active hd mark X, mark tl X -> active tl mark X, adx mark X -> adx X, adx active X -> adx X, active adx cons(X, Y) -> mark incr cons(X, adx Y), active zeros() -> mark cons(0(), zeros()), active nats() -> mark adx zeros(), active incr cons(X, Y) -> mark cons(s X, incr Y), active hd cons(X, Y) -> mark X, active tl cons(X, Y) -> mark Y, 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), s mark X -> s X, s active X -> s X, incr mark X -> incr X, incr active X -> incr X, hd mark X -> hd X, hd active X -> hd X, tl mark X -> tl X, tl active X -> tl X} DP: DP: { mark# adx X -> mark# X, mark# adx X -> adx# mark X, mark# adx X -> active# adx mark X, mark# zeros() -> active# zeros(), mark# nats() -> active# nats(), mark# cons(X1, X2) -> active# cons(X1, X2), mark# 0() -> active# 0(), mark# s X -> active# s X, mark# incr X -> mark# X, mark# incr X -> active# incr mark X, mark# incr X -> incr# mark X, mark# hd X -> mark# X, mark# hd X -> active# hd mark X, mark# hd X -> hd# mark X, mark# tl X -> mark# X, mark# tl X -> active# tl mark X, mark# tl X -> tl# mark X, adx# mark X -> adx# X, adx# active X -> adx# X, active# adx cons(X, Y) -> mark# incr cons(X, adx Y), active# adx cons(X, Y) -> adx# Y, active# adx cons(X, Y) -> cons#(X, adx Y), active# adx cons(X, Y) -> incr# cons(X, adx Y), active# zeros() -> mark# cons(0(), zeros()), active# zeros() -> cons#(0(), zeros()), active# nats() -> mark# adx zeros(), active# nats() -> adx# zeros(), active# incr cons(X, Y) -> mark# cons(s X, incr Y), active# incr cons(X, Y) -> cons#(s X, incr Y), active# incr cons(X, Y) -> s# X, active# incr cons(X, Y) -> incr# Y, active# hd cons(X, Y) -> mark# X, active# tl cons(X, Y) -> mark# Y, 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), s# mark X -> s# X, s# active X -> s# X, incr# mark X -> incr# X, incr# active X -> incr# X, hd# mark X -> hd# X, hd# active X -> hd# X, tl# mark X -> tl# X, tl# active X -> tl# X} TRS: { mark adx X -> active adx mark X, mark zeros() -> active zeros(), mark nats() -> active nats(), mark cons(X1, X2) -> active cons(X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark incr X -> active incr mark X, mark hd X -> active hd mark X, mark tl X -> active tl mark X, adx mark X -> adx X, adx active X -> adx X, active adx cons(X, Y) -> mark incr cons(X, adx Y), active zeros() -> mark cons(0(), zeros()), active nats() -> mark adx zeros(), active incr cons(X, Y) -> mark cons(s X, incr Y), active hd cons(X, Y) -> mark X, active tl cons(X, Y) -> mark Y, 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), s mark X -> s X, s active X -> s X, incr mark X -> incr X, incr active X -> incr X, hd mark X -> hd X, hd active X -> hd X, tl mark X -> tl X, tl active X -> tl X} UR: { mark adx X -> active adx mark X, mark zeros() -> active zeros(), mark nats() -> active nats(), mark cons(X1, X2) -> active cons(X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark incr X -> active incr mark X, mark hd X -> active hd mark X, mark tl X -> active tl mark X, adx mark X -> adx X, adx active X -> adx X, active adx cons(X, Y) -> mark incr cons(X, adx Y), active zeros() -> mark cons(0(), zeros()), active nats() -> mark adx zeros(), active incr cons(X, Y) -> mark cons(s X, incr Y), active hd cons(X, Y) -> mark X, active tl cons(X, Y) -> mark Y, 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), s mark X -> s X, s active X -> s X, incr mark X -> incr X, incr active X -> incr X, hd mark X -> hd X, hd active X -> hd X, tl mark X -> tl X, tl active X -> tl X} EDG: { (mark# incr X -> active# incr mark X, active# incr cons(X, Y) -> incr# Y) (mark# incr X -> active# incr mark X, active# incr cons(X, Y) -> s# X) (mark# incr X -> active# incr mark X, active# incr cons(X, Y) -> cons#(s X, incr Y)) (mark# incr X -> active# incr mark X, active# incr cons(X, Y) -> mark# cons(s X, incr Y)) (mark# tl X -> active# tl mark X, active# tl cons(X, Y) -> mark# Y) (active# nats() -> mark# adx zeros(), mark# adx X -> active# adx mark X) (active# nats() -> mark# adx zeros(), mark# adx X -> adx# mark X) (active# nats() -> mark# adx zeros(), mark# adx X -> mark# X) (mark# incr X -> mark# X, mark# tl X -> tl# mark X) (mark# incr X -> mark# X, mark# tl X -> active# tl mark X) (mark# incr X -> mark# X, mark# tl X -> mark# X) (mark# incr X -> mark# X, mark# hd X -> hd# mark X) (mark# incr X -> mark# X, mark# hd X -> active# hd mark X) (mark# incr X -> mark# X, mark# hd X -> mark# X) (mark# incr X -> mark# X, mark# incr X -> incr# mark X) (mark# incr X -> mark# X, mark# incr X -> active# incr mark X) (mark# incr X -> mark# X, mark# incr X -> mark# X) (mark# incr X -> mark# X, mark# s X -> active# s X) (mark# incr X -> mark# X, mark# 0() -> active# 0()) (mark# incr X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# incr X -> mark# X, mark# nats() -> active# nats()) (mark# incr X -> mark# X, mark# zeros() -> active# zeros()) (mark# incr X -> mark# X, mark# adx X -> active# adx mark X) (mark# incr X -> mark# X, mark# adx X -> adx# mark X) (mark# incr X -> mark# X, mark# adx X -> mark# X) (mark# tl X -> mark# X, mark# tl X -> tl# mark X) (mark# tl X -> mark# X, mark# tl X -> active# tl mark X) (mark# tl X -> mark# X, mark# tl X -> mark# X) (mark# tl X -> mark# X, mark# hd X -> hd# mark X) (mark# tl X -> mark# X, mark# hd X -> active# hd mark X) (mark# tl X -> mark# X, mark# hd X -> mark# X) (mark# tl X -> mark# X, mark# incr X -> incr# mark X) (mark# tl X -> mark# X, mark# incr X -> active# incr mark X) (mark# tl X -> mark# X, mark# incr X -> mark# X) (mark# tl X -> mark# X, mark# s X -> active# s X) (mark# tl X -> mark# X, mark# 0() -> active# 0()) (mark# tl X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# tl X -> mark# X, mark# nats() -> active# nats()) (mark# tl X -> mark# X, mark# zeros() -> active# zeros()) (mark# tl X -> mark# X, mark# adx X -> active# adx mark X) (mark# tl X -> mark# X, mark# adx X -> adx# mark X) (mark# tl X -> mark# X, mark# adx X -> mark# X) (adx# active X -> adx# X, adx# active X -> adx# X) (adx# active X -> adx# X, adx# mark X -> adx# X) (active# hd cons(X, Y) -> mark# X, mark# tl X -> tl# mark X) (active# hd cons(X, Y) -> mark# X, mark# tl X -> active# tl mark X) (active# hd cons(X, Y) -> mark# X, mark# tl X -> mark# X) (active# hd cons(X, Y) -> mark# X, mark# hd X -> hd# mark X) (active# hd cons(X, Y) -> mark# X, mark# hd X -> active# hd mark X) (active# hd cons(X, Y) -> mark# X, mark# hd X -> mark# X) (active# hd cons(X, Y) -> mark# X, mark# incr X -> incr# mark X) (active# hd cons(X, Y) -> mark# X, mark# incr X -> active# incr mark X) (active# hd cons(X, Y) -> mark# X, mark# incr X -> mark# X) (active# hd cons(X, Y) -> mark# X, mark# s X -> active# s X) (active# hd cons(X, Y) -> mark# X, mark# 0() -> active# 0()) (active# hd cons(X, Y) -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (active# hd cons(X, Y) -> mark# X, mark# nats() -> active# nats()) (active# hd cons(X, Y) -> mark# X, mark# zeros() -> active# zeros()) (active# hd cons(X, Y) -> mark# X, mark# adx X -> active# adx mark X) (active# hd cons(X, Y) -> mark# X, mark# adx X -> adx# mark X) (active# hd cons(X, Y) -> mark# X, mark# adx X -> mark# X) (s# active X -> s# X, s# active X -> s# X) (s# active X -> s# X, s# mark X -> s# X) (incr# active X -> incr# X, incr# active X -> incr# X) (incr# active X -> incr# X, incr# mark X -> incr# X) (hd# active X -> hd# X, hd# active X -> hd# X) (hd# active X -> hd# X, hd# mark X -> hd# X) (tl# active X -> tl# X, tl# active X -> tl# X) (tl# active X -> tl# X, tl# mark X -> tl# X) (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# incr cons(X, Y) -> incr# Y, incr# active X -> incr# X) (active# incr cons(X, Y) -> incr# Y, incr# mark X -> incr# X) (active# adx cons(X, Y) -> cons#(X, adx Y), cons#(active X1, X2) -> cons#(X1, X2)) (active# adx cons(X, Y) -> cons#(X, adx Y), cons#(mark X1, X2) -> cons#(X1, X2)) (mark# adx X -> adx# mark X, adx# active X -> adx# X) (mark# adx X -> adx# mark X, adx# mark X -> adx# X) (mark# incr X -> incr# mark X, incr# active X -> incr# X) (mark# incr X -> incr# mark X, incr# mark X -> incr# X) (mark# tl X -> tl# mark X, tl# active X -> tl# X) (mark# tl X -> tl# mark X, tl# mark X -> tl# X) (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# nats() -> active# nats(), active# nats() -> adx# zeros()) (mark# nats() -> active# nats(), active# nats() -> mark# adx zeros()) (mark# zeros() -> active# zeros(), active# zeros() -> mark# cons(0(), zeros())) (mark# zeros() -> active# zeros(), active# zeros() -> cons#(0(), zeros())) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (mark# hd X -> hd# mark X, hd# mark X -> hd# X) (mark# hd X -> hd# mark X, hd# active X -> hd# X) (active# tl cons(X, Y) -> mark# Y, mark# adx X -> mark# X) (active# tl cons(X, Y) -> mark# Y, mark# adx X -> adx# mark X) (active# tl cons(X, Y) -> mark# Y, mark# adx X -> active# adx mark X) (active# tl cons(X, Y) -> mark# Y, mark# zeros() -> active# zeros()) (active# tl cons(X, Y) -> mark# Y, mark# nats() -> active# nats()) (active# tl cons(X, Y) -> mark# Y, mark# cons(X1, X2) -> active# cons(X1, X2)) (active# tl cons(X, Y) -> mark# Y, mark# 0() -> active# 0()) (active# tl cons(X, Y) -> mark# Y, mark# s X -> active# s X) (active# tl cons(X, Y) -> mark# Y, mark# incr X -> mark# X) (active# tl cons(X, Y) -> mark# Y, mark# incr X -> active# incr mark X) (active# tl cons(X, Y) -> mark# Y, mark# incr X -> incr# mark X) (active# tl cons(X, Y) -> mark# Y, mark# hd X -> mark# X) (active# tl cons(X, Y) -> mark# Y, mark# hd X -> active# hd mark X) (active# tl cons(X, Y) -> mark# Y, mark# hd X -> hd# mark X) (active# tl cons(X, Y) -> mark# Y, mark# tl X -> mark# X) (active# tl cons(X, Y) -> mark# Y, mark# tl X -> active# tl mark X) (active# tl cons(X, Y) -> mark# Y, mark# tl X -> tl# mark X) (active# adx cons(X, Y) -> adx# Y, adx# mark X -> adx# X) (active# adx cons(X, Y) -> adx# Y, adx# active X -> adx# X) (active# incr cons(X, Y) -> mark# cons(s X, incr Y), mark# cons(X1, X2) -> active# cons(X1, X2)) (tl# mark X -> tl# X, tl# mark X -> tl# X) (tl# mark X -> tl# X, tl# active X -> tl# X) (hd# mark X -> hd# X, hd# mark X -> hd# X) (hd# mark X -> hd# X, hd# active X -> hd# X) (incr# mark X -> incr# X, incr# mark X -> incr# X) (incr# mark X -> incr# X, incr# active X -> incr# X) (s# mark X -> s# X, s# mark X -> s# X) (s# mark X -> s# X, s# active X -> s# X) (active# incr cons(X, Y) -> s# X, s# mark X -> s# X) (active# incr cons(X, Y) -> s# X, s# active X -> s# X) (adx# mark X -> adx# X, adx# mark X -> adx# X) (adx# mark X -> adx# X, adx# active X -> adx# X) (mark# hd X -> mark# X, mark# adx X -> mark# X) (mark# hd X -> mark# X, mark# adx X -> adx# mark X) (mark# hd X -> mark# X, mark# adx X -> active# adx mark X) (mark# hd X -> mark# X, mark# zeros() -> active# zeros()) (mark# hd X -> mark# X, mark# nats() -> active# nats()) (mark# hd X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# hd X -> mark# X, mark# 0() -> active# 0()) (mark# hd X -> mark# X, mark# s X -> active# s X) (mark# hd X -> mark# X, mark# incr X -> mark# X) (mark# hd X -> mark# X, mark# incr X -> active# incr mark X) (mark# hd X -> mark# X, mark# incr X -> incr# mark X) (mark# hd X -> mark# X, mark# hd X -> mark# X) (mark# hd X -> mark# X, mark# hd X -> active# hd mark X) (mark# hd X -> mark# X, mark# hd X -> hd# mark X) (mark# hd X -> mark# X, mark# tl X -> mark# X) (mark# hd X -> mark# X, mark# tl X -> active# tl mark X) (mark# hd X -> mark# X, mark# tl X -> tl# mark X) (mark# adx X -> mark# X, mark# adx X -> mark# X) (mark# adx X -> mark# X, mark# adx X -> adx# mark X) (mark# adx X -> mark# X, mark# adx X -> active# adx mark X) (mark# adx X -> mark# X, mark# zeros() -> active# zeros()) (mark# adx X -> mark# X, mark# nats() -> active# nats()) (mark# adx X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# adx X -> mark# X, mark# 0() -> active# 0()) (mark# adx X -> mark# X, mark# s X -> active# s X) (mark# adx X -> mark# X, mark# incr X -> mark# X) (mark# adx X -> mark# X, mark# incr X -> active# incr mark X) (mark# adx X -> mark# X, mark# incr X -> incr# mark X) (mark# adx X -> mark# X, mark# hd X -> mark# X) (mark# adx X -> mark# X, mark# hd X -> active# hd mark X) (mark# adx X -> mark# X, mark# hd X -> hd# mark X) (mark# adx X -> mark# X, mark# tl X -> mark# X) (mark# adx X -> mark# X, mark# tl X -> active# tl mark X) (mark# adx X -> mark# X, mark# tl X -> tl# mark X) (active# adx cons(X, Y) -> mark# incr cons(X, adx Y), mark# incr X -> mark# X) (active# adx cons(X, Y) -> mark# incr cons(X, adx Y), mark# incr X -> active# incr mark X) (active# adx cons(X, Y) -> mark# incr cons(X, adx Y), mark# incr X -> incr# mark X) (mark# hd X -> active# hd mark X, active# hd cons(X, Y) -> mark# X) (mark# adx X -> active# adx mark X, active# adx cons(X, Y) -> mark# incr cons(X, adx Y)) (mark# adx X -> active# adx mark X, active# adx cons(X, Y) -> adx# Y) (mark# adx X -> active# adx mark X, active# adx cons(X, Y) -> cons#(X, adx Y)) (mark# adx X -> active# adx mark X, active# adx cons(X, Y) -> incr# cons(X, adx Y)) } STATUS: arrows: 0.913086 SCCS (7): Scc: { mark# adx X -> mark# X, mark# adx X -> active# adx mark X, mark# nats() -> active# nats(), mark# incr X -> mark# X, mark# hd X -> mark# X, mark# hd X -> active# hd mark X, mark# tl X -> mark# X, mark# tl X -> active# tl mark X, active# adx cons(X, Y) -> mark# incr cons(X, adx Y), active# nats() -> mark# adx zeros(), active# hd cons(X, Y) -> mark# X, active# tl cons(X, Y) -> mark# Y} Scc: { cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)} Scc: { tl# mark X -> tl# X, tl# active X -> tl# X} Scc: { hd# mark X -> hd# X, hd# active X -> hd# X} Scc: { incr# mark X -> incr# X, incr# active X -> incr# X} Scc: { s# mark X -> s# X, s# active X -> s# X} Scc: { adx# mark X -> adx# X, adx# active X -> adx# X} SCC (12): Strict: { mark# adx X -> mark# X, mark# adx X -> active# adx mark X, mark# nats() -> active# nats(), mark# incr X -> mark# X, mark# hd X -> mark# X, mark# hd X -> active# hd mark X, mark# tl X -> mark# X, mark# tl X -> active# tl mark X, active# adx cons(X, Y) -> mark# incr cons(X, adx Y), active# nats() -> mark# adx zeros(), active# hd cons(X, Y) -> mark# X, active# tl cons(X, Y) -> mark# Y} Weak: { mark adx X -> active adx mark X, mark zeros() -> active zeros(), mark nats() -> active nats(), mark cons(X1, X2) -> active cons(X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark incr X -> active incr mark X, mark hd X -> active hd mark X, mark tl X -> active tl mark X, adx mark X -> adx X, adx active X -> adx X, active adx cons(X, Y) -> mark incr cons(X, adx Y), active zeros() -> mark cons(0(), zeros()), active nats() -> mark adx zeros(), active incr cons(X, Y) -> mark cons(s X, incr Y), active hd cons(X, Y) -> mark X, active tl cons(X, Y) -> mark Y, 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), s mark X -> s X, s active X -> s X, incr mark X -> incr X, incr active X -> incr X, hd mark X -> hd X, hd active X -> hd X, tl mark X -> tl X, tl active X -> tl X} Open SCC (4): Strict: { cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)} Weak: { mark adx X -> active adx mark X, mark zeros() -> active zeros(), mark nats() -> active nats(), mark cons(X1, X2) -> active cons(X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark incr X -> active incr mark X, mark hd X -> active hd mark X, mark tl X -> active tl mark X, adx mark X -> adx X, adx active X -> adx X, active adx cons(X, Y) -> mark incr cons(X, adx Y), active zeros() -> mark cons(0(), zeros()), active nats() -> mark adx zeros(), active incr cons(X, Y) -> mark cons(s X, incr Y), active hd cons(X, Y) -> mark X, active tl cons(X, Y) -> mark Y, 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), s mark X -> s X, s active X -> s X, incr mark X -> incr X, incr active X -> incr X, hd mark X -> hd X, hd active X -> hd X, tl mark X -> tl X, tl active X -> tl X} Open SCC (2): Strict: { tl# mark X -> tl# X, tl# active X -> tl# X} Weak: { mark adx X -> active adx mark X, mark zeros() -> active zeros(), mark nats() -> active nats(), mark cons(X1, X2) -> active cons(X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark incr X -> active incr mark X, mark hd X -> active hd mark X, mark tl X -> active tl mark X, adx mark X -> adx X, adx active X -> adx X, active adx cons(X, Y) -> mark incr cons(X, adx Y), active zeros() -> mark cons(0(), zeros()), active nats() -> mark adx zeros(), active incr cons(X, Y) -> mark cons(s X, incr Y), active hd cons(X, Y) -> mark X, active tl cons(X, Y) -> mark Y, 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), s mark X -> s X, s active X -> s X, incr mark X -> incr X, incr active X -> incr X, hd mark X -> hd X, hd active X -> hd X, tl mark X -> tl X, tl active X -> tl X} Open SCC (2): Strict: { hd# mark X -> hd# X, hd# active X -> hd# X} Weak: { mark adx X -> active adx mark X, mark zeros() -> active zeros(), mark nats() -> active nats(), mark cons(X1, X2) -> active cons(X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark incr X -> active incr mark X, mark hd X -> active hd mark X, mark tl X -> active tl mark X, adx mark X -> adx X, adx active X -> adx X, active adx cons(X, Y) -> mark incr cons(X, adx Y), active zeros() -> mark cons(0(), zeros()), active nats() -> mark adx zeros(), active incr cons(X, Y) -> mark cons(s X, incr Y), active hd cons(X, Y) -> mark X, active tl cons(X, Y) -> mark Y, 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), s mark X -> s X, s active X -> s X, incr mark X -> incr X, incr active X -> incr X, hd mark X -> hd X, hd active X -> hd X, tl mark X -> tl X, tl active X -> tl X} Open SCC (2): Strict: { incr# mark X -> incr# X, incr# active X -> incr# X} Weak: { mark adx X -> active adx mark X, mark zeros() -> active zeros(), mark nats() -> active nats(), mark cons(X1, X2) -> active cons(X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark incr X -> active incr mark X, mark hd X -> active hd mark X, mark tl X -> active tl mark X, adx mark X -> adx X, adx active X -> adx X, active adx cons(X, Y) -> mark incr cons(X, adx Y), active zeros() -> mark cons(0(), zeros()), active nats() -> mark adx zeros(), active incr cons(X, Y) -> mark cons(s X, incr Y), active hd cons(X, Y) -> mark X, active tl cons(X, Y) -> mark Y, 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), s mark X -> s X, s active X -> s X, incr mark X -> incr X, incr active X -> incr X, hd mark X -> hd X, hd active X -> hd X, tl mark X -> tl X, tl active X -> tl X} Open SCC (2): Strict: { s# mark X -> s# X, s# active X -> s# X} Weak: { mark adx X -> active adx mark X, mark zeros() -> active zeros(), mark nats() -> active nats(), mark cons(X1, X2) -> active cons(X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark incr X -> active incr mark X, mark hd X -> active hd mark X, mark tl X -> active tl mark X, adx mark X -> adx X, adx active X -> adx X, active adx cons(X, Y) -> mark incr cons(X, adx Y), active zeros() -> mark cons(0(), zeros()), active nats() -> mark adx zeros(), active incr cons(X, Y) -> mark cons(s X, incr Y), active hd cons(X, Y) -> mark X, active tl cons(X, Y) -> mark Y, 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), s mark X -> s X, s active X -> s X, incr mark X -> incr X, incr active X -> incr X, hd mark X -> hd X, hd active X -> hd X, tl mark X -> tl X, tl active X -> tl X} Open SCC (2): Strict: { adx# mark X -> adx# X, adx# active X -> adx# X} Weak: { mark adx X -> active adx mark X, mark zeros() -> active zeros(), mark nats() -> active nats(), mark cons(X1, X2) -> active cons(X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark incr X -> active incr mark X, mark hd X -> active hd mark X, mark tl X -> active tl mark X, adx mark X -> adx X, adx active X -> adx X, active adx cons(X, Y) -> mark incr cons(X, adx Y), active zeros() -> mark cons(0(), zeros()), active nats() -> mark adx zeros(), active incr cons(X, Y) -> mark cons(s X, incr Y), active hd cons(X, Y) -> mark X, active tl cons(X, Y) -> mark Y, 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), s mark X -> s X, s active X -> s X, incr mark X -> incr X, incr active X -> incr X, hd mark X -> hd X, hd active X -> hd X, tl mark X -> tl X, tl active X -> tl X} Open