fact: Definition path_correct (g: @DijkGG size inf) (prev: list V) (dist: list Z) src dst p : Prop := valid_path g p /\ path_ends g p src dst /\ path_cost g p <= (size - 1) * (Int.max_signed / size) /\ Znth dst dist = path_cost g p /\ Forall (fun (x: E) => Znth (snd x) prev = fst x) (snd p) /\ acyclic_path g p.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph