The rewrite relation of the following TRS is considered.
| isEmpty(cons(x,xs)) | → | false | (1) |
| isEmpty(nil) | → | true | (2) |
| isZero(0) | → | true | (3) |
| isZero(s(x)) | → | false | (4) |
| head(cons(x,xs)) | → | x | (5) |
| tail(cons(x,xs)) | → | xs | (6) |
| tail(nil) | → | nil | (7) |
| append(nil,x) | → | cons(x,nil) | (8) |
| append(cons(y,ys),x) | → | cons(y,append(ys,x)) | (9) |
| p(s(s(x))) | → | s(p(s(x))) | (10) |
| p(s(0)) | → | 0 | (11) |
| p(0) | → | 0 | (12) |
| inc(s(x)) | → | s(inc(x)) | (13) |
| inc(0) | → | s(0) | (14) |
| addLists(xs,ys,zs) | → | if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys))) | (15) |
| if(true,true,b,xs,ys,xs2,ys2,zs,zs2) | → | zs | (16) |
| if(true,false,b,xs,ys,xs2,ys2,zs,zs2) | → | differentLengthError | (17) |
| if(false,true,b,xs,ys,xs2,ys2,zs,zs2) | → | differentLengthError | (18) |
| if(false,false,false,xs,ys,xs2,ys2,zs,zs2) | → | addLists(xs2,ys2,zs) | (19) |
| if(false,false,true,xs,ys,xs2,ys2,zs,zs2) | → | addLists(xs,ys,zs2) | (20) |
| addList(xs,ys) | → | addLists(xs,ys,nil) | (21) |
| append#(cons(y,ys),x) | → | append#(ys,x) | (22) |
| p#(s(s(x))) | → | p#(s(x)) | (23) |
| inc#(s(x)) | → | inc#(x) | (24) |
| addLists#(xs,ys,zs) | → | append#(zs,head(ys)) | (25) |
| addLists#(xs,ys,zs) | → | head#(ys) | (26) |
| addLists#(xs,ys,zs) | → | inc#(head(ys)) | (27) |
| addLists#(xs,ys,zs) | → | p#(head(xs)) | (28) |
| addLists#(xs,ys,zs) | → | tail#(ys) | (29) |
| addLists#(xs,ys,zs) | → | tail#(xs) | (30) |
| addLists#(xs,ys,zs) | → | head#(xs) | (31) |
| addLists#(xs,ys,zs) | → | isZero#(head(xs)) | (32) |
| addLists#(xs,ys,zs) | → | isEmpty#(ys) | (33) |
| addLists#(xs,ys,zs) | → | isEmpty#(xs) | (34) |
| addLists#(xs,ys,zs) | → | if#(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys))) | (35) |
| if#(false,false,false,xs,ys,xs2,ys2,zs,zs2) | → | addLists#(xs2,ys2,zs) | (36) |
| if#(false,false,true,xs,ys,xs2,ys2,zs,zs2) | → | addLists#(xs,ys,zs2) | (37) |
| addList#(xs,ys) | → | addLists#(xs,ys,nil) | (38) |
The dependency pairs are split into 4 components.
| addLists#(xs,ys,zs) | → | if#(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys))) | (35) |
| if#(false,false,false,xs,ys,xs2,ys2,zs,zs2) | → | addLists#(xs2,ys2,zs) | (36) |
| if#(false,false,true,xs,ys,xs2,ys2,zs,zs2) | → | addLists#(xs,ys,zs2) | (37) |
| [true] | = | 1 |
| [head(x1)] | = | 0 · x1 + -∞ |
| [isEmpty(x1)] | = | 1 · x1 + 7 |
| [nil] | = | 0 |
| [0] | = | 6 |
| [append(x1, x2)] | = | 4 · x1 + 0 · x2 + 0 |
| [cons(x1, x2)] | = | 0 · x1 + 3 · x2 + -2 |
| [s(x1)] | = | 0 · x1 + 4 |
| [if#(x1,...,x9)] | = | -∞ · x1 + -∞ · x2 + 0 · x3 + 0 · x4 + -4 · x5 + -3 · x6 + -6 · x7 + -∞ · x8 + -∞ · x9 + -4 |
| [inc(x1)] | = | 0 · x1 + 0 |
| [addLists#(x1, x2, x3)] | = | -3 · x1 + -6 · x2 + -∞ · x3 + 0 |
| [p(x1)] | = | 0 · x1 + -∞ |
| [tail(x1)] | = | -3 · x1 + 0 |
| [isZero(x1)] | = | -4 · x1 + 0 |
| [false] | = | 0 |
| head(cons(x,xs)) | → | x | (5) |
| inc(s(x)) | → | s(inc(x)) | (13) |
| inc(0) | → | s(0) | (14) |
| tail(cons(x,xs)) | → | xs | (6) |
| tail(nil) | → | nil | (7) |
| p(s(s(x))) | → | s(p(s(x))) | (10) |
| p(s(0)) | → | 0 | (11) |
| p(0) | → | 0 | (12) |
| isZero(0) | → | true | (3) |
| isZero(s(x)) | → | false | (4) |
| if#(false,false,true,xs,ys,xs2,ys2,zs,zs2) | → | addLists#(xs,ys,zs2) | (37) |
| [true] | = | 0 |
| [head(x1)] | = | 0 · x1 + -∞ |
| [isEmpty(x1)] | = | 3 · x1 + -∞ |
| [nil] | = | 1 |
| [0] | = | 0 |
| [append(x1, x2)] | = | 0 · x1 + -8 · x2 + 0 |
| [cons(x1, x2)] | = | 1 · x1 + -∞ · x2 + 0 |
| [s(x1)] | = | 3 · x1 + 3 |
| [if#(x1,...,x9)] | = | -10 · x1 + -∞ · x2 + 2 · x3 + -∞ · x4 + -∞ · x5 + 3 · x6 + -∞ · x7 + -∞ · x8 + -∞ · x9 + -∞ |
| [inc(x1)] | = | 1 · x1 + 2 |
| [addLists#(x1, x2, x3)] | = | 2 · x1 + -∞ · x2 + -∞ · x3 + 4 |
| [p(x1)] | = | -2 · x1 + 0 |
| [tail(x1)] | = | -1 · x1 + 0 |
| [isZero(x1)] | = | 0 · x1 + -∞ |
| [false] | = | 3 |
| head(cons(x,xs)) | → | x | (5) |
| p(s(s(x))) | → | s(p(s(x))) | (10) |
| p(s(0)) | → | 0 | (11) |
| p(0) | → | 0 | (12) |
| isZero(0) | → | true | (3) |
| isZero(s(x)) | → | false | (4) |
| isEmpty(cons(x,xs)) | → | false | (1) |
| isEmpty(nil) | → | true | (2) |
| if#(false,false,false,xs,ys,xs2,ys2,zs,zs2) | → | addLists#(xs2,ys2,zs) | (36) |
The dependency pairs are split into 0 components.
| p#(s(s(x))) | → | p#(s(x)) | (23) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| p#(s(s(x))) | → | p#(s(x)) | (23) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| inc#(s(x)) | → | inc#(x) | (24) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| inc#(s(x)) | → | inc#(x) | (24) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| append#(cons(y,ys),x) | → | append#(ys,x) | (22) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| append#(cons(y,ys),x) | → | append#(ys,x) | (22) |
| 2 | ≥ | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.