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: |
|---|
| MAIN-theorem | proved | all subs proved
| divides-reset,
Fok-lem,
NEWPARTS-theorem,
REFINE-theorem,
MAIN,
|
| REFINE-theorem | proved | all subs proved
| REFINEONE-theorem,
resetcnt-rec,
resetcnt-empty,
inpartelem-def,
splitone-def,
split-def,
samepartitions-same,
nodups-perm,
REFINE,
|
| REFINEONE-theorem | proved | all subs proved
| partelem-sem-def,
samepartitions-def,
Fok-mod-cnt,
ADid-def,
nodups-def,
partitions-mod-count,
resetcnt-mod-cnt,
nodups-perm,
inpartelem-def,
partititions-def,
Fok-def,
okp-def,
DAid-def,
in-mod-count,
splitone-def,
split-def,
REFINEONE,
|
| nodups-perm | proved | all subs proved
| nodups-numoc,
|
| divides-reset | proved | all subs proved
| startorfin-reset,
divides-XornoX-head,
divides-def,
empty-divides,
|
| nodups-numoc | proved | all subs proved
| elem-does-occur,
one-oc,
no-oc,
nodups-def,
|
| startorfin-reset | proved | all subs proved
| member-reset,
startorfin-def,
|
| Fok-mod-cnt | proved | all subs proved
| in-mod-count,
Fok-def,
|
| NEWPARTS-theorem | proved | all subs proved
| XornoX-def,
startorfin-def,
in-mod-count,
list2set-def,
okp-def,
partelem-sem-def,
samepartitions-def,
splitone-def,
split-def,
divides-def,
updF-get,
updF-member,
Fok-def,
inpartelem-def,
partititions-def,
partitionRefinement-def,
empty-divides,
NEWPARTS,
|
| Fok-lem | proved | all subs proved
| resetcount-elem,
inpartelem-def,
resetcnt-length,
Fok-def,
|
| nodups-oc-2 | proved | all subs proved
| nodups-oc,
|
| member-reset | proved | all subs proved
| resetcnt-rec,
|
| nodups-oc | proved | all subs proved
| nodups-def,
|
| one-oc | proved | all subs proved
| no-oc,
|
| elem-does-occur | proved | all subs proved
| elem-below-occurs,
|
| divides-XornoX-head | proved | all subs proved
| divides-def,
|
| resetcnt-mod-cnt | proved | all subs proved
| resetcnt-empty,
resetcnt-rec,
|
| partitions-mod-count | proved | all subs proved
| inpartelem-def,
partititions-def,
|
| samepartitions-same | proved | all subs proved
| samepartitions-def,
|
| empty-divides | proved | all subs proved
| divides-def,
|
| in-mod-count | proved | all subs proved
| inpartelem-def,
|
| resetcnt-length | proved | all subs proved
| resetcnt-rec,
resetcnt-empty,
|
| resetcount-elem | proved | all subs proved
| resetcnt-rec,
resetcnt-empty,
|
| split-init-2 | proved | all subs proved
| inpartelem-def,
splitone-def,
split-def,
partititions-def,
|
| resetcnt-idem | proved | all subs proved
| resetcnt-rec,
resetcnt-empty,
|
| no-oc | proved | all subs proved
| |
| elem-below-occurs | proved | all subs proved
| |
| REFINEONE | axiom | | |
| DAid-def | axiom | | |
| nodups-def | axiom | | |
| ADid-def | axiom | | |
| REFINE | axiom | | |
| resetcnt-empty | axiom | | |
| resetcnt-rec | axiom | | |
| NEWPARTS | axiom | | |
| partitionRefinement-def | axiom | | |
| partititions-def | axiom | | |
| updF-member | axiom | | |
| updF-get | axiom | | |
| divides-def | axiom | | |
| split-def | axiom | | |
| splitone-def | axiom | | |
| samepartitions-def | axiom | | |
| partelem-sem-def | axiom | | |
| okp-def | axiom | | |
| list2set-def | axiom | | |
| startorfin-def | axiom | | |
| XornoX-def | axiom | | |
| MAIN | axiom | | |
| Fok-def | axiom | | |
| inpartelem-def | axiom | | |