The rewrite relation of the following TRS is considered.
merge(nil,y) | → | y | (1) |
merge(x,nil) | → | x | (2) |
merge(.(x,y),.(u,v)) | → | if(<(x,u),.(x,merge(y,.(u,v))),.(u,merge(.(x,y),v))) | (3) |
++(nil,y) | → | y | (4) |
++(.(x,y),z) | → | .(x,++(y,z)) | (5) |
if(true,x,y) | → | x | (6) |
if(false,x,y) | → | x | (7) |
merge#(.(x,y),.(u,v)) | → | if#(<(x,u),.(x,merge(y,.(u,v))),.(u,merge(.(x,y),v))) | (8) |
merge#(.(x,y),.(u,v)) | → | merge#(y,.(u,v)) | (9) |
++#(.(x,y),z) | → | ++#(y,z) | (10) |
merge#(.(x,y),.(u,v)) | → | merge#(.(x,y),v) | (11) |
The dependency pairs are split into 2 components.
++#(.(x,y),z) | → | ++#(y,z) | (10) |
[merge(x1, x2)] | = | 0 |
[<(x1, x2)] | = | 0 |
[++(x1, x2)] | = | 0 |
[false] | = | 0 |
[merge#(x1, x2)] | = | 0 |
[true] | = | 0 |
[if(x1, x2, x3)] | = | 0 |
[++#(x1, x2)] | = | x1 + 0 |
[nil] | = | 0 |
[.(x1, x2)] | = | x2 + 1 |
[if#(x1, x2, x3)] | = | 0 |
++#(.(x,y),z) | → | ++#(y,z) | (10) |
The dependency pairs are split into 0 components.
merge#(.(x,y),.(u,v)) | → | merge#(.(x,y),v) | (11) |
merge#(.(x,y),.(u,v)) | → | merge#(y,.(u,v)) | (9) |
[merge(x1, x2)] | = | 0 |
[<(x1, x2)] | = | 0 |
[++(x1, x2)] | = | 0 |
[false] | = | 0 |
[merge#(x1, x2)] | = | x1 + 0 |
[true] | = | 0 |
[if(x1, x2, x3)] | = | 0 |
[++#(x1, x2)] | = | 0 |
[nil] | = | 0 |
[.(x1, x2)] | = | x2 + 1 |
[if#(x1, x2, x3)] | = | 0 |
merge#(.(x,y),.(u,v)) | → | merge#(y,.(u,v)) | (9) |
The dependency pairs are split into 1 component.
merge#(.(x,y),.(u,v)) | → | merge#(.(x,y),v) | (11) |
[merge(x1, x2)] | = | 0 |
[<(x1, x2)] | = | 0 |
[++(x1, x2)] | = | 0 |
[false] | = | 0 |
[merge#(x1, x2)] | = | x2 + 0 |
[true] | = | 0 |
[if(x1, x2, x3)] | = | 0 |
[++#(x1, x2)] | = | 0 |
[nil] | = | 0 |
[.(x1, x2)] | = | x2 + 1 |
[if#(x1, x2, x3)] | = | 0 |
merge#(.(x,y),.(u,v)) | → | merge#(.(x,y),v) | (11) |
The dependency pairs are split into 0 components.