[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
enrich
ubi-base,
ebm-base
with
functions max-avols : apebs × volumes × queue → abstract-volumes;
max-avol : apebs × ebatbl × volid × queue → abstract-volume;
absf : abstract-volumes × apebs × volumes × queue → abstract-volumes;
absf : volid × abstract-volume × apebs × ebatbl × queue × nat → abstract-volume;
predicates abs : abstract-volumes × apebs × volumes × queue;
abs○ : abstract-volumes × apebs × volumes × queue × volid × nat;
abs○ : abstract-volumes × apebs × volumes × queue × volid;
abs : leb × apebs × ebaentry × queue;
axioms 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))));
used for: ls;
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))));
used for: ls;
absexpt-v-def
: ⊦ abs○(avols, apebs, vols, q, v0)
↔ (∀ v.
(v ∈ vols ↔ v ∈ avols)
∧ ( v ∈ vols
→ # vols[v] = # avols[v]
∧ ( v ≠ v0
→ (∀ 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)))));
used for: ls;
max-avols-in : ⊦ v ∈ max-avols(apebs, vols, q) ↔ v ∈ vols;
used for: s, ls;
max-avols-at : ⊦ v ∈ vols → max-avols(apebs, vols, q)[v] = max-avol(apebs, vols[v], v, q);
used for: s, ls;
max-avol-size : ⊦ # max-avol(apebs, ebatbl, v, q) = # ebatbl;
used for: s, ls;
max-avol-at
: ⊦ n < # ebatbl
→ max-avol(apebs, ebatbl, v, q)[n]
= (ebatbl[n] ≠ unmapped ⊃ mapped(apebs[ebatbl[n].pnum].data, apebs[ebatbl[n].pnum].fill);(v × n ∈ q ⊃ unmapped;erased));
used for: s, ls;
absfv-in : ⊦ v ∈ absf(avols, apebs, vols, q) ↔ v ∈ vols;
used for: ls;
absfv-at : ⊦ v ∈ vols → absf(avols, apebs, vols, q)[v] = absf(v, avols[v], apebs, vols[v], q, # vols[v]);
used for: ls;
absf-base : ⊦ absf(v, evol, apebs, ebatbl, q, 0) = mkabstractvolume(# ebatbl);
used for: ls;
absf-rec
: ⊦ n < # ebatbl
→ absf(v, evol, apebs, ebatbl, q, n + 1)
= absf(v, evol, apebs, ebatbl, q, n)
[n,
(ebatbl[n] = unmapped
⊃ (v × n ∈ q.lebrefs ⊃ unmapped;erased)
;mapped(apebs[ebatbl[n].pnum].data, (evol[n].mapped? ⊃ evol[n].fill;apebs[ebatbl[n].pnum].fill))
)
];
used for: ls;
end enrich