[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 infset-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:
swprovedall subs proved eq-04,
oneprovedall subs proved ne-02, ne-01, In-empty, Extension, in-04,
eqtwoprovedall subs proved in-04, In-insert, Extension,
two-01provedall subs proved ne-02, ne-01, in-04, Extension,
sub-one-01provedall subs proved ne-02, ne-01, in-04, Extension, In-empty, Subset,
eq-06provedall subs proved eq-04,
sub-twoprovedall subs proved in-04, sub-one-02, sub-add-03, add-01,
addtwoprovedall subs proved In-insert, eq-04, eq,
eqtwo-01provedall subs proved in-04, add, In-insert, In-empty, eq, Extension,
subsetprovedall subs proved Subset, sub-idem, eq, ne-02, ne-01, sub-add-01, sub-insert, add-01, In-insert,
eq-05provedall subs proved eq-04,
indefprovedall subs proved in-03, construct-set, In-insert, Extension,
eq-02provedall subs proved ne-02, ne-01, In-empty, Extension, in-04, In-insert,
twoprovedall subs proved eq-04, in-04, In-insert, Extension,
in-06provedall subs proved in-04,
in-03provedall subs proved add, in-02,
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,
in-04provedall subs proved add, In-empty, in-02,
eq-04provedall subs proved In-insert, ins-two, eq, Extension,
sub-insert-3provedall subs proved In-insert, Subset, sub-add-03,
subset-insert-sameprovedall subs proved In-insert, Subset, sub-add-03,
sub-insert-5provedall subs proved In-insert, Subset, sub-add-03,
subset-insprovedall subs proved In-insert, sub-add-03, sub-add-02,
sub-insert-01provedall subs proved sub-add-01, sub-ntrans,
sub-insert-4provedall subs proved In-insert, Subset, sub-add-03,
eq-subsetprovedall subs proved subset-equal, sub-idem,
ins-twoprovedall subs proved In-insert, eq-03,
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-add-02provedall subs proved ne-02, ne-01, Subset, In-insert,
add-01provedall subs proved In-insert, eq-03,
sub-add-03provedall subs proved ne-02, ne-01, Subset, sub-add, In-insert,
subset-insert-01provedall subs proved in, In-insert, Subset,
subset-insertprovedall subs proved in, In-insert, Subset,
subset-insert-03provedall subs proved in, In-insert, Subset,
subset-insert-06provedall subs proved in, In-insert, Subset,
sub-ntrans-01provedall subs proved ne-02, ne-01, Subset,
subset-insert-05provedall subs proved in, In-insert, Subset,
sub-add-04provedall subs proved ne-02, ne-01, In-insert, Subset,
subset-insert-02provedall subs proved in, In-insert, Subset,
sub-inprovedall subs proved ne-02, ne-01, Subset,
selprovedall subs proved ne-02, ne-01, In-empty, Extension,
subset-insert-04provedall subs proved in, In-insert, Subset,
sub-transprovedall subs proved ne-02, ne-01, Subset,
addthreeprovedall subs proved In-insert, eq-03,
ne-02provedall subs proved In-empty, Extension, ne-01,
eq-03provedall subs proved In-insert, Extension, eq,
inprovedall subs proved add,
in-01provedall subs proved add,
sub-eprovedall subs proved In-empty, Subset,
sub-addprovedall subs proved Subset, In-insert,
sub-idemprovedall subs proved Subset,
sub-add-01provedall subs proved In-insert, Subset,
addprovedall subs proved In-insert,
eqprovedall subs proved In-insert, Extension,
ne-01provedall subs proved In-empty,
ext-recprovedall subs proved In-insert, Extension,
in-05provedall subs proved In-insert, Extension,
subset-emptyprovedall subs proved In-empty, Extension, Subset,
sw-01provedall subs proved In-insert, Extension,
expandprovedall subs proved construct-set, Extension, gen,
neprovedall subs proved In-insert, In-empty, Extension,
delprovedall subs proved construct-set, In-insert, Extension,
alleprovedall subs proved In-empty, Extension,
eq-01provedall subs proved Extension, In-insert,
genaxiom
construct-setaxiom
In-emptyaxiom
Extensionaxiom
Subsetaxiom
In-insertaxiom