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: |
|---|---|---|
| nodes-gstore-at | ⊦ adr ∈ nodes(gstore, ginval) → nodes(gstore, ginval)[adr] = gstore[adr].nd | An Axiom |
| abs-log-base | ⊦ abs-log([], gstore) = [] | An Axiom |
| nodes-gstore-in | ⊦ adr ∈ nodes(gstore, ginval) ↔ ¬ ¬(adr ∈ gstore ∧ ¬ adr.lnum ∈ ginval) | An Axiom |
| abs-log-rec | ⊦ abs-log(n ' + nx, gstore) = gstore[n].ladrlist.to-adr(n) + abs-log(nx, gstore) | An Axiom |
| refsize0-addresses | ⊦ adr ∈ refsize0-addresses(gstore) ↔ ¬ ¬(adr ∈ gstore ∧ gstore[adr.lnum].ref-size = 0) | An Axiom |
| down-store-at | ⊦ n ∈ gstore → gstore ↓[n] = gstore[n] ↓ | An Axiom |
| down-store-in | ⊦ n ∈ gstore ↓ ↔ n ∈ gstore | An Axiom |
| down-block | ⊦ gblock ↓ = groupblock (prefixn(valid-group-nodes(gblock.gndlist), gblock.gndlist), prefixn(valid-group-nodes(gblock.gndlist), gblock.ladrlist), gblock.ref-size) | An Axiom |
| valid-group-nodes-rec | ⊦ valid-group-nodes(gndx + gnd ') = (gnd.end ⊃ # gndx + 1;valid-group-nodes(gndx)) | An Axiom |
| valid-group-nodes-base | ⊦ valid-group-nodes([]) = 0 | An Axiom |
| nodes-block-at | ⊦ adr ∈ nodes(n, gblock) → nodes(n, gblock)[adr] = gblock.gndlist[pos(@(adr.pos, adr.size), gblock.ladrlist)].nd | An Axiom |
| nodes-block-in | ⊦ adr ∈ nodes(n, gblock) ↔ ¬ ¬(adr.lnum = n ∧ @(adr.pos, adr.size) ∈ gblock.ladrlist) | An Axiom |
| restore-log-inv | ⊦ restore-log-inv(nx, nx1, gstore, ginval, log, err) ↔ (∃ nx0. nx = nx0 + nx1 ∧ inv(gstore \ ginval) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → log = abs-log(nx0, gstore ↓) ∧ elems nx ⊆ dom gstore ∧ elems nx ∩ ginval = ∅)) | An Axiom |
| remove-nonend-inv | ⊦ remove-nonend-inv(log, log0, ax, gndx, gndx0, boolvar) ↔ (∃ gndx1. # ax = # gndx ∧ gndx = gndx0 + gndx1 ∧ log = log0 + prefixn(# gndx0, ax) ∧ valid-group-nodes(gndx0) = valid-group-nodes(gndx) ∧ (boolvar → # gndx0 = valid-group-nodes(gndx))) | An Axiom |
| abs-log-adr-explicit-in-leb-notin | ⊦ ¬ n ∈ nx → ¬ @(n, n0, n1) ∈ abs-log(nx, gstore) | A User Theorem |
| abs-log-append-one | ⊦ abs-log(nx + n ', gstore) = abs-log(nx, gstore) + gstore[n].ladrlist.to-adr(n) | A User Theorem |
| abs-log-change-other | ⊦ ¬ n ∈ nx → abs-log(nx, gstore[n, gblock]) = abs-log(nx, gstore) | A User Theorem |
| abs-log-del | ⊦ ¬ n ∈ nx → abs-log(nx, gstore -- n) = abs-log(nx, gstore) | A User Theorem |
| abs-log-eq-butlast | ⊦ nx ≠ [] → (abs-log(nx, gstore) = abs-log(nx.butlast, gstore) + ax ↔ ax = gstore[nx.last].ladrlist.to-adr(nx.last)) | A User Theorem |
| abs-log-except-refsize | ⊦ gstore1 =○refsize gstore0 → abs-log(nx, gstore1) = abs-log(nx, gstore0) | A User Theorem |
| abs-log-except-refsize-down | ⊦ gstore1 =○refsize gstore0 → abs-log(nx, gstore1 ↓) = abs-log(nx, gstore0 ↓) | A User Theorem |
| abs-log-gcrash-down | ⊦ elems nx ∩ ginval = ∅ ∧ inv(gstore \ ginval) → abs-log(nx, crash(gstore, gstore0, ginval, nx0) ↓) = abs-log(nx, gstore ↓) | A User Theorem |
| abs-log-new | ⊦ new(ax, nodes(gstore, ginval)) ∧ elems nx ⊆ dom gstore ∧ elems nx ∩ ginval = ∅ → ax.toSet ∩ abs-log(nx, gstore).toSet = ∅ | A User Theorem |
| abs-log-no-change-eq | ⊦ (∀ n. (n ∈ gstore0 ↔ n ∈ gstore1) ∧ (n ∈ gstore0 → gstore1[n].gndlist = gstore0[n].gndlist ∧ gstore1[n].ladrlist = gstore0[n].ladrlist)) → abs-log(nx, gstore0) = abs-log(nx, gstore1) | A User Theorem |
| abs-log-one | ⊦ abs-log(n ', gstore) = gstore[n].ladrlist.to-adr(n) | A User Theorem |
| abs-log-split-head | ⊦ nx ≠ [] → abs-log(nx, gstore) = abs-log(nx.butlast, gstore) + gstore[nx.last].ladrlist.to-adr(nx.last) | A User Theorem |
| abs-log-toset-inter-restr-empty | ⊦ ¬ n ∈ nx → abs-log(nx, gstore).toSet ∩ (as | n) = ∅ | A User Theorem |
| abs-log-write-last | ⊦ nx ≠ [] ∧ ¬ dups(nx) → abs-log(nx, gstore[nx.last, gblock]) = abs-log(nx.butlast, gstore) + gblock.ladrlist.to-adr(nx.last) | A User Theorem |
| abs-log-write-nochange | ⊦ n ∈ gstore ∧ gblock.gndlist = gstore[n].gndlist ∧ gblock.ladrlist = gstore[n].ladrlist → abs-log(nx, gstore[n, gblock]) = abs-log(nx, gstore) | A User Theorem |
| addresses-restr-subseteq0 | ⊦ as0 = as | n → as0 ⊆ as | A User Theorem |
| adr-in-index-node-key | ⊦ @(n, n0, n1) ∈ ri ∧ # gndx1 = # lax1 ∧ ri-cons(ri, nodes(gstore ↓, ginval)) ∧ gstore[n] = groupblock(gndx0 + gnd ' + gndx1, lax0 + @(n0, n1) ' + lax1, m0) ∧ inv(groupblock(gndx0 + gnd ' + gndx1, lax0 + @(n0, n1) ' + lax1, m0)) → gnd.nd.key ∈ ri ∧ ri[gnd.nd.key] = @(n, n0, n1) | A User Theorem |
| adr-in-ri-in-gstore | ⊦ key ∈ ri ∧ ri[key] = adr ∧ ri-cons(ri, nodes(gstore ↓, ginval)) → adr ∈ gstore | A User Theorem |
| adr-in-ri-leb-notin-ginval | ⊦ key ∈ ri ∧ ri[key] = @(m0, m1, m2) ∧ ri-cons(ri, nodes(gstore ↓, ginval)) → (m0 ∈ ginval ↔ false) | A User Theorem |
| adr-in-ri-notin-nodes | ⊦ ri-cons(ri, nodes(gstore, ginval)) ∧ ¬ adr ∈ nodes(gstore, ginval) → ¬ adr ∈ ri | A User Theorem |
| adresses-restr-subseteq | ⊦ as | n ⊆ as | A User Theorem |
| dom-remove-refsize0-down | ⊦ dom remove-refsize0(gstore ↓) = dom remove-refsize0(gstore) | A User Theorem |
| down-block-explicit | ⊦ groupblock(gndx, lax, m0) ↓ = groupblock(prefixn(valid-group-nodes(gndx), gndx), prefixn(valid-group-nodes(gndx), lax), m0) | A User Theorem |
| down-empty | ⊦ ∅ ↓ = ∅ | A User Theorem |
| down-except-refsize | ⊦ gstore1 =○refsize gstore0 → gstore1 ↓ =○refsize gstore0 ↓ | A User Theorem |
| down-store-adr-in-explicit | ⊦ @(m0, m1, m2) ∈ gstore ↓ ↔ m0 ∈ gstore ∧ @(m1, m2) ∈ gstore ↓[m0].ladrlist | A User Theorem |
| down-store-adr-in-explicit-simp | ⊦ gstore[m0] ↓ = groupblock(gndx, lax, n0) ∧ @(m1, m2) ∈ lax → (@(m0, m1, m2) ∈ gstore ↓ ↔ m0 ∈ gstore ↓) | A User Theorem |
| down-store-at-diff | ¬ n ∈ ginval ⊦ (gstore \ ginval)↓[n] = gstore ↓[n] | A User Theorem |
| down-store-dealloc | ⊦ (gstore -- n)↓ = gstore ↓ -- n | A User Theorem |
| down-store-notin-notin | ⊦ ¬ adr ∈ gstore → ¬ adr ∈ gstore ↓ | A User Theorem |
| down-store-write | ⊦ gstore[m, gblock] ↓ = gstore ↓[m, gblock ↓] | A User Theorem |
| down-store-write-same | ⊦ @(n, n0, n1) ∈ gstore ↓[n, gblock] ↔ @(n0, n1) ∈ gblock.ladrlist | A User Theorem |
| ginval-down | ⊦ gstore ↓ \ ginval = (gstore \ ginval)↓ | A User Theorem |
| ginval-extract-abs-log | ⊦ elems nx ∩ ginval = ∅ → abs-log(nx, gstore) = abs-log(nx, gstore \ ginval) | A User Theorem |
| ginval-extract-nodes | ⊦ nodes(gstore, ginval) = nodes(gstore \ ginval, ginval) | A User Theorem |
| gstore-dom-eq-hole | ⊦ dom gstore0 = dom gstore1 ∧ gstore0 \ {n} = gstore1 \ {n} ∧ n ∈ gstore0 → (∃ gblock. gstore1 = gstore0[n, gblock]) | A User Theorem |
| in-keys-elim | ⊦ key ∈ keys(fs, ax) ↔ (∃ adr. adr ∈ ax ∧ fs[adr].key = key) | A User Theorem |
| in-nodes-down-at-same | ⊦ adr ∈ nodes(gstore ↓, ginval) ∧ gstore[adr] = gnd → gstore ↓[adr] = gstore[adr] | A User Theorem |
| in-nodes-in-gstore | ⊦ @(n, m0, m1) ∈ nodes(gstore, ginval) ∧ inv(gstore[n]) → @(n, m0, m1) ∈ gstore | A User Theorem |
| in-restr-eq-notin-log | ⊦ ax.toSet = as | n ∧ ¬ n ∈ nx → ax.toSet ∩ abs-log(nx, gstore).toSet = ∅ | A User Theorem |
| in-restr-notin-log | ⊦ ax.toSet ⊆ as | n ∧ ¬ n ∈ nx → ax.toSet ∩ abs-log(nx, gstore).toSet = ∅ | A User Theorem |
| in-ri | ⊦ key ∈ ri ∧ ri[key] = adr → adr ∈ ri | A User Theorem |
| index-update-adr-in | ⊦ ¬ dups(kx) ∧ # kx = # ax → (adr ∈ ri[kx, ax] ↔ adr ∈ ax ∨ adr ∈ range(ri \ kx.toSet)) | A User Theorem |
| index-update-append1 | ⊦ # ax = # kx → ri[kx + key ', ax + adr '] = ri[kx, ax][key, adr] | A User Theorem |
| index-update-one | ⊦ ri[key ', adr '] = ri[key, adr] | A User Theorem |
| induction-rev-list | φ([]) ∧ (∀ gndx, gnd. φ(gndx) → φ(gndx + gnd)) ⊦ φ(gndx) | A User Theorem |
| insert-subset-old | ⊦ ks ⊆ ks0 → (ks ++ key ⊆ ks0 ∪ ks1 ↔ key ∈ ks0 ∨ key ∈ ks1) | A User Theorem |
| inter-notin-add-empty | ⊦ ¬ n ∈ istore → ((ns ++ n) ∩ dom istore = ∅ ↔ ns ∩ dom istore = ∅) | A User Theorem |
| inter-subset-rem-empty | ⊦ ns0 ∩ ns1 = ∅ ∧ ns2 ⊆ ns1 → (ns0 \ ns3) ∩ ns2 = ∅ | A User Theorem |
| jnlhd-in-gstore | ⊦ elems nx ⊆ dom gstore ∧ nx ≠ [] → (¬ nx.last ∈ gstore ↔ false) | A User Theorem |
| jnlhd-notin-ginval | ⊦ elems nx ∩ ginval = ∅ ∧ nx ≠ [] → ¬ nx.last ∈ ginval | A User Theorem |
| jnlhd-notin-istore | ⊦ elems nx ⊆ dom gstore ∧ dom gstore ∩ dom istore = ∅ ∧ nx ≠ [] → ¬ nx.last ∈ istore | A User Theorem |
| key-in-ri-in-fs | ⊦ key ∈ ri ∧ ri[key] = adr ∧ ri-cons(ri, fs) → adr ∈ fs | A User Theorem |
| key-in-update-index | ⊦ # kx = # ax → (key ∈ ri[kx, ax] ↔ key ∈ ri ∨ key ∈ kx) | A User Theorem |
| keys-append | ⊦ keys(fs, ax0 + ax1) = keys(fs, ax0) + keys(fs, ax1) | A User Theorem |
| keys-at | ⊦ n < # ax → keys(fs, ax)[n] = fs[ax[n]].key | A User Theorem |
| keys-eq-empty | ⊦ keys(fs, ax) = [] ↔ ax = [] | A User Theorem |
| keys-nodes-in-ri | ⊦ ax.toSet = range ri | n ∧ ri-cons(ri, fs) → keys(fs, ax).toSet ⊆ dom ri | A User Theorem |
| keys-one | ⊦ keys(fs, adr ') = fs[adr].key ' | A User Theorem |
| keys-remove-leb | ⊦ ax.toSet = range ri | n ∧ ri-cons(ri, fs) → ¬ @(n, m0, m1) ∈ ri \ keys(fs, ax).toSet | A User Theorem |
| keys-same-fs | ⊦ fs0 | ax1.toSet = fs1 | ax1.toSet → keys(fs0, ax1) = keys(fs1, ax1) | A User Theorem |
| keys-size | ⊦ # keys(fs, ax) = # ax | A User Theorem |
| ladr-split | ⊦ lax.to-adr(n) = ax0 + ax1 ↔ (∃ lax0, lax1. lax = lax0 + lax1 ∧ ax0 = lax0.to-adr(n) ∧ ax1 = lax1.to-adr(n)) | A User Theorem |
| last-notin-butlast-nodups | ⊦ nx ≠ [] ∧ ¬ dups(nx) → ¬ nx.last ∈ nx.butlast | A User Theorem |
| lebs-dom-remove-refsize0 | ⊦ ri-cons(ri, nodes(gstore ↓, ginval)) ∧ refsize-cons(gstore, range ri) ∧ inv(gstore \ ginval) → ri.lebs ⊆ dom remove-refsize0(gstore) | A User Theorem |
| nds-split | ⊦ gndx.nds = ndx0 + ndx1 ↔ (∃ gndx0, gndx1. gndx = gndx0 + gndx1 ∧ ndx0 = gndx0.nds ∧ ndx1 = gndx1.nds) | A User Theorem |
| new-adrs-gstore | ⊦ ¬ dups(gstore[n].ladrlist + lax) → new(lax.to-adr(n), nodes(gstore, ginval)) | A User Theorem |
| new-prefixn | ⊦ new(ax, fs) → new(prefixn(n, ax), fs) | A User Theorem |
| nodes-allocate | ¬ m ∈ gstore ⊦ nodes(gstore[m, groupblock([], [], m0)], ginval -- m) = nodes(gstore, ginval) | A User Theorem |
| nodes-append-subseteq | # gndx = # lax, n0 ≤ m0 ⊦ n ∈ gstore ∧ gstore[n] = groupblock(gndx, lax, n0) → nodes(gstore ↓, ginval) ⊆ nodes(gstore ↓[n, groupblock(gndx + gnd ', lax + ladr ', m0) ↓], ginval) | A User Theorem |
| nodes-append-subseteq-nodown | # gndx = # lax, # gndx1 = # lax1 ⊦ n ∈ gstore ∧ gstore[n] = groupblock(gndx, lax, m0) → nodes(gstore ↓, ginval) ⊆ nodes(gstore ↓[n, groupblock(gndx + gndx1, lax + lax1, m0)], ginval) | A User Theorem |
| nodes-crash-down | ⊦ inv(gstore \ ginval) → nodes(crash(gstore, gstore0, ginval, nx) ↓, ginval) = nodes(gstore ↓, ginval) | A User Theorem |
| nodes-dealloc | ⊦ nodes(gstore -- n, ginval ++ n) = nodes(gstore, ginval) \ (dom nodes(gstore, ginval) | n) | A User Theorem |
| nodes-empty | ⊦ nodes(∅, ginval) = ∅ | A User Theorem |
| nodes-except-refsize | ⊦ gstore1 =○refsize gstore0 → nodes(gstore1, ginval) = nodes(gstore0, ginval) | A User Theorem |
| nodes-except-refsize-down | ⊦ gstore1 =○refsize gstore0 → nodes(gstore1 ↓, ginval) = nodes(gstore0 ↓, ginval) | A User Theorem |
| nodes-ginval-inter | ⊦ dom gstore ∩ ginval = ∅ → nodes(gstore, ginval) = nodes(gstore, ∅) | A User Theorem |
| nodes-ginval-rem | ⊦ dom gstore1 ⊆ dom gstore → nodes(gstore, ginval \ dom gstore1 \ dom gstore) = nodes(gstore, ginval) | A User Theorem |
| nodes-ginval-rem-01 | ⊦ dom gstore1 ∪ ns = dom gstore → nodes(gstore, ginval \ dom gstore1 \ dom gstore) = nodes(gstore, ginval) | A User Theorem |
| nodes-no-change-eq | ⊦ (∀ n. (n ∈ gstore0 ↔ n ∈ gstore1) ∧ (n ∈ gstore0 → gstore1[n].gndlist = gstore0[n].gndlist ∧ gstore1[n].ladrlist = gstore0[n].ladrlist)) → nodes(gstore0, ginval) = nodes(gstore1, ginval) | A User Theorem |
| nodes-referenced-adrs-leb | ⊦ ri-cons(ri, nodes(gstore ↓, ginval)) ∧ n ∈ gstore ∧ ¬ n ∈ ginval ∧ gstore[n].ladrlist = lax → referenced-adrs(lax.to-adr(n), ri).toSet = range ri | n | A User Theorem |
| nodes-remove-ginval-notin | ⊦ ¬ n ∈ gstore → nodes(gstore, ginval -- n) = nodes(gstore, ginval) | A User Theorem |
| nodes-remove-refsize0 | ⊦ dom remove-refsize0(gstore) ∩ ginval = ∅ → nodes(remove-refsize0(gstore), ∅) = nodes(gstore, ginval) \ refsize0-addresses(gstore \ ginval) | A User Theorem |
| nodes-transaction | ⊦ n ∈ gstore ∧ ¬ n ∈ ginval ∧ transaction(ndx, gndx1) ∧ gstore[n].gndlist = gndx0 ∧ gstore[n].ladrlist = lax0 ∧ # lax0 = # gndx0 ∧ # lax1 = # gndx1 ∧ ¬ dups(lax0 + lax1) → nodes(gstore[n, groupblock(gndx0 + gndx1, lax0 + lax1, m0)], ginval) = nodes(gstore, ginval)[lax1.to-adr(n), ndx] | A User Theorem |
| nodes-write-at-other | n ∈ gstore ⊦ n ≠ m0 → nodes(gstore[n, gblock], ginval)[@(m0, m1, m2)] = nodes(gstore, ginval)[@(m0, m1, m2)] | A User Theorem |
| nodes-write-nochange | ⊦ n ∈ gstore ∧ gblock.gndlist = gstore[n].gndlist ∧ gblock.ladrlist = gstore[n].ladrlist → nodes(gstore[n, gblock], ginval) = nodes(gstore, ginval) | A User Theorem |
| nodes-write-same-flushed | ⊦ gstore[m] = groupblock(gndx, lax, n0) ∧ m ∈ gstore ∧ n0 ≤ m0 ∧ valid-group-nodes(gndx) ≤ n0 → nodes(gstore ↓[m, groupblock(gndx, lax, m0) ↓], ginval) = nodes(gstore ↓, ginval) | A User Theorem |
| notin-down-eq-notin-down | ⊦ nodes(gstore0 ↓, ginval) = fs ∧ ¬ adr ∈ gstore0 → ¬ adr ∈ fs | A User Theorem |
| notin-notin-nodes-down | ⊦ ¬ adr ∈ gstore → ¬ adr ∈ nodes(gstore ↓, ginval) | A User Theorem |
| prefix-append-prefix | ⊦ nx0 ⊑ nx1 ∧ nx2 = nx1 + nx3 → nx0 ⊑ nx2 | A User Theorem |
| prefixn-toset-inter-empty | ⊦ ax.toSet ∩ as = ∅ → prefixn(n, ax).toSet ∩ as = ∅ | A User Theorem |
| prefixn-toset-restr-empty | ⊦ ax.toSet | m = ∅ → prefixn(n, ax).toSet | m = ∅ | A User Theorem |
| prefixn-toset-subseteq | ⊦ ax.toSet ⊆ as → prefixn(n, ax).toSet ⊆ as | A User Theorem |
| range-in-ri-keys-in-ri | ⊦ ax.toSet ⊆ range ri ∧ ri-cons(ri, fs) → keys(fs, ax).toSet ⊆ dom ri | A User Theorem |
| range-rem-in | ⊦ ri-cons(ri, nodes(gstore, ginval)) ∧ key ∈ ri → range(ri -- key) = range ri -- ri[key] | A User Theorem |
| refsize-0-notin-index | ⊦ gstore[n] = groupblock(gndx, lax, 0) ∧ n ∈ gstore ∧ ri-cons(ri, nodes(gstore ↓, ginval)) ∧ refsize-cons(gstore, range ri) ∧ inv(gstore \ ginval) → ¬ @(n, m0, m1) ∈ ri | A User Theorem |
| refsize-cons-remove | ⊦ refsize-cons(gstore, as) → (¬ refsize-cons(gstore -- n, as) ↔ false) | A User Theorem |
| refsize-nonzero-notin-ginval | ⊦ gstore[n] = groupblock(gndx, lax, m2) ∧ n ∈ gstore ∧ m2 ≠ 0 ∧ refsize-cons(gstore, range ri) ∧ ri-cons(ri, nodes(gstore ↓, ginval)) ∧ inv(gstore \ ginval) → ¬ n ∈ ginval | A User Theorem |
| remove-refsize0-down | ⊦ remove-refsize0(gstore) ↓ = remove-refsize0(gstore ↓) | A User Theorem |
| restr-add-01 | ⊦ (as ++ adr) | m = (as | m) ∪ (adr.lnum = m ⊃ ∅ ++ adr;∅) | A User Theorem |
| restr-add-notin | ⊦ ¬ n ∈ gstore → (ns ++ n) \ dom gstore = (ns \ dom gstore) ++ n | A User Theorem |
| restr-empty-notin | ⊦ as | n = ∅ → ¬ @(n, m0, m1) ∈ as | A User Theorem |
| restr-toset-empty-notin | ⊦ ax.toSet | n = ∅ → ¬ @(n, m0, m1) ∈ ax | A User Theorem |
| ri-cons-range-restrict-notin-gstore | ⊦ ¬ n ∈ gstore ∧ ri-cons(ri, nodes(gstore, ginval)) → range ri | n = ∅ | A User Theorem |
| ri-cons-subseteq | ⊦ fs0 ⊆ fs1 ∧ ri-cons(ri, fs0) → ri-cons(ri, fs1) | A User Theorem |
| size-0 | ⊦ ri-cons(ri, nodes(gstore ↓, ginval)) ∧ inv(gstore \ ginval) → ((range ri | m).size = 0 ↔ ¬(∃ adr. adr ∈ range ri ∧ adr.lnum = m)) | A User Theorem |
| sub-restr-sub | ⊦ ((ns -- n) \ ns0) -- n = (ns \ ns0) -- n | A User Theorem |
| toSet-diff-get | ⊦ ¬ key ∈ kx → (ri \ kx.toSet)[key] = ri[key] | A User Theorem |
| toSet-diff-in | ⊦ ¬ key ∈ kx → (key ∈ ri \ kx.toSet ↔ key ∈ ri) | A User Theorem |
| valid-group-nodes-app-transaction | ⊦ transaction(ndx, gndx1) → valid-group-nodes(gndx0 + gndx1) = (gndx1 = [] ⊃ valid-group-nodes(gndx0);# gndx0 + # gndx1) | A User Theorem |
| valid-group-nodes-app-transaction-prefix | ⊦ transaction-prefix(ndx, gndx1) → valid-group-nodes(gndx0 + gndx1) = valid-group-nodes(gndx0) | A User Theorem |
| valid-group-nodes-drop | ⊦ n ≤ valid-group-nodes(prefixn(n, gndx)) → valid-group-nodes(prefixn(n, gndx)) = # prefixn(n, gndx) | A User Theorem |
| valid-group-nodes-drop-superfluous-prefixn | ⊦ valid-group-nodes(gndx) ≤ n → valid-group-nodes(prefixn(n, gndx)) = valid-group-nodes(gndx) | A User Theorem |
| valid-group-nodes-entire | ⊦ # gndx ≤ valid-group-nodes(gndx) ↔ valid-group-nodes(gndx) = # gndx | A User Theorem |
| valid-group-nodes-last-end | ⊦ gndx.last = mkgnode(nd, m, boolvar, true) → valid-group-nodes(gndx) = # gndx | A User Theorem |
| valid-group-nodes-last-end-nosimp | ⊦ gndx.last.end → valid-group-nodes(gndx) = # gndx | A User Theorem |
| valid-group-nodes-le | ⊦ n ≤ valid-group-nodes(gndx) → n ≤ # gndx | A User Theorem |
| valid-group-nodes-ls | ⊦ n < valid-group-nodes(gndx) → n < # gndx | A User Theorem |
| valid-group-nodes-prefixn-append-nonend | ⊦ valid-group-nodes(prefixn(n, gndx + mkgnode(nd, m, boolvar, false) ')) = valid-group-nodes(prefixn(n, gndx)) | A User Theorem |
| valid-group-nodes-shorter-prefix | ⊦ n1 ≤ n0 → ¬ valid-group-nodes(prefixn(n0, gndx)) < valid-group-nodes(prefixn(n1, gndx)) | A User Theorem |
| valid-group-nodes-shorter-prefix-right | ⊦ ¬ valid-group-nodes(gndx) < valid-group-nodes(prefixn(n1, gndx)) | A User Theorem |
| valid-group-nodes-single-end | ⊦ valid-group-nodes(mkgnode(nd, m, boolvar, true) ') = 1 | A User Theorem |
| valid-journal-head-valid-group-nodes | ⊦ valid-journal-head(nx, gstore, ginval) ∧ nx ≠ [] ∧ gstore[nx.last] = groupblock(gndx, lax, lnum) → valid-group-nodes(gndx) = # gndx | A User Theorem |