proposition: Lemma triple1_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 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 -> guarded_bij (Union _ PV3 (eq root)) (Union _ PE3 PE1_root) (vmap g2) (emap g2) g2 g2' /\ 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') -> guarded_bij (Union _ PV3 (eq root)) (Union _ PE3 PE3_root) (vmap g3) (emap g3) g3 g3'.
proof: Proof. intros until es_later. intros ? ? ? ? ?. intros H_VVALID H_P H_OUT_EDGES H_NODUP H_ES [PRE_bij [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. 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_prv in PRE_vvalid, PRE_bij. rewrite ECOPY_gpre in PRE_evalid, PRE_bij. rewrite <- (Union_Empty_right (Union V PV3 (eq root))). erewrite (aux20 e0 PE1_root PE3 PE3_root) by (eauto; reflexivity). apply guarded_bij_disjointed_union. + split. - rewrite image_Empty. apply Disjoint_Empty_set_right. - destruct ECOPY_pj as [_ [? _]]. apply Prop_join_Disjoint in H1. rewrite PRE_evalid in H1. rewrite image_single; auto. + eapply guarded_bij_proper_aux1; [apply si_guarded_si, ECOPY_si | | exact PRE_bij]. pose proof pregraph_join_guarded_si _ _ _ _ ECOPY_pj. eapply guarded_si_weaken; [| | exact H1]. 1: rewrite Complement_Empty_set; apply Included_Full_set. apply Included_Complement_Disjoint. destruct ECOPY_pj as [_ [? _]]. apply Prop_join_Disjoint in H2. rewrite PRE_evalid in H2. auto. + split; [.. | split]; intros. - apply is_guarded_inj_empty. - apply is_guarded_inj_single. - inversion H1. - subst e. assert (evalid g3 e0). 1: { assert (In e0 es) by (rewrite H_ES, in_app_iff; simpl; tauto). rewrite H_OUT_EDGES in H1. destruct H1 as [? _]. rewrite <- PRE_si in ECOPY_si. rewrite <- (proj1 (proj2 ECOPY_si)); auto. } assert (evalid g3' (emap g3 e0)). 1: { destruct ECOPY_pj as [_ [[? _] _]]. specialize (H2 (emap g3 e0)). tauto. } tauto. - inversion H2. - inversion H2. + split; split; hnf; intros. - inversion H2. - inversion H2. - subst e. apply H. rewrite <- (proj1 PRE_si). eapply aux24; eauto. - subst e. apply H0. rewrite <- (proj1 PRE_si). eapply aux24; eauto. 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