YES Time: 0.111197 TRS: { a__sqr X -> sqr X, a__sqr s X -> s add(sqr X, dbl X), a__sqr 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark recip X -> recip mark X, mark terms X -> a__terms mark X, mark s X -> s X, mark 0() -> 0(), mark add(X1, X2) -> a__add(mark X1, mark X2), mark sqr X -> a__sqr mark X, mark dbl X -> a__dbl mark X, mark nil() -> nil(), mark first(X1, X2) -> a__first(mark X1, mark X2), a__terms N -> cons(recip a__sqr mark N, terms s N), a__terms X -> terms X, a__dbl X -> dbl X, a__dbl s X -> s s dbl X, a__dbl 0() -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s X, Y) -> s add(X, Y), a__add(0(), X) -> mark X, a__first(X1, X2) -> first(X1, X2), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), a__first(0(), X) -> nil()} DP: DP: { mark# cons(X1, X2) -> mark# X1, mark# recip X -> mark# X, mark# terms X -> mark# X, mark# terms X -> a__terms# mark X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2), mark# sqr X -> a__sqr# mark X, mark# sqr X -> mark# X, mark# dbl X -> mark# X, mark# dbl X -> a__dbl# mark X, mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2), a__terms# N -> a__sqr# mark N, a__terms# N -> mark# N, a__add#(0(), X) -> mark# X, a__first#(s X, cons(Y, Z)) -> mark# Y} TRS: { a__sqr X -> sqr X, a__sqr s X -> s add(sqr X, dbl X), a__sqr 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark recip X -> recip mark X, mark terms X -> a__terms mark X, mark s X -> s X, mark 0() -> 0(), mark add(X1, X2) -> a__add(mark X1, mark X2), mark sqr X -> a__sqr mark X, mark dbl X -> a__dbl mark X, mark nil() -> nil(), mark first(X1, X2) -> a__first(mark X1, mark X2), a__terms N -> cons(recip a__sqr mark N, terms s N), a__terms X -> terms X, a__dbl X -> dbl X, a__dbl s X -> s s dbl X, a__dbl 0() -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s X, Y) -> s add(X, Y), a__add(0(), X) -> mark X, a__first(X1, X2) -> first(X1, X2), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), a__first(0(), X) -> nil()} UR: { a__sqr X -> sqr X, a__sqr s X -> s add(sqr X, dbl X), a__sqr 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark recip X -> recip mark X, mark terms X -> a__terms mark X, mark s X -> s X, mark 0() -> 0(), mark add(X1, X2) -> a__add(mark X1, mark X2), mark sqr X -> a__sqr mark X, mark dbl X -> a__dbl mark X, mark nil() -> nil(), mark first(X1, X2) -> a__first(mark X1, mark X2), a__terms N -> cons(recip a__sqr mark N, terms s N), a__terms X -> terms X, a__dbl X -> dbl X, a__dbl s X -> s s dbl X, a__dbl 0() -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s X, Y) -> s add(X, Y), a__add(0(), X) -> mark X, a__first(X1, X2) -> first(X1, X2), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), a__first(0(), X) -> nil(), a(x, y) -> x, a(x, y) -> y} EDG: { (mark# terms X -> a__terms# mark X, a__terms# N -> mark# N) (mark# terms X -> a__terms# mark X, a__terms# N -> a__sqr# mark N) (mark# recip X -> mark# X, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# recip X -> mark# X, mark# dbl X -> mark# X) (mark# recip X -> mark# X, mark# sqr X -> mark# X) (mark# recip X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# recip X -> mark# X, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# recip X -> mark# X, mark# terms X -> mark# X) (mark# recip X -> mark# X, mark# recip X -> mark# X) (mark# recip X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# sqr X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# dbl X -> a__dbl# mark X) (mark# sqr X -> mark# X, mark# dbl X -> mark# X) (mark# sqr X -> mark# X, mark# sqr X -> mark# X) (mark# sqr X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# sqr X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# sqr X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# terms X -> a__terms# mark X) (mark# sqr X -> mark# X, mark# terms X -> mark# X) (mark# sqr X -> mark# X, mark# recip X -> mark# X) (mark# sqr X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# dbl X -> a__dbl# mark X) (a__add#(0(), X) -> mark# X, mark# dbl X -> mark# X) (a__add#(0(), X) -> mark# X, mark# sqr X -> mark# X) (a__add#(0(), X) -> mark# X, mark# sqr X -> a__sqr# mark X) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# terms X -> a__terms# mark X) (a__add#(0(), X) -> mark# X, mark# terms X -> mark# X) (a__add#(0(), X) -> mark# X, mark# recip X -> mark# X) (a__add#(0(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> a__first#(mark X1, mark X2), a__first#(s X, cons(Y, Z)) -> mark# Y) (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# add(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> a__sqr# mark X) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# add(X1, X2) -> mark# X2, mark# terms X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# recip X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# cons(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# cons(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# first(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# first(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# recip X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> a__sqr# mark X) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (a__terms# N -> mark# N, mark# cons(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# recip X -> mark# X) (a__terms# N -> mark# N, mark# terms X -> mark# X) (a__terms# N -> mark# N, mark# terms X -> a__terms# mark X) (a__terms# N -> mark# N, mark# add(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# add(X1, X2) -> mark# X2) (a__terms# N -> mark# N, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__terms# N -> mark# N, mark# sqr X -> a__sqr# mark X) (a__terms# N -> mark# N, mark# sqr X -> mark# X) (a__terms# N -> mark# N, mark# dbl X -> mark# X) (a__terms# N -> mark# N, mark# dbl X -> a__dbl# mark X) (a__terms# N -> mark# N, mark# first(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# first(X1, X2) -> mark# X2) (a__terms# N -> mark# N, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# add(X1, X2) -> a__add#(mark X1, mark X2), a__add#(0(), X) -> mark# X) (mark# dbl X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# recip X -> mark# X) (mark# dbl X -> mark# X, mark# terms X -> mark# X) (mark# dbl X -> mark# X, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# dbl X -> mark# X, mark# sqr X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (mark# terms X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# recip X -> mark# X) (mark# terms X -> mark# X, mark# terms X -> mark# X) (mark# terms X -> mark# X, mark# terms X -> a__terms# mark X) (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# terms X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# terms X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# terms X -> mark# X, mark# sqr X -> mark# X) (mark# terms X -> mark# X, mark# dbl X -> mark# X) (mark# terms X -> mark# X, mark# dbl X -> a__dbl# mark X) (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# terms X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# recip X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# terms X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# terms X -> a__terms# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X2) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# sqr X -> a__sqr# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# sqr X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# dbl X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# dbl X -> a__dbl# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X2) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) } EDG: { (mark# terms X -> a__terms# mark X, a__terms# N -> mark# N) (mark# terms X -> a__terms# mark X, a__terms# N -> a__sqr# mark N) (mark# recip X -> mark# X, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# recip X -> mark# X, mark# dbl X -> mark# X) (mark# recip X -> mark# X, mark# sqr X -> mark# X) (mark# recip X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# recip X -> mark# X, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# recip X -> mark# X, mark# terms X -> mark# X) (mark# recip X -> mark# X, mark# recip X -> mark# X) (mark# recip X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# sqr X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# dbl X -> a__dbl# mark X) (mark# sqr X -> mark# X, mark# dbl X -> mark# X) (mark# sqr X -> mark# X, mark# sqr X -> mark# X) (mark# sqr X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# sqr X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# sqr X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# terms X -> a__terms# mark X) (mark# sqr X -> mark# X, mark# terms X -> mark# X) (mark# sqr X -> mark# X, mark# recip X -> mark# X) (mark# sqr X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# dbl X -> a__dbl# mark X) (a__add#(0(), X) -> mark# X, mark# dbl X -> mark# X) (a__add#(0(), X) -> mark# X, mark# sqr X -> mark# X) (a__add#(0(), X) -> mark# X, mark# sqr X -> a__sqr# mark X) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# terms X -> a__terms# mark X) (a__add#(0(), X) -> mark# X, mark# terms X -> mark# X) (a__add#(0(), X) -> mark# X, mark# recip X -> mark# X) (a__add#(0(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> a__first#(mark X1, mark X2), a__first#(s X, cons(Y, Z)) -> mark# Y) (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# add(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> a__sqr# mark X) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# add(X1, X2) -> mark# X2, mark# terms X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# recip X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# cons(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# cons(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# first(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# first(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# recip X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> a__sqr# mark X) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (a__terms# N -> mark# N, mark# cons(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# recip X -> mark# X) (a__terms# N -> mark# N, mark# terms X -> mark# X) (a__terms# N -> mark# N, mark# terms X -> a__terms# mark X) (a__terms# N -> mark# N, mark# add(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# add(X1, X2) -> mark# X2) (a__terms# N -> mark# N, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__terms# N -> mark# N, mark# sqr X -> a__sqr# mark X) (a__terms# N -> mark# N, mark# sqr X -> mark# X) (a__terms# N -> mark# N, mark# dbl X -> mark# X) (a__terms# N -> mark# N, mark# dbl X -> a__dbl# mark X) (a__terms# N -> mark# N, mark# first(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# first(X1, X2) -> mark# X2) (a__terms# N -> mark# N, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# add(X1, X2) -> a__add#(mark X1, mark X2), a__add#(0(), X) -> mark# X) (mark# dbl X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# recip X -> mark# X) (mark# dbl X -> mark# X, mark# terms X -> mark# X) (mark# dbl X -> mark# X, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# dbl X -> mark# X, mark# sqr X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (mark# terms X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# recip X -> mark# X) (mark# terms X -> mark# X, mark# terms X -> mark# X) (mark# terms X -> mark# X, mark# terms X -> a__terms# mark X) (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# terms X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# terms X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# terms X -> mark# X, mark# sqr X -> mark# X) (mark# terms X -> mark# X, mark# dbl X -> mark# X) (mark# terms X -> mark# X, mark# dbl X -> a__dbl# mark X) (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# terms X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# recip X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# terms X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# terms X -> a__terms# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X2) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# sqr X -> a__sqr# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# sqr X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# dbl X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# dbl X -> a__dbl# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X2) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) } EDG: { (mark# terms X -> a__terms# mark X, a__terms# N -> mark# N) (mark# terms X -> a__terms# mark X, a__terms# N -> a__sqr# mark N) (mark# recip X -> mark# X, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# recip X -> mark# X, mark# dbl X -> mark# X) (mark# recip X -> mark# X, mark# sqr X -> mark# X) (mark# recip X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# recip X -> mark# X, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# recip X -> mark# X, mark# terms X -> mark# X) (mark# recip X -> mark# X, mark# recip X -> mark# X) (mark# recip X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# sqr X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# dbl X -> a__dbl# mark X) (mark# sqr X -> mark# X, mark# dbl X -> mark# X) (mark# sqr X -> mark# X, mark# sqr X -> mark# X) (mark# sqr X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# sqr X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# sqr X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# terms X -> a__terms# mark X) (mark# sqr X -> mark# X, mark# terms X -> mark# X) (mark# sqr X -> mark# X, mark# recip X -> mark# X) (mark# sqr X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# dbl X -> a__dbl# mark X) (a__add#(0(), X) -> mark# X, mark# dbl X -> mark# X) (a__add#(0(), X) -> mark# X, mark# sqr X -> mark# X) (a__add#(0(), X) -> mark# X, mark# sqr X -> a__sqr# mark X) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# terms X -> a__terms# mark X) (a__add#(0(), X) -> mark# X, mark# terms X -> mark# X) (a__add#(0(), X) -> mark# X, mark# recip X -> mark# X) (a__add#(0(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> a__first#(mark X1, mark X2), a__first#(s X, cons(Y, Z)) -> mark# Y) (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# add(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> a__sqr# mark X) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# add(X1, X2) -> mark# X2, mark# terms X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# recip X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# cons(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# cons(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# first(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# first(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# recip X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> a__sqr# mark X) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (a__terms# N -> mark# N, mark# cons(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# recip X -> mark# X) (a__terms# N -> mark# N, mark# terms X -> mark# X) (a__terms# N -> mark# N, mark# terms X -> a__terms# mark X) (a__terms# N -> mark# N, mark# add(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# add(X1, X2) -> mark# X2) (a__terms# N -> mark# N, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__terms# N -> mark# N, mark# sqr X -> a__sqr# mark X) (a__terms# N -> mark# N, mark# sqr X -> mark# X) (a__terms# N -> mark# N, mark# dbl X -> mark# X) (a__terms# N -> mark# N, mark# dbl X -> a__dbl# mark X) (a__terms# N -> mark# N, mark# first(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# first(X1, X2) -> mark# X2) (a__terms# N -> mark# N, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# add(X1, X2) -> a__add#(mark X1, mark X2), a__add#(0(), X) -> mark# X) (mark# dbl X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# recip X -> mark# X) (mark# dbl X -> mark# X, mark# terms X -> mark# X) (mark# dbl X -> mark# X, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# dbl X -> mark# X, mark# sqr X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (mark# terms X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# recip X -> mark# X) (mark# terms X -> mark# X, mark# terms X -> mark# X) (mark# terms X -> mark# X, mark# terms X -> a__terms# mark X) (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# terms X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# terms X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# terms X -> mark# X, mark# sqr X -> mark# X) (mark# terms X -> mark# X, mark# dbl X -> mark# X) (mark# terms X -> mark# X, mark# dbl X -> a__dbl# mark X) (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# terms X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# recip X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# terms X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# terms X -> a__terms# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X2) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# sqr X -> a__sqr# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# sqr X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# dbl X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# dbl X -> a__dbl# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X2) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) } EDG: { (mark# terms X -> a__terms# mark X, a__terms# N -> mark# N) (mark# terms X -> a__terms# mark X, a__terms# N -> a__sqr# mark N) (mark# recip X -> mark# X, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# recip X -> mark# X, mark# dbl X -> mark# X) (mark# recip X -> mark# X, mark# sqr X -> mark# X) (mark# recip X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# recip X -> mark# X, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# recip X -> mark# X, mark# terms X -> mark# X) (mark# recip X -> mark# X, mark# recip X -> mark# X) (mark# recip X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# sqr X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# dbl X -> a__dbl# mark X) (mark# sqr X -> mark# X, mark# dbl X -> mark# X) (mark# sqr X -> mark# X, mark# sqr X -> mark# X) (mark# sqr X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# sqr X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# sqr X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# sqr X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# sqr X -> mark# X, mark# terms X -> a__terms# mark X) (mark# sqr X -> mark# X, mark# terms X -> mark# X) (mark# sqr X -> mark# X, mark# recip X -> mark# X) (mark# sqr X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# dbl X -> a__dbl# mark X) (a__add#(0(), X) -> mark# X, mark# dbl X -> mark# X) (a__add#(0(), X) -> mark# X, mark# sqr X -> mark# X) (a__add#(0(), X) -> mark# X, mark# sqr X -> a__sqr# mark X) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# terms X -> a__terms# mark X) (a__add#(0(), X) -> mark# X, mark# terms X -> mark# X) (a__add#(0(), X) -> mark# X, mark# recip X -> mark# X) (a__add#(0(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> a__first#(mark X1, mark X2), a__first#(s X, cons(Y, Z)) -> mark# Y) (mark# add(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# add(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# sqr X -> a__sqr# mark X) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# add(X1, X2) -> mark# X2, mark# terms X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# recip X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# cons(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# cons(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__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# dbl X -> a__dbl# mark X) (mark# first(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__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# terms X -> a__terms# mark X) (mark# first(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# recip X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> a__sqr# mark X) (mark# add(X1, X2) -> mark# X1, mark# sqr X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# recip X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> a__sqr# mark X) (mark# first(X1, X2) -> mark# X2, mark# sqr X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (a__terms# N -> mark# N, mark# cons(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# recip X -> mark# X) (a__terms# N -> mark# N, mark# terms X -> mark# X) (a__terms# N -> mark# N, mark# terms X -> a__terms# mark X) (a__terms# N -> mark# N, mark# add(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# add(X1, X2) -> mark# X2) (a__terms# N -> mark# N, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__terms# N -> mark# N, mark# sqr X -> a__sqr# mark X) (a__terms# N -> mark# N, mark# sqr X -> mark# X) (a__terms# N -> mark# N, mark# dbl X -> mark# X) (a__terms# N -> mark# N, mark# dbl X -> a__dbl# mark X) (a__terms# N -> mark# N, mark# first(X1, X2) -> mark# X1) (a__terms# N -> mark# N, mark# first(X1, X2) -> mark# X2) (a__terms# N -> mark# N, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# add(X1, X2) -> a__add#(mark X1, mark X2), a__add#(0(), X) -> mark# X) (mark# dbl X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# recip X -> mark# X) (mark# dbl X -> mark# X, mark# terms X -> mark# X) (mark# dbl X -> mark# X, mark# terms X -> a__terms# mark X) (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) -> a__add#(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# dbl X -> mark# X, mark# sqr X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> a__dbl# mark X) (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) -> a__first#(mark X1, mark X2)) (mark# terms X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# recip X -> mark# X) (mark# terms X -> mark# X, mark# terms X -> mark# X) (mark# terms X -> mark# X, mark# terms X -> a__terms# mark X) (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# terms X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# terms X -> mark# X, mark# sqr X -> a__sqr# mark X) (mark# terms X -> mark# X, mark# sqr X -> mark# X) (mark# terms X -> mark# X, mark# dbl X -> mark# X) (mark# terms X -> mark# X, mark# dbl X -> a__dbl# mark X) (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# terms X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# terms X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# recip X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# terms X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# terms X -> a__terms# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X2) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# sqr X -> a__sqr# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# sqr X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# dbl X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# dbl X -> a__dbl# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X2) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) } STATUS: arrows: 0.469136 SCCS (1): Scc: { mark# cons(X1, X2) -> mark# X1, mark# recip X -> mark# X, mark# terms X -> mark# X, mark# terms X -> a__terms# mark X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2), mark# sqr X -> mark# X, mark# dbl X -> mark# X, mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2), a__terms# N -> mark# N, a__add#(0(), X) -> mark# X, a__first#(s X, cons(Y, Z)) -> mark# Y} SCC (15): Strict: { mark# cons(X1, X2) -> mark# X1, mark# recip X -> mark# X, mark# terms X -> mark# X, mark# terms X -> a__terms# mark X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2), mark# sqr X -> mark# X, mark# dbl X -> mark# X, mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2), a__terms# N -> mark# N, a__add#(0(), X) -> mark# X, a__first#(s X, cons(Y, Z)) -> mark# Y} Weak: { a__sqr X -> sqr X, a__sqr s X -> s add(sqr X, dbl X), a__sqr 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark recip X -> recip mark X, mark terms X -> a__terms mark X, mark s X -> s X, mark 0() -> 0(), mark add(X1, X2) -> a__add(mark X1, mark X2), mark sqr X -> a__sqr mark X, mark dbl X -> a__dbl mark X, mark nil() -> nil(), mark first(X1, X2) -> a__first(mark X1, mark X2), a__terms N -> cons(recip a__sqr mark N, terms s N), a__terms X -> terms X, a__dbl X -> dbl X, a__dbl s X -> s s dbl X, a__dbl 0() -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s X, Y) -> s add(X, Y), a__add(0(), X) -> mark X, a__first(X1, X2) -> first(X1, X2), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), a__first(0(), X) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [add](x0, x1) = x0 + x1, [a__add](x0, x1) = x0 + x1, [a__first](x0, x1) = x0 + x1 + 1, [first](x0, x1) = x0 + x1 + 1, [recip](x0) = x0, [a__sqr](x0) = x0, [mark](x0) = x0, [terms](x0) = x0 + 1, [s](x0) = 1, [a__terms](x0) = x0 + 1, [sqr](x0) = x0, [dbl](x0) = x0 + 1, [a__dbl](x0) = x0 + 1, [0] = 0, [nil] = 0, [a__add#](x0, x1) = x0 + 1, [a__first#](x0, x1) = x0 + x1 + 1, [mark#](x0) = x0 + 1, [a__terms#](x0) = x0 + 1 Strict: a__first#(s X, cons(Y, Z)) -> mark# Y 3 + 0X + 1Y + 0Z >= 1 + 1Y a__add#(0(), X) -> mark# X 1 + 1X >= 1 + 1X a__terms# N -> mark# N 1 + 1N >= 1 + 1N mark# first(X1, X2) -> a__first#(mark X1, mark X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark# first(X1, X2) -> mark# X2 2 + 1X1 + 1X2 >= 1 + 1X2 mark# first(X1, X2) -> mark# X1 2 + 1X1 + 1X2 >= 1 + 1X1 mark# dbl X -> mark# X 2 + 1X >= 1 + 1X mark# sqr X -> mark# X 1 + 1X >= 1 + 1X mark# add(X1, X2) -> a__add#(mark X1, mark X2) 1 + 1X1 + 1X2 >= 1 + 0X1 + 1X2 mark# add(X1, X2) -> mark# X2 1 + 1X1 + 1X2 >= 1 + 1X2 mark# add(X1, X2) -> mark# X1 1 + 1X1 + 1X2 >= 1 + 1X1 mark# terms X -> a__terms# mark X 2 + 1X >= 1 + 1X mark# terms X -> mark# X 2 + 1X >= 1 + 1X mark# recip X -> mark# X 1 + 1X >= 1 + 1X mark# cons(X1, X2) -> mark# X1 2 + 1X1 + 0X2 >= 1 + 1X1 Weak: a__first(0(), X) -> nil() 1 + 1X >= 0 a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)) 3 + 0X + 1Y + 0Z >= 1 + 0X + 1Y + 0Z a__first(X1, X2) -> first(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 a__add(0(), X) -> mark X 0 + 1X >= 0 + 1X a__add(s X, Y) -> s add(X, Y) 1 + 0X + 1Y >= 1 + 0X + 0Y a__add(X1, X2) -> add(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 a__dbl 0() -> 0() 1 >= 0 a__dbl s X -> s s dbl X 2 + 0X >= 1 + 0X a__dbl X -> dbl X 1 + 1X >= 1 + 1X a__terms X -> terms X 1 + 1X >= 1 + 1X a__terms N -> cons(recip a__sqr mark N, terms s N) 1 + 1N >= 1 + 1N mark first(X1, X2) -> a__first(mark X1, mark X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark nil() -> nil() 0 >= 0 mark dbl X -> a__dbl mark X 1 + 1X >= 1 + 1X mark sqr X -> a__sqr mark X 0 + 1X >= 0 + 1X mark add(X1, X2) -> a__add(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark 0() -> 0() 0 >= 0 mark s X -> s X 1 + 0X >= 1 + 0X mark terms X -> a__terms mark X 1 + 1X >= 1 + 1X mark recip X -> recip mark X 0 + 1X >= 0 + 1X mark cons(X1, X2) -> cons(mark X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 a__sqr 0() -> 0() 0 >= 0 a__sqr s X -> s add(sqr X, dbl X) 1 + 0X >= 1 + 0X a__sqr X -> sqr X 0 + 1X >= 0 + 1X SCCS (1): Scc: { mark# recip X -> mark# X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2), mark# sqr X -> mark# X, a__add#(0(), X) -> mark# X} SCC (6): Strict: { mark# recip X -> mark# X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2), mark# sqr X -> mark# X, a__add#(0(), X) -> mark# X} Weak: { a__sqr X -> sqr X, a__sqr s X -> s add(sqr X, dbl X), a__sqr 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark recip X -> recip mark X, mark terms X -> a__terms mark X, mark s X -> s X, mark 0() -> 0(), mark add(X1, X2) -> a__add(mark X1, mark X2), mark sqr X -> a__sqr mark X, mark dbl X -> a__dbl mark X, mark nil() -> nil(), mark first(X1, X2) -> a__first(mark X1, mark X2), a__terms N -> cons(recip a__sqr mark N, terms s N), a__terms X -> terms X, a__dbl X -> dbl X, a__dbl s X -> s s dbl X, a__dbl 0() -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s X, Y) -> s add(X, Y), a__add(0(), X) -> mark X, a__first(X1, X2) -> first(X1, X2), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), a__first(0(), X) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [add](x0, x1) = x0 + x1 + 1, [a__add](x0, x1) = x0 + x1 + 1, [a__first](x0, x1) = 0, [first](x0, x1) = 0, [recip](x0) = x0, [a__sqr](x0) = x0, [mark](x0) = x0, [terms](x0) = 0, [s](x0) = 0, [a__terms](x0) = 0, [sqr](x0) = x0, [dbl](x0) = x0 + 1, [a__dbl](x0) = x0 + 1, [0] = 1, [nil] = 0, [a__add#](x0, x1) = x0 + x1, [mark#](x0) = x0 Strict: a__add#(0(), X) -> mark# X 1 + 1X >= 0 + 1X mark# sqr X -> mark# X 0 + 1X >= 0 + 1X mark# add(X1, X2) -> a__add#(mark X1, mark X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark# add(X1, X2) -> mark# X2 1 + 1X1 + 1X2 >= 0 + 1X2 mark# add(X1, X2) -> mark# X1 1 + 1X1 + 1X2 >= 0 + 1X1 mark# recip X -> mark# X 0 + 1X >= 0 + 1X Weak: a__first(0(), X) -> nil() 0 + 0X >= 0 a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z a__first(X1, X2) -> first(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 a__add(0(), X) -> mark X 2 + 1X >= 0 + 1X a__add(s X, Y) -> s add(X, Y) 1 + 0X + 1Y >= 0 + 0X + 0Y a__add(X1, X2) -> add(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 a__dbl 0() -> 0() 2 >= 1 a__dbl s X -> s s dbl X 1 + 0X >= 0 + 0X a__dbl X -> dbl X 1 + 1X >= 1 + 1X a__terms X -> terms X 0 + 0X >= 0 + 0X a__terms N -> cons(recip a__sqr mark N, terms s N) 0 + 0N >= 0 + 0N mark first(X1, X2) -> a__first(mark X1, mark X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark nil() -> nil() 0 >= 0 mark dbl X -> a__dbl mark X 1 + 1X >= 1 + 1X mark sqr X -> a__sqr mark X 0 + 1X >= 0 + 1X mark add(X1, X2) -> a__add(mark X1, mark X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark 0() -> 0() 1 >= 1 mark s X -> s X 0 + 0X >= 0 + 0X mark terms X -> a__terms mark X 0 + 0X >= 0 + 0X mark recip X -> recip mark X 0 + 1X >= 0 + 1X mark cons(X1, X2) -> cons(mark X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 a__sqr 0() -> 0() 1 >= 1 a__sqr s X -> s add(sqr X, dbl X) 0 + 0X >= 0 + 0X a__sqr X -> sqr X 0 + 1X >= 0 + 1X SCCS (1): Scc: {mark# recip X -> mark# X, mark# sqr X -> mark# X} SCC (2): Strict: {mark# recip X -> mark# X, mark# sqr X -> mark# X} Weak: { a__sqr X -> sqr X, a__sqr s X -> s add(sqr X, dbl X), a__sqr 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark recip X -> recip mark X, mark terms X -> a__terms mark X, mark s X -> s X, mark 0() -> 0(), mark add(X1, X2) -> a__add(mark X1, mark X2), mark sqr X -> a__sqr mark X, mark dbl X -> a__dbl mark X, mark nil() -> nil(), mark first(X1, X2) -> a__first(mark X1, mark X2), a__terms N -> cons(recip a__sqr mark N, terms s N), a__terms X -> terms X, a__dbl X -> dbl X, a__dbl s X -> s s dbl X, a__dbl 0() -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s X, Y) -> s add(X, Y), a__add(0(), X) -> mark X, a__first(X1, X2) -> first(X1, X2), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), a__first(0(), X) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 1, [add](x0, x1) = x0 + 1, [a__add](x0, x1) = 0, [a__first](x0, x1) = 0, [first](x0, x1) = 1, [recip](x0) = x0, [a__sqr](x0) = x0 + 1, [mark](x0) = x0 + 1, [terms](x0) = 1, [s](x0) = x0 + 1, [a__terms](x0) = x0 + 1, [sqr](x0) = x0 + 1, [dbl](x0) = 1, [a__dbl](x0) = x0 + 1, [0] = 1, [nil] = 1, [mark#](x0) = x0 Strict: mark# sqr X -> mark# X 1 + 1X >= 0 + 1X mark# recip X -> mark# X 0 + 1X >= 0 + 1X Weak: a__first(0(), X) -> nil() 0 + 0X >= 1 a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)) 0 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z a__first(X1, X2) -> first(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 a__add(0(), X) -> mark X 0 + 0X >= 1 + 1X a__add(s X, Y) -> s add(X, Y) 0 + 0X + 0Y >= 2 + 0X + 1Y a__add(X1, X2) -> add(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 a__dbl 0() -> 0() 2 >= 1 a__dbl s X -> s s dbl X 2 + 1X >= 3 + 0X a__dbl X -> dbl X 1 + 1X >= 1 + 0X a__terms X -> terms X 1 + 1X >= 1 + 0X a__terms N -> cons(recip a__sqr mark N, terms s N) 1 + 1N >= 1 + 0N mark first(X1, X2) -> a__first(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark nil() -> nil() 2 >= 1 mark dbl X -> a__dbl mark X 2 + 0X >= 2 + 1X mark sqr X -> a__sqr mark X 2 + 1X >= 2 + 1X mark add(X1, X2) -> a__add(mark X1, mark X2) 2 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 mark 0() -> 0() 2 >= 1 mark s X -> s X 2 + 1X >= 1 + 1X mark terms X -> a__terms mark X 2 + 0X >= 2 + 1X mark recip X -> recip mark X 1 + 1X >= 1 + 1X mark cons(X1, X2) -> cons(mark X1, X2) 2 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 a__sqr 0() -> 0() 2 >= 1 a__sqr s X -> s add(sqr X, dbl X) 2 + 1X >= 3 + 0X a__sqr X -> sqr X 1 + 1X >= 1 + 1X SCCS (1): Scc: {mark# recip X -> mark# X} SCC (1): Strict: {mark# recip X -> mark# X} Weak: { a__sqr X -> sqr X, a__sqr s X -> s add(sqr X, dbl X), a__sqr 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark recip X -> recip mark X, mark terms X -> a__terms mark X, mark s X -> s X, mark 0() -> 0(), mark add(X1, X2) -> a__add(mark X1, mark X2), mark sqr X -> a__sqr mark X, mark dbl X -> a__dbl mark X, mark nil() -> nil(), mark first(X1, X2) -> a__first(mark X1, mark X2), a__terms N -> cons(recip a__sqr mark N, terms s N), a__terms X -> terms X, a__dbl X -> dbl X, a__dbl s X -> s s dbl X, a__dbl 0() -> 0(), a__add(X1, X2) -> add(X1, X2), a__add(s X, Y) -> s add(X, Y), a__add(0(), X) -> mark X, a__first(X1, X2) -> first(X1, X2), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), a__first(0(), X) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 1, [add](x0, x1) = 1, [a__add](x0, x1) = 0, [a__first](x0, x1) = 0, [first](x0, x1) = 1, [recip](x0) = x0 + 1, [a__sqr](x0) = x0 + 1, [mark](x0) = x0 + 1, [terms](x0) = 1, [s](x0) = x0 + 1, [a__terms](x0) = x0 + 1, [sqr](x0) = 1, [dbl](x0) = 1, [a__dbl](x0) = x0 + 1, [0] = 1, [nil] = 1, [mark#](x0) = x0 Strict: mark# recip X -> mark# X 1 + 1X >= 0 + 1X Weak: a__first(0(), X) -> nil() 0 + 0X >= 1 a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)) 0 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z a__first(X1, X2) -> first(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 a__add(0(), X) -> mark X 0 + 0X >= 1 + 1X a__add(s X, Y) -> s add(X, Y) 0 + 0X + 0Y >= 2 + 0X + 0Y a__add(X1, X2) -> add(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 a__dbl 0() -> 0() 2 >= 1 a__dbl s X -> s s dbl X 2 + 1X >= 3 + 0X a__dbl X -> dbl X 1 + 1X >= 1 + 0X a__terms X -> terms X 1 + 1X >= 1 + 0X a__terms N -> cons(recip a__sqr mark N, terms s N) 1 + 1N >= 1 + 0N mark first(X1, X2) -> a__first(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark nil() -> nil() 2 >= 1 mark dbl X -> a__dbl mark X 2 + 0X >= 2 + 1X mark sqr X -> a__sqr mark X 2 + 0X >= 2 + 1X mark add(X1, X2) -> a__add(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark 0() -> 0() 2 >= 1 mark s X -> s X 2 + 1X >= 1 + 1X mark terms X -> a__terms mark X 2 + 0X >= 2 + 1X mark recip X -> recip mark X 2 + 1X >= 2 + 1X mark cons(X1, X2) -> cons(mark X1, X2) 2 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 a__sqr 0() -> 0() 2 >= 1 a__sqr s X -> s add(sqr X, dbl X) 2 + 1X >= 2 + 0X a__sqr X -> sqr X 1 + 1X >= 1 + 0X Qed