This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| decl-03 | An Axiom | |
| decl-01 | An Axiom | |
| ADD-lemma | N = N0, V = V0 ⊦ ⟪ADD(S; V, N)⟫ (N = N0 ∪ (S \ V0) ∧ V = V0 ∪ S) | A User Theorem |
| ADD-preserves-INV | INV(C, N, V, n, source), v ∈ C ⊦ ⟪ADD(succ(v); V, N)⟫ INV(C -- v, N, V, n, source) | A User Theorem |
| ADD-preserves-INV-INVR | INV(C, N, V, n, source), v ∈ C, INVR(C, N, V, n, n0, source, dest), v ≠ dest ⊦ ⟪ADD(succ(v); V, N)⟫ (INV(C -- v, N, V, n, source) ∧ INVR(C -- v, N, V, n, n0, source, dest)) | A User Theorem |
| BFS-correct-if-reachable | reach(source, dest, n), ¬ reach<(source, dest, n) ⊦ ⟪BFS(source, dest; norfail)⟫ norfail = some(n) | A User Theorem |
| BFS-returns-fail-implies-not-reachable | ∀ n. ¬ reach(source, dest, n) ⊦ [BFS(source, dest; norfail)] norfail = fail | A User Theorem |