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: |
|---|
| square-interval-01 | proved | all subs proved
| two-def,
square-interval,
mult-com,
mult-ass,
mult-one,
distr,
|
| square-le-05 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
square-le-05a,
two-def,
|
| square-le-05a | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
square-le-04,
|
| square-interval | proved | all subs proved
| zero-ls-02,
le-posint,
square-le-04,
mult-com,
mult-ass,
mult-one,
distr,
|
| square-eq-one | proved | all subs proved
| abs-ite,
mult-com,
mult-ass,
mult-one,
square-eq,
|
| square-le-one | proved | all subs proved
| mult-com,
mult-ass,
ls-same-05,
square-gr-one,
abs-ite,
mult-one,
square-le,
|
| square-ls-03 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
square-ls-03a,
two-def,
|
| square-ls-04a | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
square-ls-04,
|
| square-ls-04 | proved | all subs proved
| square-ge-one,
two-def,
mult-com,
mult-ass,
mult-one,
distr,
|
| square-ls-03a | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
square-ls-02,
|
| square-gr-one | proved | all subs proved
| ls-same-03,
ls-same-05,
abs-ite,
mult-com,
mult-ass,
mult-one,
square-ls,
|
| square-le-04 | proved | all subs proved
| square-ls,
mult-com,
mult-ass,
mult-one,
distr,
|
| square-eq | proved | all subs proved
| abs-ite,
square-ls,
|
| invmult-ls-pos-add | proved | all subs proved
| minus-left,
distr,
mult-com,
mult-ass,
invmult-ge-pos-add,
invmult-ls-pos,
|
| square-ls-one | proved | all subs proved
| abs-ite,
mult-com,
mult-ass,
mult-one,
square-ls,
|
| square-zero-01a | proved | all subs proved
| mult-com,
mult-ass,
zero-ls-02,
mult-zero,
num-distr-addboth-ls1,
distr,
mult-one,
square-ls-02,
|
| square-ge-one | proved | all subs proved
| abs-ite,
mult-com,
mult-ass,
mult-one,
square-le,
|
| square-ls-02 | proved | all subs proved
| mult-gt-both,
square-le,
mult-com,
mult-ass,
mult-one,
distr,
|
| square-ls | proved | all subs proved
| abs-ite,
square-le,
|
| invmult-ge-pos-add | proved | all subs proved
| mult-com,
mult-ass,
minus-left,
distr,
invmult-ge-pos,
|
| invmult-le-neg-add | proved | all subs proved
| minus-left,
distr,
mult-com,
mult-ass,
invmult-gr-neg-add,
invmult-le-neg,
|
| invmult-le-pos-add | proved | all subs proved
| invmult-gr-pos-add,
mult-com,
mult-ass,
minus-left,
distr,
invmult-le-pos,
|
| square-gez-01 | proved | all subs proved
| mult-com,
mult-ass,
square-gez,
|
| square-minus | proved | all subs proved
| mult-com,
mult-ass,
square-lez-01,
mult-zero,
|
| twice-le-zero | proved | all subs proved
| mult-com,
mult-ass,
zero-le,
zero-le-03,
two-def,
|
| zero-le-03 | proved | all subs proved
| zero-gr-03,
mult-com,
mult-ass,
zero-le-01,
|
| square-lez-01 | proved | all subs proved
| zero-le,
zero-le-01,
mult-com,
mult-ass,
mult-zero,
|
| square-gez | proved | all subs proved
| mult-com,
mult-ass,
square-lez,
|
| square-le | proved | all subs proved
| zero-gr-02,
ls-pos-01,
ls-forward,
zero-ls-01,
ls-pos,
ls-neg,
zero-le,
le-pos-01,
zero-le-01,
mult-zero,
le-pos,
ple-pos,
le-neg-01,
commutativity,
minus-left,
mult-com,
mult-ass,
le-neg,
abs-ite,
|
| invmult-gr-pos-add | proved | all subs proved
| mult-com,
mult-ass,
minus-left,
distr,
invmult-gr-pos,
|
| invmult-gr-neg-add | proved | all subs proved
| mult-com,
mult-ass,
minus-left,
distr,
invmult-gr-neg,
|
| invmult-ge-pos | proved | all subs proved
| mult-com,
mult-ass,
invmult-ls-pos,
|
| abs-eqall | proved | all subs proved
| eq-nonzero,
neq-not-zero,
zero-ge-02,
zero-neq,
zero-ge-01,
zero-ls-02,
mult-com,
mult-ass,
zero-ls-01,
eq-neg,
minus-left,
abs-ite,
|
| abs-le-one-multiple | proved | all subs proved
| ls-same,
ls-same-03,
mult-zero,
le-same-01,
mult-com,
mult-ass,
le-same-02,
minus-left,
abs-ite,
|
| abs-ls-multiple-one | proved | all subs proved
| le-same-01,
le-same-02,
ls-same,
ls-same-03,
minus-left,
mult-com,
mult-ass,
mult-zero,
abs-ite,
|
| inv-gr-neg | proved | all subs proved
| inv-le-neg,
|
| inv-gr-pos | proved | all subs proved
| inv-le-pos,
|
| inv-twice | proved | all subs proved
| inv-eq,
mult-zero,
mult-com,
mult-ass,
inv-def,
|
| invmult-ls-neg-add | proved | all subs proved
| invmult-ge-neg-add,
mult-com,
mult-ass,
minus-left,
distr,
invmult-ls-neg,
|
| ls-two | proved | all subs proved
| mult-com,
mult-ass,
zero-ge-01,
|
| pzero-gr | proved | all subs proved
| mult-com,
mult-ass,
zero-gr-03,
zero-gr,
|
| pzero-ls | proved | all subs proved
| mult-com,
mult-ass,
zero-ge,
zero-ge-02,
|
| square-eq-03 | proved | all subs proved
| square-eq-02,
mult-com,
mult-ass,
mult-one,
distr,
|
| square-le-03 | proved | all subs proved
| mult-com,
mult-ass,
square-lez,
|
| square-ls-01 | proved | all subs proved
| mult-com,
mult-ass,
square-lez,
|
| square-zero-01 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
zero-le-02,
two-def,
|
| zero-ge-03 | proved | all subs proved
| zero-ls-03,
mult-com,
mult-ass,
zero-ge-01,
|
| zero-ge-case | proved | all subs proved
| zero-ls,
zero-ls-01,
mult-zero,
mult-com,
mult-ass,
zero-ge-01,
|
| zero-gr-case | proved | all subs proved
| zero-le-01,
zero-le,
mult-com,
mult-ass,
zero-gr-03,
|
| zero-le-case | proved | all subs proved
| zero-gr,
mult-zero,
zero-le,
mult-com,
mult-ass,
zero-le-01,
|
| zero-le-02 | proved | all subs proved
| zero-gr-02,
mult-com,
mult-ass,
zero-le,
|
| zero-le-01 | proved | all subs proved
| zero-gr-01,
mult-com,
mult-ass,
minus-left,
zero-le,
|
| ls-same-05 | proved | all subs proved
| le-same-01,
mult-com,
ls-same-04,
|
| square-lez | proved | all subs proved
| minus-left,
mult-com,
mult-ass,
zero-ls-02,
order,
|
| square-eq-02 | proved | all subs proved
| square-eq-01,
two-def,
mult-com,
mult-ass,
mult-zero,
num-distr-addboth-eq1,
mult-one,
distr,
|
| zero-gr-03 | proved | all subs proved
| zero-gr-01,
mult-com,
mult-ass,
mult-zero,
zero-gr-02,
|
| invmult-ge-neg-add | proved | all subs proved
| mult-com,
mult-ass,
minus-left,
distr,
invmult-ge-neg,
|
| invmult-gr-pos | proved | all subs proved
| mult-com,
mult-ass,
invmult-le-pos,
|
| invmult-gr-neg | proved | all subs proved
| mult-com,
mult-ass,
invmult-le-neg,
|
| invmult-ls-pos | proved | all subs proved
| invmult-le-pos,
invmult-eq,
mult-ass,
mult-com,
mult-one,
inv-def,
ls-pos,
|
| inv-eq | proved | all subs proved
| eq-neg-01,
eq-pos-01,
mult-com,
mult-ass,
inv-def,
|
| inv-le-pos | proved | all subs proved
| le-pos-01,
mult-com,
mult-ass,
inv-def,
|
| inv-le-neg | proved | all subs proved
| le-neg-01,
mult-com,
mult-ass,
inv-def,
|
| le-same-02 | proved | all subs proved
| eq-same-03,
mult-com,
mult-ass,
mult-one,
ls-neg,
|
| zero-ge-01 | proved | all subs proved
| zero-ls-01,
mult-com,
mult-ass,
zero-ge,
|
| zero-ge-02 | proved | all subs proved
| zero-ls-02,
mult-com,
mult-ass,
zero-ge,
|
| abs-ls-one-multiple | proved | all subs proved
| le-same,
le-same-03,
ls-same-01,
ls-same-02,
minus-left,
mult-com,
mult-ass,
mult-zero,
abs-ite,
|
| abs-ls-same | proved | all subs proved
| ls-same,
zero-ls-02,
mult-com,
mult-ass,
ls-same-02,
minus-left,
zero-gr-01,
abs-ite,
|
| abs-not-neg | proved | all subs proved
| zero-ls-02,
mult-com,
mult-ass,
zero-gr-01,
minus-left,
abs-ite,
|
| inv-ge-neg | proved | all subs proved
| inv-ls-neg,
|
| inv-ge-pos | proved | all subs proved
| inv-ls-pos,
|
| le-same-04 | proved | all subs proved
| ls-same-01,
ls-same-02,
mult-zero,
le-same,
mult-com,
mult-ass,
le-same-03,
minus-left,
abs-ite,
|
| le-same-05 | proved | all subs proved
| le-same,
le-same-03,
minus-left,
mult-com,
mult-ass,
mult-zero,
abs-ite,
|
| le-same-06 | proved | all subs proved
| mult-com,
mult-ass,
le-same,
|
| ls-two-01 | proved | all subs proved
| mult-com,
mult-ass,
zero-gr-01,
|
| ls-two-02 | proved | all subs proved
| mult-com,
mult-ass,
zero-gr-01,
|
| ls-two-03 | proved | all subs proved
| mult-com,
mult-ass,
zero-gr-01,
|
| mods-zero-07 | proved | all subs proved
| mult-zero,
zero-gr-02,
mult-com,
mult-ass,
zero-ls-02,
|
| mult-gt-one | proved | all subs proved
| mult-com,
mult-ass,
le-same,
|
| mult-pos | proved | all subs proved
| ls-same-03,
mult-com,
mult-ass,
zero-gr-01,
|
| mult-pos-pos | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
eq-same-02,
|
| square-abs | proved | all subs proved
| zero-ls-02,
mult-com,
mult-ass,
eq-neg,
zero-ls-01,
abs-ite,
|
| square-zero | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
zero-eq,
|
| square-zero-02 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
zero-ls-02,
|
| twice-ls-zero | proved | all subs proved
| mult-com,
mult-ass,
zero-ls-02,
zero-ls-01,
|
| two-le-02 | proved | all subs proved
| mult-com,
mult-ass,
le-posint,
mult-zero,
num-distr-addboth-le1,
distr,
|
| zero-ge-add-01 | proved | all subs proved
| mult-com,
mult-ass,
zero-ls-02,
|
| zero-gr-add-01 | proved | all subs proved
| mult-com,
mult-ass,
zero-gr-01,
|
| zero-ls-case | proved | all subs proved
| zero-ge,
zero-ls-03,
mult-com,
mult-ass,
zero-ls-02,
|
| zero-eq | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
zero-neq-01,
zero-neq,
|
| zero-le | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
le-pos,
|
| le-posint | proved | all subs proved
| le-pos,
|
| square-eq-01 | proved | all subs proved
| mult-gt-both,
mult-com,
mult-ass,
mult-one,
distr,
|
| zero-ge | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
le-pos,
|
| eq-same-02 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
eq-same,
|
| zero-gr-02 | proved | all subs proved
| mult-com,
mult-ass,
zero-gr,
mult-zero,
|
| ls-same-04 | proved | all subs proved
| mult-com,
mult-ass,
ls-same,
|
| eq-same-03 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
eq-same,
|
| invmult-le-pos | proved | all subs proved
| le-pos,
mult-ass,
mult-com,
mult-one,
inv-def,
|
| invmult-le-neg | proved | all subs proved
| le-neg,
mult-ass,
mult-com,
mult-one,
inv-def,
|
| invmult-ge-neg | proved | all subs proved
| mult-com,
mult-ass,
invmult-ls-neg,
|
| le-pos-01 | proved | all subs proved
| mult-com,
mult-ass,
le-pos,
|
| le-neg-01 | proved | all subs proved
| mult-com,
mult-ass,
le-neg,
|
| inv-ls-pos | proved | all subs proved
| ls-pos-01,
mult-com,
mult-ass,
inv-def,
|
| inv-ls-neg | proved | all subs proved
| ls-neg-01,
mult-com,
mult-ass,
inv-def,
|
| eq-pos-01 | proved | all subs proved
| mult-com,
mult-ass,
eq-pos,
|
| eq-neg-01 | proved | all subs proved
| mult-com,
eq-neg,
|
| zero-gr-01 | proved | all subs proved
| mult-zero,
zero-gr,
mult-com,
mult-ass,
minus-left,
order,
|
| le-same-03 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
le-neg,
|
| le-same | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
le-pos,
|
| le-same-01 | proved | all subs proved
| ls-same,
mult-one,
le-pos,
mult-com,
mult-ass,
zero-gr,
|
| zero-ls-01 | proved | all subs proved
| mult-com,
mult-ass,
zero-ls-03,
zero-ls,
|
| zero-ls-02 | proved | all subs proved
| mult-com,
mult-ass,
zero-ls,
mult-zero,
|
| eq-same-01 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
eq-same,
|
| inv-mult | proved | all subs proved
| inv-def,
mult-one,
eq-nonzero-02,
mult-com,
mult-ass,
|
| le-abs | proved | all subs proved
| ls-neg,
ls-pos,
ls-forward,
le-pos,
mult-com,
mult-ass,
le-neg,
minus-left,
abs-ite,
|
| le-negint | proved | all subs proved
| le-neg,
|
| mods-ls | proved | all subs proved
| mult-com,
mult-ass,
le-pos,
|
| mult-add-greater | proved | all subs proved
| mult-com,
mult-ass,
zero-ls,
distr,
|
| noeth-zero-ls | proved | all subs proved
| mult-com,
mult-ass,
zero-gr,
abs-ite,
|
| pls-neg | proved | all subs proved
| mult-com,
mult-ass,
eq-neg,
ls-neg,
|
| pnle-neg | proved | all subs proved
| mult-com,
mult-ass,
le-neg,
|
| pnle-pos | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
ls-forward,
le-pos,
|
| two-eq | proved | all subs proved
| mult-com,
mult-ass,
eq-nonzero-int,
|
| two-ls-02 | proved | all subs proved
| mult-com,
mult-ass,
ls-posint,
mult-zero,
num-distr-addboth-ls1,
distr,
two-def,
|
| zero-ge-add-02 | proved | all subs proved
| mult-zero,
zero-ls,
mult-com,
mult-ass,
mult-one,
distr,
ls-pos,
|
| zero-ls-03 | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
ls-neg,
|
| ls-posint | proved | all subs proved
| ls-pos,
|
| eq-nonzero-int | proved | all subs proved
| eq-nonzero,
|
| ple-pos | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
|
| mult-gt-both | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
ls-forward,
|
| zero-ls | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
ls-pos,
|
| zero-gr | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
ls-pos,
|
| le-pos | proved | all subs proved
| mult-ass,
ls-pos,
minus-left,
mult-com,
distr,
order,
|
| le-neg | proved | all subs proved
| mult-com,
mult-ass,
ls-neg,
minus-left,
distr,
order,
|
| invmult-ls-neg | proved | all subs proved
| ls-neg,
mult-ass,
mult-com,
mult-one,
inv-def,
|
| eq-nonzero-02 | proved | all subs proved
| mult-com,
mult-ass,
eq-nonzero,
|
| ls-pos-01 | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
|
| ls-neg-01 | proved | all subs proved
| mult-com,
ls-neg,
|
| eq-same | proved | all subs proved
| mult-zero,
mult-com,
mult-ass,
mult-one,
eq-nonzero,
|
| eq-pos | proved | all subs proved
| eq-nonzero,
|
| ls-same-02 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
ls-neg,
|
| ls-same-01 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
ls-pos,
|
| ls-same-03 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
ls-neg,
|
| ls-same | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
ls-pos,
|
| eq-neg | proved | all subs proved
| eq-nonzero,
|
| zero-neq | proved | all subs proved
| minus-left,
zero-neq-01,
mult-com,
mult-ass,
mult-zero,
|
| eq-nonzero-01 | proved | all subs proved
| mult-com,
mult-ass,
eq-nonzero,
|
| eq-nonzero-03 | proved | all subs proved
| mult-com,
mult-ass,
eq-nonzero,
|
| est-nle | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
ls-forward,
|
| ls-negint | proved | all subs proved
| ls-neg,
|
| ls-pos-02 | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
abs-ite,
|
| ple-neg | proved | all subs proved
| mult-com,
mult-ass,
ls-neg,
|
| ple-pos-better | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
ls-forward,
|
| pls-pos | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
ls-forward,
|
| pls-pos-01 | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
ls-forward,
|
| pls-pos-02 | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
ls-forward,
|
| pnls-neg | proved | all subs proved
| mult-com,
mult-ass,
ls-neg,
|
| pnls-negpos | proved | all subs proved
| mult-com,
mult-ass,
ls-neg,
ls-forward,
ls-pos,
|
| pnls-pos | proved | all subs proved
| mult-com,
mult-ass,
ls-pos,
ls-forward,
|
| pnls-posneg | proved | all subs proved
| mult-com,
mult-ass,
ls-neg,
ls-forward,
ls-pos,
|
| two-sub-01 | proved | all subs proved
| mult-com,
mult-ass,
two-sub,
minus-left,
|
| two-sub-02 | proved | all subs proved
| mult-com,
mult-ass,
two-sub,
minus-left,
two-def,
|
| two-sub-03 | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
num-distr-addboth-eq1,
two-sub,
distr,
two-def,
|
| two-sub-04 | proved | all subs proved
| mult-com,
mult-ass,
two-sub,
mult-zero,
num-distr-addboth-eq1,
minus-left,
distr,
two-def,
|
| two-sub-05 | proved | all subs proved
| mult-com,
mult-ass,
two-sub,
minus-left,
distr,
two-def,
|
| zero-neq-01 | proved | all subs proved
| minus-left,
order,
mult-com,
mult-ass,
mult-zero,
|
| two-sub | proved | all subs proved
| minus-left,
mult-com,
mult-ass,
mult-one,
num-distr,
|
| ls-neg | proved | all subs proved
| minus-left,
distr,
order,
mult-com,
mult-ass,
ls-forward,
|
| ls-pos | proved | all subs proved
| mult-com,
mult-ass,
ls-forward,
minus-left,
distr,
order,
|
| eq-nonzero | proved | all subs proved
| mult-one,
inv-def,
mult-com,
mult-ass,
minus-left,
distr,
|
| abs-eqneg | proved | all subs proved
| mult-com,
mult-ass,
minus-left,
abs-ite,
|
| inv-mult-add-eq | proved | all subs proved
| mult-com,
mult-ass,
minus-left,
|
| minus-one-01 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
minus-left,
|
| ls-forward | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
|
| minus-left | proved | all subs proved
| mult-ass,
mult-zero,
distr,
mult-com,
|
| neq-not-zero | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
|
| minus-one | proved | all subs proved
| mult-zero,
mult-com,
mult-ass,
mult-one,
distr,
|
| neq-not-zero-01 | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
|
| posint-factor | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
num-distr,
|
| two-le | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
num-distr-addboth-le1,
distr,
|
| two-le-01 | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
num-distr-addboth-le1,
distr,
|
| two-le-03 | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
num-distr-addboth-le1,
distr,
|
| two-le-04 | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
num-distr-addboth-le1,
distr,
|
| two-ls | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
num-distr-addboth-ls1,
distr,
|
| two-ls-01 | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
num-distr-addboth-ls1,
distr,
|
| two-ls-03 | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
num-distr-addboth-ls1,
distr,
|
| two-ls-04 | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
num-distr-addboth-ls1,
distr,
|
| zero-left | proved | all subs proved
| mult-com,
mult-ass,
mult-zero,
|
| mult-zero | proved | all subs proved
| mult-com,
mult-ass,
num-distr-eq1,
|
| add-mult-two | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
succ-lsplit,
two-def,
|
| num-distr-addboth-le1 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-addboth-ls1 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| commutativity | proved | all subs proved
| mult-com,
|
| num-distr-addboth-eq1 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-eq1 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| invmult-eq | proved | all subs proved
| mult-ass,
mult-com,
mult-one,
inv-def,
|
| succ-lsplit | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
|
| eq-dist | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| eq-succ | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
|
| eq-succ-01 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| le-dist | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| le-dist-01 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| le-dist-02 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| ls-add-02 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| ls-add-03 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| ls-dist | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| ls-dist-01 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| ls-dist-02 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| ls-dist-03 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
|
| ls-dist-04 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
|
| ls-dist-05 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
|
| ls-dist-06 | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
|
| num-distr-add-eq1 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-add-eq2 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-add-le1 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-add-le2 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-add-ls1 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-add-ls2 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-addboth-eq2 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-addboth-le2 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-addboth-ls2 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-eq2 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-le1 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-le2 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-ls1 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| num-distr-ls2 | proved | all subs proved
| mult-com,
mult-ass,
distr,
|
| succ-rmerge | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
|
| succ-rsplit | proved | all subs proved
| mult-com,
mult-ass,
mult-one,
distr,
|
| order | axiom | | |
| inv-def | axiom | | |
| distr | axiom | | |
| two-def | axiom | | |
| mult-one | axiom | | |
| abs-ite | proved | all subs proved
| |
| mult-ass | axiom | | |
| mult-com | axiom | | |