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: |
|---|
| is-aligned-elim | proved | all subs proved
| is-aligned-multiplier,
is-aligned-def,
|
| is-aligned-aligndown-zero-ls | proved | all subs proved
| is-aligned-le-eq-zero,
|
| is-aligned-aligndown-zero | proved | all subs proved
| is-aligned-ls-eq-zero,
|
| is-aligned-add | proved | all subs proved
| is-aligned-mod,
is-aligned-def,
|
| alignup-same0 | proved | all subs proved
| is-aligned-mod,
alignup-def,
|
| alignup-isnot-smaller | proved | all subs proved
| alignup-def,
alignup-is-bigger,
|
| alignup-is-even-bigger | proved | all subs proved
| alignup-def,
alignup-is-bigger,
|
| aligndown-same0 | proved | all subs proved
| is-aligned-mod,
aligndown-def,
|
| aligndown-not-smaller | proved | all subs proved
| is-aligned-def,
is-aligned-mod,
aligndown-def,
|
| aligndown-is-aligned0 | proved | all subs proved
| is-aligned-mod,
aligndown-def,
|
| is-aligned-multiplier | proved | all subs proved
| is-aligned-def,
|
| is-aligned-le-eq-zero | proved | all subs proved
| is-aligned-def,
|
| is-aligned-ls-eq-zero | proved | all subs proved
| is-aligned-def,
|
| alignup-is-bigger | proved | all subs proved
| alignup-def,
|
| is-aligned-mod | proved | all subs proved
| is-aligned-def,
|
| not-mod0-not-aligned | proved | all subs proved
| is-aligned-def,
|
| is-aligned-zero | proved | all subs proved
| is-aligned-def,
|
| is-aligned-still-space | proved | all subs proved
| is-aligned-def,
|
| is-aligned-simp | proved | all subs proved
| is-aligned-def,
|
| is-aligned-same | proved | all subs proved
| is-aligned-def,
|
| is-aligned-pad | proved | all subs proved
| is-aligned-def,
|
| is-aligned-of-mod | proved | all subs proved
| is-aligned-def,
|
| is-aligned-not-multiples | proved | all subs proved
| is-aligned-def,
|
| is-aligned-multiple-1 | proved | all subs proved
| is-aligned-def,
|
| is-aligned-multiple | proved | all subs proved
| is-aligned-def,
|
| is-aligned-mod-alignment | proved | all subs proved
| is-aligned-def,
|
| is-aligned-minus | proved | all subs proved
| is-aligned-def,
|
| is-aligned-is-aligned-mod | proved | all subs proved
| is-aligned-def,
|
| is-aligned-align-up-multiple | proved | all subs proved
| is-aligned-def,
alignup-def,
|
| is-aligned-align-down | proved | all subs proved
| is-aligned-def,
aligndown-def,
|
| is-aligned-add-diff-ls | proved | all subs proved
| is-aligned-def,
|
| is-aligned-add-diff-le | proved | all subs proved
| is-aligned-def,
|
| between-is-aligned | proved | all subs proved
| is-aligned-def,
|
| alignup-upper-bound-01 | proved | all subs proved
| is-aligned-def,
alignup-def,
|
| alignup-upper-bound | proved | all subs proved
| alignup-def,
is-aligned-def,
|
| alignup-same | proved | all subs proved
| alignup-def,
|
| alignup-multiplier | proved | all subs proved
| alignup-def,
|
| alignup-lower-bound | proved | all subs proved
| alignup-def,
is-aligned-def,
|
| alignup-le-is-aligned | proved | all subs proved
| is-aligned-def,
alignup-def,
|
| alignup-le | proved | all subs proved
| alignup-def,
|
| alignup-is-aligned | proved | all subs proved
| is-aligned-def,
alignup-def,
|
| alignup-div-mult | proved | all subs proved
| alignup-def,
|
| alignup-calc | proved | all subs proved
| is-aligned-def,
alignup-def,
|
| alignup-add-mult | proved | all subs proved
| alignup-def,
|
| alignup-add-le | proved | all subs proved
| is-aligned-def,
alignup-def,
|
| alignup-add-bounded1 | proved | all subs proved
| alignup-def,
|
| aligndown-sub-add-sub | proved | all subs proved
| div-mult-to-diff-mod,
aligndown-def,
|
| aligndown-same-equiv | proved | all subs proved
| is-aligned-def,
aligndown-def,
|
| aligndown-same | proved | all subs proved
| aligndown-def,
|
| aligndown-remainder | proved | all subs proved
| aligndown-def,
|
| aligndown-plus-remainder | proved | all subs proved
| aligndown-def,
|
| aligndown-multiplier | proved | all subs proved
| aligndown-def,
|
| aligndown-le | proved | all subs proved
| is-aligned-def,
aligndown-def,
|
| aligndown-is-zero | proved | all subs proved
| aligndown-def,
|
| aligndown-is-smaller-01 | proved | all subs proved
| aligndown-def,
|
| aligndown-is-smaller | proved | all subs proved
| aligndown-def,
|
| aligndown-is-n | proved | all subs proved
| aligndown-def,
|
| aligndown-is-aligned-add | proved | all subs proved
| is-aligned-def,
aligndown-def,
|
| aligndown-is-aligned | proved | all subs proved
| is-aligned-def,
aligndown-def,
|
| aligndown-eq-add | proved | all subs proved
| is-aligned-def,
aligndown-def,
|
| aligndown-aligndown-add | proved | all subs proved
| aligndown-def,
|
| aligndown-add-same0 | proved | all subs proved
| aligndown-def,
|
| aligndown-add-same | proved | all subs proved
| aligndown-def,
|
| aligndown-add-not-smaller | proved | all subs proved
| aligndown-def,
|
| aligndown-add-n-alignup | proved | all subs proved
| is-aligned-def,
alignup-def,
aligndown-def,
|
| aligndown-add-n | proved | all subs proved
| aligndown-def,
|
| align-down-ls-zero | proved | all subs proved
| aligndown-def,
|
| align-down-add-to-align-up | proved | all subs proved
| is-aligned-def,
alignup-def,
aligndown-def,
|
| align-down-add-ls | proved | all subs proved
| aligndown-def,
|
| align-down-add-eq-add-ls | proved | all subs proved
| aligndown-def,
|
| align-down-add-eq | proved | all subs proved
| is-aligned-def,
aligndown-def,
|
| add-n-aligndown | proved | all subs proved
| aligndown-def,
|
| div-mult-to-diff-mod | proved | all subs proved
| |
| alignup-def | axiom | | |
| is-aligned-def | axiom | | |
| aligndown-def | axiom | | |