proposition: Lemma copy_extend_copy: forall (g g2 g3: Graph) (g2' g': Graph') root es es_done e0 es_later (M: V -> Prop), vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> NoDup es -> es = es_done ++ e0 :: es_later -> (forall v : V, M v \/ ~ M v) -> let M0 := Union _ M (eq root) in let PV1 := reachable_by_through_set g (map (dst g) es_done) (Complement _ M0) in let PE1 := Intersection _ (weak_edge_prop PV1 g) (evalid g) in let PE1_root e := In e es_done in let M_rec := Union _ M0 PV1 in let PV0 := reachable_by g (dst g e0) (Complement _ M_rec) in let PE0 := Intersection _ (weak_edge_prop PV0 g) (evalid g) in copy M_rec (dst g e0) g2 g3 g' -> disjointed_guard (vvalid g') (vvalid g2') (evalid g') (evalid g2') -> (forall v, M_rec v \/ ~ M_rec v) -> exists g3': Graph', extended_copy M_rec (dst g e0) (g2, g2') (g3, g3') /\ guarded_labeled_graph_equiv (vvalid g') (evalid g') g' g3' /\ guarded_labeled_graph_equiv (vvalid g2') (evalid g2') g2' g3'.
proof: Proof. intros. pose proof disjointed_union_labeledgraph_exists_ll g' g2' H6. destruct H5 as [COPY_si [COPY_gprv [COPY_gpre [COPY_vvalid [COPY_evalid [COPY_consi COPY_bij]]]]]]. spec H8. 1: { destruct (guarded_bij_vmap_image_dec _ _ _ _ _ _ COPY_bij) as [X _]. refine (ex_intro _ _ I). intros v'; specialize (X v'). destruct X; [left | right]. + rewrite Same_set_spec in COPY_vvalid. rewrite (COPY_vvalid v'); auto. + rewrite Same_set_spec in COPY_vvalid. rewrite (COPY_vvalid v'); auto. } spec H8. 1: { destruct (guarded_bij_emap_image_dec _ _ _ _ _ _ COPY_bij) as [X _]. refine (ex_intro _ _ I). intros e'; specialize (X e'). destruct X; [left | right]. + rewrite Same_set_spec in COPY_evalid. rewrite (COPY_evalid e'); auto. + rewrite Same_set_spec in COPY_evalid. rewrite (COPY_evalid e'); auto. } destruct H8 as [g3' [? [? [? ?]]]]; exists g3'. split; [| split]; auto. split; [| split; [| split; [| split; [| split; [| split]]]]]; auto. + rewrite <- COPY_vvalid, <- COPY_evalid. rewrite pregraph_join_iff. rewrite @Prop_join_comm in H9, H10. apply guarded_lge_guarded_si in H8. tauto. + eapply boundary_dst_consistent_si with (G1' := g'); eauto. - apply COPY_bij. - apply (guarded_morphism_proper_aux1 _ _ _ _ g3 g3 g' g3'). * reflexivity. * rewrite <- COPY_vvalid, <- COPY_evalid. apply guarded_lge_guarded_si; auto. * apply COPY_bij. - rewrite <- COPY_vvalid, <- COPY_evalid. apply guarded_lge_guarded_si; auto. + apply (guarded_bij_proper_aux1 _ _ _ _ g3 g3 g' g3'). - reflexivity. - rewrite <- COPY_vvalid, <- COPY_evalid. apply guarded_lge_guarded_si; auto. - apply COPY_bij. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.graph_morphism