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: |
|---|
| class-le-predef | proved | all subs proved
| le-03,
le-05,
le-08,
le-04,
le-07,
le-06,
le-14,
le-15,
le-13,
le-12,
le-11,
le-10,
le-09,
le-02,
le-01,
predefined,
|
| le-15 | proved | all subs proved
| le-14,
lsone-15,
|
| le-13 | proved | all subs proved
| le-08,
lsone-13,
|
| le-12 | proved | all subs proved
| le-08,
lsone-12,
|
| le-11 | proved | all subs proved
| le-08,
lsone-11,
|
| le-10 | proved | all subs proved
| le-08,
lsone-10,
|
| le-09 | proved | all subs proved
| le-08,
lsone-09,
|
| le-14 | proved | all subs proved
| le-08,
lsone-14,
|
| le-06 | proved | all subs proved
| le-04,
lsone-06,
|
| le-07 | proved | all subs proved
| le-04,
lsone-07,
|
| le-08 | proved | all subs proved
| le-05,
lsone-08,
|
| obj-predefs | proved | all subs proved
| predefined,
predef-07,
predef-06,
predef-05,
predef-04,
predef-03,
predef-02,
predef-11,
predef-09,
predef-08,
predef-12,
predef-10,
predef-13,
predef-01,
predef,
predef_supers-if,
|
| predsupers-in | proved | all subs proved
| predef-14,
predef-07,
predef-06,
predef-05,
predef-04,
predef-03,
predef-02,
predef-11,
predef-09,
predef-08,
predef-12,
predef-10,
predef-13,
predef-01,
predef,
predef_supers-if,
|
| supers-nodups | proved | all subs proved
| predef_supers-if,
|
| le-04 | proved | all subs proved
| le-03,
lsone-04,
|
| le-05 | proved | all subs proved
| le-03,
lsone-05,
|
| predef_supers-if | proved | all subs proved
| predef-14,
supers-15,
predefined,
supers-not,
supers-14,
supers-13,
supers-12,
supers-11,
supers-10,
supers-09,
supers-08,
supers-07,
supers-06,
supers-05,
supers-04,
supers-03,
supers-02,
supers-01,
|
| superClass-predef | proved | all subs proved
| superClass-03,
superClass-05,
predef-12,
superClass-08,
predef-13,
superClass-04,
superClass-07,
predef-10,
superClass-06,
superClass-14,
predef-07,
superClass-15,
superClass-13,
superClass-12,
superClass-11,
superClass-10,
predef-11,
superClass-09,
superClass-02,
predef,
superClass-01,
predefined,
superClass-not,
|
| predef-supers-same | proved | all subs proved
| superClass-supers,
supers-01,
predef,
predef-supers-rec,
|
| predef-14 | proved | all subs proved
| predef-const,
|
| predef-supers-rec | proved | all subs proved
| supers-05,
supers-03,
supers-07,
supers-04,
supers-06,
supers-14,
supers-15,
supers-13,
supers-12,
supers-11,
supers-10,
supers-08,
supers-09,
supers-01,
supers-02,
predefined,
superClass-supers,
|
| predef | proved | all subs proved
| predef-const,
|
| predef-01 | proved | all subs proved
| predef-const,
|
| predef-13 | proved | all subs proved
| predef-const,
|
| predef-10 | proved | all subs proved
| predef-const,
|
| predef-12 | proved | all subs proved
| predef-const,
|
| predef-08 | proved | all subs proved
| predef-const,
|
| predef-09 | proved | all subs proved
| predef-const,
|
| predef-11 | proved | all subs proved
| predef-const,
|
| predef-02 | proved | all subs proved
| predef-const,
|
| predef-03 | proved | all subs proved
| predef-const,
|
| predef-04 | proved | all subs proved
| predef-const,
|
| predef-05 | proved | all subs proved
| predef-const,
|
| predef-06 | proved | all subs proved
| predef-const,
|
| predef-07 | proved | all subs proved
| predef-const,
|
| le-02 | proved | all subs proved
| le-01,
lsone-02,
|
| le-03 | proved | all subs proved
| le-01,
lsone-03,
|
| superClass-diff | proved | all subs proved
| supers-03,
supers-05,
supers-08,
supers-04,
supers-07,
supers-06,
supers-14,
supers-15,
supers-13,
supers-12,
supers-11,
supers-10,
supers-09,
supers-02,
predefined,
superClass-supers,
|
| le-01 | proved | all subs proved
| lsone-01,
|
| predef-const | proved | all subs proved
| predefined,
|
| superClass-supers | proved | all subs proved
| supers-03,
superClass-03,
supers-05,
superClass-05,
supers-08,
superClass-08,
supers-04,
superClass-04,
supers-07,
superClass-07,
supers-06,
superClass-06,
supers-14,
superClass-14,
supers-15,
superClass-15,
supers-13,
superClass-13,
supers-12,
superClass-12,
supers-11,
superClass-11,
supers-10,
superClass-10,
supers-09,
superClass-09,
supers-02,
superClass-02,
predefined,
|
| in-predefs | proved | all subs proved
| predefined,
predef-classes,
|
| superClass-not | axiom | | |
| superClass-01 | axiom | | |
| superClass-02 | axiom | | |
| superClass-09 | axiom | | |
| superClass-10 | axiom | | |
| superClass-11 | axiom | | |
| superClass-12 | axiom | | |
| superClass-13 | axiom | | |
| superClass-15 | axiom | | |
| superClass-14 | axiom | | |
| superClass-06 | axiom | | |
| superClass-07 | axiom | | |
| superClass-04 | axiom | | |
| superClass-08 | axiom | | |
| superClass-05 | axiom | | |
| superClass-03 | axiom | | |
| supers-not | axiom | | |
| supers-02 | axiom | | |
| supers-01 | axiom | | |
| supers-09 | axiom | | |
| supers-08 | axiom | | |
| supers-10 | axiom | | |
| supers-11 | axiom | | |
| supers-12 | axiom | | |
| supers-13 | axiom | | |
| supers-15 | axiom | | |
| supers-14 | axiom | | |
| supers-06 | axiom | | |
| supers-04 | axiom | | |
| supers-07 | axiom | | |
| supers-03 | axiom | | |
| supers-05 | axiom | | |
| lsone-15 | axiom | | |
| lsone-14 | axiom | | |
| lsone-13 | axiom | | |
| lsone-12 | axiom | | |
| lsone-11 | axiom | | |
| lsone-10 | axiom | | |
| lsone-09 | axiom | | |
| lsone-08 | axiom | | |
| lsone-07 | axiom | | |
| lsone-06 | axiom | | |
| lsone-05 | axiom | | |
| lsone-04 | axiom | | |
| lsone-03 | axiom | | |
| lsone-02 | axiom | | |
| lsone-01 | axiom | | |
| predef-classes | axiom | | |
| predefined | axiom | | |