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: |
|---|---|---|---|
| sub-succ | proved | all subs proved | sub-add, fle, ls-03, eq-02, le-ls-simp, le-def, |
| sub-add-01 | proved | all subs proved | eq-01, sub-add, ls-03, le-ls-simp, le-def, elim-sub, |
| pred | proved | all subs proved | num-01, rec, ls-le-simp, succ-02, le-def, elim-pred-c, |
| ls-add-not-03 | proved | all subs proved | le-sum, ls-add-not-01, |
| eq-pred-01 | proved | all subs proved | zero, rec, le-def, |
| eq-pred | proved | all subs proved | zero, rec, le-def, |
| eq-03 | proved | all subs proved | zero, rec, le-def, |
| add-sub-less | proved | all subs proved | sub-add, fle, ls-03, eq-02, le-ls-simp, le-def, |
| ls-add-not-01 | proved | all subs proved | ls-add-not, |
| rec | proved | all subs proved | add-01, |
| sub-add | proved | all subs proved | add, |
| succ-04 | proved | all subs proved | num-01, add-01, |
| prop-06 | proved | all subs proved | cancel-01, elim-pred-c, |
| prop-05 | proved | all subs proved | eq-01, add-01, elim-sub, |
| prop-02 | proved | all subs proved | eq-01, add-01, elim-sub, |
| prop | proved | all subs proved | cancel-01, elim-pred-c, |
| pred-02 | proved | all subs proved | cancel-01, elim-pred-c, |
| ls-add-not-02 | proved | all subs proved | le-sum, ls-add-not, |
| less | proved | all subs proved | ls-le-simp, lep-02, lels-03, elim-sub, zero-01, eq-02, lels-02, zero-02, fle, lels, |
| add-03 | proved | all subs proved | add-01, |
| add | proved | all subs proved | eq-02, le-ls-simp, le-def, |
| cancel-01 | proved | all subs proved | eq-01, shift-01, le-def, lep-02, elim-sub, |
| ls-add-not | proved | all subs proved | le-ls-simp, le-def, lep-02, le-sum, trans-ls-le, |
| zero-02 | proved | all subs proved | zero-01, lels-02, zero, |
| add-01 | proved | all subs proved | fle, eq-02, le-ls-simp, le-def, |
| succ | proved | all subs proved | eq-01, |
| sub-same | proved | all subs proved | eq-02, ls-03, le-ls-simp, le-def, elim-sub, |
| sub-ls-rew | proved | all subs proved | elim-sub, ls-01, le-def, |
| sub-le-rew | proved | all subs proved | lep-02, elim-sub, ls-03, le-ls-simp, le-def, |
| prop-07 | proved | all subs proved | eq-02, lels-03, |
| prop-04 | proved | all subs proved | ls, le-def, |
| pred-01 | proved | all subs proved | num-02, zero-01, |
| ls-pred | proved | all subs proved | succ-02, ls-01, fle, lels, succ-01, ls-02, le-def, |
| ls-07 | proved | all subs proved | elim-sub, ls-01, le-ls-simp, le-def, |
| ls-06 | proved | all subs proved | le-add, lels, ls-01, le-ls-simp, le-def, sub-base, |
| ls-05 | proved | all subs proved | zero-01, |
| ls-04 | proved | all subs proved | elim-sub, ls-01, le-ls-simp, le-def, |
| less-03 | proved | all subs proved | elim-sub, eq-02, lels, ls-01, le-ls-simp, le-def, |
| less-01 | proved | all subs proved | le, le-ls-simp, le-def, lep-02, |
| leprf | proved | all subs proved | le-add, ls-02, le-def, |
| lepr | proved | all subs proved | le-add, ls-02, le-def, |
| le-num-05 | proved | all subs proved | ls-02, le-def, |
| le-num-04 | proved | all subs proved | ls-03, le-def, |
| le-num-02 | proved | all subs proved | le, le-def, |
| l-num-05 | proved | all subs proved | ls, le-def, |
| l-num-04 | proved | all subs proved | ls-01, le-def, |
| add-num-04 | proved | all subs proved | eq-02, le-def, eq-01, |
| add-num-02 | proved | all subs proved | eq-02, le-def, |
| add-num-01 | proved | all subs proved | eq-02, le-def, |
| le-sum | proved | all subs proved | lep-02, ls-le-simp, succ-01, lels, anti, ler, succ-02, le-one, fle, le-ls-simp, le-def, lez-01, |
| zero-01 | proved | all subs proved | ler, lels-03, elim-sub, |
| ls-02 | proved | all subs proved | lep-02, elim-sub, |
| le | proved | all subs proved | lep-02, elim-sub, |
| ls | proved | all subs proved | elim-sub, |
| ls-01 | proved | all subs proved | elim-sub, |
| zero | proved | all subs proved | le-def, elim-sub, |
| ls-03 | proved | all subs proved | lep-02, elim-sub, |
| eq-01 | proved | all subs proved | le-def, elim-sub, |
| eq-02 | proved | all subs proved | elim-sub, |
| succ-05 | proved | all subs proved | elim-pred-c, lep, le-def, elim-sub, |
| sub-ls | proved | all subs proved | lep, le-def, elim-sub, |
| prop-01 | proved | all subs proved | elim-sub, |
| less-02 | proved | all subs proved | ls-le-simp, lels, lep, elim-sub, |
| lels-04 | proved | all subs proved | pls, |
| le-num-01 | proved | all subs proved | lep-02, le-def, elim-sub, |
| le-add-02 | proved | all subs proved | le-add, eqle-one, le-addex, |
| le-add-01 | proved | all subs proved | le-add, lep-02, |
| l-num-02 | proved | all subs proved | le-def, elim-sub, |
| l-num-01 | proved | all subs proved | le-def, elim-sub, |
| eq | proved | all subs proved | le-add, |
| pls | proved | all subs proved | fle, ls-le-simp, lep-02, ler, anti, lels, |
| le-one | proved | all subs proved | ls-le-simp, succ-02, fle, le-def, |
| eqle-one | proved | all subs proved | ls-le-simp, lels, succ-01, |
| le-add | proved | all subs proved | ler, lep-01, |
| elim-sub | proved | all subs proved | elim-pred-c, shift-01, num-02, succ-02, num-01, le-def, succ-01, sub-base, |
| les | proved | all subs proved | lep-02, ls-le-simp, succ-02, lels-02, |
| le-num-06 | proved | all subs proved | fle, succ-02, succ-01, |
| l-num-03 | proved | all subs proved | fle, succ-02, succ-01, lels, |
| ge | proved | all subs proved | le-def, ls-le-simp, ge-def, |
| add-ls-right2-le | proved | all subs proved | le-ls-simp, le-def, lep-02, trans-le-le, ls-le-simp, lels, |
| add-le-right2-ls | proved | all subs proved | le-def, trans-le-le, ls-le-simp, lep-02, lels, |
| trans-ls-le | proved | all subs proved | le-ls-simp, fle, lels, |
| le-addex | proved | all subs proved | lez-01, le-rec, lep, |
| lep-01 | proved | all subs proved | one-01, lep-02, lez-01, ler, |
| succ-02 | proved | all subs proved | le-def, le-ls-simp, |
| ls-le-simp | proved | all subs proved | le-ls-simp, |
| trans-le-le | proved | all subs proved | le-ls-simp, fle, le-def, |
| trans-le-ls | proved | all subs proved | le-ls-simp, fle, lels, |
| not-zero | proved | all subs proved | lez-01, |
| neq-01 | proved | all subs proved | le-ls-simp, succ-01, |
| let | proved | all subs proved | le-ls-simp, fle, le-def, |
| fle-01 | proved | all subs proved | le-ls-simp, fle, lels, |
| le-rec | proved | all subs proved | le-def, lels-02, |
| lez-01 | proved | all subs proved | lels-02, |
| elim-pred-c | proved | all subs proved | num-01, num-02, |
| le-ls-simp | proved | all subs proved | fle, |
| shift | proved | all subs proved | shift-01, |
| one-02 | proved | all subs proved | lels-02, |
| lels-02 | proved | all subs proved | anti, lels, lels-03, |
| num-02 | proved | all subs proved | num-01, |
| shift-01 | proved | all subs proved | rax, sub-base, |
| fle | proved | all subs proved | ler, anti, le-def, lels, |
| rax | proved | all subs proved | pred-03, sub-rec, |
| one-01 | proved | all subs proved | succ-01, |
| anti | proved | all subs proved | succ-01, lez, lels, le-def, |
| num-01 | proved | all subs proved | pred-03, |
| lep-02 | proved | all subs proved | succ-01, lez, lep, |
| add-02 | proved | all subs proved | succ-01, |
| pred-03 | proved | all subs proved | sub-base, sub-rec, |
| lels-03 | proved | all subs proved | le-def, |
| lep | proved | all subs proved | le-def, |
| ler | proved | all subs proved | le-def, |
| lez | proved | all subs proved | le-def, |
| lels | proved | all subs proved | le-def, |
| succ-01 | proved | all subs proved | le-def, |
| le-num-03 | proved | all subs proved | le-def, |
| sub-rec | axiom | ||
| ge-def | axiom | ||
| sub-base | axiom | ||
| le-def | axiom |