| # vols[v0] = # avols[v0], apebs[vols[v0][m1].pnum] = mkpeb(aehdr0, avhdr0, buf0, m3, boolvar0), vols[v][m] = ⌜n⌝ , avols[v][m] = mapped(buf, m0), apebs[n] = mkpeb(aehdr, avhdr, buf, m2, boolvar), m1 < # avols[v0], m < # vols[v], v0 ∈ avols, v0 ∈ vols, v ∈ vols, m2 ≤ m0, ∀ m1. (v0 ≠ v ∨ m1 ≠ m) ∧ m1 < # avols[v0] → (vols[v0][m1] = unmapped → ¬ avols[v0][m1].mapped?) ∧ ( vols[v0][m1] ≠ unmapped → avols[v0][m1].mapped? ∧ avols[v0][m1].data = apebs[vols[v0][m1].pnum].data ∧ apebs[vols[v0][m1].pnum].fill ≤ avols[v0][m1].fill) ∧ (avols[v0][m1] = erased → ¬ v0 × m1 ∈ q), ∀ v1. (v1 ∈ vols ↔ v1 ∈ avols) ∧ ( v1 ∈ vols → # vols[v1] = # avols[v1] ∧ (∀ m1. (v1 ≠ v ∨ m1 ≠ m) ∧ m1 < # vols[v1] → (vols[v1][m1] = unmapped → ¬ avols[v1][m1].mapped?) ∧ ( vols[v1][m1] ≠ unmapped → avols[v1][m1].mapped? ∧ avols[v1][m1].data = apebs[vols[v1][m1].pnum].data ∧ apebs[vols[v1][m1].pnum].fill ≤ avols[v1][m1].fill) ∧ (avols[v1][m1] = erased → ¬ v1 × m1 ∈ q))) ⊦ (vols[v0][m1] = unmapped → ¬ avols[v0][m1].mapped?) ∧ (vols[v0][m1] ≠ unmapped → avols[v0][m1].mapped? ∧ avols[v0][m1].data = buf0 ∧ m3 ≤ avols[v0][m1].fill) ∧ (avols[v0][m1] = erased → ¬ v0 × m1 ∈ q) |
Used simplifier rules: ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).fill = m; (s)%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic% ⊦ ⌜m⌝ .pnum = m; (s)% ⊦ m < n → n ≠ 0; (s)% ⊦ unmapped ≠ ⌜m⌝ ; (s)% ⊦ mapped(buf, m).mapped?; (s)% ⊦ mapped(buf, m).data = buf; (s)% ⊦ mapped(buf, m).fill = m; (s)% ⊦ erased ≠ mapped(buf, 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) Used terms: m1