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.