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: |
|---|
| finremtau-split-weak | proved | all subs proved
| finremtau-def,
remtau-split-weak,
finremtau-append,
|
| remtau-equiv | proved | all subs proved
| remtau-append,
not-lessto,
remtau_of_to-to_of_rmtau,
finremtau-def,
to_of_remtau-remtau_of_to,
|
| finremtau-split-fin | proved | all subs proved
| remtau-split-fin,
finremtau-append,
|
| remtau-split-list-fin | proved | all subs proved
| remtau-split-fin,
|
| remtau-split-list-weak | proved | all subs proved
| finremtau-empty,
remtau-append,
remtau-split-list,
|
| remtau-split-list-inf | proved | all subs proved
| remtau-split-list,
|
| remtau-split-list | proved | all subs proved
| remtau-append,
finremtau-def,
remtau-split,
|
| remtau-split-fin | proved | all subs proved
| finremtau-append,
finremtau-def,
remtau-split,
|
| remtau_of_to-to_of_rmtau | proved | all subs proved
| remtau-append,
finremtau-empty,
finremtau-def,
remtau-split,
|
| remtau-split-weak | proved | all subs proved
| finremtau-empty,
remtau-append,
finremtau-def,
remtau-split,
|
| remtau-split-inf | proved | all subs proved
| finremtau-def,
remtau-split,
|
| remtau-split | proved | all subs proved
| remtau-one-02,
finremtau-cons,
finremtau-append,
remtau-append,
remtau-split-one,
finremtau-def,
|
| remtau-split-one-fin | proved | all subs proved
| finremtau-cons,
finremtau-append,
finremtau-def,
remtau-split-one,
|
| remtau-inf | proved | all subs proved
| finremtau-def,
remtau-split-one,
remtau-empty-equiv,
|
| remtau-split-one-inf | proved | all subs proved
| remtau-split-one,
|
| remtau-one-02 | proved | all subs proved
| remtau-one-03,
remtau-one,
|
| remtau-split-one | proved | all subs proved
| finremtau-cons,
remtau-append,
remtau-empty,
addopt,
remtau-cons,
finremtau-empty,
finremtau-def,
ex-first-nontau,
|
| not-lessto | proved | all subs proved
| remtau-append,
not-lessto-fin,
finremtau-def,
|
| size-to-less | proved | all subs proved
| not-lessto-inf,
|
| remtau-toempty-from-inf | proved | all subs proved
| remtau-toempty-from,
|
| finremtau-one | proved | all subs proved
| remtau-one,
remtau-one-03,
|
| ex-first-nontau | proved | all subs proved
| remtau-empty-equiv,
|
| not-lessto-fin | proved | all subs proved
| finremtau-append,
|
| remtau-toempty-from | proved | all subs proved
| remtau-empty-equiv,
finremtau-def,
remtau-append,
|
| remtau-one-03 | proved | all subs proved
| one-eq-empty,
finremtau-empty,
finremtau-cons,
|
| not-lessto-inf | proved | all subs proved
| remtau-append,
|
| to_of_remtau-remtau_of_to | proved | all subs proved
| remtau-append,
finremtau-def,
|
| remtau-notless | proved | all subs proved
| remtau-notless-fin,
finremtau-def,
|
| remtau-fromempty-to | proved | all subs proved
| remtau-empty-equiv,
remtau-append,
|
| to-addone | proved | all subs proved
| finremtau-append,
|
| finremtau-empty-equiv | proved | all subs proved
| finremtau-def,
remtau-empty-equiv,
|
| one-eq-empty | proved | all subs proved
| remtau-one,
addopt,
remtau-empty,
finremtau-def,
remtau-cons,
|
| remtau-empty-equiv | proved | all subs proved
| remtau-alltau,
remtau-nontau-lem,
addopt,
remtau-cons,
remtau-empty,
|
| remtau-notless-fin | proved | all subs proved
| finremtau-cons,
finremtau-empty,
|
| remtau-append | proved | all subs proved
| finremtau-def,
remtau-append-fin,
|
| finremtau-append | proved | all subs proved
| finremtau-cons,
finremtau-empty,
|
| finremtau-nontau-lem | proved | all subs proved
| finremtau-cons,
|
| remtau-nontau-lem | proved | all subs proved
| addopt,
remtau-cons,
|
| finremtau-empty | proved | all subs proved
| finremtau-def,
remtau-empty,
|
| remtau-one | proved | all subs proved
| addopt,
remtau-empty,
finremtau-def,
remtau-cons,
|
| finremtau-cons | proved | all subs proved
| addopt,
finremtau-def,
remtau-cons,
|
| remtau-append-fin | proved | all subs proved
| addopt,
remtau-cons,
remtau-empty,
|
| remtau-fin | proved | all subs proved
| finremtau-def,
|
| remtau-empty | axiom | | |
| remtau-cons | axiom | | |
| addopt | axiom | | |
| remtau-alltau | axiom | | |
| finremtau-def | axiom | | |