The rewrite relation of the following TRS is considered.
a__fib(N) | → | a__sel(mark(N),a__fib1(s(0),s(0))) | (1) |
a__fib1(X,Y) | → | cons(mark(X),fib1(Y,add(X,Y))) | (2) |
a__add(0,X) | → | mark(X) | (3) |
a__add(s(X),Y) | → | s(a__add(mark(X),mark(Y))) | (4) |
a__sel(0,cons(X,XS)) | → | mark(X) | (5) |
a__sel(s(N),cons(X,XS)) | → | a__sel(mark(N),mark(XS)) | (6) |
mark(fib(X)) | → | a__fib(mark(X)) | (7) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (8) |
mark(fib1(X1,X2)) | → | a__fib1(mark(X1),mark(X2)) | (9) |
mark(add(X1,X2)) | → | a__add(mark(X1),mark(X2)) | (10) |
mark(s(X)) | → | s(mark(X)) | (11) |
mark(0) | → | 0 | (12) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (13) |
a__fib(X) | → | fib(X) | (14) |
a__sel(X1,X2) | → | sel(X1,X2) | (15) |
a__fib1(X1,X2) | → | fib1(X1,X2) | (16) |
a__add(X1,X2) | → | add(X1,X2) | (17) |
a__sel#(s(N),cons(X,XS)) | → | a__sel#(mark(N),mark(XS)) | (18) |
mark#(fib1(X1,X2)) | → | a__fib1#(mark(X1),mark(X2)) | (19) |
mark#(add(X1,X2)) | → | mark#(X1) | (20) |
mark#(s(X)) | → | mark#(X) | (21) |
mark#(fib(X)) | → | mark#(X) | (22) |
a__add#(s(X),Y) | → | mark#(X) | (23) |
a__add#(s(X),Y) | → | a__add#(mark(X),mark(Y)) | (24) |
mark#(add(X1,X2)) | → | a__add#(mark(X1),mark(X2)) | (25) |
mark#(add(X1,X2)) | → | mark#(X2) | (26) |
a__add#(s(X),Y) | → | mark#(Y) | (27) |
mark#(sel(X1,X2)) | → | a__sel#(mark(X1),mark(X2)) | (28) |
mark#(fib1(X1,X2)) | → | mark#(X1) | (29) |
mark#(fib(X)) | → | a__fib#(mark(X)) | (30) |
mark#(cons(X1,X2)) | → | mark#(X1) | (31) |
mark#(sel(X1,X2)) | → | mark#(X2) | (32) |
a__fib#(N) | → | a__sel#(mark(N),a__fib1(s(0),s(0))) | (33) |
a__fib#(N) | → | a__fib1#(s(0),s(0)) | (34) |
mark#(sel(X1,X2)) | → | mark#(X1) | (35) |
a__add#(0,X) | → | mark#(X) | (36) |
a__sel#(s(N),cons(X,XS)) | → | mark#(N) | (37) |
a__fib1#(X,Y) | → | mark#(X) | (38) |
mark#(fib1(X1,X2)) | → | mark#(X2) | (39) |
a__sel#(0,cons(X,XS)) | → | mark#(X) | (40) |
a__sel#(s(N),cons(X,XS)) | → | mark#(XS) | (41) |
a__fib#(N) | → | mark#(N) | (42) |
The dependency pairs are split into 1 component.
a__fib#(N) | → | mark#(N) | (42) |
a__add#(s(X),Y) | → | mark#(Y) | (27) |
a__sel#(s(N),cons(X,XS)) | → | mark#(XS) | (41) |
mark#(add(X1,X2)) | → | mark#(X2) | (26) |
a__sel#(0,cons(X,XS)) | → | mark#(X) | (40) |
mark#(add(X1,X2)) | → | a__add#(mark(X1),mark(X2)) | (25) |
mark#(fib1(X1,X2)) | → | mark#(X2) | (39) |
a__fib1#(X,Y) | → | mark#(X) | (38) |
a__add#(s(X),Y) | → | a__add#(mark(X),mark(Y)) | (24) |
a__sel#(s(N),cons(X,XS)) | → | mark#(N) | (37) |
a__add#(s(X),Y) | → | mark#(X) | (23) |
a__add#(0,X) | → | mark#(X) | (36) |
mark#(sel(X1,X2)) | → | mark#(X1) | (35) |
mark#(fib(X)) | → | mark#(X) | (22) |
mark#(s(X)) | → | mark#(X) | (21) |
mark#(add(X1,X2)) | → | mark#(X1) | (20) |
a__fib#(N) | → | a__fib1#(s(0),s(0)) | (34) |
a__fib#(N) | → | a__sel#(mark(N),a__fib1(s(0),s(0))) | (33) |
mark#(fib1(X1,X2)) | → | a__fib1#(mark(X1),mark(X2)) | (19) |
mark#(sel(X1,X2)) | → | mark#(X2) | (32) |
mark#(cons(X1,X2)) | → | mark#(X1) | (31) |
mark#(fib(X)) | → | a__fib#(mark(X)) | (30) |
mark#(fib1(X1,X2)) | → | mark#(X1) | (29) |
a__sel#(s(N),cons(X,XS)) | → | a__sel#(mark(N),mark(XS)) | (18) |
mark#(sel(X1,X2)) | → | a__sel#(mark(X1),mark(X2)) | (28) |
[s(x1)] | = | x1 + 0 |
[a__add#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib1#(x1, x2)] | = | max(x1 + 0, 0) |
[fib1(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[fib(x1)] | = | x1 + 2 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 1 |
[sel(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[a__sel#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[mark(x1)] | = | x1 + 0 |
[a__sel(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[a__fib#(x1)] | = | x1 + 1 |
[cons(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib(x1)] | = | x1 + 2 |
[add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib1(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
a__add(s(X),Y) | → | s(a__add(mark(X),mark(Y))) | (4) |
a__sel(X1,X2) | → | sel(X1,X2) | (15) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (8) |
a__fib(N) | → | a__sel(mark(N),a__fib1(s(0),s(0))) | (1) |
a__add(0,X) | → | mark(X) | (3) |
a__fib1(X1,X2) | → | fib1(X1,X2) | (16) |
a__add(X1,X2) | → | add(X1,X2) | (17) |
a__sel(0,cons(X,XS)) | → | mark(X) | (5) |
mark(add(X1,X2)) | → | a__add(mark(X1),mark(X2)) | (10) |
mark(fib(X)) | → | a__fib(mark(X)) | (7) |
a__fib(X) | → | fib(X) | (14) |
mark(0) | → | 0 | (12) |
mark(s(X)) | → | s(mark(X)) | (11) |
mark(fib1(X1,X2)) | → | a__fib1(mark(X1),mark(X2)) | (9) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (13) |
a__sel(s(N),cons(X,XS)) | → | a__sel(mark(N),mark(XS)) | (6) |
a__fib1(X,Y) | → | cons(mark(X),fib1(Y,add(X,Y))) | (2) |
a__fib#(N) | → | mark#(N) | (42) |
mark#(sel(X1,X2)) | → | mark#(X1) | (35) |
mark#(fib(X)) | → | mark#(X) | (22) |
mark#(fib(X)) | → | a__fib#(mark(X)) | (30) |
The dependency pairs are split into 1 component.
a__add#(s(X),Y) | → | mark#(Y) | (27) |
a__add#(s(X),Y) | → | mark#(X) | (23) |
a__add#(s(X),Y) | → | a__add#(mark(X),mark(Y)) | (24) |
mark#(sel(X1,X2)) | → | mark#(X2) | (32) |
mark#(sel(X1,X2)) | → | a__sel#(mark(X1),mark(X2)) | (28) |
a__add#(0,X) | → | mark#(X) | (36) |
a__sel#(0,cons(X,XS)) | → | mark#(X) | (40) |
mark#(add(X1,X2)) | → | mark#(X2) | (26) |
mark#(add(X1,X2)) | → | mark#(X1) | (20) |
mark#(add(X1,X2)) | → | a__add#(mark(X1),mark(X2)) | (25) |
mark#(s(X)) | → | mark#(X) | (21) |
mark#(fib1(X1,X2)) | → | mark#(X2) | (39) |
mark#(fib1(X1,X2)) | → | mark#(X1) | (29) |
mark#(fib1(X1,X2)) | → | a__fib1#(mark(X1),mark(X2)) | (19) |
mark#(cons(X1,X2)) | → | mark#(X1) | (31) |
a__sel#(s(N),cons(X,XS)) | → | mark#(XS) | (41) |
a__sel#(s(N),cons(X,XS)) | → | mark#(N) | (37) |
a__sel#(s(N),cons(X,XS)) | → | a__sel#(mark(N),mark(XS)) | (18) |
a__fib1#(X,Y) | → | mark#(X) | (38) |
[s(x1)] | = | x1 + 0 |
[a__add#(x1, x2)] | = | max(x1 + 18458, x2 + 18458, 0) |
[a__add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib1#(x1, x2)] | = | max(x1 + 18458, 0) |
[fib1(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[fib(x1)] | = | x1 + 1325 |
[mark#(x1)] | = | x1 + 18458 |
[0] | = | 1 |
[sel(x1, x2)] | = | max(x1 + 1325, x2 + 0, 0) |
[a__sel#(x1, x2)] | = | max(x1 + 18459, x2 + 18458, 0) |
[mark(x1)] | = | x1 + 0 |
[a__sel(x1, x2)] | = | max(x1 + 1325, x2 + 0, 0) |
[a__fib#(x1)] | = | x1 + 1 |
[cons(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib(x1)] | = | x1 + 1325 |
[add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib1(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
a__add(s(X),Y) | → | s(a__add(mark(X),mark(Y))) | (4) |
a__sel(X1,X2) | → | sel(X1,X2) | (15) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (8) |
a__fib(N) | → | a__sel(mark(N),a__fib1(s(0),s(0))) | (1) |
a__add(0,X) | → | mark(X) | (3) |
a__fib1(X1,X2) | → | fib1(X1,X2) | (16) |
a__add(X1,X2) | → | add(X1,X2) | (17) |
a__sel(0,cons(X,XS)) | → | mark(X) | (5) |
mark(add(X1,X2)) | → | a__add(mark(X1),mark(X2)) | (10) |
mark(fib(X)) | → | a__fib(mark(X)) | (7) |
a__fib(X) | → | fib(X) | (14) |
mark(0) | → | 0 | (12) |
mark(s(X)) | → | s(mark(X)) | (11) |
mark(fib1(X1,X2)) | → | a__fib1(mark(X1),mark(X2)) | (9) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (13) |
a__sel(s(N),cons(X,XS)) | → | a__sel(mark(N),mark(XS)) | (6) |
a__fib1(X,Y) | → | cons(mark(X),fib1(Y,add(X,Y))) | (2) |
a__sel#(s(N),cons(X,XS)) | → | mark#(N) | (37) |
The dependency pairs are split into 1 component.
a__add#(s(X),Y) | → | mark#(Y) | (27) |
a__add#(s(X),Y) | → | mark#(X) | (23) |
a__add#(s(X),Y) | → | a__add#(mark(X),mark(Y)) | (24) |
mark#(sel(X1,X2)) | → | mark#(X2) | (32) |
mark#(sel(X1,X2)) | → | a__sel#(mark(X1),mark(X2)) | (28) |
a__add#(0,X) | → | mark#(X) | (36) |
a__sel#(0,cons(X,XS)) | → | mark#(X) | (40) |
mark#(add(X1,X2)) | → | mark#(X2) | (26) |
mark#(add(X1,X2)) | → | mark#(X1) | (20) |
mark#(add(X1,X2)) | → | a__add#(mark(X1),mark(X2)) | (25) |
mark#(s(X)) | → | mark#(X) | (21) |
mark#(fib1(X1,X2)) | → | mark#(X2) | (39) |
mark#(fib1(X1,X2)) | → | mark#(X1) | (29) |
mark#(fib1(X1,X2)) | → | a__fib1#(mark(X1),mark(X2)) | (19) |
mark#(cons(X1,X2)) | → | mark#(X1) | (31) |
a__sel#(s(N),cons(X,XS)) | → | mark#(XS) | (41) |
a__sel#(s(N),cons(X,XS)) | → | a__sel#(mark(N),mark(XS)) | (18) |
a__fib1#(X,Y) | → | mark#(X) | (38) |
[s(x1)] | = | x1 + 0 |
[a__add#(x1, x2)] | = | max(x1 + 18588, x2 + 18588, 0) |
[a__add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib1#(x1, x2)] | = | max(x1 + 18588, 0) |
[fib1(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[fib(x1)] | = | x1 + 39474 |
[mark#(x1)] | = | x1 + 18588 |
[0] | = | 16908 |
[sel(x1, x2)] | = | max(x1 + 21241, x2 + 21240, 0) |
[a__sel#(x1, x2)] | = | max(x1 + 39826, x2 + 39827, 0) |
[mark(x1)] | = | x1 + 0 |
[a__sel(x1, x2)] | = | max(x1 + 21241, x2 + 21240, 0) |
[a__fib#(x1)] | = | x1 + 1 |
[cons(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib(x1)] | = | x1 + 39474 |
[add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib1(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
a__add(s(X),Y) | → | s(a__add(mark(X),mark(Y))) | (4) |
a__sel(X1,X2) | → | sel(X1,X2) | (15) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (8) |
a__fib(N) | → | a__sel(mark(N),a__fib1(s(0),s(0))) | (1) |
a__add(0,X) | → | mark(X) | (3) |
a__fib1(X1,X2) | → | fib1(X1,X2) | (16) |
a__add(X1,X2) | → | add(X1,X2) | (17) |
a__sel(0,cons(X,XS)) | → | mark(X) | (5) |
mark(add(X1,X2)) | → | a__add(mark(X1),mark(X2)) | (10) |
mark(fib(X)) | → | a__fib(mark(X)) | (7) |
a__fib(X) | → | fib(X) | (14) |
mark(0) | → | 0 | (12) |
mark(s(X)) | → | s(mark(X)) | (11) |
mark(fib1(X1,X2)) | → | a__fib1(mark(X1),mark(X2)) | (9) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (13) |
a__sel(s(N),cons(X,XS)) | → | a__sel(mark(N),mark(XS)) | (6) |
a__fib1(X,Y) | → | cons(mark(X),fib1(Y,add(X,Y))) | (2) |
mark#(sel(X1,X2)) | → | mark#(X2) | (32) |
mark#(sel(X1,X2)) | → | a__sel#(mark(X1),mark(X2)) | (28) |
a__sel#(0,cons(X,XS)) | → | mark#(X) | (40) |
a__sel#(s(N),cons(X,XS)) | → | mark#(XS) | (41) |
The dependency pairs are split into 2 components.
a__sel#(s(N),cons(X,XS)) | → | a__sel#(mark(N),mark(XS)) | (18) |
π(a__fib1#) | = | 2 |
π(a__sel#) | = | 1 |
π(mark) | = | 1 |
prec(s) | = | 4 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(a__add#) | = | 0 | status(a__add#) | = | [2] | list-extension(a__add#) | = | Lex | ||
prec(a__add) | = | 5 | status(a__add) | = | [2, 1] | list-extension(a__add) | = | Lex | ||
prec(fib1) | = | 3 | status(fib1) | = | [] | list-extension(fib1) | = | Lex | ||
prec(fib) | = | 1 | status(fib) | = | [] | list-extension(fib) | = | Lex | ||
prec(mark#) | = | 0 | status(mark#) | = | [] | list-extension(mark#) | = | Lex | ||
prec(0) | = | 0 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(sel) | = | 2 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(a__sel) | = | 2 | status(a__sel) | = | [] | list-extension(a__sel) | = | Lex | ||
prec(a__fib#) | = | 0 | status(a__fib#) | = | [] | list-extension(a__fib#) | = | Lex | ||
prec(cons) | = | 1 | status(cons) | = | [1] | list-extension(cons) | = | Lex | ||
prec(a__fib) | = | 1 | status(a__fib) | = | [] | list-extension(a__fib) | = | Lex | ||
prec(add) | = | 5 | status(add) | = | [2, 1] | list-extension(add) | = | Lex | ||
prec(a__fib1) | = | 3 | status(a__fib1) | = | [] | list-extension(a__fib1) | = | Lex |
[s(x1)] | = | x1 + 0 |
[a__add#(x1, x2)] | = | max(x2 + 1, 0) |
[a__add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[fib1(x1, x2)] | = | max(x1 + 8947, x2 + 8947, 0) |
[fib(x1)] | = | 17895 |
[mark#(x1)] | = | 1 |
[0] | = | 1 |
[sel(x1, x2)] | = | x2 + 8946 |
[a__sel(x1, x2)] | = | x2 + 8946 |
[a__fib#(x1)] | = | 1 |
[cons(x1, x2)] | = | max(x1 + 8947, x2 + 0, 0) |
[a__fib(x1)] | = | 17895 |
[add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib1(x1, x2)] | = | max(x1 + 8947, x2 + 8947, 0) |
a__add(s(X),Y) | → | s(a__add(mark(X),mark(Y))) | (4) |
a__sel(X1,X2) | → | sel(X1,X2) | (15) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (8) |
a__fib(N) | → | a__sel(mark(N),a__fib1(s(0),s(0))) | (1) |
a__add(0,X) | → | mark(X) | (3) |
a__fib1(X1,X2) | → | fib1(X1,X2) | (16) |
a__add(X1,X2) | → | add(X1,X2) | (17) |
a__sel(0,cons(X,XS)) | → | mark(X) | (5) |
mark(add(X1,X2)) | → | a__add(mark(X1),mark(X2)) | (10) |
mark(fib(X)) | → | a__fib(mark(X)) | (7) |
a__fib(X) | → | fib(X) | (14) |
mark(0) | → | 0 | (12) |
mark(s(X)) | → | s(mark(X)) | (11) |
mark(fib1(X1,X2)) | → | a__fib1(mark(X1),mark(X2)) | (9) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (13) |
a__sel(s(N),cons(X,XS)) | → | a__sel(mark(N),mark(XS)) | (6) |
a__fib1(X,Y) | → | cons(mark(X),fib1(Y,add(X,Y))) | (2) |
a__sel#(s(N),cons(X,XS)) | → | a__sel#(mark(N),mark(XS)) | (18) |
The dependency pairs are split into 0 components.
a__add#(s(X),Y) | → | mark#(Y) | (27) |
a__add#(s(X),Y) | → | mark#(X) | (23) |
a__add#(s(X),Y) | → | a__add#(mark(X),mark(Y)) | (24) |
a__add#(0,X) | → | mark#(X) | (36) |
mark#(add(X1,X2)) | → | mark#(X2) | (26) |
mark#(add(X1,X2)) | → | mark#(X1) | (20) |
mark#(add(X1,X2)) | → | a__add#(mark(X1),mark(X2)) | (25) |
mark#(s(X)) | → | mark#(X) | (21) |
mark#(fib1(X1,X2)) | → | mark#(X2) | (39) |
mark#(fib1(X1,X2)) | → | mark#(X1) | (29) |
mark#(fib1(X1,X2)) | → | a__fib1#(mark(X1),mark(X2)) | (19) |
mark#(cons(X1,X2)) | → | mark#(X1) | (31) |
a__fib1#(X,Y) | → | mark#(X) | (38) |
[s(x1)] | = | x1 + 0 |
[a__add#(x1, x2)] | = | max(x1 + 13359, x2 + 13359, 0) |
[a__add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib1#(x1, x2)] | = | max(x1 + 13360, 0) |
[fib1(x1, x2)] | = | max(x1 + 4188, x2 + 4188, 0) |
[fib(x1)] | = | x1 + 35931 |
[mark#(x1)] | = | x1 + 13359 |
[0] | = | 1 |
[sel(x1, x2)] | = | max(x1 + 31742, x2 + 31742, 0) |
[a__sel#(x1, x2)] | = | max(0) |
[mark(x1)] | = | x1 + 0 |
[a__sel(x1, x2)] | = | max(x1 + 31742, x2 + 31742, 0) |
[a__fib#(x1)] | = | 1 |
[cons(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[a__fib(x1)] | = | x1 + 35931 |
[add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib1(x1, x2)] | = | max(x1 + 4188, x2 + 4188, 0) |
a__add(s(X),Y) | → | s(a__add(mark(X),mark(Y))) | (4) |
a__sel(X1,X2) | → | sel(X1,X2) | (15) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (8) |
a__fib(N) | → | a__sel(mark(N),a__fib1(s(0),s(0))) | (1) |
a__add(0,X) | → | mark(X) | (3) |
a__fib1(X1,X2) | → | fib1(X1,X2) | (16) |
a__add(X1,X2) | → | add(X1,X2) | (17) |
a__sel(0,cons(X,XS)) | → | mark(X) | (5) |
mark(add(X1,X2)) | → | a__add(mark(X1),mark(X2)) | (10) |
mark(fib(X)) | → | a__fib(mark(X)) | (7) |
a__fib(X) | → | fib(X) | (14) |
mark(0) | → | 0 | (12) |
mark(s(X)) | → | s(mark(X)) | (11) |
mark(fib1(X1,X2)) | → | a__fib1(mark(X1),mark(X2)) | (9) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (13) |
a__sel(s(N),cons(X,XS)) | → | a__sel(mark(N),mark(XS)) | (6) |
a__fib1(X,Y) | → | cons(mark(X),fib1(Y,add(X,Y))) | (2) |
mark#(fib1(X1,X2)) | → | mark#(X2) | (39) |
mark#(fib1(X1,X2)) | → | mark#(X1) | (29) |
mark#(fib1(X1,X2)) | → | a__fib1#(mark(X1),mark(X2)) | (19) |
mark#(cons(X1,X2)) | → | mark#(X1) | (31) |
a__fib1#(X,Y) | → | mark#(X) | (38) |
The dependency pairs are split into 1 component.
a__add#(s(X),Y) | → | mark#(Y) | (27) |
a__add#(s(X),Y) | → | mark#(X) | (23) |
a__add#(s(X),Y) | → | a__add#(mark(X),mark(Y)) | (24) |
a__add#(0,X) | → | mark#(X) | (36) |
mark#(add(X1,X2)) | → | mark#(X2) | (26) |
mark#(add(X1,X2)) | → | mark#(X1) | (20) |
mark#(add(X1,X2)) | → | a__add#(mark(X1),mark(X2)) | (25) |
mark#(s(X)) | → | mark#(X) | (21) |
π(a__fib1#) | = | 2 |
π(a__sel#) | = | 1 |
π(mark) | = | 1 |
prec(s) | = | 4 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(a__add#) | = | 6 | status(a__add#) | = | [1, 2] | list-extension(a__add#) | = | Lex | ||
prec(a__add) | = | 7 | status(a__add) | = | [2, 1] | list-extension(a__add) | = | Lex | ||
prec(fib1) | = | 3 | status(fib1) | = | [] | list-extension(fib1) | = | Lex | ||
prec(fib) | = | 1 | status(fib) | = | [] | list-extension(fib) | = | Lex | ||
prec(mark#) | = | 5 | status(mark#) | = | [1] | list-extension(mark#) | = | Lex | ||
prec(0) | = | 0 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(sel) | = | 2 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(a__sel) | = | 2 | status(a__sel) | = | [] | list-extension(a__sel) | = | Lex | ||
prec(a__fib#) | = | 0 | status(a__fib#) | = | [] | list-extension(a__fib#) | = | Lex | ||
prec(cons) | = | 1 | status(cons) | = | [1] | list-extension(cons) | = | Lex | ||
prec(a__fib) | = | 1 | status(a__fib) | = | [] | list-extension(a__fib) | = | Lex | ||
prec(add) | = | 7 | status(add) | = | [2, 1] | list-extension(add) | = | Lex | ||
prec(a__fib1) | = | 3 | status(a__fib1) | = | [] | list-extension(a__fib1) | = | Lex |
[s(x1)] | = | x1 + 0 |
[a__add#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[fib1(x1, x2)] | = | max(x1 + 2, x2 + 2, 0) |
[fib(x1)] | = | 5 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 1 |
[sel(x1, x2)] | = | x2 + 1 |
[a__sel(x1, x2)] | = | x2 + 1 |
[a__fib#(x1)] | = | 1 |
[cons(x1, x2)] | = | max(x1 + 2, x2 + 0, 0) |
[a__fib(x1)] | = | 5 |
[add(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__fib1(x1, x2)] | = | max(x1 + 2, x2 + 2, 0) |
a__add(s(X),Y) | → | s(a__add(mark(X),mark(Y))) | (4) |
a__sel(X1,X2) | → | sel(X1,X2) | (15) |
mark(sel(X1,X2)) | → | a__sel(mark(X1),mark(X2)) | (8) |
a__fib(N) | → | a__sel(mark(N),a__fib1(s(0),s(0))) | (1) |
a__add(0,X) | → | mark(X) | (3) |
a__fib1(X1,X2) | → | fib1(X1,X2) | (16) |
a__add(X1,X2) | → | add(X1,X2) | (17) |
a__sel(0,cons(X,XS)) | → | mark(X) | (5) |
mark(add(X1,X2)) | → | a__add(mark(X1),mark(X2)) | (10) |
mark(fib(X)) | → | a__fib(mark(X)) | (7) |
a__fib(X) | → | fib(X) | (14) |
mark(0) | → | 0 | (12) |
mark(s(X)) | → | s(mark(X)) | (11) |
mark(fib1(X1,X2)) | → | a__fib1(mark(X1),mark(X2)) | (9) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (13) |
a__sel(s(N),cons(X,XS)) | → | a__sel(mark(N),mark(XS)) | (6) |
a__fib1(X,Y) | → | cons(mark(X),fib1(Y,add(X,Y))) | (2) |
a__add#(s(X),Y) | → | mark#(Y) | (27) |
a__add#(s(X),Y) | → | mark#(X) | (23) |
a__add#(s(X),Y) | → | a__add#(mark(X),mark(Y)) | (24) |
a__add#(0,X) | → | mark#(X) | (36) |
mark#(add(X1,X2)) | → | mark#(X2) | (26) |
mark#(add(X1,X2)) | → | mark#(X1) | (20) |
mark#(add(X1,X2)) | → | a__add#(mark(X1),mark(X2)) | (25) |
mark#(s(X)) | → | mark#(X) | (21) |
The dependency pairs are split into 0 components.