| # apebs = # wlar, avhdr1.leb = VTBL_LNUM, avhdr2.leb = avhdr.leb, avhdr1.vol = VTBL_VOLID, avhdr2.vol = avhdr.vol, wlar[n0] = wl-entry(m8, used), wlar[m] = wl-entry(m7, used), apebs[n1] = mkpeb(aehdr3, avhdr3, buf3, m5, boolvar3), apebs[n, mkpeb(aehdr, avhdr, buf, m1, boolvar)][n1] = mkpeb(aehdr0, avhdr0, buf0, m2, boolvar0), vols[avhdr.vol][avhdr.leb] = unmapped, apebs[n0] = mkpeb(aehdr1, avhdr1, buf1, m3, boolvar1), apebs[m] = mkpeb(aehdr2, avhdr2, buf2, m4, boolvar2), wlar[n, wl-entry(aehdr.ec, used)][n1] = wl-entry(m6, stat), avhdr.leb < # vols[avhdr.vol], n < # wlar, n0 < # wlar, n1 < # wlar, m < # wlar, is-encoded(to-vtbl(vols), buf1), valid-peb(mkpeb(aehdr, avhdr, buf, m1, boolvar)), avhdr.vol ∈ vols, valid-sqns(avhdr.vol, avhdr.leb, apebs) ≠ ∅ → valid-sqns(avhdr.vol, avhdr.leb, apebs).max < avhdr.sqn, ∀ n. n < # wlar → (wlar[n].status = erroneous ↔ apebs[n].bad) ∧ (wlar[n].status = free → apebs[n].vidhdr = empty) ∧ (wlar[n].status ≠ erroneous ∧ wlar[n].status ≠ erasing → apebs[n].echdr = aechdr(wlar[n].ec)) ∧ (wlar[n].status = used → (∃ v, m. valid-peb(v, m, apebs[n]) ∧ apebs[n].vidhdr.sqn = valid-sqns(v, m, apebs).max)) ⊦ m = n, VTBL_VOLID ∈ vols, (stat = erroneous ↔ boolvar0) ∧ (stat = free → avhdr3 = empty) ∧ (stat ≠ erroneous ∧ stat ≠ erasing → aehdr0 = aechdr(m6)) ∧ ( stat = used → (∃ v, m0. valid-peb(v, m0, mkpeb(aehdr0, avhdr0, buf0, m2, false)) ∧ avhdr0.sqn = valid-sqns(v, m0, apebs[n, mkpeb(aehdr, avhdr, buf, m1, boolvar)]).max)), avhdr2.valid? ∧ m ≠ n0 |
Used simplifier rules: ⊦ wl-entry(m, stat).status = stat; (s)% ⊦ used ≠ erroneous; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad ↔ boolvar; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)%⊦ valid-peb(v, m, mkpeb(aehdr, avhdr, buf, m0, boolvar)) → avhdr.leb = m; (s)%⊦ valid-peb(v, m, mkpeb(aehdr, avhdr, buf, m0, boolvar)) → avhdr.vol = v; (s)% ⊦ used ≠ erasing; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr; (s)% ⊦ wl-entry(m, stat).ec = m; (s)% ⊦ used ≠ free; (s)%⊦ valid-peb(v, m, mkpeb(aehdr, avhdr, buf, m0, boolvar)) → avhdr.valid?; (ss)%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)%n < # apebs ⊦ apebs[n] = apeb ∧ valid-peb(v, m, apeb) → valid-sqns(v, m, apebs) ≠ ∅; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%⊦ mkpeb(aehdr, avhdr, buf, m, boolvar) = mkpeb(aehdr0, avhdr0, buf0, m0, boolvar0) ↔ aehdr = aehdr0 ∧ avhdr = avhdr0 ∧ buf = buf0 ∧ m = m0 ∧ (boolvar ↔ boolvar0); (s)% ⊦ wl-entry(m, stat) = wl-entry(m0, stat0) ↔ m = m0 ∧ stat = stat0; (ws)% ⊦ m < n → n ≠ 0; (s) Used terms: m