proposition: Lemma eventually_Unlock : 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 -> exists c, eventually (fun s => In (mkPacket c Server Unlock) (nwPackets (evt_a (hd s)))) s.
proof: Proof. Proof using. intros. find_apply_lem_hyp Nth_something_at_head. break_exists_name holder. break_exists. exists (Client holder). remember H0 as Hlbs; clear HeqHlbs. invcs H0. find_eapply_lem_hyp head_grant_state_unlock; eauto. intuition. - eapply eventually_trans with (inv := lb_step_execution lb_step_async /\_ weak_fairness (lb_step_async(labeled_multi_params := LockServ_LabeledParams)) Silent) (P := now (occurred (MsgLocked holder))). all:unfold and_tl in *; intuition. + eauto using lb_step_execution_invar. + eauto using weak_fairness_invar. + find_apply_lem_hyp MsgLocked_held; eauto. destruct s. simpl in *. eauto using lb_step_execution_invar, weak_fairness_invar, E_next, held_eventually_Unlock. + apply Locked_in_network_eventually_MsgLocked; auto. - eauto using held_eventually_Unlock. - eauto using E0. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)