proposition: Lemma do_gen_graph_unmarked: forall from to roots roots' g g', graph_has_gen g to -> do_generation_relation from to roots roots' g g' -> graph_unmarked g -> graph_unmarked g'.
proof: Proof. intros. destruct H0 as [g1 [g2 [? [? ?]]]]. rewrite graph_gen_unmarked_iff in H1. assert (forall gen, from <> gen -> gen_unmarked g1 gen) by (intros; eapply frr_gen_unmarked; eauto). assert (forall gen, from <> gen -> gen_unmarked g2 gen). { intros. destruct H2 as [n [? ?]]. eapply (svwl_gen_unmarked _ _ _ g1 g2); eauto. rewrite <- frr_graph_has_gen; eauto. } subst g'. rewrite graph_gen_unmarked_iff. intros. destruct (Nat.eq_dec from gen). - subst. apply gen_unmarked_reset_same. - apply gen_unmarked_reset_diff. apply H5. assumption. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen