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: |
|---|---|---|
| peb-size | ⊦ PAGES_PER_PEB = PAGES_PER_LEB + 2 | An Axiom |
| leb-size | ⊦ PAGES_PER_LEB ≠ 0 | An Axiom |
| page-size | ⊦ EB_PAGE_SIZE ≠ 0 | An Axiom |
| emptypeb-at | n < # emptypeb ⊦ (emptypeb)[n] = empty | An Axiom |
| emptypeb-size | ⊦ # emptypeb = PAGES_PER_PEB * EB_PAGE_SIZE | An Axiom |
| emptyleb-at | n < # emptyleb ⊦ (emptyleb)[n] = empty | An Axiom |
| emptyleb-size | ⊦ # emptyleb = PAGES_PER_LEB * EB_PAGE_SIZE | An Axiom |
| emptypage-at | n < # emptypage ⊦ (emptypage)[n] = empty | An Axiom |
| emptypage-size | ⊦ # emptypage = EB_PAGE_SIZE | An Axiom |
| pebsize | ⊦ PEB_SIZE = PAGES_PER_PEB * EB_PAGE_SIZE | An Axiom |
| lebsize | ⊦ LEB_SIZE = PAGES_PER_LEB * EB_PAGE_SIZE | An Axiom |
| isempty | ⊦ isempty(buf) ↔ buf = mkempbuf(# buf) | An Axiom |
| leb-size-rewrite | ⊦ PAGES_PER_LEB * EB_PAGE_SIZE = LEB_SIZE | A User Theorem |
| lebsize-2page-size-le | ⊦ LEB_SIZE < m ∧ m + 2 * EB_PAGE_SIZE ≤ n → PEB_SIZE < n | A User Theorem |
| lebsize-add-eq-0 | ⊦ LEB_SIZE + n ≠ 0 | A User Theorem |
| lebsize-eq-2page-size-pebsize | ⊦ m = LEB_SIZE → (PEB_SIZE < m + 2 * EB_PAGE_SIZE ↔ false) | A User Theorem |
| lebsize-ls-2page-size-pebsize | ⊦ m < LEB_SIZE → (PEB_SIZE < m + 2 * EB_PAGE_SIZE ↔ false) | A User Theorem |
| lebsize-neq-zero | ⊦ LEB_SIZE ≠ 0 | A User Theorem |
| lebsize-page-size-is-aligned | ⊦ ¬ is-aligned(LEB_SIZE, EB_PAGE_SIZE) ↔ false | A User Theorem |
| lebsize-pebsize | ⊦ LEB_SIZE + 2 * EB_PAGE_SIZE = PEB_SIZE | A User Theorem |
| lebsize-simp-ls | ⊦ LEB_SIZE < PAGES_PER_LEB * EB_PAGE_SIZE ↔ false | A User Theorem |
| peb-size-ge2 | ⊦ ¬ PAGES_PER_PEB < 2 | A User Theorem |
| peb-size-not0 | ⊦ PAGES_PER_PEB ≠ 0 | A User Theorem |
| peb-size-rewrite | ⊦ PAGES_PER_PEB * EB_PAGE_SIZE = PEB_SIZE | A User Theorem |
| peb-vs-leb-size | ⊦ ¬ PAGES_PER_PEB < PAGES_PER_LEB | A User Theorem |
| peb-vs-leb-size-ext | ⊦ PAGES_PER_PEB < n + PAGES_PER_LEB → n > 2 | A User Theorem |
| pebsize-le-2page-size | ⊦ PEB_SIZE < 2 * EB_PAGE_SIZE ↔ false | A User Theorem |
| pebsize-le-2page-size-lebsize | ⊦ m ≤ LEB_SIZE → (PEB_SIZE < m + 2 * EB_PAGE_SIZE ↔ false) | A User Theorem |
| pebsize-le-2page-size-n | ⊦ PEB_SIZE < 2 * EB_PAGE_SIZE + n ↔ LEB_SIZE < n | A User Theorem |
| pebsize-le-minus-eb-page-size | ⊦ PEB_SIZE ≤ EB_PAGE_SIZE + n → (n < LEB_SIZE + EB_PAGE_SIZE ↔ false) | A User Theorem |
| pebsize-le-page-size | ⊦ PEB_SIZE < EB_PAGE_SIZE ↔ false | A User Theorem |
| pebsize-ls-2page-size-n | ⊦ PEB_SIZE ≤ 2 * EB_PAGE_SIZE + n ↔ LEB_SIZE ≤ n | A User Theorem |
| pebsize-ls-lebsize | ⊦ PEB_SIZE < LEB_SIZE ↔ false | A User Theorem |
| pebsize-minus-2eb-page-size | ⊦ PEB_SIZE = n + 2 * EB_PAGE_SIZE → n = LEB_SIZE | A User Theorem |
| pebsize-minus-eb-page-size | ⊦ PEB_SIZE = n + EB_PAGE_SIZE → n = LEB_SIZE + EB_PAGE_SIZE | A User Theorem |
| pebsize-page-size-is-aligned | ⊦ ¬ is-aligned(PEB_SIZE, EB_PAGE_SIZE) ↔ false | A User Theorem |
| pebsize-simp-ls | ⊦ PEB_SIZE < PAGES_PER_PEB * EB_PAGE_SIZE ↔ false | A User Theorem |
| pebsize-simp-ls-rev | ⊦ PAGES_PER_PEB * EB_PAGE_SIZE < PEB_SIZE ↔ false | A User Theorem |
| pebsize-simp-neq | ⊦ PEB_SIZE ≠ PAGES_PER_PEB * EB_PAGE_SIZE ↔ false | A User Theorem |
| subarray-emptypeb-eq-emptyleb | ⊦ subarray(emptypeb, 2 * EB_PAGE_SIZE, LEB_SIZE) = emptyleb | A User Theorem |
| subarray-emptypeb-eq-emptypage | ⊦ subarray(emptypeb, 0, EB_PAGE_SIZE) = emptypage | A User Theorem |
| subarray-emptypeb-eq-emptypage1 | ⊦ subarray(emptypeb, EB_PAGE_SIZE, EB_PAGE_SIZE) = emptypage | A User Theorem |