| # apebs = # wlar, apebs[m] = mkpeb(aehdr, avhdr, buf, m2, boolvar), valid-sqns(v, n, apebs, m) = ∅, m < # wlar, valid-peb(v, n, mkpeb(aehdr, avhdr, buf, m2, boolvar)), ∀ n0. ¬ m < n0 → (wlar[m, wl-entry(m0, used)][n0].status = erroneous ↔ apebs[n0].bad) ∧ (wlar[m, wl-entry(m0, used)][n0].status = free → apebs[n0].vidhdr = empty) ∧ ( wlar[m, wl-entry(m0, used)][n0].status ≠ erroneous ∧ wlar[m, wl-entry(m0, used)][n0].status ≠ erasing → apebs[n0].echdr = aechdr(wlar[m, wl-entry(m0, used)][n0].ec)) ∧ ( wlar[m, wl-entry(m0, used)][n0].status = used → (∃ v0, m1. valid-peb(v0, m1, apebs[n0]) ∧ apebs[n0].vidhdr.sqn = (valid-sqns(v0, m1, apebs, m) ∪ (v = v0 ∧ n = m1 ⊃ {avhdr.sqn} ;∅)).max)), ∀ n0. n0 < m → (wlar[n0].status = erroneous ↔ apebs[n0].bad) ∧ (wlar[n0].status = free → apebs[n0].vidhdr = empty) ∧ (wlar[n0].status ≠ erroneous ∧ wlar[n0].status ≠ erasing → apebs[n0].echdr = aechdr(wlar[n0].ec)) ∧ (wlar[n0].status = used → (∃ v0, m1. valid-peb(v0, m1, apebs[n0]) ∧ apebs[n0].vidhdr.sqn = valid-sqns(v0, m1, apebs, m).max)) ⊦ aehdr.ec = m0 |
Used simplifier rules: ⊦ ¬ n < n; (s)% ⊦ m < # wlar → wlar[m, wle][m] = wle; (s)% ⊦ wl-entry(m, stat).status = stat; (s)% ⊦ used ≠ erroneous; (s)% ⊦ used ≠ free; (s)% ⊦ used ≠ erasing; (s)% ⊦ wl-entry(m, stat).ec = m; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr; (s)%⊦ valid-peb(v0, m0, apeb) → (valid-peb(v1, m1, apeb) ↔ v0 = v1 ∧ m0 = m1); (s)% ⊦ bag ∪ {n} = bag ++ n; (s)%union-ass: ⊦ bag ∪ bag3 ∪ bag4 = (bag ∪ bag3) ∪ bag4; from specification bag-union[nat-bag]%union-com: ⊦ bag ∪ bag2 = bag2 ∪ bag; from specification bag-union[nat-bag]% ⊦ m = (bag ++ m).max ↔ ¬(bag ≠ ∅ ∧ m < bag.max); (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad ↔ boolvar; (s)% ⊦ aechdr(m).ec = m; (s) Used terms: m