[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 set-basic

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:
sub-size-eqprovedall subs proved sizesubl, ne-02, ne-01, sub-in, Extension,
sizesublprovedall subs proved sub-size, sub-insert, Size-insert, indef, ne-02, ne-01,
subsize-eq-01provedall subs proved subsize-eq, sub-idem,
subset-insert-02provedall subs proved in, Subset, subset-insert, add, ins-two, eq, ne-02, ne-01, sub-insert, addthree, addtwo, subset-insert-01, add-01, rax,
sub-sizeneqexprovedall subs proved sub-size, size-exgr,
sub-oneprovedall subs proved sub-one-01, size-one-03, size-zero, size-zero-01, sub-idem,
sizesubprovedall subs proved sub-size,
size-two-05provedall subs proved size-two, in-04, rax,
subsize-eqprovedall subs proved size-exgr, rax, Size-insert, indef, Subset, ne-02, ne-01, sub-in, Extension,
subset-insert-01provedall subs proved in, Subset, add, ins-two, eq, ne-02, ne-01, sub-insert, addthree, addtwo, subset-insert, add-01, rax,
size-one-03provedall subs proved size-one, size-one-01,
sub-sizeprovedall subs proved sub-in, ne-02, size-exgr, size-zero,
size-twoprovedall subs proved in-04, size-one-01, one-size, size-one, Size-insert, indef, ne-02, ne-01, selsize, size-two-01,
size-two-04provedall subs proved in-04, size-one-01, size-exgr, ne-02, ne-01,
size-three-02provedall subs proved size-two-01, eq, size-zero, size-zero-02, rax, in-04, ne, size-one-01, one-in, size-one-02, in-02, add, Size-insert, indef, ne-02, ne-01, selsize,
size-threeprovedall subs proved add, Size-insert, in-04, eq, ne, size-exgr, size-one-01, two-01, ne-02, selsize, size-zero,
subset-insertprovedall subs proved in, Subset, add, sub-idem, sub-add-01, ins-two, eq, ne-02, ne-01, sub-insert, addtwo, subset, add-01, rax,
one-inprovedall subs proved ne-01, size-one-02, in-04, Extension,
size-exgrprovedall subs proved add, in-02, indef, ne-01, eq, ne-02, rax, Size-insert, eq-03, ne, size-zero-01, size-zero, In-empty, Size-empty, gen,
size-oneprovedall subs proved alle, Size-empty, size-zero-02, rax, Size-insert, indef, ne-02, ne-01, size-one-02, In-empty, sel, in-04, Extension,
size-two-03provedall subs proved add, eq-03, size-zero-01, Size-insert, ne-02, ne-01, eq, ne, size-zero, rax, Size-empty, gen,
eq-02provedall subs proved size-zero-01, ne-02, size-zero-02, in-05, Size-insert, one-size,
subsetprovedall subs proved sub-insert, add, ins-two, sub-add-01, add-01, rax,
size-two-01provedall subs proved Size-insert, in-04, eq, size-one-01, add-01,
size-one-02provedall subs proved In-empty, size-zero-02, Size-insert, eq, rax, Size-empty, gen, ne-02, ne-01,
size-zero-01provedall subs proved size-zero-02,
subset-insert-sameprovedall subs proved rax, sub-add-03, sub-add-02,
subset-insprovedall subs proved rax, sub-add-03, sub-add-02,
sub-twoprovedall subs proved sub-add-03, in-04, sub-one-02, add-01,
size-two-06provedall subs proved size-zero-02, Size-insert, size-less-01, rax, In-empty, Size-empty, gen, ne-02, ne-01,
size-two-02provedall subs proved Size-insert, add-01, in-04, size-one-01, eq, ne, size-zero,
size-three-01provedall subs proved size-zero-02, add, in-02, Size-insert, indef, ne-02, ne-01,
addthreeprovedall subs proved rax, add, eq-03,
sub-add-02provedall subs proved sub-add-03,
ins-twoprovedall subs proved in, eq-03,
sub-one-02provedall subs proved sub-e, sub-add-03,
sub-insertprovedall subs proved ne-02, ne-01, rax, Subset, sub-idem, eq, sub-ntrans, sub-insert-01,
add-01provedall subs proved add, eq-03,
indefprovedall subs proved del, ne-02, ne-01, in-03,
one-sizeprovedall subs proved size-one-01,
size-zero-02provedall subs proved Size-insert, eq, size-zero, size-one-01, ne, gen,
eqtwo-01provedall subs proved two,
sub-one-01provedall subs proved ne-02, ne-01, In-empty, Extension, in-04, Subset,
sub-insert-01provedall subs proved sub-add-01, sub-ntrans,
sub-add-03provedall subs proved ne-02, ne-01, sub-add, rax, Subset,
size-less-01provedall subs proved Size-insert, eq, ne-02, size-zero,
two-01provedall subs proved ne-02, ne-01, in-04, Extension,
size-one-01provedall subs proved Size-insert, In-empty, Size-empty, eq,
delprovedall subs proved in-02, eq-04, add, eq-01, in-03, eq, rax, In-empty, gen, ne-02, ne-01,
twoprovedall subs proved eq-04, in-04, rax, Extension,
eq-03provedall subs proved eq, in, in-03, Extension,
swprovedall subs proved eq-04,
size-lessprovedall subs proved Size-insert, eq, ne, size-zero,
size-insprovedall subs proved Size-insert, eq,
oneprovedall subs proved ne-02, ne-01, In-empty, in-04, Extension,
in-06provedall subs proved in-04,
eqtwoprovedall subs proved in-04, eq, in-05,
eq-06provedall subs proved eq-04,
eq-05provedall subs proved eq-04,
addtwoprovedall subs proved in-02, rax, Extension,
sub-add-01provedall subs proved rax, Subset,
sub-ntransprovedall subs proved sub-ntrans-01, sub-trans,
sub-addprovedall subs proved rax, Subset,
neprovedall subs proved rax, In-empty, Extension,
in-04provedall subs proved rax, In-empty, in-02,
in-05provedall subs proved rax, Extension,
eqprovedall subs proved in, in-03, Extension,
eq-01provedall subs proved rax, Extension,
eq-04provedall subs proved rax, Extension,
sw-01provedall subs proved rax, Extension,
subset-insert-06provedall subs proved in, rax, add, Subset,
subset-insert-05provedall subs proved in, rax, add, Subset,
subset-insert-04provedall subs proved in, rax, add, Subset,
subset-insert-03provedall subs proved in, rax, add, Subset,
sub-add-04provedall subs proved ne-02, ne-01, rax, Subset,
ext-recprovedall subs proved rax, Extension,
sub-ntrans-01provedall subs proved sub-trans,
in-03provedall subs proved in-01, in-02,
raxprovedall subs proved add, in-02,
eq-subsetprovedall subs proved sub-idem, subset-equal,
sub-inprovedall subs proved ne-02, ne-01, Subset,
sub-transprovedall subs proved ne-02, ne-01, Subset,
selprovedall subs proved ne-02, ne-01, In-empty, Extension,
alleprovedall subs proved ne-02, ne-01, In-empty, Extension,
subset-equalprovedall subs proved ne-02, ne-01, Extension, Subset,
in-02provedall subs proved in, In-insert,
selsizeprovedall subs proved In-empty, Extension, size-zero,
in-01provedall subs proved add,
inprovedall subs proved add,
ne-02provedall subs proved ne-01,
sub-eprovedall subs proved In-empty, Subset,
size-zeroprovedall subs proved Size-empty,
sub-idemprovedall subs proved Subset,
ne-01provedall subs proved In-empty,
addprovedall subs proved In-insert,
subset-emptyprovedall subs proved Extension, In-empty, Subset,
size-zero-03provedall subs proved Size-empty,
Subsetaxiom
Size-emptyaxiom
Size-insertaxiom
genaxiom
In-emptyaxiom
Extensionaxiom
In-insertaxiom