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: |
|---|---|---|---|
| abs-mone | proved | all subs proved | abs-one, abs-neg, |
| absp-01 | proved | all subs proved | sub-def, abssub-02, abs-06, Abs-pos, le-def, |
| abs-01 | proved | all subs proved | Abs-pos, Abs-neg, abs-neg, |
| abs-zero | proved | all subs proved | le-def, abs-02, abs-06, |
| abs-21 | proved | all subs proved | absneg-01, Abs-pos, Abs-neg, |
| abs-ls-02 | proved | all subs proved | sub-def, abssub-02, abs-06, Abs-pos, le-def, |
| zero-not | proved | all subs proved | abs-06, Abs-pos, abs-16, Abs-neg, le-def, |
| absneg-01 | proved | all subs proved | abs-16, le-def, abseq, |
| abs-06 | proved | all subs proved | abs-16, Abs-neg, abs-02, |
| abs-neg | proved | all subs proved | abseq, Abs-pos, le-def, abs-18, Abs-neg, |
| absa | proved | all subs proved | abs-02, Abs-pos, abseq, Abs-neg, le-def, |
| abs-04 | proved | all subs proved | le-def, abs-18, absle, |
| abs-07 | proved | all subs proved | Abs-pos, Abs-neg, abs-02, |
| abs-09 | proved | all subs proved | le-def, abs-18, abssub, |
| abs-12 | proved | all subs proved | zero-gs, le-def, abs-18, absle, |
| abssub-04 | proved | all subs proved | abssub, sub-def, |
| abssub | proved | all subs proved | lenls, le-def, sub-le-01, abs-18, |
| absle | proved | all subs proved | lenls, le-def, abs-18, |
| abseq | proved | all subs proved | Abs-pos, Abs-neg, le-def, abs-16, |
| abs-02 | proved | all subs proved | Abs-pos, abs-16, |
| absp | proved | all subs proved | abs-ls-03, abs-16, le-def, |
| le-lem | proved | all subs proved | le-def, lenls, |
| antr | proved | all subs proved | lenls, le-def, |
| abs-ls-01 | proved | all subs proved | abs-ls-03, abs-16, le-def, |
| lels | proved | all subs proved | le-def, lenls, |
| absneg | proved | all subs proved | absneg-02, |
| absneg-02 | proved | all subs proved | Abs-neg, le-def, abs-18, |
| lenls | proved | all subs proved | lels-03, |
| abs-16 | proved | all subs proved | le-def, abs-18, |
| abssub-02 | proved | all subs proved | le-def, sub-le-01, abs-18, sub-def, |
| betweenlele-zero-one | proved | all subs proved | le-num, |
| lsle-add-notge | proved | all subs proved | lels-add-notge, |
| abs-03 | proved | all subs proved | absls, le-def, |
| lsle-add-noteq | proved | all subs proved | lels-add-noteq, |
| abs-17 | proved | all subs proved | le-def, abs-18, |
| betweenlels-zero-one | proved | all subs proved | le-num, |
| abs-19 | proved | all subs proved | absls-01, le-def, |
| ple-02 | proved | all subs proved | notle-pos, |
| absle-01 | proved | all subs proved | absls-02, le-def, |
| lep-02 | proved | all subs proved | le-def, le-add, |
| abs-11 | proved | all subs proved | absls, |
| abs-sub | proved | all subs proved | Abs-pos, absls, |
| mone-neg | proved | all subs proved | not-mone, |
| abs-two | proved | all subs proved | le-def, abs-18, |
| betweenlsle-zero-one | proved | all subs proved | le-num, |
| abssub-01 | proved | all subs proved | le-def, sub-le-01, abs-18, |
| lsle-add-notgr | proved | all subs proved | lels-add-notgr, |
| lels-add-notgr | proved | all subs proved | le-def, |
| sub-le-01 | proved | all subs proved | le-def, |
| not-mone | proved | all subs proved | le-def, |
| lels-03 | proved | all subs proved | le-def, |
| zero-gs | proved | all subs proved | le-def, |
| le-add | proved | all subs proved | le-def, |
| absls-02 | proved | all subs proved | Abs-pos, Abs-neg, le-def, |
| notle-pos | proved | all subs proved | le-def, |
| absls-01 | proved | all subs proved | Abs-pos, Abs-neg, |
| lels-add-noteq | proved | all subs proved | le-def, |
| abs-18 | proved | all subs proved | Abs-pos, le-def, Abs-neg, |
| absls | proved | all subs proved | Abs-pos, Abs-neg, |
| lels-add-notge | proved | all subs proved | le-def, |
| le-num | proved | all subs proved | le-def, |
| abs-ls-03 | proved | all subs proved | Abs-pos, Abs-neg, |
| abs-one | proved | all subs proved | Abs-pos, Abs-neg, |
| estimate-add2-ls-left | proved | all subs proved | le-def, |
| absls-04 | proved | all subs proved | Abs-pos, Abs-neg, |
| absls-05 | proved | all subs proved | Abs-neg, Abs-pos, le-def, |
| absls-06 | proved | all subs proved | Abs-neg, Abs-pos, |
| estimate-add2-lsle-left | proved | all subs proved | le-def, |
| absls-03 | proved | all subs proved | Abs-pos, Abs-neg, |
| lep | proved | all subs proved | le-def, |
| ler | proved | all subs proved | le-def, |
| negle-13 | proved | all subs proved | le-def, |
| estimate-add1-ls-right | proved | all subs proved | le-def, |
| discard-add2-lels-left | proved | all subs proved | le-def, |
| forward-lele | proved | all subs proved | le-def, |
| abs-add | proved | all subs proved | Abs-neg, |
| estimate-add2-ls-right | proved | all subs proved | le-def, |
| negle-07 | proved | all subs proved | le-def, |
| real-add-pos-01 | proved | all subs proved | le-def, |
| zero-gels-03 | proved | all subs proved | le-def, |
| estimate-add1-le-right | proved | all subs proved | le-def, |
| zero-gels-04 | proved | all subs proved | le-def, |
| zero-gels-01 | proved | all subs proved | le-def, |
| zero-gels-02 | proved | all subs proved | le-def, |
| lele-add-notgr | proved | all subs proved | le-def, |
| estimate-add1-ls-left | proved | all subs proved | le-def, |
| not-mtwo | proved | all subs proved | le-def, |
| ex-le-add | proved | all subs proved | le-def, |
| zero-ge-01 | proved | all subs proved | le-def, |
| ple-04 | proved | all subs proved | le-def, |
| forward-lels | proved | all subs proved | le-def, |
| estimate-add2-le-left | proved | all subs proved | le-def, |
| ple-03 | proved | all subs proved | le-def, |
| estimate-add2-lsle-right | proved | all subs proved | le-def, |
| ple-01 | proved | all subs proved | le-def, |
| estimate-add1-lsle-left | proved | all subs proved | le-def, |
| ttwo | proved | all subs proved | le-def, |
| abs | proved | all subs proved | Abs-pos, Abs-neg, |
| lep-01 | proved | all subs proved | le-def, |
| abs-10 | proved | all subs proved | Abs-pos, Abs-neg, |
| zero-eq | proved | all subs proved | le-def, |
| abs-14 | proved | all subs proved | Abs-neg, |
| abs-15 | proved | all subs proved | Abs-neg, le-def, |
| forward-le-01 | proved | all subs proved | le-def, |
| forward-le-02 | proved | all subs proved | le-def, |
| estimate-add1-lsle-right | proved | all subs proved | le-def, |
| forward-le-03 | proved | all subs proved | le-def, |
| lenum-add2 | proved | all subs proved | le-def, |
| estimate-add1-le-left | proved | all subs proved | le-def, |
| lenum-add1 | proved | all subs proved | le-def, |
| lels-02 | proved | all subs proved | le-def, |
| lenum-add4 | proved | all subs proved | le-def, |
| lenum-add3 | proved | all subs proved | le-def, |
| abs-ls-04 | proved | all subs proved | Abs-neg, le-def, |
| forward-le-04 | proved | all subs proved | le-def, |
| forward-le-05 | proved | all subs proved | le-def, |
| transrew | proved | all subs proved | le-def, |
| zero-ge | proved | all subs proved | le-def, |
| real-simp-11 | proved | all subs proved | le-def, |
| forward-le | proved | all subs proved | le-def, |
| real-add-same-pos | proved | all subs proved | gr-def, |
| minus-gr | proved | all subs proved | gr-def, |
| lenum-addboth1 | proved | all subs proved | le-def, |
| transrew-01 | proved | all subs proved | le-def, |
| pls-01 | proved | all subs proved | le-def, |
| forward-lsle | proved | all subs proved | le-def, |
| lenum-addboth2 | proved | all subs proved | le-def, |
| estimate-add2-le-right | proved | all subs proved | le-def, |
| le-add-03 | proved | all subs proved | le-def, ge-def, |
| abs-ls | proved | all subs proved | Abs-neg, |
| le-add-07 | proved | all subs proved | le-def, |
| zero-gels | proved | all subs proved | le-def, |
| le-add-06 | proved | all subs proved | le-def, |
| lsls-add-notge | proved | all subs proved | le-def, |
| le-add-05 | proved | all subs proved | le-def, |
| le-add-04 | proved | all subs proved | le-def, ge-def, |
| ple | proved | all subs proved | le-def, |
| le-add-08 | proved | all subs proved | le-def, |
| real-add-pos | proved | all subs proved | le-def, |
| pls | proved | all subs proved | le-def, |
| abs-le-succ | proved | all subs proved | Abs-pos, Abs-neg, le-def, |
| sub-le | proved | all subs proved | le-def, |
| ge-def | axiom | ||
| gr-def | axiom | ||
| sub-def | axiom | ||
| Abs-neg | axiom | ||
| Abs-pos | axiom | ||
| le-def | axiom |