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: |
|---|---|---|
| cyclic-def | ⊦ cyclic(r, H) ↔ (∃ m, n, r0. m < n ∧ reachable-n(H, m, r, r0) ∧ reachable-n(H, n, r, r0)) | An Axiom |
| legal-def | ⊦ legal(H) ↔ (∀ r. r ∈ H ∧ H[r] .nxt ≠ null → H[r] .nxt ∈ H) | An Axiom |
| cyclic-all-cyclic | ⊦ reachable-n(H, n, r, r) ∧ reachable-n(H, m, r, r0) → (¬ reachable-n(H, n, r0, r0) ↔ false) | A User Theorem |
| cyclic-all-ncyclic | ⊦ reachable-n(H, n, r, r) ∧ reachable-n(H, m, r, r0) → (¬ reachable-n(H, n0 * n, r0, r0) ↔ false) | A User Theorem |
| cyclic-alt-def | ⊦ cyclic(r, H) ↔ (∃ m, r0. reachable-n(H, m, r, r0) ∧ (∃ n. n ≠ 0 ∧ (∀ n0. reachable-n(H, m + n0 * n, r, r0)))) | A User Theorem |
| cyclic-brent-def | ⊦ cyclic(r, H) ↔ (∃ n, m, r0. m ≠ 0 ∧ m ≤ 2 ^ n ∧ reachable-n(H, 2 ^ n - 1, r, r0) ∧ reachable-n(H, m, r0, r0)) | A User Theorem |
| cyclic-floyd-def | ⊦ cyclic(r, H) ↔ (∃ n, r0. n ≠ 0 ∧ reachable-n(H, n, r, r0) ∧ reachable-n(H, n + n, r, r0)) | A User Theorem |
| cyclic-ncyclic | ⊦ reachable-n(H, n, r, r) → (¬ reachable-n(H, n0 * n, r, r) ↔ false) | A User Theorem |
| cyclic-weak-def | ⊦ cyclic(r, H) ↔ (∀ n. ∃ r0. reachable-n(H, n, r, r0)) | A User Theorem |
| legal-noncylic-equiv-reaches-null | legal(H), r ∈ H, r ≠ null ⊦ ¬ cyclic(r, H) ↔ (∃ r0. reachable(r, r0, H) ∧ H[r0] .nxt = null) | A User Theorem |
| legal-nxt-1 | ⊦ legal(H) ∧ r ∈ H ∧ H[r] .nxt ≠ null → (¬ H[r] .nxt ∈ H ↔ false) | A User Theorem |
| legal-nxt-2 | ⊦ legal(H) ∧ r ∈ H ∧ ¬ H[r] .nxt ∈ H → H[r] .nxt = null | A User Theorem |
| path-dups | ⊦ path(x, H) ∧ dups(x) → cyclic(hd x, H) | A User Theorem |
| path-nodups-subset | ⊦ path(x, H) ∧ ¬ dups(x) → # x ≤ # H | A User Theorem |
| reach-n-next-legal | ⊦ reachable-n(H, n, r, r0) ∧ legal(H) ∧ r ≠ null ∧ r ∈ H → (¬ reachable-n(H, n + 1, r, H[r0] .nxt) ↔ H[r0] .nxt = null) | A User Theorem |