Reference
Graph algorithms
8 modules in src/rainbow/algorithms/proofs/graph/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| algorithms.proofs.graph.bellman-ford-convergence-attained | BELLMAN-FORD CONVERGENCE, ATTAINMENT HALF (second half, part (R)). | 1 |
| algorithms.proofs.graph.bellman-ford-convergence-upper | BELLMAN-FORD CONVERGENCE, UPPER HALF (second half, part (U)). | 1 |
| algorithms.proofs.graph.dijkstra-invariant | DIJKSTRA'S INVARIANT (the Dijkstra step family's Level-3 half). | 7 |
| algorithms.proofs.graph.floyd-warshall-convergence-attained | FLOYD-WARSHALL, ATTAINMENT HALF (second half, part (R)). | 1 |
| algorithms.proofs.graph.floyd-warshall-convergence-upper | FLOYD-WARSHALL INVARIANT, UPPER HALF (part (U)). | 1 |
| algorithms.proofs.graph.walk-concat | CONCATENATING WALKS, for the Floyd-Warshall invariant. | 5 |
| algorithms.proofs.graph.walk-cycle-cut | CUTTING A CYCLE OUT OF A WALK, the step of the Bellman-Ford cycle-removal lemma. | 5 |
| algorithms.proofs.graph.walk-shorten | CYCLE REMOVAL: without negative closed walks, every walk over n nodes can be replaced by one of FEWER THAN n arcs with the same ends that is no longer: signed/walk-shorten : no-negative-cycles n W -> forall k x, (forall t <= k, x t < n) -> exists k', k' < n /\ exists y, (forall t <= k', y t < n) /\ y 0 = x 0 /\ y k' = x k /\ walk-length (y, k') <= walk-length (x, k) Proof by strong induction on a | 4 |