proposition: Lemma MsgLock_in_queue_or_Locked : forall c s, lb_step_execution lb_step_async s -> weak_fairness lb_step_async label_silent s -> now (occurred (MsgLock c)) s -> next (fun s => In (mkPacket Server (Client c) Locked) (nwPackets (evt_a (hd s)))) s \/ exists n, next (fun s => Nth (queue (nwState (evt_a (hd s)) Server)) (S n) c) s.
proof: Proof. Proof using. intros. invcs H. invcs H2. - monad_unfold. unfold NetHandler in *. break_match_hyp. + unfold occurred in *. find_apply_lem_hyp ClientNetHandler_lbcases; intuition; congruence. + unfold occurred in *. find_apply_lem_hyp ServerNetHandler_lbcases; intuition; break_exists; intuition; try congruence; [left|right]; fold LockServ_MultiParams in *; repeat find_rewrite; simpl. * left. congruence. * update_destruct_max_simplify; try congruence. find_inversion. repeat find_rewrite. destruct (queue (nwState (evt_a e) Server)) eqn:?; try congruence. exists (length l). simpl. constructor. apply Nth_snoc. - monad_unfold. find_apply_lem_hyp InputHandler_lbcases. intuition; try congruence. break_exists. intuition; congruence. - unfold occurred in *. congruence. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)