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

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