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: |
|---|---|---|
| abs | ⊦ abs(buf, x) ↔ buf .len = n→i(# x) ∧ x = tolist(buf, i→n(buf .len)) | An Axiom |
| tolist-base | ⊦ tolist(buf, 0) = [] | An Axiom |
| tolist-rec | ⊦ (i→n(buf .first) + n) % i→n(buf .size) < # buf .data → tolist(buf, n + 1) = push(tolist(buf, n), (buf .data)[(i→n(buf .first) + n) % i→n(buf .size)]) | An Axiom |
| at-first-mod | ⊦ inv(buf) → i→n(buf .first) % i→n(buf .size) = i→n(buf .first) | A User Theorem |
| at-n-mod | ⊦ n < i→n(buf .size) → n % i→n(buf .size) = n | A User Theorem |
| clear-corr | inv(buf) ⊦ 〈clear#(; buf)〉 (inv(buf) ∧ abs(buf, [])) | A User Theorem |
| create-corr | 0 < i ⊦ 〈create#(i; buf)〉 (inv(buf) ∧ abs(buf, []) ∧ buf .size = i) | A User Theorem |
| head-corr | inv(buf), abs(buf, a + x) ⊦ 〈head#(buf; b)〉 a = b | A User Theorem |
| int-mod-distr | ⊦ 0 < j ∧ 0 ≤ i → i→n(i % j) = i→n(i) % i→n(j) | A User Theorem |
| mod-twice | m ≠ 0 ⊦ (n0 % m + n1) % m = (n0 + n1) % m | A User Theorem |
| pop-corr | inv(buf), abs(buf, a + x) ⊦ 〈pop#(; buf, b)〉 (inv(buf) ∧ abs(buf, x) ∧ a = b) | A User Theorem |
| push-corr | inv(buf), abs(buf, x), buf .len < buf .size ⊦ 〈push#(a; buf)〉 (inv(buf) ∧ abs(buf, push(x, a))) | A User Theorem |
| test | ⊦ ⟪test#(a, b, c)⟫ true | A User Theorem |
| tolist-at | m < n ⊦ inv(buf) → (tolist(buf, n)[m]) = (buf .data)[(i→n(buf .first) + m) % i→n(buf .size)] | A User Theorem |
| tolist-ext-one | ⊦ inv(buf) ∧ m < n → (x = tolist(buf, n) ↔ x = tolist(buf, n) ∧ x[m] = (buf .data)[(i→n(buf .first) + m) % i→n(buf .size)]) | A User Theorem |
| tolist-rec-inv | ⊦ inv(buf) → tolist(buf, n + 1) = push(tolist(buf, n), (buf .data)[(i→n(buf .first) + n) % i→n(buf .size)]) | A User Theorem |
| tolist-size | ⊦ inv(buf) → # tolist(buf, n) = n | A User Theorem |