proposition: Lemma triple2_copy: forall (g g1 g2: Graph) (g1' g2': Graph') (M: V -> Prop) root es es_done e0 es_later, vvalid g root -> ~ M root -> let M0 := Union _ M (eq root) in (forall e, In e es <-> out_edges g root e) -> es = es_done ++ e0 :: es_later -> 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 g ~=~ g1 -> 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 extended_copy M_rec (dst g e0) (g1, g1') (g2, g2') -> g ~=~ g2.
proof: Proof. intros. destruct H4 as [? [? [? [? [? [? [? ?]]]]]]]. transitivity g1; auto. 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