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

# 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)])

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 352:
# wlar0 = n0 + vtblpnum, # apebs = n0 + vtblpnum, apebs[vtblpnum] = mkpeb(aechdr(m), avhdr1, buf1, m0, false), avhdr1 = avidhdr(v, m1, m2, m3, m4), m3 = 0, avhdr1.valid?, recs[v × m1].pnum < n0 + vtblpnum, nx < 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)), v × m1 ∈ recs, recs[v × m1].sqn ≤ m2 ⊦ avhdr1 = empty, n0 = 0, dups(nx), indices-erasing (wlar0[vtblpnum, wl-entry(m, used)][recs[v × m1].pnum, wl-entry(wlar0[vtblpnum, wl-entry(m, used)][recs[v × m1].pnum].ec, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum + 1), max(sqnum, m2 + 1)) ∧ valid-eraseq (subarray (wlar0[vtblpnum, wl-entry(m, used)][recs[v × m1].pnum, wl-entry(wlar0[vtblpnum, wl-entry(m, used)][recs[v × m1].pnum].ec, erasing)], 0, vtblpnum + 1), q + eq-entry(recs[v × m1].pnum, v × m1) ') ∧ bflipset-cons ((bflipset0 ++ vtblpnum) -- recs[v × m1].pnum, subarray (wlar0[vtblpnum, wl-entry(m, used)][recs[v × m1].pnum, wl-entry(wlar0[vtblpnum, wl-entry(m, used)][recs[v × m1].pnum].ec, erasing)], 0, vtblpnum + 1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum + 1), q + eq-entry(recs[v × m1].pnum, v × m1) ') ∧ valid-wl (subarray(apebs, 0, vtblpnum + 1), subarray (wlar0[vtblpnum, wl-entry(m, used)][recs[v × m1].pnum, wl-entry(wlar0[vtblpnum, wl-entry(m, used)][recs[v × m1].pnum].ec, erasing)], 0, vtblpnum + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum, m2)]) ∧ valid-recs (subarray(apebs, 0, vtblpnum + 1), subarray (wlar0[vtblpnum, wl-entry(m, used)][recs[v × m1].pnum, wl-entry(wlar0[vtblpnum, wl-entry(m, used)][recs[v × m1].pnum].ec, erasing)], 0, vtblpnum + 1), recs[v × m1, recovery-entry(vtblpnum, m2)])

Rule argument

spec: avidheader name: elim seq: ⊦ avhdr.valid? → ( ( ((v = avhdr.vol ∧ m = avhdr.leb) ∧ m0 = avhdr.sqn) ∧ m1 = avhdr.size) ∧ m2 = avhdr.checksum ↔ avhdr = avidhdr(v, m, m0, m1, m2)) subst: [avhdr, v, m, m0, m1, m2] → [avhdr1, v, m1, m2, m3, m4]

Additional information

Used simplifier rules: ⊦ avhdr.valid? → ( ( ((v = avhdr.vol ∧ m = avhdr.leb) ∧ m0 = avhdr.sqn) ∧ m1 = avhdr.size) ∧ m2 = avhdr.checksum ↔ avhdr = avidhdr(v, m, m0, m1, m2)); (elim) Used terms: avhdr1, v, m1, m2, m3, m4