fact: Fixpoint prog_list_helper (i: nat) (n: nat) : list (val * val) := match n with | O => nil | S n' => if (le_dec i n') then (Vundef, Vundef) :: prog_list_helper i n' else (Vint (Int.repr (Z.of_nat (n'))), Vint (Int.repr 0)) :: prog_list_helper i n' end.
imports: CertiGraph.lib.List_ext CertiGraph.unionfind.env_unionfind_arr CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.graph.UnionFind CertiGraph.msl_application.ArrayGraph CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_array_graph Coq.Lists.List CertiGraph.unionfind.uf_arr_specs VST.floyd.library