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

# wlar0 = # wlar0.mapIndices(nx, λ wle. wle.ec:= 0), # wlar = # wlar0, # wlar1 = # wlar0, # apebs0 = # wlar0, apebs0[m1] = mkpeb(aehdr, avhdr, buf1, m0, false), recs0[VTBL_VOLID × VTBL_LNUM] = recovery-entry(m1, avhdr.sqn), 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-cons(apebs0, vols1, wlar1, q1, bflipset1, m1, vtblpnum5), ubi-io-inv(apebs0), 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-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, wlar0), valid-wl(apebs0, wlar), valid-wl(apebs0, wlar1), VTBL_VOLID × VTBL_LNUM ∈ recs0, q ⊆ q0 ⊦ dups(nx), VTBL_VOLID ∈ vols1, m1 ∈ q, VTBL_VOLID ∈ vols0, m1 ∈ q1, VTBL_VOLID ∈ vols, m1 ∈ q0, true ∧ vols⌈vols1, q1⌉

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 184:
# apebs0 = # wlar0, # wlar0 = # wlar0.mapIndices(nx, λ wle. wle.ec:= 0), # wlar = # wlar0, # wlar1 = # wlar0, apebs0[m1] = mkpeb(aehdr, avhdr, buf1, m0, false), recs0[VTBL_VOLID × VTBL_LNUM] = recovery-entry(m1, avhdr.sqn), 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)), 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-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, wlar0), valid-wl(apebs0, wlar), valid-wl(apebs0, wlar1), VTBL_VOLID × VTBL_LNUM ∈ recs0, q ⊆ q0 ⊦ dups(nx), VTBL_VOLID ∈ vols1, m1 ∈ q, VTBL_VOLID ∈ vols0, m1 ∈ q1, VTBL_VOLID ∈ vols, m1 ∈ q0, vols⌈vols1, q1⌉

Rule argument

Additional information

Used simplifier rules: ⊦ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ↔ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, n1) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0); (s)