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: |
|---|---|---|
| datasize-rec | ⊦ datasize(buf, n + 1) = (buf[n] = empty ⊃ datasize(buf, n);n + 1) | An Axiom |
| datasize-base | ⊦ datasize(buf, 0) = 0 | An Axiom |
| datasize | ⊦ datasize(buf) = datasize(buf, # buf) | An Axiom |
| datasize-add-empty-h | ⊦ subarray(buf, n0, n1) = mkempbuf(n1) ∧ n0 + n1 ≤ # buf → datasize(buf, n0 + n1) = datasize(buf, n0) | A User Theorem |
| datasize-append | ⊦ datasize(buf0 + buf1) = (datasize(buf1) = 0 ⊃ datasize(buf0);# buf0 + datasize(buf1)) | A User Theorem |
| datasize-append-empty-h | ⊦ m ≤ # buf0 + # buf1 ∧ (m ≥ # buf0 → datasize(buf1, m - # buf0) = 0) → datasize(buf0 + buf1, m) = datasize(buf0, min(m, # buf0)) | A User Theorem |
| datasize-append-h-new | ⊦ m ≤ # buf0 + # buf1 → datasize(buf0 + buf1, m) = (m ≤ # buf0 ∨ datasize(buf1, m - # buf0) = 0 ⊃ datasize(buf0, min(m, # buf0));# buf0 + datasize(buf1, m - # buf0)) | A User Theorem |
| datasize-append-lower-h | m ≤ # buf0 ⊦ datasize(buf0 + buf1, m) = datasize(buf0, m) | A User Theorem |
| datasize-at | ⊦ datasize(buf) ≤ n ∧ n < # buf → buf[n] = empty | A User Theorem |
| datasize-at-h | ⊦ datasize(buf, m) ≤ n ∧ n < m ∧ m ≤ # buf → buf[n] = empty | A User Theorem |
| datasize-datasize-elim-h | n ≤ # buf ⊦ datasize(buf, datasize(buf, n)) = datasize(buf, n) | A User Theorem |
| datasize-empbuf | ⊦ datasize(buf + mkempbuf(n)) = datasize(buf) | A User Theorem |
| datasize-empbuf-h | ⊦ m ≤ # buf + n → datasize(buf + mkempbuf(n), m) = datasize(buf, min(# buf, m)) | A User Theorem |
| datasize-further | ⊦ n0 ≤ # buf ∧ n0 ≤ n1 → (datasize(buf, n0) = datasize(buf, n1) ↔ (∀ n. n0 ≤ n ∧ n < n1 → buf[n] = empty)) | A User Theorem |
| datasize-is-smaller | ⊦ n < datasize(buf) → n < # buf | A User Theorem |
| datasize-is-smaller-help | ⊦ ¬ n < datasize(buf, n) | A User Theorem |
| datasize-le | ⊦ m ≠ 0 → (m ≤ datasize(buf) ↔ (∃ n. n + 1 ≥ m ∧ n < # buf ∧ buf[n] ≠ empty)) | A User Theorem |
| datasize-le-fwd | ⊦ m ≤ datasize(buf) → m ≤ # buf | A User Theorem |
| datasize-le-h | ⊦ m0 ≤ # buf ∧ m ≠ 0 → (m ≤ datasize(buf, m0) ↔ (∃ n. n + 1 ≥ m ∧ n < m0 ∧ buf[n] ≠ empty)) | A User Theorem |
| datasize-ls | ⊦ m ≠ 0 → (datasize(buf) < m ↔ ¬(∃ n. n + 1 ≥ m ∧ n < # buf ∧ buf[n] ≠ empty)) | A User Theorem |
| datasize-ls-add | n ≠ 0, m ≤ # buf ⊦ ¬ m + n < datasize(buf, m) | A User Theorem |
| datasize-ls-datasize-h | ⊦ datasize(buf, # buf) < datasize(buf) ↔ false | A User Theorem |
| datasize-ls-h | ⊦ m0 ≤ # buf ∧ m ≠ 0 → (datasize(buf, m0) < m ↔ ¬(∃ n. n + 1 ≥ m ∧ n < m0 ∧ buf[n] ≠ empty)) | A User Theorem |
| datasize-ls-samedata | ⊦ # buf0 = # buf1 ∧ range=(buf0, 0, buf1, 0, datasize(buf1)) → (datasize(buf0) < datasize(buf1) ↔ false) | A User Theorem |
| datasize-ls-samedata-h | ⊦ # buf0 = # buf1 ∧ m ≤ # buf0 ∧ range=(buf0, 0, buf1, 0, datasize(buf1)) → (datasize(buf0, m) < datasize(buf1, m) ↔ false) | A User Theorem |
| datasize-mkempbuffer | ⊦ datasize(mkempbuf(n)) = 0 | A User Theorem |
| datasize-mkempbuffer-h | ⊦ m ≤ n → datasize(mkempbuf(n), m) = 0 | A User Theorem |
| datasize-samebuf-h | ⊦ m < n ∧ n ≤ # buf ∧ m ≤ # buf → (datasize(buf, n) < datasize(buf, m) ↔ false) | A User Theorem |
| datasize-split-empty | ⊦ m ≤ # buf ∧ m = # buf0 ∧ buf = buf0 + buf1 ∧ buf1 = mkempbuf(# buf1) → datasize(buf) = datasize(buf0) | A User Theorem |
| datasize-split-empty-h | ⊦ m ≤ # buf ∧ m = # buf0 ∧ m0 ≤ # buf1 ∧ buf = buf0 + buf1 ∧ buf1 = mkempbuf(# buf1) → datasize(buf, # buf0 + m0) = datasize(buf0, # buf0) | A User Theorem |
| datasize-subarray | ⊦ m0 + m1 = # buf → datasize(subarray(buf, m0, m1)) = (datasize(buf) ≤ m0 ⊃ 0;datasize(buf) - m0) | A User Theorem |
| datasize-subarray-h | ⊦ m0 + m1 = # buf ∧ m ≤ m1 → datasize(subarray(buf, m0, m1), m) = (datasize(buf, m0 + m) ≤ m0 ⊃ 0;datasize(buf, m0 + m) - m0) | A User Theorem |
| datasize-subarray0 | m ≤ # buf ⊦ datasize(subarray(buf, 0, m)) = datasize(buf, m) | A User Theorem |
| datasize-subarray0-h | ⊦ m ≤ # buf ∧ m0 ≤ m → datasize(subarray(buf, 0, m), m0) = datasize(buf, m0) | A User Theorem |
| datasize-zero | ⊦ datasize(buf) = 0 ↔ (∀ n. n < # buf → buf[n] = empty) | A User Theorem |
| datasize-zero-h | ⊦ datasize(buf, m) = 0 ↔ (∀ n. n < m → buf[n] = empty) | A User Theorem |
| datsize-write-higher | ⊦ m + n ≤ # buf ∧ n ≤ # buf0 ∧ ¬ m < datasize(buf) → (datasize(copy(buf0, 0, buf, m, n)) < datasize(buf) ↔ false) | A User Theorem |
| datsize-write-higher-h | ⊦ m + n ≤ # buf ∧ n ≤ # buf0 ∧ ¬ m < datasize(buf) ∧ m0 ≤ # buf → (datasize(copy(buf0, 0, buf, m, n), m0) < datasize(buf, m0) ↔ false) | A User Theorem |