The rewrite relation of the following TRS is considered.
| a__nats | → | cons(0,incr(nats)) | (1) |
| a__pairs | → | cons(0,incr(odds)) | (2) |
| a__odds | → | a__incr(a__pairs) | (3) |
| a__incr(cons(X,XS)) | → | cons(s(mark(X)),incr(XS)) | (4) |
| a__head(cons(X,XS)) | → | mark(X) | (5) |
| a__tail(cons(X,XS)) | → | mark(XS) | (6) |
| mark(nats) | → | a__nats | (7) |
| mark(incr(X)) | → | a__incr(mark(X)) | (8) |
| mark(pairs) | → | a__pairs | (9) |
| mark(odds) | → | a__odds | (10) |
| mark(head(X)) | → | a__head(mark(X)) | (11) |
| mark(tail(X)) | → | a__tail(mark(X)) | (12) |
| mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (13) |
| mark(0) | → | 0 | (14) |
| mark(s(X)) | → | s(mark(X)) | (15) |
| a__nats | → | nats | (16) |
| a__incr(X) | → | incr(X) | (17) |
| a__pairs | → | pairs | (18) |
| a__odds | → | odds | (19) |
| a__head(X) | → | head(X) | (20) |
| a__tail(X) | → | tail(X) | (21) |
| mark#(cons(X1,X2)) | → | mark#(X1) | (22) |
| mark#(tail(X)) | → | a__tail#(mark(X)) | (23) |
| mark#(incr(X)) | → | a__incr#(mark(X)) | (24) |
| mark#(odds) | → | a__odds# | (25) |
| a__odds# | → | a__incr#(a__pairs) | (26) |
| a__odds# | → | a__pairs# | (27) |
| mark#(incr(X)) | → | mark#(X) | (28) |
| mark#(tail(X)) | → | mark#(X) | (29) |
| a__head#(cons(X,XS)) | → | mark#(X) | (30) |
| mark#(head(X)) | → | mark#(X) | (31) |
| a__incr#(cons(X,XS)) | → | mark#(X) | (32) |
| mark#(pairs) | → | a__pairs# | (33) |
| a__tail#(cons(X,XS)) | → | mark#(XS) | (34) |
| mark#(nats) | → | a__nats# | (35) |
| mark#(s(X)) | → | mark#(X) | (36) |
| mark#(head(X)) | → | a__head#(mark(X)) | (37) |
The dependency pairs are split into 1 component.
| mark#(head(X)) | → | a__head#(mark(X)) | (37) |
| mark#(incr(X)) | → | mark#(X) | (28) |
| mark#(s(X)) | → | mark#(X) | (36) |
| a__tail#(cons(X,XS)) | → | mark#(XS) | (34) |
| a__incr#(cons(X,XS)) | → | mark#(X) | (32) |
| a__odds# | → | a__incr#(a__pairs) | (26) |
| mark#(odds) | → | a__odds# | (25) |
| mark#(incr(X)) | → | a__incr#(mark(X)) | (24) |
| mark#(tail(X)) | → | a__tail#(mark(X)) | (23) |
| mark#(head(X)) | → | mark#(X) | (31) |
| a__head#(cons(X,XS)) | → | mark#(X) | (30) |
| mark#(tail(X)) | → | mark#(X) | (29) |
| mark#(cons(X1,X2)) | → | mark#(X1) | (22) |
| [incr(x1)] | = | x1 + 0 |
| [s(x1)] | = | x1 + 0 |
| [a__head#(x1)] | = | x1 + 1 |
| [a__incr(x1)] | = | x1 + 0 |
| [pairs] | = | 19496 |
| [a__nats] | = | 41990 |
| [a__pairs#] | = | 0 |
| [a__odds] | = | 19496 |
| [tail(x1)] | = | x1 + 2 |
| [mark#(x1)] | = | x1 + 0 |
| [0] | = | 0 |
| [odds] | = | 19496 |
| [a__nats#] | = | 0 |
| [mark(x1)] | = | x1 + 0 |
| [nats] | = | 41990 |
| [a__incr#(x1)] | = | x1 + 0 |
| [head(x1)] | = | x1 + 869 |
| [cons(x1, x2)] | = | x1 + x2 + 0 |
| [a__odds#] | = | 19496 |
| [a__pairs] | = | 19496 |
| [a__tail(x1)] | = | x1 + 2 |
| [a__tail#(x1)] | = | x1 + 1 |
| [a__head(x1)] | = | x1 + 869 |
| a__pairs | → | pairs | (18) |
| a__incr(cons(X,XS)) | → | cons(s(mark(X)),incr(XS)) | (4) |
| mark(s(X)) | → | s(mark(X)) | (15) |
| mark(incr(X)) | → | a__incr(mark(X)) | (8) |
| a__nats | → | cons(0,incr(nats)) | (1) |
| a__odds | → | a__incr(a__pairs) | (3) |
| a__nats | → | nats | (16) |
| a__tail(X) | → | tail(X) | (21) |
| a__odds | → | odds | (19) |
| a__incr(X) | → | incr(X) | (17) |
| a__head(cons(X,XS)) | → | mark(X) | (5) |
| mark(odds) | → | a__odds | (10) |
| mark(nats) | → | a__nats | (7) |
| a__head(X) | → | head(X) | (20) |
| mark(0) | → | 0 | (14) |
| mark(tail(X)) | → | a__tail(mark(X)) | (12) |
| mark(head(X)) | → | a__head(mark(X)) | (11) |
| mark(pairs) | → | a__pairs | (9) |
| mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (13) |
| a__tail(cons(X,XS)) | → | mark(XS) | (6) |
| a__pairs | → | cons(0,incr(odds)) | (2) |
| mark#(head(X)) | → | a__head#(mark(X)) | (37) |
| a__tail#(cons(X,XS)) | → | mark#(XS) | (34) |
| mark#(tail(X)) | → | a__tail#(mark(X)) | (23) |
| mark#(head(X)) | → | mark#(X) | (31) |
| a__head#(cons(X,XS)) | → | mark#(X) | (30) |
| mark#(tail(X)) | → | mark#(X) | (29) |
The dependency pairs are split into 1 component.
| a__incr#(cons(X,XS)) | → | mark#(X) | (32) |
| mark#(s(X)) | → | mark#(X) | (36) |
| mark#(incr(X)) | → | mark#(X) | (28) |
| mark#(incr(X)) | → | a__incr#(mark(X)) | (24) |
| a__odds# | → | a__incr#(a__pairs) | (26) |
| mark#(odds) | → | a__odds# | (25) |
| mark#(cons(X1,X2)) | → | mark#(X1) | (22) |
| [incr(x1)] | = | x1 + 0 |
| [s(x1)] | = | x1 + 0 |
| [a__head#(x1)] | = | 0 |
| [a__incr(x1)] | = | x1 + 0 |
| [pairs] | = | 25151 |
| [a__nats] | = | 25151 |
| [a__pairs#] | = | 0 |
| [a__odds] | = | 25151 |
| [tail(x1)] | = | x1 + 1 |
| [mark#(x1)] | = | x1 + 15923 |
| [0] | = | 9227 |
| [odds] | = | 25151 |
| [a__nats#] | = | 0 |
| [mark(x1)] | = | x1 + 0 |
| [nats] | = | 25151 |
| [a__incr#(x1)] | = | x1 + 0 |
| [head(x1)] | = | x1 + 46823 |
| [cons(x1, x2)] | = | max(x1 + 15924, x2 + 0, 0) |
| [a__odds#] | = | 25152 |
| [a__pairs] | = | 25151 |
| [a__tail(x1)] | = | x1 + 1 |
| [a__tail#(x1)] | = | 0 |
| [a__head(x1)] | = | x1 + 46823 |
| a__pairs | → | pairs | (18) |
| a__incr(cons(X,XS)) | → | cons(s(mark(X)),incr(XS)) | (4) |
| mark(s(X)) | → | s(mark(X)) | (15) |
| mark(incr(X)) | → | a__incr(mark(X)) | (8) |
| a__nats | → | cons(0,incr(nats)) | (1) |
| a__odds | → | a__incr(a__pairs) | (3) |
| a__nats | → | nats | (16) |
| a__tail(X) | → | tail(X) | (21) |
| a__odds | → | odds | (19) |
| a__incr(X) | → | incr(X) | (17) |
| a__head(cons(X,XS)) | → | mark(X) | (5) |
| mark(odds) | → | a__odds | (10) |
| mark(nats) | → | a__nats | (7) |
| a__head(X) | → | head(X) | (20) |
| mark(0) | → | 0 | (14) |
| mark(tail(X)) | → | a__tail(mark(X)) | (12) |
| mark(head(X)) | → | a__head(mark(X)) | (11) |
| mark(pairs) | → | a__pairs | (9) |
| mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (13) |
| a__tail(cons(X,XS)) | → | mark(XS) | (6) |
| a__pairs | → | cons(0,incr(odds)) | (2) |
| a__incr#(cons(X,XS)) | → | mark#(X) | (32) |
| mark#(incr(X)) | → | a__incr#(mark(X)) | (24) |
| a__odds# | → | a__incr#(a__pairs) | (26) |
| mark#(odds) | → | a__odds# | (25) |
| mark#(cons(X1,X2)) | → | mark#(X1) | (22) |
The dependency pairs are split into 1 component.
| mark#(s(X)) | → | mark#(X) | (36) |
| mark#(incr(X)) | → | mark#(X) | (28) |
| [incr(x1)] | = | x1 + 4 |
| [s(x1)] | = | x1 + 1 |
| [a__head#(x1)] | = | 1 |
| [a__incr(x1)] | = | 3 |
| [pairs] | = | 3 |
| [a__nats] | = | 2 |
| [a__pairs#] | = | 0 |
| [a__odds] | = | 2 |
| [tail(x1)] | = | 3 |
| [mark#(x1)] | = | x1 + 0 |
| [0] | = | 2 |
| [odds] | = | 3 |
| [a__nats#] | = | 0 |
| [mark(x1)] | = | 1 |
| [nats] | = | 0 |
| [a__incr#(x1)] | = | 0 |
| [head(x1)] | = | x1 + 1 |
| [cons(x1, x2)] | = | 4 |
| [a__odds#] | = | 0 |
| [a__pairs] | = | 2 |
| [a__tail(x1)] | = | 2 |
| [a__tail#(x1)] | = | 1 |
| [a__head(x1)] | = | 0 |
| mark#(s(X)) | → | mark#(X) | (36) |
| mark#(incr(X)) | → | mark#(X) | (28) |
The dependency pairs are split into 0 components.