proposition: Lemma reachable_sane : true_in_reachable step_dup step_async_init sequence_sane.
proof: Proof. Proof using. apply inductive_invariant_true_in_reachable. unfold inductive_invariant, inductive. unfold sequence_sane. simpl in *. intuition. match goal with | [ H : step_dup _ _ _ |- _ ] => invcs H end; try find_inversion. - unfold seq_num_net_handlers in *. simpl in *. do_in_app. intuition. + do_in_map. subst; simpl in *. repeat break_match; try find_inversion; simpl in *; intuition. eapply processPackets_correct; eauto. + simpl in *. repeat find_rewrite. do_in_app. repeat break_match; try find_inversion. * rewrite <- e. intuition auto with datatypes. * apply processPackets_num_monotonic in Heqp0. apply Nat.lt_le_trans with (m := (tdNum (nwState a (pDst p0)))); auto. rewrite <- e. intuition auto with datatypes. * intuition auto with datatypes. * intuition auto with datatypes. - unfold seq_num_input_handlers in *. simpl in *. do_in_app. intuition. + do_in_map. subst; simpl in *. repeat break_match; try find_inversion; simpl in *; intuition. eapply processPackets_correct; eauto. + simpl in *. repeat break_match; try find_inversion; simpl in *; find_apply_lem_hyp processPackets_num_monotonic; find_apply_hyp_hyp; try lia. - in_crush; eauto with *. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)