Go backward to While Loops Go up to Top Go forward to Reasoning about Least Fixed Points |
To prove P(fix F), it suffices to prove
If predicate holds for every element of chain, it also holds for its least upper bound.
Mainly useful for showing equivalences of program constructs.