proposition: Lemma step_dup_star_revert_simulation : forall net tr, step_dup_star step_async_init net tr -> exists tr', step_async_star step_async_init (revertNetwork net) tr' /\ filterMap trace_non_empty_out tr = filterMap trace_non_empty_out tr'.
proof: Proof. Proof using. intros. remember step_async_init as y in *. revert Heqy. induction H using refl_trans_1n_trace_n1_ind; simpl; intros. - find_rewrite. exists []; simpl. split; auto. apply RT1nTBase. - concludes. subst. break_exists_name tr'. break_and. assert (H_r: reachable step_dup step_async_init x') by (exists tr1; auto). eapply reachable_revert_step in H_r; eauto. break_or_hyp. * exists (tr' ++ tr2); split. + eapply refl_trans_1n_trace_trans; eauto. rewrite <- (app_nil_r tr2). eapply RT1nTStep; eauto. apply RT1nTBase. + rewrite filterMap_app. rewrite filterMap_app. find_reverse_rewrite. reflexivity. * break_and. find_rewrite. exists tr'; split; simpl; auto. match goal with | [H : filterMap _ _ = filterMap _ _ |- _ ] => rewrite <- H end. rewrite filterMap_app. destruct tr2; simpl in *; [ rewrite app_nil_r | idtac ]; auto. match goal with | [H : _ = [] |- _ ] => rewrite H end. rewrite app_nil_r; auto. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)