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