proposition: Lemma triple4_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 M_rec := Union _ M0 PV1 in vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> es = es_done ++ e0 :: es_later -> g ~=~ g1 /\ guarded_pointwise_relation (Complement V (reachable_by g root (Complement _ M))) eq (vmap g) (vmap g1) -> extended_copy M_rec (dst g e0) (g1, g1') (g2, g2') -> guarded_pointwise_relation (Complement V (reachable_by g root (Complement _ M))) eq (vmap g) (vmap g2).
proof: Proof. intros until es_later. intros ? ? ?. intros H_VVALID H_M H_OUT_EDGES H_ES [PRE_si PRE_gpr] COPY. destruct COPY as [COPY_si [COPY_gprv [COPY_gpre [? [? [COPY_DEC COPY_bij]]]]]]. transitivity (vmap g1); auto. eapply guarded_pointwise_relation_weaken; [| eauto]. rewrite <- PRE_si. apply Complement_Included_rev. unfold Included, Ensembles.In; intros. apply step_reachable_by with (dst g e0); auto. + assert (In e0 es) by (rewrite H_ES, in_app_iff; simpl; tauto). rewrite H_OUT_EDGES in H2. destruct H2. exists e0; auto. + eapply reachable_by_weaken; eauto. unfold Included, Ensembles.In; intros. generalize x0, H2. apply Complement_Included_rev. eapply Included_trans; [| apply left_Included_Union]. apply left_Included_Union. 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