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: |
|---|
| add-eq2pot-01 | proved | all subs proved
| add-eq2pot,
succ,
|
| div-div-rec-01 | proved | all subs proved
| div-div-rec,
|
| pot2-le-pred | proved | all subs proved
| two-lsz,
2pot-leone,
pot2-pos-01,
ls-pos-2pot-01,
Pot-neg,
Pot-pos,
|
| lemon2pot-01 | proved | all subs proved
| lemon2pot,
|
| lemon2pot | proved | all subs proved
| ls-pos-2pot,
|
| ls-pos-2pot-01 | proved | all subs proved
| ls-pos-2pot,
|
| div-div-rec | proved | all subs proved
| ls-mult-2pot,
two-zero,
two-lsz,
succ,
two-lez-01,
zero,
pot2-pos,
|
| add-eq2pot | proved | all subs proved
| ls-pos-2pot,
two-minus,
pot-dist-pos,
|
| two-ls | proved | all subs proved
| two-le-01,
pot2-pos,
pot2-pos-01,
|
| pot2-le-pred-01 | proved | all subs proved
| pot2-ls-pred,
|
| exin2pot-neg | proved | all subs proved
| pot2-ls-pred,
two-le,
pot2-pos,
ls-2pot,
succ,
exin2pot,
|
| mod-two-ge | proved | all subs proved
| pot-dist-pos,
div-twopot,
two-zero,
|
| pot-div3-nls | proved | all subs proved
| pot-nls,
Pot-pos,
|
| le-2pot-01 | proved | all subs proved
| succ,
ls-pos-2pot,
Pot-pos,
|
| mod-two-ls | proved | all subs proved
| pot2-pos,
ls-pos-2pot,
two-lsz,
|
| pot-nls | proved | all subs proved
| one-01,
one,
ls-pos,
|
| ls-mult-2pot | proved | all subs proved
| grz,
two-le,
ls-pos,
two-minus,
pot-dist-pos,
|
| div-twopot | proved | all subs proved
| eq-two,
two-zero,
two-le,
two-lsz,
two-lez,
two-minus,
pot-dist-pos,
|
| pot2-ls-pred | proved | all subs proved
| two-le,
two-lsz,
two-minus,
|
| ls-pos-2pot | proved | all subs proved
| ls-pos,
|
| two-le-01 | proved | all subs proved
| two-le,
|
| pot2-ls-pred-01 | proved | all subs proved
| pot2-pos-01,
two-lsz,
two-leone,
Pot-neg,
Pot-pos,
|
| exinpot | proved | all subs proved
| ls-pos,
Pot-zero,
succ,
|
| divmod2-2pot | proved | all subs proved
| mod2-2pot-01,
|
| lemon2pot-02 | proved | all subs proved
| ls-pos,
|
| mod-two-ge-01 | proved | all subs proved
| pot-dist-pos,
pot2-pos,
pot2-pos-01,
two-zero,
|
| div2 | proved | all subs proved
| 2pot-leone,
zero-02,
Pot-neg,
two-minus,
Pot-pos,
|
| pot-root-est | proved | all subs proved
| le-pos,
pot-square-est,
pot-square-04,
notneg-02,
ls-pos-03,
pot-pot-02,
notneg,
|
| mod-two-ls-01 | proved | all subs proved
| two-lez,
two-le,
|
| pot-square-est | proved | all subs proved
| pot-square-est-div6,
|
| 2pot-leone | proved | all subs proved
| two-minus,
two-lez-01,
|
| ls-2pot | proved | all subs proved
| pot2-pos,
|
| mod2-2pot-01 | proved | all subs proved
| pot2-pos,
two-zero,
succ,
Pot-pos,
|
| ls-pos | proved | all subs proved
| le-pos,
|
| two-le | proved | all subs proved
| le-pos,
|
| pot2-pos-01 | proved | all subs proved
| two-leone,
pot2-pos,
|
| ls-2pot-01 | proved | all subs proved
| pot2-pos,
|
| divmod2-2pot-neg | proved | all subs proved
| div2-2pot-04,
mod-2pot,
pot2-pos,
|
| div2-2pot | proved | all subs proved
| pot2-pos,
succ,
|
| mod-add1-pospos | proved | all subs proved
| pot2-pos,
zero,
|
| pot-lez | proved | all subs proved
| one-01,
eqone-02,
zero-02,
Pot-neg,
pot-zero-01,
notneg-02,
|
| twopot-mone-div | proved | all subs proved
| pot2-pos,
eq-one,
two-zero,
Pot-pos,
|
| mod2-2pot-06 | proved | all subs proved
| mod2-2pot-05,
|
| pot2-pos-03 | proved | all subs proved
| two-minus,
pot2-pos,
|
| mod-ngez-01 | proved | all subs proved
| pot2-pos,
|
| mod-lesame | proved | all subs proved
| pot2-pos,
|
| div2-2pot-01 | proved | all subs proved
| pot2-pos,
succ,
|
| mod-add1-negneg | proved | all subs proved
| pot2-pos,
zero,
|
| mod-ngez | proved | all subs proved
| pot2-pos,
|
| ls-pos-03 | proved | all subs proved
| le-pos-01,
ls-pos-02,
|
| two-lez-01 | proved | all subs proved
| two-lez,
two-minus,
|
| mod2-2pot-05 | proved | all subs proved
| grz,
|
| pot-zero-01 | proved | all subs proved
| one-01,
eqone-02,
grz,
Pot-neg,
|
| le-pos | proved | all subs proved
| notone,
Pot-neg,
notneg-01,
grz,
Pot-zero,
Pot-pos,
|
| pot-square-est-div6 | proved | all subs proved
| pot2-est-div6,
two-lsz,
le-pos-01,
pot-square-03,
pot-pot-02,
pot-pot,
|
| pot2-pos | proved | all subs proved
| grz,
|
| two-zero-01 | proved | all subs proved
| two-zero,
|
| mod2-pos | proved | all subs proved
| grz,
|
| two-mod-01 | proved | all subs proved
| two-mone,
Pot-pos,
|
| mod2-2pot-02 | proved | all subs proved
| two-lez,
Pot-pos,
|
| pred-le | proved | all subs proved
| two-lez,
succ,
|
| mod2-2pot | proved | all subs proved
| two-lez,
Pot-pos,
|
| pot2-pos-05 | proved | all subs proved
| pot2-pos-02,
|
| pot2-pos-02 | proved | all subs proved
| two-lsz,
|
| two-mone | proved | all subs proved
| notneg-01,
|
| two-lez | proved | all subs proved
| notneg-01,
|
| two-zero | proved | all subs proved
| notneg-01,
|
| grz | proved | all subs proved
| notneg-01,
one-01,
zero-03,
zero-02,
Pot-neg,
eqone-01,
|
| le-pos-01 | proved | all subs proved
| Pot-zero,
notneg,
succ,
ls-pos-01,
|
| pot2-pos-04 | proved | all subs proved
| two-lsz,
|
| twolezero | proved | all subs proved
| notneg-01,
|
| abs-2pot | proved | all subs proved
| two-lsz,
|
| mod2-2pot-04 | proved | all subs proved
| two-lsz,
Pot-pos,
|
| div2-2pot-03 | proved | all subs proved
| two-lsz,
Pot-pos,
succ,
|
| ls-pos-01 | proved | all subs proved
| ls-pos-02,
|
| two-lsz | proved | all subs proved
| notneg-02,
|
| notneg-01 | proved | all subs proved
| notneg-02,
Pot-zero,
zero,
|
| minus-odd | proved | all subs proved
| minus-square,
Pot-pos,
|
| equal-minus-one | proved | all subs proved
| minus-one-odd,
zero-02,
one-01,
Pot-pos,
zero-01,
Pot-neg,
minus-one-even,
Pot-zero,
|
| minus-one-even | proved | all subs proved
| one-01,
pot-square,
|
| minus-one-odd | proved | all subs proved
| one-01,
pot-square,
succ,
|
| minus-square | proved | all subs proved
| pot-square-02,
pot-square,
|
| notneg-02 | proved | all subs proved
| Pot-neg,
zero-03,
zero-02,
notneg,
|
| ls-pos-02 | proved | all subs proved
| Pot-neg,
notneg,
succ,
Pot-zero,
|
| notneg | proved | all subs proved
| one-01,
Pot-zero,
Pot-pos,
notone,
|
| pot-square | proved | all subs proved
| pot-square-02,
|
| pot2-succ-01 | proved | all subs proved
| pot2-succ,
|
| pot-square-01 | proved | all subs proved
| pot-square-02,
|
| square-mod-four | proved | all subs proved
| mod-next-square,
|
| mod-next-square | proved | all subs proved
| pot-square-04,
|
| pot-square-02 | proved | all subs proved
| pot-square-04,
pot-pot-02,
|
| zero-03 | proved | all subs proved
| zero-02,
|
| pot2-succ | proved | all subs proved
| eq-two,
succ,
|
| one-01 | proved | all subs proved
| zero-02,
Pot-neg,
one-02,
|
| mod-lez | proved | all subs proved
| mod-lsz,
|
| pot-pot-01 | proved | all subs proved
| pot-pot-03,
|
| pot2-div2 | proved | all subs proved
| eq-two,
succ,
|
| eq2 | proved | all subs proved
| eqone-01,
two-leone,
Pot-neg,
Pot-pos,
|
| minus-square-01 | proved | all subs proved
| pot-square-05,
pot-square-04,
|
| pot2-add | proved | all subs proved
| eq-two,
succ,
|
| pot-square-03 | proved | all subs proved
| pot-square-05,
|
| eq-one | proved | all subs proved
| two-minus,
eq-pos,
|
| pot-pot-03 | proved | all subs proved
| pot-pot-02,
|
| eq-two | proved | all subs proved
| eq-pos,
|
| two-leone | proved | all subs proved
| two-minus,
notone,
|
| pot-square-04 | proved | all subs proved
| pot-square-05,
|
| mod-lsz | proved | all subs proved
| zero,
|
| zero-02 | proved | all subs proved
| zero,
|
| div2-2pot-04 | proved | all subs proved
| div2-2pot-neg,
div2-2pot-02,
|
| pot-div | proved | all subs proved
| Pot-zero,
zero,
pot-dist-pos,
|
| square-nls | proved | all subs proved
| pot-square-05,
|
| pot-sub-dist | proved | all subs proved
| Pot-zero,
zero,
pot-dist-pos,
|
| two-minus-01 | proved | all subs proved
| two-minus,
|
| pot-pot | proved | all subs proved
| pot-dist-pos,
Pot-zero,
Pot-pos,
|
| pot2-est-div6 | proved | all subs proved
| pot2-est-mult8,
Pot-pos,
|
| div2-2pot-neg | proved | all subs proved
| div2-2pot-02,
|
| exin2pot | proved | all subs proved
| pot-dist-pos,
Pot-pos,
|
| eq-pos | proved | all subs proved
| eqone-01,
Pot-zero,
Pot-pos,
|
| pot-pot-02 | proved | all subs proved
| pot-dist-pos,
Pot-zero,
Pot-pos,
|
| pot-square-05 | proved | all subs proved
| one,
Pot-pos,
|
| two-minus | proved | all subs proved
| notone,
Pot-neg,
|
| eqone-02 | proved | all subs proved
| eqone-01,
|
| mod-2pot | proved | all subs proved
| mod2-2pot-03,
|
| zero | proved | all subs proved
| Pot-zero,
Pot-pos,
zero-01,
|
| le-2pot-succ | proved | all subs proved
| succ,
|
| pot-square-est-02 | proved | all subs proved
| succ,
|
| one-03 | proved | all subs proved
| one,
|
| le-same | proved | all subs proved
| succ,
|
| pot-square-est-01 | proved | all subs proved
| Pot-neg,
succ,
|
| mod-pot-shift-pos | proved | all subs proved
| succ,
Pot-pos,
Pot-zero,
|
| geom-mod | proved | all subs proved
| succ,
Pot-zero,
|
| ls-same | proved | all subs proved
| succ,
|
| one-02 | proved | all subs proved
| Pot-pos,
|
| pot2-est-mult8 | proved | all subs proved
| Pot-pos,
|
| div2-2pot-02 | proved | all subs proved
| Pot-pos,
|
| zero-01 | proved | all subs proved
| Pot-pos,
|
| mod2-2pot-03 | proved | all subs proved
| Pot-pos,
|
| eqone-01 | proved | all subs proved
| Pot-pos,
|
| one | proved | all subs proved
| Pot-zero,
Pot-pos,
|
| notone | proved | all subs proved
| Pot-zero,
Pot-pos,
|
| pot-dist-pos | proved | all subs proved
| Pot-zero,
Pot-pos,
|
| succ | proved | all subs proved
| Pot-pos,
|
| pot2-subls | proved | all subs proved
| Pot-pos,
|
| mod-same | proved | all subs proved
| Pot-pos,
|
| le-2pot | proved | all subs proved
| Pot-pos,
|
| pot2-mod2-zero | proved | all subs proved
| Pot-pos,
|
| eqone | proved | all subs proved
| Pot-pos,
|
| two-mod | proved | all subs proved
| Pot-pos,
|
| pot2-suble | proved | all subs proved
| Pot-pos,
|
| Pot-pos | axiom | | |
| Pot-neg | axiom | | |
| Pot-zero | axiom | | |