[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 163 from proof refine-add-gnds (previous step)

# gndx0 = # lax0, # buf0 = gndx0.flashsize, # lpt0 = # avol, # lpt1 = # avol, (elems nx ∪ dom gstore0) ++ n = dom gstore1 ∪ ginval, gstore1[n] = groupblock(gndx1, lax1, m1), avol[n] = mapped(buf1), lpt1[n] = mklp(m1, # buf1, LP_GROUP_NODES, m2), ax = lax0.to-adr(pstate.lnum), err0 = ESUCCESS, gstore = gstore1[pstate.lnum, gstore1[pstate.lnum].gndlist:= (gstore1[pstate.lnum].gndlist + prefixn(# lax0, gndx0))] [pstate.lnum, gstore1[pstate.lnum, gstore1[pstate.lnum].gndlist:= (gstore1[pstate.lnum].gndlist + prefixn(# lax0, gndx0))][pstate.lnum] .ladrlist:= ( gstore1[pstate.lnum, gstore1[pstate.lnum].gndlist:= (gstore1[pstate.lnum].gndlist + prefixn(# lax0, gndx0))][pstate.lnum] .ladrlist + lax0) ], keyset(gch) = gc-heap(lpt1, nx + n '), pstate = journal(n), remove-refsize0(gstore0) = gstore0, remove-refsize0(istore1) = istore1, ginval ∩ elems nx = ∅, ginval < # avol, n < # avol, abs-gstore(avol, lpt1, gstore1, ginval), abs-istore(avol, lpt1, istore2), abs-nodes(buf0, # buf1, gndx0, lax0, false), awbuf-inv(avol[n, mapped(buf1 + buf0)], buffered(n)), awbuf-inv(avol, buffered(n)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n), lpt1, avol), bufs-log-only(buffered(n), nx + n ', lpt1), flash-lpt-cons(lpt0, istore1, gstore0), freelist-cons(lpt1, freelist), inv(groupblock(gndx1, lax1, m1)), inv(gstore1 \ ginval), inv(gstore0), inv(istore2), inv(istore1), log-group-block(nx + n ', lpt1), lpt-free-unref(lpt0), lpt-free-unref(lpt1), lpt-leb-size(lpt0), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt0, nx + n '), pstate.lnum ∈ gstore1, pstate.lnum ∈ gstore1[pstate.lnum, gstore1[pstate.lnum].gndlist:= (gstore1[pstate.lnum].gndlist + prefixn(# lax0, gndx0))], n ∈ gstore1, # buf1 + gndx0.flashsize ≤ LEB_SIZE, istore1 ⊑ istore2, isbuf → synced(avol), pstate.index? ∨ pstate.journal? ⊦ gndx0 = [], dups(nx), n ∈ nx, n ∈ ginval, ∃ isbuf1. abs-gstore (avol[pstate.lnum, mapped(avol[pstate.lnum].data + buf0)], lpt1 [pstate.lnum, mklp(lpt1[pstate.lnum].ref-size, lpt1[pstate.lnum].size + gndx0.flashsize, lpt1[pstate.lnum].flags, lpt1[pstate.lnum].gcheapidx) ], gstore, ginval) ∧ (isbuf1 → is-aligned(# avol[pstate.lnum].data + # buf0, EB_PAGE_SIZE)) ∧ pstate ≠ unbuffered ∧ pstate ≠ readonly ∧ n = pstate.lnum ∧ lax0.to-adr(pstate.lnum) = ax ∧ ESUCCESS = err0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 164:
# lpt1 = # avol, # lpt0 = # avol, # buf0 = gndx0.flashsize, # gndx0 = # lax0, (elems nx ∪ dom gstore0) ++ n = dom gstore1 ∪ ginval, lpt1[n] = mklp(m1, # buf1, LP_GROUP_NODES, m2), avol[n] = mapped(buf1), gstore1[n] = groupblock(gndx1, lax1, m1), keyset(gch) = gc-heap(lpt1, nx + n '), remove-refsize0(istore1) = istore1, remove-refsize0(gstore0) = gstore0, ginval ∩ elems nx = ∅, ginval < # avol, n < # avol, abs-gstore(avol, lpt1, gstore1, ginval), abs-istore(avol, lpt1, istore2), abs-leb(mapped(buf1), groupblock(gndx1, lax1, m1), mklp(m1, # buf1, LP_GROUP_NODES, m2)), abs-nodes(buf0, # buf1, gndx0, lax0, false), awbuf-inv(avol, buffered(n)), awbuf-inv(avol[n, mapped(buf1 + buf0)], buffered(n)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n), lpt1, avol), bufs-log-only(buffered(n), nx + n ', lpt1), flash-lpt-cons(lpt0, istore1, gstore0), freelist-cons(lpt1, freelist), inv(istore1), inv(istore2), inv(gstore0), inv(gstore1 \ ginval), inv(groupblock(gndx1, lax1, m1)), log-group-block(nx + n ', lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, nx + n '), n ∈ gstore1, # buf1 + gndx0.flashsize ≤ LEB_SIZE, istore1 ⊑ istore2, isbuf → synced(avol) ⊦ gndx0 = [], abs-leb(mapped(buf1 + buf0), groupblock(gndx1 + gndx0, lax1 + lax0, m1), mklp(m1, # buf1 + gndx0.flashsize, LP_GROUP_NODES, m2)), dups(nx), n ∈ ginval, n ∈ nx

Rule argument

Additional information

Used simplifier rules: fwd-in-gstore-lpt: ⊦ n ∈ gstore ∧ abs-gstore(avol, lpt, gstore, ginval) → n < # lpt ∧ lpt[n].ref-size = gstore[n].ref-size ∧ lpt[n].flags = LP_GROUP_NODES;% ⊦ mklp(n2, n3, lpf, m).gcheapidx = m; (s)% ⊦ mklp(n2, n3, lpf, m).size = n3; (s)%⊦ groupblock(gndx, lax, m).ladrlist:= lax0 = groupblock(gndx, lax0, m); (s)% ⊦ groupblock(gndx, lax, m).ladrlist = lax; (s)%⊦ groupblock(gndx, lax, m).gndlist:= gndx0 = groupblock(gndx0, lax, m); (s)% ⊦ groupblock(gndx, lax, m).gndlist = gndx; (s)% ⊦ mapped(buf).data = buf; (s)% ⊦ groupblock(gndx, lax, m).ref-size = m; (s)% ⊦ mklp(n2, n3, lpf, m).flags = lpf; (s)% ⊦ (gblock.gndlist:= gndx).ref-size = gblock.ref-size; (s)% ⊦ (gblock.ladrlist:= lax).ref-size = gblock.ref-size; (s)% ⊦ mklp(n2, n3, lpf, m).ref-size = n2; (s)%# lpt = # avol ⊦ abs-gstore(avol, lpt, gstore, ginval) → ( abs-gstore (avol[n, aleb], lpt[n, lp], gstore[n, gblock], ginval) ↔ n < # lpt ∧ ( ( lpt[n].flags = LP_GROUP_NODES → lpt[n].ref-size = gstore[n].ref-size) → lp.ref-size = gblock.ref-size ∧ lp.flags = LP_GROUP_NODES) ∧ ( ¬ n ∈ ginval ∧ ( lpt[n].flags = LP_GROUP_NODES → abs-leb(avol[n], gstore[n], lpt[n])) → abs-leb(aleb, gblock, lp))); (ss)% ⊦ readonly ≠ journal(m); (s)% ⊦ unbuffered ≠ journal(m); (s)% ⊦ gstore[n, gblock][n, gblock0] = gstore[n, gblock0]; (s)% ⊦ (gblock.gndlist:= gndx).ladrlist = gblock.ladrlist; (s)% ⊦ gstore[n, gblock][n] = gblock; (s)% ⊦ journal(m).journal?; (s)% ⊦ ¬ journal(m).index?; (s)% ⊦ n ∈ gstore[n, gblock]; (s)%# gndx ≤ m ⊦ prefixn(m, gndx) = gndx; (s)% ⊦ ¬ natkey < natkey; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ journal(m).lnum = m; (s)