[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-mod

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:
RSA-decrypt-ij-varsprovedall subs proved fermat-for-rsa, congmod-def-mod, congmod-def-mod-01, mod-crt, mod-pot-pot, mod-zero-03, congmod-def, mod-zero,
fermat-for-rsaprovedall subs proved mod-mod, mod-zero-03, mod-mult-01, fermat-2-mod, mod-mult-law,
fermat-2-modprovedall subs proved mod-one, mod-zero, congmod-def-mod, fermat-2,
fermat-2provedall subs proved fermat-1, cong-mult-rew, congmod-inverse,
fermat-1-modprovedall subs proved congmod-def-mod, fermat-1,
Lagrange-SumOf4Squaresprovedall subs proved Lagrange-SumOf4Squares-primes, lagrange-primedivisors,
fermat-1provedall subs proved cong-neg, congmod-def, cong-same, fermat-pos,
Lagrange-SumOf4Squares-primesprovedall subs proved four-square-mod-zero, four-square-odd-ls, four-square-congmod, four-square-divides-all, congmod-def, ex-modeq-half-all, even-sum, lagrange-lemma-smallest,
fermat-posprovedall subs proved cong-add, cong-zero, cong-same-add, cong-same,
lagrange-lemma-smallestprovedall subs proved lagrange-lemma,
lagrange-lemmaprovedall subs proved congmod-def, congmod-def-mod, diff-primes-neg, diff-primes, diff-primes-dups,
cong-addprovedall subs proved cong-mult,
ex-modeq-half-allprovedall subs proved ex-modeq-half,
congmod-inverse-smallestprovedall subs proved mod-zero, mod-mult-add, mod-mod, mod-mult-law, mod-zero-01, mod-one, mod-pos-def, congmod-def, congmod-def-mod, mod-le-same, mod-pos, cong-one, cong-zero, congmod-inverse-pos,
Diffie-Hellmanprovedall subs proved mod-pot-pot,
diff-primesprovedall subs proved congmod-def, congmod-def-mod,
diff-primes-negprovedall subs proved congmod-def, congmod-def-mod,
ex-modeq-halfprovedall subs proved mod-neg-def, mod-pos-def, mod-le-same, mod-mod, congmod-def-mod,
congmod-inverse-posprovedall subs proved mod-one, mod-zero, congmod-def-mod, rem-mod-pos, cong-zero, cong-one, cong-same, congmod-inverse,
cong-multprovedall subs proved mod-mult-add, congmod-def, congmod-def-mod,
mod-crtprovedall subs proved congmod-def-mod, cong-crt-01,
congmod-def-mod-01provedall subs proved mod-zero, mod-pos-def, mod-neg-def, congmod-def-mod, congmod-mod-abs,
mod-pot-potprovedall subs proved mod-mod, mod-mult-law,
range-cong-dupsprovedall subs proved congmod-def-mod, mod-le-same, mod-pos,
congmod-def-mod-02provedall subs proved mod-pos-def, mod-neg-def, congmod-def-mod, congmod-mod-abs,
mod-mult-lawprovedall subs proved mod-mult-add, mod-ex-div,
rem-mod-posprovedall subs proved mod-zero, mod-mult-add,
congmod-def-modprovedall subs proved mod-mod, mod-ex-div, mod-mult-add, congmod-def,
mod-mult-add-01provedall subs proved mod-mult-add,
mod-add-lawprovedall subs proved mod-mult-add, mod-ex-div,
mod-mult-addprovedall subs proved mod-plus, mod-rec-plus, mod-rec-any,
mod-rec-plusprovedall subs proved mod-plus,
mod-plusprovedall subs proved mod-rec-any,
mod-rec-anyprovedall subs proved mod-mult-04, mod-zero-neg, mod-rec-neg, mod-zero, mod-rec,
mod-negprovedall subs proved mod-pos-def, mod-mult-03, mod-mult-01, mod-neg-def,
mod-rec-negprovedall subs proved mod-mult-01, mod-neg-def,
mod-zero-negprovedall subs proved mod-mult-01, mod-neg-def,
mod-mult-03provedall subs proved mod-mult-02,
congmod-inverseprovedall subs proved congmod-def, cong-one-01, cong-one, cong-zero, cong-same,
mod-mult-02provedall subs proved mod-mult,
diff-primes-dupsprovedall subs proved mod-le-same, mod-pos,
mod-mult-01provedall subs proved mod-mult,
cong-zeroprovedall subs proved congmod-def, cong-same,
mod-modprovedall subs proved mod-le-same, mod-pos, mod-zero,
mod-zero-03provedall subs proved mod-zero,
mod-zero-04provedall subs proved mod-zero-01,
mod-zero-02provedall subs proved mod-zero-01,
mod-abs-neg-divprovedall subs proved mod-pos-def, mod-mult,
cong-mult-03provedall subs proved cong-mult-02,
Shor-algorithmprovedall subs proved cong-same, congmod-def,
mod-recprovedall subs proved mod-pos-def,
mod-mult-04provedall subs proved mod-pos-def, mod-neg-def,
cong-crt-01provedall subs proved congmod-def,
mod-multprovedall subs proved mod-pos-def, mod-neg-def,
cong-same-addprovedall subs proved congmod-def,
cong-mult-rewprovedall subs proved congmod-def,
cong-negprovedall subs proved congmod-def,
mod-posprovedall subs proved mod-pos-def, mod-neg-def,
mod-le-sameprovedall subs proved mod-pos-def, mod-neg-def,
mod-zero-01provedall subs proved mod-pos-def,
mod-oneprovedall subs proved mod-pos-def,
cong-oneprovedall subs proved congmod-def,
cong-one-01provedall subs proved congmod-def,
congmod-mod-absprovedall subs proved congmod-def,
mod-ex-divprovedall subs proved mod-neg-def, mod-pos-def,
cong-mult-02provedall subs proved congmod-def,
cong-sameprovedall subs proved congmod-def,
mod-zeroprovedall subs proved mod-pos-def,
four-square-divides-allprovedall subs proved congmod-def,
four-square-congmodprovedall subs proved congmod-def,
four-square-mod-zeroprovedall subs proved congmod-def,
mod-pos-revprovedall subs proved mod-pos-def,
mod-i2nprovedall subs proved mod-pos-def,
mod-abs-posprovedall subs proved mod-pos-def, mod-neg-def,
mod-abs-neg-negprovedall subs proved mod-neg-def,
div-mod-eqprovedall subs proved div-pos-def, div-neg-def, mod-neg-def, mod-pos-def,
cong-crtprovedall subs proved congmod-def,
cong-commprovedall subs proved congmod-def,
div-neg-defaxiom
div-pos-defaxiom
mod-neg-defaxiom
mod-pos-defaxiom
even-sumprovedall subs proved
congmod-defaxiom
four-square-odd-lsprovedall subs proved
lagrange-primedivisorsprovedall subs proved