proposition: Lemma eventually_MsgUnlock : forall n 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 -> Nth (queue (nwState (evt_a (hd s)) Server)) (S n) c -> eventually (now (occurred MsgUnlock)) s.
proof: Proof. Proof using. intros n c s Hstar Hexec Hfair HNth. pattern s in Hexec. pattern s in Hfair. find_copy_eapply_lem_hyp eventually_Unlock; eauto. break_exists. match goal with | H1 : (fun x => ?J1) s, H2 : (fun x => ?J2) s |- _ => assert (and_tl (fun x => J1) (fun x => J2) s) as Hand by (now unfold and_tl); clear H1; clear H2 end; simpl in *. eapply eventually_trans. 4:eauto. 3:apply Hand. 2:intros; eapply Unlock_in_network_eventually_MsgUnlock. all:unfold and_tl in *; intuition eauto. - eauto using lb_step_execution_invar. - simpl. eauto using weak_fairness_invar. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)