[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 206 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, wlar1[m2] = wl-entry(m7, stat), 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), stat = used, 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, stat = used → v0 = v ∧ m5 = m6 ∧ avhdr0.sqn = valid-sqns(v, m6, apebs0).max, stat ≠ erasing → m3 = m7 ⊦ avhdr0 = empty, m2 = m1, stat = erroneous, stat = free, 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 207:
# apebs0 = # wlar0, # wlar0 = # wlar0.mapIndices(nx, λ wle. wle.ec:= 0), # wlar = # wlar0, # wlar1 = # wlar0, avhdr0.sqn = valid-sqns(v, m6, apebs0).max, wlar1[m2] = wl-entry(m7, used), vols1[v][m6] = unmapped, apebs0[m1] = mkpeb(aehdr, avhdr, buf1, m0, false), recs0[VTBL_VOLID × VTBL_LNUM] = recovery-entry(m1, avhdr.sqn), vols[v][m6] = ⌜m2⌝ , wlar0[m2] = wl-entry(m7, used), wlar0.mapIndices(nx, λ wle. wle.ec:= 0)[m2] = wl-entry(m4, used), apebs0[m2] = mkpeb(aechdr(m7), avhdr0, buf, m, false), m6 < # vols1[v], m6 < # vols[v], 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(aehdr, avhdr, buf1, m0, false)), ubi-io-peb-inv(mkpeb(aechdr(m7), avhdr0, buf, m, 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(v, m6, mkpeb(aechdr(m7), 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), v ∈ vols1, v ∈ vols, VTBL_VOLID × VTBL_LNUM ∈ recs0, q ⊆ q0 ⊦ avhdr0 = empty, m2 = m1, dups(nx), m2 ∈ q0, eq-entry(m2, v × m6) ∈ q1, VTBL_VOLID ∈ vols1, m1 ∈ q, VTBL_VOLID ∈ vols0, m1 ∈ q1, VTBL_VOLID ∈ vols, m1 ∈ q0

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-mapped-valid-peb: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-wl(apebs, wlar) → valid-peb(v, m, apebs[n]);%⊦ valid-peb(v0, m0, apeb) → (valid-peb(v1, m1, apeb) ↔ v0 = v1 ∧ m0 = m1); (s)% ⊦ m < n → n ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic% ⊦ used ≠ erasing; (s)% ⊦ used ≠ erroneous; (s)% ⊦ used ≠ free; (s)