proposition: Lemma forward_loop_add_tail_vpp: forall from to depth x g g1 g2 g3 roots i, 0 <= i < Zlength (raw_fields (vlabel g x)) -> forward_loop from to depth (sublist 0 i (vertex_pos_pairs g x)) g1 g2 -> forward_relation from to depth (forward_p2forward_t (inr (x, i)) roots g2) g2 g3 -> forward_loop from to depth (sublist 0 (i + 1) (vertex_pos_pairs g x)) g1 g3.
proof: Proof. intros. rewrite <- vpp_Zlength in H. rewrite sublist_last_1; [|lia..]. rewrite vpp_Zlength in H. rewrite vpp_Znth by assumption. apply forward_loop_add_tail with (g2 := g2) (roots := roots); 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