This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| abs-def | ⊦ abs(avols, apebs, vols, q) ↔ (∀ v. (v ∈ vols ↔ v ∈ avols) ∧ ( v ∈ vols → # vols[v] = # avols[v] ∧ (∀ m. m < # vols[v] → (vols[v][m] = unmapped → ¬ avols[v][m].mapped?) ∧ ( vols[v][m] ≠ unmapped → avols[v][m].mapped? ∧ avols[v][m].data = apebs[vols[v][m].pnum].data ∧ apebs[vols[v][m].pnum].fill ≤ avols[v][m].fill) ∧ (avols[v][m] = erased → ¬ v × m ∈ q)))) | An Axiom |
| max-avol-at | ⊦ n < # ebatbl → max-avol(apebs, ebatbl, v, q)[n] = (ebatbl[n] ≠ unmapped ⊃ mapped(apebs[ebatbl[n].pnum].data, apebs[ebatbl[n].pnum].fill);(v × n ∈ q ⊃ unmapped;erased)) | An Axiom |
| max-avol-size | ⊦ # max-avol(apebs, ebatbl, v, q) = # ebatbl | An Axiom |
| max-avols-at | ⊦ v ∈ vols → max-avols(apebs, vols, q)[v] = max-avol(apebs, vols[v], v, q) | An Axiom |
| max-avols-in | ⊦ v ∈ max-avols(apebs, vols, q) ↔ v ∈ vols | An Axiom |
| absexpt-def | ⊦ abs○(avols, apebs, vols, q, v0, m0) ↔ (∀ v. (v ∈ vols ↔ v ∈ avols) ∧ ( v ∈ vols → # vols[v] = # avols[v] ∧ (∀ m. (v ≠ v0 ∨ m ≠ m0) ∧ m < # vols[v] → (vols[v][m] = unmapped → ¬ avols[v][m].mapped?) ∧ ( vols[v][m] ≠ unmapped → avols[v][m].mapped? ∧ avols[v][m].data = apebs[vols[v][m].pnum].data ∧ apebs[vols[v][m].pnum].fill ≤ avols[v][m].fill) ∧ (avols[v][m] = erased → ¬ v × m ∈ q)))) | An Axiom |
| absexpt-v-def | ⊦ abs○(avols, apebs, vols, q, v0) ↔ (∀ v. (v ∈ vols ↔ v ∈ avols) ∧ ( v ∈ vols → # vols[v] = # avols[v] ∧ ( v ≠ v0 → (∀ m. m < # vols[v] → (vols[v][m] = unmapped → ¬ avols[v][m].mapped?) ∧ ( vols[v][m] ≠ unmapped → avols[v][m].mapped? ∧ avols[v][m].data = apebs[vols[v][m].pnum].data ∧ apebs[vols[v][m].pnum].fill ≤ avols[v][m].fill) ∧ (avols[v][m] = erased → ¬ v × m ∈ q))))) | An Axiom |
| absf-rec | ⊦ n < # ebatbl → absf(v, evol, apebs, ebatbl, q, n + 1) = absf(v, evol, apebs, ebatbl, q, n) [n, (ebatbl[n] = unmapped ⊃ (v × n ∈ q.lebrefs ⊃ unmapped;erased) ;mapped(apebs[ebatbl[n].pnum].data, (evol[n].mapped? ⊃ evol[n].fill;apebs[ebatbl[n].pnum].fill)) ) ] | An Axiom |
| absf-base | ⊦ absf(v, evol, apebs, ebatbl, q, 0) = mkabstractvolume(# ebatbl) | An Axiom |
| absfv-at | ⊦ v ∈ vols → absf(avols, apebs, vols, q)[v] = absf(v, avols[v], apebs, vols[v], q, # vols[v]) | An Axiom |
| absfv-in | ⊦ v ∈ absf(avols, apebs, vols, q) ↔ v ∈ vols | An Axiom |
| abs-absexpt | ⊦ abs(avols, apebs, vols, q) → abs○(avols, apebs, vols, q, v, m) | A User Theorem |
| abs-absexpt-v | ⊦ abs(avols, apebs, vols, q) → abs○(avols, apebs, vols, q, v) | A User Theorem |
| abs-avols-in | ⊦ v ∈ avols ∧ abs(avols, apebs, vols, q) → v ∈ vols | A User Theorem |
| abs-avols-size | ⊦ v ∈ avols ∧ m < # avols[v] ∧ abs(avols, apebs, vols, q) → m < # vols[v] | A User Theorem |
| abs-erase | ⊦ v ∈ vols ∧ m < # vols[v] ∧ abs(avols, apebs, vols, q) ∧ vols0 = vols[v, vols[v][m, unmapped]] → abs(avols[v, avols[v][m, erased]], apebs, vols0, q - v × m) | A User Theorem |
| abs-erase-emptyq | ⊦ v ∈ vols ∧ m < # vols[v] ∧ abs(avols, apebs, vols, q) ∧ vols0 = vols[v, vols[v][m, unmapped]] → abs(avols[v, avols[v][m, erased]], apebs, vols0, []) | A User Theorem |
| abs-id-apebs-used | n < # wlar, # wlar = # apebs, stat ≠ used ⊦ wlar[n] = wl-entry(m0, stat) ∧ valid-ebatbl(apebs, wlar, vols, n0) → (abs(avols, apebs[n, apeb], vols, q) ↔ abs(avols, apebs, vols, q)) | A User Theorem |
| abs-idset-fwd | ⊦ id(apebs1, apebs0, mapped-pebs(vols)) ∧ valid-ebatbl(apebs0, wlar, vols, n0) ∧ abs(avols, apebs0, vols, q) → abs(avols, apebs1, vols, q) | A User Theorem |
| abs-lebrefs-subset | ⊦ q1.lebrefs ⊆ q0.lebrefs ∧ abs(avols, apebs, vols, q0) → abs(avols, apebs, vols, q1) | A User Theorem |
| abs-lebrefs-subset-noterased-some | ⊦ q1.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ abs(avols, apebs, vols, q0) ∧ v ∈ avols ∧ m < # avols[v] ∧ avols[v][m] ≠ erased → abs(avols, apebs, vols, q1) | A User Theorem |
| abs-queue-notin | ⊦ ¬ v ∈ vols → (abs(avols, apebs, vols, q + eq-entry(n, v × m) ') ↔ abs(avols, apebs, vols, q)) | A User Theorem |
| abs-queue-subset | ⊦ q1 ⊆ q0 ∧ abs(avols, apebs, vols, q0) → abs(avols, apebs, vols, q1) | A User Theorem |
| abs-unmap | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ abs(avols, apebs, vols, q) → abs(avols[v, avols[v][m, unmapped]], apebs, vols[v, vols[v][m, unmapped]], q + eq-entry(n, v × m) ') | A User Theorem |
| abs-unmap-twice | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = unmapped ∧ abs(avols, apebs, vols, q) → abs(avols[v, avols[v][m, unmapped]], apebs, vols, q) | A User Theorem |
| abs-vols-in | ⊦ v ∈ vols ∧ abs(avols, apebs, vols, q) → v ∈ avols | A User Theorem |
| abs-vols-mapped | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ abs(avols, apebs, vols, q) → avols[v][m].mapped? | A User Theorem |
| abs-vols-size | ⊦ v ∈ vols ∧ m < # vols[v] ∧ abs(avols, apebs, vols, q) → m < # avols[v] | A User Theorem |
| abs-vols-unmapped | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = unmapped ∧ abs(avols, apebs, vols, q) → ¬ avols[v][m].mapped? | A User Theorem |
| absexpt-avols-write | ⊦ v ∈ avols ∧ m < # avols[v] → (abs○(avols[v, avols[v][m, leb]], apebs, vols, q, v, m) ↔ abs○(avols, apebs, vols, q, v, m)) | A User Theorem |
| absexpt-id-apebs-used | n < # wlar, # wlar = # apebs, stat ≠ used ⊦ wlar[n] = wl-entry(m0, stat) ∧ valid-ebatbl(apebs, wlar, vols, n0) → (abs○(avols, apebs[n, apeb], vols, q, v, m) ↔ abs○(avols, apebs, vols, q, v, m)) | A User Theorem |
| absexpt-idset | ⊦ abs(avols, apebs0, vols, q) ∧ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ id(apebs1, apebs0, mapped-pebs(vols) -- n) ∧ valid-ebatbl(apebs0, wlar, vols, n0) → abs○(avols, apebs1, vols, q, v, m) | A User Theorem |
| absexpt-mapped-abs | ⊦ abs○(avols, apebs, vols, q, v, m) ∧ v ∈ vols ∧ m < # vols[v] ∧ avols[v][m] = mapped(buf, m0) ∧ vols[v][m] = ⌜n⌝ ∧ apebs[n].data = buf ∧ apebs[n].fill ≤ m0 → abs(avols, apebs, vols, q) | A User Theorem |
| absexpt-pebs-write | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → (abs○(avols, apebs[n, apeb], vols, q, v, m) ↔ abs○(avols, apebs, vols, q, v, m)) | A User Theorem |
| absexpt-v-vols-write | ⊦ ¬ v ∈ vols ∧ ¬ v ∈ avols ∧ # evol = # ebatbl → (abs○(avols[v, evol], apebs, vols[v, ebatbl], q, v) ↔ abs○(avols, apebs, vols, q, v)) | A User Theorem |
| absexpt-vols-abs | ⊦ ¬ v ∈ vols ∧ abs○(avols, apebs, vols, q, v) → abs(avols[v, fill(mkabstractvolume(n), erased)], apebs, vols[v, fill(mkebatbl(n), unmapped)], q - v) | A User Theorem |
| absexpt-vols-write | ⊦ v ∈ vols ∧ m < # vols[v] → (abs○(avols, apebs, vols[v, vols[v][m, ebae]], q, v, m) ↔ abs○(avols, apebs, vols, q, v, m)) | A User Theorem |
| absf-at | ⊦ n < m ∧ m ≤ # ebatbl → absf(v, evol, apebs, ebatbl, q, m)[n] = (ebatbl[n] = unmapped ⊃ (v × n ∈ q.lebrefs ⊃ unmapped;erased) ;mapped(apebs[ebatbl[n].pnum].data, (evol[n].mapped? ⊃ evol[n].fill;apebs[ebatbl[n].pnum].fill)) ) | A User Theorem |
| absf-size | ⊦ m ≤ # ebatbl → # absf(v, evol, apebs, ebatbl, q, m) = # ebatbl | A User Theorem |