[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,
exputinprovedall subs proved put-neq, In-insert, exin,
put-size-inc-inprovedall subs proved Size-insert, size-in,
size-neqprovedall subs proved Size-insert, size-in,
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,
k-Del-rec1provedall subs proved k-Extension, notin-del-notin, Del-rec-same,
subset-put-03provedall subs proved subset-put-04,
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,
delete-put-rewprovedall subs proved Del-at-strong, lookupisempty, Del-notin, in-neq, At-other, In-insert, At-same, Del-at, Del-in, Extension,
exnotemptyprovedall subs proved notmemlookup, Del-in, ins-same-01, del-put, In-empty, Extension, neq,
k-Del-rec2provedall subs proved In-insert, At-same, Del-at-strong, Del-in, lookupisempty, At-other, Del-notin, in-neq, Extension,
subset-delete-02provedall subs proved subset-delete-01,
subset-newprovedall subs proved subset-put-01,
sw-01provedall subs proved Del-in, Del-at, lookupisempty, Extension,
subset-put-02provedall subs proved At-other, in-neq, Del-in, Del-at-strong, 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-in, At-other, Del-at-strong, in-neq, In-insert, At-same, Extension,
Del-other-dataprovedall subs proved Del-in, notmemlookup,
eq-shift-delprovedall subs proved notmemlookup, At-other, in-neq, Del-at, Del-in, In-insert, At-same, k-Extension,
inj-put-01provedall subs proved ins-same-01, In-insert, ins, At-other, At-same, Extension,
subset-deleteprovedall subs proved superset-elem-in-01, subset-elem-eq-02, Del-at, Del-in, Subset,
subset-putprovedall subs proved Del-in, Del-at-strong, At-other, in-neq, In-insert, Del-notin, At-same, Subset,
subset-put-strongprovedall subs proved subset-put-strong-03,
subset-put-strong-01provedall subs proved subset-put-strong-04,
subset-put-strong-02provedall subs proved subset-put-strong-05,
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,
del-existsprovedall subs proved in-neq, Extension, At-other, inj-put, insins, At-same, In-insert, In-empty, gen,
eq-put-distinct-rewprovedall subs proved rew,
ins4provedall subs proved ins3, insins, rew,
put-neq-01provedall subs proved inj-put,
put-sameprovedall subs proved insins,
superset-elem-eqprovedall subs proved subset-elem-eq-02,
subset-empty-01provedall subs proved notmemlookup, Extension, subset-empty, In-empty, Subset,
subset-elem-eq-02provedall subs proved subset-elem-eq-01,
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,
rewprovedall subs proved In-insert, At-same, At-other, in-neq, 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,
At-in-outprovedall subs proved At-other, notmemlookup, At-same,
eq-put2provedall subs proved put-neq,
eq-shift-putprovedall subs proved in-neq, At-other, In-insert, At-same, notmemlookup, Extension,
ext-recprovedall subs proved notmemlookup, Extension, In-insert, At-other, in-neq, At-same,
in-oneprovedall subs proved In-insert, In-empty, in-neq,
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,
neqprovedall subs proved In-insert, At-same, In-empty, Extension,
put-neqprovedall subs proved At-same, 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,
At-other-numprovedall subs proved At-other,
indefprovedall subs proved At-other, At-same, In-insert, Extension,
insinprovedall subs proved In-insert,
k-At-sameprovedall subs proved At-same,
sub-transprovedall subs proved Subset,
subset-elem-eqprovedall subs proved Subset,
superset-elem-inprovedall subs proved Subset,
Subsetaxiom
Size-emptyaxiom
Size-insertaxiom
Extensionaxiom
In-emptyaxiom
In-insertaxiom
genaxiom
Del-emptyaxiom
Del-rec-otheraxiom
Del-rec-sameaxiom
At-sameaxiom
At-otheraxiom