proposition: Lemma correspond_reachable : forall net tr_m, step_async_star step_async_init net tr_m -> forall st tr_1, step_1_star init st tr_1 -> inputs_1 tr_1 = inputs_m tr_m -> correspond st (nwState net) tr_1 tr_m.
proof: Proof. Proof using. intros net tr_m H. find_apply_lem_hyp refl_trans_1n_n1_trace. prep_induction H. induction H; intros; subst. - simpl in *. rewrite inputs_m_on_nil' in H3. destruct tr_1; try discriminate. invc H. + simpl. apply correspond_init. + invc H1. discriminate. - repeat concludes. invc H1; simpl in *. + find_apply_lem_hyp PB_net_defn. intuition; subst; try rewrite inputs_m_app in *; try rewrite inputs_m_inr_singleton in *; try rewrite app_nil_r in *; try break_exists; try break_let; try break_and; subst; repeat find_rewrite; eauto using correspond_preserved_primary_same_no_outputs, correspond_preserved_primary_apply_entry, update_nop, update_eq, update_diff, outputs_m_inr_nil_singleton. + find_apply_lem_hyp PB_input_handler_defn. intuition; subst; repeat rewrite snoc_assoc in *; repeat rewrite inputs_m_app in *. * break_exists. break_and. subst. rewrite inputs_m_inr_singleton in *. rewrite app_nil_r in *. rewrite inputs_m_primary_inl_request_singleton in *. find_apply_lem_hyp inputs_1_invert_app. break_exists. break_and. subst. simpl in *. find_inversion. destruct x1. find_apply_lem_hyp step_1_snoc_inv. break_exists. break_and. { eapply correspond_preserved_primary_same_no_outputs; eauto. eapply correspond_preserved_snoc; eauto. - eauto using step_1_singleton_inversion. - rewrite update_eq by auto. auto. - rewrite update_eq by auto. auto. } * rewrite inputs_m_inr_singleton in *. rewrite app_nil_r in *. rewrite inputs_m_inl_read_singleton in *. rewrite app_nil_r in *. eauto using correspond_preserved_primary_same_no_outputs, update_nop, outputs_m_inl_read_singleton, outputs_m_read_response_singleton. * rewrite inputs_m_inr_singleton in *. rewrite inputs_m_backup_singleton in *. repeat rewrite app_nil_r in *. eauto using correspond_preserved_primary_same_no_outputs, update_diff. Qed.
imports: Verdi(Verdi HandlerMonad)