The rewrite relation of the following TRS is considered.
| admit(x,nil) | → | nil | (1) |
| admit(x,.(u,.(v,.(w,z)))) | → | cond(=(sum(x,u,v),w),.(u,.(v,.(w,admit(carry(x,u,v),z))))) | (2) |
| cond(true,y) | → | y | (3) |
| prec(admit) | = | 5 | stat(admit) | = | lex | |
| prec(nil) | = | 1 | stat(nil) | = | mul | |
| prec(.) | = | 5 | stat(.) | = | lex | |
| prec(w) | = | 0 | stat(w) | = | mul | |
| prec(cond) | = | 2 | stat(cond) | = | lex | |
| prec(=) | = | 3 | stat(=) | = | mul | |
| prec(sum) | = | 4 | stat(sum) | = | lex | |
| prec(carry) | = | 0 | stat(carry) | = | mul | |
| prec(true) | = | 6 | stat(true) | = | mul |
| π(admit) | = | [2,1] |
| π(nil) | = | [] |
| π(.) | = | [1,2] |
| π(w) | = | [] |
| π(cond) | = | [2,1] |
| π(=) | = | [1,2] |
| π(sum) | = | [1,3,2] |
| π(carry) | = | [1,2,3] |
| π(true) | = | [] |
| admit(x,nil) | → | nil | (1) |
| admit(x,.(u,.(v,.(w,z)))) | → | cond(=(sum(x,u,v),w),.(u,.(v,.(w,admit(carry(x,u,v),z))))) | (2) |
| cond(true,y) | → | y | (3) |
There are no rules in the TRS. Hence, it is terminating.