The rewrite relation of the following TRS is considered.
active(from(X)) | → | mark(cons(X,from(s(X)))) | (1) |
active(2ndspos(0,Z)) | → | mark(rnil) | (2) |
active(2ndspos(s(N),cons(X,Z))) | → | mark(2ndspos(s(N),cons2(X,Z))) | (3) |
active(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(posrecip(Y),2ndsneg(N,Z))) | (4) |
active(2ndsneg(0,Z)) | → | mark(rnil) | (5) |
active(2ndsneg(s(N),cons(X,Z))) | → | mark(2ndsneg(s(N),cons2(X,Z))) | (6) |
active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(negrecip(Y),2ndspos(N,Z))) | (7) |
active(pi(X)) | → | mark(2ndspos(X,from(0))) | (8) |
active(plus(0,Y)) | → | mark(Y) | (9) |
active(plus(s(X),Y)) | → | mark(s(plus(X,Y))) | (10) |
active(times(0,Y)) | → | mark(0) | (11) |
active(times(s(X),Y)) | → | mark(plus(Y,times(X,Y))) | (12) |
active(square(X)) | → | mark(times(X,X)) | (13) |
mark(from(X)) | → | active(from(mark(X))) | (14) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (15) |
mark(s(X)) | → | active(s(mark(X))) | (16) |
mark(2ndspos(X1,X2)) | → | active(2ndspos(mark(X1),mark(X2))) | (17) |
mark(0) | → | active(0) | (18) |
mark(rnil) | → | active(rnil) | (19) |
mark(cons2(X1,X2)) | → | active(cons2(X1,mark(X2))) | (20) |
mark(rcons(X1,X2)) | → | active(rcons(mark(X1),mark(X2))) | (21) |
mark(posrecip(X)) | → | active(posrecip(mark(X))) | (22) |
mark(2ndsneg(X1,X2)) | → | active(2ndsneg(mark(X1),mark(X2))) | (23) |
mark(negrecip(X)) | → | active(negrecip(mark(X))) | (24) |
mark(pi(X)) | → | active(pi(mark(X))) | (25) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (26) |
mark(times(X1,X2)) | → | active(times(mark(X1),mark(X2))) | (27) |
mark(square(X)) | → | active(square(mark(X))) | (28) |
from(mark(X)) | → | from(X) | (29) |
from(active(X)) | → | from(X) | (30) |
cons(mark(X1),X2) | → | cons(X1,X2) | (31) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (32) |
cons(active(X1),X2) | → | cons(X1,X2) | (33) |
cons(X1,active(X2)) | → | cons(X1,X2) | (34) |
s(mark(X)) | → | s(X) | (35) |
s(active(X)) | → | s(X) | (36) |
2ndspos(mark(X1),X2) | → | 2ndspos(X1,X2) | (37) |
2ndspos(X1,mark(X2)) | → | 2ndspos(X1,X2) | (38) |
2ndspos(active(X1),X2) | → | 2ndspos(X1,X2) | (39) |
2ndspos(X1,active(X2)) | → | 2ndspos(X1,X2) | (40) |
cons2(mark(X1),X2) | → | cons2(X1,X2) | (41) |
cons2(X1,mark(X2)) | → | cons2(X1,X2) | (42) |
cons2(active(X1),X2) | → | cons2(X1,X2) | (43) |
cons2(X1,active(X2)) | → | cons2(X1,X2) | (44) |
rcons(mark(X1),X2) | → | rcons(X1,X2) | (45) |
rcons(X1,mark(X2)) | → | rcons(X1,X2) | (46) |
rcons(active(X1),X2) | → | rcons(X1,X2) | (47) |
rcons(X1,active(X2)) | → | rcons(X1,X2) | (48) |
posrecip(mark(X)) | → | posrecip(X) | (49) |
posrecip(active(X)) | → | posrecip(X) | (50) |
2ndsneg(mark(X1),X2) | → | 2ndsneg(X1,X2) | (51) |
2ndsneg(X1,mark(X2)) | → | 2ndsneg(X1,X2) | (52) |
2ndsneg(active(X1),X2) | → | 2ndsneg(X1,X2) | (53) |
2ndsneg(X1,active(X2)) | → | 2ndsneg(X1,X2) | (54) |
negrecip(mark(X)) | → | negrecip(X) | (55) |
negrecip(active(X)) | → | negrecip(X) | (56) |
pi(mark(X)) | → | pi(X) | (57) |
pi(active(X)) | → | pi(X) | (58) |
plus(mark(X1),X2) | → | plus(X1,X2) | (59) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (60) |
plus(active(X1),X2) | → | plus(X1,X2) | (61) |
plus(X1,active(X2)) | → | plus(X1,X2) | (62) |
times(mark(X1),X2) | → | times(X1,X2) | (63) |
times(X1,mark(X2)) | → | times(X1,X2) | (64) |
times(active(X1),X2) | → | times(X1,X2) | (65) |
times(X1,active(X2)) | → | times(X1,X2) | (66) |
square(mark(X)) | → | square(X) | (67) |
square(active(X)) | → | square(X) | (68) |
There are 119 ruless (increase limit for explicit display).
The dependency pairs are split into 14 components.
active#(pi(X)) | → | mark#(2ndspos(X,from(0))) | (140) |
mark#(2ndspos(X1,X2)) | → | active#(2ndspos(mark(X1),mark(X2))) | (185) |
mark#(cons2(X1,X2)) | → | active#(cons2(X1,mark(X2))) | (137) |
mark#(pi(X)) | → | active#(pi(mark(X))) | (138) |
active#(from(X)) | → | mark#(cons(X,from(s(X)))) | (182) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (132) |
mark#(2ndspos(X1,X2)) | → | mark#(X1) | (131) |
mark#(plus(X1,X2)) | → | mark#(X1) | (130) |
mark#(negrecip(X)) | → | mark#(X) | (127) |
mark#(rcons(X1,X2)) | → | mark#(X2) | (123) |
mark#(cons2(X1,X2)) | → | mark#(X2) | (178) |
mark#(times(X1,X2)) | → | mark#(X2) | (121) |
mark#(times(X1,X2)) | → | mark#(X1) | (176) |
mark#(square(X)) | → | mark#(X) | (117) |
active#(square(X)) | → | mark#(times(X,X)) | (116) |
active#(2ndsneg(s(N),cons(X,Z))) | → | mark#(2ndsneg(s(N),cons2(X,Z))) | (174) |
mark#(square(X)) | → | active#(square(mark(X))) | (171) |
active#(2ndspos(s(N),cons(X,Z))) | → | mark#(2ndspos(s(N),cons2(X,Z))) | (169) |
active#(plus(0,Y)) | → | mark#(Y) | (168) |
mark#(pi(X)) | → | mark#(X) | (107) |
mark#(2ndsneg(X1,X2)) | → | active#(2ndsneg(mark(X1),mark(X2))) | (164) |
mark#(plus(X1,X2)) | → | mark#(X2) | (105) |
active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(negrecip(Y),2ndspos(N,Z))) | (102) |
active#(plus(s(X),Y)) | → | mark#(s(plus(X,Y))) | (161) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (159) |
mark#(cons(X1,X2)) | → | mark#(X1) | (95) |
mark#(2ndsneg(X1,X2)) | → | mark#(X1) | (157) |
mark#(times(X1,X2)) | → | active#(times(mark(X1),mark(X2))) | (91) |
mark#(posrecip(X)) | → | active#(posrecip(mark(X))) | (89) |
mark#(posrecip(X)) | → | mark#(X) | (86) |
mark#(from(X)) | → | mark#(X) | (153) |
mark#(s(X)) | → | active#(s(mark(X))) | (84) |
active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(posrecip(Y),2ndsneg(N,Z))) | (82) |
mark#(s(X)) | → | mark#(X) | (83) |
active#(times(s(X),Y)) | → | mark#(plus(Y,times(X,Y))) | (81) |
mark#(rcons(X1,X2)) | → | active#(rcons(mark(X1),mark(X2))) | (148) |
mark#(rcons(X1,X2)) | → | mark#(X1) | (79) |
mark#(from(X)) | → | active#(from(mark(X))) | (77) |
mark#(2ndspos(X1,X2)) | → | mark#(X2) | (74) |
mark#(2ndsneg(X1,X2)) | → | mark#(X2) | (73) |
mark#(negrecip(X)) | → | active#(negrecip(mark(X))) | (72) |
[negrecip(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | 2 |
[rnil] | = | 1 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | 2 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | 2 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | 1 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 2 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | 2 |
[times(x1, x2)] | = | 2 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 1 |
[2ndsneg(x1, x2)] | = | 2 |
[plus(x1, x2)] | = | 2 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | 1 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[cons(x1, x2)] | = | 1 |
[active#(x1)] | = | x1 + 0 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | 1 |
posrecip(active(X)) | → | posrecip(X) | (50) |
2ndsneg(X1,active(X2)) | → | 2ndsneg(X1,X2) | (54) |
s(active(X)) | → | s(X) | (36) |
square(active(X)) | → | square(X) | (68) |
times(mark(X1),X2) | → | times(X1,X2) | (63) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (32) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (60) |
cons(X1,active(X2)) | → | cons(X1,X2) | (34) |
times(active(X1),X2) | → | times(X1,X2) | (65) |
cons2(X1,active(X2)) | → | cons2(X1,X2) | (44) |
cons(active(X1),X2) | → | cons(X1,X2) | (33) |
times(X1,mark(X2)) | → | times(X1,X2) | (64) |
2ndspos(active(X1),X2) | → | 2ndspos(X1,X2) | (39) |
posrecip(mark(X)) | → | posrecip(X) | (49) |
2ndsneg(X1,mark(X2)) | → | 2ndsneg(X1,X2) | (52) |
from(active(X)) | → | from(X) | (30) |
plus(X1,active(X2)) | → | plus(X1,X2) | (62) |
negrecip(active(X)) | → | negrecip(X) | (56) |
cons(mark(X1),X2) | → | cons(X1,X2) | (31) |
rcons(mark(X1),X2) | → | rcons(X1,X2) | (45) |
pi(mark(X)) | → | pi(X) | (57) |
2ndsneg(mark(X1),X2) | → | 2ndsneg(X1,X2) | (51) |
2ndspos(X1,active(X2)) | → | 2ndspos(X1,X2) | (40) |
square(mark(X)) | → | square(X) | (67) |
negrecip(mark(X)) | → | negrecip(X) | (55) |
plus(mark(X1),X2) | → | plus(X1,X2) | (59) |
2ndspos(X1,mark(X2)) | → | 2ndspos(X1,X2) | (38) |
plus(active(X1),X2) | → | plus(X1,X2) | (61) |
pi(active(X)) | → | pi(X) | (58) |
rcons(X1,active(X2)) | → | rcons(X1,X2) | (48) |
2ndsneg(active(X1),X2) | → | 2ndsneg(X1,X2) | (53) |
rcons(active(X1),X2) | → | rcons(X1,X2) | (47) |
2ndspos(mark(X1),X2) | → | 2ndspos(X1,X2) | (37) |
cons2(mark(X1),X2) | → | cons2(X1,X2) | (41) |
cons2(X1,mark(X2)) | → | cons2(X1,X2) | (42) |
rcons(X1,mark(X2)) | → | rcons(X1,X2) | (46) |
times(X1,active(X2)) | → | times(X1,X2) | (66) |
s(mark(X)) | → | s(X) | (35) |
from(mark(X)) | → | from(X) | (29) |
cons2(active(X1),X2) | → | cons2(X1,X2) | (43) |
mark#(cons2(X1,X2)) | → | active#(cons2(X1,mark(X2))) | (137) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (132) |
mark#(posrecip(X)) | → | active#(posrecip(mark(X))) | (89) |
mark#(s(X)) | → | active#(s(mark(X))) | (84) |
mark#(rcons(X1,X2)) | → | active#(rcons(mark(X1),mark(X2))) | (148) |
mark#(negrecip(X)) | → | active#(negrecip(mark(X))) | (72) |
The dependency pairs are split into 1 component.
active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(posrecip(Y),2ndsneg(N,Z))) | (82) |
mark#(cons(X1,X2)) | → | mark#(X1) | (95) |
active#(pi(X)) | → | mark#(2ndspos(X,from(0))) | (140) |
active#(from(X)) | → | mark#(cons(X,from(s(X)))) | (182) |
active#(2ndspos(s(N),cons(X,Z))) | → | mark#(2ndspos(s(N),cons2(X,Z))) | (169) |
mark#(s(X)) | → | mark#(X) | (83) |
mark#(rcons(X1,X2)) | → | mark#(X2) | (123) |
mark#(rcons(X1,X2)) | → | mark#(X1) | (79) |
mark#(plus(X1,X2)) | → | mark#(X2) | (105) |
mark#(plus(X1,X2)) | → | mark#(X1) | (130) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (159) |
mark#(2ndspos(X1,X2)) | → | mark#(X2) | (74) |
mark#(2ndspos(X1,X2)) | → | mark#(X1) | (131) |
mark#(2ndspos(X1,X2)) | → | active#(2ndspos(mark(X1),mark(X2))) | (185) |
mark#(times(X1,X2)) | → | mark#(X2) | (121) |
mark#(times(X1,X2)) | → | mark#(X1) | (176) |
mark#(times(X1,X2)) | → | active#(times(mark(X1),mark(X2))) | (91) |
mark#(posrecip(X)) | → | mark#(X) | (86) |
mark#(square(X)) | → | mark#(X) | (117) |
mark#(square(X)) | → | active#(square(mark(X))) | (171) |
active#(plus(s(X),Y)) | → | mark#(s(plus(X,Y))) | (161) |
active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(negrecip(Y),2ndspos(N,Z))) | (102) |
mark#(cons2(X1,X2)) | → | mark#(X2) | (178) |
mark#(pi(X)) | → | mark#(X) | (107) |
mark#(pi(X)) | → | active#(pi(mark(X))) | (138) |
mark#(from(X)) | → | mark#(X) | (153) |
mark#(from(X)) | → | active#(from(mark(X))) | (77) |
active#(times(s(X),Y)) | → | mark#(plus(Y,times(X,Y))) | (81) |
mark#(2ndsneg(X1,X2)) | → | mark#(X2) | (73) |
mark#(2ndsneg(X1,X2)) | → | mark#(X1) | (157) |
mark#(2ndsneg(X1,X2)) | → | active#(2ndsneg(mark(X1),mark(X2))) | (164) |
mark#(negrecip(X)) | → | mark#(X) | (127) |
active#(plus(0,Y)) | → | mark#(Y) | (168) |
active#(square(X)) | → | mark#(times(X,X)) | (116) |
active#(2ndsneg(s(N),cons(X,Z))) | → | mark#(2ndsneg(s(N),cons2(X,Z))) | (174) |
[negrecip(x1)] | = | x1 + 1 |
[cons#(x1, x2)] | = | max(0) |
[s(x1)] | = | x1 + 0 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | max(x1 + 3, x2 + 1, 0) |
[rnil] | = | 2 |
[plus#(x1, x2)] | = | max(0) |
[square(x1)] | = | x1 + 4 |
[cons2#(x1, x2)] | = | max(0) |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 36421 |
[rcons#(x1, x2)] | = | max(0) |
[rcons(x1, x2)] | = | max(x1 + 3, x2 + 0, 0) |
[times#(x1, x2)] | = | max(0) |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 29537 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 6882 |
[times(x1, x2)] | = | max(x1 + 1, x2 + 3, 0) |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[2ndsneg(x1, x2)] | = | max(x1 + 3, x2 + 1, 0) |
[plus(x1, x2)] | = | max(x1 + 2, x2 + 0, 0) |
[2ndspos#(x1, x2)] | = | max(0) |
[cons2(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | max(x1 + 3, x2 + 0, 0) |
[active#(x1)] | = | x1 + 0 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | max(0) |
[posrecip(x1)] | = | x1 + 1 |
mark(0) | → | active(0) | (18) |
posrecip(active(X)) | → | posrecip(X) | (50) |
active(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(posrecip(Y),2ndsneg(N,Z))) | (4) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (15) |
active(pi(X)) | → | mark(2ndspos(X,from(0))) | (8) |
2ndsneg(X1,active(X2)) | → | 2ndsneg(X1,X2) | (54) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (1) |
active(2ndspos(s(N),cons(X,Z))) | → | mark(2ndspos(s(N),cons2(X,Z))) | (3) |
mark(s(X)) | → | active(s(mark(X))) | (16) |
mark(rcons(X1,X2)) | → | active(rcons(mark(X1),mark(X2))) | (21) |
s(active(X)) | → | s(X) | (36) |
square(active(X)) | → | square(X) | (68) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (26) |
times(mark(X1),X2) | → | times(X1,X2) | (63) |
mark(rnil) | → | active(rnil) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (32) |
mark(2ndspos(X1,X2)) | → | active(2ndspos(mark(X1),mark(X2))) | (17) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (60) |
mark(times(X1,X2)) | → | active(times(mark(X1),mark(X2))) | (27) |
cons(X1,active(X2)) | → | cons(X1,X2) | (34) |
mark(posrecip(X)) | → | active(posrecip(mark(X))) | (22) |
mark(square(X)) | → | active(square(mark(X))) | (28) |
times(active(X1),X2) | → | times(X1,X2) | (65) |
cons2(X1,active(X2)) | → | cons2(X1,X2) | (44) |
active(2ndsneg(0,Z)) | → | mark(rnil) | (5) |
cons(active(X1),X2) | → | cons(X1,X2) | (33) |
times(X1,mark(X2)) | → | times(X1,X2) | (64) |
active(plus(s(X),Y)) | → | mark(s(plus(X,Y))) | (10) |
2ndspos(active(X1),X2) | → | 2ndspos(X1,X2) | (39) |
active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(negrecip(Y),2ndspos(N,Z))) | (7) |
mark(cons2(X1,X2)) | → | active(cons2(X1,mark(X2))) | (20) |
mark(pi(X)) | → | active(pi(mark(X))) | (25) |
posrecip(mark(X)) | → | posrecip(X) | (49) |
2ndsneg(X1,mark(X2)) | → | 2ndsneg(X1,X2) | (52) |
from(active(X)) | → | from(X) | (30) |
plus(X1,active(X2)) | → | plus(X1,X2) | (62) |
mark(from(X)) | → | active(from(mark(X))) | (14) |
negrecip(active(X)) | → | negrecip(X) | (56) |
cons(mark(X1),X2) | → | cons(X1,X2) | (31) |
active(times(s(X),Y)) | → | mark(plus(Y,times(X,Y))) | (12) |
rcons(mark(X1),X2) | → | rcons(X1,X2) | (45) |
mark(2ndsneg(X1,X2)) | → | active(2ndsneg(mark(X1),mark(X2))) | (23) |
mark(negrecip(X)) | → | active(negrecip(mark(X))) | (24) |
pi(mark(X)) | → | pi(X) | (57) |
active(times(0,Y)) | → | mark(0) | (11) |
active(plus(0,Y)) | → | mark(Y) | (9) |
active(square(X)) | → | mark(times(X,X)) | (13) |
2ndsneg(mark(X1),X2) | → | 2ndsneg(X1,X2) | (51) |
2ndspos(X1,active(X2)) | → | 2ndspos(X1,X2) | (40) |
square(mark(X)) | → | square(X) | (67) |
negrecip(mark(X)) | → | negrecip(X) | (55) |
plus(mark(X1),X2) | → | plus(X1,X2) | (59) |
active(2ndsneg(s(N),cons(X,Z))) | → | mark(2ndsneg(s(N),cons2(X,Z))) | (6) |
2ndspos(X1,mark(X2)) | → | 2ndspos(X1,X2) | (38) |
plus(active(X1),X2) | → | plus(X1,X2) | (61) |
pi(active(X)) | → | pi(X) | (58) |
rcons(X1,active(X2)) | → | rcons(X1,X2) | (48) |
2ndsneg(active(X1),X2) | → | 2ndsneg(X1,X2) | (53) |
rcons(active(X1),X2) | → | rcons(X1,X2) | (47) |
2ndspos(mark(X1),X2) | → | 2ndspos(X1,X2) | (37) |
cons2(mark(X1),X2) | → | cons2(X1,X2) | (41) |
cons2(X1,mark(X2)) | → | cons2(X1,X2) | (42) |
rcons(X1,mark(X2)) | → | rcons(X1,X2) | (46) |
times(X1,active(X2)) | → | times(X1,X2) | (66) |
s(mark(X)) | → | s(X) | (35) |
from(mark(X)) | → | from(X) | (29) |
cons2(active(X1),X2) | → | cons2(X1,X2) | (43) |
active(2ndspos(0,Z)) | → | mark(rnil) | (2) |
mark#(cons(X1,X2)) | → | mark#(X1) | (95) |
active#(pi(X)) | → | mark#(2ndspos(X,from(0))) | (140) |
mark#(rcons(X1,X2)) | → | mark#(X1) | (79) |
mark#(plus(X1,X2)) | → | mark#(X1) | (130) |
mark#(2ndspos(X1,X2)) | → | mark#(X2) | (74) |
mark#(2ndspos(X1,X2)) | → | mark#(X1) | (131) |
mark#(times(X1,X2)) | → | mark#(X2) | (121) |
mark#(times(X1,X2)) | → | mark#(X1) | (176) |
mark#(posrecip(X)) | → | mark#(X) | (86) |
mark#(square(X)) | → | mark#(X) | (117) |
mark#(pi(X)) | → | mark#(X) | (107) |
mark#(from(X)) | → | mark#(X) | (153) |
mark#(2ndsneg(X1,X2)) | → | mark#(X2) | (73) |
mark#(2ndsneg(X1,X2)) | → | mark#(X1) | (157) |
mark#(negrecip(X)) | → | mark#(X) | (127) |
active#(square(X)) | → | mark#(times(X,X)) | (116) |
The dependency pairs are split into 1 component.
active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(posrecip(Y),2ndsneg(N,Z))) | (82) |
active#(from(X)) | → | mark#(cons(X,from(s(X)))) | (182) |
active#(2ndspos(s(N),cons(X,Z))) | → | mark#(2ndspos(s(N),cons2(X,Z))) | (169) |
mark#(s(X)) | → | mark#(X) | (83) |
mark#(rcons(X1,X2)) | → | mark#(X2) | (123) |
mark#(plus(X1,X2)) | → | mark#(X2) | (105) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (159) |
mark#(2ndspos(X1,X2)) | → | active#(2ndspos(mark(X1),mark(X2))) | (185) |
mark#(times(X1,X2)) | → | active#(times(mark(X1),mark(X2))) | (91) |
mark#(square(X)) | → | active#(square(mark(X))) | (171) |
active#(plus(s(X),Y)) | → | mark#(s(plus(X,Y))) | (161) |
active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(negrecip(Y),2ndspos(N,Z))) | (102) |
mark#(cons2(X1,X2)) | → | mark#(X2) | (178) |
mark#(pi(X)) | → | active#(pi(mark(X))) | (138) |
mark#(from(X)) | → | active#(from(mark(X))) | (77) |
active#(times(s(X),Y)) | → | mark#(plus(Y,times(X,Y))) | (81) |
mark#(2ndsneg(X1,X2)) | → | active#(2ndsneg(mark(X1),mark(X2))) | (164) |
active#(plus(0,Y)) | → | mark#(Y) | (168) |
active#(2ndsneg(s(N),cons(X,Z))) | → | mark#(2ndsneg(s(N),cons2(X,Z))) | (174) |
[negrecip(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | 26532 |
[rnil] | = | 1 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | 26531 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | 26531 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | 1 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 26532 |
[0] | = | 0 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | 26532 |
[times(x1, x2)] | = | 26532 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 1 |
[2ndsneg(x1, x2)] | = | 26532 |
[plus(x1, x2)] | = | 26532 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | 1 |
[from#(x1)] | = | 0 |
[active(x1)] | = | 1 |
[cons(x1, x2)] | = | 1 |
[active#(x1)] | = | x1 + 0 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | 1 |
mark(0) | → | active(0) | (18) |
posrecip(active(X)) | → | posrecip(X) | (50) |
active(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(posrecip(Y),2ndsneg(N,Z))) | (4) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (15) |
active(pi(X)) | → | mark(2ndspos(X,from(0))) | (8) |
2ndsneg(X1,active(X2)) | → | 2ndsneg(X1,X2) | (54) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (1) |
active(2ndspos(s(N),cons(X,Z))) | → | mark(2ndspos(s(N),cons2(X,Z))) | (3) |
mark(s(X)) | → | active(s(mark(X))) | (16) |
mark(rcons(X1,X2)) | → | active(rcons(mark(X1),mark(X2))) | (21) |
s(active(X)) | → | s(X) | (36) |
square(active(X)) | → | square(X) | (68) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (26) |
times(mark(X1),X2) | → | times(X1,X2) | (63) |
mark(rnil) | → | active(rnil) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (32) |
mark(2ndspos(X1,X2)) | → | active(2ndspos(mark(X1),mark(X2))) | (17) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (60) |
mark(times(X1,X2)) | → | active(times(mark(X1),mark(X2))) | (27) |
cons(X1,active(X2)) | → | cons(X1,X2) | (34) |
mark(posrecip(X)) | → | active(posrecip(mark(X))) | (22) |
mark(square(X)) | → | active(square(mark(X))) | (28) |
times(active(X1),X2) | → | times(X1,X2) | (65) |
cons2(X1,active(X2)) | → | cons2(X1,X2) | (44) |
active(2ndsneg(0,Z)) | → | mark(rnil) | (5) |
cons(active(X1),X2) | → | cons(X1,X2) | (33) |
times(X1,mark(X2)) | → | times(X1,X2) | (64) |
active(plus(s(X),Y)) | → | mark(s(plus(X,Y))) | (10) |
2ndspos(active(X1),X2) | → | 2ndspos(X1,X2) | (39) |
active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(negrecip(Y),2ndspos(N,Z))) | (7) |
mark(cons2(X1,X2)) | → | active(cons2(X1,mark(X2))) | (20) |
mark(pi(X)) | → | active(pi(mark(X))) | (25) |
posrecip(mark(X)) | → | posrecip(X) | (49) |
2ndsneg(X1,mark(X2)) | → | 2ndsneg(X1,X2) | (52) |
from(active(X)) | → | from(X) | (30) |
plus(X1,active(X2)) | → | plus(X1,X2) | (62) |
mark(from(X)) | → | active(from(mark(X))) | (14) |
negrecip(active(X)) | → | negrecip(X) | (56) |
cons(mark(X1),X2) | → | cons(X1,X2) | (31) |
active(times(s(X),Y)) | → | mark(plus(Y,times(X,Y))) | (12) |
rcons(mark(X1),X2) | → | rcons(X1,X2) | (45) |
mark(2ndsneg(X1,X2)) | → | active(2ndsneg(mark(X1),mark(X2))) | (23) |
mark(negrecip(X)) | → | active(negrecip(mark(X))) | (24) |
pi(mark(X)) | → | pi(X) | (57) |
active(times(0,Y)) | → | mark(0) | (11) |
active(plus(0,Y)) | → | mark(Y) | (9) |
active(square(X)) | → | mark(times(X,X)) | (13) |
2ndsneg(mark(X1),X2) | → | 2ndsneg(X1,X2) | (51) |
2ndspos(X1,active(X2)) | → | 2ndspos(X1,X2) | (40) |
square(mark(X)) | → | square(X) | (67) |
negrecip(mark(X)) | → | negrecip(X) | (55) |
plus(mark(X1),X2) | → | plus(X1,X2) | (59) |
active(2ndsneg(s(N),cons(X,Z))) | → | mark(2ndsneg(s(N),cons2(X,Z))) | (6) |
2ndspos(X1,mark(X2)) | → | 2ndspos(X1,X2) | (38) |
plus(active(X1),X2) | → | plus(X1,X2) | (61) |
pi(active(X)) | → | pi(X) | (58) |
rcons(X1,active(X2)) | → | rcons(X1,X2) | (48) |
2ndsneg(active(X1),X2) | → | 2ndsneg(X1,X2) | (53) |
rcons(active(X1),X2) | → | rcons(X1,X2) | (47) |
2ndspos(mark(X1),X2) | → | 2ndspos(X1,X2) | (37) |
cons2(mark(X1),X2) | → | cons2(X1,X2) | (41) |
cons2(X1,mark(X2)) | → | cons2(X1,X2) | (42) |
rcons(X1,mark(X2)) | → | rcons(X1,X2) | (46) |
times(X1,active(X2)) | → | times(X1,X2) | (66) |
s(mark(X)) | → | s(X) | (35) |
from(mark(X)) | → | from(X) | (29) |
cons2(active(X1),X2) | → | cons2(X1,X2) | (43) |
active(2ndspos(0,Z)) | → | mark(rnil) | (2) |
mark#(square(X)) | → | active#(square(mark(X))) | (171) |
mark#(pi(X)) | → | active#(pi(mark(X))) | (138) |
The dependency pairs are split into 1 component.
active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(posrecip(Y),2ndsneg(N,Z))) | (82) |
active#(from(X)) | → | mark#(cons(X,from(s(X)))) | (182) |
active#(2ndspos(s(N),cons(X,Z))) | → | mark#(2ndspos(s(N),cons2(X,Z))) | (169) |
mark#(s(X)) | → | mark#(X) | (83) |
mark#(rcons(X1,X2)) | → | mark#(X2) | (123) |
mark#(plus(X1,X2)) | → | mark#(X2) | (105) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (159) |
mark#(2ndspos(X1,X2)) | → | active#(2ndspos(mark(X1),mark(X2))) | (185) |
mark#(times(X1,X2)) | → | active#(times(mark(X1),mark(X2))) | (91) |
active#(plus(s(X),Y)) | → | mark#(s(plus(X,Y))) | (161) |
active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(negrecip(Y),2ndspos(N,Z))) | (102) |
mark#(cons2(X1,X2)) | → | mark#(X2) | (178) |
mark#(from(X)) | → | active#(from(mark(X))) | (77) |
active#(times(s(X),Y)) | → | mark#(plus(Y,times(X,Y))) | (81) |
mark#(2ndsneg(X1,X2)) | → | active#(2ndsneg(mark(X1),mark(X2))) | (164) |
active#(plus(0,Y)) | → | mark#(Y) | (168) |
active#(2ndsneg(s(N),cons(X,Z))) | → | mark#(2ndsneg(s(N),cons2(X,Z))) | (174) |
[negrecip(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | 1 |
[rnil] | = | 0 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 37749 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | 1 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x2 + 0 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | x1 + 26532 |
[0] | = | 0 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | 2 |
[times(x1, x2)] | = | 8855 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[2ndsneg(x1, x2)] | = | 1 |
[plus(x1, x2)] | = | x2 + 0 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x2 + 1 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | 1 |
[active#(x1)] | = | x1 + 26532 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | 18841 |
mark(0) | → | active(0) | (18) |
posrecip(active(X)) | → | posrecip(X) | (50) |
active(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(posrecip(Y),2ndsneg(N,Z))) | (4) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (15) |
active(pi(X)) | → | mark(2ndspos(X,from(0))) | (8) |
2ndsneg(X1,active(X2)) | → | 2ndsneg(X1,X2) | (54) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (1) |
active(2ndspos(s(N),cons(X,Z))) | → | mark(2ndspos(s(N),cons2(X,Z))) | (3) |
mark(s(X)) | → | active(s(mark(X))) | (16) |
mark(rcons(X1,X2)) | → | active(rcons(mark(X1),mark(X2))) | (21) |
s(active(X)) | → | s(X) | (36) |
square(active(X)) | → | square(X) | (68) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (26) |
times(mark(X1),X2) | → | times(X1,X2) | (63) |
mark(rnil) | → | active(rnil) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (32) |
mark(2ndspos(X1,X2)) | → | active(2ndspos(mark(X1),mark(X2))) | (17) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (60) |
mark(times(X1,X2)) | → | active(times(mark(X1),mark(X2))) | (27) |
cons(X1,active(X2)) | → | cons(X1,X2) | (34) |
mark(posrecip(X)) | → | active(posrecip(mark(X))) | (22) |
mark(square(X)) | → | active(square(mark(X))) | (28) |
times(active(X1),X2) | → | times(X1,X2) | (65) |
cons2(X1,active(X2)) | → | cons2(X1,X2) | (44) |
active(2ndsneg(0,Z)) | → | mark(rnil) | (5) |
cons(active(X1),X2) | → | cons(X1,X2) | (33) |
times(X1,mark(X2)) | → | times(X1,X2) | (64) |
active(plus(s(X),Y)) | → | mark(s(plus(X,Y))) | (10) |
2ndspos(active(X1),X2) | → | 2ndspos(X1,X2) | (39) |
active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(negrecip(Y),2ndspos(N,Z))) | (7) |
mark(cons2(X1,X2)) | → | active(cons2(X1,mark(X2))) | (20) |
mark(pi(X)) | → | active(pi(mark(X))) | (25) |
posrecip(mark(X)) | → | posrecip(X) | (49) |
2ndsneg(X1,mark(X2)) | → | 2ndsneg(X1,X2) | (52) |
from(active(X)) | → | from(X) | (30) |
plus(X1,active(X2)) | → | plus(X1,X2) | (62) |
mark(from(X)) | → | active(from(mark(X))) | (14) |
negrecip(active(X)) | → | negrecip(X) | (56) |
cons(mark(X1),X2) | → | cons(X1,X2) | (31) |
active(times(s(X),Y)) | → | mark(plus(Y,times(X,Y))) | (12) |
rcons(mark(X1),X2) | → | rcons(X1,X2) | (45) |
mark(2ndsneg(X1,X2)) | → | active(2ndsneg(mark(X1),mark(X2))) | (23) |
mark(negrecip(X)) | → | active(negrecip(mark(X))) | (24) |
pi(mark(X)) | → | pi(X) | (57) |
active(times(0,Y)) | → | mark(0) | (11) |
active(plus(0,Y)) | → | mark(Y) | (9) |
active(square(X)) | → | mark(times(X,X)) | (13) |
2ndsneg(mark(X1),X2) | → | 2ndsneg(X1,X2) | (51) |
2ndspos(X1,active(X2)) | → | 2ndspos(X1,X2) | (40) |
square(mark(X)) | → | square(X) | (67) |
negrecip(mark(X)) | → | negrecip(X) | (55) |
plus(mark(X1),X2) | → | plus(X1,X2) | (59) |
active(2ndsneg(s(N),cons(X,Z))) | → | mark(2ndsneg(s(N),cons2(X,Z))) | (6) |
2ndspos(X1,mark(X2)) | → | 2ndspos(X1,X2) | (38) |
plus(active(X1),X2) | → | plus(X1,X2) | (61) |
pi(active(X)) | → | pi(X) | (58) |
rcons(X1,active(X2)) | → | rcons(X1,X2) | (48) |
2ndsneg(active(X1),X2) | → | 2ndsneg(X1,X2) | (53) |
rcons(active(X1),X2) | → | rcons(X1,X2) | (47) |
2ndspos(mark(X1),X2) | → | 2ndspos(X1,X2) | (37) |
cons2(mark(X1),X2) | → | cons2(X1,X2) | (41) |
cons2(X1,mark(X2)) | → | cons2(X1,X2) | (42) |
rcons(X1,mark(X2)) | → | rcons(X1,X2) | (46) |
times(X1,active(X2)) | → | times(X1,X2) | (66) |
s(mark(X)) | → | s(X) | (35) |
from(mark(X)) | → | from(X) | (29) |
cons2(active(X1),X2) | → | cons2(X1,X2) | (43) |
active(2ndspos(0,Z)) | → | mark(rnil) | (2) |
active#(from(X)) | → | mark#(cons(X,from(s(X)))) | (182) |
mark#(cons2(X1,X2)) | → | mark#(X2) | (178) |
The dependency pairs are split into 1 component.
active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(posrecip(Y),2ndsneg(N,Z))) | (82) |
active#(2ndspos(s(N),cons(X,Z))) | → | mark#(2ndspos(s(N),cons2(X,Z))) | (169) |
mark#(s(X)) | → | mark#(X) | (83) |
mark#(rcons(X1,X2)) | → | mark#(X2) | (123) |
mark#(plus(X1,X2)) | → | mark#(X2) | (105) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (159) |
mark#(2ndspos(X1,X2)) | → | active#(2ndspos(mark(X1),mark(X2))) | (185) |
mark#(times(X1,X2)) | → | active#(times(mark(X1),mark(X2))) | (91) |
active#(plus(s(X),Y)) | → | mark#(s(plus(X,Y))) | (161) |
active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(negrecip(Y),2ndspos(N,Z))) | (102) |
mark#(from(X)) | → | active#(from(mark(X))) | (77) |
active#(times(s(X),Y)) | → | mark#(plus(Y,times(X,Y))) | (81) |
mark#(2ndsneg(X1,X2)) | → | active#(2ndsneg(mark(X1),mark(X2))) | (164) |
active#(plus(0,Y)) | → | mark#(Y) | (168) |
active#(2ndsneg(s(N),cons(X,Z))) | → | mark#(2ndsneg(s(N),cons2(X,Z))) | (174) |
[negrecip(x1)] | = | 12384 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 13259 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | 2 |
[rnil] | = | 1 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | 3699 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | 20860 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | 1 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 26534 |
[0] | = | 0 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | 1 |
[times(x1, x2)] | = | 2 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 0 |
[2ndsneg(x1, x2)] | = | 2 |
[plus(x1, x2)] | = | 2 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | 25644 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[cons(x1, x2)] | = | 13704 |
[active#(x1)] | = | x1 + 26532 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | 1 |
posrecip(active(X)) | → | posrecip(X) | (50) |
2ndsneg(X1,active(X2)) | → | 2ndsneg(X1,X2) | (54) |
s(active(X)) | → | s(X) | (36) |
square(active(X)) | → | square(X) | (68) |
times(mark(X1),X2) | → | times(X1,X2) | (63) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (32) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (60) |
cons(X1,active(X2)) | → | cons(X1,X2) | (34) |
times(active(X1),X2) | → | times(X1,X2) | (65) |
cons2(X1,active(X2)) | → | cons2(X1,X2) | (44) |
cons(active(X1),X2) | → | cons(X1,X2) | (33) |
times(X1,mark(X2)) | → | times(X1,X2) | (64) |
2ndspos(active(X1),X2) | → | 2ndspos(X1,X2) | (39) |
posrecip(mark(X)) | → | posrecip(X) | (49) |
2ndsneg(X1,mark(X2)) | → | 2ndsneg(X1,X2) | (52) |
from(active(X)) | → | from(X) | (30) |
plus(X1,active(X2)) | → | plus(X1,X2) | (62) |
negrecip(active(X)) | → | negrecip(X) | (56) |
cons(mark(X1),X2) | → | cons(X1,X2) | (31) |
rcons(mark(X1),X2) | → | rcons(X1,X2) | (45) |
pi(mark(X)) | → | pi(X) | (57) |
2ndsneg(mark(X1),X2) | → | 2ndsneg(X1,X2) | (51) |
2ndspos(X1,active(X2)) | → | 2ndspos(X1,X2) | (40) |
square(mark(X)) | → | square(X) | (67) |
negrecip(mark(X)) | → | negrecip(X) | (55) |
plus(mark(X1),X2) | → | plus(X1,X2) | (59) |
2ndspos(X1,mark(X2)) | → | 2ndspos(X1,X2) | (38) |
plus(active(X1),X2) | → | plus(X1,X2) | (61) |
pi(active(X)) | → | pi(X) | (58) |
rcons(X1,active(X2)) | → | rcons(X1,X2) | (48) |
2ndsneg(active(X1),X2) | → | 2ndsneg(X1,X2) | (53) |
rcons(active(X1),X2) | → | rcons(X1,X2) | (47) |
2ndspos(mark(X1),X2) | → | 2ndspos(X1,X2) | (37) |
cons2(mark(X1),X2) | → | cons2(X1,X2) | (41) |
cons2(X1,mark(X2)) | → | cons2(X1,X2) | (42) |
rcons(X1,mark(X2)) | → | rcons(X1,X2) | (46) |
times(X1,active(X2)) | → | times(X1,X2) | (66) |
s(mark(X)) | → | s(X) | (35) |
from(mark(X)) | → | from(X) | (29) |
cons2(active(X1),X2) | → | cons2(X1,X2) | (43) |
mark#(from(X)) | → | active#(from(mark(X))) | (77) |
The dependency pairs are split into 1 component.
active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(posrecip(Y),2ndsneg(N,Z))) | (82) |
active#(2ndspos(s(N),cons(X,Z))) | → | mark#(2ndspos(s(N),cons2(X,Z))) | (169) |
mark#(s(X)) | → | mark#(X) | (83) |
mark#(rcons(X1,X2)) | → | mark#(X2) | (123) |
mark#(plus(X1,X2)) | → | mark#(X2) | (105) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (159) |
mark#(2ndspos(X1,X2)) | → | active#(2ndspos(mark(X1),mark(X2))) | (185) |
mark#(times(X1,X2)) | → | active#(times(mark(X1),mark(X2))) | (91) |
active#(plus(s(X),Y)) | → | mark#(s(plus(X,Y))) | (161) |
active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(negrecip(Y),2ndspos(N,Z))) | (102) |
active#(times(s(X),Y)) | → | mark#(plus(Y,times(X,Y))) | (81) |
mark#(2ndsneg(X1,X2)) | → | active#(2ndsneg(mark(X1),mark(X2))) | (164) |
active#(plus(0,Y)) | → | mark#(Y) | (168) |
active#(2ndsneg(s(N),cons(X,Z))) | → | mark#(2ndsneg(s(N),cons2(X,Z))) | (174) |
π(2ndspos) | = | 1 |
π(rcons) | = | 2 |
π(mark#) | = | 1 |
π(mark) | = | 1 |
π(2ndsneg) | = | 1 |
π(cons2) | = | 1 |
π(active) | = | 1 |
π(active#) | = | 1 |
π(pi#) | = | 1 |
prec(negrecip) | = | 1 | status(negrecip) | = | [] | list-extension(negrecip) | = | Lex | ||
prec(cons#) | = | 0 | status(cons#) | = | [] | list-extension(cons#) | = | Lex | ||
prec(s) | = | 1 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(negrecip#) | = | 0 | status(negrecip#) | = | [] | list-extension(negrecip#) | = | Lex | ||
prec(rnil) | = | 2 | status(rnil) | = | [] | list-extension(rnil) | = | Lex | ||
prec(plus#) | = | 0 | status(plus#) | = | [1, 2] | list-extension(plus#) | = | Lex | ||
prec(square) | = | 4 | status(square) | = | [1] | list-extension(square) | = | Lex | ||
prec(cons2#) | = | 0 | status(cons2#) | = | [] | list-extension(cons2#) | = | Lex | ||
prec(square#) | = | 0 | status(square#) | = | [] | list-extension(square#) | = | Lex | ||
prec(pi) | = | 0 | status(pi) | = | [1] | list-extension(pi) | = | Lex | ||
prec(rcons#) | = | 0 | status(rcons#) | = | [1, 2] | list-extension(rcons#) | = | Lex | ||
prec(times#) | = | 0 | status(times#) | = | [] | list-extension(times#) | = | Lex | ||
prec(0) | = | 3 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(posrecip#) | = | 0 | status(posrecip#) | = | [] | list-extension(posrecip#) | = | Lex | ||
prec(from) | = | 0 | status(from) | = | [1] | list-extension(from) | = | Lex | ||
prec(times) | = | 3 | status(times) | = | [2, 1] | list-extension(times) | = | Lex | ||
prec(s#) | = | 0 | status(s#) | = | [] | list-extension(s#) | = | Lex | ||
prec(plus) | = | 2 | status(plus) | = | [1, 2] | list-extension(plus) | = | Lex | ||
prec(2ndspos#) | = | 0 | status(2ndspos#) | = | [1, 2] | list-extension(2ndspos#) | = | Lex | ||
prec(from#) | = | 0 | status(from#) | = | [] | list-extension(from#) | = | Lex | ||
prec(cons) | = | 0 | status(cons) | = | [1] | list-extension(cons) | = | Lex | ||
prec(2ndsneg#) | = | 0 | status(2ndsneg#) | = | [1, 2] | list-extension(2ndsneg#) | = | Lex | ||
prec(posrecip) | = | 1 | status(posrecip) | = | [] | list-extension(posrecip) | = | Lex |
[negrecip(x1)] | = | 0 |
[cons#(x1, x2)] | = | max(0) |
[s(x1)] | = | x1 + 0 |
[negrecip#(x1)] | = | 0 |
[rnil] | = | 0 |
[plus#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[square(x1)] | = | x1 + 0 |
[cons2#(x1, x2)] | = | max(0) |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 0 |
[rcons#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[times#(x1, x2)] | = | max(0) |
[0] | = | 0 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 0 |
[times(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[s#(x1)] | = | 0 |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[2ndspos#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[from#(x1)] | = | 0 |
[cons(x1, x2)] | = | max(x1 + 0, 0) |
[2ndsneg#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[posrecip(x1)] | = | 0 |
mark(0) | → | active(0) | (18) |
posrecip(active(X)) | → | posrecip(X) | (50) |
active(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(posrecip(Y),2ndsneg(N,Z))) | (4) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (15) |
active(pi(X)) | → | mark(2ndspos(X,from(0))) | (8) |
2ndsneg(X1,active(X2)) | → | 2ndsneg(X1,X2) | (54) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (1) |
active(2ndspos(s(N),cons(X,Z))) | → | mark(2ndspos(s(N),cons2(X,Z))) | (3) |
mark(s(X)) | → | active(s(mark(X))) | (16) |
mark(rcons(X1,X2)) | → | active(rcons(mark(X1),mark(X2))) | (21) |
s(active(X)) | → | s(X) | (36) |
square(active(X)) | → | square(X) | (68) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (26) |
times(mark(X1),X2) | → | times(X1,X2) | (63) |
mark(rnil) | → | active(rnil) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (32) |
mark(2ndspos(X1,X2)) | → | active(2ndspos(mark(X1),mark(X2))) | (17) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (60) |
mark(times(X1,X2)) | → | active(times(mark(X1),mark(X2))) | (27) |
cons(X1,active(X2)) | → | cons(X1,X2) | (34) |
mark(posrecip(X)) | → | active(posrecip(mark(X))) | (22) |
mark(square(X)) | → | active(square(mark(X))) | (28) |
times(active(X1),X2) | → | times(X1,X2) | (65) |
cons2(X1,active(X2)) | → | cons2(X1,X2) | (44) |
active(2ndsneg(0,Z)) | → | mark(rnil) | (5) |
cons(active(X1),X2) | → | cons(X1,X2) | (33) |
times(X1,mark(X2)) | → | times(X1,X2) | (64) |
active(plus(s(X),Y)) | → | mark(s(plus(X,Y))) | (10) |
2ndspos(active(X1),X2) | → | 2ndspos(X1,X2) | (39) |
active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(negrecip(Y),2ndspos(N,Z))) | (7) |
mark(cons2(X1,X2)) | → | active(cons2(X1,mark(X2))) | (20) |
mark(pi(X)) | → | active(pi(mark(X))) | (25) |
posrecip(mark(X)) | → | posrecip(X) | (49) |
2ndsneg(X1,mark(X2)) | → | 2ndsneg(X1,X2) | (52) |
from(active(X)) | → | from(X) | (30) |
plus(X1,active(X2)) | → | plus(X1,X2) | (62) |
mark(from(X)) | → | active(from(mark(X))) | (14) |
negrecip(active(X)) | → | negrecip(X) | (56) |
cons(mark(X1),X2) | → | cons(X1,X2) | (31) |
active(times(s(X),Y)) | → | mark(plus(Y,times(X,Y))) | (12) |
rcons(mark(X1),X2) | → | rcons(X1,X2) | (45) |
mark(2ndsneg(X1,X2)) | → | active(2ndsneg(mark(X1),mark(X2))) | (23) |
mark(negrecip(X)) | → | active(negrecip(mark(X))) | (24) |
pi(mark(X)) | → | pi(X) | (57) |
active(times(0,Y)) | → | mark(0) | (11) |
active(plus(0,Y)) | → | mark(Y) | (9) |
active(square(X)) | → | mark(times(X,X)) | (13) |
2ndsneg(mark(X1),X2) | → | 2ndsneg(X1,X2) | (51) |
2ndspos(X1,active(X2)) | → | 2ndspos(X1,X2) | (40) |
square(mark(X)) | → | square(X) | (67) |
negrecip(mark(X)) | → | negrecip(X) | (55) |
plus(mark(X1),X2) | → | plus(X1,X2) | (59) |
active(2ndsneg(s(N),cons(X,Z))) | → | mark(2ndsneg(s(N),cons2(X,Z))) | (6) |
2ndspos(X1,mark(X2)) | → | 2ndspos(X1,X2) | (38) |
plus(active(X1),X2) | → | plus(X1,X2) | (61) |
pi(active(X)) | → | pi(X) | (58) |
rcons(X1,active(X2)) | → | rcons(X1,X2) | (48) |
2ndsneg(active(X1),X2) | → | 2ndsneg(X1,X2) | (53) |
rcons(active(X1),X2) | → | rcons(X1,X2) | (47) |
2ndspos(mark(X1),X2) | → | 2ndspos(X1,X2) | (37) |
cons2(mark(X1),X2) | → | cons2(X1,X2) | (41) |
cons2(X1,mark(X2)) | → | cons2(X1,X2) | (42) |
rcons(X1,mark(X2)) | → | rcons(X1,X2) | (46) |
times(X1,active(X2)) | → | times(X1,X2) | (66) |
s(mark(X)) | → | s(X) | (35) |
from(mark(X)) | → | from(X) | (29) |
cons2(active(X1),X2) | → | cons2(X1,X2) | (43) |
active(2ndspos(0,Z)) | → | mark(rnil) | (2) |
active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(posrecip(Y),2ndsneg(N,Z))) | (82) |
mark#(s(X)) | → | mark#(X) | (83) |
mark#(plus(X1,X2)) | → | mark#(X2) | (105) |
active#(plus(s(X),Y)) | → | mark#(s(plus(X,Y))) | (161) |
active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark#(rcons(negrecip(Y),2ndspos(N,Z))) | (102) |
active#(times(s(X),Y)) | → | mark#(plus(Y,times(X,Y))) | (81) |
active#(plus(0,Y)) | → | mark#(Y) | (168) |
The dependency pairs are split into 1 component.
active#(2ndspos(s(N),cons(X,Z))) | → | mark#(2ndspos(s(N),cons2(X,Z))) | (169) |
mark#(rcons(X1,X2)) | → | mark#(X2) | (123) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (159) |
mark#(2ndspos(X1,X2)) | → | active#(2ndspos(mark(X1),mark(X2))) | (185) |
mark#(times(X1,X2)) | → | active#(times(mark(X1),mark(X2))) | (91) |
mark#(2ndsneg(X1,X2)) | → | active#(2ndsneg(mark(X1),mark(X2))) | (164) |
active#(2ndsneg(s(N),cons(X,Z))) | → | mark#(2ndsneg(s(N),cons2(X,Z))) | (174) |
[negrecip(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 0 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | 43985 |
[rnil] | = | 43991 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 43984 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | 43983 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x2 + 11453 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | x1 + 26534 |
[0] | = | 4 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | 39891 |
[times(x1, x2)] | = | x1 + 43986 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + 43985 |
[plus(x1, x2)] | = | 43988 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | 36725 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | x1 + 39893 |
[active#(x1)] | = | 70519 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | 1 |
2ndsneg(X1,active(X2)) | → | 2ndsneg(X1,X2) | (54) |
s(active(X)) | → | s(X) | (36) |
times(mark(X1),X2) | → | times(X1,X2) | (63) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (32) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (60) |
cons(X1,active(X2)) | → | cons(X1,X2) | (34) |
times(active(X1),X2) | → | times(X1,X2) | (65) |
cons(active(X1),X2) | → | cons(X1,X2) | (33) |
times(X1,mark(X2)) | → | times(X1,X2) | (64) |
2ndspos(active(X1),X2) | → | 2ndspos(X1,X2) | (39) |
2ndsneg(X1,mark(X2)) | → | 2ndsneg(X1,X2) | (52) |
plus(X1,active(X2)) | → | plus(X1,X2) | (62) |
cons(mark(X1),X2) | → | cons(X1,X2) | (31) |
rcons(mark(X1),X2) | → | rcons(X1,X2) | (45) |
2ndsneg(mark(X1),X2) | → | 2ndsneg(X1,X2) | (51) |
2ndspos(X1,active(X2)) | → | 2ndspos(X1,X2) | (40) |
plus(mark(X1),X2) | → | plus(X1,X2) | (59) |
2ndspos(X1,mark(X2)) | → | 2ndspos(X1,X2) | (38) |
plus(active(X1),X2) | → | plus(X1,X2) | (61) |
rcons(X1,active(X2)) | → | rcons(X1,X2) | (48) |
2ndsneg(active(X1),X2) | → | 2ndsneg(X1,X2) | (53) |
rcons(active(X1),X2) | → | rcons(X1,X2) | (47) |
2ndspos(mark(X1),X2) | → | 2ndspos(X1,X2) | (37) |
rcons(X1,mark(X2)) | → | rcons(X1,X2) | (46) |
times(X1,active(X2)) | → | times(X1,X2) | (66) |
s(mark(X)) | → | s(X) | (35) |
mark#(rcons(X1,X2)) | → | mark#(X2) | (123) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (159) |
mark#(times(X1,X2)) | → | active#(times(mark(X1),mark(X2))) | (91) |
The dependency pairs are split into 1 component.
active#(2ndspos(s(N),cons(X,Z))) | → | mark#(2ndspos(s(N),cons2(X,Z))) | (169) |
mark#(2ndspos(X1,X2)) | → | active#(2ndspos(mark(X1),mark(X2))) | (185) |
mark#(2ndsneg(X1,X2)) | → | active#(2ndsneg(mark(X1),mark(X2))) | (164) |
active#(2ndsneg(s(N),cons(X,Z))) | → | mark#(2ndsneg(s(N),cons2(X,Z))) | (174) |
[negrecip(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 0 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x2 + 30116 |
[rnil] | = | 858 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 41961 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | 59541 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | 878 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | x1 + 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 29424 |
[times(x1, x2)] | = | x2 + 32664 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[2ndsneg(x1, x2)] | = | x2 + 4453 |
[plus(x1, x2)] | = | x2 + 0 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | 29422 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | x1 + 29424 |
[active#(x1)] | = | x1 + 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | 1 |
mark(0) | → | active(0) | (18) |
posrecip(active(X)) | → | posrecip(X) | (50) |
active(2ndspos(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(posrecip(Y),2ndsneg(N,Z))) | (4) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (15) |
active(pi(X)) | → | mark(2ndspos(X,from(0))) | (8) |
2ndsneg(X1,active(X2)) | → | 2ndsneg(X1,X2) | (54) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (1) |
active(2ndspos(s(N),cons(X,Z))) | → | mark(2ndspos(s(N),cons2(X,Z))) | (3) |
mark(s(X)) | → | active(s(mark(X))) | (16) |
mark(rcons(X1,X2)) | → | active(rcons(mark(X1),mark(X2))) | (21) |
s(active(X)) | → | s(X) | (36) |
square(active(X)) | → | square(X) | (68) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (26) |
times(mark(X1),X2) | → | times(X1,X2) | (63) |
mark(rnil) | → | active(rnil) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (32) |
mark(2ndspos(X1,X2)) | → | active(2ndspos(mark(X1),mark(X2))) | (17) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (60) |
mark(times(X1,X2)) | → | active(times(mark(X1),mark(X2))) | (27) |
cons(X1,active(X2)) | → | cons(X1,X2) | (34) |
mark(posrecip(X)) | → | active(posrecip(mark(X))) | (22) |
mark(square(X)) | → | active(square(mark(X))) | (28) |
times(active(X1),X2) | → | times(X1,X2) | (65) |
cons2(X1,active(X2)) | → | cons2(X1,X2) | (44) |
active(2ndsneg(0,Z)) | → | mark(rnil) | (5) |
cons(active(X1),X2) | → | cons(X1,X2) | (33) |
times(X1,mark(X2)) | → | times(X1,X2) | (64) |
active(plus(s(X),Y)) | → | mark(s(plus(X,Y))) | (10) |
2ndspos(active(X1),X2) | → | 2ndspos(X1,X2) | (39) |
active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) | → | mark(rcons(negrecip(Y),2ndspos(N,Z))) | (7) |
mark(cons2(X1,X2)) | → | active(cons2(X1,mark(X2))) | (20) |
mark(pi(X)) | → | active(pi(mark(X))) | (25) |
posrecip(mark(X)) | → | posrecip(X) | (49) |
2ndsneg(X1,mark(X2)) | → | 2ndsneg(X1,X2) | (52) |
from(active(X)) | → | from(X) | (30) |
plus(X1,active(X2)) | → | plus(X1,X2) | (62) |
mark(from(X)) | → | active(from(mark(X))) | (14) |
negrecip(active(X)) | → | negrecip(X) | (56) |
cons(mark(X1),X2) | → | cons(X1,X2) | (31) |
active(times(s(X),Y)) | → | mark(plus(Y,times(X,Y))) | (12) |
rcons(mark(X1),X2) | → | rcons(X1,X2) | (45) |
mark(2ndsneg(X1,X2)) | → | active(2ndsneg(mark(X1),mark(X2))) | (23) |
mark(negrecip(X)) | → | active(negrecip(mark(X))) | (24) |
pi(mark(X)) | → | pi(X) | (57) |
active(times(0,Y)) | → | mark(0) | (11) |
active(plus(0,Y)) | → | mark(Y) | (9) |
active(square(X)) | → | mark(times(X,X)) | (13) |
2ndsneg(mark(X1),X2) | → | 2ndsneg(X1,X2) | (51) |
2ndspos(X1,active(X2)) | → | 2ndspos(X1,X2) | (40) |
square(mark(X)) | → | square(X) | (67) |
negrecip(mark(X)) | → | negrecip(X) | (55) |
plus(mark(X1),X2) | → | plus(X1,X2) | (59) |
active(2ndsneg(s(N),cons(X,Z))) | → | mark(2ndsneg(s(N),cons2(X,Z))) | (6) |
2ndspos(X1,mark(X2)) | → | 2ndspos(X1,X2) | (38) |
plus(active(X1),X2) | → | plus(X1,X2) | (61) |
pi(active(X)) | → | pi(X) | (58) |
rcons(X1,active(X2)) | → | rcons(X1,X2) | (48) |
2ndsneg(active(X1),X2) | → | 2ndsneg(X1,X2) | (53) |
rcons(active(X1),X2) | → | rcons(X1,X2) | (47) |
2ndspos(mark(X1),X2) | → | 2ndspos(X1,X2) | (37) |
cons2(mark(X1),X2) | → | cons2(X1,X2) | (41) |
cons2(X1,mark(X2)) | → | cons2(X1,X2) | (42) |
rcons(X1,mark(X2)) | → | rcons(X1,X2) | (46) |
times(X1,active(X2)) | → | times(X1,X2) | (66) |
s(mark(X)) | → | s(X) | (35) |
from(mark(X)) | → | from(X) | (29) |
cons2(active(X1),X2) | → | cons2(X1,X2) | (43) |
active(2ndspos(0,Z)) | → | mark(rnil) | (2) |
active#(2ndspos(s(N),cons(X,Z))) | → | mark#(2ndspos(s(N),cons2(X,Z))) | (169) |
mark#(2ndspos(X1,X2)) | → | active#(2ndspos(mark(X1),mark(X2))) | (185) |
mark#(2ndsneg(X1,X2)) | → | active#(2ndsneg(mark(X1),mark(X2))) | (164) |
active#(2ndsneg(s(N),cons(X,Z))) | → | mark#(2ndsneg(s(N),cons2(X,Z))) | (174) |
The dependency pairs are split into 0 components.
pi#(active(X)) | → | pi#(X) | (108) |
pi#(mark(X)) | → | pi#(X) | (155) |
[negrecip(x1)] | = | 66 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1685 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x2 + 8017 |
[rnil] | = | 8019 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 31370 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 20955 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 1684 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 63765 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | 12940 |
[times(x1, x2)] | = | x2 + 63763 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | 1748 |
[plus(x1, x2)] | = | x2 + 1683 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x2 + 12944 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | x1 + 12942 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | x1 + 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 32221 |
s(active(X)) | → | s(X) | (36) |
cons2(X1,active(X2)) | → | cons2(X1,X2) | (44) |
cons2(mark(X1),X2) | → | cons2(X1,X2) | (41) |
cons2(X1,mark(X2)) | → | cons2(X1,X2) | (42) |
s(mark(X)) | → | s(X) | (35) |
cons2(active(X1),X2) | → | cons2(X1,X2) | (43) |
pi#(active(X)) | → | pi#(X) | (108) |
pi#(mark(X)) | → | pi#(X) | (155) |
The dependency pairs are split into 0 components.
square#(mark(X)) | → | square#(X) | (173) |
square#(active(X)) | → | square#(X) | (85) |
[negrecip(x1)] | = | 115887 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 16801 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x2 + 19148 |
[rnil] | = | 95847 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 18229 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | x1 + 0 |
[pi(x1)] | = | x1 + 31848 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 6332 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 63765 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 36665 |
[times(x1, x2)] | = | x1 + x2 + 18231 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 32080 |
[plus(x1, x2)] | = | 35034 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 36669 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 36667 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 86154 |
square#(mark(X)) | → | square#(X) | (173) |
square#(active(X)) | → | square#(X) | (85) |
The dependency pairs are split into 0 components.
plus#(active(X1),X2) | → | plus#(X1,X2) | (133) |
plus#(X1,mark(X2)) | → | plus#(X1,X2) | (128) |
plus#(X1,active(X2)) | → | plus#(X1,X2) | (122) |
plus#(mark(X1),X2) | → | plus#(X1,X2) | (165) |
[negrecip(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x2 + 1 |
[rnil] | = | 4 |
[plus#(x1, x2)] | = | x1 + x2 + 0 |
[square(x1)] | = | x1 + 1 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 1 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 6332 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 1 |
[times(x1, x2)] | = | x1 + x2 + 1132 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 1 |
[plus(x1, x2)] | = | 4342 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 5 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 3 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 1 |
plus#(active(X1),X2) | → | plus#(X1,X2) | (133) |
plus#(X1,mark(X2)) | → | plus#(X1,X2) | (128) |
plus#(X1,active(X2)) | → | plus#(X1,X2) | (122) |
plus#(mark(X1),X2) | → | plus#(X1,X2) | (165) |
The dependency pairs are split into 0 components.
s#(mark(X)) | → | s#(X) | (183) |
s#(active(X)) | → | s#(X) | (146) |
[negrecip(x1)] | = | 15037 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x2 + 7942 |
[rnil] | = | 9625 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 16772 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 17534 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 122421 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 63913 |
[times(x1, x2)] | = | x1 + x2 + 16774 |
[s#(x1)] | = | x1 + 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 9622 |
[plus(x1, x2)] | = | 16778 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 63917 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 63915 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 59155 |
s#(mark(X)) | → | s#(X) | (183) |
s#(active(X)) | → | s#(X) | (146) |
The dependency pairs are split into 0 components.
2ndspos#(X1,mark(X2)) | → | 2ndspos#(X1,X2) | (180) |
2ndspos#(mark(X1),X2) | → | 2ndspos#(X1,X2) | (109) |
2ndspos#(active(X1),X2) | → | 2ndspos#(X1,X2) | (100) |
2ndspos#(X1,active(X2)) | → | 2ndspos#(X1,X2) | (156) |
[negrecip(x1)] | = | 12 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x2 + 1 |
[rnil] | = | 34899 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 1 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 1 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 1 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 34896 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 1 |
[times(x1, x2)] | = | x1 + x2 + 3 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 1 |
[plus(x1, x2)] | = | 7 |
[2ndspos#(x1, x2)] | = | x1 + 0 |
[cons2(x1, x2)] | = | x1 + x2 + 5 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 3 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 63920 |
2ndspos#(mark(X1),X2) | → | 2ndspos#(X1,X2) | (109) |
2ndspos#(active(X1),X2) | → | 2ndspos#(X1,X2) | (100) |
The dependency pairs are split into 1 component.
2ndspos#(X1,active(X2)) | → | 2ndspos#(X1,X2) | (156) |
2ndspos#(X1,mark(X2)) | → | 2ndspos#(X1,X2) | (180) |
[negrecip(x1)] | = | 80825 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 22463 |
[rnil] | = | 22466 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 5560 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 55430 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 962 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 32968 |
[times(x1, x2)] | = | x1 + x2 + 5562 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 15841 |
[plus(x1, x2)] | = | 5566 |
[2ndspos#(x1, x2)] | = | x2 + 0 |
[cons2(x1, x2)] | = | x1 + x2 + 32972 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 32970 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 87447 |
2ndspos#(X1,active(X2)) | → | 2ndspos#(X1,X2) | (156) |
2ndspos#(X1,mark(X2)) | → | 2ndspos#(X1,X2) | (180) |
The dependency pairs are split into 0 components.
cons#(mark(X1),X2) | → | cons#(X1,X2) | (104) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (158) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (93) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (149) |
[negrecip(x1)] | = | 10128 |
[cons#(x1, x2)] | = | x1 + x2 + 0 |
[s(x1)] | = | x1 + 1751 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 1 |
[rnil] | = | 4 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 58000 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 1 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 60191 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 1 |
[times(x1, x2)] | = | x1 + x2 + 58002 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 1 |
[plus(x1, x2)] | = | 59755 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 29220 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 29218 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 1 |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (104) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (158) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (93) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (149) |
The dependency pairs are split into 0 components.
rcons#(X1,active(X2)) | → | rcons#(X1,X2) | (126) |
rcons#(mark(X1),X2) | → | rcons#(X1,X2) | (172) |
rcons#(X1,mark(X2)) | → | rcons#(X1,X2) | (99) |
rcons#(active(X1),X2) | → | rcons#(X1,X2) | (145) |
[negrecip(x1)] | = | 22534 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 1 |
[rnil] | = | 5 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 1 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 1 |
[rcons#(x1, x2)] | = | x1 + x2 + 0 |
[rcons(x1, x2)] | = | x1 + 4105 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 1 |
[times(x1, x2)] | = | x1 + x2 + 3 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 1 |
[plus(x1, x2)] | = | 7 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 13318 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 13316 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 22534 |
rcons#(X1,active(X2)) | → | rcons#(X1,X2) | (126) |
rcons#(mark(X1),X2) | → | rcons#(X1,X2) | (172) |
rcons#(X1,mark(X2)) | → | rcons#(X1,X2) | (99) |
rcons#(active(X1),X2) | → | rcons#(X1,X2) | (145) |
The dependency pairs are split into 0 components.
posrecip#(active(X)) | → | posrecip#(X) | (120) |
posrecip#(mark(X)) | → | posrecip#(X) | (90) |
[negrecip(x1)] | = | 32021 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 16995 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 10034 |
[rnil] | = | 50069 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 46623 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 14473 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 90318 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | x1 + 0 |
[from(x1)] | = | x1 + 4440 |
[times(x1, x2)] | = | x1 + x2 + 46625 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 50066 |
[plus(x1, x2)] | = | 63622 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 27639 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 27637 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 28468 |
posrecip#(active(X)) | → | posrecip#(X) | (120) |
posrecip#(mark(X)) | → | posrecip#(X) | (90) |
The dependency pairs are split into 0 components.
2ndsneg#(mark(X1),X2) | → | 2ndsneg#(X1,X2) | (118) |
2ndsneg#(active(X1),X2) | → | 2ndsneg#(X1,X2) | (110) |
2ndsneg#(X1,active(X2)) | → | 2ndsneg#(X1,X2) | (106) |
2ndsneg#(X1,mark(X2)) | → | 2ndsneg#(X1,X2) | (87) |
[negrecip(x1)] | = | 41476 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 30361 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 1 |
[rnil] | = | 10090 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 16458 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 1 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 16804 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 1 |
[times(x1, x2)] | = | x1 + x2 + 16460 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 10087 |
[plus(x1, x2)] | = | 63622 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 8916 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 8914 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | x1 + x2 + 0 |
[posrecip(x1)] | = | x1 + 31390 |
2ndsneg#(mark(X1),X2) | → | 2ndsneg#(X1,X2) | (118) |
2ndsneg#(active(X1),X2) | → | 2ndsneg#(X1,X2) | (110) |
2ndsneg#(X1,active(X2)) | → | 2ndsneg#(X1,X2) | (106) |
2ndsneg#(X1,mark(X2)) | → | 2ndsneg#(X1,X2) | (87) |
The dependency pairs are split into 0 components.
times#(X1,mark(X2)) | → | times#(X1,X2) | (166) |
times#(active(X1),X2) | → | times#(X1,X2) | (103) |
times#(X1,active(X2)) | → | times#(X1,X2) | (152) |
times#(mark(X1),X2) | → | times#(X1,X2) | (70) |
[negrecip(x1)] | = | 41476 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 1 |
[rnil] | = | 4 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 27378 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 1 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 1 |
[times#(x1, x2)] | = | x1 + 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 1 |
[times(x1, x2)] | = | x1 + x2 + 27380 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 1 |
[plus(x1, x2)] | = | 27384 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 5 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 3 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 12 |
times#(active(X1),X2) | → | times#(X1,X2) | (103) |
times#(mark(X1),X2) | → | times#(X1,X2) | (70) |
The dependency pairs are split into 1 component.
times#(X1,mark(X2)) | → | times#(X1,X2) | (166) |
times#(X1,active(X2)) | → | times#(X1,X2) | (152) |
[negrecip(x1)] | = | 64973 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 32240 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 1 |
[rnil] | = | 48487 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 8473 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 1 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 25377 |
[times#(x1, x2)] | = | x2 + 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 1 |
[times(x1, x2)] | = | x1 + x2 + 8475 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 48484 |
[plus(x1, x2)] | = | 40717 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 4813 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 4811 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 16490 |
times#(X1,mark(X2)) | → | times#(X1,X2) | (166) |
times#(X1,active(X2)) | → | times#(X1,X2) | (152) |
The dependency pairs are split into 0 components.
from#(mark(X)) | → | from#(X) | (175) |
from#(active(X)) | → | from#(X) | (76) |
[negrecip(x1)] | = | 9327 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 20367 |
[rnil] | = | 48787 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 33106 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 73862 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 71630 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 24944 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 28553 |
[times(x1, x2)] | = | x1 + x2 + 33108 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 23841 |
[plus(x1, x2)] | = | 33112 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 28557 |
[from#(x1)] | = | x1 + 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 28555 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 40131 |
from#(mark(X)) | → | from#(X) | (175) |
from#(active(X)) | → | from#(X) | (76) |
The dependency pairs are split into 0 components.
cons2#(mark(X1),X2) | → | cons2#(X1,X2) | (179) |
cons2#(X1,active(X2)) | → | cons2#(X1,X2) | (75) |
cons2#(X1,mark(X2)) | → | cons2#(X1,X2) | (143) |
cons2#(active(X1),X2) | → | cons2#(X1,X2) | (69) |
[negrecip(x1)] | = | 9327 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 14022 |
[rnil] | = | 50896 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 1 |
[cons2#(x1, x2)] | = | x2 + 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 1 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 38347 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 36872 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 21093 |
[times(x1, x2)] | = | x1 + x2 + 3 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 3123 |
[plus(x1, x2)] | = | 13 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 21097 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 21095 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 40133 |
cons2#(X1,active(X2)) | → | cons2#(X1,X2) | (75) |
cons2#(X1,mark(X2)) | → | cons2#(X1,X2) | (143) |
The dependency pairs are split into 1 component.
cons2#(mark(X1),X2) | → | cons2#(X1,X2) | (179) |
cons2#(active(X1),X2) | → | cons2#(X1,X2) | (69) |
[negrecip(x1)] | = | 74205 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[negrecip#(x1)] | = | 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 29219 |
[rnil] | = | 50896 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 1 |
[cons2#(x1, x2)] | = | x1 + 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 3138 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 15882 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 37432 |
[times(x1, x2)] | = | x1 + x2 + 3 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 15213 |
[plus(x1, x2)] | = | 7 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 37436 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 37434 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 88211 |
cons2#(mark(X1),X2) | → | cons2#(X1,X2) | (179) |
cons2#(active(X1),X2) | → | cons2#(X1,X2) | (69) |
The dependency pairs are split into 0 components.
negrecip#(active(X)) | → | negrecip#(X) | (80) |
negrecip#(mark(X)) | → | negrecip#(X) | (141) |
[negrecip(x1)] | = | 24859 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[negrecip#(x1)] | = | x1 + 0 |
[2ndspos(x1, x2)] | = | x1 + x2 + 585 |
[rnil] | = | 588 |
[plus#(x1, x2)] | = | 0 |
[square(x1)] | = | x1 + 3714 |
[cons2#(x1, x2)] | = | 0 |
[square#(x1)] | = | 0 |
[pi(x1)] | = | x1 + 585 |
[rcons#(x1, x2)] | = | 0 |
[rcons(x1, x2)] | = | x1 + 800 |
[times#(x1, x2)] | = | 0 |
[mark#(x1)] | = | 70519 |
[0] | = | 1 |
[posrecip#(x1)] | = | 0 |
[from(x1)] | = | x1 + 1 |
[times(x1, x2)] | = | x1 + x2 + 3716 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[2ndsneg(x1, x2)] | = | x1 + x2 + 507 |
[plus(x1, x2)] | = | 3720 |
[2ndspos#(x1, x2)] | = | 0 |
[cons2(x1, x2)] | = | x1 + x2 + 12575 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 12573 |
[active#(x1)] | = | 70518 |
[pi#(x1)] | = | 0 |
[2ndsneg#(x1, x2)] | = | 0 |
[posrecip(x1)] | = | x1 + 24937 |
negrecip#(active(X)) | → | negrecip#(X) | (80) |
negrecip#(mark(X)) | → | negrecip#(X) | (141) |
The dependency pairs are split into 0 components.