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

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:
Data-notin-other-3provedall subs proved Data-notin-other, Data-notin-other-2,
Data-notin-other-2provedall subs proved Data-notin-other,
Data-notin-otherprovedall subs proved In-data-in, in-neq, At-same, At-other, Data-in,
Data-in-putdelputprovedall subs proved In-data-in, Del-at, Del-in, in-neq, At-other, At-same, Data-in,
Data-in-putdelprovedall subs proved In-data-in, Del-at, Del-in, in-neq, At-other, At-same, Data-in,
Data-in-delput-2provedall subs proved In-data-in, in-neq, At-other, At-same, Del-at, Del-in, Data-in,
Data-in-delputprovedall subs proved In-data-in, in-neq, At-other, At-same, Del-at, Del-in, Data-in,
Data-in-delprovedall subs proved In-data-in, Del-at, Del-in, Data-in,
In-data-inprovedall subs proved Data-in-putsame, At-same, exin,
inexprovedall subs proved At-same, In-insert, exin, Extension,
exputinprovedall subs proved put-neq-01, In-insert, exin,
exinprovedall subs proved In-insert, del-exists,
sw-01provedall subs proved Del-in, deldel, lookupisempty, Del-at, Extension,
deldelprovedall subs proved lookupisempty, Del-in, del-notin, Del-at, Extension,
del-existsprovedall subs proved rew, insins, In-insert, At-same, At-other, In-empty,
swprovedall subs proved delete-put-rew,
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,
emptyprovedall subs proved In-insert, At-same, Size-empty, notmemlookup, Del-in, del-put, Size-insert, indef, In-empty, Extension,
dom-isempprovedall subs proved dom-ins, exnotempty, dom-emp,
del-emptyprovedall subs proved In-empty, del-notin,
delete-put-rewprovedall subs proved lookupisempty, At-other, in-neq, In-insert, Del-at, At-same, Del-in, Extension,
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,
indefprovedall subs proved At-other, in-neq, At-same, In-insert, Extension, del-put,
exnotemptyprovedall subs proved Del-in, ins-same, del-put, notmemlookup, In-empty, Extension, neq,
rewprovedall subs proved In-insert, At-other, At-same, in-neq, k-Extension,
del-notinprovedall subs proved Del-at, Del-in, k-Extension,
subset-put-01provedall subs proved At-other, ins-same, In-insert, Subset,
subset-putprovedall subs proved At-other, ins-same, In-insert, Subset,
put-sameprovedall subs proved Extension, insins,
insertprovedall subs proved At-other, in-neq, Del-in, lookupisempty, Del-at, Extension,
ins-same-01provedall subs proved In-insert, ins-same, Extension,
inj-put-01provedall subs proved put-neq,
inj-putprovedall subs proved ins, At-same, At-other, In-insert, ins-same, Extension,
eq-shift-putprovedall subs proved At-other, in-neq, Extension, In-insert, At-same, ins-same, insins,
del-putsameprovedall subs proved At-other, in-neq, At-same, In-insert, Extension, del-put,
subset-elem-eq-02provedall subs proved subset-elem-eq-01,
put-neqprovedall subs proved notmemlookup, In-insert, At-same, At-other, Extension,
insprovedall subs proved At-other, in-neq, At-same, In-insert, Extension,
ins-sameprovedall subs proved At-other, in-neq, At-same, In-insert, Extension,
lookupisemptyprovedall subs proved Del-in, notmemlookup,
del-putprovedall subs proved Del-at, At-other, in-neq, Del-in, In-insert, At-same, Extension,
k-Extensionprovedall subs proved notmemlookup, Extension,
insinsprovedall subs proved At-other, in-neq, In-insert, At-same, Extension,
superset-elem-eqprovedall subs proved subset-elem-eq-01,
subset-empty-01provedall subs proved notmemlookup, Extension, In-empty, Subset,
subset-deleteprovedall subs proved subset-delete-01,
ins3provedall subs proved At-other, in-neq, In-insert, At-same, Extension,
indef-01provedall subs proved At-other, in-neq, At-same, In-insert, Extension,
Data-in-puteqprovedall subs proved Data-in-putsame,
superset-elem-in-01provedall subs proved Subset,
subset-elem-eq-01provedall subs proved Subset,
subset-delete-01provedall subs proved Del-at, Del-in, Subset,
put-neq-01provedall subs proved At-same, Extension,
neqprovedall subs proved In-insert, At-same, In-empty, Extension,
notmemlookupprovedall subs proved At-other, In-insert,
dom-empprovedall subs proved In-empty, Dom,
dom-insprovedall subs proved In-insert, Dom,
Data-in-putsameprovedall subs proved In-insert, At-same, Data-in,
in-neqprovedall subs proved In-insert,
superset-elem-inprovedall subs proved Subset,
subset-emptyprovedall subs proved In-empty, Subset,
subset-elem-eqprovedall subs proved Subset,
subset-delete-02provedall subs proved Del-at, Del-in, Subset,
sub-transprovedall subs proved Subset,
sub-refprovedall subs proved Subset,
notin-empprovedall subs proved In-empty, Extension,
insinprovedall subs proved In-insert,
in-notempprovedall subs proved In-empty,
dom-delprovedall subs proved Del-in, Dom,
At-other-strongprovedall subs proved At-other,
At-other-numprovedall subs proved At-other,
At-in-outprovedall subs proved At-other, At-same,
Subsetaxiom
Size-insertaxiom
Size-emptyaxiom
Domaxiom
Extensionaxiom
In-emptyaxiom
In-insertaxiom
Data-inaxiom
Del-inaxiom
Del-ataxiom
At-sameaxiom
At-otheraxiom