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