| apebs[n].data = buf, avols[v][m] = mapped(buf, m0), vols[v][m] = ⌜n⌝ , m < # vols[v], abs○(avols, apebs, vols, q, v, m), v ∈ vols, apebs[n].fill ≤ m0 ⊦ abs(avols, apebs, vols, q) |
avols[v][m] = mapped(apebs[n].data, m0), vols[v][m] = ⌜n⌝ , m < # vols[v], v ∈ vols, apebs[n].fill ≤ m0, ∀ 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))) ⊦ (v0 ∈ vols ↔ v0 ∈ avols) ∧ ( v0 ∈ vols → # vols[v0] = # avols[v0] ∧ ( m1 < # vols[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)))
Used simplifier rules: absexpt-def: ⊦ abs○(avols, apebs, vols, q, v0, m0) ↔ (∀ v. (v ∈ vols ↔ v ∈ avols) ∧ ( v ∈ vols → # vols[v] = # avols[v] ∧ (∀ m. (v ≠ v0 ∨ m ≠ m0) ∧ m < # vols[v] → (vols[v][m] = unmapped → ¬ avols[v][m].mapped?) ∧ ( vols[v][m] ≠ unmapped → avols[v][m].mapped? ∧ avols[v][m].data = apebs[vols[v][m].pnum].data ∧ apebs[vols[v][m].pnum].fill ≤ avols[v][m].fill) ∧ (avols[v][m] = erased → ¬ v × m ∈ q))));%abs-def: ⊦ abs(avols, apebs, vols, q) ↔ (∀ v. (v ∈ vols ↔ v ∈ avols) ∧ ( v ∈ vols → # vols[v] = # avols[v] ∧ (∀ m. m < # vols[v] → (vols[v][m] = unmapped → ¬ avols[v][m].mapped?) ∧ ( vols[v][m] ≠ unmapped → avols[v][m].mapped? ∧ avols[v][m].data = apebs[vols[v][m].pnum].data ∧ apebs[vols[v][m].pnum].fill ≤ avols[v][m].fill) ∧ (avols[v][m] = erased → ¬ v × m ∈ q))));% ⊦ m < n → n ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic