Some obligations are about infinite behaviour: every requester is eventually granted, no requester starves. The flow used in this course has no liveness mode, so true eventually is not expressible here; the course proves bounded response instead, a safety property, and teaches the engine view, fairness and lassos, with runnable substitutes. Liveness-to-safety is the bridge: it rewrites an eventually property as a safety property that a safety engine can run. The arbiter carries the topic: its correct form never makes a persistent requester wait more than 3 cycles (it is granted in the fourth), and its buggy form starves three of them forever.

Suggested order: top to bottom. Fairness first, because every liveness statement needs its environment contract. Lassos second, because the counterexample shape motivates the substitutes. The counter and saved-state constructions third, because they are the routes by which an eventually property reaches a safety engine. The too-strong-fairness trap last, because it is the review rule that guards the other three.