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: |
|---|---|---|---|
| num-ls-rec | proved | all subs proved | ls, trans, succ, l, ls-succ-04, pred, ls-pred, |
| two-ls | proved | all subs proved | ls-01, numeral-01, numeral, lsrec, trans, |
| minus-one | proved | all subs proved | ls-01, numlsf, numeral-01, numeral, lsrec, trans, |
| ls-rec | proved | all subs proved | ls, trans, succ, l, ls-succ-04, pred, ls-pred, |
| ls-zero | proved | all subs proved | ls-01, lsrec, trans, l, numeral-01, numeral, |
| k-lsrec | proved | all subs proved | trans, ls, succ, l, pred, ls-succ-04, |
| numeral-01 | proved | all subs proved | ls-succ-02, elim-pred, |
| ls-succ-04 | proved | all subs proved | ls, trans, succ, l, ls-succ, irref, ls-succ-02, lsrec, |
| numeral-02 | proved | all subs proved | ls-succ-02, elim-pred, |
| ls-succ-02 | proved | all subs proved | succpred, ls-pred, |
| ls-pred-01 | proved | all subs proved | predsucc, ls-pred-04, |
| forward-pos | proved | all subs proved | ls-02, ls-01, lsrec, l, trans, |
| ls-pred-03 | proved | all subs proved | ls-succ, ls-pred-04, |
| ls-pred-02 | proved | all subs proved | irref, ls-succ, ls-pred-04, |
| ls-02 | proved | all subs proved | ls-succ, trans, l, |
| ls-pred-04 | proved | all subs proved | elim-pred, ls-succ, |
| ls-pred | proved | all subs proved | ls-succ, elim-pred, |
| lf-01 | proved | all subs proved | ls-succ, trans, l, |
| trans-succ | proved | all subs proved | ls-succ, trans, l, |
| numlsf | proved | all subs proved | ls-01, trans, l, |
| ls-succ | proved | all subs proved | l, succpred, irref, ls-01, lssucc, succ-in, lsrec, |
| lf-02 | proved | all subs proved | ls-01, l, |
| tot | proved | all subs proved | l, |
| lf-05 | proved | all subs proved | ls-01, l, |
| lst-01 | proved | all subs proved | l, |
| forward-any-lsle | proved | all subs proved | ls-01, trans, l, |
| lf-08 | proved | all subs proved | ls-01, trans, l, |
| lf | proved | all subs proved | ls, trans, l, |
| lf-07 | proved | all subs proved | ls-01, trans, l, |
| lf-04 | proved | all subs proved | ls-01, trans, l, |
| lst | proved | all subs proved | ls-01, trans, l, |
| lf-03 | proved | all subs proved | ls-01, l, |
| lf-06 | proved | all subs proved | ls-01, l, |
| numlslsdel-01 | proved | all subs proved | ls-01, trans, l, |
| numlslsdel | proved | all subs proved | ls-01, trans, l, |
| trans-lem | proved | all subs proved | ls-01, trans, l, |
| l | proved | all subs proved | lst-02, ls-01, |
| lst-02 | proved | all subs proved | ls-01, lssucc, succ-in, succpred, one-less, elim-pred, pred, ls-succ-01, trans, lsrec, numeral, gen, |
| one-less | proved | all subs proved | succpred, lssucc, elim-pred, |
| ls | proved | all subs proved | irref, succ, lsrec, |
| mone | proved | all subs proved | numeral, |
| elim-pred | proved | all subs proved | succpred, pred, |
| numeral | proved | all subs proved | pred, succpred, |
| succ | proved | all subs proved | pred, predsucc, succ-in, gen, |
| pred-in | proved | all subs proved | predsucc, pred, |
| ls-succ-01 | proved | all subs proved | lsrec, |
| succ-in | proved | all subs proved | succpred, |
| pred | proved | all subs proved | succpred, predsucc, |
| ls-01 | proved | all subs proved | irref, trans, |
| gen | axiom | ||
| lssucc | axiom | ||
| predsucc | axiom | ||
| succpred | axiom | ||
| lsrec | axiom | ||
| irref | axiom | ||
| trans | axiom |