proposition: Lemma super_compatible_add: forall g ti gi sp i (Hs: 0 <= i < MAX_SPACES) roots out, ~ graph_has_gen g (Z.to_nat i) -> graph_has_gen g (Z.to_nat (i - 1)) -> (forall (gr: LGraph), generation_space_compatible gr (Z.to_nat i, gi, sp)) -> number_of_vertices gi = O -> super_compatible g (ti_heap ti) (frames2rootpairs (ti_frames ti)) roots out -> super_compatible (lgraph_add_new_gen g gi) (add_new_space (ti_heap ti) sp i Hs) (frames2rootpairs (ti_frames ti)) roots out.
proof: Proof. intros. destruct H3 as [? [? [? ?]]]. split; [|split; [|split]]. - apply gti_compatible_add; assumption. - apply fta_compatible_add; [|destruct H5]; assumption. - apply ang_roots_compatible; assumption. - apply ang_outlier_compatible; assumption. 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