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

# 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(bflipset, 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 (bflipset -- 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)])

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 396:
# wlar0 = n0 + vtblpnum, # apebs = n0 + vtblpnum, apebs[vtblpnum] = mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false), recs[v × m1].pnum < n0 + vtblpnum, nx < vtblpnum, bflipset-cons(bflipset, subarray(wlar0, 0, vtblpnum)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), 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 ⊦ 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 (bflipset -- 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

Additional information

Used simplifier rules: ubi-io-inv-fwd: n < # apebs ⊦ apebs[n] = apeb ∧ ubi-io-inv(apebs) → ubi-io-peb-inv(apeb);%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%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)% ⊦ avidhdr(v, m, m0, m1, m2).valid?; (s)% ⊦ empty ≠ avidhdr(v, m, m0, m1, m2); (s)