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: |
|---|
| sqle | proved | all subs proved
| ls-08,
mult-c,
mult-a,
zero-06,
sqp,
|
| square-even-01 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
square-even,
|
| square-even | proved | all subs proved
| rdist,
dist,
modeq,
ex-two,
mult-c,
mult-a,
rsucc-01,
|
| sqp | proved | all subs proved
| mult-c,
mult-a,
mult-le-01,
|
| sqr-09 | proved | all subs proved
| mult-c,
mult-a,
mult-le-01,
|
| le2-03 | proved | all subs proved
| mult-c,
mult-a,
ls2-02,
|
| ls2-02 | proved | all subs proved
| mult-c,
mult-a,
ls-03-num,
|
| ex-two | proved | all subs proved
| mult-c,
mult-a,
two-succ-05,
two-02,
|
| mult-le-01 | proved | all subs proved
| sqls,
sqr-08,
mult-c,
mult-a,
one-01,
sqzero,
sqle-02,
le-succ,
|
| two-succ-04 | proved | all subs proved
| mult-c,
mult-a,
modls,
|
| mult-eq-succ-01 | proved | all subs proved
| mult-c,
mult-a,
mult-eq-succ-02,
mult-eq-succ,
|
| le2-04 | proved | all subs proved
| mult-c,
mult-a,
modls,
|
| two-succ-05 | proved | all subs proved
| mult-c,
mult-a,
modeq-01,
|
| ls-03-num | proved | all subs proved
| mult-c,
mult-a,
zero,
ls-03,
|
| mult-eq-succ | proved | all subs proved
| zero,
mult-le,
mult-c,
mult-a,
one,
rsucc-01,
|
| le-succ | proved | all subs proved
| zero-01,
mult-c,
mult-a,
one,
modp,
|
| modls | proved | all subs proved
| modp,
modeq-01,
ls,
mult-c,
mult-a,
zero-01,
|
| ls-09 | proved | all subs proved
| mult-c,
mult-a,
ls-03,
zero,
|
| sqr-02 | proved | all subs proved
| mult-c,
mult-a,
ls-04,
sqr-01,
|
| sqr-06 | proved | all subs proved
| mult-c,
mult-a,
mult-le,
|
| mult-eq-succ-02 | proved | all subs proved
| one,
zero,
mod-neq-02,
mult-c,
mult-a,
|
| sqle-02 | proved | all subs proved
| mult-c,
mult-a,
le-05,
|
| sqr-08 | proved | all subs proved
| mult-c,
mult-a,
ls-04,
sqr-03,
sqzero,
le-04,
|
| modeq-01 | proved | all subs proved
| mult-c,
mult-a,
zero-02,
mod-neq-02,
|
| modp | proved | all subs proved
| zero-01,
rsucc-01,
mult-c,
mult-a,
le-05,
zero,
|
| mult-le | proved | all subs proved
| mult-c,
mult-a,
ls-04,
zero-01,
leone,
|
| sqr-01 | proved | all subs proved
| leone,
mult-c,
mult-a,
ls-04,
sqzero,
|
| ls-03 | proved | all subs proved
| mult-c,
mult-a,
zero,
ls-10,
|
| ls-05 | proved | all subs proved
| mult-c,
mult-a,
le-05,
|
| coef-22 | proved | all subs proved
| coef-16,
mult-c,
mult-a,
zero,
|
| twole-01 | proved | all subs proved
| mult-c,
mult-a,
le-02,
|
| twole-02 | proved | all subs proved
| mult-c,
mult-a,
twols,
|
| square-inject | proved | all subs proved
| zero-02,
mult-c,
mult-a,
coef-21,
numeral-24,
succ,
dist,
rsucc-01,
square-interval,
|
| mod-neq-03 | proved | all subs proved
| mod-neq-02,
mult-c,
mult-a,
rsucc-01,
modeq,
|
| nonumsimp-mod-neq | proved | all subs proved
| mult-c,
mult-a,
mod-neq,
rsucc-01,
|
| square-eq-02 | proved | all subs proved
| square-eq-03,
|
| square-eq-01 | proved | all subs proved
| mult-c,
mult-a,
succ,
dist,
rsucc-01,
square-eq,
|
| sqle-01 | proved | all subs proved
| mult-c,
mult-a,
le-05,
|
| square-le-01 | proved | all subs proved
| mult-c,
mult-a,
succ,
dist,
rsucc-01,
square-le,
|
| le2-02 | proved | all subs proved
| mult-c,
mult-a,
le-05,
|
| sqr | proved | all subs proved
| mult-c,
mult-a,
sqr-05,
|
| sqr-05 | proved | all subs proved
| mult-c,
mult-a,
ls-01,
|
| square-le | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
square-ls,
|
| sqls | proved | all subs proved
| sqr-07,
ls-07,
mult-c,
mult-a,
sqzero,
|
| square-eq | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
square-ls,
|
| square-eq-03 | proved | all subs proved
| mult-c,
mult-a,
dist,
square-ls-05,
|
| mod-neq | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
modls-01,
|
| square-interval | proved | all subs proved
| coef-18,
numeral-20,
mult-c,
mult-a,
rsucc-01,
succ,
dist,
coef-21,
numeral-24,
square-ls,
|
| twols | proved | all subs proved
| mult-c,
mult-a,
ls-01,
|
| le-02 | proved | all subs proved
| mult-c,
mult-a,
ls-01,
|
| coef-16 | proved | all subs proved
| mult-c,
mult-a,
ls-01,
ls-08,
|
| ls-10 | proved | all subs proved
| mult-c,
mult-a,
ls-01,
|
| le-05 | proved | all subs proved
| mult-c,
mult-a,
ls-01,
zero,
|
| mod-neq-02 | proved | all subs proved
| mult-c,
mult-a,
ls-01,
zero-01,
coef-04,
numeral-08,
numeral-07,
|
| le-04 | proved | all subs proved
| leone,
one,
mult-c,
mult-a,
zero,
|
| sqr-03 | proved | all subs proved
| sqr-07,
mult-c,
mult-a,
sqzero,
|
| ls-04 | proved | all subs proved
| leone,
mult-c,
mult-a,
one,
zero-06,
|
| square-ls-03 | proved | all subs proved
| square-ls-05,
|
| square-ls-02 | proved | all subs proved
| mult-c,
mult-a,
succ,
dist,
rsucc-01,
square-ls,
|
| square-ls-01 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
square-ls,
|
| twole | proved | all subs proved
| mult-c,
mult-a,
leone,
|
| mod-neq-01 | proved | all subs proved
| modls-01,
|
| modls-02 | proved | all subs proved
| modls-01,
|
| square-le-03 | proved | all subs proved
| square-ls-05,
|
| twoeqf-02 | proved | all subs proved
| mult-c,
mult-a,
twoeqf,
|
| two-03 | proved | all subs proved
| modls-01,
zero,
twoeq,
mult-c,
mult-a,
|
| twoeqf | proved | all subs proved
| mult-c,
mult-a,
two-zero-01,
two-02,
|
| modls-01 | proved | all subs proved
| mult-c,
mult-a,
mod-nle,
|
| sqr-07 | proved | all subs proved
| one,
numeral-20,
two-02,
rsucc-01,
mult-c,
mult-a,
|
| leone | proved | all subs proved
| coef-18,
zero-06,
one,
mult-c,
mult-a,
zero,
rsucc-01,
|
| square-ls | proved | all subs proved
| ls,
le-num,
square-less,
two-02,
succ,
dist,
mult-c,
mult-a,
rsucc-01,
|
| square-ls-05 | proved | all subs proved
| zero,
le,
ls-06,
ls,
square-le-02,
mult-c,
mult-a,
dist,
|
| ls-01 | proved | all subs proved
| coef-18,
rsucc-01,
mult-c,
mult-a,
zero,
|
| square-ls-04 | proved | all subs proved
| two-02,
rsucc-01,
square-less,
square-le-02,
mult-c,
mult-a,
sqzero,
|
| mod-nls | proved | all subs proved
| mod-nle,
|
| mod-neq-05 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
mod-neq-04,
|
| nonumsimp-mod-neq-05 | proved | all subs proved
| one,
numeral-19,
two-02,
zero-06,
zero,
mult-c,
mult-a,
rsucc-01,
|
| nonumsimp-twoeq | proved | all subs proved
| two-02,
mult-c,
mult-a,
one,
numeral-19,
|
| three | proved | all subs proved
| zero-06,
succ,
two-02,
rsucc-01,
threeeq,
one,
zero,
mult-c,
mult-a,
|
| square-two | proved | all subs proved
| le-num,
two-zero-01,
twoeq,
coef-18,
mult-c,
mult-a,
coef-17,
|
| mod-nle-01 | proved | all subs proved
| mult-c,
mod-nle,
|
| twoeqf-03 | proved | all subs proved
| two-02,
|
| twoeqf-01 | proved | all subs proved
| mult-c,
mult-a,
two-zero-01,
two-02,
|
| mod-neq-04 | proved | all subs proved
| mult-c,
mult-a,
modeq,
|
| mod-nle | proved | all subs proved
| ls,
modls-03,
mult-c,
mult-a,
modeq,
|
| coef-18 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-05,
|
| square-le-02 | proved | all subs proved
| square-less,
mult-c,
mult-a,
ls-06,
|
| two-02 | proved | all subs proved
| mult-c,
mult-a,
one,
numeral-25,
|
| coef-15 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-05,
|
| succ-01 | proved | all subs proved
| mult-c,
mult-a,
zero,
modeq,
|
| threels | proved | all subs proved
| ls2-03,
rsucc-01,
mult-c,
mult-a,
|
| ls2-03 | proved | all subs proved
| mult-c,
mult-a,
two-one-01,
zero-06,
|
| coef-05 | proved | all subs proved
| mult-c,
mult-a,
coef-08,
zero,
dist,
le,
|
| numeral-25 | proved | all subs proved
| rsucc-01,
mult-c,
mult-a,
coef-17,
|
| numeral-19 | proved | all subs proved
| rsucc-01,
mult-c,
mult-a,
coef-17,
|
| coef-21 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-08,
|
| modeq | proved | all subs proved
| coef-17,
rsucc-01,
mult-c,
mult-a,
zero-01,
ls-08,
zero,
|
| square-less | proved | all subs proved
| ls-06,
ls,
le,
mult-c,
mult-a,
sqzero,
|
| le-same | proved | all subs proved
| one,
mult-base,
coef-17,
mult-c,
mult-a,
zero-01,
|
| coef-23 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-08,
|
| coef-19 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-06,
|
| coef-06 | proved | all subs proved
| mult-c,
mult-a,
zero,
coef-03,
|
| two-one-01 | proved | all subs proved
| mult-c,
mult-a,
one-01,
|
| threeeq | proved | all subs proved
| one-01,
rsucc-01,
mult-c,
mult-a,
|
| numeral-07 | proved | all subs proved
| coef-01,
dist,
mult-c,
mult-a,
coef-04,
|
| coef-08 | proved | all subs proved
| mult-c,
mult-a,
zero,
coef-03,
|
| coef-17 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-04,
|
| ls-06 | proved | all subs proved
| mult-c,
mult-a,
zero-06,
zero,
ls,
|
| mult-sub-less | proved | all subs proved
| mult-c,
mult-a,
zero-02,
dist-sub-04,
|
| two-ls-01 | proved | all subs proved
| mult-c,
mult-a,
ls,
|
| dist-sub | proved | all subs proved
| mult-c,
mult-a,
zero-02,
dist-sub-04,
|
| numeral-01 | proved | all subs proved
| dist,
mult-c,
mult-a,
coef-04,
|
| le-03 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
le,
rsucc,
|
| le-rew | proved | all subs proved
| mult-c,
mult-a,
ls,
le,
|
| coef-20 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-07,
|
| coef-11 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-03,
|
| coef-14 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-04,
|
| coef-13 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-03,
|
| coef-03 | proved | all subs proved
| mult-c,
mult-a,
coef-02,
zero,
dist,
ls-02,
|
| coef-07 | proved | all subs proved
| mult-c,
mult-a,
zero,
coef-02,
|
| twoeq | proved | all subs proved
| mult-c,
mult-a,
one-02,
|
| rsucc | proved | all subs proved
| mult-c,
mult-a,
eq-01,
rsucc-01,
|
| coef-04 | proved | all subs proved
| mult-c,
mult-a,
zero,
coef-01,
|
| one-01 | proved | all subs proved
| one,
rsucc-01,
zero,
mult-c,
mult-a,
|
| succ | proved | all subs proved
| mult-c,
mult-a,
eq-01,
rsucc-01,
|
| dist-sub-04 | proved | all subs proved
| mult-c,
mult-a,
zero-02,
dist,
|
| ls | proved | all subs proved
| mult-c,
mult-a,
ls-02,
zero-01,
|
| nonumsimp-lstwo | proved | all subs proved
| mult-c,
mult-a,
one,
numeral-24,
dist,
rsucc-01,
|
| two-succ-03 | proved | all subs proved
| mult-c,
mult-a,
eq-01,
rsucc-01,
|
| leq-mult2 | proved | all subs proved
| mult-c,
mult-a,
one,
numeral-32,
|
| succ-merge | proved | all subs proved
| mult-c,
mult-a,
eq-01,
rsucc-01,
|
| nonumsimp-succ | proved | all subs proved
| mult-c,
mult-a,
eq-01,
rsucc-01,
|
| nonumsimp-twoeq-01 | proved | all subs proved
| mult-c,
mult-a,
one,
numeral-28,
|
| mult-ineq-lt | proved | all subs proved
| mult-c,
mult-a,
ls-02,
|
| nonumsimp-twole | proved | all subs proved
| mult-c,
mult-a,
one,
numeral-32,
|
| dist-sub-03 | proved | all subs proved
| mult-c,
mult-a,
zero-02,
dist,
|
| dist-sub-01 | proved | all subs proved
| mult-c,
mult-a,
zero-02,
rsucc-01,
|
| dist-merge | proved | all subs proved
| mult-c,
mult-a,
coef-01,
dist,
|
| nonumsimp-twonle | proved | all subs proved
| mult-c,
mult-a,
one,
numeral-27,
|
| coef-12 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-02,
|
| coef-10 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-02,
|
| coef-09 | proved | all subs proved
| mult-c,
mult-a,
one,
coef-01,
|
| coef-02 | proved | all subs proved
| mult-c,
mult-a,
zero,
dist,
le,
|
| one-02 | proved | all subs proved
| mult-c,
mult-a,
zero,
zero-03,
|
| ls-02 | proved | all subs proved
| mult-c,
mult-a,
le,
|
| coef-01 | proved | all subs proved
| mult-c,
mult-a,
zero,
dist,
eq,
|
| le-num | proved | all subs proved
| mult-c,
mult-a,
le,
|
| eq-01 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
eq,
|
| zero-02 | proved | all subs proved
| mult-c,
mult-a,
zero,
eq,
|
| one | proved | all subs proved
| zero-03,
rsucc-01,
mult-c,
mult-a,
|
| mult-ineq-le | proved | all subs proved
| mult-c,
mult-a,
le,
|
| zero-04 | proved | all subs proved
| mult-c,
mult-a,
zero,
eq,
|
| neqone | proved | all subs proved
| mult-c,
mult-a,
zero,
zero-03,
|
| two-zero-01 | proved | all subs proved
| mult-c,
mult-a,
zero-06,
|
| eq | proved | all subs proved
| rsucc-01,
mult-c,
mult-a,
zero-06,
zero,
|
| zero-03 | proved | all subs proved
| zero-01,
rsucc-01,
zero-06,
mult-c,
mult-a,
zero,
|
| ls-07 | proved | all subs proved
| zero-06,
rsucc-01,
mult-c,
mult-a,
zero,
|
| sqzero | proved | all subs proved
| mult-c,
mult-a,
zero-06,
|
| le | proved | all subs proved
| numeral-05,
mult-c,
mult-a,
zero-06,
numeral-03,
|
| zero-num | proved | all subs proved
| mult-c,
mult-a,
zero,
zero-06,
|
| numeral-17 | proved | all subs proved
| zero-06,
rsucc-01,
mult-c,
mult-a,
zero-01,
|
| numeral-10 | proved | all subs proved
| zero-06,
rsucc-01,
mult-c,
mult-a,
zero-01,
|
| two-les-01 | proved | all subs proved
| mult-c,
mult-a,
numeral-33,
|
| twols-01 | proved | all subs proved
| zero-06,
rsucc-01,
mult-c,
mult-a,
|
| numeral-03 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-05 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-33 | proved | all subs proved
| mult-c,
mult-a,
ls-08,
|
| numeral-08 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| zero-06 | proved | all subs proved
| mult-c,
mult-a,
zero,
zero-01,
|
| modls-03 | proved | all subs proved
| dist,
rsucc-01,
mult-c,
mult-a,
ls-08,
zero,
|
| addle | proved | all subs proved
| addle-01,
mult-a,
mult-c,
|
| numeral-09 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-04 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-06 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-15 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-12 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-18 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-16 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-11 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-29 | proved | all subs proved
| mult-c,
mult-a,
ls-08,
|
| le-01 | proved | all subs proved
| mult-c,
mult-a,
ls-08,
|
| nonumsimp-addls-01 | proved | all subs proved
| mult-c,
mult-a,
dist,
|
| numeral-27 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| numeral-28 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| ls-08 | proved | all subs proved
| rsucc-01,
mult-c,
mult-a,
zero,
|
| addle-01 | proved | all subs proved
| rsucc-01,
mult-c,
mult-a,
zero,
|
| numeral-32 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| numeral-24 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| dist | proved | all subs proved
| rsucc-01,
mult-c,
mult-a,
zero,
|
| zero-01 | proved | all subs proved
| rsucc-01,
mult-c,
mult-a,
zero,
|
| numeral-20 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| two-succ-06 | proved | all subs proved
| rsucc-01,
mult-c,
mult-a,
|
| lssucc | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| numeral-26 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| numeral-23 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| numeral-21 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| numeral-36 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| numeral-35 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| numeral-30 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| nonumsimp-eqsucc | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| square-one | proved | all subs proved
| mult-c,
mult-a,
|
| dist-sub-02 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| nonumsimp-twols | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| lssucc-01 | proved | all subs proved
| mult-c,
mult-a,
rsucc-01,
|
| zero-05 | proved | all subs proved
| mult-c,
mult-a,
zero,
rsucc-01,
|
| mult-c | proved | all subs proved
| rsucc-01,
rsucc-02,
mult-a,
zero,
mult-base,
|
| zero | proved | all subs proved
| rsucc-02,
mult-a,
|
| rsucc-01 | proved | all subs proved
| rsucc-02,
mult-a,
mult-base,
|
| mult-a | proved | all subs proved
| rdist,
rsucc-02,
mult-base,
|
| rdist | proved | all subs proved
| rsucc-02,
mult-base,
|
| rsucc-02 | proved | all subs proved
| mult-rec,
|
| four | proved | all subs proved
| four-01,
|
| four-01 | proved | all subs proved
| |
| mult-rec | axiom | | |
| mult-base | axiom | | |