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

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:
butmin-put-02provedall subs proved butmin-put-01,
butmin-put-01provedall subs proved insert-03, min-def, min-put-01, Butmin,
butmin-rewputprovedall subs proved min-put, min-def, Min-in, min, Keys, inf, Min-min, Butmin,
butmin-put-rewprovedall subs proved min-def, Keys, inf, Min-min, Min-in, min-put-ls, Butmin,
butmin-oneprovedall subs proved min, Butmin,
butmin-putprovedall subs proved mk-in, min-def, min, Butmin,
min-put-01provedall subs proved insert-03, min-def,
min-put-lsprovedall subs proved empty-01, insert-03, min-def, Keys, inf, Min-min, Min-in,
minprovedall subs proved empty, insert-03, min-def,
min-putprovedall subs proved empty, Keys, inf, Min-min, notempty, insert-03, min-def,
butmin-idprovedall subs proved min-def, Min-in, Butmin,
min-inprovedall subs proved mk-in, min-def,
butmin-sizeprovedall subs proved min-def, Min-in, Butmin,
butmin-size-01provedall subs proved min-def, Min-in, Butmin,
butmin-inprovedall subs proved min-def, Butmin,
min-defprovedall subs proved mk-in, Keys, inf, Min-min, Min-in,
size-del-02provedall subs proved empty-02, del-01, Keys, inf, Min-min,
empty-02provedall subs proved notempty, inf, Min-min,
mk-inprovedall subs proved inkeys, empty-01, Keys, inf, Min-min, Min-in,
size-del-01provedall subs proved del-01,
size-delprovedall subs proved notempty, inkeys, Keys, inf, Min-min, del-01,
notemptyprovedall subs proved inkeys, Keys, inf, Min-min,
del-01provedall subs proved del, Keys, inf, Min-min,
empty-01provedall subs proved empty, Keys, inf, Min-min, Min-in,
insertprovedall subs proved inf, Min-min, Keys, insert-03,
inf-01provedall subs proved inf, Min-min, Keys,
k-keys-recprovedall subs proved insert-03,
neqprovedall subs proved Keys, insert-03,
delprovedall subs proved Keys,
inkeysprovedall subs proved Keys,
insert-03provedall subs proved Keys,
infprovedall subs proved Min-min, Keys,
emptyprovedall subs proved Keys,
butmin-notinprovedall subs proved Butmin,
butmin-emptyprovedall subs proved Butmin,
subprovedall subs proved Keys,
butmin-atprovedall subs proved Butmin,
inkeys-01provedall subs proved Keys,
Butminaxiom
Min-inaxiom
Min-minaxiom
Keysaxiom