[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 ablock-store-refsize-cons

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:
refsize-cons-allocprovedall subs proved restrict-add-other, size-emp, size-rec-rem, restrict-add, refsize-cons-def,
size-rec-remprovedall subs proved size-rec, size-rem,
size-eq-0-allocprovedall subs proved subseteq-dom-nodes-alloc-restrict-empty, size-eq-0,
restrict-union-inter-empty-leftprovedall subs proved restrict-in, restrict-leb,
restrict-unionprovedall subs proved restrict-in, restrict-leb,
remove-refsize0-subset-refedprovedall subs proved restrict-in, size-eq-0, refsize-cons-def, valid-adrs,
remove-refsize0-refsize-consprovedall subs proved restrict-in, size-eq-0, refsize-cons-def,
refsize-cons-remove-index-0provedall subs proved restrict-del-other, restrict-in, size-rem, restrict-del, refsize-cons-def,
refsize-cons-remove-indexprovedall subs proved restrict-del-other, restrict-in, size-rem, restrict-del, refsize-cons-def,
refsize-cons-appendprovedall subs proved restrict-add-other, restrict-in, size-rec, restrict-add, refsize-cons-def,
in-remove-refsize0-refsize-consprovedall subs proved restrict-in, size-eq-0, refsize-cons-def,
subseteq-dom-nodes-alloc-restrict-emptyprovedall subs proved restrict-leb,
restrict-delprovedall subs proved restrict-leb,
size-remprovedall subs proved size-rec,
restrict-del-otherprovedall subs proved restrict-leb,
restrict-addprovedall subs proved restrict-leb,
restrict-add-otherprovedall subs proved restrict-leb,
size-eq-0provedall subs proved size-rec, size-emp,
restrict-inprovedall subs proved restrict-leb,
size-rec-simpprovedall subs proved size-rec,
restrict-emptyprovedall subs proved restrict-leb,
refsize-cons-writeprovedall subs proved refsize-cons-def,
refsize-cons-remove-refsize0provedall subs proved refsize-cons-def,
refsize-cons-emtpyprovedall subs proved refsize-cons-def,
refsize-cons-deallocprovedall subs proved refsize-cons-def,
inv-valid-adrsprovedall subs proved valid-adrs,
restrict-lebaxiom
size-recaxiom
size-empaxiom
valid-adrsaxiom
refsize-cons-defaxiom