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 | proved | all subs proved
| square-even-01,
div-two-zero-01,
div-lezero,
mult-ls-01,
square-even,
square-even-02,
div2zero,
square-ls-01,
|
| square-ls-01 | proved | all subs proved
| square-ls,
|
| square-ls-02 | proved | all subs proved
| square-ls,
|
| div-minus255-256-01 | proved | all subs proved
| div-minus-onediff-01,
|
| square-ls | proved | all subs proved
| square-even-01,
ls-even,
|
| square-even-02 | proved | all subs proved
| square-even-01,
|
| div-minus-onediff-01 | proved | all subs proved
| one-02,
mod-div-zero,
one-01,
div-eq-zero-01,
div-add1-negpos-neg-01,
div-add-rew,
mod-mult-04,
div-add-both,
div-mult-03,
modex,
|
| modmod-add-law | proved | all subs proved
| mod-neg,
modmod-add-law-pos,
|
| square-even-01 | proved | all subs proved
| modeven-neg,
modeven-neg-01,
even-mult,
square-even,
|
| modmod-add-law-pos | proved | all subs proved
| mod-less-01,
mod-lsz,
modmod-add-case,
|
| div-add-rew | proved | all subs proved
| add-div-mult,
|
| mod-div-zero | proved | all subs proved
| mod-not-less,
mod-neg-01,
div-elim-posneg,
mod-neg,
mod-les,
abs-shift,
div-eq-zero-01,
|
| zero-07 | proved | all subs proved
| neg-01,
zero-05,
|
| pdiv-ls | proved | all subs proved
| lsfc-01,
|
| modmod-add-if3 | proved | all subs proved
| modmod-add2-negpos-neg,
modmod-add-zero,
modmod-add2-posneg-neg,
mod-neq,
mod-neq-01,
modmod-add-if,
|
| mod-nls-04 | proved | all subs proved
| mod-les,
abs-shift,
one-01,
mod-less-01,
mod-lezero,
|
| mod-div-ls | proved | all subs proved
| div-le-pos,
less-mult-div-02,
mod-mult-04,
div-mult-03,
div-ls,
div-elim-pospos,
|
| le-abs-numerator | proved | all subs proved
| div-elim-posneg,
div-zero-ngr-01,
div-ls-zero,
Div-left,
div-elim-negneg,
zero-05,
div-ls-same,
div-zero-nls,
ls-same-pos,
|
| div-sum-ls-01 | proved | all subs proved
| div-sum-ls,
|
| div-mult-two-nls | proved | all subs proved
| div-mult-ls,
|
| div-mult-le | proved | all subs proved
| div-mult-ls,
|
| div-minus255-256 | proved | all subs proved
| div-minus-onediff,
|
| div-two-zero-01 | proved | all subs proved
| letwozero,
div-elim-pos,
|
| even-mult | proved | all subs proved
| mod-two-02,
modex,
even-not,
even-not-ex,
|
| lsfc-01 | proved | all subs proved
| ls-02,
|
| modmod-add-case | proved | all subs proved
| modmod-add2-posneg-neg-02,
modmod-add2-posneg-neg-01,
mod-ls-same-02,
modmod-add2-posneg-neg,
modmod-add2-posneg-pos,
modmod-add-zero,
modmod-add2-negpos-pos-02,
modmod-add2-negpos-pos-01,
mod-zero-09,
mod-one,
mod-ls-same-01,
modmod-add2-negpos-pos,
modmod-add-02,
modmod-add2-negpos-neg,
modmod-add,
|
| modmod-add-if | proved | all subs proved
| modmod-add2-negpos-pos-01,
mod-zero-09,
mod-ls-same-01,
modmod-add2-negpos-pos,
modmod-add2-negpos-neg,
modmod-add-02,
modmod-add2-posneg-neg-01,
mod-one,
mod-ls-same-02,
modmod-add2-posneg-neg,
modmod-add2-posneg-pos,
modmod-add,
|
| abs-shift | proved | all subs proved
| mod-ngez-01,
mod-ngez,
mod-zero-06,
mod-neg,
mod-zero-01,
mod-neg-01,
|
| less-mult-div-02 | proved | all subs proved
| less-mult-div-01,
|
| zero-05 | proved | all subs proved
| one,
neg-01,
ls,
div-ngr-zero,
zero-06,
|
| div-sum-ls | proved | all subs proved
| ls-02,
less-mult-div-01,
|
| div-mult-ls | proved | all subs proved
| div-mult-nls-zero,
div-mult-03,
mod-mult-04,
div-add1-pospos,
div-elim-pospos,
|
| div-minus-onediff | proved | all subs proved
| div-zero-02,
div-mult-03,
mod-mult-04,
div-add1-negneg,
div-elim-negpos,
|
| add-div-mult | proved | all subs proved
| div-mult-pos-01,
div-mult-03,
mod-mult-04,
div-add1-pospos,
div-elim-pospos,
mod-zero-one,
|
| zero-02 | proved | all subs proved
| neg,
zero-03,
|
| one-pos | proved | all subs proved
| div-zero-02,
|
| nls-mult-div | proved | all subs proved
| less-mult-div-01,
zero,
abs-intro,
|
| modmod-mult-09 | proved | all subs proved
| mod-neg,
modmod-mult-07,
|
| mod-nls-02 | proved | all subs proved
| mod-zero-06,
mod-ls-same-01,
|
| mod-next-square | proved | all subs proved
| mod-zero-num,
modex-odd-neg-01,
mod-two-01,
modex-odd,
mod-two,
mod-mult-04,
modex,
|
| mod-lsz-01 | proved | all subs proved
| mod-grz-01,
mod-zero-06,
|
| mod-gez | proved | all subs proved
| mod-zero-06,
mod-grz-01,
|
| lsfc | proved | all subs proved
| ls,
|
| lsf-02 | proved | all subs proved
| neg-01,
ls,
|
| lsf-01 | proved | all subs proved
| ls,
|
| lsf | proved | all subs proved
| ls-02,
|
| ls-succ | proved | all subs proved
| ls,
|
| ls-even-01 | proved | all subs proved
| div-elim,
div-elim-negpos,
div-ls-zero,
lstwozero,
two-even,
divmult,
num-ls,
neg-01,
mod-neg-01,
ls-even,
|
| leone-two | proved | all subs proved
| div-elim-pos,
lstwozero,
|
| even-add | proved | all subs proved
| mod-two-02,
even-not,
even-not-ex,
modex,
|
| div2-nle-02 | proved | all subs proved
| nummult-eq-01,
lstwozero,
div-elim-pospos,
|
| div2-neg-01 | proved | all subs proved
| div-elim2,
div2-neg,
|
| div-twoodd-07 | proved | all subs proved
| div-zero-02,
zero,
num-neg,
neg,
div-twoodd-03,
num-neg-01,
|
| div-twoodd-05 | proved | all subs proved
| nummult-ls-02,
div-zero-02,
zero,
num-neg,
div-twoodd-03,
|
| div-two-intro | proved | all subs proved
| div-eq-zero,
neg,
div-twoodd,
num-neg-01,
mult-02,
mod-mult-02,
div-add1-pospos,
nummult-ls-02,
div-zero-02,
zero,
num-neg,
div-twoodd-04,
div-twoodd-03,
nummult-ls,
div-elim-negpos,
div-elim-pospos,
div-mult-01,
div-mult-03,
modex,
|
| div-nls-01 | proved | all subs proved
| neg-01,
neg,
div-nls,
div-zero-ngr-01,
abs-intro,
|
| div-div-pred-01 | proved | all subs proved
| nummult-ls,
div-mult-num-01,
div-zero-02,
div-mult-num,
nummult-le-01,
mod-zero-num,
div-add1-negneg,
div-elim-negpos,
div-ls-zero,
div-div-pred,
|
| div-div-num | proved | all subs proved
| div-div,
|
| div-div-intro | proved | all subs proved
| div-div,
|
| div-add1-posneg-pos-02 | proved | all subs proved
| div-add1-posneg-pos-01,
div-add1-posneg-pos,
one,
one-01,
div-add-succ-neg,
div-add-nosucc-neg,
|
| div-add1-negpos-neg-02 | proved | all subs proved
| div-add1-negpos-neg-01,
div-add1-negpos-neg,
mod-one,
mod-zero-04,
one,
one-01,
div-add-succ,
div-add-nosucc,
|
| abs-shift-01 | proved | all subs proved
| mod-grz-01,
mod-neg-01,
mod-zero-06,
|
| abs-03 | proved | all subs proved
| abs,
abs-02,
|
| zero-03 | proved | all subs proved
| pos,
|
| modmod-mult-07 | proved | all subs proved
| mod-neg-01,
modnum-neg,
modmod-mult-08,
|
| mod-neq-01 | proved | all subs proved
| mod-neq,
mod-neg,
|
| modmod-add2-negpos-neg | proved | all subs proved
| mod-mult-pos-01,
mod-mult-04,
mod-add1-posneg-neg,
div-elim-pospos,
|
| modmod-add2-negpos-pos-01 | proved | all subs proved
| mod-mult-04,
mod-add1-posneg-pos,
div-elim-pospos,
mod-zero-09,
mod-one,
mod-ls-same-01,
|
| modmod-add2-negpos-pos-02 | proved | all subs proved
| modmod-add-zero,
|
| modmod-add2-posneg-pos | proved | all subs proved
| mod-mult-04,
mod-add1-negpos-pos,
div-elim-negpos,
|
| modmod-add2-posneg-neg-01 | proved | all subs proved
| mod-mult-04,
mod-add1-negpos-neg,
div-elim-negpos,
mod-one,
mod-ls-same-02,
|
| modmod-add2-posneg-neg-02 | proved | all subs proved
| modmod-add-zero,
|
| modex-odd-neg-01 | proved | all subs proved
| modex-odd-neg,
|
| ls | proved | all subs proved
| div-zero-ngr,
div-ls-same,
div-elim,
div-elim-pos,
|
| even-not | proved | all subs proved
| mod-add1-negpos-neg,
mod-two-02,
mod-add1-pospos,
|
| lstwozero | proved | all subs proved
| div-zero-ngr,
|
| div2-neg | proved | all subs proved
| div-ls-zero,
|
| letwozero | proved | all subs proved
| div-ngr-zero,
|
| less-mult-div-01 | proved | all subs proved
| zero,
prod-div-less-01,
prod-div-less,
div-mult-03,
div-zero-ngr,
mod-mult-04,
div-add-pos,
|
| ls-02 | proved | all subs proved
| div-zero-ngr,
div-elim-pos,
neg-01,
ls-01,
|
| div-nls | proved | all subs proved
| div-ls-same,
|
| div-mult-nls-zero | proved | all subs proved
| div-ls-zero,
|
| one-02 | proved | all subs proved
| div-eq-same-01,
|
| div-zero-02 | proved | all subs proved
| neg,
neg-01,
zero,
div-eq-zero-01,
div-zero-01,
div-zero,
|
| div-div | proved | all subs proved
| neg-01,
neg,
div-eq-same-01,
Div-right,
div-div-pos,
|
| div-add-nosucc-neg | proved | all subs proved
| mod-neg-01,
div-add-nosucc,
Div-left,
|
| div-add1-posneg-pos | proved | all subs proved
| div-add1-negpos-pos,
|
| div-add1-negpos-neg | proved | all subs proved
| div-add1-posneg-neg,
|
| mod-zero-one | proved | all subs proved
| mod-zero-01,
div-zero-ngr,
num-ls,
div-mult-03,
mod-less-01,
|
| mod-zero-06 | proved | all subs proved
| div-elim-posneg,
div-mone-01,
ls-same-pos-02,
mod-rew,
mod-ls-same-01,
|
| abs-02 | proved | all subs proved
| abs,
|
| two-add-square-01 | proved | all subs proved
| two-add-square,
|
| square-nls-02 | proved | all subs proved
| square-nls,
square-nls-01,
|
| square-nle-02 | proved | all subs proved
| square-nle-01,
|
| quad-div-less | proved | all subs proved
| prod-div-less-01,
|
| one-lez | proved | all subs proved
| one-04,
div-lezero,
|
| modmod-ma-negpos-neg | proved | all subs proved
| mod-mult-04,
mod-add1-posneg-neg,
mod-add1-pospos,
div-elim-pospos,
|
| mod-two-pred-02 | proved | all subs proved
| mod-two-pred-01,
mod-neg-01,
|
| mod-sub-01 | proved | all subs proved
| mod-neg-01,
mod-add-01,
|
| mod-nls-03 | proved | all subs proved
| mod-grz-01,
mod-ls-same-02,
|
| mod-nls | proved | all subs proved
| mod-lezero,
|
| mod-mult-neg-03 | proved | all subs proved
| mod-mult-neg-02,
|
| letwo | proved | all subs proved
| div2-nle,
|
| even-or-succ-even | proved | all subs proved
| mod-mult-pos-01,
even-not-ex,
|
| div2-zero | proved | all subs proved
| div-two-zero,
div-elim2,
|
| div2-nls-03 | proved | all subs proved
| div2-nls-02,
|
| div2-nls-01 | proved | all subs proved
| div2-nls,
|
| div-nle | proved | all subs proved
| div-ls-same,
|
| div-nearer-zero | proved | all subs proved
| neg-01,
Div-right,
ls-same-pos-02,
abs,
|
| div-mult-shift-holds | proved | all subs proved
| div-zero,
div-mult-03,
mod-mult-04,
div-add1-pospos,
div-elim-pospos,
mult-split-mod,
div-mult-rew,
|
| div-est-num | proved | all subs proved
| div-zero-ngr,
div-elim-negpos,
div-elim-pospos,
|
| div-abs | proved | all subs proved
| div-eq-zero-01,
|
| abs-01 | proved | all subs proved
| abs,
|
| pos | proved | all subs proved
| div-zero-nls,
|
| two-add-square | proved | all subs proved
| div-mult-pos-rew,
|
| square-nls-01 | proved | all subs proved
| square-nls,
|
| square-nle-01 | proved | all subs proved
| square-nle,
|
| div2zero | proved | all subs proved
| divmult,
mod-two-06,
|
| one-04 | proved | all subs proved
| div-eq-zero,
|
| modmod-mult-08 | proved | all subs proved
| mod-shift,
|
| mod-add1-negpos-pos | proved | all subs proved
| mod-mult-pos,
div-elim-pospos,
div-elim-negpos,
|
| mod-add1-posneg-pos | proved | all subs proved
| div-elim-pospos,
div-elim-negpos,
|
| mod-add1-posneg-neg | proved | all subs proved
| div-elim-pospos,
div-elim-negpos,
|
| modmod-add2-negpos-pos | proved | all subs proved
| mod-mult-pos-01,
div-elim-pospos,
|
| modmod-add-zero | proved | all subs proved
| div-elim-pospos,
mod-mult-04,
modex,
div-elim-negpos,
modmod-add-02,
modmod-add,
|
| modmod-add2-posneg-neg | proved | all subs proved
| mod-mult-04,
mod-add1-negneg,
div-elim-negpos,
|
| modex-odd-neg | proved | all subs proved
| div-elim-negpos,
div-elim-pospos,
|
| mod-two-pred-01 | proved | all subs proved
| nummult-ls,
div-elim-negpos,
|
| mod-add-01 | proved | all subs proved
| mod-zero-04,
div-elim-negpos,
|
| mod-ls-same-02 | proved | all subs proved
| div-elim-pospos,
div-elim-posneg,
mod-nls-01,
div-elim-negpos,
div-elim-negneg,
mod-zero-05,
|
| mod-ls-same-01 | proved | all subs proved
| div-elim-posneg,
div-elim-pospos,
modnum-neg-01,
mod-one,
mod-zero-04,
div-elim-negneg,
div-elim-negpos,
|
| mod-lezero | proved | all subs proved
| div-elim-negpos,
mod-ls-zero,
|
| mod-two | proved | all subs proved
| mod-two-06,
|
| modex-odd | proved | all subs proved
| nummult-eq-01,
div-elim-negpos,
div-elim-pospos,
mod-two-04,
|
| mod-neq | proved | all subs proved
| div-elim-pospos,
div-elim-posneg,
div-elim-negpos,
div-elim-negneg,
|
| mod-mult-neg-02 | proved | all subs proved
| mod-zero-05,
div-elim-negpos,
mod-mult-neg,
|
| div-le-pos | proved | all subs proved
| div-elim-negpos,
div-elim-pospos,
|
| div-ngr-zero | proved | all subs proved
| div-elim-negpos,
|
| div2-nle | proved | all subs proved
| div-le-same,
|
| prod-div-less-01 | proved | all subs proved
| prod-div-less,
|
| mod-add1-negpos-neg | proved | all subs proved
| div-elim-pospos,
div-elim-negpos,
|
| even-not-ex | proved | all subs proved
| nummult-ls,
div-elim-negpos,
div-elim-pospos,
|
| div-two-zero | proved | all subs proved
| div-eq-zero,
|
| div2-nls-02 | proved | all subs proved
| nummult-ls,
nummult-eq-01,
div-elim-negpos,
div-elim-pospos,
|
| div2-nls | proved | all subs proved
| nummult-eq-01,
div-elim-negpos,
div-elim-pospos,
|
| div-ls-same | proved | all subs proved
| div-elim-pospos,
div-elim-negpos,
|
| div-mult-rew | proved | all subs proved
| mult-split-mod,
|
| div-zero-ngr | proved | all subs proved
| div-elim-negpos,
|
| div-div-pred | proved | all subs proved
| nummult-le-02,
nummult-ls,
div-elim-negpos,
|
| div-ls-zero | proved | all subs proved
| div-zero-nls,
div-elim-negpos,
|
| div-eq-same-01 | proved | all subs proved
| div-elim-posneg,
div-elim-negpos,
div-elim-pospos,
div-elim-negneg,
one,
zero,
|
| div-add-succ-neg | proved | all subs proved
| mod-neg-01,
div-add-succ,
Div-left,
|
| div-add1-posneg-pos-01 | proved | all subs proved
| div-elim-pospos,
div-elim-negpos,
|
| div-add1-negpos-pos | proved | all subs proved
| div-mult-pos,
div-elim-pospos,
div-elim-negpos,
|
| div-add1-negpos-neg-01 | proved | all subs proved
| div-elim-pospos,
div-elim-negpos,
|
| div-add1-posneg-neg | proved | all subs proved
| div-elim-pospos,
div-elim-negpos,
|
| div-add-nosucc | proved | all subs proved
| div-mult-pos-01,
div-eq-zero,
mod-mult-04,
div-add-pos,
div-mult-03,
modex,
|
| div-eq-zero-01 | proved | all subs proved
| div-elim-posneg,
div-elim-pospos,
zero,
div-same,
div-elim-negneg,
div-elim-negpos,
div-eq-zero,
|
| abs | proved | all subs proved
| div-zero-nls,
div-zero-ngr-01,
div-lezero,
div-elim3,
Div-right,
neg-01,
|
| sub-ls-01 | proved | all subs proved
| div-zero-nls,
|
| nummult-ls-02-01 | proved | all subs proved
| mult-ls,
nummult-ls-02,
|
| mult-split-mod-02 | proved | all subs proved
| mult-split-mod,
|
| modmod-mult-06 | proved | all subs proved
| mod-shift,
|
| modmod-ma-01 | proved | all subs proved
| mod-shift,
modmod-add,
mod-zero,
modmod-add-01,
|
| mod256 | proved | all subs proved
| mod-nls-05,
|
| mod-twoodd-01 | proved | all subs proved
| mod-twoodd,
div-two,
mod-two-04,
exodd,
|
| mod-two-05 | proved | all subs proved
| mod-two-06,
|
| mod-pred-neg-01 | proved | all subs proved
| div-elim-negpos,
|
| mod-pred-neg | proved | all subs proved
| div-elim-negpos,
|
| mod-pred-04 | proved | all subs proved
| div-elim-pospos,
mod-succ-01,
|
| mod-pred-01 | proved | all subs proved
| mod-succ-02,
|
| mod-pred | proved | all subs proved
| mod-succ-01,
|
| mod-nls-06 | proved | all subs proved
| mod-neg,
mod-nls-05,
|
| mod-nle-02 | proved | all subs proved
| mod-zero-01,
div-elim-negpos,
|
| mod-mult-pos-02 | proved | all subs proved
| mod-mult-pos-01,
|
| mod-le | proved | all subs proved
| mod-nls-05,
|
| div2-neg-odd | proved | all subs proved
| Div-left,
div2-odd-01,
|
| div2-add-neg | proved | all subs proved
| div-mult-num,
div-two,
nummult-le-03,
div-elim2,
div-elim-pos,
|
| div-zero-nls-01 | proved | all subs proved
| div-zero-nls,
|
| div-zero-06 | proved | all subs proved
| div-eq-zero,
|
| div-zero-04 | proved | all subs proved
| div-eq-zero,
|
| div-mult-two-nls-01 | proved | all subs proved
| nummult-ls-02,
div-elim-pospos,
|
| div-mult-rew-01 | proved | all subs proved
| mult-split-mod,
|
| div-mult-ls-pos | proved | all subs proved
| div-mult-le-01,
|
| div-ls-mone | proved | all subs proved
| div-elim-pospos,
div-elim-negpos,
|
| div-ls-01 | proved | all subs proved
| div-ls,
|
| div-le-same-neg | proved | all subs proved
| div-elim-negpos,
|
| div-eq-same | proved | all subs proved
| div-elim-pospos,
div-elim-posneg,
div-elim-negpos,
div-elim-negneg,
divmult,
|
| div-mult-pos-rew | proved | all subs proved
| div-mult-pos-03,
|
| square-nls | proved | all subs proved
| div-elim-pospos,
|
| square-nle | proved | all subs proved
| div-elim-pospos,
|
| square-even | proved | all subs proved
| div-elim-pospos,
|
| mod-shift | proved | all subs proved
| mod-mult-04,
mod-add-pos,
div-elim-pospos,
|
| mod-succ-02 | proved | all subs proved
| mod-mult-04,
div-elim-pospos,
|
| mod-succ-01 | proved | all subs proved
| div-elim-pospos,
|
| mod-nls-05 | proved | all subs proved
| mod-pos-not-neg,
div-elim-pospos,
|
| prod-div-less | proved | all subs proved
| div-elim-pospos,
|
| mod-mult-pos-01 | proved | all subs proved
| mod-mult-pos,
div-elim-pospos,
|
| mod-two-06 | proved | all subs proved
| div-elim-pospos,
|
| div-le-same | proved | all subs proved
| div-elim-pospos,
one,
|
| div2-odd-01 | proved | all subs proved
| one,
div-mult-num-01,
neg-01,
mod-two-02,
mod-neg-01,
div2-odd,
|
| div-two | proved | all subs proved
| div-mult-pos-03,
|
| nummult-ls-02 | proved | all subs proved
| div-elim-pospos,
mult-ls,
|
| mult-split-mod | proved | all subs proved
| div-mult-03,
mod-mult-04,
div-add-pos,
div-elim-pospos,
|
| div-mult-le-01 | proved | all subs proved
| div-elim-pospos,
divmult,
|
| div-ls | proved | all subs proved
| div-elim-pospos,
div-mult-03,
modex,
|
| div-elim-negpos | proved | all subs proved
| div-elim2,
mod-less-01,
mod-grz,
mod-mult-neg,
div-mult-neg,
div-lezero,
divmod-rew,
|
| div-add-succ | proved | all subs proved
| div-zero,
div-mult-03,
mod-mult-04,
div-elim-pospos,
div-same,
mod-same,
div-add-pos,
|
| div-eq-zero | proved | all subs proved
| div-elim-pospos,
|
| div-zero-nls | proved | all subs proved
| div-elim-pospos,
|
| square-inject | proved | all subs proved
| div-elim-pospos,
|
| modmod-pos | proved | all subs proved
| mod-same,
mod-zero-03,
mod-mult-04,
mod-mult-02,
mod-add-pos,
div-elim-pospos,
|
| modmod-add-04 | proved | all subs proved
| mod-mult-04,
mod-add-pos,
div-elim-pospos,
|
| modeven-pos | proved | all subs proved
| mod-two-04,
div-elim-pos,
|
| mod-zero-07 | proved | all subs proved
| div-elim-pospos,
|
| mod-pred-03 | proved | all subs proved
| mod-mult-04,
modeq-pos,
div-elim-pospos,
|
| mod-pred-02 | proved | all subs proved
| div-elim-pos,
div-elim-pospos,
|
| mod-nle | proved | all subs proved
| div-elim-pospos,
|
| mod-mult-neg-01 | proved | all subs proved
| mod-mult-neg,
|
| mod-add-zero | proved | all subs proved
| div-elim-pospos,
mod-zero-01,
|
| le-norest | proved | all subs proved
| div-elim-pospos,
|
| div-zero-03 | proved | all subs proved
| div-elim-pospos,
|
| div-twoodd-01 | proved | all subs proved
| divmult,
Div-left,
mod-neg-01,
div2-odd,
two-even,
num-neg,
|
| div-shift-two | proved | all subs proved
| mult-02,
div-elim-pospos,
div-div-pos,
|
| div-mult-three-nls | proved | all subs proved
| div-elim-pospos,
|
| div-mult-nls-est-01 | proved | all subs proved
| div-elim-pospos,
|
| div-mult-nls-est | proved | all subs proved
| div-elim-pospos,
|
| div-mult-nle-est | proved | all subs proved
| div-elim-pospos,
|
| div-le-modnotzero | proved | all subs proved
| div-elim-pospos,
|
| div-est-nls | proved | all subs proved
| div-elim-pospos,
|
| div-est-nle-pos | proved | all subs proved
| div-elim-pospos,
|
| div-est-denom-pos | proved | all subs proved
| div-elim-pospos,
|
| div-am-rew | proved | all subs proved
| div-mult-03,
mod-mult-04,
div-add-pos,
div-elim-pospos,
|
| div-addthree-rew | proved | all subs proved
| div-mult-03,
div-mult-pos-03,
div-add1-pospos,
div-elim-pospos,
|
| modeven-neg-01 | proved | all subs proved
| mod-two-02,
div-elim2,
modeven-neg,
|
| mod-two-04 | proved | all subs proved
| mod-mult-pos,
|
| div2-odd | proved | all subs proved
| divmult,
two-even,
div-add-pos,
|
| mod-mult-neg | proved | all subs proved
| mod-mult-pos,
mod-zero-05,
mod-neg-01,
|
| div-mult-pos-03 | proved | all subs proved
| div-mult-pos-01,
|
| div-elim-pospos | proved | all subs proved
| div-elim-pos,
mod-mult-pos,
div-mult-pos,
mod-less-01,
mod-zero,
divmod-rew,
|
| two-odd | proved | all subs proved
| two-mult-01,
nummult-eq-01,
mod-two-02,
exeven,
two-even,
|
| mod2-add-neg | proved | all subs proved
| mod-two-03,
div-elim2,
mod-two-02,
div-elim-pos,
mod-neg-01,
|
| mod-twoeven | proved | all subs proved
| nummult-eq-01,
div-mult-num,
mod-mult-02,
mod-two-02,
exeven,
|
| mod-by6 | proved | all subs proved
| mod-zero-num,
mod-add1-pospos,
modby6-help,
|
| mod-add1-negneg | proved | all subs proved
| mod-add-neg,
|
| exodd | proved | all subs proved
| nummult-eq-01,
div-elim-pos,
|
| exeven | proved | all subs proved
| nummult-eq-01,
div-elim2,
div-elim-pos,
|
| mod-add1-pospos | proved | all subs proved
| mod-add-pos,
|
| mod-two-02 | proved | all subs proved
| mod-zero-num,
|
| two-even | proved | all subs proved
| div-mult-num,
divmult,
|
| mod-mult-pos | proved | all subs proved
| mod-zero-05,
mod-mult-04,
mod-add-pos,
|
| div-add1-negneg | proved | all subs proved
| div-add-neg,
|
| div-mult-num-01 | proved | all subs proved
| div-div-switch,
|
| div-add1-pospos | proved | all subs proved
| div-add-pos,
|
| div-mult-pos-01 | proved | all subs proved
| div-mult-03,
mod-mult-04,
div-add-pos,
|
| mod-twoodd-03 | proved | all subs proved
| nummult-eq-01,
mod-twoodd,
mod-neg-01,
|
| mod-mult-03 | proved | all subs proved
| nummult-eq-01,
mod-mult-02,
|
| div-le-modzero-01 | proved | all subs proved
| mult-ls-01,
div-ls-modzero,
|
| mod-lsz | proved | all subs proved
| mod-zero-01,
div-elim2,
mod-less-01,
|
| mod-add-pos | proved | all subs proved
| modeq-pos,
div-elim-pos,
mod-less-01,
|
| mod-add-neg | proved | all subs proved
| mod-zero-05,
mod-mult-04,
modeq-neg,
div-elim2,
mod-less-01,
|
| nummult-eq-01 | proved | all subs proved
| div-mult-03,
modex,
mult-div-switch,
|
| div-div-switch | proved | all subs proved
| div-mult-01,
div-mult-03,
modex,
|
| div-add-both | proved | all subs proved
| div-mult-03,
modex,
|
| div-ls-modzero | proved | all subs proved
| div-mult-03,
modex,
mult-ls-01,
|
| mod-zero-num | proved | all subs proved
| mod-mult-04,
modex,
|
| div-mult-num | proved | all subs proved
| div-mult-03,
modex,
|
| div-add-neg | proved | all subs proved
| diveq-neg,
div-elim2,
mod-less-01,
|
| div-add-pos | proved | all subs proved
| diveq-pos,
div-elim-pos,
mod-less-01,
|
| nummult-modls-01 | proved | all subs proved
| div-mult-03,
modex,
|
| nummult-modle-01 | proved | all subs proved
| div-mult-03,
modex,
|
| mod-mod-less | proved | all subs proved
| modmod-mult-03,
modex,
|
| mod-less | proved | all subs proved
| mod-less-01,
|
| mod-add-both-zero | proved | all subs proved
| mod-mult-04,
modex,
|
| div-sub-01 | proved | all subs proved
| div-mult-03,
modex,
|
| div-le-modzero | proved | all subs proved
| mult-ls,
div-mult-03,
modex,
|
| mod-less-01 | proved | all subs proved
| mod-les,
|
| modex | proved | all subs proved
| div-elim3,
div-elim2,
div-elim1,
div-elim-pos,
mod-mult-04,
|
| one-05 | proved | all subs proved
| one-03,
modnum-neg,
|
| nummult-eq | proved | all subs proved
| mult-div-switch,
div-mult-03,
mod-mult-04,
|
| modmod-law-mult | proved | all subs proved
| modmod-mult-01,
|
| modmod-add-03 | proved | all subs proved
| mod-grz-01,
modmod-add-02,
|
| mod-two-pred | proved | all subs proved
| mod-two-03,
|
| mod-succ | proved | all subs proved
| one-03,
mod-add,
|
| mod-nle-01 | proved | all subs proved
| mod-les,
|
| mod-neq-02 | proved | all subs proved
| mod-les,
|
| mod-le-num | proved | all subs proved
| mod-nls-01,
|
| mod-le-01 | proved | all subs proved
| mod-nls-01,
|
| two-mult-01 | proved | all subs proved
| mult-05,
|
| modmod-mult-01 | proved | all subs proved
| mod-neg,
modmod-mult-02,
|
| mod-two-03 | proved | all subs proved
| modeq-pos-04,
|
| one-03 | proved | all subs proved
| mod-zero-09,
|
| mod-nls-01 | proved | all subs proved
| mod-pos-not-neg,
div-elim-pos,
|
| mod-les | proved | all subs proved
| div-elim-pos,
mod-pos-not-neg,
|
| ls-even | proved | all subs proved
| divmult,
num-ls,
|
| div-twoodd-04 | proved | all subs proved
| neg,
div-twoodd-03,
num-neg-01,
|
| mod-one | proved | all subs proved
| one-01,
|
| mod-same | proved | all subs proved
| div-same,
mod-rew,
|
| mod-mult-04 | proved | all subs proved
| div-mult-03,
mod-rew,
|
| mod-grz-01 | proved | all subs proved
| div-elim-negneg,
mod-pos-not-neg,
mod-grz,
|
| mod-ngez | proved | all subs proved
| mod-ngr,
|
| mod-ngez-01 | proved | all subs proved
| mod-grz-02,
|
| nummult-ls-01-01 | proved | all subs proved
| mult-ls-01,
nummult-ls-01,
|
| mod-zero-08 | proved | all subs proved
| mod-zero-09,
|
| div-twoodd-06 | proved | all subs proved
| mult-02,
div-twoodd-02,
|
| div-sub | proved | all subs proved
| div-mult-03,
|
| div-mult | proved | all subs proved
| div-mult-03,
|
| div-mone | proved | all subs proved
| div-mone-01,
|
| div-ls-pos-better | proved | all subs proved
| mult-ls,
num-ls,
|
| div-elim-divides | proved | all subs proved
| div-mult-03,
divmult,
|
| mult-05 | proved | all subs proved
| one,
mult-04,
|
| nummult-ls-01 | proved | all subs proved
| div-elim2,
mult-ls-01,
|
| modmod-mult-02 | proved | all subs proved
| mod-neg-01,
modmod-mult,
|
| modmod-add-02 | proved | all subs proved
| mod-neg-01,
modmod-add-01,
|
| mod-zero-09 | proved | all subs proved
| mod-zero-05,
|
| mod-twoodd | proved | all subs proved
| divmod-rew,
div-twoodd,
mod-rew,
|
| modeq-pos-04 | proved | all subs proved
| mod-neg-01,
modeq-pos-03,
|
| mod-grz-02 | proved | all subs proved
| div-elim-negneg,
|
| mod-ngr | proved | all subs proved
| mod-grz,
|
| mod-two-01 | proved | all subs proved
| mod2-neg-odd,
|
| mod-ls-zero | proved | all subs proved
| mod-grz,
mod-zero-01,
|
| mod-pos-not-neg | proved | all subs proved
| mod-grz,
|
| mod-not-less | proved | all subs proved
| div-elim-negneg,
|
| div-twoodd-02 | proved | all subs proved
| neg,
div-twoodd,
num-neg-01,
|
| div-twoodd-03 | proved | all subs proved
| neg-01,
div-twoodd,
nummult-ls,
num-neg,
|
| div-mone-01 | proved | all subs proved
| one,
num-neg-01,
|
| num-ls | proved | all subs proved
| div-elim-pos,
mult-ls,
|
| div-mult-neg | proved | all subs proved
| div-mult-pos,
Div-left,
|
| one-01 | proved | all subs proved
| one,
mod-rew,
|
| div-same | proved | all subs proved
| zero,
div-rec-01,
div-rec,
|
| div-mult-03 | proved | all subs proved
| one,
div-mult-01,
|
| zero-01 | proved | all subs proved
| div-lezero,
|
| sub-ls | proved | all subs proved
| div-lezero,
|
| nummult-ls-03-01 | proved | all subs proved
| nummult-ls-03,
|
| nummult-le-03-01 | proved | all subs proved
| nummult-le-03,
|
| nummult-le-01-01 | proved | all subs proved
| nummult-le-01,
|
| modmod-ma | proved | all subs proved
| mod-zero-01,
mod-zero-02,
modmod-mult,
modmod-add,
|
| modmod | proved | all subs proved
| modmod-mult-05,
|
| mod-twoodd-02 | proved | all subs proved
| mod-mult-02,
div-elim-pos,
|
| mod-sub | proved | all subs proved
| mod-neg-01,
mod-add,
|
| mod-mult-01 | proved | all subs proved
| mod-mult-02,
|
| lsfc-02 | proved | all subs proved
| zero-04,
|
| less-mult-div | proved | all subs proved
| div-lezero,
|
| div2-nle-01 | proved | all subs proved
| div-lezero,
|
| div-mult-three | proved | all subs proved
| nummult-ls,
div-lezero,
|
| div-mult-pos-02 | proved | all subs proved
| div-mult-pos,
|
| div-le-modnotzero-01 | proved | all subs proved
| div-ls-modnotzero,
|
| zero-06 | proved | all subs proved
| div-elim3,
|
| nummult-ls-03 | proved | all subs proved
| div-elim2,
|
| mult-04 | proved | all subs proved
| mult-03,
|
| modmod-mult | proved | all subs proved
| div-elim2,
modeq-pos-02,
div-elim-pos,
|
| modmod-add-01 | proved | all subs proved
| mod-neg,
modmod-add,
|
| modmod-mult-05 | proved | all subs proved
| mod-neg,
modmod-mult-03,
|
| modeven-neg | proved | all subs proved
| div-elim2,
|
| modeq-pos-03 | proved | all subs proved
| modeq-pos-01,
div-elim2,
|
| mod2-neg-odd | proved | all subs proved
| div-elim2,
|
| mod-add | proved | all subs proved
| mod-rec,
|
| modeq-neg | proved | all subs proved
| div-elim2,
|
| mod-zero-05 | proved | all subs proved
| div-elim2,
mod-zero-03,
|
| zero-04 | proved | all subs proved
| div-elim,
div-elim-pos,
div-elim2,
|
| nummult-le-03 | proved | all subs proved
| div-elim2,
|
| div-zero-01 | proved | all subs proved
| div-elim2,
|
| mod-mult-02 | proved | all subs proved
| divmod-rew,
div-mult-01,
mod-rew,
|
| div-twoodd | proved | all subs proved
| mult,
mult-02,
div-elim-pos,
|
| div-rec-01 | proved | all subs proved
| minus-add,
neg,
neg-01,
div-rec,
|
| mult-ls-01 | proved | all subs proved
| div-elim-pos,
div-elim2,
|
| mult-ls | proved | all subs proved
| div-elim-pos,
div-elim2,
|
| div-ls-modnotzero | proved | all subs proved
| nummult-le-04,
|
| div-elim-negneg | proved | all subs proved
| div-elim3,
|
| mod-grz | proved | all subs proved
| div-elim2,
|
| nummult-le-01 | proved | all subs proved
| div-elim2,
div-elim-pos,
|
| div-mult-pos | proved | all subs proved
| mult,
|
| one | proved | all subs proved
| div-elim2,
div-elim-pos,
|
| diveq-neg | proved | all subs proved
| div-elim2,
|
| div-lezero | proved | all subs proved
| div-elim-pos,
div-elim2,
div-elim,
|
| div-zero-ngr-01 | proved | all subs proved
| div-elim-posneg,
|
| two-mult | proved | all subs proved
| mult-03,
|
| mult-01 | proved | all subs proved
| neg,
mult,
|
| modeq-neg-02 | proved | all subs proved
| div-elim2,
div-elim-pos,
|
| mod-rec-01 | proved | all subs proved
| mod-neg,
mod-neg-01,
mod-rec,
|
| mod-mult | proved | all subs proved
| divmod-rew,
div-mult-01,
mod-rew,
|
| div2-notzero | proved | all subs proved
| div-elim2,
|
| div-two-01 | proved | all subs proved
| div-mult-01,
|
| div-ls-02 | proved | all subs proved
| ls-03,
|
| mult-03 | proved | all subs proved
| mult-02,
|
| modmod-add | proved | all subs proved
| modeq-pos-02,
div-elim-pos,
|
| modmod-mult-03 | proved | all subs proved
| mod-neg-01,
mod-neg,
modmod-mult-04,
|
| mod-rec | proved | all subs proved
| div-elim-pos,
div-elim,
|
| div-rec | proved | all subs proved
| div-elim,
div-elim-pos,
|
| mult | proved | all subs proved
| zero,
div-elim,
|
| nummult-le-04 | proved | all subs proved
| nummult-le,
|
| ls-03 | proved | all subs proved
| ls-01,
|
| div-elim-posneg | proved | all subs proved
| div-elim1,
|
| div-mult-01 | proved | all subs proved
| neg,
Div-right,
neg-01,
div-mult-02,
|
| div-div-pos | proved | all subs proved
| mult-02,
div-elim-pos,
|
| div-elim2 | proved | all subs proved
| divmod-rew,
mod-neg-01,
neg-01,
div-elim,
|
| div-elim3 | proved | all subs proved
| mod-neg,
mod-neg-01,
neg,
neg-01,
div-elim,
|
| one-neg | proved | all subs proved
| div-elim1,
div-elim,
|
| nummult-modls | proved | all subs proved
| div-elim,
|
| nummult-modle | proved | all subs proved
| div-elim,
|
| nummult-ls-04 | proved | all subs proved
| nummult-ls,
|
| nummult-le-02-01 | proved | all subs proved
| nummult-le-02,
|
| mod-four | proved | all subs proved
| mod-zero-03,
|
| estimate-01 | proved | all subs proved
| div-elim,
|
| div-zero-05 | proved | all subs proved
| div-zero,
|
| nummult-le | proved | all subs proved
| div-elim-pos,
|
| modmod-mult-04 | proved | all subs proved
| modeq-pos,
div-elim-pos,
|
| modeq-pos-02 | proved | all subs proved
| modeq-pos,
div-elim-pos,
|
| mod-zero-03 | proved | all subs proved
| div-elim-pos,
|
| ls-01 | proved | all subs proved
| div-elim-pos,
|
| div-mult-02 | proved | all subs proved
| div-elim-pos,
|
| div-elim | proved | all subs proved
| div-elim-pos,
|
| div-elim1 | proved | all subs proved
| mod-neg,
neg,
div-elim-pos,
|
| nummult-ls | proved | all subs proved
| div-elim-pos,
|
| nummult-le-02 | proved | all subs proved
| div-elim-pos,
|
| mult-02 | proved | all subs proved
| div-elim-pos,
|
| div-zero | proved | all subs proved
| div-elim-pos,
|
| div-elim-pos | proved | all subs proved
| modeq-pos,
diveq-pos,
mod-ls-same,
mod-zero,
divmod-rew,
|
| mod-abs-intro | proved | all subs proved
| mod-abs,
|
| mult-div-switch | proved | all subs proved
| divmult,
|
| modnum-neg | proved | all subs proved
| mod-neg-01,
|
| mod-zero-02 | proved | all subs proved
| mod-zero-01,
|
| modeq-pos-01 | proved | all subs proved
| modeq-pos,
|
| modnum-neg-01 | proved | all subs proved
| mod-neg,
|
| mod-abs | proved | all subs proved
| mod-neg,
|
| mod-zero | proved | all subs proved
| mod-zero-01,
|
| mod-zero-ls | proved | all subs proved
| mod-zero-01,
|
| mod-ls-same | proved | all subs proved
| ls-same-pos-01,
mod-rew,
|
| modeq-pos | proved | all subs proved
| diveq-pos,
mod-rew,
|
| divmult | proved | all subs proved
| mod-rew,
|
| mod-zero-04 | proved | all subs proved
| zero,
mod-rew,
|
| mod-neg-01 | proved | all subs proved
| divmod-rew,
Div-left,
mod-rew,
|
| mod-zero-01 | proved | all subs proved
| ls-same-pos-02,
mod-rew,
|
| mod-neg | proved | all subs proved
| divmod-rew,
Div-right,
mod-rew,
|
| div2one-01 | proved | all subs proved
| mod-rew,
|
| mod-rew | proved | all subs proved
| divmod-rew,
|
| num-neg | proved | all subs proved
| neg-01,
|
| minus-add | proved | all subs proved
| neg-01,
|
| abs-intro | proved | all subs proved
| neg,
neg-01,
|
| num-neg-01 | proved | all subs proved
| neg,
|
| zero | proved | all subs proved
| neg,
Div-def,
|
| mod-sub-02 | proved | all subs proved
| is-div,
divmod-rew,
|
| div2one | proved | all subs proved
| divmod-rew,
|
| is-div | proved | all subs proved
| Div-def,
|
| ls-same-pos-01 | proved | all subs proved
| Div-def,
|
| ls-same-pos | proved | all subs proved
| Div-def,
|
| ls-same-pos-02 | proved | all subs proved
| Div-def,
|
| divmod-rew | proved | all subs proved
| Mod-def,
|
| diveq-pos | proved | all subs proved
| Div-def,
|
| neg | proved | all subs proved
| Div-right,
|
| neg-01 | proved | all subs proved
| Div-left,
|
| modby6-help | proved | all subs proved
| |
| Mod-def | axiom | | |
| Div-def | axiom | | |
| Div-left | axiom | | |
| Div-right | axiom | | |