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