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

# wlar0 = n1 + vtblpnum1, # apebs = n1 + vtblpnum1, avhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum1).max, apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false), recs[v × m1] = recovery-entry(m4, avhdr.sqn), apebs[m4] = mkpeb(aehdr, avhdr, buf, m5, boolvar), wlar0[m4] = wl-entry(m6, stat), m4 < n1 + vtblpnum1, m4 < vtblpnum1, nx < vtblpnum1, bflipset-cons(bflipset0, subarray(wlar0, 0, vtblpnum1)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m5, boolvar)), 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-peb(v, m1, mkpeb(aehdr, avhdr, buf, m5, boolvar)), 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, avhdr.sqn ≤ m2, m3 ≤ datasize(buf1), bitflips0 ∨ bitflips ⊦ m3 = 0, n1 = 0, dups(nx), m4 ∈ q, indices-erasing(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(m6, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum1 + 1), max(sqnum, m2 + 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(m6, erasing)], 0, vtblpnum1 + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum1, m2)])

User applied rule cut formula

And obtained the following new goals

Proof step 149:
# apebs = n1 + vtblpnum1, # wlar0 = n1 + vtblpnum1, avhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum1).max, wlar0[m4] = wl-entry(m6, stat), apebs[m4] = mkpeb(aehdr, avhdr, buf, m5, boolvar), recs[v × m1] = recovery-entry(m4, avhdr.sqn), apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false), nx < vtblpnum1, m4 < vtblpnum1, m4 < n1 + vtblpnum1, bflipset-cons(bflipset0, 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)), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m5, boolvar)), 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-peb(v, m1, mkpeb(aehdr, avhdr, buf, m5, boolvar)), valid-peb(apebs[vtblpnum1]), 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), avhdr.sqn ≤ m2, m3 ≤ LEB_SIZE, bitflips0 ∨ bitflips ⊦ m3 = 0, n1 = 0, dups(nx), m4 ∈ q, indices-erasing(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(m6, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum1 + 1), max(sqnum, m2 + 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(m6, erasing)], 0, vtblpnum1 + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum1, m2)])
Proof step 163:
# apebs = n1 + vtblpnum1, # wlar0 = n1 + vtblpnum1, avhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum1).max, wlar0[m4] = wl-entry(m6, stat), apebs[m4] = mkpeb(aehdr, avhdr, buf, m5, boolvar), recs[v × m1] = recovery-entry(m4, avhdr.sqn), apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false), nx < vtblpnum1, m4 < vtblpnum1, m4 < n1 + vtblpnum1, bflipset-cons(bflipset0, 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)), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m5, boolvar)), 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-peb(v, m1, mkpeb(aehdr, avhdr, buf, m5, boolvar)), 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), avhdr.sqn ≤ m2, m3 ≤ LEB_SIZE, bitflips0 ∨ bitflips ⊦ m3 = 0, n1 = 0, dups(nx), valid-peb(apebs[vtblpnum1]), m4 ∈ q, indices-erasing(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(m6, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum1 + 1), max(sqnum, m2 + 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(m6, erasing)], 0, vtblpnum1 + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum1, m2)])

Rule argument

fma: valid-peb(apebs[vtblpnum1])

Additional information

Used formulas: valid-peb(apebs[vtblpnum1])