proposition: Lemma clients_only_move_up_in_queue : forall n c s, lb_step_execution lb_step_async s -> Nth (queue (nwState (evt_a (hd s)) Server)) (S n) c -> weak_until (fun s => Nth (queue (nwState (evt_a (hd s)) Server)) (S n) c) (next (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. cofix CIH. destruct s. destruct e. intros Hexec HNth. invcs Hexec. invcs H1. - unfold runGenHandler, NetHandler in *. break_match. + coinductive_case CIH. find_rewrite. simpl. now rewrite_update. + find_apply_lem_hyp ServerNetHandler_lbcases. intuition. * coinductive_case CIH. repeat find_rewrite. simpl. rewrite_update. break_exists. intuition; repeat find_rewrite; try solve_by_inversion. now eauto using Nth_app. * exfalso. clear CIH. subst. invcs HNth. repeat find_reverse_rewrite. simpl in *. repeat find_rewrite. now solve_by_inversion. * clear CIH. apply W0. simpl. fold LockServ_MultiParams in *. repeat find_rewrite. simpl. rewrite_update. repeat find_rewrite. intuition eauto using Nth_tl. break_exists. intuition. subst. find_apply_lem_hyp Nth_tl. repeat find_rewrite. invcs HNth. auto. * coinductive_case CIH. repeat find_rewrite. simpl. now rewrite_update. - unfold runGenHandler in *. find_apply_lem_hyp InputHandler_cases. intuition. + break_exists. break_and. subst. coinductive_case CIH. repeat find_rewrite. simpl. now rewrite_update. + coinductive_case CIH. repeat find_rewrite. simpl. update_destruct; subst; now rewrite_update. - coinductive_case CIH. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)