proposition: Lemma clients_move_up_in_queue : 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 (fun s => Nth (queue (nwState (evt_a (hd s)) Server)) n c /\ (n = 0 -> In (mkPacket Server (Client c) Locked) (nwPackets (evt_a (hd s))))) s.
proof: Proof. Proof using. intros n c s Hstar Hexec Hfair HNth. apply eventually_next. pattern s in HNth. 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 eventually_MsgUnlock. - intros. unfold and_tl in *. intuition. eapply MsgUnlock_moves_client; 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 clients_only_move_up_in_queue. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)