The rewrite relation of the following conditional TRS is considered.
| size(empty) | → | 0 | |
| size(push(x,y)) | → | s(size(x)) | |
| m | → | s(s(s(s(0)))) | |
| pop(empty) | → | empty | |
| pop(push(x,y)) | → | x | | le(size(x),m) ≈ true |
| top(empty) | → | eentry | |
| top(push(x,y)) | → | y | | le(size(x),m) ≈ true |
| le(x,0) | → | false | |
| le(0,s(x)) | → | true | |
| le(s(x),s(y)) | → | le(x,y) |