proposition: Lemma extend_copy_emap_root: forall (g g1 g2 g3: Graph) (g1' g2' g3': Graph') root es es_done e0 es_later (M: V -> Prop), vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> NoDup es -> es = es_done ++ e0 :: es_later -> (forall v : V, M v \/ ~ M v) -> vcopy1 root g g1 g1' -> edge_copy_list g root es_done M (g1, g1') (g2, g2') -> 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 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 (forall v, M_rec v \/ ~ M_rec v) -> extended_copy M_rec (dst g e0) (g2, g2') (g3, g3') -> map (emap g2) es_done = map (emap g3) es_done.
proof: Proof. intros. destruct H8 as [_ [_ [? _]]]. rewrite guarded_pointwise_relation_spec in H8. apply Coqlib.list_map_exten. intros e ?; symmetry. apply (H8 e). intro. pose proof triple_vcopy1_edge_copy_list g g1 g2 g1' g2' root es es_done _ M H H0 H1 H2 H3 H4 H5 H6. destruct H11 as [? [? [? [? [? [? ?]]]]]]. unfold Ensembles.In in H10. rewrite Intersection_spec in H10; destruct H10. unfold weak_edge_prop in H10; apply reachable_by_foot_prop in H10. rewrite <- (si_src2 _ _ _ H12) in H10 by auto. assert (src g e = root). 1: { rewrite H3 in H1. specialize (H1 e). rewrite in_app_iff in H1. pose proof (proj1 H1 (or_introl H9)). destruct H19; auto. } rewrite H19 in H10. apply H10. clear. unfold Ensembles.In. subst M_rec PV1 M0. rewrite !Union_spec. left; right; 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