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