[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
,
Theorem base summary for Specification int-mod
Status:
Proved!
Axioms: 5, User Theorems: 82 (Proved: 82, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 1158, Interactions: 651
Diffie-Hellman(8,4)
cong-mult(10,4)
cong-zero(2,1)
diff-primes(41,24)
fermat-1(16,7)
four-square-odd-ls(26,15)
mod-crt(5,3)
mod-mult-04(4,2)
mod-pos-def(0,0)
mod-zero-02(2,1)
Lagrange-SumOf4Squares(13,7)
cong-mult-02(5,3)
congmod-def(0,0)
diff-primes-dups(27,15)
fermat-1-mod(4,2)
lagrange-lemma(52,37)
mod-ex-div(15,6)
mod-mult-add(20,11)
mod-pos-rev(2,1)
mod-zero-03(1,0)
Lagrange-SumOf4Squares-primes(82,58)
cong-mult-03(2,1)
congmod-def-mod(14,8)
diff-primes-neg(41,24)
fermat-2(14,10)
lagrange-lemma-smallest(11,6)
mod-i2n(4,2)
mod-mult-add-01(1,0)
mod-pot-pot(15,8)
mod-zero-04(2,1)
RSA-decrypt-ij-vars(44,24)
cong-mult-rew(12,7)
congmod-def-mod-01(22,14)
div-mod-eq(8,5)
fermat-2-mod(6,3)
lagrange-primedivisors(12,5)
mod-le-same(4,2)
mod-mult-law(19,13)
mod-rec(8,2)
mod-zero-neg(6,1)
Shor-algorithm(28,15)
cong-neg(7,5)
congmod-def-mod-02(42,26)
div-neg-def(0,0)
fermat-for-rsa(14,8)
mod-abs-neg(1,0)
mod-mod(2,1)
mod-neg(14,4)
mod-rec-any(10,5)
range-cong-dups(9,5)
cong-add(2,1)
cong-one(1,1)
congmod-inverse(36,19)
div-pos-def(0,0)
fermat-pos(27,15)
mod-abs-neg-div(4,2)
mod-mult(4,2)
mod-neg-def(0,0)
mod-rec-neg(19,9)
rem-mod-pos(2,0)
cong-comm(5,3)
cong-one-01(1,1)
congmod-inverse-pos(24,10)
even-sum(48,26)
four-square-congmod(35,18)
mod-abs-neg-neg(4,2)
mod-mult-01(2,1)
mod-one(1,1)
mod-rec-plus(1,0)
cong-crt(12,6)
cong-same(1,1)
congmod-inverse-smallest(23,12)
ex-modeq-half(33,19)
four-square-divides-all(68,42)
mod-abs-pos(8,4)
mod-mult-02(3,2)
mod-plus(2,1)
mod-zero(4,1)
cong-crt-01(17,9)
cong-same-add(3,2)
congmod-mod-abs(5,2)
ex-modeq-half-all(9,5)
four-square-mod-zero(28,15)
mod-add-law(12,9)
mod-mult-03(1,1)
mod-pos(4,2)
mod-zero-01(2,1)