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.