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

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