[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, empty-01, size, notin-del-notin, Size-insert, subset-elem-eq-01, subset-put-01, in-pair, subset-put-02, ins, size-in, empty, Size-empty, subset-empty, gen-04,
key-sizeprovedall subs proved Del-in, size, Size-insert, size-in, In-insert, In-empty, empty, Size-empty, gen-04,
emptyprovedall subs proved Size-insert, In-empty, size-in, gen-04, 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, insert, 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,
inexprovedall subs proved Del-notin, ins-same-01, del-put,
inj-put-01provedall subs proved In-insert, notmemlookup, ins, At-same, At-other, in-neq, Extension, ins-same-01,
exnotemptyprovedall subs proved Del-notin, ins-same-01, del-put, notmemlookup, In-empty, Extension, neq,
del-putsameprovedall subs proved ins-same-01, del-put,
deldelprovedall subs proved Del-at, lookupisempty, notin-del-notin, Del-notin, Del-in, Extension,
ins-same-01provedall subs proved ins-same,
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-put-03provedall subs proved subset-put-04,
rem-eqprovedall subs proved Del-at-strong, Del-notin, Extension, notin-del-notin,
k-Del-rec1provedall subs proved notin-del-notin, insert,
subset-put-strong-05provedall subs proved subset-elem-eq-02, At-other, At-same, superset-elem-in-01, in-neq, In-insert, Subset,
subset-put-strong-04provedall subs proved subset-elem-eq-02, At-other, At-same, superset-elem-in-01, in-neq, In-insert, Subset,
subset-put-strong-03provedall subs proved subset-elem-eq-02, At-other, At-same, superset-elem-in-01, in-neq, In-insert, Subset,
subset-put-04provedall subs proved In-store, Subset, subset-put-01,
insertprovedall subs proved At-other, Del-at-strong, in-neq, Del-in, lookupisempty, Del-notin, Extension,
ins-sameprovedall subs proved In-insert, At-same, Extension, notmemlookup, ins,
notin-del-notinprovedall subs proved Del-at, notmemlookup, lookupisempty, Del-notin, Del-in, Extension,
sw-01provedall subs proved Del-at-strong, Del-in, notmemlookup, lookupisempty, Del-notin, Extension,
swprovedall subs proved In-insert, At-same, Del-at-strong, Del-in, At-other, lookupisempty, in-neq, Del-notin, Extension,
superset-elem-eqprovedall subs proved subset-elem-eq-02,
subset-newprovedall subs proved in-pair, subset-put-01,
subset-elem-eqprovedall subs proved subset-elem-eq-02,
subset-delete-02provedall subs proved subset-delete-01,
subset-deleteprovedall subs proved superset-elem-in-01, subset-elem-eq-02, Del-at-strong, Del-in, Subset,
put-sameprovedall subs proved insins,
put-neq-01provedall subs proved inj-put,
k-Del-rec2provedall subs proved In-insert, At-same, Del-at, Del-in, At-other, lookupisempty, in-neq, Del-notin, Extension,
ins4provedall subs proved ins3, insins, rew,
eq-shift-delprovedall subs proved notmemlookup, At-other, in-neq, Del-at, Del-in, At-same, In-insert, k-Extension,
delete-put-rewprovedall subs proved lookupisempty, Del-notin, At-other, in-neq, In-insert, Del-at, At-same, Del-in, Extension,
del-existsprovedall subs proved in-neq, Extension, At-other, inj-put, insins, At-same, In-insert, In-empty, gen-04,
subset-put-02provedall subs proved At-other, in-neq, In-insert, At-same, in-pair, Del-at-strong, Del-in, Subset,
empty-01provedall subs proved Del-in, notmemlookup, In-empty, Extension,
subset-empty-01provedall subs proved notmemlookup, Extension, subset-empty, In-empty, Subset,
subset-put-01provedall subs proved In-insert, At-other, in-neq, At-same, Del-at-strong, Del-in, in-pair, Subset,
subset-delete-01provedall subs proved Del-at-strong, Del-in, 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,
insprovedall subs proved At-other, in-neq, At-same, In-insert, Extension,
neqprovedall subs proved In-insert, notmemlookup, In-empty, Extension,
k-Extensionprovedall subs proved notmemlookup, Extension,
lookupisemptyprovedall subs proved Del-in, notmemlookup,
del-putprovedall subs proved Del-at, At-other, Del-in, in-neq, In-insert, At-same, Extension,
insinsprovedall subs proved At-other, in-neq, In-insert, At-same, Extension,
inj-putprovedall subs proved At-other, in-neq, notmemlookup, At-same, In-insert, Extension,
superset-elem-inprovedall subs proved superset-elem-in-01,
subset-putprovedall subs proved At-other, in-neq, In-insert, At-same, in-pair, Del-at-strong, Del-in, Subset,
ext-recprovedall subs proved notmemlookup, Extension, In-insert, At-other, in-neq, At-same,
eq-shift-putprovedall subs proved At-other, in-neq, In-insert, At-same, notmemlookup, Extension,
Del-other-dataprovedall subs proved notmemlookup, Del-in,
At-in-outprovedall subs proved At-other, notmemlookup, At-same,
in-pairprovedall subs proved In-store,
subset-emptyprovedall subs proved In-empty, Subset,
subset-elem-eq-01provedall subs proved Subset,
superset-elem-in-01provedall subs proved Subset,
Del-at-strongprovedall subs proved Del-at,
put-neqprovedall subs proved At-same, Extension,
Del-notinprovedall subs proved Del-in,
in-neqprovedall subs proved In-insert,
notmemlookupprovedall subs proved At-other, In-insert, gen-04,
sub-transprovedall subs proved Subset,
sub-refprovedall 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
In-storeaxiom
Size-emptyaxiom
Size-insertaxiom
gen-04axiom
In-emptyaxiom
In-insertaxiom
Extensionaxiom
Del-inaxiom
Del-ataxiom
At-sameaxiom
At-otheraxiom