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: |
|---|---|---|---|
| branchsize-1 | proved | all subs proved | branchsize, |
| branchsize-0 | proved | all subs proved | minsize, branchsize, |
| branchsize | axiom | ||
| minsize | axiom |