proposition: Lemma triple6_ecopy1: forall (g g2 g3: Graph) (g' g2' g3': Graph') (M: V -> Prop) root es es_done e0 es_later, let M0 := Union _ M (eq root) in let PE1_root e := In e es_done in let PV3 := reachable_by_through_set g (map (dst g) (es_done ++ e0 :: nil)) (Complement _ M0) in let PE3 := Intersection _ (weak_edge_prop PV3 g) (evalid g) in let PE3_root e := In e (es_done ++ e0 :: nil) in vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> NoDup es -> es = es_done ++ e0 :: es_later -> Same_set (vvalid g2') (image_set (Union _ PV3 (eq root)) (vmap g2)) /\ Same_set (evalid g2') (image_set (Union _ PE3 PE1_root) (emap g2)) /\ g ~=~ g2 -> ecopy1 e0 (g2, g2') (g3, g3') -> Same_set (vvalid g3') (image_set (Union _ PV3 (eq root)) (vmap g3)) /\ Same_set (evalid g3') (image_set (Union _ PE3 PE3_root) (emap g3)).
proof: Proof. intros until es_later. intros ? ? ? ? ?. intros H_VVALID H_P H_OUT_EDGES H_NODUP H_ES [PRE_vvalid [PRE_evalid PRE_si]] ECOPY. destruct ECOPY as [ECOPY_si [ECOPY_prv [ECOPY_gpre [ECOPY_pj [? ?]]]]]. apply guarded_pointwise_relation_pointwise_relation with (P := Union V PV3 (eq root)) in ECOPY_prv. rewrite ECOPY_prv in PRE_vvalid. apply guarded_pointwise_relation_weaken with (P2 := Union E PE3 PE1_root) in ECOPY_gpre. 2: { apply Included_Complement_Disjoint. apply Union_left_Disjoint; split. + eapply aux10; eauto; reflexivity. + eapply aux11; eauto; reflexivity. } rewrite ECOPY_gpre in PRE_evalid. split. + rewrite !Same_set_spec. intro v'. destruct ECOPY_pj as [[? _] _]. rewrite H1. rewrite (PRE_vvalid v'). tauto. + erewrite (aux20 e0 PE1_root PE3 PE3_root) by (eauto; reflexivity). rewrite image_Union, image_single. rewrite !Same_set_spec. intro e'. destruct ECOPY_pj as [_ [[? _] _]]. rewrite H1. rewrite (PRE_evalid e'). rewrite Union_spec. tauto. 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