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) |
| prec(merge) | = | 1 | stat(merge) | = | lex | |
| prec(nil) | = | 2 | stat(nil) | = | mul | |
| prec(.) | = | 0 | stat(.) | = | lex | |
| prec(if) | = | 0 | stat(if) | = | mul | |
| prec(<) | = | 0 | stat(<) | = | lex | |
| prec(++) | = | 3 | stat(++) | = | lex | |
| prec(true) | = | 4 | stat(true) | = | mul | |
| prec(false) | = | 5 | stat(false) | = | mul |
| π(merge) | = | [1,2] |
| π(nil) | = | [] |
| π(.) | = | [1,2] |
| π(if) | = | [1,2,3] |
| π(<) | = | [1,2] |
| π(++) | = | [1,2] |
| π(true) | = | [] |
| π(false) | = | [] |
| 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) |
There are no rules in the TRS. Hence, it is terminating.