The text says to prove that step r x y ==> iter r n x y
(if the transitive closure of r contains x y, then you can go from x to y via r in n steps). The proper lemma should be step r x y ==> exists n. iter r n x y
right? Is there a better place to report this?
The exercise is to
Correct and prove the
following claim.
Ah :face_palm:reading too fast
Last updated: Dec 21 2024 at 16:20 UTC