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