proposition: Lemma frr_semi_iso: forall (from to : nat) (roots1 roots2: roots_t) (g1 g2 : LGraph), from <> to -> sound_gc_graph g1 -> graph_has_gen g1 to -> gen_unmarked g1 from -> roots_graph_compatible roots1 g1 -> no_dangling_dst g1 -> copy_compatible g1 -> forward_roots_relation from to roots1 g1 roots2 g2 -> exists l, gc_graph_semi_iso g1 g2 from to l /\ roots2 = roots_map l roots1.
proof: Proof. intros. pose proof (semi_iso_refl g1 from to H0 H2). apply frl_semi_iso with (g:=g1)(l1:=nil) in H6; auto. destruct H6 as [l2 [? ?]]. rewrite app_nil_r in *. exists l2; split; auto. subst roots2. unfold quasi_roots_map, roots_map. apply Znth_eq_ext. list_solve. intros. rewrite Zlength_map in H8. rewrite !Znth_map by auto. destruct (Znth i roots1) eqn:? ; simpl; auto. f_equal. apply list_map_bi_map. intro. eapply semi_iso_In_map_snd in H9; eauto. apply H9. red in H3. rewrite Forall_forall in H3. destruct H0. red in H0. rewrite H0. apply H3. rewrite <- filter_sum_right_In_iff, <- Heqr. apply Znth_In; auto. 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