proposition: Lemma inductive_simulation : forall net net' tr, step_async net net' tr -> step_1_star (revert_state net) (revert_state net') (revert_trace tr).
proof: Proof. Proof using. intros. invc H. - repeat rewrite revert_state_defn. simpl. rewrite app_nil_r. simpl in *. find_apply_lem_hyp PB_net_defn. intuition; subst. + rewrite update_nop. constructor. + rewrite update_nop. constructor. + break_exists. intuition; break_let. * intuition. subst. rewrite <- app_nil_r. econstructor; constructor. repeat find_rewrite. rewrite update_eq by auto. auto. * break_exists. intuition. subst. simpl in *. rewrite <- app_nil_r. econstructor; constructor. repeat find_rewrite. rewrite update_eq by auto. auto. + repeat find_rewrite. rewrite update_diff by auto. constructor. - repeat rewrite revert_state_defn. simpl in *. find_apply_lem_hyp PB_input_handler_defn. intuition; subst. + rewrite update_eq by auto. repeat find_rewrite. constructor. + rewrite update_nop. constructor. + rewrite update_diff by auto. constructor. Qed.
imports: Verdi(Verdi HandlerMonad)