The rewrite relation of the following TRS is considered.
eq | → | true | (1) |
eq | → | eq | (2) |
eq | → | false | (3) |
inf(X) | → | cons | (4) |
take(0,X) | → | nil | (5) |
take(s,cons) | → | cons | (6) |
length(nil) | → | 0 | (7) |
length(cons) | → | s | (8) |
t0 | = | eq |
→ | eq | |
= | t1 |