[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,

Lemma dependency for Specification ubi-abs

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
absf-atprovedall subs proved absf-size, absf-rec, absf-base,
absf-sizeprovedall subs proved absf-rec, absf-base,
absexpt-vols-writeprovedall subs proved absexpt-def,
absexpt-vols-absprovedall subs proved abs-def, absexpt-v-def,
absexpt-v-vols-writeprovedall subs proved absexpt-v-def,
absexpt-pebs-writeprovedall subs proved absexpt-def,
absexpt-mapped-absprovedall subs proved abs-def, absexpt-def,
absexpt-idsetprovedall subs proved absexpt-def, abs-def,
absexpt-id-apebs-usedprovedall subs proved absexpt-def,
absexpt-avols-writeprovedall subs proved absexpt-def,
abs-vols-unmappedprovedall subs proved abs-def,
abs-vols-sizeprovedall subs proved abs-def,
abs-vols-mappedprovedall subs proved abs-def,
abs-vols-inprovedall subs proved abs-def,
abs-unmap-twiceprovedall subs proved abs-def,
abs-unmapprovedall subs proved abs-def,
abs-queue-subsetprovedall subs proved abs-def,
abs-queue-notinprovedall subs proved abs-def,
abs-lebrefs-subset-noterased-someprovedall subs proved abs-def,
abs-lebrefs-subsetprovedall subs proved abs-def,
abs-idset-fwdprovedall subs proved abs-def,
abs-id-apebs-usedprovedall subs proved abs-def,
abs-erase-emptyqprovedall subs proved abs-def,
abs-eraseprovedall subs proved abs-def,
abs-avols-sizeprovedall subs proved abs-def,
abs-avols-inprovedall subs proved abs-def,
abs-absexpt-vprovedall subs proved absexpt-v-def, abs-def,
abs-absexptprovedall subs proved absexpt-def, abs-def,
absf-baseaxiom
absf-recaxiom
absexpt-v-defaxiom
abs-defaxiom
absexpt-defaxiom