The rewrite relation of the following conditional TRS is considered.
| add(0,y) | → | y | |
| add(s(x),y) | → | s(add(x,y)) | |
| mul(0,y) | → | 0 | |
| mul(x,0) | → | 0 | |
| mul(s(x),s(y)) | → | s(add(mul(x,s(y)),y)) | |
| leq(0,0) | → | T | |
| leq(s(x),0) | → | F | |
| leq(0,s(y)) | → | T | |
| leq(s(x),s(y)) | → | leq(x,y) | |
| n(xd,xm,xy) | → | add(xd,add(mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))),xm),mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))),xy))) | | leq(0,xd) ≈ T, leq(xd,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))) ≈ T, leq(0,xm) ≈ T, leq(xm,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) ≈ T |