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

# 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(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false)), 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-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)]), vtblpnum1 < # apebs ∧ m4 < vtblpnum1 ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1), q) ∧ valid-peb(v, m1, apebs[vtblpnum1]) ∧ valid-sqns(v, m1, apebs, vtblpnum1).max < apebs[vtblpnum1].vidhdr.sqn ∧ valid-peb(v, m1, apebs[m4]) ∧ ¬ m4 ∈ q

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 153:
# wlar0 = n1 + vtblpnum1, # apebs = n1 + vtblpnum1, avhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum1).max, apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, avhdr.sqn, 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, avhdr.sqn, 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(aechdr(m), avidhdr(v, m1, avhdr.sqn, m3, checksum(buf1, m3)), buf1, m0, false)), valid-peb(mkpeb(aechdr(m), avidhdr(v, m1, avhdr.sqn, m3, checksum(buf1, m3)), buf1, m0, false)), 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, 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-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, avhdr.sqn)])

Rule argument

Additional information

Used simplifier rules: ubi-io-inv-fwd: n < # apebs ⊦ apebs[n] = apeb ∧ ubi-io-inv(apebs) → ubi-io-peb-inv(apeb);% ⊦ m + m0 ≤ m ↔ m0 = 0; (s)% ⊦ m ≤ m; (s)% ⊦ m ≤ n → (n ≤ m ↔ m = n); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ avidhdr(v, m, m0, m1, m2).leb = m; (s)% ⊦ avidhdr(v, m, m0, m1, m2).vol = v; (s)%⊦ valid-peb(apeb) → (valid-peb(v, m, apeb) ↔ v = apeb.vidhdr.vol ∧ m = apeb.vidhdr.leb); (ss)%⊦ valid-peb(v0, m0, apeb) → (valid-peb(v1, m1, apeb) ↔ v0 = v1 ∧ m0 = m1); (s)% ⊦ avidhdr(v, m, m0, m1, m2).sqn = m0; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m < m + n ↔ n ≠ 0; (s)