[Imprint][Data Privacy Statement][E-Mail]
View long theorem info.
View the proof.
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
Theorem commutativity
- Type: A user defined theorem
- Validity: The proof is valid.
- Features: simp,
localsimp,
- Comment:
- Used by: 5-not-even,
7-not-even,
abs-eqall,
abs-eqneg,
abs-ls-same,
abs-ls-same-01,
add-mult-two,
associativity,
auxexdivmod,
auxexdivmod-01,
dist-lsplit,
dist-rmerge,
dist-sub-merge,
dist-sub-split,
eq-dist,
eq-neg,
eq-nonzero,
eq-nonzero-01,
eq-nonzero-02,
eq-nonzero-03,
eq-one,
eq-one-neg,
eq-pos,
eq-pos-01,
eq-same,
eq-same-01,
eq-same-02,
eq-same-03,
eq-succ,
est-nle,
ex-two,
exdivmod,
exdivmodpos,
four,
le-abs,
le-dist,
le-dist-01,
le-dist-02,
le-neg,
le-neg-01,
le-one,
le-pos,
le-pos-01,
le-same,
le-same-01,
le-same-02,
le-same-03,
le-same-04,
le-same-05,
le-same-06,
le-two,
ls-add,
ls-add-02,
ls-add-03,
ls-dist,
ls-dist-01,
ls-dist-02,
ls-dist-03,
ls-dist-04,
ls-dist-05,
ls-dist-06,
ls-forward,
ls-neg,
ls-pos,
ls-pos-01,
ls-same,
ls-same-01,
ls-same-02,
ls-same-03,
ls-same-04,
ls-same-05,
ls-same-06,
ls-sub,
ls-two,
ls-two-01,
ls-two-02,
ls-two-03,
minus-left,
minus-one,
minus-one-01,
minus-one-02,
mod-neq,
mod-nle,
mod-nls,
modeqp,
modeqp-02,
modeqp-03,
modeqp-copied,
modeqp-neg,
modlep,
modlep-03,
modlep-04,
modlsp,
modlsp-03,
modlsp-04,
modlsp-06,
modneqp,
mods-ls,
mods-ls-01,
mods-ls-02,
mods-ls-03,
mods-ls-04,
mods-nls,
mods-zero-07,
modzero,
modzero-01,
modzero-02,
modzero-03,
modzero-04,
modzero-05,
modzero-06,
modzero-07,
modzero-08,
mult-add-greater,
mult-gt-both,
mult-gt-one,
mult-pos,
mult-pos-pos,
mult-sub-less,
mult-sub-lesseq,
neq-3-not-even,
neq-5-not-even,
neq-7-not-even,
neq-9-not-even,
neq-not-zero,
neq-not-zero-01,
neq-two,
noeth-ls-pos,
noeth-modlep,
noeth-zero-ls,
numabs,
numabs-01,
numdist,
numeq,
numeq-01,
numeq-02,
numeq-03,
numeq-04,
numle,
numle-01,
numle-02,
numle-03,
numle-04,
numle-05,
numle-06,
numle-07,
numle-08,
numle-09,
numle-10,
numle-11,
numle-12,
numle-13,
numleneg,
numleneg-01,
numleneg-02,
numleneg-03,
numls,
numls-01,
numls-02,
numls-03,
numls-04,
numls-05,
numls-06,
numls-07,
numls-08,
numls-09,
numls-10,
numls-11,
numls-12,
numls-13,
numlsneg,
numlsneg-01,
numlsneg-02,
numlsneg-03,
numsub,
numsucc,
odd-even,
one-01,
ple-pos,
ple-pos-better,
pls-neg,
pls-pos,
pls-pos-01,
pls-pos-02,
pnle-pos,
pnls-negpos,
pnls-pos,
pnls-posneg,
pred-rmerge,
short-mult-max,
square-abs,
square-eq,
square-eq-01,
square-even,
square-ex,
square-gez,
square-gez-01,
square-gez-02,
square-inject,
square-interval,
square-le,
square-le-01,
square-le-02,
square-le-03,
square-le-04,
square-le-06,
square-lez-01,
square-ls,
square-ls-01,
square-ls-02,
square-ls-04,
square-minus,
square-one-le,
square-zero,
square-zero-01,
square-zero-02,
succ-rmerge,
three,
three-01,
two-le,
two-le-01,
two-le-02,
two-le-03,
two-le-04,
two-leone,
two-ls,
two-ls-01,
two-ls-02,
two-ls-03,
two-ls-04,
two-mone,
two-oddeq,
two-pred,
two-sub,
two-sub-01,
two-zero,
zero-eq,
zero-ge,
zero-ge-01,
zero-ge-02,
zero-ge-03,
zero-ge-add,
zero-ge-add-01,
zero-ge-add-02,
zero-ge-case,
zero-gr,
zero-gr-01,
zero-gr-02,
zero-gr-03,
zero-gr-add,
zero-gr-add-01,
zero-gr-add-02,
zero-gr-case,
zero-le,
zero-le-01,
zero-le-02,
zero-le-03,
zero-le-case,
zero-ls,
zero-ls-01,
zero-ls-02,
zero-ls-03,
zero-ls-case,
zero-ls-sub,
zero-ls-two,
zero-neq,
zero-neq-01,
- Used by units in proved state:
int-pot,
int-gcd,
int-div,
intnat,
int-square,
int-pair,
int-min,
- Proof exists?: Yes
Infos about the proof