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: |
|---|
| max-rem-notsame | proved | all subs proved
| max-one,
bag-rem-notmax,
bag-rem-empty,
max-rec,
|
| bag-rem-notmax | proved | all subs proved
| bag-rem-subseteq,
max-subseteq,
bag-rem-empty,
max-one,
max-rec,
|
| unique-elems-rem | proved | all subs proved
| bag-rem-subseteq,
unique-elems-subset,
|
| unique-elems-addtwice | proved | all subs proved
| unique-elems-add,
|
| unique-elems-addmax | proved | all subs proved
| max-in-bag,
unique-elems-add,
|
| max-rem-ls | proved | all subs proved
| bag-rem-subseteq,
max-subseteq,
|
| max-biggest | proved | all subs proved
| max-in-ls,
|
| bag-single-max | proved | all subs proved
| max-one,
|
| unique-elems-subset | proved | all subs proved
| unique-elems,
|
| unique-elems-add | proved | all subs proved
| unique-elems,
|
| max-in-bag | proved | all subs proved
| max-rec,
|
| max-in-ls | proved | all subs proved
| bag-in-single,
max-rec,
|
| max-one | proved | all subs proved
| max-rec,
|
| max-subseteq | proved | all subs proved
| max-rec,
|
| unique-elems-rem-notin | proved | all subs proved
| unique-elems,
|
| unique-elems-empty | proved | all subs proved
| unique-elems,
|
| max-rec-simp | proved | all subs proved
| max-rec,
|
| max-add-smaller | proved | all subs proved
| max-rec,
|
| max-add-one-different | proved | all subs proved
| max-rec,
|
| max-add-bigger | proved | all subs proved
| max-rec,
|
| unique-elems | axiom | | |
| bag-in-single | proved | all subs proved
| |
| max-rec | axiom | | |
| bag-rem-empty | proved | all subs proved
| |
| bag-rem-subseteq | proved | all subs proved
| |