[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 350 from proof prepost-scan-all (previous step)

# wlar0 = n0 + vtblpnum, # apebs = n0 + vtblpnum, avhdr.size = 0, apebs[vtblpnum] = mkpeb(aechdr(m), avhdr1, buf1, m0, false), avhdr = apebs[vtblpnum].vidhdr, bflipset = bflipset0 ++ vtblpnum, bitflips, buf = mkbuf(LEB_SIZE), err = ESUCCESS, err = err0, ladr = avhdr.vol × avhdr.leb, n = 0, vtblpnum0 = recs[ladr].pnum, wlar = wlar1[vtblpnum, wl-entry(wlar1[vtblpnum].ec, used)], wlar1 = wlar0[vtblpnum, wlar0[vtblpnum].ec:= m], avhdr.valid?, apebs[vtblpnum].vidhdr.valid?, vtblpnum < # wlar1, vtblpnum < # apebs, nx < vtblpnum, vtblpnum < # wlar0, vtblpnum0 < # wlar, bflipset-cons(bflipset0, subarray(wlar0, 0, vtblpnum)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avhdr1, buf1, m0, false)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum), q), valid-global-sqn(subarray(apebs, 0, vtblpnum), sqnum), valid-recs(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum)), ladr ∈ recs, recs[ladr].sqn ≤ avhdr.sqn, avhdr.size ≠ 0 → avhdr.size ≤ datasize(buf) ∧ avhdr.checksum = checksum(buf, avhdr.size), avhdr.size ≠ 0 → avhdr.valid? ∧ (avhdr.size ≤ datasize(buf) → avhdr.valid? ∧ avhdr.valid?), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ apebs[vtblpnum].vidhdr = empty, n0 = 0, dups(nx), vtblpnum + 1 ≤ # apebs ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # apebs = # wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, erasing)] ∧ nx < vtblpnum + 1 ∧ indices-erasing(wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum + 1), max(sqnum, avhdr.sqn + 1)) ∧ valid-eraseq (subarray(wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, erasing)], 0, vtblpnum + 1), q + eq-entry(vtblpnum0, avhdr.vol × avhdr.leb) ') ∧ bflipset-cons(bflipset -- vtblpnum0, subarray(wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, erasing)], 0, vtblpnum + 1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum + 1), q + eq-entry(vtblpnum0, avhdr.vol × avhdr.leb) ') ∧ valid-wl(subarray(apebs, 0, vtblpnum + 1), subarray(wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, erasing)], 0, vtblpnum + 1)) ∧ valid-recs-sqns(apebs, recs[ladr, recovery-entry(vtblpnum, avhdr.sqn)]) ∧ valid-recs (subarray(apebs, 0, vtblpnum + 1), subarray(wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, erasing)], 0, vtblpnum + 1), recs[ladr, recovery-entry(vtblpnum, avhdr.sqn)])) ∧ # apebs < n0 + vtblpnum + 1

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 351:
# apebs = n0 + vtblpnum, # wlar0 = n0 + vtblpnum, avhdr1.size = 0, apebs[vtblpnum] = mkpeb(aechdr(m), avhdr1, buf1, m0, false), avhdr1.valid?, nx < vtblpnum, recs[avhdr1.vol × avhdr1.leb].pnum < n0 + vtblpnum, bflipset-cons(bflipset0, subarray(wlar0, 0, vtblpnum)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avhdr1, buf1, m0, false)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum), q), valid-global-sqn(subarray(apebs, 0, vtblpnum), sqnum), valid-recs(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum)), avhdr1.vol × avhdr1.leb ∈ recs, recs[avhdr1.vol × avhdr1.leb].sqn ≤ avhdr1.sqn ⊦ avhdr1 = empty, n0 = 0, dups(nx), indices-erasing (wlar0[vtblpnum, wl-entry(m, used)] [recs[avhdr1.vol × avhdr1.leb].pnum, wl-entry(wlar0[vtblpnum, wl-entry(m, used)][recs[avhdr1.vol × avhdr1.leb].pnum].ec, erasing) ], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum + 1), max(sqnum, avhdr1.sqn + 1)) ∧ valid-eraseq (subarray (wlar0[vtblpnum, wl-entry(m, used)] [recs[avhdr1.vol × avhdr1.leb].pnum, wl-entry(wlar0[vtblpnum, wl-entry(m, used)][recs[avhdr1.vol × avhdr1.leb].pnum].ec, erasing) ], 0, vtblpnum + 1), q + eq-entry(recs[avhdr1.vol × avhdr1.leb].pnum, avhdr1.vol × avhdr1.leb) ') ∧ bflipset-cons ((bflipset0 ++ vtblpnum) -- recs[avhdr1.vol × avhdr1.leb].pnum, subarray (wlar0[vtblpnum, wl-entry(m, used)] [recs[avhdr1.vol × avhdr1.leb].pnum, wl-entry(wlar0[vtblpnum, wl-entry(m, used)][recs[avhdr1.vol × avhdr1.leb].pnum].ec, erasing) ], 0, vtblpnum + 1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum + 1), q + eq-entry(recs[avhdr1.vol × avhdr1.leb].pnum, avhdr1.vol × avhdr1.leb) ') ∧ valid-wl (subarray(apebs, 0, vtblpnum + 1), subarray (wlar0[vtblpnum, wl-entry(m, used)] [recs[avhdr1.vol × avhdr1.leb].pnum, wl-entry(wlar0[vtblpnum, wl-entry(m, used)][recs[avhdr1.vol × avhdr1.leb].pnum].ec, erasing) ], 0, vtblpnum + 1)) ∧ valid-recs-sqns(apebs, recs[avhdr1.vol × avhdr1.leb, recovery-entry(vtblpnum, avhdr1.sqn)]) ∧ valid-recs (subarray(apebs, 0, vtblpnum + 1), subarray (wlar0[vtblpnum, wl-entry(m, used)] [recs[avhdr1.vol × avhdr1.leb].pnum, wl-entry(wlar0[vtblpnum, wl-entry(m, used)][recs[avhdr1.vol × avhdr1.leb].pnum].ec, erasing) ], 0, vtblpnum + 1), recs[avhdr1.vol × avhdr1.leb, recovery-entry(vtblpnum, avhdr1.sqn)])

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ m < m + n ↔ n ≠ 0; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic% ⊦ m < n + 1 ↔ ¬ n < m; (s)% ⊦ nx < m → nx < m + n; (ss)% ⊦ m + 1 ≤ n ↔ m < n; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ # wlar[n, wle] = # wlar; (s)%m < # wlar ⊦ wlar[m, wle][m, wle0] = wlar[m, wle0]; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m + m0 ≤ m ↔ m0 = 0; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ (wle.ec:= m).ec = m; (s)% ⊦ m < # wlar → wlar[m, wle][m] = wle; (s)