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: |
|---|
| three | proved | all subs proved
| one-01,
three-01,
eq-same-02,
ls-same-01,
zero-le,
one,
modneqp,
commutativity,
associativity,
|
| modeqp-pos | proved | all subs proved
| modneqp,
|
| modeqp-neg | proved | all subs proved
| commutativity,
associativity,
minus-left,
modneqp,
|
| modneqp | proved | all subs proved
| ls-pos,
associativity,
ls-forward,
commutativity,
modlep-03,
|
| modlep-04 | proved | all subs proved
| le-pos,
commutativity,
associativity,
ls-pos,
modlep-03,
|
| modeqp-copied | proved | all subs proved
| commutativity,
modlep-03,
|
| modlep-03 | proved | all subs proved
| commutativity,
associativity,
one,
ls-add-03,
modlep-02,
|
| square-inject | proved | all subs proved
| eq-pos,
le-pos,
zero-ls,
numls-04,
numsucc,
commutativity,
associativity,
one,
dist-lsplit,
square-interval,
|
| square-eq-02 | proved | all subs proved
| square-eq-01,
|
| mods-ls-04 | proved | all subs proved
| commutativity,
modlsp-02,
mods-ls-02,
|
| mods-ls-01 | proved | all subs proved
| commutativity,
modlep-02,
|
| mods-ls | proved | all subs proved
| commutativity,
modlep-02,
|
| square-interval | proved | all subs proved
| le-pos,
numle-03,
zero-ls,
numls-04,
numsucc,
commutativity,
associativity,
one,
dist-lsplit,
square-ls-02,
|
| square-eq-01 | proved | all subs proved
| square-ls-02,
commutativity,
associativity,
one,
dist-lsplit,
|
| mods-ls-02 | proved | all subs proved
| commutativity,
modlep-01,
|
| modlep-02 | proved | all subs proved
| modlep-01,
|
| square-ls-03 | proved | all subs proved
| square-ls-02,
|
| square-le-05 | proved | all subs proved
| square-le-04,
|
| mods-ls-03 | proved | all subs proved
| commutativity,
modlep-01,
|
| mod-neq | proved | all subs proved
| eq-pos,
modeqp-01,
modeqp,
associativity,
eq-neg,
modeqp-02,
commutativity,
modeqp-03,
|
| square-le-04 | proved | all subs proved
| square-le,
square-ls,
commutativity,
associativity,
one,
dist-lsplit,
|
| square-ls-02 | proved | all subs proved
| square-ls,
square-le,
commutativity,
associativity,
one,
dist-lsplit,
|
| modlep-01 | proved | all subs proved
| modlep,
|
| modeqp-03 | proved | all subs proved
| eq-neg,
commutativity,
associativity,
minus-left,
modeqp-01,
|
| square-one-le | proved | all subs proved
| commutativity,
associativity,
square-le,
|
| square-le-06 | proved | all subs proved
| one,
modlep,
commutativity,
associativity,
zero-gr-01,
|
| square-ex | proved | all subs proved
| one-01,
le-pos,
zero-gr,
square-le,
le-one,
numle-03,
le-dist-02,
one,
dist-lsplit,
commutativity,
associativity,
square-ls,
|
| neq-7-not-even | proved | all subs proved
| neq-9-not-even,
commutativity,
associativity,
odd-even,
|
| le-two | proved | all subs proved
| commutativity,
associativity,
zero-left,
numls-02,
modlsp-02,
modlep,
|
| square-le | proved | all subs proved
| commutativity,
associativity,
square-ls,
|
| neq-9-not-even | proved | all subs proved
| commutativity,
associativity,
odd-even,
|
| modeqp-02 | proved | all subs proved
| commutativity,
associativity,
minus-left,
modeqp,
|
| modeqp-01 | proved | all subs proved
| modeqp,
|
| modlep | proved | all subs proved
| modlsp,
eq-pos,
modeqp,
commutativity,
associativity,
le-pos,
|
| square-gez-02 | proved | all subs proved
| zero-ls-02,
commutativity,
associativity,
square-le-01,
square-le-02,
|
| square-even | proved | all subs proved
| numdist,
modeqp,
ex-two,
commutativity,
associativity,
one,
dist-lsplit,
|
| square-eq | proved | all subs proved
| eq-pos,
abs-eqneg,
minus-left,
square-ls,
square-abs,
abs-eqall,
square-zero,
commutativity,
associativity,
pls-pos,
|
| neq-5-not-even | proved | all subs proved
| commutativity,
associativity,
odd-even,
|
| neq-3-not-even | proved | all subs proved
| commutativity,
associativity,
odd-even,
|
| mods-eq | proved | all subs proved
| modeqp,
|
| 7-not-even | proved | all subs proved
| commutativity,
associativity,
odd-even,
|
| 5-not-even | proved | all subs proved
| commutativity,
associativity,
odd-even,
|
| three-01 | proved | all subs proved
| commutativity,
associativity,
two-oddeq,
|
| square-le-02 | proved | all subs proved
| ls-same,
commutativity,
associativity,
square-abs,
abs-eqall,
|
| square-ls | proved | all subs proved
| square-lez-01,
pls-pos,
square-abs,
abs-eqall,
square-lez,
commutativity,
associativity,
ple-pos,
|
| modeqp | proved | all subs proved
| dist-lsplit,
one,
dist-rsplit,
zero-eq,
zero-ge-add,
ls-add,
commutativity,
associativity,
Mult-zero,
|
| odd-even | proved | all subs proved
| commutativity,
associativity,
two-oddeq,
|
| two-mone | proved | all subs proved
| commutativity,
associativity,
eq-one-neg,
|
| square-minus | proved | all subs proved
| square-lez-01,
commutativity,
associativity,
|
| square-ls-04 | proved | all subs proved
| square-lez-01,
commutativity,
associativity,
one,
dist-lsplit,
|
| exdivmod | proved | all subs proved
| zero-left,
one,
dist-lsplit,
minus-left,
commutativity,
associativity,
zero-ge-add,
exdivmodpos,
|
| eq-one-neg | proved | all subs proved
| one,
one-01,
commutativity,
associativity,
eq-one,
minus-left,
|
| square-lez-01 | proved | all subs proved
| zero-le-case,
commutativity,
associativity,
|
| square-abs | proved | all subs proved
| square-lez,
commutativity,
associativity,
abs-eqall,
|
| two-oddeq | proved | all subs proved
| dist-sub-split,
commutativity,
associativity,
eq-one,
|
| zero-ge-add | proved | all subs proved
| zero-ls,
minus-one,
commutativity,
associativity,
one,
dist-rsplit,
zero-ge-03,
|
| zero-le-two | proved | all subs proved
| zero-le-case,
|
| zero-ge-case | proved | all subs proved
| commutativity,
associativity,
zero-ge-03,
zero-ge,
|
| square-zero-02 | proved | all subs proved
| commutativity,
associativity,
zero-ls-03,
square-zero-01,
|
| square-gez-01 | proved | all subs proved
| commutativity,
associativity,
square-gez,
|
| neq-two | proved | all subs proved
| commutativity,
associativity,
eq-one,
|
| modzero-08 | proved | all subs proved
| modzero,
mods-nls,
commutativity,
associativity,
abs-eqall,
|
| zero-ge-03 | proved | all subs proved
| zero-ls-03,
commutativity,
associativity,
zero-ge-01,
|
| eq-same-02 | proved | all subs proved
| one,
commutativity,
associativity,
mult-pos-pos,
|
| square-zero-01 | proved | all subs proved
| square-lez,
numls-13,
numsucc,
one,
commutativity,
associativity,
dist-lsplit,
|
| zero-le-case | proved | all subs proved
| commutativity,
associativity,
zero-le-03,
zero-le,
|
| square-gez | proved | all subs proved
| commutativity,
associativity,
square-lez,
|
| abs-eqall | proved | all subs proved
| zero-ge-02,
zero-le-01,
zero-ge-01,
commutativity,
associativity,
minus-left,
|
| eq-one | proved | all subs proved
| one-01,
zero-gr-01,
square-lez,
one,
minus-left,
minus-one-02,
commutativity,
associativity,
zero-left,
pzero-ls,
pls-pos,
|
| two-zero | proved | all subs proved
| commutativity,
associativity,
zero-neq-01,
|
| square-ls-01 | proved | all subs proved
| commutativity,
associativity,
square-lez,
|
| square-le-03 | proved | all subs proved
| commutativity,
associativity,
square-lez,
|
| modzero-03 | proved | all subs proved
| minus-one,
commutativity,
associativity,
one,
dist-rsplit,
zero-ge-01,
|
| modzero-02 | proved | all subs proved
| minus-one,
commutativity,
associativity,
one,
dist-rsplit,
zero-ge-01,
|
| modzero-01 | proved | all subs proved
| zero-left,
minus-one,
commutativity,
associativity,
one,
dist-rsplit,
zero-ge-01,
|
| modlsp-06 | proved | all subs proved
| commutativity,
associativity,
minus-left,
modlsp-03,
|
| modlsp-05 | proved | all subs proved
| modlsp-04,
|
| abs-ls | proved | all subs proved
| modzero-06,
|
| zero-le-03 | proved | all subs proved
| zero-gr-03,
commutativity,
associativity,
zero-le-01,
|
| zero-neq-01 | proved | all subs proved
| zero-left,
commutativity,
associativity,
zero-eq,
|
| ls-same-01 | proved | all subs proved
| one-01,
zero-gr,
commutativity,
associativity,
mult-gt-one,
|
| square-zero | proved | all subs proved
| commutativity,
associativity,
zero-eq,
|
| abs-eqneg | proved | all subs proved
| eq-neg,
commutativity,
associativity,
minus-left,
|
| modzero | proved | all subs proved
| commutativity,
associativity,
zero-left,
modlsp-02,
|
| modlsp-03 | proved | all subs proved
| commutativity,
associativity,
one,
ls-add-03,
modlsp-02,
|
| modlsp-04 | proved | all subs proved
| commutativity,
associativity,
minus-left,
modlsp-02,
|
| ls-add | proved | all subs proved
| zero-gr,
one-01,
commutativity,
associativity,
one,
modlsp-02,
|
| exdivmodpos | proved | all subs proved
| one,
dist-lsplit,
ls-pos,
commutativity,
associativity,
zero-gr,
auxexdivmod-01,
|
| mult-pos-pos | proved | all subs proved
| one,
commutativity,
associativity,
eq-same,
|
| pzero-ls | proved | all subs proved
| zero-ls-case,
|
| square-lez | proved | all subs proved
| zero-ls-case,
|
| modzero-06 | proved | all subs proved
| minus-one,
commutativity,
associativity,
one,
dist-rsplit,
zero-ls-01,
|
| zero-ge-01 | proved | all subs proved
| zero-ls-01,
commutativity,
associativity,
zero-ge,
|
| zero-neq | proved | all subs proved
| zero-left,
commutativity,
associativity,
zero-eq,
|
| pnls-neg | proved | all subs proved
| ple-neg,
|
| numle-07 | proved | all subs proved
| zero-ls,
zero-left,
le-same-02,
associativity,
zero-ls-03,
le-same,
commutativity,
|
| modzero-05 | proved | all subs proved
| minus-one,
commutativity,
associativity,
one,
dist-rsplit,
zero-ls-01,
|
| modzero-04 | proved | all subs proved
| minus-one,
commutativity,
associativity,
one,
dist-rsplit,
zero-ls-01,
|
| le-same-05 | proved | all subs proved
| zero-left,
commutativity,
associativity,
le-same-04,
|
| eq-same-03 | proved | all subs proved
| one,
commutativity,
associativity,
eq-same,
|
| eq-same-01 | proved | all subs proved
| one,
commutativity,
associativity,
eq-same,
|
| eq-pos-01 | proved | all subs proved
| commutativity,
associativity,
eq-pos,
|
| abs-ls-same-01 | proved | all subs proved
| one,
eq-dist,
zero-le-01,
minus-left,
le-same-01,
minus-one-02,
zero-left,
commutativity,
associativity,
mods-nls,
|
| abs-ls-same | proved | all subs proved
| ls-same,
abs-not-neg,
commutativity,
associativity,
zero-left,
|
| square-le-01 | proved | all subs proved
| commutativity,
associativity,
zero-ls-03,
ls-same,
|
| zero-ls-case | proved | all subs proved
| zero-ls-03,
commutativity,
associativity,
zero-ls,
|
| ple-neg | proved | all subs proved
| pls-neg,
|
| le-same-02 | proved | all subs proved
| commutativity,
associativity,
one,
le-neg,
|
| zero-ls-01 | proved | all subs proved
| zero-ls-03,
commutativity,
associativity,
zero-ls,
|
| zero-eq | proved | all subs proved
| commutativity,
associativity,
zero-left,
eq-nonzero,
|
| mult-gt-one | proved | all subs proved
| commutativity,
associativity,
le-same,
|
| modlsp-02 | proved | all subs proved
| modlsp-01,
|
| le-same-04 | proved | all subs proved
| zero-left,
commutativity,
associativity,
one,
le-pos-01,
|
| auxexdivmod-01 | proved | all subs proved
| one-01,
one,
zero-le,
le-same,
commutativity,
associativity,
zero-left,
auxexdivmod,
|
| eq-same | proved | all subs proved
| one-01,
neq-not-zero-01,
commutativity,
associativity,
one,
eq-nonzero,
|
| eq-pos | proved | all subs proved
| commutativity,
associativity,
zero-left,
eq-nonzero,
|
| abs-not-neg | proved | all subs proved
| zero-ls-02,
|
| eq-neg | proved | all subs proved
| commutativity,
associativity,
zero-left,
eq-nonzero,
|
| zero-le-01 | proved | all subs proved
| commutativity,
associativity,
Mult-zero,
le-neg,
|
| zero-ge-02 | proved | all subs proved
| zero-ls-02,
commutativity,
associativity,
zero-ge,
|
| zero-ls-sub | proved | all subs proved
| zero-ls-03,
commutativity,
associativity,
zero-ls,
|
| zero-le-02 | proved | all subs proved
| zero-gr-02,
commutativity,
associativity,
zero-le,
|
| zero-ge-add-01 | proved | all subs proved
| commutativity,
associativity,
zero-ls-02,
|
| two-leone | proved | all subs proved
| commutativity,
associativity,
le-one,
|
| two-le-02 | proved | all subs proved
| commutativity,
associativity,
numle-10,
|
| two-eq | proved | all subs proved
| eq-nonzero,
|
| short-mult-max | proved | all subs proved
| le-pos,
zero-gr,
ls-pos,
zero-ge,
commutativity,
associativity,
zero-gr-02,
|
| pzero-gr | proved | all subs proved
| zero-gr-case,
|
| pnls-pos | proved | all subs proved
| zero-ls-02,
commutativity,
associativity,
zero-left,
ple-pos,
|
| pnle-pos | proved | all subs proved
| zero-le,
commutativity,
associativity,
zero-left,
pls-pos,
|
| pnle-neg | proved | all subs proved
| pls-neg,
|
| ple-pos-better | proved | all subs proved
| zero-ls-02,
commutativity,
associativity,
zero-left,
ple-pos,
|
| numls-07 | proved | all subs proved
| zero-gr,
ls-same-02,
zero-ls-03,
commutativity,
associativity,
zero-gr-03,
ls-same-04,
|
| numle-11 | proved | all subs proved
| commutativity,
associativity,
le-neg,
|
| numabs | proved | all subs proved
| commutativity,
associativity,
zero-left,
numabs-01,
|
| mult-gt-both | proved | all subs proved
| zero-le,
zero-left,
numle-10,
ls-pos,
commutativity,
associativity,
ls-forward,
|
| modzero-07 | proved | all subs proved
| commutativity,
associativity,
ls-same-03,
|
| mod-nls | proved | all subs proved
| associativity,
zero-gr-add-02,
numls-12,
commutativity,
|
| mod-nle | proved | all subs proved
| dist-sub-split,
zero-left,
one-01,
zero-le,
commutativity,
associativity,
one,
|
| ls-two | proved | all subs proved
| commutativity,
associativity,
zero-ge,
|
| le-same-06 | proved | all subs proved
| commutativity,
associativity,
le-same,
|
| le-same-03 | proved | all subs proved
| commutativity,
associativity,
one,
le-neg,
|
| le-neg-01 | proved | all subs proved
| commutativity,
associativity,
le-neg,
|
| le-abs | proved | all subs proved
| commutativity,
associativity,
ls-forward,
le-pos-01,
|
| eq-nonzero-03 | proved | all subs proved
| commutativity,
associativity,
eq-nonzero,
|
| eq-nonzero-02 | proved | all subs proved
| commutativity,
associativity,
eq-nonzero,
|
| eq-nonzero-01 | proved | all subs proved
| commutativity,
associativity,
eq-nonzero,
|
| le-one | proved | all subs proved
| zero-gr,
commutativity,
associativity,
ls-same,
|
| zero-gr-case | proved | all subs proved
| zero-gr-03,
commutativity,
associativity,
zero-gr-01,
zero-gr,
|
| ple-pos | proved | all subs proved
| commutativity,
associativity,
ls-pos,
pls-pos,
|
| pls-neg | proved | all subs proved
| commutativity,
associativity,
ls-neg,
|
| ls-same-04 | proved | all subs proved
| commutativity,
associativity,
ls-same,
|
| ls-same-02 | proved | all subs proved
| commutativity,
associativity,
one,
ls-neg,
|
| zero-ls-03 | proved | all subs proved
| zero-ls,
commutativity,
associativity,
zero-left,
ls-neg,
|
| numabs-01 | proved | all subs proved
| commutativity,
associativity,
zero-ls,
|
| numle-10 | proved | all subs proved
| commutativity,
associativity,
le-pos,
|
| ls-same-03 | proved | all subs proved
| commutativity,
associativity,
one,
ls-neg,
|
| modlsp-01 | proved | all subs proved
| modlsp,
|
| zero-gr-add-02 | proved | all subs proved
| zero-ls,
one,
eq-dist,
zero-gr,
commutativity,
associativity,
zero-left,
|
| zero-ge | proved | all subs proved
| commutativity,
associativity,
zero-left,
le-pos,
|
| le-neg | proved | all subs proved
| commutativity,
associativity,
ls-neg,
|
| le-pos-01 | proved | all subs proved
| commutativity,
associativity,
le-pos,
|
| eq-nonzero | proved | all subs proved
| ls-pos,
commutativity,
associativity,
ls-neg,
|
| le-same | proved | all subs proved
| commutativity,
associativity,
one,
le-pos,
|
| zero-le | proved | all subs proved
| commutativity,
associativity,
zero-left,
le-pos,
|
| zero-ls-02 | proved | all subs proved
| zero-ls,
commutativity,
associativity,
zero-left,
|
| mods-nls | proved | all subs proved
| zero-gr,
minus-left,
associativity,
zero-left,
ls-same,
commutativity,
|
| le-same-01 | proved | all subs proved
| commutativity,
associativity,
one,
le-pos,
|
| zero-ls-two | proved | all subs proved
| commutativity,
associativity,
zero-ls,
|
| zero-ge-add-02 | proved | all subs proved
| zero-ls,
commutativity,
associativity,
ls-same,
dist-lsplit,
|
| two-ls-02 | proved | all subs proved
| commutativity,
associativity,
numls-10,
|
| pnls-posneg | proved | all subs proved
| ls-neg,
ls-pos,
commutativity,
associativity,
ls-forward,
|
| pnls-negpos | proved | all subs proved
| ls-pos,
ls-neg,
commutativity,
associativity,
ls-forward,
|
| numls-11 | proved | all subs proved
| commutativity,
associativity,
ls-neg,
|
| noeth-modlep | proved | all subs proved
| ls-add-02,
ls-pos,
ls-forward,
Mult-zero,
ls-pos-01,
numsucc,
minus-one-01,
dist-sub-split,
one,
dist-lsplit,
commutativity,
associativity,
minus-left,
|
| mult-sub-lesseq | proved | all subs proved
| commutativity,
associativity,
le-pos,
|
| mods-zero-07 | proved | all subs proved
| commutativity,
associativity,
zero-ls,
|
| ls-same-05 | proved | all subs proved
| commutativity,
associativity,
ls-same,
|
| ls-pos-02 | proved | all subs proved
| ls-pos-01,
|
| numls-10 | proved | all subs proved
| commutativity,
associativity,
ls-pos,
|
| zero-gr-03 | proved | all subs proved
| zero-gr-01,
zero-left,
commutativity,
associativity,
zero-gr-02,
|
| zero-ls | proved | all subs proved
| commutativity,
associativity,
zero-left,
ls-pos,
|
| modlsp | proved | all subs proved
| commutativity,
associativity,
one,
dist-rsplit,
ls-pos,
|
| ls-pos-01 | proved | all subs proved
| commutativity,
associativity,
ls-pos,
|
| le-pos | proved | all subs proved
| commutativity,
associativity,
ls-pos,
|
| pls-pos | proved | all subs proved
| commutativity,
associativity,
ls-pos,
|
| ls-neg | proved | all subs proved
| commutativity,
associativity,
minus-left,
ls-pos,
|
| auxexdivmod | proved | all subs proved
| dist-sub-split,
ls-pos,
zero-gr,
commutativity,
associativity,
one,
dist-lsplit,
|
| ls-same | proved | all subs proved
| commutativity,
associativity,
one,
ls-pos,
|
| zero-gr-add-01 | proved | all subs proved
| commutativity,
associativity,
zero-gr-01,
|
| pls-pos-02 | proved | all subs proved
| ls-pos,
commutativity,
associativity,
ls-forward,
|
| pls-pos-01 | proved | all subs proved
| ls-pos,
commutativity,
associativity,
ls-forward,
|
| noeth-ls-pos | proved | all subs proved
| commutativity,
associativity,
ls-pos,
|
| mult-sub-less | proved | all subs proved
| commutativity,
associativity,
ls-pos,
|
| mult-pos | proved | all subs proved
| commutativity,
associativity,
zero-gr-01,
|
| mult-add-greater | proved | all subs proved
| commutativity,
associativity,
ls-pos,
|
| ls-sub | proved | all subs proved
| commutativity,
associativity,
ls-pos,
|
| est-nle | proved | all subs proved
| ls-pos,
commutativity,
associativity,
ls-forward,
|
| zero-gr-02 | proved | all subs proved
| zero-gr,
commutativity,
associativity,
zero-left,
|
| zero-gr-01 | proved | all subs proved
| commutativity,
associativity,
minus-left,
zero-gr,
|
| ls-pos | proved | all subs proved
| dist-lsplit,
one,
dist-rsplit,
zero-gr,
commutativity,
associativity,
Mult-zero,
|
| zero-gr-add | proved | all subs proved
| commutativity,
associativity,
zero-gr,
succ-lsplit,
|
| ls-two-03 | proved | all subs proved
| commutativity,
associativity,
zero-gr,
|
| ls-two-02 | proved | all subs proved
| commutativity,
associativity,
zero-gr,
|
| ls-two-01 | proved | all subs proved
| commutativity,
associativity,
zero-gr,
|
| zero-gr | proved | all subs proved
| minus-left,
commutativity,
associativity,
zero-left,
noeth-zero-ls,
|
| noeth-zero-ls | proved | all subs proved
| ls-forward,
minus-one-02,
one,
dist-lsplit,
commutativity,
associativity,
minus-left,
|
| minus-one | proved | all subs proved
| commutativity,
associativity,
minus-one-02,
|
| numls-13 | proved | all subs proved
| commutativity,
associativity,
ls-dist-03,
|
| ex-two | proved | all subs proved
| commutativity,
associativity,
one,
numeq-03,
|
| numls-12 | proved | all subs proved
| commutativity,
associativity,
ls-dist-04,
|
| minus-one-02 | proved | all subs proved
| commutativity,
associativity,
minus-one-01,
|
| two-ls-04 | proved | all subs proved
| commutativity,
associativity,
ls-dist-02,
|
| two-ls-03 | proved | all subs proved
| commutativity,
associativity,
ls-dist,
|
| two-ls-01 | proved | all subs proved
| commutativity,
associativity,
ls-add-03,
|
| two-le-04 | proved | all subs proved
| commutativity,
associativity,
le-dist-02,
|
| two-le-03 | proved | all subs proved
| commutativity,
associativity,
le-dist,
|
| numlsneg-03 | proved | all subs proved
| commutativity,
associativity,
minus-left,
|
| numlsneg-02 | proved | all subs proved
| commutativity,
associativity,
minus-left,
|
| numlsneg-01 | proved | all subs proved
| commutativity,
associativity,
minus-left,
|
| numlsneg | proved | all subs proved
| commutativity,
associativity,
minus-left,
|
| numls-06 | proved | all subs proved
| commutativity,
associativity,
ls-add-02,
|
| numleneg-03 | proved | all subs proved
| commutativity,
associativity,
minus-left,
|
| numleneg-02 | proved | all subs proved
| commutativity,
associativity,
minus-left,
|
| numleneg-01 | proved | all subs proved
| commutativity,
associativity,
minus-left,
|
| numleneg | proved | all subs proved
| commutativity,
associativity,
minus-left,
|
| numle-13 | proved | all subs proved
| commutativity,
associativity,
ls-dist-05,
|
| numle-12 | proved | all subs proved
| commutativity,
associativity,
ls-dist-06,
|
| ls-same-06 | proved | all subs proved
| commutativity,
associativity,
ls-dist-03,
|
| add-mult-two | proved | all subs proved
| commutativity,
associativity,
one,
numeq-03,
|
| ls-dist-02 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| ls-dist | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| le-dist | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| numls-04 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| le-dist-02 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| numle-03 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| ls-dist-04 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| ls-dist-05 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| ls-dist-06 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| ls-add-02 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| ls-add-03 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| minus-one-01 | proved | all subs proved
| commutativity,
associativity,
zero-left,
numsucc,
|
| ls-dist-03 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| numls-02 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| numeq-03 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| minus-left | proved | all subs proved
| commutativity,
associativity,
zero-left,
dist-sub-split,
|
| two-sub-01 | proved | all subs proved
| commutativity,
associativity,
one,
numeq-02,
|
| two-ls | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| two-le-01 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| two-le | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| numls-09 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| numls-08 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| numls-05 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| numls-03 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| numls-01 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| numls | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| numle-09 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| numle-08 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| numle-06 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| numle-05 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| numle-04 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| numle-02 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| numle-01 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| numle | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| numeq-04 | proved | all subs proved
| commutativity,
associativity,
one,
dist-lsplit,
|
| numeq | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| ls-dist-01 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| le-dist-01 | proved | all subs proved
| commutativity,
associativity,
dist-lsplit,
|
| eq-succ-01 | proved | all subs proved
| dist-lsplit,
|
| numeq-02 | proved | all subs proved
| commutativity,
associativity,
eq-succ,
|
| numdist | proved | all subs proved
| associativity,
commutativity,
eq-dist,
|
| numsucc | proved | all subs proved
| commutativity,
associativity,
one,
eq-dist,
|
| dist-lsplit | proved | all subs proved
| commutativity,
associativity,
eq-dist,
|
| dist-sub-split | proved | all subs proved
| commutativity,
associativity,
eq-dist,
|
| two-sub | proved | all subs proved
| associativity,
commutativity,
eq-dist,
|
| two-pred | proved | all subs proved
| commutativity,
associativity,
eq-dist,
|
| succ-rmerge | proved | all subs proved
| commutativity,
associativity,
one,
eq-dist,
|
| pred-rmerge | proved | all subs proved
| commutativity,
associativity,
one,
eq-dist,
|
| numsub | proved | all subs proved
| commutativity,
associativity,
one,
eq-dist,
|
| numeq-01 | proved | all subs proved
| commutativity,
associativity,
eq-dist,
|
| dist-sub-merge | proved | all subs proved
| associativity,
commutativity,
eq-dist,
|
| dist-rmerge | proved | all subs proved
| associativity,
commutativity,
eq-dist,
|
| eq-succ | proved | all subs proved
| commutativity,
associativity,
one,
dist-rsplit,
|
| ls-forward | proved | all subs proved
| commutativity,
associativity,
zero-left,
|
| neq-not-zero-01 | proved | all subs proved
| commutativity,
associativity,
zero-left,
|
| one-01 | proved | all subs proved
| commutativity,
associativity,
one,
|
| eq-dist | proved | all subs proved
| commutativity,
associativity,
dist-rsplit,
|
| neq-not-zero | proved | all subs proved
| commutativity,
associativity,
zero-left,
|
| four | proved | all subs proved
| commutativity,
associativity,
|
| associativity | proved | all subs proved
| commutativity,
one,
dist-rsplit,
Mult-zero,
|
| one | proved | all subs proved
| zero-left,
succ-lsplit,
|
| commutativity | proved | all subs proved
| succ-lsplit,
succ-rsplit,
zero-left,
Mult-zero,
|
| succ-lsplit | proved | all subs proved
| succ-rsplit,
Mult-zero,
|
| dist-rsplit | proved | all subs proved
| succ-rsplit,
Mult-zero,
|
| zero-left | proved | all subs proved
| succ-rsplit,
|
| succ-rsplit | proved | all subs proved
| Mult-succ,
|
| Mult-succ | axiom | | |
| Mult-zero | axiom | | |