proposition: Lemma semi_quasi_iso: forall from to g1 g2 l roots1 roots2, reachable_iff_marked g1 g2 roots1 from -> gc_graph_semi_iso g1 g2 from to l -> roots2 = roots_map l roots1 -> gc_graph_quasi_iso g1 roots1 g2 roots2 from to.
proof: Proof. intros from to g1 g2 l roots1 roots2 Hr H H0. destruct H as [? [? ?]]. split; auto. exists l. split; auto. split. - intros. specialize (H1 _ _ H3). now destruct H1. - destruct (split l) as [from_l to_l]. destruct H2 as [? [? ?]]. split3; auto. destruct H2. split; auto. intros. red in Hr. unfold roots_reachable_in_gen, marked_in_gen in Hr. now rewrite Hr, H5. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics 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 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph