The rewrite relation of the following TRS is considered.
| if(true,x,y) | → | x | (1) |
| if(false,x,y) | → | y | (2) |
| if(x,y,y) | → | y | (3) |
| if(if(x,y,z),u,v) | → | if(x,if(y,u,v),if(z,u,v)) | (4) |
| [if(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
| [true] | = | 2 |
| [false] | = | 2 |
| [u] | = | 0 |
| [v] | = | 0 |
| if(true,x,y) | → | x | (1) |
| if(false,x,y) | → | y | (2) |
| [if(x1, x2, x3)] | = | 1 + 2 · x1 + 1 · x2 + 1 · x3 |
| [u] | = | 0 |
| [v] | = | 0 |
| if(x,y,y) | → | y | (3) |
| prec(if) | = | 0 | stat(if) | = | lex | |
| prec(u) | = | 1 | stat(u) | = | lex | |
| prec(v) | = | 1 | stat(v) | = | lex |
| π(if) | = | [1,2,3] |
| π(u) | = | [] |
| π(v) | = | [] |
| if(if(x,y,z),u,v) | → | if(x,if(y,u,v),if(z,u,v)) | (4) |
There are no rules in the TRS. Hence, it is terminating.