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: |
|---|---|---|
| emptypage-at | ⊦ n < VFS_PAGE_SIZE → (zeropage)[n] = zero | An Axiom |
| emptypage-size | ⊦ # zeropage = VFS_PAGE_SIZE | An Axiom |
| page-size | ⊦ VFS_PAGE_SIZE ≠ 0 | An Axiom |