fact: Definition extended_copy (M: V -> Prop) root (p1 p2: Graph * Graph') := let (g1, g1') := p1 in let (g2, g2') := p2 in let PV := reachable_by g1 root (Complement _ M) in let PE := Intersection _ (weak_edge_prop PV g1) (evalid g1) in g1 ~=~ g2 /\ guarded_pointwise_relation (Complement _ PV) eq (vmap g1) (vmap g2) /\ guarded_pointwise_relation (Complement _ PE) eq (emap g1) (emap g2) /\ pregraph_join (image_set PV (vmap g2)) (image_set PE (emap g2)) g1' g2' /\ boundary_dst_consistent PE (Intersection _ (Complement _ PV) (vvalid g1)) (vmap g2) (emap g2) g2 g2' /\ (forall v, M v \/ ~ M v) /\ guarded_bij PV PE (vmap g2) (emap g2) g2 g2'.
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