proposition: Theorem locking_clients_eventually_receive_lock_lb : 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 (now (occurred (MsgLocked c))) s.
proof: Proof. Proof using. intros c s Hss Hlbs Hfair. match goal with | H : _ (hd s) |- _ => pattern s in H end. match goal with | H1 : ?J1 s, H2 : ?J2 s, H3 : ?J3 s |- _ => assert ((J1 /\_ J2 /\_ J3) s) as Hand by (now unfold and_tl); clear H1; clear H2; clear H3 end; simpl in *. intros. eapply eventually_trans. 4:eapply InputLock_eventually_MsgLock; eauto; unfold and_tl in *; intuition. 3:apply Hand. all:unfold and_tl in *. all:intuition eauto using lb_step_execution_invar, weak_fairness_invar. - find_apply_lem_hyp step_async_star_lb_step_execution; auto. destruct s0. simpl in *. find_apply_lem_hyp always_Cons. intuition. find_apply_lem_hyp always_Cons. intuition. - eauto using MsgLock_eventually_MsgLocked. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)