proposition: Theorem locking_clients_eventually_receive_lock_st : forall c s, event_step_star step_async step_async_init (hd s) -> lb_step_execution lb_step_async s -> weak_fairness lb_step_async label_silent s -> now (occurred (InputLock c)) s -> eventually (fun s => held (nwState (evt_a (hd s)) (Client c)) = true) s.
proof: Proof. Proof using. intros. find_eapply_lem_hyp locking_clients_eventually_receive_lock_lb; eauto. apply eventually_next. eapply eventually_monotonic with (J := lb_step_execution lb_step_async). 4:eauto. all:eauto using lb_step_execution_invar. eauto using MsgLocked_held. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)