proposition: Lemma triple4_ecopy1: forall (g g2 g3: Graph) (g2' g3': Graph') (M: V -> Prop) root es es_done e0 es_later, let M0 := Union _ M (eq root) in vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> es = es_done ++ e0 :: es_later -> guarded_pointwise_relation (Complement V (reachable_by g root (Complement _ M))) eq (vmap g) (vmap g2) -> ecopy1 e0 (g2, g2') (g3, g3') -> guarded_pointwise_relation (Complement V (reachable_by g root (Complement _ M))) eq (vmap g) (vmap g3).
proof: Proof. intros until es_later. intros H_VVALID H_P P0 H_OUT_EDGES H_ES PRE_gpr ECOPY. destruct ECOPY as [ECOPY_si [ECOPY_prv [ECOPY_gpre [? [? ?]]]]]. transitivity (vmap g2); auto. eapply guarded_pointwise_relation_pointwise_relation; 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