MAYBE Time: 0.088939 TRS: { sqr s X -> s n__add(sqr activate X, dbl activate X), sqr 0() -> 0(), s X -> n__s X, terms N -> cons(recip sqr N, n__terms s N), terms X -> n__terms X, activate X -> X, activate n__terms X -> terms X, activate n__add(X1, X2) -> add(X1, X2), activate n__s X -> s X, activate n__dbl X -> dbl X, activate n__first(X1, X2) -> first(X1, X2), dbl X -> n__dbl X, dbl s X -> s n__s n__dbl activate X, dbl 0() -> 0(), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s n__add(activate X, Y), add(0(), X) -> X, first(X1, X2) -> n__first(X1, X2), first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)), first(0(), X) -> nil()} DP: DP: { sqr# s X -> sqr# activate X, sqr# s X -> s# n__add(sqr activate X, dbl activate X), sqr# s X -> activate# X, sqr# s X -> dbl# activate X, terms# N -> sqr# N, terms# N -> s# N, activate# n__terms X -> terms# X, activate# n__add(X1, X2) -> add#(X1, X2), activate# n__s X -> s# X, activate# n__dbl X -> dbl# X, activate# n__first(X1, X2) -> first#(X1, X2), dbl# s X -> s# n__s n__dbl activate X, dbl# s X -> activate# X, add#(s X, Y) -> s# n__add(activate X, Y), add#(s X, Y) -> activate# X, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Z} TRS: { sqr s X -> s n__add(sqr activate X, dbl activate X), sqr 0() -> 0(), s X -> n__s X, terms N -> cons(recip sqr N, n__terms s N), terms X -> n__terms X, activate X -> X, activate n__terms X -> terms X, activate n__add(X1, X2) -> add(X1, X2), activate n__s X -> s X, activate n__dbl X -> dbl X, activate n__first(X1, X2) -> first(X1, X2), dbl X -> n__dbl X, dbl s X -> s n__s n__dbl activate X, dbl 0() -> 0(), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s n__add(activate X, Y), add(0(), X) -> X, first(X1, X2) -> n__first(X1, X2), first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)), first(0(), X) -> nil()} UR: { sqr s X -> s n__add(sqr activate X, dbl activate X), sqr 0() -> 0(), s X -> n__s X, terms N -> cons(recip sqr N, n__terms s N), terms X -> n__terms X, activate X -> X, activate n__terms X -> terms X, activate n__add(X1, X2) -> add(X1, X2), activate n__s X -> s X, activate n__dbl X -> dbl X, activate n__first(X1, X2) -> first(X1, X2), dbl X -> n__dbl X, dbl s X -> s n__s n__dbl activate X, dbl 0() -> 0(), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s n__add(activate X, Y), add(0(), X) -> X, first(X1, X2) -> n__first(X1, X2), first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)), first(0(), X) -> nil(), a(x, y) -> x, a(x, y) -> y} EDG: {(sqr# s X -> dbl# activate X, dbl# s X -> activate# X) (sqr# s X -> dbl# activate X, dbl# s X -> s# n__s n__dbl activate X) (activate# n__add(X1, X2) -> add#(X1, X2), add#(s X, Y) -> activate# X) (activate# n__add(X1, X2) -> add#(X1, X2), add#(s X, Y) -> s# n__add(activate X, Y)) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(X1, X2)) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__dbl X -> dbl# X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> add#(X1, X2)) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> terms# X) (activate# n__terms X -> terms# X, terms# N -> s# N) (activate# n__terms X -> terms# X, terms# N -> sqr# N) (activate# n__dbl X -> dbl# X, dbl# s X -> activate# X) (activate# n__dbl X -> dbl# X, dbl# s X -> s# n__s n__dbl activate X) (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> first#(X1, X2)) (add#(s X, Y) -> activate# X, activate# n__dbl X -> dbl# X) (add#(s X, Y) -> activate# X, activate# n__s X -> s# X) (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2)) (add#(s X, Y) -> activate# X, activate# n__terms X -> terms# X) (terms# N -> sqr# N, sqr# s X -> dbl# activate X) (terms# N -> sqr# N, sqr# s X -> activate# X) (terms# N -> sqr# N, sqr# s X -> s# n__add(sqr activate X, dbl activate X)) (terms# N -> sqr# N, sqr# s X -> sqr# activate X) (first#(s X, cons(Y, Z)) -> activate# X, activate# n__terms X -> terms# X) (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2)) (first#(s X, cons(Y, Z)) -> activate# X, activate# n__s X -> s# X) (first#(s X, cons(Y, Z)) -> activate# X, activate# n__dbl X -> dbl# X) (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> first#(X1, X2)) (dbl# s X -> activate# X, activate# n__terms X -> terms# X) (dbl# s X -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2)) (dbl# s X -> activate# X, activate# n__s X -> s# X) (dbl# s X -> activate# X, activate# n__dbl X -> dbl# X) (dbl# s X -> activate# X, activate# n__first(X1, X2) -> first#(X1, X2)) (sqr# s X -> activate# X, activate# n__terms X -> terms# X) (sqr# s X -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2)) (sqr# s X -> activate# X, activate# n__s X -> s# X) (sqr# s X -> activate# X, activate# n__dbl X -> dbl# X) (sqr# s X -> activate# X, activate# n__first(X1, X2) -> first#(X1, X2)) (activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# X) (activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# Z) (sqr# s X -> sqr# activate X, sqr# s X -> sqr# activate X) (sqr# s X -> sqr# activate X, sqr# s X -> s# n__add(sqr activate X, dbl activate X)) (sqr# s X -> sqr# activate X, sqr# s X -> activate# X) (sqr# s X -> sqr# activate X, sqr# s X -> dbl# activate X)} STATUS: arrows: 0.851211 SCCS (1): Scc: { sqr# s X -> sqr# activate X, sqr# s X -> activate# X, sqr# s X -> dbl# activate X, terms# N -> sqr# N, activate# n__terms X -> terms# X, activate# n__add(X1, X2) -> add#(X1, X2), activate# n__dbl X -> dbl# X, activate# n__first(X1, X2) -> first#(X1, X2), dbl# s X -> activate# X, add#(s X, Y) -> activate# X, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Z} SCC (12): Strict: { sqr# s X -> sqr# activate X, sqr# s X -> activate# X, sqr# s X -> dbl# activate X, terms# N -> sqr# N, activate# n__terms X -> terms# X, activate# n__add(X1, X2) -> add#(X1, X2), activate# n__dbl X -> dbl# X, activate# n__first(X1, X2) -> first#(X1, X2), dbl# s X -> activate# X, add#(s X, Y) -> activate# X, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Z} Weak: { sqr s X -> s n__add(sqr activate X, dbl activate X), sqr 0() -> 0(), s X -> n__s X, terms N -> cons(recip sqr N, n__terms s N), terms X -> n__terms X, activate X -> X, activate n__terms X -> terms X, activate n__add(X1, X2) -> add(X1, X2), activate n__s X -> s X, activate n__dbl X -> dbl X, activate n__first(X1, X2) -> first(X1, X2), dbl X -> n__dbl X, dbl s X -> s n__s n__dbl activate X, dbl 0() -> 0(), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s n__add(activate X, Y), add(0(), X) -> X, first(X1, X2) -> n__first(X1, X2), first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)), first(0(), X) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [n__add](x0, x1) = x0 + x1 + 1, [add](x0, x1) = x0 + x1 + 1, [first](x0, x1) = x0 + x1, [n__first](x0, x1) = x0 + x1, [recip](x0) = 0, [sqr](x0) = 1, [n__terms](x0) = x0, [s](x0) = x0, [terms](x0) = x0, [activate](x0) = x0, [dbl](x0) = x0, [n__s](x0) = x0, [n__dbl](x0) = x0, [0] = 0, [nil] = 0, [add#](x0, x1) = x0 + 1, [first#](x0, x1) = x0 + x1, [sqr#](x0) = x0, [terms#](x0) = x0, [activate#](x0) = x0, [dbl#](x0) = x0 Strict: first#(s X, cons(Y, Z)) -> activate# Z 0 + 1X + 0Y + 1Z >= 0 + 1Z first#(s X, cons(Y, Z)) -> activate# X 0 + 1X + 0Y + 1Z >= 0 + 1X add#(s X, Y) -> activate# X 1 + 1X + 0Y >= 0 + 1X dbl# s X -> activate# X 0 + 1X >= 0 + 1X activate# n__first(X1, X2) -> first#(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate# n__dbl X -> dbl# X 0 + 1X >= 0 + 1X activate# n__add(X1, X2) -> add#(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 0X2 activate# n__terms X -> terms# X 0 + 1X >= 0 + 1X terms# N -> sqr# N 0 + 1N >= 0 + 1N sqr# s X -> dbl# activate X 0 + 1X >= 0 + 1X sqr# s X -> activate# X 0 + 1X >= 0 + 1X sqr# s X -> sqr# activate X 0 + 1X >= 0 + 1X Weak: first(0(), X) -> nil() 0 + 1X >= 0 first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)) 0 + 1X + 0Y + 1Z >= 0 + 1X + 0Y + 1Z first(X1, X2) -> n__first(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 add(0(), X) -> X 1 + 1X >= 1X add(s X, Y) -> s n__add(activate X, Y) 1 + 1X + 1Y >= 1 + 1X + 1Y add(X1, X2) -> n__add(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 dbl 0() -> 0() 0 >= 0 dbl s X -> s n__s n__dbl activate X 0 + 1X >= 0 + 1X dbl X -> n__dbl X 0 + 1X >= 0 + 1X activate n__first(X1, X2) -> first(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__dbl X -> dbl X 0 + 1X >= 0 + 1X activate n__s X -> s X 0 + 1X >= 0 + 1X activate n__add(X1, X2) -> add(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate n__terms X -> terms X 0 + 1X >= 0 + 1X activate X -> X 0 + 1X >= 1X terms X -> n__terms X 0 + 1X >= 0 + 1X terms N -> cons(recip sqr N, n__terms s N) 0 + 1N >= 0 + 1N s X -> n__s X 0 + 1X >= 0 + 1X sqr 0() -> 0() 1 >= 0 sqr s X -> s n__add(sqr activate X, dbl activate X) 1 + 0X >= 2 + 1X SCCS (1): Scc: { sqr# s X -> sqr# activate X, sqr# s X -> activate# X, sqr# s X -> dbl# activate X, terms# N -> sqr# N, activate# n__terms X -> terms# X, activate# n__dbl X -> dbl# X, activate# n__first(X1, X2) -> first#(X1, X2), dbl# s X -> activate# X, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Z} SCC (10): Strict: { sqr# s X -> sqr# activate X, sqr# s X -> activate# X, sqr# s X -> dbl# activate X, terms# N -> sqr# N, activate# n__terms X -> terms# X, activate# n__dbl X -> dbl# X, activate# n__first(X1, X2) -> first#(X1, X2), dbl# s X -> activate# X, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Z} Weak: { sqr s X -> s n__add(sqr activate X, dbl activate X), sqr 0() -> 0(), s X -> n__s X, terms N -> cons(recip sqr N, n__terms s N), terms X -> n__terms X, activate X -> X, activate n__terms X -> terms X, activate n__add(X1, X2) -> add(X1, X2), activate n__s X -> s X, activate n__dbl X -> dbl X, activate n__first(X1, X2) -> first(X1, X2), dbl X -> n__dbl X, dbl s X -> s n__s n__dbl activate X, dbl 0() -> 0(), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s n__add(activate X, Y), add(0(), X) -> X, first(X1, X2) -> n__first(X1, X2), first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)), first(0(), X) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [n__add](x0, x1) = x0, [add](x0, x1) = x0, [first](x0, x1) = x0 + x1, [n__first](x0, x1) = x0 + x1, [recip](x0) = 0, [sqr](x0) = 0, [n__terms](x0) = x0 + 1, [s](x0) = x0, [terms](x0) = x0 + 1, [activate](x0) = x0, [dbl](x0) = x0, [n__s](x0) = x0, [n__dbl](x0) = x0, [0] = 0, [nil] = 0, [first#](x0, x1) = x0 + x1, [sqr#](x0) = x0, [terms#](x0) = x0, [activate#](x0) = x0, [dbl#](x0) = x0 Strict: first#(s X, cons(Y, Z)) -> activate# Z 0 + 1X + 0Y + 1Z >= 0 + 1Z first#(s X, cons(Y, Z)) -> activate# X 0 + 1X + 0Y + 1Z >= 0 + 1X dbl# s X -> activate# X 0 + 1X >= 0 + 1X activate# n__first(X1, X2) -> first#(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate# n__dbl X -> dbl# X 0 + 1X >= 0 + 1X activate# n__terms X -> terms# X 1 + 1X >= 0 + 1X terms# N -> sqr# N 0 + 1N >= 0 + 1N sqr# s X -> dbl# activate X 0 + 1X >= 0 + 1X sqr# s X -> activate# X 0 + 1X >= 0 + 1X sqr# s X -> sqr# activate X 0 + 1X >= 0 + 1X Weak: first(0(), X) -> nil() 0 + 1X >= 0 first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)) 0 + 1X + 0Y + 1Z >= 0 + 1X + 0Y + 1Z first(X1, X2) -> n__first(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 add(0(), X) -> X 0 + 1X >= 1X add(s X, Y) -> s n__add(activate X, Y) 0 + 0X + 1Y >= 0 + 0X + 1Y add(X1, X2) -> n__add(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 dbl 0() -> 0() 0 >= 0 dbl s X -> s n__s n__dbl activate X 0 + 1X >= 0 + 1X dbl X -> n__dbl X 0 + 1X >= 0 + 1X activate n__first(X1, X2) -> first(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__dbl X -> dbl X 0 + 1X >= 0 + 1X activate n__s X -> s X 0 + 1X >= 0 + 1X activate n__add(X1, X2) -> add(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 activate n__terms X -> terms X 1 + 1X >= 1 + 1X activate X -> X 0 + 1X >= 1X terms X -> n__terms X 1 + 1X >= 1 + 1X terms N -> cons(recip sqr N, n__terms s N) 1 + 1N >= 1 + 1N s X -> n__s X 0 + 1X >= 0 + 1X sqr 0() -> 0() 0 >= 0 sqr s X -> s n__add(sqr activate X, dbl activate X) 0 + 0X >= 0 + 1X SCCS (2): Scc: {sqr# s X -> sqr# activate X} Scc: { activate# n__dbl X -> dbl# X, activate# n__first(X1, X2) -> first#(X1, X2), dbl# s X -> activate# X, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Z} SCC (1): Strict: {sqr# s X -> sqr# activate X} Weak: { sqr s X -> s n__add(sqr activate X, dbl activate X), sqr 0() -> 0(), s X -> n__s X, terms N -> cons(recip sqr N, n__terms s N), terms X -> n__terms X, activate X -> X, activate n__terms X -> terms X, activate n__add(X1, X2) -> add(X1, X2), activate n__s X -> s X, activate n__dbl X -> dbl X, activate n__first(X1, X2) -> first(X1, X2), dbl X -> n__dbl X, dbl s X -> s n__s n__dbl activate X, dbl 0() -> 0(), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s n__add(activate X, Y), add(0(), X) -> X, first(X1, X2) -> n__first(X1, X2), first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)), first(0(), X) -> nil()} Fail SCC (5): Strict: { activate# n__dbl X -> dbl# X, activate# n__first(X1, X2) -> first#(X1, X2), dbl# s X -> activate# X, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Z} Weak: { sqr s X -> s n__add(sqr activate X, dbl activate X), sqr 0() -> 0(), s X -> n__s X, terms N -> cons(recip sqr N, n__terms s N), terms X -> n__terms X, activate X -> X, activate n__terms X -> terms X, activate n__add(X1, X2) -> add(X1, X2), activate n__s X -> s X, activate n__dbl X -> dbl X, activate n__first(X1, X2) -> first(X1, X2), dbl X -> n__dbl X, dbl s X -> s n__s n__dbl activate X, dbl 0() -> 0(), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s n__add(activate X, Y), add(0(), X) -> X, first(X1, X2) -> n__first(X1, X2), first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)), first(0(), X) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [n__add](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [first](x0, x1) = 0, [n__first](x0, x1) = x0 + x1 + 1, [recip](x0) = 0, [sqr](x0) = x0 + 1, [n__terms](x0) = 0, [s](x0) = x0 + 1, [terms](x0) = 0, [activate](x0) = 0, [dbl](x0) = 1, [n__s](x0) = x0 + 1, [n__dbl](x0) = x0 + 1, [0] = 1, [nil] = 0, [first#](x0, x1) = x0 + x1 + 1, [activate#](x0) = x0 + 1, [dbl#](x0) = x0 + 1 Strict: first#(s X, cons(Y, Z)) -> activate# Z 2 + 1X + 0Y + 1Z >= 1 + 1Z first#(s X, cons(Y, Z)) -> activate# X 2 + 1X + 0Y + 1Z >= 1 + 1X dbl# s X -> activate# X 2 + 1X >= 1 + 1X activate# n__first(X1, X2) -> first#(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate# n__dbl X -> dbl# X 2 + 1X >= 1 + 1X Weak: first(0(), X) -> nil() 0 + 0X >= 0 first(s X, cons(Y, Z)) -> cons(Y, n__first(activate X, activate Z)) 0 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z first(X1, X2) -> n__first(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 1X2 add(0(), X) -> X 2 + 0X >= 1X add(s X, Y) -> s n__add(activate X, Y) 2 + 1X + 0Y >= 2 + 0X + 1Y add(X1, X2) -> n__add(X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 1X2 dbl 0() -> 0() 1 >= 1 dbl s X -> s n__s n__dbl activate X 1 + 0X >= 3 + 0X dbl X -> n__dbl X 1 + 0X >= 1 + 1X activate n__first(X1, X2) -> first(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__dbl X -> dbl X 0 + 0X >= 1 + 0X activate n__s X -> s X 0 + 0X >= 1 + 1X activate n__add(X1, X2) -> add(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2 activate n__terms X -> terms X 0 + 0X >= 0 + 0X activate X -> X 0 + 0X >= 1X terms X -> n__terms X 0 + 0X >= 0 + 0X terms N -> cons(recip sqr N, n__terms s N) 0 + 0N >= 0 + 0N s X -> n__s X 1 + 1X >= 1 + 1X sqr 0() -> 0() 2 >= 1 sqr s X -> s n__add(sqr activate X, dbl activate X) 2 + 1X >= 3 + 0X Qed