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