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) |
| admit#(x,.(u,.(v,.(w,z)))) | → | admit#(carry(x,u,v),z) | (4) |
| admit#(x,.(u,.(v,.(w,z)))) | → | cond#(=(sum(x,u,v),w),.(u,.(v,.(w,admit(carry(x,u,v),z))))) | (5) |
The dependency pairs are split into 1 component.
| admit#(x,.(u,.(v,.(w,z)))) | → | admit#(carry(x,u,v),z) | (4) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| admit#(x,.(u,.(v,.(w,z)))) | → | admit#(carry(x,u,v),z) | (4) |
| 2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.