proposition: Lemma vcopy1_edge_copy_list_copy: forall root es (g1 g2 g3 g2' g3': Graph), vvalid g1 root -> WeakMarkGraph.unmarked g1 root -> (forall e, In e es <-> out_edges g1 root e) -> NoDup es -> vcopy1 root g1 g2 g2' -> edge_copy_list g1 es (g2, g2') (g3, g3') -> copy root g1 g3 g3'.
proof: Proof. intros. pose proof vcopy1_edge_copy_list_spec root es es nil g1 g2 g3 g2' g3' H H0 (eq_sym (app_nil_r _)) H1 H2 H3 H4. destruct H5. split; [| split]. + pose proof LocalGraphCopy.triple_vcopy1_edge_copy_list g1 g2 g3 g2' g3' root es es nil (WeakMarkGraph.marked g1) H H0 H1 H2 (eq_sym (app_nil_r _)). spec H7; [intro v; destruct (node_pred_dec (WeakMarkGraph.marked g1) v); auto |]. destruct H3 as [_ [_ ?]]. specialize (H7 H3 H5). destruct H7 as [_ [? _]]; auto. + pose proof WeakMarkGraph.mark1_componded_mark_list_mark root (map (dst g1) es) g1 g3 H H0. apply H7. - apply out_edges_step_list; auto. - destruct H3 as [_ [? _]]. split_relation_list (g1 :: g2 :: g2 :: g3 :: nil); auto; apply WeakMarkGraph.eq_do_nothing; auto. + destruct H3 as [_ [_ ?]]. apply (LocalGraphCopy.vcopy1_edge_copy_list_copy g1 g2 g3 g2' g3' root es (WeakMarkGraph.marked g1)); auto. intro v; destruct (node_pred_dec (WeakMarkGraph.marked g1) v); auto. Qed.
imports: VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.dag CertiGraph.graph.weak_mark_lemmas CertiGraph.graph.graph_morphism CertiGraph.graph.local_graph_copy CertiGraph.msl_application.Graph Coq.Logic.Classical