[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 36 from proof prepost-add-log-leb (previous step)

# buf3 = EB_PAGE_SIZE, m5 + # lpt = # avol, avol[m6] = mapped(buf1), avol[0] = mapped(buf2), avol[m2] = mapped(buf0), avol0 = avol, err = ESUCCESS, err = err0, logoff = # buf1, avol[m6].mapped?, m6 < # avol, disk-layout(mksb(adr, m7, m6, m2, m3, m4, m5), # lpt), ebm-vol-inv(avol), ebm-vol-inv(avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))]), is-encoded(log, buf1), is-encoded(lpt, lebs(avol, m4, lptlebs(# lpt, LEB_SIZE))), is-encoded(mksb(adr, m7, m6, m2, m3, m4, m5), buf2), is-encoded(rnode(m8), buf3), is-encoded-pad(orphans, m3, buf0), mapped-full?(avol, m4, lptlebs(# lpt, LEB_SIZE)), # buf1 + EB_PAGE_SIZE ≤ LEB_SIZE, 0 + EB_PAGE_SIZE ≤ # buf3, # buf1 ≥ # avol[m6].data, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ # buf1 = LEB_SIZE, (err = ESUCCESS ∨ ⌊err⌋ ) ∧ subarray(avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))], m5, # lpt) = subarray(avol0, m5, # lpt) ∧ ( err = ESUCCESS → m5 + # lpt = # avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))] ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][0].mapped? ∧ is-encoded (mksb(adr, m7, m6, m2, m3, m4, m5), avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][0].data) ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m2].mapped? ∧ is-encoded-pad (orphans, m3, avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m2].data) ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].mapped? ∧ ( logoff + EB_PAGE_SIZE ≠ LEB_SIZE → # avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].data = logoff + EB_PAGE_SIZE) ∧ is-encoded (log + m8 ', avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].data) ∧ mapped-full? (avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))], m4, lptlebs(# lpt, LEB_SIZE)) ∧ is-encoded (lpt, lebs (avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))], m4, lptlebs(# lpt, LEB_SIZE)))) ∧ ( err ≠ ESUCCESS → m5 + # lpt = # avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))] ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][0].mapped? ∧ is-encoded (mksb(adr, m7, m6, m2, m3, m4, m5), avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][0].data) ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m2].mapped? ∧ is-encoded-pad (orphans, m3, avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m2].data) ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].mapped? ∧ ( logoff + EB_PAGE_SIZE ≠ LEB_SIZE → # avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].data = logoff + EB_PAGE_SIZE) ∧ is-encoded(log, avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].data) ∧ mapped-full? (avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))], m4, lptlebs(# lpt, LEB_SIZE)) ∧ is-encoded (lpt, lebs (avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))], m4, lptlebs(# lpt, LEB_SIZE))))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Used simplifier rules: ⊦ is-encoded-pad(ns0, n, buf) → (is-encoded-pad(ns1, n, buf) ↔ ns0 = ns1); (s)% ⊦ m ≤ m; (s)% ⊦ mkempbuf(0) + buf = buf; (s)% ⊦ m - m = 0; (s)% ⊦ mapped(buf) = mapped(buf0) ↔ buf = buf0; (s)% ⊦ m + n = m + n0 ↔ n = n0; (s)% ⊦ n ≤ n0 → (m + (n0 - n)) + n = m + n0; (s)% ⊦ # mkempbuf(n) = n; (s)% ⊦ #(buf + buf0) = # buf + # buf0; (s)% ⊦ ¬ disk-layout(mksb(adr, m0, m, m, n, m3, m4), mainareasize); (s)%m ≠ n ⊦ avol[m, aleb][n] = avol[n]; (s)% ⊦ ¬ disk-layout(mksb(adr, n0, 0, n2, m, n3, n), mainareasize); (s)% ⊦ 0 < m ↔ m ≠ 0; (s)% ⊦ mapped(buf).mapped?; (s)% ⊦ mapped(buf).data = buf; (s)% ⊦ m < # avol → avol[m, aleb][m] = aleb; (s)% ⊦ # avol[n, aleb] = # avol; (s)%n < n0 ⊦ subarray(avol[n, aleb], n0, n1) = subarray(avol, n0, n1); (s)%n ≤ n1 ⊦ ¬ disk-layout(mksb(adr, n0, n1, n2, m, n3, n), mainareasize); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ aleb.mapped? ↔ (∃ buf. aleb = mapped(buf)); (as)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ n + 0 = n; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)