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: |
|---|
| KoenigsLemma | proved | all subs proved
| KoenigsLemma-aux,
it-succ,
it-zero,
allreachable-def,
finout-def,
finroot-def,
infgraph-def,
hpal-root,
hpal-next,
|
| hpal-root | proved | all subs proved
| hpal-reachset-set,
allreachable-def,
finout-def,
infgraph-def,
finroot-def,
|
| hpal-reachset-set | proved | all subs proved
| reach-def,
reachle-def,
finreachle-fin,
haspathanylength-def,
finout-def,
|
| hpal-next | proved | all subs proved
| haspathanylength-def,
hpal-next-aux,
finout-def,
|
| finreachle-fin | proved | all subs proved
| reachle-def,
finreach-fin,
finout-def,
|
| finreach-fin | proved | all subs proved
| finset-nextfin,
reach-def,
finout-def,
|
| hpal-next-aux | proved | all subs proved
| haspathanylength-def,
hpal-next-auxh,
|
| KoenigsLemma-aux | proved | all subs proved
| it-succ,
it-zero,
|
| hpal-next-auxh | proved | all subs proved
| haspathanylength-def,
|
| finset-nextfin | proved | all subs proved
| finout-def,
|
| infgraph-def | axiom | | |
| finroot-def | axiom | | |
| allreachable-def | axiom | | |
| it-zero | axiom | | |
| it-succ | axiom | | |
| reachle-def | axiom | | |
| reach-def | axiom | | |
| finout-def | axiom | | |
| haspathanylength-def | axiom | | |