MAYBE Time: 0.080441 TRS: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} DP: DP: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2), mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# recip X -> mark# X, mark# recip X -> recip# mark X, mark# recip X -> active# recip mark X, mark# sqr X -> mark# X, mark# sqr X -> sqr# mark X, mark# sqr X -> active# sqr mark X, mark# terms X -> mark# X, mark# terms X -> terms# mark X, mark# terms X -> active# terms mark X, mark# s X -> active# s X, mark# 0() -> active# 0(), mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2), mark# add(X1, X2) -> add#(mark X1, mark X2), mark# dbl X -> mark# X, mark# dbl X -> active# dbl mark X, mark# dbl X -> dbl# mark X, mark# nil() -> active# nil(), mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2), mark# first(X1, X2) -> first#(mark X1, mark X2), cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2), recip# mark X -> recip# X, recip# active X -> recip# X, sqr# mark X -> sqr# X, sqr# active X -> sqr# X, terms# mark X -> terms# X, terms# active X -> terms# X, s# mark X -> s# X, s# active X -> s# X, active# sqr s X -> mark# s add(sqr X, dbl X), active# sqr s X -> sqr# X, active# sqr s X -> s# add(sqr X, dbl X), active# sqr s X -> add#(sqr X, dbl X), active# sqr s X -> dbl# X, active# sqr 0() -> mark# 0(), active# terms N -> mark# cons(recip sqr N, terms s N), active# terms N -> cons#(recip sqr N, terms s N), active# terms N -> recip# sqr N, active# terms N -> sqr# N, active# terms N -> terms# s N, active# terms N -> s# N, active# add(s X, Y) -> mark# s add(X, Y), active# add(s X, Y) -> s# add(X, Y), active# add(s X, Y) -> add#(X, Y), active# add(0(), X) -> mark# X, active# dbl s X -> mark# s s dbl X, active# dbl s X -> s# s dbl X, active# dbl s X -> s# dbl X, active# dbl s X -> dbl# X, active# dbl 0() -> mark# 0(), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), active# first(s X, cons(Y, Z)) -> first#(X, Z), active# first(0(), X) -> mark# nil(), add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2), dbl# mark X -> dbl# X, dbl# active X -> dbl# X, first#(X1, mark X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)} TRS: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} UR: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), a(x, y) -> x, a(x, y) -> y} EDG: { (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(active X1, X2) -> first#(X1, X2)) (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(mark X1, X2) -> first#(X1, X2)) (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, active X2) -> first#(X1, X2)) (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, mark X2) -> first#(X1, X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> mark# X2) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> mark# X1) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# nil() -> active# nil()) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# dbl X -> dbl# mark X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# dbl X -> active# dbl mark X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# dbl X -> mark# X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# add(X1, X2) -> mark# X2) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# add(X1, X2) -> mark# X1) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# 0() -> active# 0()) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> active# s X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# terms X -> active# terms mark X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# terms X -> terms# mark X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# terms X -> mark# X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# sqr X -> active# sqr mark X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# sqr X -> sqr# mark X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# sqr X -> mark# X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# recip X -> active# recip mark X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# recip X -> recip# mark X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# recip X -> mark# X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(0(), X) -> mark# nil()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# dbl 0() -> mark# 0()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# dbl s X -> dbl# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# dbl s X -> s# dbl X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# dbl s X -> s# s dbl X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# dbl s X -> mark# s s dbl X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# add(0(), X) -> mark# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# add(s X, Y) -> add#(X, Y)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# add(s X, Y) -> s# add(X, Y)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# terms N -> s# N) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# terms N -> terms# s N) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# terms N -> sqr# N) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# terms N -> recip# sqr N) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# terms N -> cons#(recip sqr N, terms s N)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# terms N -> mark# cons(recip sqr N, terms s N)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sqr 0() -> mark# 0()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sqr s X -> dbl# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sqr s X -> add#(sqr X, dbl X)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sqr s X -> s# add(sqr X, dbl X)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sqr s X -> sqr# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sqr s X -> mark# s add(sqr X, dbl X)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# recip X -> recip# mark X, recip# active X -> recip# X) (mark# recip X -> recip# mark X, recip# mark X -> recip# X) (mark# terms X -> terms# mark X, terms# active X -> terms# X) (mark# terms X -> terms# mark X, terms# mark X -> terms# X) (mark# dbl X -> dbl# mark X, dbl# active X -> dbl# X) (mark# dbl X -> dbl# mark X, dbl# mark X -> dbl# X) (active# terms N -> recip# sqr N, recip# active X -> recip# X) (active# terms N -> recip# sqr N, recip# mark X -> recip# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# first(0(), X) -> mark# nil()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# dbl 0() -> mark# 0()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# dbl s X -> dbl# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# dbl s X -> s# dbl X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# dbl s X -> s# s dbl X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# dbl s X -> mark# s s dbl X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(0(), X) -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# terms N -> s# N) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# terms N -> terms# s N) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# terms N -> sqr# N) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# terms N -> recip# sqr N) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# terms N -> cons#(recip sqr N, terms s N)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# terms N -> mark# cons(recip sqr N, terms s N)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# sqr 0() -> mark# 0()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# sqr s X -> dbl# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# sqr s X -> add#(sqr X, dbl X)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# sqr s X -> s# add(sqr X, dbl X)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# sqr s X -> sqr# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# sqr s X -> mark# s add(sqr X, dbl X)) (active# sqr s X -> s# add(sqr X, dbl X), s# active X -> s# X) (active# sqr s X -> s# add(sqr X, dbl X), s# mark X -> s# X) (active# sqr 0() -> mark# 0(), mark# 0() -> active# 0()) (active# first(0(), X) -> mark# nil(), mark# nil() -> active# nil()) (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)) (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (first#(X1, active X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)) (first#(X1, active X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2)) (first#(X1, active X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2)) (first#(X1, active X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2)) (first#(active X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)) (first#(active X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2)) (first#(active X1, X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2)) (first#(active X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2)) (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# nil() -> active# nil()) (mark# add(X1, X2) -> mark# X2, mark# dbl X -> dbl# mark X) (mark# add(X1, X2) -> mark# X2, mark# dbl X -> active# dbl mark X) (mark# add(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s X) (mark# add(X1, X2) -> mark# X2, mark# terms X -> active# terms mark X) (mark# add(X1, X2) -> mark# X2, mark# terms X -> terms# mark X) (mark# add(X1, X2) -> mark# X2, mark# terms X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> active# sqr mark X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> sqr# mark X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# recip X -> active# recip mark X) (mark# add(X1, X2) -> mark# X2, mark# recip X -> recip# mark X) (mark# add(X1, X2) -> mark# X2, mark# recip X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# recip X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# recip X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# recip X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# recip X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# recip X -> mark# X, mark# nil() -> active# nil()) (mark# recip X -> mark# X, mark# dbl X -> dbl# mark X) (mark# recip X -> mark# X, mark# dbl X -> active# dbl mark X) (mark# recip X -> mark# X, mark# dbl X -> mark# X) (mark# recip X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# recip X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# recip X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# recip X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# recip X -> mark# X, mark# 0() -> active# 0()) (mark# recip X -> mark# X, mark# s X -> active# s X) (mark# recip X -> mark# X, mark# terms X -> active# terms mark X) (mark# recip X -> mark# X, mark# terms X -> terms# mark X) (mark# recip X -> mark# X, mark# terms X -> mark# X) (mark# recip X -> mark# X, mark# sqr X -> active# sqr mark X) (mark# recip X -> mark# X, mark# sqr X -> sqr# mark X) (mark# recip X -> mark# X, mark# sqr X -> mark# X) (mark# recip X -> mark# X, mark# recip X -> active# recip mark X) (mark# recip X -> mark# X, mark# recip X -> recip# mark X) (mark# recip X -> mark# X, mark# recip X -> mark# X) (mark# recip X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# recip X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# recip X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# terms X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# nil() -> active# nil()) (mark# terms X -> mark# X, mark# dbl X -> dbl# mark X) (mark# terms X -> mark# X, mark# dbl X -> active# dbl mark X) (mark# terms X -> mark# X, mark# dbl X -> mark# X) (mark# terms X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# terms X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# 0() -> active# 0()) (mark# terms X -> mark# X, mark# s X -> active# s X) (mark# terms X -> mark# X, mark# terms X -> active# terms mark X) (mark# terms X -> mark# X, mark# terms X -> terms# mark X) (mark# terms X -> mark# X, mark# terms X -> mark# X) (mark# terms X -> mark# X, mark# sqr X -> active# sqr mark X) (mark# terms X -> mark# X, mark# sqr X -> sqr# mark X) (mark# terms X -> mark# X, mark# sqr X -> mark# X) (mark# terms X -> mark# X, mark# recip X -> active# recip mark X) (mark# terms X -> mark# X, mark# recip X -> recip# mark X) (mark# terms X -> mark# X, mark# recip X -> mark# X) (mark# terms X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# terms X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# terms X -> mark# X, mark# cons(X1, X2) -> mark# X1) (recip# mark X -> recip# X, recip# active X -> recip# X) (recip# mark X -> recip# X, recip# mark X -> recip# X) (sqr# mark X -> sqr# X, sqr# active X -> sqr# X) (sqr# mark X -> sqr# X, sqr# mark X -> sqr# X) (terms# mark X -> terms# X, terms# active X -> terms# X) (terms# mark X -> terms# X, terms# mark X -> terms# X) (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (active# sqr s X -> sqr# X, sqr# active X -> sqr# X) (active# sqr s X -> sqr# X, sqr# mark X -> sqr# X) (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# nil() -> active# nil()) (active# add(0(), X) -> mark# X, mark# dbl X -> dbl# mark X) (active# add(0(), X) -> mark# X, mark# dbl X -> active# dbl mark X) (active# add(0(), X) -> mark# X, mark# dbl X -> mark# X) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# 0() -> active# 0()) (active# add(0(), X) -> mark# X, mark# s X -> active# s X) (active# add(0(), X) -> mark# X, mark# terms X -> active# terms mark X) (active# add(0(), X) -> mark# X, mark# terms X -> terms# mark X) (active# add(0(), X) -> mark# X, mark# terms X -> mark# X) (active# add(0(), X) -> mark# X, mark# sqr X -> active# sqr mark X) (active# add(0(), X) -> mark# X, mark# sqr X -> sqr# mark X) (active# add(0(), X) -> mark# X, mark# sqr X -> mark# X) (active# add(0(), X) -> mark# X, mark# recip X -> active# recip mark X) (active# add(0(), X) -> mark# X, mark# recip X -> recip# mark X) (active# add(0(), X) -> mark# X, mark# recip X -> mark# X) (active# add(0(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# add(0(), X) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# add(0(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (dbl# mark X -> dbl# X, dbl# active X -> dbl# X) (dbl# mark X -> dbl# X, dbl# mark X -> dbl# X) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# cons(X1, X2) -> mark# X1, mark# dbl X -> dbl# mark X) (mark# cons(X1, X2) -> mark# X1, mark# dbl X -> active# dbl mark X) (mark# cons(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s X) (mark# cons(X1, X2) -> mark# X1, mark# terms X -> active# terms mark X) (mark# cons(X1, X2) -> mark# X1, mark# terms X -> terms# mark X) (mark# cons(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> active# sqr mark X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> sqr# mark X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# recip X -> active# recip mark X) (mark# cons(X1, X2) -> mark# X1, mark# recip X -> recip# mark X) (mark# cons(X1, X2) -> mark# X1, mark# recip X -> mark# X) (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# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# first(X1, X2) -> mark# X1, mark# dbl X -> dbl# mark X) (mark# first(X1, X2) -> mark# X1, mark# dbl X -> active# dbl mark X) (mark# first(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# first(X1, X2) -> mark# X1, mark# s X -> active# s X) (mark# first(X1, X2) -> mark# X1, mark# terms X -> active# terms mark X) (mark# first(X1, X2) -> mark# X1, mark# terms X -> terms# mark X) (mark# first(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> active# sqr mark X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> sqr# mark X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# recip X -> active# recip mark X) (mark# first(X1, X2) -> mark# X1, mark# recip X -> recip# mark X) (mark# first(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (active# terms N -> sqr# N, sqr# active X -> sqr# X) (active# terms N -> sqr# N, sqr# mark X -> sqr# X) (active# dbl s X -> mark# s s dbl X, mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# dbl s X -> mark# s s dbl X, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# dbl s X -> mark# s s dbl X, mark# first(X1, X2) -> mark# X2) (active# dbl s X -> mark# s s dbl X, mark# first(X1, X2) -> mark# X1) (active# dbl s X -> mark# s s dbl X, mark# nil() -> active# nil()) (active# dbl s X -> mark# s s dbl X, mark# dbl X -> dbl# mark X) (active# dbl s X -> mark# s s dbl X, mark# dbl X -> active# dbl mark X) (active# dbl s X -> mark# s s dbl X, mark# dbl X -> mark# X) (active# dbl s X -> mark# s s dbl X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# dbl s X -> mark# s s dbl X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# dbl s X -> mark# s s dbl X, mark# add(X1, X2) -> mark# X2) (active# dbl s X -> mark# s s dbl X, mark# add(X1, X2) -> mark# X1) (active# dbl s X -> mark# s s dbl X, mark# 0() -> active# 0()) (active# dbl s X -> mark# s s dbl X, mark# s X -> active# s X) (active# dbl s X -> mark# s s dbl X, mark# terms X -> active# terms mark X) (active# dbl s X -> mark# s s dbl X, mark# terms X -> terms# mark X) (active# dbl s X -> mark# s s dbl X, mark# terms X -> mark# X) (active# dbl s X -> mark# s s dbl X, mark# sqr X -> active# sqr mark X) (active# dbl s X -> mark# s s dbl X, mark# sqr X -> sqr# mark X) (active# dbl s X -> mark# s s dbl X, mark# sqr X -> mark# X) (active# dbl s X -> mark# s s dbl X, mark# recip X -> active# recip mark X) (active# dbl s X -> mark# s s dbl X, mark# recip X -> recip# mark X) (active# dbl s X -> mark# s s dbl X, mark# recip X -> mark# X) (active# dbl s X -> mark# s s dbl X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# dbl s X -> mark# s s dbl X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# dbl s X -> mark# s s dbl X, mark# cons(X1, X2) -> mark# X1) (mark# sqr X -> active# sqr mark X, active# first(0(), X) -> mark# nil()) (mark# sqr X -> active# sqr mark X, active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# sqr X -> active# sqr mark X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# sqr X -> active# sqr mark X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# sqr X -> active# sqr mark X, active# dbl 0() -> mark# 0()) (mark# sqr X -> active# sqr mark X, active# dbl s X -> dbl# X) (mark# sqr X -> active# sqr mark X, active# dbl s X -> s# dbl X) (mark# sqr X -> active# sqr mark X, active# dbl s X -> s# s dbl X) (mark# sqr X -> active# sqr mark X, active# dbl s X -> mark# s s dbl X) (mark# sqr X -> active# sqr mark X, active# add(0(), X) -> mark# X) (mark# sqr X -> active# sqr mark X, active# add(s X, Y) -> add#(X, Y)) (mark# sqr X -> active# sqr mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# sqr X -> active# sqr mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# sqr X -> active# sqr mark X, active# terms N -> s# N) (mark# sqr X -> active# sqr mark X, active# terms N -> terms# s N) (mark# sqr X -> active# sqr mark X, active# terms N -> sqr# N) (mark# sqr X -> active# sqr mark X, active# terms N -> recip# sqr N) (mark# sqr X -> active# sqr mark X, active# terms N -> cons#(recip sqr N, terms s N)) (mark# sqr X -> active# sqr mark X, active# terms N -> mark# cons(recip sqr N, terms s N)) (mark# sqr X -> active# sqr mark X, active# sqr 0() -> mark# 0()) (mark# sqr X -> active# sqr mark X, active# sqr s X -> dbl# X) (mark# sqr X -> active# sqr mark X, active# sqr s X -> add#(sqr X, dbl X)) (mark# sqr X -> active# sqr mark X, active# sqr s X -> s# add(sqr X, dbl X)) (mark# sqr X -> active# sqr mark X, active# sqr s X -> sqr# X) (mark# sqr X -> active# sqr mark X, active# sqr s X -> mark# s add(sqr X, dbl X)) (mark# dbl X -> active# dbl mark X, active# first(0(), X) -> mark# nil()) (mark# dbl X -> active# dbl mark X, active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# dbl X -> active# dbl mark X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# dbl X -> active# dbl mark X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# dbl X -> active# dbl mark X, active# dbl 0() -> mark# 0()) (mark# dbl X -> active# dbl mark X, active# dbl s X -> dbl# X) (mark# dbl X -> active# dbl mark X, active# dbl s X -> s# dbl X) (mark# dbl X -> active# dbl mark X, active# dbl s X -> s# s dbl X) (mark# dbl X -> active# dbl mark X, active# dbl s X -> mark# s s dbl X) (mark# dbl X -> active# dbl mark X, active# add(0(), X) -> mark# X) (mark# dbl X -> active# dbl mark X, active# add(s X, Y) -> add#(X, Y)) (mark# dbl X -> active# dbl mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# dbl X -> active# dbl mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# dbl X -> active# dbl mark X, active# terms N -> s# N) (mark# dbl X -> active# dbl mark X, active# terms N -> terms# s N) (mark# dbl X -> active# dbl mark X, active# terms N -> sqr# N) (mark# dbl X -> active# dbl mark X, active# terms N -> recip# sqr N) (mark# dbl X -> active# dbl mark X, active# terms N -> cons#(recip sqr N, terms s N)) (mark# dbl X -> active# dbl mark X, active# terms N -> mark# cons(recip sqr N, terms s N)) (mark# dbl X -> active# dbl mark X, active# sqr 0() -> mark# 0()) (mark# dbl X -> active# dbl mark X, active# sqr s X -> dbl# X) (mark# dbl X -> active# dbl mark X, active# sqr s X -> add#(sqr X, dbl X)) (mark# dbl X -> active# dbl mark X, active# sqr s X -> s# add(sqr X, dbl X)) (mark# dbl X -> active# dbl mark X, active# sqr s X -> sqr# X) (mark# dbl X -> active# dbl mark X, active# sqr s X -> mark# s add(sqr X, dbl X)) (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> mark# X2) (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> mark# X1) (active# add(s X, Y) -> mark# s add(X, Y), mark# nil() -> active# nil()) (active# add(s X, Y) -> mark# s add(X, Y), mark# dbl X -> dbl# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# dbl X -> active# dbl mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# dbl X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X2) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X1) (active# add(s X, Y) -> mark# s add(X, Y), mark# 0() -> active# 0()) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s X) (active# add(s X, Y) -> mark# s add(X, Y), mark# terms X -> active# terms mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# terms X -> terms# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# terms X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# sqr X -> active# sqr mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# sqr X -> sqr# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# sqr X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# recip X -> active# recip mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# recip X -> recip# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# recip X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# cons(X1, X2) -> mark# X1) (active# dbl s X -> s# s dbl X, s# mark X -> s# X) (active# dbl s X -> s# s dbl X, s# active X -> s# X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# cons(X1, X2) -> mark# X1) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# recip X -> mark# X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# recip X -> recip# mark X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# recip X -> active# recip mark X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# sqr X -> mark# X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# sqr X -> sqr# mark X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# sqr X -> active# sqr mark X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# terms X -> mark# X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# terms X -> terms# mark X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# terms X -> active# terms mark X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# s X -> active# s X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# 0() -> active# 0()) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# add(X1, X2) -> mark# X1) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# add(X1, X2) -> mark# X2) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# dbl X -> mark# X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# dbl X -> active# dbl mark X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# dbl X -> dbl# mark X) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# nil() -> active# nil()) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# first(X1, X2) -> mark# X1) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# first(X1, X2) -> mark# X2) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# sqr s X -> mark# s add(sqr X, dbl X), mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# terms X -> active# terms mark X, active# sqr s X -> mark# s add(sqr X, dbl X)) (mark# terms X -> active# terms mark X, active# sqr s X -> sqr# X) (mark# terms X -> active# terms mark X, active# sqr s X -> s# add(sqr X, dbl X)) (mark# terms X -> active# terms mark X, active# sqr s X -> add#(sqr X, dbl X)) (mark# terms X -> active# terms mark X, active# sqr s X -> dbl# X) (mark# terms X -> active# terms mark X, active# sqr 0() -> mark# 0()) (mark# terms X -> active# terms mark X, active# terms N -> mark# cons(recip sqr N, terms s N)) (mark# terms X -> active# terms mark X, active# terms N -> cons#(recip sqr N, terms s N)) (mark# terms X -> active# terms mark X, active# terms N -> recip# sqr N) (mark# terms X -> active# terms mark X, active# terms N -> sqr# N) (mark# terms X -> active# terms mark X, active# terms N -> terms# s N) (mark# terms X -> active# terms mark X, active# terms N -> s# N) (mark# terms X -> active# terms mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# terms X -> active# terms mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# terms X -> active# terms mark X, active# add(s X, Y) -> add#(X, Y)) (mark# terms X -> active# terms mark X, active# add(0(), X) -> mark# X) (mark# terms X -> active# terms mark X, active# dbl s X -> mark# s s dbl X) (mark# terms X -> active# terms mark X, active# dbl s X -> s# s dbl X) (mark# terms X -> active# terms mark X, active# dbl s X -> s# dbl X) (mark# terms X -> active# terms mark X, active# dbl s X -> dbl# X) (mark# terms X -> active# terms mark X, active# dbl 0() -> mark# 0()) (mark# terms X -> active# terms mark X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# terms X -> active# terms mark X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# terms X -> active# terms mark X, active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# terms X -> active# terms mark X, active# first(0(), X) -> mark# nil()) (mark# recip X -> active# recip mark X, active# sqr s X -> mark# s add(sqr X, dbl X)) (mark# recip X -> active# recip mark X, active# sqr s X -> sqr# X) (mark# recip X -> active# recip mark X, active# sqr s X -> s# add(sqr X, dbl X)) (mark# recip X -> active# recip mark X, active# sqr s X -> add#(sqr X, dbl X)) (mark# recip X -> active# recip mark X, active# sqr s X -> dbl# X) (mark# recip X -> active# recip mark X, active# sqr 0() -> mark# 0()) (mark# recip X -> active# recip mark X, active# terms N -> mark# cons(recip sqr N, terms s N)) (mark# recip X -> active# recip mark X, active# terms N -> cons#(recip sqr N, terms s N)) (mark# recip X -> active# recip mark X, active# terms N -> recip# sqr N) (mark# recip X -> active# recip mark X, active# terms N -> sqr# N) (mark# recip X -> active# recip mark X, active# terms N -> terms# s N) (mark# recip X -> active# recip mark X, active# terms N -> s# N) (mark# recip X -> active# recip mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# recip X -> active# recip mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# recip X -> active# recip mark X, active# add(s X, Y) -> add#(X, Y)) (mark# recip X -> active# recip mark X, active# add(0(), X) -> mark# X) (mark# recip X -> active# recip mark X, active# dbl s X -> mark# s s dbl X) (mark# recip X -> active# recip mark X, active# dbl s X -> s# s dbl X) (mark# recip X -> active# recip mark X, active# dbl s X -> s# dbl X) (mark# recip X -> active# recip mark X, active# dbl s X -> dbl# X) (mark# recip X -> active# recip mark X, active# dbl 0() -> mark# 0()) (mark# recip X -> active# recip mark X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# recip X -> active# recip mark X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# recip X -> active# recip mark X, active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# recip X -> active# recip mark X, active# first(0(), X) -> mark# nil()) (active# terms N -> s# N, s# mark X -> s# X) (active# terms N -> s# N, s# active X -> s# X) (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# recip X -> recip# mark X) (mark# add(X1, X2) -> mark# X1, mark# recip X -> active# recip mark X) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> sqr# mark X) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> active# sqr mark X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> terms# mark X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> active# terms mark X) (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s X) (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> active# dbl mark X) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> dbl# mark X) (mark# add(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2)) (dbl# active X -> dbl# X, dbl# mark X -> dbl# X) (dbl# active X -> dbl# X, dbl# active X -> dbl# X) (active# dbl s X -> dbl# X, dbl# mark X -> dbl# X) (active# dbl s X -> dbl# X, dbl# active X -> dbl# X) (active# sqr s X -> dbl# X, dbl# mark X -> dbl# X) (active# sqr s X -> dbl# X, dbl# active X -> dbl# X) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (terms# active X -> terms# X, terms# mark X -> terms# X) (terms# active X -> terms# X, terms# active X -> terms# X) (sqr# active X -> sqr# X, sqr# mark X -> sqr# X) (sqr# active X -> sqr# X, sqr# active X -> sqr# X) (recip# active X -> recip# X, recip# mark X -> recip# X) (recip# active X -> recip# X, recip# active X -> recip# X) (mark# dbl X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# dbl X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# dbl X -> mark# X, mark# recip X -> mark# X) (mark# dbl X -> mark# X, mark# recip X -> recip# mark X) (mark# dbl X -> mark# X, mark# recip X -> active# recip mark X) (mark# dbl X -> mark# X, mark# sqr X -> mark# X) (mark# dbl X -> mark# X, mark# sqr X -> sqr# mark X) (mark# dbl X -> mark# X, mark# sqr X -> active# sqr mark X) (mark# dbl X -> mark# X, mark# terms X -> mark# X) (mark# dbl X -> mark# X, mark# terms X -> terms# mark X) (mark# dbl X -> mark# X, mark# terms X -> active# terms mark X) (mark# dbl X -> mark# X, mark# s X -> active# s X) (mark# dbl X -> mark# X, mark# 0() -> active# 0()) (mark# dbl X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# dbl X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# dbl X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> active# dbl mark X) (mark# dbl X -> mark# X, mark# dbl X -> dbl# mark X) (mark# dbl X -> mark# X, mark# nil() -> active# nil()) (mark# dbl X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# dbl X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# sqr X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# sqr X -> mark# X, mark# recip X -> mark# X) (mark# sqr X -> mark# X, mark# recip X -> recip# mark X) (mark# sqr X -> mark# X, mark# recip X -> active# recip mark X) (mark# sqr X -> mark# X, mark# sqr X -> mark# X) (mark# sqr X -> mark# X, mark# sqr X -> sqr# mark X) (mark# sqr X -> mark# X, mark# sqr X -> active# sqr mark X) (mark# sqr X -> mark# X, mark# terms X -> mark# X) (mark# sqr X -> mark# X, mark# terms X -> terms# mark X) (mark# sqr X -> mark# X, mark# terms X -> active# terms mark X) (mark# sqr X -> mark# X, mark# s X -> active# s X) (mark# sqr X -> mark# X, mark# 0() -> active# 0()) (mark# sqr X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# sqr X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# dbl X -> mark# X) (mark# sqr X -> mark# X, mark# dbl X -> active# dbl mark X) (mark# sqr X -> mark# X, mark# dbl X -> dbl# mark X) (mark# sqr X -> mark# X, mark# nil() -> active# nil()) (mark# sqr X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# sqr X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# recip X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# recip X -> recip# mark X) (mark# first(X1, X2) -> mark# X2, mark# recip X -> active# recip mark X) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> sqr# mark X) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> active# sqr mark X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> terms# mark X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> active# terms mark X) (mark# first(X1, X2) -> mark# X2, mark# s X -> active# s X) (mark# first(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> active# dbl mark X) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> dbl# mark X) (mark# first(X1, X2) -> mark# X2, mark# nil() -> active# nil()) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X2) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(X1, mark X2) -> cons#(X1, X2)) (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(X1, active X2) -> cons#(X1, X2)) (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(mark X1, X2) -> cons#(X1, X2)) (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(active X1, X2) -> cons#(X1, X2)) (first#(mark X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2)) (first#(mark X1, X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2)) (first#(mark X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2)) (first#(mark X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)) (first#(X1, mark X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2)) (first#(X1, mark X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2)) (first#(X1, mark X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2)) (first#(X1, mark X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (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)) (active# dbl 0() -> mark# 0(), mark# 0() -> active# 0()) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# cons(X1, X2) -> mark# X1) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# recip X -> mark# X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# recip X -> recip# mark X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# recip X -> active# recip mark X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# sqr X -> mark# X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# sqr X -> sqr# mark X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# sqr X -> active# sqr mark X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# terms X -> mark# X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# terms X -> terms# mark X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# terms X -> active# terms mark X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# s X -> active# s X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# 0() -> active# 0()) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# add(X1, X2) -> mark# X1) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# add(X1, X2) -> mark# X2) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# dbl X -> mark# X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# dbl X -> active# dbl mark X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# dbl X -> dbl# mark X) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# nil() -> active# nil()) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# first(X1, X2) -> mark# X1) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# first(X1, X2) -> mark# X2) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# terms N -> mark# cons(recip sqr N, terms s N), mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sqr s X -> mark# s add(sqr X, dbl X)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sqr s X -> sqr# X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sqr s X -> s# add(sqr X, dbl X)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sqr s X -> add#(sqr X, dbl X)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sqr s X -> dbl# X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sqr 0() -> mark# 0()) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# terms N -> mark# cons(recip sqr N, terms s N)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# terms N -> cons#(recip sqr N, terms s N)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# terms N -> recip# sqr N) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# terms N -> sqr# N) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# terms N -> terms# s N) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# terms N -> s# N) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(0(), X) -> mark# X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# dbl s X -> mark# s s dbl X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# dbl s X -> s# s dbl X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# dbl s X -> s# dbl X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# dbl s X -> dbl# X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# dbl 0() -> mark# 0()) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(0(), X) -> mark# nil()) (active# terms N -> terms# s N, terms# mark X -> terms# X) (active# terms N -> terms# s N, terms# active X -> terms# X) (active# dbl s X -> s# dbl X, s# mark X -> s# X) (active# dbl s X -> s# dbl X, s# active X -> s# X) (mark# s X -> active# s X, active# sqr s X -> mark# s add(sqr X, dbl X)) (mark# s X -> active# s X, active# sqr s X -> sqr# X) (mark# s X -> active# s X, active# sqr s X -> s# add(sqr X, dbl X)) (mark# s X -> active# s X, active# sqr s X -> add#(sqr X, dbl X)) (mark# s X -> active# s X, active# sqr s X -> dbl# X) (mark# s X -> active# s X, active# sqr 0() -> mark# 0()) (mark# s X -> active# s X, active# terms N -> mark# cons(recip sqr N, terms s N)) (mark# s X -> active# s X, active# terms N -> cons#(recip sqr N, terms s N)) (mark# s X -> active# s X, active# terms N -> recip# sqr N) (mark# s X -> active# s X, active# terms N -> sqr# N) (mark# s X -> active# s X, active# terms N -> terms# s N) (mark# s X -> active# s X, active# terms N -> s# N) (mark# s X -> active# s X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# s X -> active# s X, active# add(s X, Y) -> s# add(X, Y)) (mark# s X -> active# s X, active# add(s X, Y) -> add#(X, Y)) (mark# s X -> active# s X, active# add(0(), X) -> mark# X) (mark# s X -> active# s X, active# dbl s X -> mark# s s dbl X) (mark# s X -> active# s X, active# dbl s X -> s# s dbl X) (mark# s X -> active# s X, active# dbl s X -> s# dbl X) (mark# s X -> active# s X, active# dbl s X -> dbl# X) (mark# s X -> active# s X, active# dbl 0() -> mark# 0()) (mark# s X -> active# s X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# s X -> active# s X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# s X -> active# s X, active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# s X -> active# s X, active# first(0(), X) -> mark# nil()) (mark# sqr X -> sqr# mark X, sqr# mark X -> sqr# X) (mark# sqr X -> sqr# mark X, sqr# active X -> sqr# X) (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark X2) -> first#(X1, X2)) (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, active X2) -> first#(X1, X2)) (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(mark X1, X2) -> first#(X1, X2)) (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(active X1, X2) -> first#(X1, X2)) (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X) (active# add(s X, Y) -> s# add(X, Y), s# active X -> s# X) (active# terms N -> cons#(recip sqr N, terms s N), cons#(X1, mark X2) -> cons#(X1, X2)) (active# terms N -> cons#(recip sqr N, terms s N), cons#(X1, active X2) -> cons#(X1, X2)) (active# terms N -> cons#(recip sqr N, terms s N), cons#(mark X1, X2) -> cons#(X1, X2)) (active# terms N -> cons#(recip sqr N, terms s N), cons#(active X1, X2) -> cons#(X1, X2)) (active# sqr s X -> add#(sqr X, dbl X), add#(X1, mark X2) -> add#(X1, X2)) (active# sqr s X -> add#(sqr X, dbl X), add#(X1, active X2) -> add#(X1, X2)) (active# sqr s X -> add#(sqr X, dbl X), add#(mark X1, X2) -> add#(X1, X2)) (active# sqr s X -> add#(sqr X, dbl X), add#(active X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, active X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(mark X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, X2) -> add#(X1, X2)) } STATUS: arrows: 0.864327 SCCS (9): Scc: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# recip X -> mark# X, mark# recip X -> active# recip mark X, mark# sqr X -> mark# X, mark# sqr X -> active# sqr mark X, mark# terms X -> mark# X, mark# terms X -> active# terms mark X, mark# s X -> active# s X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2), mark# dbl X -> mark# X, mark# dbl X -> active# dbl mark X, mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sqr s X -> mark# s add(sqr X, dbl X), active# terms N -> mark# cons(recip sqr N, terms s N), active# add(s X, Y) -> mark# s add(X, Y), active# add(0(), X) -> mark# X, active# dbl s X -> mark# s s dbl X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))} Scc: { terms# mark X -> terms# X, terms# active X -> terms# X} Scc: { dbl# mark X -> dbl# X, dbl# active X -> dbl# X} Scc: { s# mark X -> s# X, s# active X -> s# X} Scc: { sqr# mark X -> sqr# X, sqr# active X -> sqr# X} Scc: { recip# mark X -> recip# X, recip# active X -> recip# X} Scc: { cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)} Scc: { first#(X1, mark X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)} Scc: { add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)} SCC (23): Strict: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# recip X -> mark# X, mark# recip X -> active# recip mark X, mark# sqr X -> mark# X, mark# sqr X -> active# sqr mark X, mark# terms X -> mark# X, mark# terms X -> active# terms mark X, mark# s X -> active# s X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2), mark# dbl X -> mark# X, mark# dbl X -> active# dbl mark X, mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sqr s X -> mark# s add(sqr X, dbl X), active# terms N -> mark# cons(recip sqr N, terms s N), active# add(s X, Y) -> mark# s add(X, Y), active# add(0(), X) -> mark# X, active# dbl s X -> mark# s s dbl X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} Open SCC (2): Strict: { terms# mark X -> terms# X, terms# active X -> terms# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} Open SCC (2): Strict: { dbl# mark X -> dbl# X, dbl# active X -> dbl# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} Open SCC (2): Strict: { s# mark X -> s# X, s# active X -> s# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} Open SCC (2): Strict: { sqr# mark X -> sqr# X, sqr# active X -> sqr# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} Open SCC (2): Strict: { recip# mark X -> recip# X, recip# active X -> recip# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} 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 cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} Open SCC (4): Strict: { first#(X1, mark X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} Open SCC (4): Strict: { add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark recip X -> active recip mark X, mark sqr X -> active sqr mark X, mark terms X -> active terms mark X, mark s X -> active s X, mark 0() -> active 0(), mark add(X1, X2) -> active add(mark X1, mark X2), mark dbl X -> active dbl mark X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), recip mark X -> recip X, recip active X -> recip X, sqr mark X -> sqr X, sqr active X -> sqr X, terms mark X -> terms X, terms active X -> terms X, s mark X -> s X, s active X -> s X, active sqr s X -> mark s add(sqr X, dbl X), active sqr 0() -> mark 0(), active terms N -> mark cons(recip sqr N, terms s N), active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, active dbl s X -> mark s s dbl X, active dbl 0() -> mark 0(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active first(0(), X) -> mark nil(), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), dbl mark X -> dbl X, dbl active X -> dbl X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2)} Open