proposition: Lemma not_null_copy1: forall (G: Graph) (x x0: addr) l r, vgamma G x = (null, l, r) -> vvalid G x -> x0 <> null -> vcopy1 x G (Graph_vgen G x x0) (initial_copied_Graph x x0 G) /\ x0 = LocalGraphCopy.vmap (Graph_vgen G x x0) x /\ is_guarded_BinMaFin' (fun v => x0 <> v) (fun e => ~ In e nil) (initial_copied_Graph x x0 G).
proof: Proof. intros. split; [split; [| split] | split]. + reflexivity. + split; [| split]. - reflexivity. - simpl. unfold update_vlabel. destruct_eq_dec x x; congruence. - intros. simpl. unfold update_vlabel; simpl. destruct_eq_dec x n'; [congruence |]. tauto. + split; [| split; [| split]]. - reflexivity. - apply guarded_pointwise_relation_spec; intros. simpl. unfold update_vlabel; simpl. destruct_eq_dec x x1; [congruence | auto]. - apply guarded_pointwise_relation_spec; intros. auto. - reflexivity. + simpl. unfold update_vlabel; simpl. destruct_eq_dec x x; [auto | congruence]. + assert (LocalGraphCopy.vmap (Graph_vgen G x x0) x = x0). 1: { simpl. unfold update_vlabel; simpl. destruct_eq_dec x x; auto; congruence. } pattern x0 at 1; rewrite <- H2. apply single_vertex_guarded_BinMaFin'. Qed.
imports: CertiGraph.lib.Ensembles_ext Coq.Lists.List VST.msl.seplog VST.msl.log_normalize VST.msl.ramification_lemmas VST.msl.Coqlib2 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon 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 CertiGraph.msl_application.GraphBin CertiGraph.msl_application.Graph_Copy Coq.Logic.Classical