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: |
|---|---|---|
| elems-def | ⊦ n ∈ elems nx ↔ n ∈ nx | An Axiom |
| crash-logblock | ⊦ crash-logblock(gblock, n) = groupblock(gblock.gndlist, gblock.ladrlist, n) | An Axiom |
| crash-group-at | ⊦ n ∈ crash(gstore, gstore0, ginval, nx) → crash(gstore, gstore0, ginval, nx)[n] = (n ∈ nx ∨ ¬ n ∈ ginval ⊃ groupblock(gstore[n].gndlist, gstore[n].ladrlist, (n ∈ gstore0 ⊃ gstore0[n].ref-size;0));gstore0[n]) | An Axiom |
| crash-group-in | ⊦ n ∈ crash(gstore, gstore0, ginval, nx) ↔ n ∈ gstore ∨ n ∈ ginval | An Axiom |
| crash-index-at | ⊦ n ∈ istore0 → crash(istore, istore0)[n] = indexblock(istore[n].indlist, istore[n].ladrlist, istore0[n].ref-size) | An Axiom |
| crash-index-in | ⊦ n ∈ crash(istore, istore0) ↔ n ∈ istore0 | An Axiom |
| inv-index | ⊦ inv-index(istore, istore0) ↔ inv(istore) ∧ inv(istore0) ∧ istore0 ⊑ istore ∧ remove-refsize0(istore0) = istore0 | An Axiom |
| inv-journal | ⊦ inv-journal(nx, gstore, gstore0, ginval) ↔ inv(gstore \ ginval) ∧ inv(gstore0) ∧ elems nx ∩ ginval = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ remove-refsize0(gstore0) = gstore0 | An Axiom |
| inv | ⊦ inv(nx, gstore, gstore0, ginval, istore, istore0) ↔ ¬ ¬(inv-journal(nx, gstore, gstore0, ginval) ∧ inv-index(istore, istore0)) | An Axiom |
| inv-state | ⊦ inv-state(pstate, nx, gstore, istore, syn) ↔ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn) | An Axiom |
| crash-gstore-inv | ⊦ inv(gstore \ ginval) ∧ inv(gstore0) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval → inv(crash(gstore, gstore0, ginval, nx) \ ginval) | A User Theorem |
| crash-update-reverted | ⊦ gstore[n] = groupblock(gndx, lax, m0) ∧ n ∈ gstore → crash(gstore[n, groupblock(gndx, lax, m2)], gstore1, ginval, nx) = crash(gstore, gstore1, ginval, nx) | A User Theorem |
| dom-disj-in-l | ⊦ dom gstore ∩ dom istore = ∅ ∧ n ∈ gstore → (n ∈ istore ↔ false) | A User Theorem |
| dom-disj-in-r | ⊦ dom gstore ∩ dom istore = ∅ ∧ n ∈ istore → (n ∈ gstore ↔ false) | A User Theorem |
| dom-gstore-crash | ⊦ dom crash(gstore, gstore0, ginval, nx) = dom gstore ∪ ginval | A User Theorem |
| dom-gstore-intersect-in-gstore | ⊦ ns ∩ dom gstore = ∅ ∧ n ∈ gstore → ¬ n ∈ ns | A User Theorem |
| dom-istore-crash | ⊦ dom crash(istore, istore0) = dom istore0 | A User Theorem |
| dom-istore-crash-refm-refsize0 | ⊦ remove-refsize0(istore0) = istore0 → dom remove-refsize0(crash(istore, istore0)) = dom istore0 | A User Theorem |
| elems-append | ⊦ elems(nx0 + n ') = elems nx0 ++ n | A User Theorem |
| elems-empty | ⊦ elems [] = ∅ | A User Theorem |
| elems-in-diff | ⊦ n ∈ nx0 ∧ ¬ n ∈ nx1 → n ∈ elems nx0 \ elems nx1 | A User Theorem |
| elems-in-fwd | ⊦ n ∈ nx ∧ elems nx ⊆ ns → n ∈ ns | A User Theorem |
| elems-in-notin-ginval | ⊦ n ∈ nx ∧ elems nx ∩ ns = ∅ → ¬ n ∈ ns | A User Theorem |
| elems-log-subset-gstore-union-ginval | ⊦ ns ∪ elems nx = dom gstore ∪ ginval → elems nx ⊆ dom gstore ∪ ginval | A User Theorem |
| elems-minus | ⊦ elems(nx -l n) = elems nx -- n | A User Theorem |
| elems-prepend | ⊦ elems(n ' + nx0) = elems nx0 ++ n | A User Theorem |
| elems-subseteq-add-diff-notin | ⊦ ¬ n ∈ nx0 ∧ elems nx1 ⊆ elems nx0 → (elems nx0 ++ n) \ elems nx1 = (elems nx0 \ elems nx1) ++ n | A User Theorem |
| fwd-in-gstore-loghead | ⊦ nx ≠ [] ∧ ginval ∩ elems nx = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval → nx.last ∈ gstore | A User Theorem |
| fwd-in-gstore0 | ⊦ n ∈ gstore ∧ ¬ n ∈ nx ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval → n ∈ gstore0 | A User Theorem |
| fwd-in-log-in-gstore | ⊦ n ∈ nx ∧ ginval ∩ elems nx = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval → n ∈ gstore | A User Theorem |
| fwd-inv-gblock | ⊦ inv(gstore) ∧ n ∈ gstore ∧ gstore[n] = gblock → inv(gblock) | A User Theorem |
| fwd-inv-gblock-rem | ⊦ inv(gstore \ ginval) ∧ n ∈ gstore ∧ ¬ n ∈ ginval ∧ gstore[n] = gblock → inv(gblock) | A User Theorem |
| fwd-inv-gblock-rem-del | ⊦ inv(gstore \ (ginval -- n)) ∧ n ∈ gstore ∧ gstore[n] = gblock → inv(gblock) | A User Theorem |
| fwd-inv-iblock | ⊦ inv(istore) ∧ n ∈ istore ∧ istore[n] = iblock → inv(iblock) | A User Theorem |
| fwd-inv-loghead | ⊦ nx ≠ [] ∧ inv(gstore \ ginval) ∧ ginval ∩ elems nx = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval → inv(gstore[nx.last]) | A User Theorem |
| icrash-inv | ⊦ inv(istore) ∧ istore0 ⊑ istore → inv(remove-refsize0(crash(istore, istore0))) | A User Theorem |
| icrash-refsize-cons | ⊦ refsize-cons(crash(istore1, istore0), as) ↔ refsize-cons(istore0, as) | A User Theorem |
| icrash-remove-refsize0-prefix | ⊦ istore0 ⊑ istore ∧ istore0 = remove-refsize0(istore0) → istore0 ⊑ remove-refsize0(crash(istore, istore0)) | A User Theorem |
| in-crash-at-gstore | ⊦ @(m0, m1, m2) ∈ crash(gstore, gstore0, ginval, nx) ∧ ¬ m0 ∈ ginval → crash(gstore, gstore0, ginval, nx)[@(m0, m1, m2)] = gstore[@(m0, m1, m2)] | A User Theorem |
| in-crash-in-gstore | ⊦ @(m0, m1, m2) ∈ crash(gstore, gstore0, ginval, nx) ∧ ¬ m0 ∈ ginval → @(m0, m1, m2) ∈ gstore | A User Theorem |
| inv-crash | ⊦ istore0 ⊑ istore ∧ inv(istore) → inv(crash(istore, istore0)) | A User Theorem |
| notin-gstore-ginval-notin-gstore0 | ⊦ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ ¬ n ∈ gstore ∧ n ∈ gstore0 → n ∈ ginval | A User Theorem |
| store-diff-union-elems-notin | ⊦ ¬ n ∈ ns ∧ ¬ n ∈ nx → (gstore \ (ns ∪ elems nx))[n] = gstore[n] | A User Theorem |