proposition: Lemma gc_graph_iso_cons_roots_inv: forall roots1 roots2 g1 g2 p1 p2, gc_graph_iso g1 (p1 :: roots1) g2 (p2 :: roots2) -> gc_graph_iso g1 roots1 g2 roots2.
proof: Proof. intros. destruct H as [vmap12 [vmap21 [emap12 [emap21 [Hroots Hiso]]]]]. simpl in Hroots. inversion Hroots as [[Hhead Hrest]]. clear Hroots. exists vmap12, vmap21, emap12, emap21. split. 1: reflexivity. simpl in Hiso. destruct p1; simpl in Hhead; subst p2. 1: subst; assumption. rewrite <- Hrest. destruct Hiso. split. - clear - Hrest lp_pregraph_iso. assert (v = vmap21 (vmap12 v)) as Hv. { destruct lp_pregraph_iso. rewrite surjective; auto. apply bijective_sym. assumption. } assert (roots1 = map (root_map vmap21) roots2) as Hrest'. { eapply map_root_map_bijective; eauto. destruct lp_pregraph_iso. assumption. } split. + destruct lp_pregraph_iso. assumption. + destruct lp_pregraph_iso. assumption. + eapply pregraph_iso_cons_vvalid; eauto. + remember (vmap12 v) as v'. clear Heqv'. subst v. apply pregraph_iso_exp_sym in lp_pregraph_iso. eapply pregraph_iso_cons_vvalid; eauto. + eapply pregraph_iso_cons_evalid; eauto. + remember (vmap12 v) as v'. clear Heqv'. subst v. apply pregraph_iso_exp_sym in lp_pregraph_iso. eapply pregraph_iso_cons_evalid; eauto. + intros e Hev. pose proof (evalid_reachable_sub_cons v Hev) as Hersd. destruct lp_pregraph_iso. simpl in *. unfold predicate_evalid in *. apply src_bij; assumption. + intros e Hev. pose proof (evalid_reachable_sub_cons v Hev) as Hersd. destruct lp_pregraph_iso. simpl in *. unfold predicate_evalid in *. apply dst_bij; assumption. - intros v0 Hv. apply vlabel_iso. apply vvalid_reachable_sub_cons. assumption. - intros e He. apply elabel_iso. apply evalid_reachable_sub_cons. assumption. 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