proposition: Lemma clients_move_way_up_in_queue : forall n n' c s, n' <= n -> 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 /\ (S n = 0 -> In (mkPacket Server (Client c) Locked) (nwPackets (evt_a (hd s))))) -> 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. induction n; intros; simpl in *; auto. - intuition. assert (n' = 0) by lia. subst. eauto using clients_move_up_in_queue. - 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 *. find_apply_lem_hyp le_lt_eq_dec. intuition. + assert (n' <= n) by lia. find_eapply_lem_hyp clients_move_up_in_queue; eauto; try solve [unfold and_tl in *; intuition]; [idtac]. eapply eventually_trans. 4:eauto. 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. + subst. unfold and_tl in *. intuition. eauto using clients_move_up_in_queue. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)