proposition: Lemma triple6_copy: forall (g g1 g2: Graph) (g1' g2': Graph') (M: V -> Prop) root es es_done e0 es_later, let M0 := Union _ M (eq root) in 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 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 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 vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> es = es_done ++ e0 :: es_later -> Same_set (vvalid g1') (image_set (Union _ PV1 (eq root)) (vmap g1)) /\ Same_set (evalid g1') (image_set (Union _ PE1 PE1_root) (emap g1)) /\ g ~=~ g1 -> extended_copy M_rec (dst g e0) (g1, g1') (g2, g2') -> (forall v : V, M v \/ ~ M v) -> Same_set (vvalid g2') (image_set (Union _ PV3 (eq root)) (vmap g2)) /\ Same_set (evalid g2') (image_set (Union _ PE3 PE1_root) (emap g2)).
proof: Proof. intros until es_later. intros ? ? ? ? ? ? ? ? ?. intros H_VVALID H_P H_OUT_EDGES H_ES [PRE_vvalid [PRE_evalid PRE_si]] COPY M_DEC. destruct COPY as [COPY_si [COPY_gprv [COPY_gpre [COPY_pj [? [COPY_DEC COPY_bij]]]]]]. erewrite (aux18 root PV1 PV3 PV0) by first [eassumption | reflexivity]. erewrite (aux19 PE1 PE1_root PE3 PE0) by first [eassumption | reflexivity]. rewrite <- PRE_si in COPY_si. rewrite <- PRE_si in COPY_gprv at 1. rewrite <- PRE_si in COPY_gpre at 1. rewrite <- (weak_edge_prop_si _ _ _ PRE_si) in COPY_gpre. rewrite <- PRE_si in COPY_pj at 1 2. rewrite <- (weak_edge_prop_si _ _ _ PRE_si) in COPY_pj. apply guarded_pointwise_relation_weaken with (P2 := Union V PV1 (eq root)) in COPY_gprv. 2: { apply Included_Complement_Disjoint. apply Union_left_Disjoint. split; [eapply (aux06 PV1 PV0) | eapply (aux08 root PV0)]; first [eassumption | reflexivity]. } apply guarded_pointwise_relation_weaken with (P2 := Union E PE1 PE1_root) in COPY_gpre. 2: { apply Included_Complement_Disjoint. apply Union_left_Disjoint. split; [eapply (aux07 PE1 PE0) | eapply (aux09 PE1_root PE0)]; first [eassumption | reflexivity]. } rewrite COPY_gprv in PRE_vvalid. rewrite COPY_gpre in PRE_evalid. split. + destruct COPY_pj as [? _]. destruct H0. rewrite image_Union. rewrite Same_set_spec in PRE_vvalid |- *; intro v'; specialize (PRE_vvalid v'). clear - H0 PRE_vvalid. unfold PV0. rewrite H0, PRE_vvalid, Union_spec. reflexivity. + destruct COPY_pj as [_ [? _]]. destruct H0. rewrite image_Union. rewrite Same_set_spec in PRE_evalid |- *; intro v'; specialize (PRE_evalid v'). clear - H0 PRE_evalid. unfold PE0. rewrite H0, PRE_evalid, Union_spec. reflexivity. 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