[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:
subset-insprovedall subs proved rax, sub-add-03, sub-add-02,
subsetprovedall subs proved sub-insert, add, ins-two, sub-add-01, add-01, rax,
sub-twoprovedall subs proved sub-add-03, in-04, sub-one-02, add-01,
sub-add-02provedall subs proved sub-add-03,
ins-twoprovedall subs proved in, eq-03,
add-01provedall subs proved add, eq-03,
sub-one-02provedall subs proved sub-e, sub-add-03,
eqtwo-01provedall subs proved two,
addthreeprovedall subs proved rax, add, eq-03,
sub-add-03provedall subs proved ne-02, ne-01, sub-add, rax, Subset,
twoprovedall subs proved eq-04, in-04, rax, Extension,
eq-03provedall subs proved eq, in, in-03, Extension,
two-01provedall subs proved ne-02, ne-01, in-04, Extension,
swprovedall subs proved eq-04,
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,
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,
eq-02provedall subs proved ne-02, ne-01, In-empty, in-04, rax, Extension,
addtwoprovedall subs proved rax, add, eq-04, eq,
sub-insertprovedall subs proved rax, Subset,
sub-ntransprovedall subs proved sub-ntrans-01, sub-trans,
sub-add-01provedall subs proved rax, Subset,
sub-addprovedall subs proved rax, Subset,
in-05provedall subs proved rax, Extension,
in-04provedall subs proved rax, In-empty, in-02,
eqprovedall subs proved in, in-03, Extension,
eq-04provedall subs proved rax, Extension,
sw-01provedall subs proved rax, Extension,
sub-add-04provedall subs proved ne-02, ne-01, rax, Subset,
neprovedall subs proved rax, In-empty, Extension,
eq-01provedall 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-transprovedall subs proved ne-02, ne-01, Subset,
in-02provedall subs proved in, In-insert,
subset-equalprovedall subs proved ne-02, ne-01, Extension, Subset,
sub-inprovedall 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,
in-01provedall subs proved add,
inprovedall subs proved add,
ne-02provedall subs proved ne-01,
sub-eprovedall subs proved In-empty, Subset,
sub-idemprovedall subs proved Subset,
ne-01provedall subs proved In-empty,
addprovedall subs proved In-insert,
subset-emptyprovedall subs proved Extension, In-empty, Subset,
Subsetaxiom
Extensionaxiom
In-emptyaxiom
In-insertaxiom