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: |
|---|---|---|
| in-abs | ⊦ a ∈ abs(T1, T2, h1, h2) ↔ ¬ ¬(T1[h1(a)] = full(a) ∨ T2[h2(a)] = full(a)) | An Axiom |
| inv | ⊦ inv(T, h) ↔ # T = SIZE ∧ (∀ a. h(a) < SIZE) ∧ (∀ n, a. n < # T ∧ T[n] = full(a) → h(a) = n) | An Axiom |
| disj | ⊦ disj(T1, T2) ↔ (∀ n, m. n < # T1 ∧ m < # T2 ∧ T1[n] ≠ empty ∧ T2[m] ≠ empty → T1[n].elem ≠ T2[m].elem) | An Axiom |
| abs-sym | ⊦ abs(T1, T2, h1, h2) = abs(T2, T1, h2, h1) | A User Theorem |
| at-put | ⊦ inv(T, h) → T[h(a), slot][h(b)] = (h(a) = h(b) ⊃ slot;T[h(b)]) | A User Theorem |
| disj-neq | ⊦ disj(T1, T2) ∧ n < # T1 ∧ m < # T2 ∧ T1[n] = full(a) → T2[m] ≠ full(a) | A User Theorem |
| disj-reduce | ⊦ disj(T1, T2) → ( ¬ disj(T3, T4) ↔ ¬ (∀ n, m. (n < # T1 ∧ m < # T2 ∧ T1[n] ≠ empty ∧ T2[m] ≠ empty → T1[n].elem ≠ T2[m].elem) → n < # T3 ∧ m < # T4 ∧ T3[n] ≠ empty ∧ T4[m] ≠ empty → T3[n].elem ≠ T4[m].elem)) | A User Theorem |
| hash-given | ⊦ inv(T, h) ∧ T[h(b)] = full(a) → h(a) = h(b) | A User Theorem |
| hash-same | ⊦ inv(T, h) ∧ n < SIZE ∧ T[n] = full(a) → h(a) = n | A User Theorem |
| insert-correct | s = abs(T1, T2, h1, h2), inv(T1, h1), inv(T2, h2), disj(T1, T2) ⊦ [insert(a, h1, h2; T1, T2)] (s ++ a = abs(T1, T2, h1, h2) ∧ inv(T1, h1) ∧ inv(T2, h2) ∧ disj(T1, T2)) | A User Theorem |
| insert-rec-correct | ¬ a ∈ s, s = abs(T1, T2, h1, h2), inv(T1, h1), inv(T2, h2), disj(T1, T2) ⊦ [insert_rec(a, h1, h2; T1, T2)] (s ++ a = abs(T1, T2, h1, h2) ∧ inv(T1, h1) ∧ inv(T2, h2) ∧ disj(T1, T2)) | A User Theorem |
| inv-reduce | ⊦ inv(T1, h) → (¬ inv(T2, h) ↔ ¬((# T1 = SIZE → # T2 = SIZE) ∧ (∀ n, a. (n < # T1 ∧ T1[n] = full(a) → h(a) = n) → n < # T2 ∧ T2[n] = full(a) → h(a) = n))) | A User Theorem |
| less | ⊦ inv(T, h) → (¬ h(a) < SIZE ↔ false) | A User Theorem |
| lookup-correct | s = abs(T1, T2, h1, h2) ⊦ ⟨lookup(a, T1, T2, h1, h2; found?)⟩ (found? ↔ a ∈ s) | A User Theorem |
| size | ⊦ inv(T, h) → # T = SIZE | A User Theorem |