The rewrite relation of the following TRS is considered.
| empty(nil) | → | true | (1) |
| empty(cons(x,l)) | → | false | (2) |
| head(cons(x,l)) | → | x | (3) |
| tail(nil) | → | nil | (4) |
| tail(cons(x,l)) | → | l | (5) |
| rev(nil) | → | nil | (6) |
| rev(cons(x,l)) | → | cons(rev1(x,l),rev2(x,l)) | (7) |
| last(x,l) | → | if(empty(l),x,l) | (8) |
| if(true,x,l) | → | x | (9) |
| if(false,x,l) | → | last(head(l),tail(l)) | (10) |
| rev2(x,nil) | → | nil | (11) |
| rev2(x,cons(y,l)) | → | rev(cons(x,rev2(y,l))) | (12) |
| rev#(cons(x,l)) | → | rev2#(x,l) | (13) |
| last#(x,l) | → | empty#(l) | (14) |
| last#(x,l) | → | if#(empty(l),x,l) | (15) |
| if#(false,x,l) | → | tail#(l) | (16) |
| if#(false,x,l) | → | head#(l) | (17) |
| if#(false,x,l) | → | last#(head(l),tail(l)) | (18) |
| rev2#(x,cons(y,l)) | → | rev2#(y,l) | (19) |
| rev2#(x,cons(y,l)) | → | rev#(cons(x,rev2(y,l))) | (20) |
The dependency pairs are split into 2 components.
| rev2#(x,cons(y,l)) | → | rev2#(y,l) | (19) |
| rev2#(x,cons(y,l)) | → | rev#(cons(x,rev2(y,l))) | (20) |
| rev#(cons(x,l)) | → | rev2#(x,l) | (13) |
| π(rev2#) | = | { 2 } |
| π(rev#) | = | { 1 } |
| π(rev2) | = | { 2 } |
| π(rev) | = | { 1 } |
| π(cons) | = | { 2, 2 } |
| rev2#(x,cons(y,l)) | → | rev2#(y,l) | (19) |
| rev#(cons(x,l)) | → | rev2#(x,l) | (13) |
The dependency pairs are split into 0 components.
| if#(false,x,l) | → | last#(head(l),tail(l)) | (18) |
| last#(x,l) | → | if#(empty(l),x,l) | (15) |
| [if#(x1, x2, x3)] | = | 0 · x1 + -∞ · x2 + 0 · x3 + -∞ |
| [false] | = | 2 |
| [empty(x1)] | = | 1 · x1 + -8 |
| [cons(x1, x2)] | = | 6 · x1 + 10 · x2 + 3 |
| [last#(x1, x2)] | = | -∞ · x1 + 2 · x2 + 0 |
| [head(x1)] | = | 0 · x1 + -4 |
| [nil] | = | 0 |
| [tail(x1)] | = | -8 · x1 + 0 |
| [true] | = | 1 |
| tail(nil) | → | nil | (4) |
| tail(cons(x,l)) | → | l | (5) |
| empty(nil) | → | true | (1) |
| empty(cons(x,l)) | → | false | (2) |
| last#(x,l) | → | if#(empty(l),x,l) | (15) |
The dependency pairs are split into 0 components.