YES Time: 1.982231 TRS: { sqr 0() -> 0(), sqr s X -> s add(sqr X, dbl X), terms N -> cons(recip sqr N, n__terms n__s N), terms X -> n__terms X, s X -> n__s X, add(0(), X) -> X, add(s X, Y) -> s add(X, Y), dbl 0() -> 0(), dbl s X -> s s dbl X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__terms X -> terms activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2)} DP: DP: { sqr# s X -> sqr# X, sqr# s X -> s# add(sqr X, dbl X), sqr# s X -> add#(sqr X, dbl X), sqr# s X -> dbl# X, terms# N -> sqr# N, add#(s X, Y) -> s# add(X, Y), add#(s X, Y) -> add#(X, Y), dbl# s X -> s# s dbl X, dbl# s X -> s# dbl X, dbl# s X -> dbl# X, first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> terms# activate X, activate# n__terms X -> activate# X, activate# n__s X -> s# activate X, activate# n__s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} TRS: { sqr 0() -> 0(), sqr s X -> s add(sqr X, dbl X), terms N -> cons(recip sqr N, n__terms n__s N), terms X -> n__terms X, s X -> n__s X, add(0(), X) -> X, add(s X, Y) -> s add(X, Y), dbl 0() -> 0(), dbl s X -> s s dbl X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__terms X -> terms activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2)} EDG: {(sqr# s X -> dbl# X, dbl# s X -> dbl# X) (sqr# s X -> dbl# X, dbl# s X -> s# dbl X) (sqr# s X -> dbl# X, dbl# s X -> s# s dbl X) (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> activate# X2) (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> activate# X1) (activate# n__terms X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (activate# n__terms X -> activate# X, activate# n__s X -> activate# X) (activate# n__terms X -> activate# X, activate# n__s X -> s# activate X) (activate# n__terms X -> activate# X, activate# n__terms X -> activate# X) (activate# n__terms X -> activate# X, activate# n__terms X -> terms# activate X) (sqr# s X -> add#(sqr X, dbl X), add#(s X, Y) -> add#(X, Y)) (sqr# s X -> add#(sqr X, dbl X), add#(s X, Y) -> s# add(X, Y)) (terms# N -> sqr# N, sqr# s X -> dbl# X) (terms# N -> sqr# N, sqr# s X -> add#(sqr X, dbl X)) (terms# N -> sqr# N, sqr# s X -> s# add(sqr X, dbl X)) (terms# N -> sqr# N, sqr# s X -> sqr# X) (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2) (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X1) (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> activate# X) (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> s# activate X) (activate# n__first(X1, X2) -> activate# X1, activate# n__terms X -> activate# X) (activate# n__first(X1, X2) -> activate# X1, activate# n__terms X -> terms# activate X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X2) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X1) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> activate# X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# activate X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> activate# X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> terms# activate X) (add#(s X, Y) -> add#(X, Y), add#(s X, Y) -> s# add(X, Y)) (add#(s X, Y) -> add#(X, Y), add#(s X, Y) -> add#(X, Y)) (activate# n__first(X1, X2) -> activate# X2, activate# n__terms X -> terms# activate X) (activate# n__first(X1, X2) -> activate# X2, activate# n__terms X -> activate# X) (activate# n__first(X1, X2) -> activate# X2, activate# n__s X -> s# activate X) (activate# n__first(X1, X2) -> activate# X2, activate# n__s X -> activate# X) (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X1) (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X2) (activate# n__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# Z) (activate# n__s X -> activate# X, activate# n__terms X -> terms# activate X) (activate# n__s X -> activate# X, activate# n__terms X -> activate# X) (activate# n__s X -> activate# X, activate# n__s X -> s# activate X) (activate# n__s X -> activate# X, activate# n__s X -> activate# X) (activate# n__s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (activate# n__s X -> activate# X, activate# n__first(X1, X2) -> activate# X1) (activate# n__s X -> activate# X, activate# n__first(X1, X2) -> activate# X2) (dbl# s X -> dbl# X, dbl# s X -> s# s dbl X) (dbl# s X -> dbl# X, dbl# s X -> s# dbl X) (dbl# s X -> dbl# X, dbl# s X -> dbl# X) (sqr# s X -> sqr# X, sqr# s X -> sqr# X) (sqr# s X -> sqr# X, sqr# s X -> s# add(sqr X, dbl X)) (sqr# s X -> sqr# X, sqr# s X -> add#(sqr X, dbl X)) (sqr# s X -> sqr# X, sqr# s X -> dbl# X) (activate# n__terms X -> terms# activate X, terms# N -> sqr# N)} STATUS: arrows: 0.830247 SCCS (4): Scc: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> activate# X, activate# n__s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} Scc: {sqr# s X -> sqr# X} Scc: {dbl# s X -> dbl# X} Scc: {add#(s X, Y) -> add#(X, Y)} SCC (6): Strict: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> activate# X, activate# n__s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} Weak: { sqr 0() -> 0(), sqr s X -> s add(sqr X, dbl X), terms N -> cons(recip sqr N, n__terms n__s N), terms X -> n__terms X, s X -> n__s X, add(0(), X) -> X, add(s X, Y) -> s add(X, Y), dbl 0() -> 0(), dbl s X -> s s dbl X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__terms X -> terms activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [add](x0, x1) = x0 + 1, [first](x0, x1) = x0 + x1, [n__first](x0, x1) = x0 + x1, [recip](x0) = x0 + 1, [sqr](x0) = 1, [n__terms](x0) = x0 + 1, [n__s](x0) = x0, [terms](x0) = x0 + 1, [s](x0) = x0, [dbl](x0) = 0, [activate](x0) = x0, [0] = 1, [nil] = 1, [first#](x0, x1) = x0, [activate#](x0) = x0 Strict: activate# n__first(X1, X2) -> activate# X2 0 + 1X1 + 1X2 >= 0 + 1X2 activate# n__first(X1, X2) -> activate# X1 0 + 1X1 + 1X2 >= 0 + 1X1 activate# n__first(X1, X2) -> first#(activate X1, activate X2) 0 + 1X1 + 1X2 >= 0 + 0X1 + 1X2 activate# n__s X -> activate# X 0 + 1X >= 0 + 1X activate# n__terms X -> activate# X 1 + 1X >= 0 + 1X first#(s X, cons(Y, Z)) -> activate# Z 0 + 0X + 0Y + 1Z >= 0 + 1Z Weak: activate n__first(X1, X2) -> first(activate X1, activate X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__s X -> s activate X 0 + 1X >= 0 + 1X activate n__terms X -> terms activate X 1 + 1X >= 1 + 1X activate X -> X 0 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 0 + 1X + 0Y + 1Z >= 0 + 1X + 0Y + 1Z first(0(), X) -> nil() 1 + 1X >= 1 first(X1, X2) -> n__first(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 dbl s X -> s s dbl X 0 + 0X >= 0 + 0X dbl 0() -> 0() 0 >= 1 add(s X, Y) -> s add(X, Y) 1 + 1X + 0Y >= 1 + 1X + 0Y add(0(), X) -> X 2 + 0X >= 1X s X -> n__s X 0 + 1X >= 0 + 1X terms X -> n__terms X 1 + 1X >= 1 + 1X terms N -> cons(recip sqr N, n__terms n__s N) 1 + 1N >= 1 + 1N sqr s X -> s add(sqr X, dbl X) 1 + 0X >= 2 + 0X sqr 0() -> 0() 1 >= 1 SCCS (1): Scc: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} SCC (5): Strict: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} Weak: { sqr 0() -> 0(), sqr s X -> s add(sqr X, dbl X), terms N -> cons(recip sqr N, n__terms n__s N), terms X -> n__terms X, s X -> n__s X, add(0(), X) -> X, add(s X, Y) -> s add(X, Y), dbl 0() -> 0(), dbl s X -> s s dbl X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__terms X -> terms activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [add](x0, x1) = x0 + x1 + 1, [first](x0, x1) = x0 + x1, [n__first](x0, x1) = x0 + x1, [recip](x0) = 0, [sqr](x0) = x0, [n__terms](x0) = 0, [n__s](x0) = x0 + 1, [terms](x0) = 0, [s](x0) = x0 + 1, [dbl](x0) = x0, [activate](x0) = x0, [0] = 1, [nil] = 1, [first#](x0, x1) = x0, [activate#](x0) = x0 Strict: activate# n__first(X1, X2) -> activate# X2 0 + 1X1 + 1X2 >= 0 + 1X2 activate# n__first(X1, X2) -> activate# X1 0 + 1X1 + 1X2 >= 0 + 1X1 activate# n__first(X1, X2) -> first#(activate X1, activate X2) 0 + 1X1 + 1X2 >= 0 + 0X1 + 1X2 activate# n__s X -> activate# X 1 + 1X >= 0 + 1X first#(s X, cons(Y, Z)) -> activate# Z 0 + 0X + 0Y + 1Z >= 0 + 1Z Weak: activate n__first(X1, X2) -> first(activate X1, activate X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__s X -> s activate X 1 + 1X >= 1 + 1X activate n__terms X -> terms activate X 0 + 0X >= 0 + 0X activate X -> X 0 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 1 + 1X + 0Y + 1Z >= 0 + 1X + 0Y + 1Z first(0(), X) -> nil() 1 + 1X >= 1 first(X1, X2) -> n__first(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 dbl s X -> s s dbl X 1 + 1X >= 2 + 1X dbl 0() -> 0() 1 >= 1 add(s X, Y) -> s add(X, Y) 2 + 1X + 1Y >= 2 + 1X + 1Y add(0(), X) -> X 2 + 1X >= 1X s X -> n__s X 1 + 1X >= 1 + 1X terms X -> n__terms X 0 + 0X >= 0 + 0X terms N -> cons(recip sqr N, n__terms n__s N) 0 + 0N >= 0 + 0N sqr s X -> s add(sqr X, dbl X) 1 + 1X >= 2 + 2X sqr 0() -> 0() 1 >= 1 SCCS (1): Scc: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} SCC (4): Strict: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} Weak: { sqr 0() -> 0(), sqr s X -> s add(sqr X, dbl X), terms N -> cons(recip sqr N, n__terms n__s N), terms X -> n__terms X, s X -> n__s X, add(0(), X) -> X, add(s X, Y) -> s add(X, Y), dbl 0() -> 0(), dbl s X -> s s dbl X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__terms X -> terms activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [add](x0, x1) = x0 + x1 + 1, [first](x0, x1) = x0 + x1, [n__first](x0, x1) = x0 + x1, [recip](x0) = 0, [sqr](x0) = x0, [n__terms](x0) = 0, [n__s](x0) = x0 + 1, [terms](x0) = 0, [s](x0) = x0 + 1, [dbl](x0) = x0, [activate](x0) = x0, [0] = 0, [nil] = 0, [first#](x0, x1) = x0 + x1, [activate#](x0) = x0 Strict: activate# n__first(X1, X2) -> activate# X2 0 + 1X1 + 1X2 >= 0 + 1X2 activate# n__first(X1, X2) -> activate# X1 0 + 1X1 + 1X2 >= 0 + 1X1 activate# n__first(X1, X2) -> first#(activate X1, activate X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 first#(s X, cons(Y, Z)) -> activate# Z 1 + 1X + 0Y + 1Z >= 0 + 1Z Weak: activate n__first(X1, X2) -> first(activate X1, activate X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__s X -> s activate X 1 + 1X >= 1 + 1X activate n__terms X -> terms activate X 0 + 0X >= 0 + 0X activate X -> X 0 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 1 + 1X + 0Y + 1Z >= 0 + 1X + 0Y + 1Z first(0(), X) -> nil() 0 + 1X >= 0 first(X1, X2) -> n__first(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 dbl s X -> s s dbl X 1 + 1X >= 2 + 1X dbl 0() -> 0() 0 >= 0 add(s X, Y) -> s add(X, Y) 2 + 1X + 1Y >= 2 + 1X + 1Y add(0(), X) -> X 1 + 1X >= 1X s X -> n__s X 1 + 1X >= 1 + 1X terms X -> n__terms X 0 + 0X >= 0 + 0X terms N -> cons(recip sqr N, n__terms n__s N) 0 + 0N >= 0 + 0N sqr s X -> s add(sqr X, dbl X) 1 + 1X >= 2 + 2X sqr 0() -> 0() 0 >= 0 SCCS (1): Scc: {activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} SCC (2): Strict: {activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} Weak: { sqr 0() -> 0(), sqr s X -> s add(sqr X, dbl X), terms N -> cons(recip sqr N, n__terms n__s N), terms X -> n__terms X, s X -> n__s X, add(0(), X) -> X, add(s X, Y) -> s add(X, Y), dbl 0() -> 0(), dbl s X -> s s dbl X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__terms X -> terms activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [add](x0, x1) = 1, [first](x0, x1) = 0, [n__first](x0, x1) = x0 + x1 + 1, [recip](x0) = 1, [sqr](x0) = x0 + 1, [n__terms](x0) = x0 + 1, [n__s](x0) = 1, [terms](x0) = x0 + 1, [s](x0) = x0 + 1, [dbl](x0) = x0 + 1, [activate](x0) = x0 + 1, [0] = 1, [nil] = 0, [activate#](x0) = x0 Strict: activate# n__first(X1, X2) -> activate# X2 1 + 1X1 + 1X2 >= 0 + 1X2 activate# n__first(X1, X2) -> activate# X1 1 + 1X1 + 1X2 >= 0 + 1X1 Weak: activate n__first(X1, X2) -> first(activate X1, activate X2) 2 + 1X1 + 1X2 >= 0 + 0X1 + 0X2 activate n__s X -> s activate X 2 + 0X >= 2 + 1X activate n__terms X -> terms activate X 2 + 1X >= 2 + 1X activate X -> X 1 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 1Y + 0Z first(0(), X) -> nil() 0 + 0X >= 0 first(X1, X2) -> n__first(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 1X2 dbl s X -> s s dbl X 2 + 1X >= 3 + 1X dbl 0() -> 0() 2 >= 1 add(s X, Y) -> s add(X, Y) 1 + 0X + 0Y >= 2 + 0X + 0Y add(0(), X) -> X 1 + 0X >= 1X s X -> n__s X 1 + 1X >= 1 + 0X terms X -> n__terms X 1 + 1X >= 1 + 1X terms N -> cons(recip sqr N, n__terms n__s N) 1 + 1N >= 1 + 0N sqr s X -> s add(sqr X, dbl X) 2 + 1X >= 2 + 0X sqr 0() -> 0() 2 >= 1 Qed SCC (1): Strict: {sqr# s X -> sqr# X} Weak: { sqr 0() -> 0(), sqr s X -> s add(sqr X, dbl X), terms N -> cons(recip sqr N, n__terms n__s N), terms X -> n__terms X, s X -> n__s X, add(0(), X) -> X, add(s X, Y) -> s add(X, Y), dbl 0() -> 0(), dbl s X -> s s dbl X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__terms X -> terms activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [add](x0, x1) = 1, [first](x0, x1) = x0 + 1, [n__first](x0, x1) = x0 + 1, [recip](x0) = 1, [sqr](x0) = x0 + 1, [n__terms](x0) = x0 + 1, [n__s](x0) = 1, [terms](x0) = x0 + 1, [s](x0) = x0 + 1, [dbl](x0) = x0 + 1, [activate](x0) = x0 + 1, [0] = 1, [nil] = 0, [sqr#](x0) = x0 Strict: sqr# s X -> sqr# X 1 + 1X >= 0 + 1X Weak: activate n__first(X1, X2) -> first(activate X1, activate X2) 2 + 0X1 + 1X2 >= 2 + 1X1 + 0X2 activate n__s X -> s activate X 2 + 0X >= 2 + 1X activate n__terms X -> terms activate X 2 + 1X >= 2 + 1X activate X -> X 1 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 2 + 1X + 0Y + 0Z >= 0 + 0X + 1Y + 0Z first(0(), X) -> nil() 2 + 0X >= 0 first(X1, X2) -> n__first(X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 1X2 dbl s X -> s s dbl X 2 + 1X >= 3 + 1X dbl 0() -> 0() 2 >= 1 add(s X, Y) -> s add(X, Y) 1 + 0X + 0Y >= 2 + 0X + 0Y add(0(), X) -> X 1 + 0X >= 1X s X -> n__s X 1 + 1X >= 1 + 0X terms X -> n__terms X 1 + 1X >= 1 + 1X terms N -> cons(recip sqr N, n__terms n__s N) 1 + 1N >= 1 + 0N sqr s X -> s add(sqr X, dbl X) 2 + 1X >= 2 + 0X sqr 0() -> 0() 2 >= 1 Qed SCC (1): Strict: {dbl# s X -> dbl# X} Weak: { sqr 0() -> 0(), sqr s X -> s add(sqr X, dbl X), terms N -> cons(recip sqr N, n__terms n__s N), terms X -> n__terms X, s X -> n__s X, add(0(), X) -> X, add(s X, Y) -> s add(X, Y), dbl 0() -> 0(), dbl s X -> s s dbl X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__terms X -> terms activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [add](x0, x1) = 1, [first](x0, x1) = x0 + 1, [n__first](x0, x1) = x0 + 1, [recip](x0) = 1, [sqr](x0) = x0 + 1, [n__terms](x0) = x0 + 1, [n__s](x0) = 1, [terms](x0) = x0 + 1, [s](x0) = x0 + 1, [dbl](x0) = x0 + 1, [activate](x0) = x0 + 1, [0] = 1, [nil] = 0, [dbl#](x0) = x0 Strict: dbl# s X -> dbl# X 1 + 1X >= 0 + 1X Weak: activate n__first(X1, X2) -> first(activate X1, activate X2) 2 + 0X1 + 1X2 >= 2 + 1X1 + 0X2 activate n__s X -> s activate X 2 + 0X >= 2 + 1X activate n__terms X -> terms activate X 2 + 1X >= 2 + 1X activate X -> X 1 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 2 + 1X + 0Y + 0Z >= 0 + 0X + 1Y + 0Z first(0(), X) -> nil() 2 + 0X >= 0 first(X1, X2) -> n__first(X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 1X2 dbl s X -> s s dbl X 2 + 1X >= 3 + 1X dbl 0() -> 0() 2 >= 1 add(s X, Y) -> s add(X, Y) 1 + 0X + 0Y >= 2 + 0X + 0Y add(0(), X) -> X 1 + 0X >= 1X s X -> n__s X 1 + 1X >= 1 + 0X terms X -> n__terms X 1 + 1X >= 1 + 1X terms N -> cons(recip sqr N, n__terms n__s N) 1 + 1N >= 1 + 0N sqr s X -> s add(sqr X, dbl X) 2 + 1X >= 2 + 0X sqr 0() -> 0() 2 >= 1 Qed SCC (1): Strict: {add#(s X, Y) -> add#(X, Y)} Weak: { sqr 0() -> 0(), sqr s X -> s add(sqr X, dbl X), terms N -> cons(recip sqr N, n__terms n__s N), terms X -> n__terms X, s X -> n__s X, add(0(), X) -> X, add(s X, Y) -> s add(X, Y), dbl 0() -> 0(), dbl s X -> s s dbl X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__terms X -> terms activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [add](x0, x1) = 1, [first](x0, x1) = x0 + 1, [n__first](x0, x1) = x0 + 1, [recip](x0) = 1, [sqr](x0) = x0 + 1, [n__terms](x0) = x0 + 1, [n__s](x0) = 1, [terms](x0) = x0 + 1, [s](x0) = x0 + 1, [dbl](x0) = x0 + 1, [activate](x0) = x0 + 1, [0] = 1, [nil] = 0, [add#](x0, x1) = x0 Strict: add#(s X, Y) -> add#(X, Y) 1 + 1X + 0Y >= 0 + 1X + 0Y Weak: activate n__first(X1, X2) -> first(activate X1, activate X2) 2 + 0X1 + 1X2 >= 2 + 1X1 + 0X2 activate n__s X -> s activate X 2 + 0X >= 2 + 1X activate n__terms X -> terms activate X 2 + 1X >= 2 + 1X activate X -> X 1 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 2 + 1X + 0Y + 0Z >= 0 + 0X + 1Y + 0Z first(0(), X) -> nil() 2 + 0X >= 0 first(X1, X2) -> n__first(X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 1X2 dbl s X -> s s dbl X 2 + 1X >= 3 + 1X dbl 0() -> 0() 2 >= 1 add(s X, Y) -> s add(X, Y) 1 + 0X + 0Y >= 2 + 0X + 0Y add(0(), X) -> X 1 + 0X >= 1X s X -> n__s X 1 + 1X >= 1 + 0X terms X -> n__terms X 1 + 1X >= 1 + 1X terms N -> cons(recip sqr N, n__terms n__s N) 1 + 1N >= 1 + 0N sqr s X -> s add(sqr X, dbl X) 2 + 1X >= 2 + 0X sqr 0() -> 0() 2 >= 1 Qed