[Imprint][Data Privacy Statement][E-Mail]

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,

Lemma dependency for Specification int-pot

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:
div-div-rec-01provedall subs proved div-div-rec,
add-eq2pot-01provedall subs proved add-eq2pot, succ,
div-div-recprovedall subs proved ls-mult-2pot, two-zero, two-lsz, succ, two-lez-01, zero, pot2-pos,
add-eq2potprovedall subs proved ls-pos-2pot, two-minus, pot-dist-pos,
two-lsprovedall subs proved two-le-01, pot2-pos, pot2-pos-01,
pot2-le-pred-01provedall subs proved pot2-ls-pred,
pot-div3-nlsprovedall subs proved pot-nls, Pot-pos,
mod-two-lsprovedall subs proved pot2-pos, ls-pos-2pot, two-lsz,
mod-two-geprovedall subs proved pot-dist-pos, div-twopot, two-zero,
ls-pos-2pot-01provedall subs proved ls-pos-2pot,
lemon2pot-01provedall subs proved lemon2pot,
le-2pot-01provedall subs proved succ, ls-pos-2pot, Pot-pos,
le-2potprovedall subs proved ls-pos-2pot, Pot-pos,
exin2pot-negprovedall subs proved pot2-ls-pred, two-le, pot2-pos, ls-2pot, succ, exin2pot,
two-le-01provedall subs proved two-le,
pot-nlsprovedall subs proved one-01, one, ls-pos,
div-twopotprovedall subs proved eq-two, two-zero, two-le, two-lsz, two-lez, two-minus, pot-dist-pos,
lemon2potprovedall subs proved ls-pos,
pot2-ls-predprovedall subs proved two-le, two-lsz, two-minus,
ls-mult-2potprovedall subs proved grz, two-le, ls-pos, two-minus, pot-dist-pos,
ls-pos-2potprovedall subs proved ls-pos,
pot2-ls-pred-01provedall subs proved pot2-pos-01, two-lsz, two-leone, Pot-neg, Pot-pos,
pot2-le-predprovedall subs proved two-lsz, 2pot-leone, two-leone, Pot-neg, Pot-pos,
pot-root-estprovedall subs proved le-pos, pot-square-est, pot-square-04, notneg-02, ls-pos-03, pot-pot-02, notneg,
mod-two-ls-01provedall subs proved two-lez, two-le,
mod-two-ge-01provedall subs proved pot-dist-pos, pot2-pos, pot2-pos-01, two-zero,
lemon2pot-02provedall subs proved ls-pos,
exinpotprovedall subs proved ls-pos, Pot-zero, succ,
div2provedall subs proved 2pot-leone, zero-02, Pot-neg, two-minus, Pot-pos,
pot-square-estprovedall subs proved pot-square-est-div6,
pot2-pos-01provedall subs proved two-leone, pot2-pos,
ls-posprovedall subs proved le-pos,
exin2potprovedall subs proved pot-dist-pos, pot2-pos, Pot-pos, two-leone,
ls-2potprovedall subs proved pot2-pos,
2pot-leoneprovedall subs proved two-minus, two-lez-01,
two-leprovedall subs proved le-pos,
twopot-mone-divprovedall subs proved pot2-pos, eq-one, two-zero, Pot-pos,
pot2-pos-03provedall subs proved two-minus, pot2-pos,
pot-lezprovedall subs proved one-01, eqone-02, zero-02, Pot-neg, pot-zero-01, notneg-02,
mod2-2pot-06provedall subs proved mod2-2pot-05,
mod-ngez-01provedall subs proved pot2-pos,
mod-ngezprovedall subs proved pot2-pos,
mod-lesameprovedall subs proved pot2-pos,
mod-add1-posposprovedall subs proved pot2-pos, zero,
mod-add1-negnegprovedall subs proved pot2-pos, zero,
ls-2pot-01provedall subs proved pot2-pos,
divmod2-2pot-negprovedall subs proved div2-2pot-04, mod-2pot, pot2-pos,
divmod2-2potprovedall subs proved mod2-2pot-01,
pot-square-est-div6provedall subs proved pot2-est-div6, two-lsz, le-pos-01, pot-square-03, pot-pot-02, pot-pot,
ls-pos-03provedall subs proved le-pos-01, ls-pos-02,
pot-zero-01provedall subs proved one-01, eqone-02, grz, Pot-neg,
mod2-2pot-05provedall subs proved grz,
le-posprovedall subs proved notone, Pot-neg, notneg-01, grz, Pot-zero, Pot-pos,
mod2-2pot-01provedall subs proved two-lez, two-zero, Pot-pos,
pot2-posprovedall subs proved grz,
two-lez-01provedall subs proved two-lez, two-minus,
two-zero-01provedall subs proved two-zero,
two-mod-01provedall subs proved two-mone, Pot-pos,
pred-leprovedall subs proved two-lez, succ,
pot2-pos-05provedall subs proved pot2-pos-02,
mod2-posprovedall subs proved grz,
mod2-2pot-02provedall subs proved two-lez, Pot-pos,
mod2-2potprovedall subs proved two-lez, Pot-pos,
div2-2pot-01provedall subs proved Pot-pos, two-lez,
div2-2potprovedall subs proved Pot-pos, two-lez,
two-moneprovedall subs proved notneg-01,
pot2-pos-02provedall subs proved two-lsz,
le-pos-01provedall subs proved Pot-zero, notneg, succ, ls-pos-01,
grzprovedall subs proved notneg-01, one-01, zero-03, zero-02, Pot-neg, eqone-01,
two-lezprovedall subs proved notneg-01,
two-zeroprovedall subs proved notneg-01,
twolezeroprovedall subs proved notneg-01,
pot2-pos-04provedall subs proved two-lsz,
mod2-2pot-04provedall subs proved two-lsz, Pot-pos,
div2-2pot-03provedall subs proved two-lsz, Pot-pos,
abs-2potprovedall subs proved two-lsz,
ls-pos-01provedall subs proved ls-pos-02,
notneg-01provedall subs proved notneg-02, Pot-zero, zero,
two-lszprovedall subs proved notneg-02,
minus-oddprovedall subs proved minus-square, Pot-pos,
equal-minus-oneprovedall subs proved minus-one-odd, zero-02, one-01, Pot-pos, zero-01, Pot-neg, minus-one-even, Pot-zero,
notneg-02provedall subs proved zero-03, zero-02, Pot-neg, notneg,
minus-squareprovedall subs proved pot-square-02, pot-square,
ls-pos-02provedall subs proved Pot-neg, notneg, succ, Pot-zero,
minus-one-evenprovedall subs proved one-01, pot-square,
minus-one-oddprovedall subs proved one-01, pot-square, succ,
pot-squareprovedall subs proved pot-square-02,
notnegprovedall subs proved one-01, Pot-zero, Pot-pos, notone,
square-mod-fourprovedall subs proved mod-next-square,
pot2-succ-01provedall subs proved pot2-succ,
pot-square-01provedall subs proved pot-square-02,
mod-next-squareprovedall subs proved pot-square-04,
pot2-succprovedall subs proved eq-two, succ,
pot-square-02provedall subs proved pot-square-04, pot-pot-02,
zero-03provedall subs proved zero-02,
one-01provedall subs proved zero-02, Pot-neg, one-02,
pot2-div2provedall subs proved eq-two, succ,
pot2-addprovedall subs proved eq-two, succ,
pot-pot-01provedall subs proved pot-pot-03,
mod-lezprovedall subs proved mod-lsz,
minus-square-01provedall subs proved pot-square-05, pot-square-04,
eq2provedall subs proved eqone-01, two-leone, Pot-neg, Pot-pos,
eq-oneprovedall subs proved two-minus, eq-pos,
pot-square-03provedall subs proved pot-square-05,
pot-pot-03provedall subs proved pot-pot-02,
mod-lszprovedall subs proved zero,
pot-square-04provedall subs proved pot-square-05,
two-leoneprovedall subs proved two-minus, notone,
div2-2pot-04provedall subs proved div2-2pot-neg, div2-2pot-02,
zero-02provedall subs proved zero,
eq-twoprovedall subs proved eq-pos,
two-minus-01provedall subs proved two-minus,
square-nlsprovedall subs proved pot-square-05,
pot-sub-distprovedall subs proved Pot-zero, zero, pot-dist-pos,
pot-divprovedall subs proved Pot-zero, zero, pot-dist-pos,
pot-potprovedall subs proved pot-dist-pos, Pot-zero, Pot-pos,
pot2-est-div6provedall subs proved pot2-est-mult8, Pot-pos,
pot-pot-02provedall subs proved pot-dist-pos, Pot-zero, Pot-pos,
eqone-02provedall subs proved eqone-01,
pot-square-05provedall subs proved one, Pot-pos,
eq-posprovedall subs proved eqone-01, Pot-zero, Pot-pos,
mod-2potprovedall subs proved mod2-2pot-03,
div2-2pot-negprovedall subs proved div2-2pot-02,
zeroprovedall subs proved Pot-zero, Pot-pos, zero-01,
two-minusprovedall subs proved notone, Pot-neg,
pot-square-est-02provedall subs proved succ,
pot-square-est-01provedall subs proved Pot-neg, succ,
one-03provedall subs proved one,
mod-pot-shift-posprovedall subs proved succ, Pot-pos, Pot-zero,
ls-sameprovedall subs proved succ,
le-sameprovedall subs proved succ,
le-2pot-succprovedall subs proved succ,
geom-modprovedall subs proved succ, Pot-zero,
pot2-est-mult8provedall subs proved Pot-pos,
oneprovedall subs proved Pot-zero, Pot-pos,
one-02provedall subs proved Pot-pos,
mod2-2pot-03provedall subs proved Pot-pos,
notoneprovedall subs proved Pot-zero, Pot-pos,
zero-01provedall subs proved Pot-pos,
eqone-01provedall subs proved Pot-pos,
div2-2pot-02provedall subs proved Pot-pos,
succprovedall subs proved Pot-pos,
pot-dist-posprovedall subs proved Pot-zero, Pot-pos,
two-modprovedall subs proved Pot-pos,
pot2-sublsprovedall subs proved Pot-pos,
pot2-subleprovedall subs proved Pot-pos,
pot2-mod2-zeroprovedall subs proved Pot-pos,
mod-sameprovedall subs proved Pot-pos,
eqoneprovedall subs proved Pot-pos,
Pot-zeroaxiom
Pot-posaxiom
Pot-negaxiom