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: |
|---|
| min-ls-self2 | proved | all subs proved
| min-c,
min-a,
min-ls-self1,
|
| min-neq2 | proved | all subs proved
| min-c,
min-a,
Min-left,
min-neq1,
|
| max-ls-self2 | proved | all subs proved
| max-c,
max-a,
max-ls-self1,
|
| max-neq2 | proved | all subs proved
| max-c,
max-a,
Max-left,
max-neq1,
|
| max-neq1 | proved | all subs proved
| max-c,
max-a,
Max-left,
Max-right,
|
| max-ls-self1 | proved | all subs proved
| Max-right,
max-c,
max-a,
Max-left,
|
| min-neq1 | proved | all subs proved
| min-c,
min-a,
Min-left,
Min-right,
|
| min-ls-self1 | proved | all subs proved
| Min-right,
min-c,
min-a,
Min-left,
|
| max-i | proved | all subs proved
| Max-right,
max-c,
max-a,
Max-left,
|
| min-ls-both | proved | all subs proved
| Min-right,
min-c,
min-a,
Min-left,
|
| min-i | proved | all subs proved
| Min-right,
min-c,
min-a,
Min-left,
|
| max-distr | proved | all subs proved
| Max-right,
max-c,
max-a,
Max-left,
|
| min-distr | proved | all subs proved
| Min-right,
min-c,
min-a,
Min-left,
|
| max-ls-both | proved | all subs proved
| Max-right,
max-c,
max-a,
Max-left,
|
| max-c | proved | all subs proved
| Max-right,
max-a,
Max-left,
|
| min-c | proved | all subs proved
| Min-right,
min-a,
Min-left,
|
| max-a | proved | all subs proved
| Max-right,
Max-left,
|
| min-a | proved | all subs proved
| Min-right,
Min-left,
|
| Max-left | axiom | | |
| Max-right | axiom | | |
| Min-left | axiom | | |
| Min-right | axiom | | |