The rewrite relation of the following TRS is considered.
active(fst(0,Z)) | → | mark(nil) | (1) |
active(fst(s(X),cons(Y,Z))) | → | mark(cons(Y,fst(X,Z))) | (2) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (3) |
active(add(0,X)) | → | mark(X) | (4) |
active(add(s(X),Y)) | → | mark(s(add(X,Y))) | (5) |
active(len(nil)) | → | mark(0) | (6) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
active(cons(X1,X2)) | → | cons(active(X1),X2) | (8) |
active(fst(X1,X2)) | → | fst(active(X1),X2) | (9) |
active(fst(X1,X2)) | → | fst(X1,active(X2)) | (10) |
active(from(X)) | → | from(active(X)) | (11) |
active(add(X1,X2)) | → | add(active(X1),X2) | (12) |
active(add(X1,X2)) | → | add(X1,active(X2)) | (13) |
active(len(X)) | → | len(active(X)) | (14) |
cons(mark(X1),X2) | → | mark(cons(X1,X2)) | (15) |
fst(mark(X1),X2) | → | mark(fst(X1,X2)) | (16) |
fst(X1,mark(X2)) | → | mark(fst(X1,X2)) | (17) |
from(mark(X)) | → | mark(from(X)) | (18) |
add(mark(X1),X2) | → | mark(add(X1,X2)) | (19) |
add(X1,mark(X2)) | → | mark(add(X1,X2)) | (20) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(0) | → | ok(0) | (22) |
proper(s(X)) | → | s(proper(X)) | (23) |
proper(nil) | → | ok(nil) | (24) |
proper(cons(X1,X2)) | → | cons(proper(X1),proper(X2)) | (25) |
proper(fst(X1,X2)) | → | fst(proper(X1),proper(X2)) | (26) |
proper(from(X)) | → | from(proper(X)) | (27) |
proper(add(X1,X2)) | → | add(proper(X1),proper(X2)) | (28) |
proper(len(X)) | → | len(proper(X)) | (29) |
s(ok(X)) | → | ok(s(X)) | (30) |
cons(ok(X1),ok(X2)) | → | ok(cons(X1,X2)) | (31) |
fst(ok(X1),ok(X2)) | → | ok(fst(X1,X2)) | (32) |
from(ok(X)) | → | ok(from(X)) | (33) |
add(ok(X1),ok(X2)) | → | ok(add(X1,X2)) | (34) |
len(ok(X)) | → | ok(len(X)) | (35) |
top(mark(X)) | → | top(proper(X)) | (36) |
top(ok(X)) | → | top(active(X)) | (37) |
active#(fst(s(X),cons(Y,Z))) | → | fst#(X,Z) | (38) |
proper#(fst(X1,X2)) | → | proper#(X1) | (39) |
active#(fst(X1,X2)) | → | active#(X2) | (40) |
proper#(add(X1,X2)) | → | proper#(X2) | (41) |
top#(mark(X)) | → | proper#(X) | (42) |
proper#(fst(X1,X2)) | → | fst#(proper(X1),proper(X2)) | (43) |
add#(mark(X1),X2) | → | add#(X1,X2) | (44) |
proper#(from(X)) | → | from#(proper(X)) | (45) |
len#(mark(X)) | → | len#(X) | (46) |
active#(cons(X1,X2)) | → | active#(X1) | (47) |
fst#(mark(X1),X2) | → | fst#(X1,X2) | (48) |
proper#(from(X)) | → | proper#(X) | (49) |
top#(ok(X)) | → | top#(active(X)) | (50) |
from#(mark(X)) | → | from#(X) | (51) |
fst#(ok(X1),ok(X2)) | → | fst#(X1,X2) | (52) |
active#(from(X)) | → | s#(X) | (53) |
active#(from(X)) | → | active#(X) | (54) |
active#(add(X1,X2)) | → | active#(X2) | (55) |
active#(fst(X1,X2)) | → | active#(X1) | (56) |
proper#(cons(X1,X2)) | → | proper#(X2) | (57) |
proper#(cons(X1,X2)) | → | proper#(X1) | (58) |
top#(mark(X)) | → | top#(proper(X)) | (59) |
active#(from(X)) | → | from#(active(X)) | (60) |
active#(add(s(X),Y)) | → | s#(add(X,Y)) | (61) |
proper#(s(X)) | → | s#(proper(X)) | (62) |
from#(ok(X)) | → | from#(X) | (63) |
active#(cons(X1,X2)) | → | cons#(active(X1),X2) | (64) |
active#(from(X)) | → | cons#(X,from(s(X))) | (65) |
add#(X1,mark(X2)) | → | add#(X1,X2) | (66) |
active#(len(X)) | → | active#(X) | (67) |
top#(ok(X)) | → | active#(X) | (68) |
fst#(X1,mark(X2)) | → | fst#(X1,X2) | (69) |
active#(fst(X1,X2)) | → | fst#(active(X1),X2) | (70) |
proper#(add(X1,X2)) | → | add#(proper(X1),proper(X2)) | (71) |
len#(ok(X)) | → | len#(X) | (72) |
proper#(fst(X1,X2)) | → | proper#(X2) | (73) |
active#(fst(X1,X2)) | → | fst#(X1,active(X2)) | (74) |
proper#(cons(X1,X2)) | → | cons#(proper(X1),proper(X2)) | (75) |
proper#(add(X1,X2)) | → | proper#(X1) | (76) |
active#(len(cons(X,Z))) | → | len#(Z) | (77) |
active#(add(X1,X2)) | → | active#(X1) | (78) |
active#(add(s(X),Y)) | → | add#(X,Y) | (79) |
active#(len(X)) | → | len#(active(X)) | (80) |
active#(len(cons(X,Z))) | → | s#(len(Z)) | (81) |
add#(ok(X1),ok(X2)) | → | add#(X1,X2) | (82) |
s#(ok(X)) | → | s#(X) | (83) |
active#(add(X1,X2)) | → | add#(active(X1),X2) | (84) |
proper#(len(X)) | → | len#(proper(X)) | (85) |
active#(fst(s(X),cons(Y,Z))) | → | cons#(Y,fst(X,Z)) | (86) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (87) |
active#(add(X1,X2)) | → | add#(X1,active(X2)) | (88) |
proper#(s(X)) | → | proper#(X) | (89) |
proper#(len(X)) | → | proper#(X) | (90) |
active#(from(X)) | → | from#(s(X)) | (91) |
cons#(ok(X1),ok(X2)) | → | cons#(X1,X2) | (92) |
The dependency pairs are split into 9 components.
top#(mark(X)) | → | top#(proper(X)) | (59) |
top#(ok(X)) | → | top#(active(X)) | (50) |
[len#(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 11650 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x1 + x2 + 43209 |
[top#(x1)] | = | x1 + 0 |
[fst#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | x1 + 0 |
[0] | = | 5876 |
[from(x1)] | = | x1 + 41055 |
[s#(x1)] | = | 0 |
[nil] | = | 32018 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | x1 + 41054 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x1 + x2 + 12280 |
[len(x1)] | = | x1 + 1 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
cons(mark(X1),X2) | → | mark(cons(X1,X2)) | (15) |
active(cons(X1,X2)) | → | cons(active(X1),X2) | (8) |
active(fst(0,Z)) | → | mark(nil) | (1) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (3) |
fst(mark(X1),X2) | → | mark(fst(X1,X2)) | (16) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(fst(X1,X2)) | → | fst(proper(X1),proper(X2)) | (26) |
add(mark(X1),X2) | → | mark(add(X1,X2)) | (19) |
fst(ok(X1),ok(X2)) | → | ok(fst(X1,X2)) | (32) |
fst(X1,mark(X2)) | → | mark(fst(X1,X2)) | (17) |
proper(from(X)) | → | from(proper(X)) | (27) |
add(ok(X1),ok(X2)) | → | ok(add(X1,X2)) | (34) |
proper(0) | → | ok(0) | (22) |
proper(add(X1,X2)) | → | add(proper(X1),proper(X2)) | (28) |
active(add(s(X),Y)) | → | mark(s(add(X,Y))) | (5) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(fst(X1,X2)) | → | fst(X1,active(X2)) | (10) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
add(X1,mark(X2)) | → | mark(add(X1,X2)) | (20) |
proper(cons(X1,X2)) | → | cons(proper(X1),proper(X2)) | (25) |
s(ok(X)) | → | ok(s(X)) | (30) |
active(len(X)) | → | len(active(X)) | (14) |
cons(ok(X1),ok(X2)) | → | ok(cons(X1,X2)) | (31) |
active(add(X1,X2)) | → | add(active(X1),X2) | (12) |
proper(s(X)) | → | s(proper(X)) | (23) |
proper(nil) | → | ok(nil) | (24) |
active(from(X)) | → | from(active(X)) | (11) |
active(fst(X1,X2)) | → | fst(active(X1),X2) | (9) |
active(add(X1,X2)) | → | add(X1,active(X2)) | (13) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
proper(len(X)) | → | len(proper(X)) | (29) |
active(fst(s(X),cons(Y,Z))) | → | mark(cons(Y,fst(X,Z))) | (2) |
top#(mark(X)) | → | top#(proper(X)) | (59) |
The dependency pairs are split into 1 component.
top#(ok(X)) | → | top#(active(X)) | (50) |
[len#(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x1 + 1 |
[top#(x1)] | = | x1 + 0 |
[fst#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 27377 |
[ok(x1)] | = | x1 + 27377 |
[0] | = | 1 |
[from(x1)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[nil] | = | 32018 |
[mark(x1)] | = | 1 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[cons(x1, x2)] | = | x1 + 1 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x1 + 1 |
[len(x1)] | = | x1 + 0 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
cons(mark(X1),X2) | → | mark(cons(X1,X2)) | (15) |
active(cons(X1,X2)) | → | cons(active(X1),X2) | (8) |
active(fst(0,Z)) | → | mark(nil) | (1) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (3) |
fst(mark(X1),X2) | → | mark(fst(X1,X2)) | (16) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(fst(X1,X2)) | → | fst(proper(X1),proper(X2)) | (26) |
add(mark(X1),X2) | → | mark(add(X1,X2)) | (19) |
fst(ok(X1),ok(X2)) | → | ok(fst(X1,X2)) | (32) |
fst(X1,mark(X2)) | → | mark(fst(X1,X2)) | (17) |
proper(from(X)) | → | from(proper(X)) | (27) |
add(ok(X1),ok(X2)) | → | ok(add(X1,X2)) | (34) |
proper(0) | → | ok(0) | (22) |
proper(add(X1,X2)) | → | add(proper(X1),proper(X2)) | (28) |
active(add(s(X),Y)) | → | mark(s(add(X,Y))) | (5) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(fst(X1,X2)) | → | fst(X1,active(X2)) | (10) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
add(X1,mark(X2)) | → | mark(add(X1,X2)) | (20) |
proper(cons(X1,X2)) | → | cons(proper(X1),proper(X2)) | (25) |
s(ok(X)) | → | ok(s(X)) | (30) |
active(len(X)) | → | len(active(X)) | (14) |
cons(ok(X1),ok(X2)) | → | ok(cons(X1,X2)) | (31) |
active(add(X1,X2)) | → | add(active(X1),X2) | (12) |
proper(s(X)) | → | s(proper(X)) | (23) |
proper(nil) | → | ok(nil) | (24) |
active(from(X)) | → | from(active(X)) | (11) |
active(fst(X1,X2)) | → | fst(active(X1),X2) | (9) |
active(add(X1,X2)) | → | add(X1,active(X2)) | (13) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
proper(len(X)) | → | len(proper(X)) | (29) |
active(fst(s(X),cons(Y,Z))) | → | mark(cons(Y,fst(X,Z))) | (2) |
top#(ok(X)) | → | top#(active(X)) | (50) |
The dependency pairs are split into 0 components.
proper#(len(X)) | → | proper#(X) | (90) |
proper#(s(X)) | → | proper#(X) | (89) |
proper#(cons(X1,X2)) | → | proper#(X1) | (58) |
proper#(cons(X1,X2)) | → | proper#(X2) | (57) |
proper#(from(X)) | → | proper#(X) | (49) |
proper#(add(X1,X2)) | → | proper#(X1) | (76) |
proper#(fst(X1,X2)) | → | proper#(X2) | (73) |
proper#(add(X1,X2)) | → | proper#(X2) | (41) |
proper#(fst(X1,X2)) | → | proper#(X1) | (39) |
[len#(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x1 + x2 + 1 |
[top#(x1)] | = | x1 + 0 |
[fst#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | 1 |
[0] | = | 1 |
[from(x1)] | = | x1 + 11575 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | 625 |
[proper#(x1)] | = | x1 + 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 21027 |
[cons(x1, x2)] | = | x1 + x2 + 1 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x1 + x2 + 1 |
[len(x1)] | = | x1 + 1 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
cons(mark(X1),X2) | → | mark(cons(X1,X2)) | (15) |
active(cons(X1,X2)) | → | cons(active(X1),X2) | (8) |
active(fst(0,Z)) | → | mark(nil) | (1) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (3) |
fst(mark(X1),X2) | → | mark(fst(X1,X2)) | (16) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(fst(X1,X2)) | → | fst(proper(X1),proper(X2)) | (26) |
add(mark(X1),X2) | → | mark(add(X1,X2)) | (19) |
fst(ok(X1),ok(X2)) | → | ok(fst(X1,X2)) | (32) |
fst(X1,mark(X2)) | → | mark(fst(X1,X2)) | (17) |
proper(from(X)) | → | from(proper(X)) | (27) |
add(ok(X1),ok(X2)) | → | ok(add(X1,X2)) | (34) |
proper(0) | → | ok(0) | (22) |
proper(add(X1,X2)) | → | add(proper(X1),proper(X2)) | (28) |
active(add(s(X),Y)) | → | mark(s(add(X,Y))) | (5) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(fst(X1,X2)) | → | fst(X1,active(X2)) | (10) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
add(X1,mark(X2)) | → | mark(add(X1,X2)) | (20) |
proper(cons(X1,X2)) | → | cons(proper(X1),proper(X2)) | (25) |
s(ok(X)) | → | ok(s(X)) | (30) |
active(len(X)) | → | len(active(X)) | (14) |
cons(ok(X1),ok(X2)) | → | ok(cons(X1,X2)) | (31) |
active(add(X1,X2)) | → | add(active(X1),X2) | (12) |
proper(s(X)) | → | s(proper(X)) | (23) |
proper(nil) | → | ok(nil) | (24) |
active(from(X)) | → | from(active(X)) | (11) |
active(fst(X1,X2)) | → | fst(active(X1),X2) | (9) |
active(add(X1,X2)) | → | add(X1,active(X2)) | (13) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
proper(len(X)) | → | len(proper(X)) | (29) |
active(fst(s(X),cons(Y,Z))) | → | mark(cons(Y,fst(X,Z))) | (2) |
proper#(len(X)) | → | proper#(X) | (90) |
proper#(s(X)) | → | proper#(X) | (89) |
proper#(cons(X1,X2)) | → | proper#(X1) | (58) |
proper#(cons(X1,X2)) | → | proper#(X2) | (57) |
proper#(from(X)) | → | proper#(X) | (49) |
proper#(add(X1,X2)) | → | proper#(X1) | (76) |
proper#(fst(X1,X2)) | → | proper#(X2) | (73) |
proper#(add(X1,X2)) | → | proper#(X2) | (41) |
proper#(fst(X1,X2)) | → | proper#(X1) | (39) |
The dependency pairs are split into 0 components.
active#(fst(X1,X2)) | → | active#(X1) | (56) |
active#(add(X1,X2)) | → | active#(X2) | (55) |
active#(from(X)) | → | active#(X) | (54) |
active#(add(X1,X2)) | → | active#(X1) | (78) |
active#(cons(X1,X2)) | → | active#(X1) | (47) |
active#(fst(X1,X2)) | → | active#(X2) | (40) |
active#(len(X)) | → | active#(X) | (67) |
[len#(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x1 + x2 + 1 |
[top#(x1)] | = | x1 + 0 |
[fst#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | 1 |
[0] | = | 1 |
[from(x1)] | = | x1 + 11575 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | 1 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[cons(x1, x2)] | = | x1 + x2 + 1 |
[active#(x1)] | = | x1 + 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x1 + x2 + 1 |
[len(x1)] | = | x1 + 12063 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
cons(mark(X1),X2) | → | mark(cons(X1,X2)) | (15) |
active(cons(X1,X2)) | → | cons(active(X1),X2) | (8) |
active(fst(0,Z)) | → | mark(nil) | (1) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (3) |
fst(mark(X1),X2) | → | mark(fst(X1,X2)) | (16) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(fst(X1,X2)) | → | fst(proper(X1),proper(X2)) | (26) |
add(mark(X1),X2) | → | mark(add(X1,X2)) | (19) |
fst(ok(X1),ok(X2)) | → | ok(fst(X1,X2)) | (32) |
fst(X1,mark(X2)) | → | mark(fst(X1,X2)) | (17) |
proper(from(X)) | → | from(proper(X)) | (27) |
add(ok(X1),ok(X2)) | → | ok(add(X1,X2)) | (34) |
proper(0) | → | ok(0) | (22) |
proper(add(X1,X2)) | → | add(proper(X1),proper(X2)) | (28) |
active(add(s(X),Y)) | → | mark(s(add(X,Y))) | (5) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(fst(X1,X2)) | → | fst(X1,active(X2)) | (10) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
add(X1,mark(X2)) | → | mark(add(X1,X2)) | (20) |
proper(cons(X1,X2)) | → | cons(proper(X1),proper(X2)) | (25) |
s(ok(X)) | → | ok(s(X)) | (30) |
active(len(X)) | → | len(active(X)) | (14) |
cons(ok(X1),ok(X2)) | → | ok(cons(X1,X2)) | (31) |
active(add(X1,X2)) | → | add(active(X1),X2) | (12) |
proper(s(X)) | → | s(proper(X)) | (23) |
proper(nil) | → | ok(nil) | (24) |
active(from(X)) | → | from(active(X)) | (11) |
active(fst(X1,X2)) | → | fst(active(X1),X2) | (9) |
active(add(X1,X2)) | → | add(X1,active(X2)) | (13) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
proper(len(X)) | → | len(proper(X)) | (29) |
active(fst(s(X),cons(Y,Z))) | → | mark(cons(Y,fst(X,Z))) | (2) |
active#(fst(X1,X2)) | → | active#(X1) | (56) |
active#(add(X1,X2)) | → | active#(X2) | (55) |
active#(from(X)) | → | active#(X) | (54) |
active#(add(X1,X2)) | → | active#(X1) | (78) |
active#(cons(X1,X2)) | → | active#(X1) | (47) |
active#(fst(X1,X2)) | → | active#(X2) | (40) |
active#(len(X)) | → | active#(X) | (67) |
The dependency pairs are split into 0 components.
len#(mark(X)) | → | len#(X) | (46) |
len#(ok(X)) | → | len#(X) | (72) |
[len#(x1)] | = | x1 + 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x1 + 1 |
[top#(x1)] | = | x1 + 0 |
[fst#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[from(x1)] | = | x1 + 32570 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 0 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | x2 + 1 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x2 + 44249 |
[len(x1)] | = | x1 + 0 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
cons(mark(X1),X2) | → | mark(cons(X1,X2)) | (15) |
active(cons(X1,X2)) | → | cons(active(X1),X2) | (8) |
active(fst(0,Z)) | → | mark(nil) | (1) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (3) |
fst(mark(X1),X2) | → | mark(fst(X1,X2)) | (16) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(fst(X1,X2)) | → | fst(proper(X1),proper(X2)) | (26) |
add(mark(X1),X2) | → | mark(add(X1,X2)) | (19) |
fst(ok(X1),ok(X2)) | → | ok(fst(X1,X2)) | (32) |
fst(X1,mark(X2)) | → | mark(fst(X1,X2)) | (17) |
proper(from(X)) | → | from(proper(X)) | (27) |
add(ok(X1),ok(X2)) | → | ok(add(X1,X2)) | (34) |
proper(0) | → | ok(0) | (22) |
proper(add(X1,X2)) | → | add(proper(X1),proper(X2)) | (28) |
active(add(s(X),Y)) | → | mark(s(add(X,Y))) | (5) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(fst(X1,X2)) | → | fst(X1,active(X2)) | (10) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
add(X1,mark(X2)) | → | mark(add(X1,X2)) | (20) |
proper(cons(X1,X2)) | → | cons(proper(X1),proper(X2)) | (25) |
s(ok(X)) | → | ok(s(X)) | (30) |
active(len(X)) | → | len(active(X)) | (14) |
cons(ok(X1),ok(X2)) | → | ok(cons(X1,X2)) | (31) |
active(add(X1,X2)) | → | add(active(X1),X2) | (12) |
proper(s(X)) | → | s(proper(X)) | (23) |
proper(nil) | → | ok(nil) | (24) |
active(from(X)) | → | from(active(X)) | (11) |
active(fst(X1,X2)) | → | fst(active(X1),X2) | (9) |
active(add(X1,X2)) | → | add(X1,active(X2)) | (13) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
proper(len(X)) | → | len(proper(X)) | (29) |
active(fst(s(X),cons(Y,Z))) | → | mark(cons(Y,fst(X,Z))) | (2) |
len#(ok(X)) | → | len#(X) | (72) |
The dependency pairs are split into 1 component.
len#(mark(X)) | → | len#(X) | (46) |
[len#(x1)] | = | x1 + 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x2 + 1 |
[top#(x1)] | = | 0 |
[fst#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[from(x1)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 3 |
[cons(x1, x2)] | = | x2 + 1 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x2 + 1 |
[len(x1)] | = | x1 + 0 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
active(fst(0,Z)) | → | mark(nil) | (1) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(0) | → | ok(0) | (22) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
s(ok(X)) | → | ok(s(X)) | (30) |
proper(nil) | → | ok(nil) | (24) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
len#(mark(X)) | → | len#(X) | (46) |
The dependency pairs are split into 0 components.
fst#(ok(X1),ok(X2)) | → | fst#(X1,X2) | (52) |
fst#(mark(X1),X2) | → | fst#(X1,X2) | (48) |
fst#(X1,mark(X2)) | → | fst#(X1,X2) | (69) |
[len#(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x2 + 1 |
[top#(x1)] | = | 0 |
[fst#(x1, x2)] | = | x1 + 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[from(x1)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[nil] | = | 3 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 3 |
[cons(x1, x2)] | = | x2 + 1 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x2 + 1 |
[len(x1)] | = | x1 + 0 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
active(fst(0,Z)) | → | mark(nil) | (1) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(0) | → | ok(0) | (22) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
s(ok(X)) | → | ok(s(X)) | (30) |
proper(nil) | → | ok(nil) | (24) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
fst#(ok(X1),ok(X2)) | → | fst#(X1,X2) | (52) |
fst#(mark(X1),X2) | → | fst#(X1,X2) | (48) |
The dependency pairs are split into 1 component.
fst#(X1,mark(X2)) | → | fst#(X1,X2) | (69) |
[len#(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x2 + 1 |
[top#(x1)] | = | 0 |
[fst#(x1, x2)] | = | x2 + 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[from(x1)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 14756 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 14758 |
[cons(x1, x2)] | = | x2 + 1 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x2 + 1 |
[len(x1)] | = | x1 + 0 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
active(fst(0,Z)) | → | mark(nil) | (1) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(0) | → | ok(0) | (22) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
s(ok(X)) | → | ok(s(X)) | (30) |
proper(nil) | → | ok(nil) | (24) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
fst#(X1,mark(X2)) | → | fst#(X1,X2) | (69) |
The dependency pairs are split into 0 components.
add#(X1,mark(X2)) | → | add#(X1,X2) | (66) |
add#(ok(X1),ok(X2)) | → | add#(X1,X2) | (82) |
add#(mark(X1),X2) | → | add#(X1,X2) | (44) |
[len#(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 31675 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x2 + 1 |
[top#(x1)] | = | 0 |
[fst#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[from(x1)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 63039 |
[cons(x1, x2)] | = | x2 + 31363 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | x1 + x2 + 0 |
[add(x1, x2)] | = | x2 + 1 |
[len(x1)] | = | x1 + 0 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
active(fst(0,Z)) | → | mark(nil) | (1) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(0) | → | ok(0) | (22) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
s(ok(X)) | → | ok(s(X)) | (30) |
proper(nil) | → | ok(nil) | (24) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
add#(X1,mark(X2)) | → | add#(X1,X2) | (66) |
add#(ok(X1),ok(X2)) | → | add#(X1,X2) | (82) |
add#(mark(X1),X2) | → | add#(X1,X2) | (44) |
The dependency pairs are split into 0 components.
from#(ok(X)) | → | from#(X) | (63) |
from#(mark(X)) | → | from#(X) | (51) |
[len#(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x2 + 1 |
[top#(x1)] | = | 0 |
[fst#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[from(x1)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | x1 + 0 |
[active(x1)] | = | x1 + 3 |
[cons(x1, x2)] | = | x2 + 1 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x2 + 1 |
[len(x1)] | = | x1 + 0 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
active(fst(0,Z)) | → | mark(nil) | (1) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(0) | → | ok(0) | (22) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
s(ok(X)) | → | ok(s(X)) | (30) |
proper(nil) | → | ok(nil) | (24) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
from#(ok(X)) | → | from#(X) | (63) |
from#(mark(X)) | → | from#(X) | (51) |
The dependency pairs are split into 0 components.
s#(ok(X)) | → | s#(X) | (83) |
[len#(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x2 + 1 |
[top#(x1)] | = | 0 |
[fst#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[from(x1)] | = | x1 + 16898 |
[s#(x1)] | = | x1 + 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 3 |
[cons(x1, x2)] | = | x2 + 1 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x2 + 1 |
[len(x1)] | = | x1 + 0 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
active(fst(0,Z)) | → | mark(nil) | (1) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(0) | → | ok(0) | (22) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
s(ok(X)) | → | ok(s(X)) | (30) |
proper(nil) | → | ok(nil) | (24) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
s#(ok(X)) | → | s#(X) | (83) |
The dependency pairs are split into 0 components.
cons#(ok(X1),ok(X2)) | → | cons#(X1,X2) | (92) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (87) |
[len#(x1)] | = | 0 |
[cons#(x1, x2)] | = | x1 + 0 |
[s(x1)] | = | x1 + 1 |
[top(x1)] | = | 0 |
[fst(x1, x2)] | = | x2 + 1 |
[top#(x1)] | = | 0 |
[fst#(x1, x2)] | = | 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[0] | = | 1 |
[from(x1)] | = | x1 + 1 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[from#(x1)] | = | 0 |
[active(x1)] | = | x1 + 3 |
[cons(x1, x2)] | = | x2 + 1 |
[active#(x1)] | = | 0 |
[add#(x1, x2)] | = | 0 |
[add(x1, x2)] | = | x2 + 1 |
[len(x1)] | = | x1 + 0 |
from(mark(X)) | → | mark(from(X)) | (18) |
active(add(0,X)) | → | mark(X) | (4) |
active(fst(0,Z)) | → | mark(nil) | (1) |
len(mark(X)) | → | mark(len(X)) | (21) |
proper(0) | → | ok(0) | (22) |
from(ok(X)) | → | ok(from(X)) | (33) |
active(len(cons(X,Z))) | → | mark(s(len(Z))) | (7) |
s(ok(X)) | → | ok(s(X)) | (30) |
proper(nil) | → | ok(nil) | (24) |
active(len(nil)) | → | mark(0) | (6) |
len(ok(X)) | → | ok(len(X)) | (35) |
cons#(ok(X1),ok(X2)) | → | cons#(X1,X2) | (92) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (87) |
The dependency pairs are split into 0 components.