[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 201 from proof inv-recover (previous step)

# apebs0 = # wlar0, # wlar0 = # wlar0.mapIndices(nx, λ wle. wle.ec:= 0), # wlar = # wlar0, # wlar1 = # wlar0, avhdr0.sqn = valid-sqns(v0, m5, apebs0).max, vols1[v0][m5] = unmapped, apebs0[m1] = mkpeb(aehdr, avhdr, buf1, m0, false), recs0[VTBL_VOLID × VTBL_LNUM] = recovery-entry(m1, avhdr.sqn), vols[v0][m5] = ⌜m2⌝ , wlar0[m2] = wl-entry(m3, used), wlar0.mapIndices(nx, λ wle. wle.ec:= 0)[m2] = wl-entry(m4, used), apebs0[m2] = mkpeb(aechdr(m3), avhdr0, buf, m, false), m5 < # vols1[v0], m5 < # vols[v0], m2 < # wlar0, nx < # wlar0, m1 < # wlar0, bflipset-cons(bflipset2, wlar0), bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset1, wlar1), bflipset-cons(bflipset2, wlar0.mapIndices(nx, λ wle. wle.ec:= 0)), indices-erasing(wlar, nx), is-encoded(vtbl0, buf1), is-max(apebs0, vols, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), q0, bflipset2, m1, sqnum), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aechdr(m3), avhdr0, buf, m, false)), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf1, m0, false)), unique-sqns(apebs0), unmapped-vols(vols0), valid-ebatbl(apebs0, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), vols, m1), valid-ebatbl(apebs0, wlar0, vols, m1), valid-ebatbl(apebs0, wlar1, vols1, m1), valid-eraseq(apebs0, q0), valid-eraseq(wlar0.mapIndices(nx, λ wle. wle.ec:= 0), q0), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(wlar, q), valid-eraseq(apebs0, q1), valid-eraseq(wlar1, q1), valid-eraseq(q1), valid-eraseq-strong(apebs0, vtbl0, q0), valid-eraseq-stronger(apebs0, q), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs0, vtblpnum5), valid-indices(wlar0, nx), valid-peb(v0, m5, mkpeb(aechdr(m3), avhdr0, buf, m, false)), valid-recs(apebs0, wlar, recs0), valid-recs-sqns(apebs0, recs0), valid-vtbl(apebs0, vols, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), m1), valid-vtbl(apebs0, vols, wlar0, m1), valid-vtbl(apebs0, vols0, wlar, m1), valid-vtbl(apebs0, vols1, wlar1, m1), valid-vtbl-weak(apebs0, m1), valid-wl(apebs0, wlar0.mapIndices(nx, λ wle. wle.ec:= 0)), valid-wl(apebs0, wlar), v0 ∈ vols1, v0 ∈ vols, VTBL_VOLID × VTBL_LNUM ∈ recs0, q ⊆ q0, ∀ n. n < # wlar1 → (wlar1[n].status = erroneous ↔ apebs0[n].bad) ∧ (wlar1[n].status = free → apebs0[n].vidhdr = empty) ∧ (wlar1[n].status ≠ erroneous ∧ wlar1[n].status ≠ erasing → apebs0[n].echdr = aechdr(wlar1[n].ec)) ∧ (wlar1[n].status = used → (∃ v, m. valid-peb(v, m, apebs0[n]) ∧ apebs0[n].vidhdr.sqn = valid-sqns(v, m, apebs0).max)) ⊦ m2 = m1, dups(nx), m2 ∈ q0, eq-entry(m2, v0 × m5) ∈ q1, VTBL_VOLID ∈ vols1, m1 ∈ q, VTBL_VOLID ∈ vols0, m1 ∈ q1, VTBL_VOLID ∈ vols, m1 ∈ q0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 202:
# wlar1 = # wlar0, # wlar = # wlar0, # wlar0 = # wlar0.mapIndices(nx, λ wle. wle.ec:= 0), # apebs0 = # wlar0, avhdr0.sqn = valid-sqns(v0, m5, apebs0).max, apebs0[m2] = mkpeb(aechdr(m3), avhdr0, buf, m, false), wlar0.mapIndices(nx, λ wle. wle.ec:= 0)[m2] = wl-entry(m4, used), wlar0[m2] = wl-entry(m3, used), vols[v0][m5] = ⌜m2⌝ , recs0[VTBL_VOLID × VTBL_LNUM] = recovery-entry(m1, avhdr.sqn), apebs0[m1] = mkpeb(aehdr, avhdr, buf1, m0, false), vols1[v0][m5] = unmapped, m1 < # wlar0, nx < # wlar0, m2 < # wlar0, m5 < # vols[v0], m5 < # vols1[v0], bflipset-cons(bflipset2, wlar0.mapIndices(nx, λ wle. wle.ec:= 0)), bflipset-cons(bflipset1, wlar1), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset2, wlar0), indices-erasing(wlar, nx), is-encoded(vtbl0, buf1), is-max(apebs0, vols, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), q0, bflipset2, m1, sqnum), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf1, m0, false)), ubi-io-peb-inv(mkpeb(aechdr(m3), avhdr0, buf, m, false)), unique-sqns(apebs0), unmapped-vols(vols0), valid-ebatbl(apebs0, wlar1, vols1, m1), valid-ebatbl(apebs0, wlar0, vols, m1), valid-ebatbl(apebs0, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), vols, m1), valid-eraseq(q1), valid-eraseq(wlar1, q1), valid-eraseq(apebs0, q1), valid-eraseq(wlar, q), valid-eraseq(wlar0, q0), valid-eraseq(q0), valid-eraseq(wlar0.mapIndices(nx, λ wle. wle.ec:= 0), q0), valid-eraseq(apebs0, q0), valid-eraseq-strong(apebs0, vtbl0, q0), valid-eraseq-stronger(apebs0, q), valid-global-sqn(apebs0, vtblpnum5), valid-global-sqn(apebs0, sqnum), valid-indices(wlar0, nx), valid-peb(v0, m5, mkpeb(aechdr(m3), avhdr0, buf, m, false)), valid-recs(apebs0, wlar, recs0), valid-recs-sqns(apebs0, recs0), valid-vtbl(apebs0, vols1, wlar1, m1), valid-vtbl(apebs0, vols0, wlar, m1), valid-vtbl(apebs0, vols, wlar0, m1), valid-vtbl(apebs0, vols, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), m1), valid-vtbl-weak(apebs0, m1), valid-wl(apebs0, wlar), valid-wl(apebs0, wlar0.mapIndices(nx, λ wle. wle.ec:= 0)), VTBL_VOLID × VTBL_LNUM ∈ recs0, v0 ∈ vols, v0 ∈ vols1, q ⊆ q0, ∀ n. n < # wlar0 → (wlar1[n].status = erroneous ↔ apebs0[n].bad) ∧ (wlar1[n].status = free → apebs0[n].vidhdr = empty) ∧ (wlar1[n].status ≠ erroneous ∧ wlar1[n].status ≠ erasing → apebs0[n].echdr = aechdr(wlar1[n].ec)) ∧ (wlar1[n].status = used → (∃ v, m. valid-peb(v, m, apebs0[n]) ∧ apebs0[n].vidhdr.sqn = valid-sqns(v, m, apebs0).max)) ⊦ m2 = m1, dups(nx), m1 ∈ q0, VTBL_VOLID ∈ vols, m1 ∈ q1, VTBL_VOLID ∈ vols0, m1 ∈ q, VTBL_VOLID ∈ vols1, eq-entry(m2, v0 × m5) ∈ q1, m2 ∈ q0

Proof step 201 from proof inv-recover (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information