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

# apebs = n1 + vtblpnum1, # wlar0 = n1 + vtblpnum1, apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false), recs[v × m1].pnum < n1 + vtblpnum1, nx < vtblpnum1, bflipset-cons(bflipset, subarray(wlar0, 0, vtblpnum1)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum1), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1), q), valid-global-sqn(subarray(apebs, 0, vtblpnum1), sqnum), valid-recs(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1)), v × m1 ∈ recs, m3 ≤ datasize(buf1), recs[v × m1].sqn ≤ m2, m3 ≤ LEB_SIZE ⊦ m3 = 0, n1 = 0, dups(nx), indices-erasing (wlar0[vtblpnum1, wl-entry(m, used)][recs[v × m1].pnum, wl-entry(wlar0[vtblpnum1, wl-entry(m, used)][recs[v × m1].pnum].ec, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum1 + 1), max(sqnum, m2 + 1)) ∧ valid-eraseq (subarray (wlar0[vtblpnum1, wl-entry(m, used)][recs[v × m1].pnum, wl-entry(wlar0[vtblpnum1, wl-entry(m, used)][recs[v × m1].pnum].ec, erasing)], 0, vtblpnum1 + 1), q + eq-entry(recs[v × m1].pnum, v × m1) ') ∧ bflipset-cons (bflipset -- recs[v × m1].pnum, subarray (wlar0[vtblpnum1, wl-entry(m, used)][recs[v × m1].pnum, wl-entry(wlar0[vtblpnum1, wl-entry(m, used)][recs[v × m1].pnum].ec, erasing)], 0, vtblpnum1 + 1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1 + 1), q + eq-entry(recs[v × m1].pnum, v × m1) ') ∧ valid-wl (subarray(apebs, 0, vtblpnum1 + 1), subarray (wlar0[vtblpnum1, wl-entry(m, used)][recs[v × m1].pnum, wl-entry(wlar0[vtblpnum1, wl-entry(m, used)][recs[v × m1].pnum].ec, erasing)], 0, vtblpnum1 + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum1, m2)]) ∧ valid-recs (subarray(apebs, 0, vtblpnum1 + 1), subarray (wlar0[vtblpnum1, wl-entry(m, used)][recs[v × m1].pnum, wl-entry(wlar0[vtblpnum1, wl-entry(m, used)][recs[v × m1].pnum].ec, erasing)], 0, vtblpnum1 + 1), recs[v × m1, recovery-entry(vtblpnum1, m2)])

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 184:
# wlar0 = n1 + vtblpnum1, # apebs = n1 + vtblpnum1, apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false), recs[v × m1] = recovery-entry(m4, m5), nx < vtblpnum1, m4 < n1 + vtblpnum1, bflipset-cons(bflipset, subarray(wlar0, 0, vtblpnum1)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum1), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1), q), valid-global-sqn(subarray(apebs, 0, vtblpnum1), sqnum), valid-recs(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1)), v × m1 ∈ recs, m3 ≤ LEB_SIZE, m5 ≤ m2, m3 ≤ datasize(buf1) ⊦ m3 = 0, n1 = 0, dups(nx), indices-erasing(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(wlar0[vtblpnum1, wl-entry(m, used)][m4].ec, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum1 + 1), max(sqnum, m2 + 1)) ∧ valid-eraseq (subarray(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(wlar0[vtblpnum1, wl-entry(m, used)][m4].ec, erasing)], 0, vtblpnum1 + 1), q + eq-entry(m4, v × m1) ') ∧ bflipset-cons (bflipset -- m4, subarray(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(wlar0[vtblpnum1, wl-entry(m, used)][m4].ec, erasing)], 0, vtblpnum1 + 1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1 + 1), q + eq-entry(m4, v × m1) ') ∧ valid-wl (subarray(apebs, 0, vtblpnum1 + 1), subarray(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(wlar0[vtblpnum1, wl-entry(m, used)][m4].ec, erasing)], 0, vtblpnum1 + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum1, m2)]) ∧ valid-recs (subarray(apebs, 0, vtblpnum1 + 1), subarray(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(wlar0[vtblpnum1, wl-entry(m, used)][m4].ec, erasing)], 0, vtblpnum1 + 1), recs[v × m1, recovery-entry(vtblpnum1, m2)])

Rule argument

spec: recovery-entry name: elim seq: ⊦ m = rec.pnum ∧ m0 = rec.sqn ↔ rec = recovery-entry(m, m0) subst: [rec, m, m0] → [recs[v × m1], m4, m5]

Additional information

Used simplifier rules: ⊦ m = rec.pnum ∧ m0 = rec.sqn ↔ rec = recovery-entry(m, m0); (elim) Used terms: recs[v × m1], m4, m5