proposition: Lemma held_eventually_Unlock : forall s c, lb_step_execution lb_step_async s -> weak_fairness lb_step_async label_silent s -> held (nwState (evt_a (hd s)) (Client c)) = true -> eventually (fun s => In (mkPacket (Client c) Server Unlock) (nwPackets (evt_a (hd s)))) s.
proof: Proof. Proof using. intros. apply eventually_next. match goal with | H : context [held] |- _ => pattern s in H end. match goal with | H1 : ?J1 s, H2 : ?J2 s, H3 : ?J3 s |- _ => assert ((J1 /\_ J2 /\_ J3) s) by (now unfold and_tl); eapply weak_until_eventually with (J := (and_tl J1 (and_tl J2 J3))) end; simpl in *. 2:now unfold and_tl. 3:eauto using held_eventually_InputUnlock. - intros. unfold and_tl in *. intuition. eapply InputUnlock_held; eauto. - apply weak_until_always; eauto using lb_step_execution_invar, always_inv. apply weak_until_always; eauto using weak_fairness_invar, always_inv. eauto using held_until_Unlock. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)