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