proposition: Lemma triple5_ecopy1: forall (g g2 g3: Graph) (g2' g3': Graph') (M: V -> Prop) root es es_done e0 es_later, let PV := reachable_by g root (Complement _ M) in let PE := Intersection E (weak_edge_prop PV g) (evalid g) in 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 -> g ~=~ g2 /\ guarded_pointwise_relation (Complement E PE) eq (emap g) (emap g2) -> ecopy1 e0 (g2, g2') (g3, g3') -> guarded_pointwise_relation (Complement E PE) eq (emap g) (emap g3).
proof: Proof. intros until es_later. intros PV PE M0 H_VVALID H_P H_OUT_EDGES H_ES [PRE_si PRE_gpr] ECOPY. destruct ECOPY as [ECOPY_si [ECOPY_prv [ECOPY_gpre [? [? ?]]]]]. transitivity (emap g2); auto. eapply guarded_pointwise_relation_weaken; [| eauto]. apply Complement_Included_rev. assert (In e0 es) by (rewrite H_ES, in_app_iff; simpl; tauto). rewrite H_OUT_EDGES in H2. destruct H2. unfold PE, Included, Ensembles.In; intros. subst x. rewrite Intersection_spec; split; [| auto]. unfold weak_edge_prop, PV. rewrite H3. apply reachable_by_refl; 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