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: |
|---|---|---|
| empty-node | ⊦ Node(a) = Node(a, ∅) | An Axiom |
| inj | ⊦ inj(map) ↔ (∀ r0, r1. r0 ∈ map ∧ r1 ∈ map → (map[r0] = map[r1] ↔ r0 = r1)) | An Axiom |
| closed | ⊦ closed(H) ↔ (∀ r. r ∈ H → closed(H[r].edges, H)) | An Axiom |
| dom | ⊦ r ∈ dom H ↔ r ∈ H | An Axiom |
| closeds | ⊦ closed(succ, H) ↔ (∀ a. a ∈ succ → succ[a] ∈ H) | An Axiom |
| ran | ⊦ r ∈ ran map ↔ r ∈ran map | An Axiom |
| reachable | ⊦ reachable(r0, r1, H) ↔ (∃ x. path(x, r0, r1, H)) | An Axiom |
| path-rec | ⊦ path(a ' + x, r0, r1, H) ↔ r0 ∈ H ∧ a ∈ H[r0].edges ∧ path(x, (H[r0].edges)[a], r1, H) | An Axiom |
| path-emp | ⊦ path([], r0, r1, H) ↔ r0 = r1 ∧ r0 ∈ H | An Axiom |
| connected | ⊦ connected(r0, H) ↔ (∀ r1. reachable(r0, r1, H)) | An Axiom |
| reachset | ⊦ r1 ∈ reachset(r0, H) ↔ reachable(r0, r1, H) | An Axiom |
| at-apply-succ | ⊦ a ∈ succ → apply(succ, map)[a] = map[succ[a]] | An Axiom |
| in-apply-succ | ⊦ a ∈ apply(succ, map) ↔ a ∈ succ | An Axiom |
| at-apply | ⊦ r0 ∈ map ∧ r0 ∈ H ∧ map[r0] = r1 → apply(H, map)[r1] = Node(H[r0].value, apply(H[r0].edges, map)) | An Axiom |
| in-apply | ⊦ ¬ ¬ r1 ∈ apply(H, map) ↔ (∃ r0. r0 ∈ map ∧ r0 ∈ H ∧ map[r0] = r1) | An Axiom |
| hom | ⊦ hom(H0, map, H1) ↔ apply(H0, map) = H1 | An Axiom |
| H-dom-subset | ⊦ dom H ⊆ dom map ∧ r ∈ H → (¬ r ∈ map ↔ false) | A User Theorem |
| apply-empty | ⊦ apply(H, ∅) = ∅ | A User Theorem |
| apply-succ-empty | ⊦ apply(∅, map) = ∅ | A User Theorem |
| closed-empty | ⊦ closed(∅) | A User Theorem |
| closed-succ | ⊦ r ∈ H ∧ H[r] = Node(a, succ) ∧ b ∈ succ ∧ closed(H) → (¬ succ[b] ∈ H ↔ false) | A User Theorem |
| closed-succ-in | ⊦ a ∈ succ ∧ closed(succ, H) → (¬ succ[a] ∈ H ↔ false) | A User Theorem |
| closed-succ-in-subheap | ⊦ a ∈ succ ∧ closed(succ, H0) ∧ H0 ⊆ H1 → (¬ succ[a] ∈ H1 ↔ false) | A User Theorem |
| closed-succ-rm | ⊦ closed(succ, H) → (¬ closed(succ -- a, H) ↔ false) | A User Theorem |
| closeds-empty | ⊦ closed(∅, H) | A User Theorem |
| closeds-subset | ⊦ closed(succ, H0) ∧ dom H0 ⊆ dom H1 → (¬ closed(succ, H1) ↔ false) | A User Theorem |
| dom-alloc | ⊦ ¬ r ∈ H ∧ r ≠ null → dom(H ++ r) = dom H ++ r | A User Theorem |
| dom-empty | ⊦ dom ∅ = ∅ | A User Theorem |
| dom-write | ⊦ r ∈ H → dom H[r, nd] = dom H | A User Theorem |
| hom-empty | ⊦ hom(H, ∅, ∅) | A User Theorem |
| inj-empty | ⊦ inj(∅) | A User Theorem |
| inj-eq | ⊦ inj(map) ∧ r0 ∈ map ∧ r1 ∈ map → (map[r0] = map[r1] ↔ r0 = r1) | A User Theorem |
| map-path | ⊦ reachset(r0, H) ⊆ dom map ∧ inj(map) ∧ closed(H) → (path(x, r0, r1, H) ↔ path(x, map[r0], map[r1], apply(H, map)) ∧ r0 ∈ map ∧ r1 ∈ map) | A User Theorem |
| path-first-in | ⊦ path(x, r0, r1, H) → r0 ∈ H | A User Theorem |
| path-last-in | ⊦ path(x, r0, r1, H) → r1 ∈ H | A User Theorem |
| ran-empty | ⊦ ran ∅ = ∅ | A User Theorem |
| ran-in-heap-eq | ⊦ r ∈ map ∧ ran map = dom H → (¬ map[r] ∈ H ↔ false) | A User Theorem |
| ran-put-new | ⊦ ¬ r0 ∈ map → ran map[r0, r1] = ran map ++ r1 | A User Theorem |
| reachable-closed | ⊦ reachable(r0, r1, H0 ∪ H1) ∧ H0 ⊥ H1 ∧ closed(H1) ∧ r0 ∈ H1 → r1 ∈ H1 | A User Theorem |
| reachable-eq | ⊦ reachable(r, r, H) ↔ r ∈ H | A User Theorem |
| reachable-one | ⊦ r ∈ H ∧ H[r] = Node(b, succ) ∧ a ∈ succ → (reachable(r, succ[a], H) ↔ succ[a] ∈ H) | A User Theorem |
| reachset-succ | ⊦ r ∈ H ∧ H[r] = Node(b, succ) ∧ a ∈ succ → (¬ reachset(succ[a], H) ⊆ reachset(r, H) ↔ false) | A User Theorem |