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) |
| p(s(s(x))) | → | s(p(s(x))) | (8) |
| p(s(0)) | → | 0 | (9) |
| p(0) | → | 0 | (10) |
| inc(s(x)) | → | s(inc(x)) | (11) |
| inc(0) | → | s(0) | (12) |
| sumList(xs,y) | → | if(isEmpty(xs),isZero(head(xs)),y,tail(xs),cons(p(head(xs)),tail(xs)),inc(y)) | (13) |
| if(true,b,y,xs,ys,x) | → | y | (14) |
| if(false,true,y,xs,ys,x) | → | sumList(xs,y) | (15) |
| if(false,false,y,xs,ys,x) | → | sumList(ys,x) | (16) |
| sum(xs) | → | sumList(xs,0) | (17) |
| p#(s(s(x))) | → | p#(s(x)) | (18) |
| inc#(s(x)) | → | inc#(x) | (19) |
| sumList#(xs,y) | → | inc#(y) | (20) |
| sumList#(xs,y) | → | p#(head(xs)) | (21) |
| sumList#(xs,y) | → | tail#(xs) | (22) |
| sumList#(xs,y) | → | head#(xs) | (23) |
| sumList#(xs,y) | → | isZero#(head(xs)) | (24) |
| sumList#(xs,y) | → | isEmpty#(xs) | (25) |
| sumList#(xs,y) | → | if#(isEmpty(xs),isZero(head(xs)),y,tail(xs),cons(p(head(xs)),tail(xs)),inc(y)) | (26) |
| if#(false,true,y,xs,ys,x) | → | sumList#(xs,y) | (27) |
| if#(false,false,y,xs,ys,x) | → | sumList#(ys,x) | (28) |
| sum#(xs) | → | sumList#(xs,0) | (29) |
The dependency pairs are split into 3 components.
| sumList#(xs,y) | → | if#(isEmpty(xs),isZero(head(xs)),y,tail(xs),cons(p(head(xs)),tail(xs)),inc(y)) | (26) |
| if#(false,true,y,xs,ys,x) | → | sumList#(xs,y) | (27) |
| if#(false,false,y,xs,ys,x) | → | sumList#(ys,x) | (28) |
| [true] | = | 1 |
| [head(x1)] | = | 1 · x1 + -∞ |
| [isEmpty(x1)] | = | -6 · x1 + 2 |
| [nil] | = | 0 |
| [sumList#(x1, x2)] | = | -1 · x1 + -∞ · x2 + 0 |
| [if#(x1,...,x6)] | = | -2 · x1 + 0 · x2 + -∞ · x3 + 0 · x4 + -1 · x5 + -8 · x6 + 0 |
| [0] | = | 6 |
| [p(x1)] | = | 0 · x1 + -∞ |
| [cons(x1, x2)] | = | -1 · x1 + 1 · x2 + -∞ |
| [s(x1)] | = | -1 · x1 + 7 |
| [inc(x1)] | = | -∞ · x1 + 7 |
| [tail(x1)] | = | -1 · x1 + 0 |
| [isZero(x1)] | = | -5 · x1 + 0 |
| [false] | = | 2 |
| inc(s(x)) | → | s(inc(x)) | (11) |
| inc(0) | → | s(0) | (12) |
| p(s(s(x))) | → | s(p(s(x))) | (8) |
| p(s(0)) | → | 0 | (9) |
| p(0) | → | 0 | (10) |
| head(cons(x,xs)) | → | x | (5) |
| tail(cons(x,xs)) | → | xs | (6) |
| tail(nil) | → | nil | (7) |
| isZero(0) | → | true | (3) |
| isZero(s(x)) | → | false | (4) |
| isEmpty(cons(x,xs)) | → | false | (1) |
| isEmpty(nil) | → | true | (2) |
| if#(false,true,y,xs,ys,x) | → | sumList#(xs,y) | (27) |
| [true] | = | 0 |
| [head(x1)] | = | 0 · x1 + -2 |
| [isEmpty(x1)] | = | 0 · x1 + -∞ |
| [nil] | = | 2 |
| [sumList#(x1, x2)] | = | 0 · x1 + -∞ · x2 + 1 |
| [if#(x1,...,x6)] | = | -∞ · x1 + 0 · x2 + -∞ · x3 + -∞ · x4 + 0 · x5 + -∞ · x6 + -∞ |
| [0] | = | 0 |
| [p(x1)] | = | -1 · x1 + 0 |
| [cons(x1, x2)] | = | 0 · x1 + -∞ · x2 + -8 |
| [s(x1)] | = | 1 · x1 + 6 |
| [inc(x1)] | = | -3 · x1 + 2 |
| [tail(x1)] | = | 0 · x1 + -∞ |
| [isZero(x1)] | = | -5 · x1 + 0 |
| [false] | = | 1 |
| p(s(s(x))) | → | s(p(s(x))) | (8) |
| p(s(0)) | → | 0 | (9) |
| p(0) | → | 0 | (10) |
| head(cons(x,xs)) | → | x | (5) |
| isZero(0) | → | true | (3) |
| isZero(s(x)) | → | false | (4) |
| sumList#(xs,y) | → | if#(isEmpty(xs),isZero(head(xs)),y,tail(xs),cons(p(head(xs)),tail(xs)),inc(y)) | (26) |
The dependency pairs are split into 0 components.
| p#(s(s(x))) | → | p#(s(x)) | (18) |
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)) | (18) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| inc#(s(x)) | → | inc#(x) | (19) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| inc#(s(x)) | → | inc#(x) | (19) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.