| # wlar = # apebs, avhdr0.vol × avhdr0.leb ∈ recs ∧ m11 = m5 ↔ stat0 = used ∧ m5 < m, wlar[m, wl-entry(m3, used)][m5] = wl-entry(m10, used), recs[v × n, recovery-entry(m, m0)][avhdr0.vol × avhdr0.leb] = recovery-entry(m7, m8), apebs[m] = mkpeb(aehdr, avidhdr(v, n, m0, m1, m4), buf, m2, boolvar), apebs[m5] = mkpeb(aehdr1, avhdr0, buf1, m13, boolvar1), recs[avhdr0.vol × avhdr0.leb] = recovery-entry(m11, m12), wlar[m5] = wl-entry(m14, stat0), m5 < # apebs, m < # apebs, m5 ≤ m ⊦ v × n ∈ recs, avhdr0.vol × avhdr0.leb ∈ recs[v × n, recovery-entry(m, m0)] ∧ m7 = m5 |
Used simplifier rules: ⊦ m ≠ n → wlar[n, wle][m] = wlar[m]; (s)% ⊦ m ≠ n → (m ≤ n ↔ m < n); (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic% ⊦ wl-entry(m, stat) = wl-entry(m0, stat0) ↔ m = m0 ∧ stat = stat0; (ws)% ⊦ ladr ∈ recs ∧ ¬ ladr0 ∈ recs → recs[ladr0, rec][ladr] = recs[ladr]; (s)% ⊦ m < n → n ≠ 0; (s)% ⊦ m +1 = m + 1; (s)% ⊦ ladr ∈ recs[ladr0, rec] ↔ ladr = ladr0 ∨ ladr ∈ recs; (ws)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic% ⊦ recovery-entry(m, m0) = recovery-entry(m1, m2) ↔ m = m1 ∧ m0 = m2; (ws)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)%m < # wlar ⊦ wlar[m, wle][m] = wle; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m ≤ m; (s)%⊦ mkpeb(aehdr, avhdr, buf, m, boolvar) = mkpeb(aehdr0, avhdr0, buf0, m0, boolvar0) ↔ aehdr = aehdr0 ∧ avhdr = avhdr0 ∧ buf = buf0 ∧ m = m0 ∧ (boolvar ↔ boolvar0); (s)% ⊦ avidhdr(v, m, m0, m1, m2).vol = v; (s)% ⊦ avidhdr(v, m, m0, m1, m2).leb = m; (s)% ⊦ ¬ ladr ∈ recs → recs[ladr] = (∅)[ladr]; (s)% ⊦ recs[ladr, rec][ladr] = rec; (s)% ⊦ ladr ∈ recs[ladr, rec]; (s) Used formulas: m5 = m