proposition: Lemma svfl_add_tail: forall from to v l roots i g1 g2 g3, scan_vertex_for_loop from to v l g1 g2 -> forward_relation from to 0 (forward_p2forward_t (inr (v, Z.of_nat i)) roots g2) g2 g3 -> scan_vertex_for_loop from to v (l +:: i) g1 g3.
proof: Proof. do 4 intro. revert from to v. induction l; intros; inversion H; subst. - simpl. rewrite forward_p2t_inr_roots in H0. apply svfl_cons with g3. 1: assumption. constructor. - simpl app. apply svfl_cons with g4. 1: assumption. apply IHl with roots g2; 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