proposition: Lemma reachable_seen : true_in_reachable step_dup step_async_init sequence_seen.
proof: Proof. Proof using. apply true_in_reachable_reqs; unfold sequence_seen; simpl in *; intuition. find_apply_lem_hyp reachable_sane. unfold sequence_sane in *. match goal with H : step_dup _ _ _ |- _ => invcs H end. - unfold seq_num_net_handlers in *. repeat (break_match; try find_inversion; simpl in *; eauto); match goal with | [ H : processPackets _ _ = _ |- _ ] => apply processPackets_num_monotonic in H end; try break_if; simpl in *; intuition; subst; eauto; repeat find_rewrite; (eapply Nat.lt_le_trans; [|eauto]; eauto). * case (name_eq_dec (pSrc p) (pDst p)); intro. + rewrite <- e in H2. rewrite get_set_same_default in H2. rewrite e in H2. case H2; intro. -- rewrite <- H. rewrite <- e. eapply H0. apply in_or_app. right; left. auto. -- eapply H1; eauto. + match goal with | [H: In _ (assoc_default _ (assoc_set _ _ _ _) _ _) |- _ ] => rewrite get_set_diff_default in H end; eauto. * case (name_eq_dec (pSrc p) h); intro. + rewrite <- e in H2. rewrite get_set_same_default in H2. rewrite e in H2. case H2; intro. -- rewrite <- H. rewrite <- e. eapply H0. apply in_or_app. right; left. auto. -- eapply H1; eauto. + match goal with | [H: In _ (assoc_default _ (assoc_set _ _ _ _) _ _) |- _ ] => rewrite get_set_diff_default in H end; eauto. - unfold seq_num_input_handlers in *. repeat (break_match; try find_inversion; simpl in *; eauto); match goal with | [ H : processPackets _ _ = _ |- _ ] => apply processPackets_num_monotonic in H end; try break_if; simpl in *; intuition; subst; eauto; repeat find_rewrite; (eapply Nat.lt_le_trans; [|eauto]; eauto). - eauto. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)