proposition: Lemma lacv_unmarked_gen_size: forall g v to from, from <> to -> graph_has_gen g to -> unmarked_gen_size g from = unmarked_gen_size (lgraph_add_copied_v g v to) from.
proof: Proof. intros. unfold unmarked_gen_size. rewrite lacv_nth_gen by assumption. remember (nat_inc_list (number_of_vertices (nth_gen g from))) as l. assert (forall i, (from, i) <> new_copied_v g to). { intros. intro. inversion H1. apply H. assumption. } assert (filter (fun i : nat => negb (raw_mark (vlabel g (from, i)))) l = filter (fun i : nat => negb(raw_mark(vlabel(lgraph_add_copied_v g v to) (from,i)))) l). { apply filter_ext. intros. rewrite lacv_vlabel_old by apply H1. reflexivity. } rewrite <- H2. apply fold_left_ext. intros. unfold vertex_size_accum. f_equal. unfold vertex_size. rewrite lacv_vlabel_old by apply H1. reflexivity. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen