[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 24 from proof prepost-get-peb (previous step)

# apebs = # wlar, apebs = apebs, apebs0 = apebs, apebs1 = apebs, bflipset0 = bflipset, free-ecs(wlar) = ∅, lref0 = lref, m0 = m, q2 = [], q3 = q1, sqnum0 = sqnum, vols0 = vols, vtblpnum1 = vtblpnum0, wlar = wlar, wlar0 = wlar, wlar1 = wlar, m < # wlar, bflipset-cons(bflipset, wlar), ubi-cons(apebs, vols, wlar, [] + eq-entry(m, lref) ' + q1, bflipset, vtblpnum0, sqnum), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum0), valid-eraseq(apebs, eq-entry(m, lref) ' + q1), valid-eraseq(wlar, eq-entry(m, lref) ' + q1), valid-eraseq(eq-entry(m, lref) ' + q1), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum0), valid-wl(apebs, wlar) ⊦ [ubi_erase_worker_helper#(m; wlar, apebs; err)] ( (err = ESUCCESS → ubi-cons(apebs, vols0, wlar, q2 + q3, bflipset0, vtblpnum1, sqnum0)) ∧ (err ≠ ESUCCESS → ubi-cons(apebs, vols0, wlar, q2 + eq-entry(m0, lref0) ' + q3, bflipset0, vtblpnum1, sqnum0)) ∧ ubi-io-inv(apebs) ∧ wlar[m0].status ≠ used ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(wlar, wlar1, m0) ∧ id○(apebs, apebs1, m0) ∧ id(apebs, apebs1, mapped-pebs(vols0)) → ⟪vtblpnum := m; q0 := eq-entry(m, lref) ' + q1; q := eq-entry(m, lref) ' + q1; if err = ESUCCESS then {q := q.tail; if wlar[vtblpnum].status ≠ free then err := ENOSPC} else err := ENOSPC⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err ≠ ESUCCESS → # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum0) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum0)) ∧ ubi-io-inv(apebs) ∧ q.lebrefs ⊆ q0.lebrefs ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ ( err = ESUCCESS → vtblpnum < # apebs ∧ wlar[vtblpnum].status = free ∧ ( apebs0 = apebs ∧ wlar0 = wlar ∧ q0 = q ∨ id○(apebs0, apebs, vtblpnum) ∧ id○(wlar0, wlar, vtblpnum) ∧ q0 ≠ [] ∧ q0 = eq-entry(vtblpnum, q0.head.lebref) ' + q) ∧ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum0) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum0)))), vtblpnum0 = m, VTBL_VOLID ∈ vols, vtblpnum0 ∈ q1

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 25:
# apebs = # wlar, apebs0 = apebs, free-ecs(wlar) = ∅, wlar0 = wlar, vtblpnum0 ≠ m, m < # wlar, bflipset-cons(bflipset, wlar), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum0), valid-eraseq(apebs, eq-entry(m, lref) ' + q1), valid-eraseq(wlar, eq-entry(m, lref) ' + q1), valid-eraseq(eq-entry(m, lref) ' + q1), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum0), valid-wl(apebs, wlar), ¬ VTBL_VOLID ∈ vols, ¬ vtblpnum0 ∈ q1 ⊦ [ubi_erase_worker_helper#(m; wlar, apebs; err)] ( ( err = ESUCCESS → # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar, q1) ∧ valid-eraseq(apebs, q1) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum0) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum0)) ∧ ( err ≠ ESUCCESS → # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(wlar, eq-entry(m, lref) ' + q1) ∧ valid-eraseq(apebs, eq-entry(m, lref) ' + q1) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum0) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum0)) ∧ ubi-io-inv(apebs) ∧ wlar[m].status ≠ used ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(wlar, wlar0, m) ∧ id○(apebs, apebs0, m) ∧ id(apebs, apebs0, mapped-pebs(vols)) → ⟪vtblpnum := m; q0 := eq-entry(m, lref) ' + q1; q := eq-entry(m, lref) ' + q1; if err = ESUCCESS then {q := q.tail; if wlar[vtblpnum].status ≠ free then err := ENOSPC} else err := ENOSPC⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err ≠ ESUCCESS → # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum0) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum0)) ∧ q.lebrefs ⊆ q0.lebrefs ∧ ( err = ESUCCESS → vtblpnum < # apebs ∧ wlar[vtblpnum].status = free ∧ ( apebs0 = apebs ∧ wlar0 = wlar ∧ q0 = q ∨ id○(apebs0, apebs, vtblpnum) ∧ id○(wlar0, wlar, vtblpnum) ∧ q0 ≠ [] ∧ q0 = eq-entry(vtblpnum, q0.head.lebref) ' + q) ∧ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum0) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum0))))

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%⊦ 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)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]% ⊦ [] + q = q; (s)