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

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:
size-subsetprovedall subs proved subset-size,
subset-sizeprovedall subs proved In-empty, subset-empty-01, Del-empty, size, notin-del-notin, Size-insert, subset-put-01, subset-put-02, ins, size-in, empty, Size-empty, subset-empty, gen,
key-sizeprovedall subs proved Del-in, size, Size-insert, size-in, In-insert, In-empty, empty, Size-empty, gen,
emptyprovedall subs proved Size-insert, In-empty, size-in, gen, Size-empty,
size-neqprovedall subs proved Size-insert, size-in,
exputinprovedall subs proved put-neq, In-insert, exin,
sizeprovedall subs proved Size-insert, Del-in, deldel, Del-rec-same, indef-01,
exinprovedall subs proved In-insert, inex,
size-inprovedall subs proved In-insert, Size-insert, Del-in, insins, indef-01,
indef-01provedall subs proved In-insert, At-same, notmemlookup, notin-del-notin, ins-same-01, del-put, Extension,
deldelprovedall subs proved Del-at-strong, Del-in, lookupisempty, Del-notin, notin-del-notin, Extension,
inexprovedall subs proved Del-in, del-putsame, Extension,
subset-put-03provedall subs proved subset-put-04,
k-Del-rec1provedall subs proved k-Extension, notin-del-notin, Del-rec-same,
subset-put-04provedall subs proved sub-ref, subset-put-01,
del-putsameprovedall subs proved ins-same-01, del-put,
notin-del-notinprovedall subs proved Del-at-strong, notmemlookup, lookupisempty, Del-notin, Del-in, Extension,
sw-01provedall subs proved Del-at, Del-in, lookupisempty, Extension,
subset-newprovedall subs proved subset-put-01,
subset-delete-02provedall subs proved subset-delete-01,
k-Del-rec2provedall subs proved In-insert, At-same, Del-at-strong, Del-in, At-other, lookupisempty, in-neq, Del-notin, Extension,
exnotemptyprovedall subs proved notmemlookup, Del-in, ins-same-01, del-put, In-empty, Extension, neq,
delete-put-rewprovedall subs proved Del-at-strong, lookupisempty, Del-notin, in-neq, At-other, In-insert, Del-at, At-same, Del-in, Extension,
subset-put-02provedall subs proved At-other, in-neq, Del-at-strong, Del-in, In-insert, Del-notin, At-same, Subset,
subset-put-01provedall subs proved Del-at-strong, In-insert, At-other, in-neq, Del-in, At-same, Subset,
subset-delete-01provedall subs proved Del-at, Del-in, Subset,
lookupisemptyprovedall subs proved Del-in, notmemlookup,
del-putprovedall subs proved Del-at-strong, At-other, Del-in, in-neq, In-insert, At-same, Extension,
subset-put-strong-02provedall subs proved subset-put-strong-05,
subset-put-strong-01provedall subs proved subset-put-strong-04,
subset-put-strongprovedall subs proved subset-put-strong-03,
subset-putprovedall subs proved Del-in, Del-at-strong, At-other, in-neq, In-insert, Del-notin, At-same, Subset,
subset-deleteprovedall subs proved superset-elem-in-01, subset-elem-eq-02, Del-at, Del-in, Subset,
inj-put-01provedall subs proved ins-same-01, ins, In-insert, At-same, At-other, Extension,
eq-shift-delprovedall subs proved notmemlookup, At-other, in-neq, Del-at, Del-in, At-same, In-insert, k-Extension,
Del-other-dataprovedall subs proved notmemlookup, Del-in,
subset-put-strong-05provedall subs proved subset-elem-eq-02, At-other, At-same, superset-elem-in-01, In-insert, Subset,
subset-put-strong-04provedall subs proved subset-elem-eq-02, At-other, At-same, superset-elem-in-01, In-insert, Subset,
subset-put-strong-03provedall subs proved superset-elem-in-01, subset-elem-eq-02, At-other, In-insert, At-same, Subset,
ins-same-01provedall subs proved ins-same,
Del-inprovedall subs proved In-insert, Del-notin, in-neq, Del-rec-same, Del-rec-other, In-empty, Del-empty, gen,
superset-elem-eqprovedall subs proved subset-elem-eq-02,
put-sameprovedall subs proved insins,
put-neq-01provedall subs proved inj-put,
ins4provedall subs proved ins3, insins, rew,
del-existsprovedall subs proved in-neq, Extension, At-other, inj-put, insins, At-same, In-insert, In-empty, gen,
subset-empty-01provedall subs proved notmemlookup, Extension, subset-empty, In-empty, Subset,
subset-elem-eq-02provedall subs proved subset-elem-eq-01,
rewprovedall subs proved In-insert, At-other, At-same, in-neq, Extension,
ins3provedall subs proved At-other, in-neq, In-insert, At-same, Extension,
ins-sameprovedall subs proved In-insert, At-same, Extension, notmemlookup, ins,
k-Extensionprovedall subs proved notmemlookup, Extension,
Del-at-strongprovedall subs proved Del-at,
insinsprovedall subs proved At-other, in-neq, In-insert, At-same, Extension,
inj-putprovedall subs proved At-other, notmemlookup, In-insert, At-same, Extension,
Del-notinprovedall subs proved in-neq, Del-rec-same, Del-rec-other, In-empty, Del-empty, gen,
ext-recprovedall subs proved notmemlookup, Extension, In-insert, At-other, in-neq, At-same,
eq-shift-putprovedall subs proved in-neq, At-other, In-insert, At-same, notmemlookup, Extension,
At-in-outprovedall subs proved At-other, notmemlookup, At-same,
sub-refprovedall subs proved Subset,
subset-emptyprovedall subs proved In-empty, Subset,
subset-elem-eq-01provedall subs proved Subset,
superset-elem-in-01provedall subs proved Subset,
insprovedall subs proved At-other, At-same, In-insert, Extension,
put-neqprovedall subs proved At-same, Extension,
neqprovedall subs proved In-insert, At-same, In-empty, Extension,
in-neqprovedall subs proved In-insert,
Del-atprovedall subs proved Del-rec-same, At-other, Del-rec-other, At-same, Del-empty, gen,
notmemlookupprovedall subs proved At-other, In-insert, gen,
superset-elem-inprovedall subs proved Subset,
subset-elem-eqprovedall subs proved Subset,
sub-transprovedall subs proved Subset,
k-At-sameprovedall subs proved At-same,
insinprovedall subs proved In-insert,
indefprovedall subs proved At-other, At-same, In-insert, Extension,
At-other-numprovedall subs proved At-other,
Subsetaxiom
Size-emptyaxiom
Size-insertaxiom
Extensionaxiom
In-emptyaxiom
In-insertaxiom
genaxiom
Del-emptyaxiom
Del-rec-otheraxiom
Del-rec-sameaxiom
At-sameaxiom
At-otheraxiom