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: |
|---|---|---|
| reachable-n-rec | ⊦ reachable-n(H, n + 1, r, r0) ↔ (∃ r1. reachable-1(H, r, r1) ∧ reachable-n(H, n, r1, r0)) | An Axiom |
| path-empty | ⊦ ¬ path([], H) | An Axiom |
| path-one | ⊦ path(r ', H) ↔ ¬ ¬(r ∈ H ∧ r ≠ null) | An Axiom |
| path-two | ⊦ path(r ' + r0 ', H) ↔ ¬ ¬(r ∈ H ∧ r0 ∈ H ∧ r ≠ null ∧ r0 ≠ null ∧ H[r].nxt = r0) | An Axiom |
| path-cons | ⊦ path(r ' + r0 ' + x, H) ↔ ¬ ¬(r ∈ H ∧ r ≠ null ∧ H[r].nxt = r0 ∧ path(r0 ' + x, H)) | An Axiom |
| reachable-def | ⊦ reachable(r, r0, H) ↔ (∃ x. path(r ' + x, H) ∧ (r ' + x).last = r0) | An Axiom |
| reachable-n-base | ⊦ reachable-n(H, 0, r, r0) ↔ r = r0 | An Axiom |
| reachable-1-def | ⊦ reachable-1(H, r, r0) ↔ r ≠ null ∧ r0 ≠ null ∧ r ∈ H ∧ r0 ∈ H ∧ H[r].nxt = r0 | An Axiom |
| reachable-star-def | ⊦ reachable*(H, r, r0) ↔ (∃ n. reachable-n(H, n, r, r0)) | An Axiom |
| acyclic-rem-not-reachable | ∀ r. r ∈ H → ¬ reachable(H[r].nxt, r, H), reachable(r, r0, H), H[r0].nxt ≠ null, H[r0].nxt ∈ H, ce.nxt = H[H[r0].nxt].nxt ⊦ ¬ reachable(r, H[r0].nxt, H[r0, ce]) | A User Theorem |
| add-preserves-reachable | ⊦ H[r1].nxt = H[r2].nxt ∧ ce.nxt = r2 ∧ reachable(r, r0, H) ∧ ¬ reachable(r, r2, H) ∧ r2 ≠ null ∧ r2 ∈ H ∧ reachable(r, r1, H) → reachable(r, r0, H[r1, ce]) | A User Theorem |
| add-preserves-reachable-rev | ⊦ H[r1].nxt = H[r2].nxt ∧ r0 ≠ r2 ∧ ce.nxt = r2 ∧ ¬ reachable(r, r0, H) ∧ ¬ reachable(r, r2, H) ∧ r2 ≠ null ∧ r2 ∈ H ∧ reachable(r, r1, H) → (reachable(r, r0, H[r1, ce]) ↔ false) | A User Theorem |
| changenonnxt-reachable | ⊦ reachable(r, r0, H) ∧ ce.nxt = H[r1].nxt → (¬ reachable(r, r0, H[r1, ce]) ↔ false) | A User Theorem |
| changenonnxt-reachable-rev | ⊦ reachable(r, r0, H[r1, ce]) ∧ ce.nxt = H[r1].nxt ∧ r1 ∈ H → (¬ reachable(r, r0, H) ↔ false) | A User Theorem |
| endnotinH-notreachable | ⊦ ¬ r0 ∈ H → (reachable(r, r0, H) ↔ false) | A User Theorem |
| frommodified | ⊦ r ≠ null ∧ ce.nxt ≠ r → (reachable(r, r0, H[r, ce]) ↔ r = r0 ∨ ce.nxt ≠ null ∧ ce.nxt ∈ H ∧ reachable(ce.nxt, r0, H[r, ce])) | A User Theorem |
| fromnext-reachable | ⊦ reachable(r, r0, H) ∧ r ≠ r0 → (¬ reachable(H[r].nxt, r0, H) ↔ false) | A User Theorem |
| fromnext-reachable-rev | ⊦ reachable(H[r].nxt, r0, H) ∧ r ≠ r0 ∧ r ≠ null ∧ r ∈ H → (¬ reachable(r, r0, H) ↔ false) | A User Theorem |
| id-reachable | ⊦ H[r].nxt = null → (reachable(r, r0, H) ↔ ¬ ¬(r ∈ H ∧ r ≠ null ∧ r = r0)) | A User Theorem |
| k-path | ⊦ path(x, H) ↔ # x = 1 ∧ hd x ∈ H ∧ hd x ≠ null ∨ # x = 1 + 1 ∧ hd x ∈ H ∧ hd tl x ∈ H ∧ hd x ≠ null ∧ hd tl x ≠ null ∧ H[hd x].nxt = hd tl x ∨ # x ≥ 1 + 1 ∧ hd x ∈ H ∧ hd x ≠ null ∧ H[hd x].nxt = hd tl x ∧ path(tl x, H) | A User Theorem |
| k-reachable-def | ⊦ reachable(r, r0, H) ↔ r ≠ null ∧ r ∈ H ∧ reachable*(H, r, r0) | A User Theorem |
| linearity | reachable(r, r0, H), reachable(r, r1, H) ⊦ reachable(r0, r1, H) ∨ reachable(r1, r0, H) | A User Theorem |
| linearity-path | path(r ' + x, H), path(r ' + y, H) ⊦ x = y ∨ (∃ r0, y0. x = y + r0 ' + y0) ∨ (∃ r0, x0. y = x + r0 ' + x0) | A User Theorem |
| modified-stays-reachable | ⊦ reachable(r, r0, H) → (¬ reachable(r, r0, H[r0, ce]) ↔ false) | A User Theorem |
| modified-stays-reachable-rev | ⊦ r0 ∈ H ∧ reachable(r, r0, H[r0, ce]) → (¬ reachable(r, r0, H) ↔ false) | A User Theorem |
| modnotreachable-reachable | ⊦ reachable(r, r0, H) ∧ ¬ reachable(r, r1, H) → (¬ reachable(r, r0, H[r1, ce]) ↔ false) | A User Theorem |
| modnotreachable-reachable-rev | ⊦ ¬ reachable(r, r0, H) ∧ ¬ reachable(r, r1, H) ∧ r0 ∈ H → (reachable(r, r1, H[r0, ce]) ↔ false) | A User Theorem |
| modnotreachable-reachable-rev-weak | ⊦ ¬ reachable(r, r0, H) ∧ ¬ reachable(r, r1, H) ∧ r0 ≠ null ∧ r0 ∈ H → (reachable(r, r1, H[r0, ce]) ↔ false) | A User Theorem |
| modnotreachable-reachable-weak | ⊦ ¬ reachable(r, r0, H) ∧ reachable(r, r1, H) ∧ r0 ≠ null ∧ r0 ∈ H → (¬ reachable(r, r1, H[r0, ce]) ↔ false) | A User Theorem |
| notnull-reachable | ⊦ ¬ reachable(null, r1, H) | A User Theorem |
| null-not-reachable | ⊦ ¬ reachable(r, null, H) | A User Theorem |
| null-not-start-of-path | ⊦ ¬ path(null ' + x, H) | A User Theorem |
| path-butlast | ⊦ path(r ' + x + r0 ', H) → (¬ path(r ' + x, H) ↔ false) | A User Theorem |
| path-delnonmember | ⊦ path(x, H) ∧ ¬ r ∈ x → path(x, H -- r) | A User Theorem |
| path-first-in-H | ⊦ path(r ' + x, H) → (¬ r ∈ H ↔ false) | A User Theorem |
| path-last | ⊦ path(r ' + x, H) → (¬ (r ' + x).last ∈ H ↔ false) | A User Theorem |
| path-last-not-null | ⊦ ¬ path(r ' + x + null ', H) | A User Theorem |
| path-last-nxt | ⊦ path(r ' + x + r0 ', H) → (H[(r ' + x).last].nxt ≠ r0 ↔ false) | A User Theorem |
| path-modify | ⊦ ¬ r0 ∈ x → (path(x, H[r0, ce]) ↔ path(x, H)) | A User Theorem |
| path-modify-strong | ⊦ ¬ r0 ∈ x ∧ r0 ∈ H → (path(x + r1 ', H[r0, ce]) ↔ path(x + r1 ', H)) | A User Theorem |
| path-new-irrelevant-strong | ⊦ ¬ r2 ∈ H ∧ ¬ r2 ∈ x ∧ r ∈ H → (path(r ' + x, H[r2, ce]) ↔ path(r ' + x, H)) | A User Theorem |
| path-postfix | ⊦ path(x + r ' + y, H) → (¬ path(r ' + y, H) ↔ false) | A User Theorem |
| path-prefix | ⊦ path(r ' + x + y, H) → (¬ path(r ' + x, H) ↔ false) | A User Theorem |
| path-prelast | ⊦ path(r ' + x + r0 ', H) → (¬ (r ' + x).last ∈ H ↔ false) | A User Theorem |
| path-split-last | ⊦ path(r ' + x + r0 ', H) ↔ path(r ' + x, H) ∧ H[(r ' + x).last].nxt = r0 ∧ r0 ∈ H ∧ r0 ≠ null | A User Theorem |
| path-trans | path(x, H) ∧ x.last = r ∧ path(r ' + y, H) ⊦ path(x + y, H) | A User Theorem |
| reach-alloc | ⊦ reachable(r, r1, H) → r1 ∈ H | A User Theorem |
| reach-n-path-n | ⊦ n ≠ 0 → (reachable-n(H, n, r, r0) ↔ (∃ x. path(x, H) ∧ hd x = r ∧ x.last = r0 ∧ # x = n + 1)) | A User Theorem |
| reach-n-split | reachable-n(H, n, r, r0), m < n ⊦ ∃ r1. reachable-n(H, m, r, r1) ∧ reachable-n(H, n - m, r1, r0) | A User Theorem |
| reach-n-split-le | reachable-n(H, n, r, r0), m ≤ n ⊦ ∃ r1. reachable-n(H, m, r, r1) ∧ reachable-n(H, n - m, r1, r0) | A User Theorem |
| reach-n-unique | ⊦ reachable-n(H, n, r, r0) ∧ reachable-n(H, n, r, r1) → r0 = r1 | A User Theorem |
| reach-reachnext | ⊦ reachable(r, r1, H) → (¬ reachable(r, H[r1].nxt, H) ↔ H[r1].nxt = null ∨ ¬ H[r1].nxt ∈ H) | A User Theorem |
| reachable-addnew | ⊦ reachable(r, r1, H) ∧ ¬ r2 ∈ H → (¬ reachable(r, r1, H[r2, ce]) ↔ false) | A User Theorem |
| reachable-addnew-rev | ⊦ ¬ r2 ∈ H ∧ r ∈ H ∧ ¬ reachable(r, r1, H) → (reachable(r, r1, H[r2, ce]) ↔ (∃ r0. reachable(r, r0, H) ∧ H[r0].nxt = r2 ∧ r2 ≠ null ∧ (r1 = r2 ∨ reachable(ce.nxt, r1, H)))) | A User Theorem |
| reachable-addnewtonull-rev | ⊦ reachable(r, r1, H[r2, ce]) ∧ ce.nxt = null ∧ r1 ∈ H ∧ ¬ r2 ∈ H → (¬ reachable(r, r1, H) ↔ false) | A User Theorem |
| reachable-modbehind | ⊦ reachable(r, r0, H) ∧ reachable(r0, r1, H) ∧ ¬ reachable(r1, r0, H) → (¬ reachable(r, r0, H[r1, ce]) ↔ false) | A User Theorem |
| reachable-n-1 | ⊦ reachable-n(H, 1, r, r0) ↔ reachable-1(H, r, r0) | A User Theorem |
| reachable-n-rec-rev | ⊦ reachable-n(H, n + 1, r, r0) ↔ (∃ r1. reachable-n(H, n, r, r1) ∧ reachable-1(H, r1, r0)) | A User Theorem |
| reachable-n-rec-rev2 | ⊦ reachable-n(H, n + 2, r, r0) ↔ (∃ r1. reachable-n(H, n, r, r1) ∧ reachable-1(H, r1, H[r1].nxt) ∧ reachable-1(H, H[r1].nxt, r0)) | A User Theorem |
| reachable-n-rec-strong | ⊦ reachable-n(H, n + 1, r, r0) ↔ reachable-1(H, r, H[r].nxt) ∧ reachable-n(H, n, H[r].nxt, r0) | A User Theorem |
| reachable-n-rec-strong2 | ⊦ reachable-n(H, n + 2, r, r0) ↔ reachable-1(H, r, H[r].nxt) ∧ reachable-n(H, n + 1, H[r].nxt, r0) | A User Theorem |
| reachable-n-rec2 | ⊦ reachable-n(H, 2, r, r0) ↔ reachable-1(H, r, H[r].nxt) ∧ reachable-1(H, H[r].nxt, r0) | A User Theorem |
| reachable-n-trans | ⊦ reachable-n(H, n, r, r0) ∧ reachable-n(H, n0, r0, r1) → (¬ reachable-n(H, n + n0, r, r1) ↔ false) | A User Theorem |
| reachable-nodups-def | ⊦ reachable(r, r0, H) ↔ (∃ x. path(r ' + x, H) ∧ (r ' + x).last = r0 ∧ ¬ dups(r ' + x)) | A User Theorem |
| reachable-notnullinH | ⊦ reachable(r, r1, H) → (¬ r1 ∈ H ↔ false) | A User Theorem |
| reachable-split-first | ⊦ r ≠ r0 → (reachable(r, r0, H) ↔ r ≠ null ∧ r ∈ H ∧ (∃ r1. H[r].nxt = r1 ∧ r1 ∈ H ∧ r1 ≠ null ∧ reachable(r1, r0, H))) | A User Theorem |
| reachable-split-last | ⊦ r ≠ r0 → (reachable(r, r0, H) ↔ (∃ r1. reachable(r, r1, H) ∧ H[r1].nxt = r0 ∧ r0 ∈ H ∧ r0 ≠ null)) | A User Theorem |
| reachable-trans | ⊦ reachable(r, r0, H) ∧ reachable(r0, r1, H) → reachable(r, r1, H) | A User Theorem |
| reachable-trans-simp | ⊦ reachable(r, r0, H) ∧ reachable(r0, r1, H) → (¬ reachable(r, r1, H) ↔ false) | A User Theorem |
| reachnext | ⊦ reachable(r0, H[r0].nxt, H) ↔ ¬ ¬(r0 ≠ null ∧ r0 ∈ H ∧ H[r0].nxt ∈ H ∧ H[r0].nxt ≠ null) | A User Theorem |
| rem-reachable | ⊦ reachable(r, r0, H) ∧ ce.nxt = H[H[r1].nxt].nxt ∧ r0 ≠ H[r1].nxt ∧ H[r1].nxt ∈ H ∧ H[r1].nxt ≠ null ∧ r1 ≠ null ∧ r1 ∈ H → (¬ reachable(r, r0, H[r1, ce]) ↔ false) | A User Theorem |
| rem-reachable-rev | ⊦ ce.nxt = H[H[r1].nxt].nxt ∧ r0 ≠ H[r1].nxt ∧ H[r1].nxt ∈ H ∧ H[r1].nxt ≠ null ∧ r1 ≠ null ∧ r1 ∈ H → (reachable(r, r0, H[r1, ce]) ↔ reachable(r, r0, H)) | A User Theorem |
| rem-reachable-rev-weak | ⊦ reachable(r, r0, H[r1, ce]) ∧ ce.nxt = H[H[r1].nxt].nxt ∧ r0 ≠ H[r1].nxt ∧ H[r1].nxt ∈ H ∧ H[r1].nxt ≠ null ∧ r1 ≠ null ∧ r1 ∈ H → (¬ reachable(r, r0, H) ↔ false) | A User Theorem |
| rem-stays-reachable-aux | reachable(r, r0, H), H[r0].nxt ≠ null, H[r0].nxt ∈ H, H[r0].nxt ≠ H[H[r0].nxt].nxt, ce.nxt = H[H[r0].nxt].nxt ⊦ reachable(r, H[r0].nxt, H[r0, ce]) ↔ H[H[r0].nxt].nxt = H[r0].nxt ∨ r ≠ r0 ∧ r = H[r0].nxt ∨ (∃ x. path(r ' + x + H[r0].nxt ', H) ∧ r0 ≠ r ∧ ¬ r0 ∈ x) ∨ (∃ x. path(H[r0].nxt ' + x + H[r0].nxt ', H) ∧ ¬ r0 ∈ x) | A User Theorem |
| rem-stays-reachable-aux1 | r0 ∈ H, H[r0].nxt ≠ null, H[r0].nxt ∈ H, H[r0].nxt ≠ H[H[r0].nxt].nxt ⊦ reachable(H[H[r0].nxt].nxt, H[r0].nxt, H) ∧ ¬ reachable(H[H[r0].nxt].nxt, r0, H) ↔ (∃ x. path(H[r0].nxt ' + x + H[r0].nxt ', H) ∧ ¬ r0 ∈ x) | A User Theorem |
| rem-stays-reachable-aux2 | reachable(r, r0, H), H[r0].nxt ≠ null, H[r0].nxt ∈ H ⊦ (∃ r1. reachable(r, r1, H) ∧ H[r0].nxt = H[r1].nxt ∧ ¬ reachable(r0, r1, H)) ↔ (∃ x. path(r ' + x + H[r0].nxt ', H) ∧ r0 ≠ r ∧ ¬ r0 ∈ x) | A User Theorem |
| removed-stays-reachable | ⊦ reachable(r, r0, H) ∧ H[r0].nxt ≠ null ∧ H[r0].nxt ∈ H ∧ ce.nxt = H[H[r0].nxt].nxt → ( reachable(r, H[r0].nxt, H[r0, ce]) ↔ H[H[r0].nxt].nxt = H[r0].nxt ∨ r ≠ r0 ∧ r = H[r0].nxt ∨ reachable(H[H[r0].nxt].nxt, H[r0].nxt, H) ∧ ¬ reachable(H[H[r0].nxt].nxt, r0, H) ∨ (∃ r1. reachable(r, r1, H) ∧ H[r1].nxt = H[r0].nxt ∧ ¬ reachable(r0, r1, H))) | A User Theorem |
| self-reachable | ⊦ reachable(r, r, H) ↔ ¬ ¬(r ≠ null ∧ r ∈ H) | A User Theorem |
| startnotinH-notreachable | ⊦ ¬ r ∈ H → (reachable(r, r0, H) ↔ false) | A User Theorem |