This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| congmod-def | ⊦ ≡mod(i, i0, j) ↔ j | abs(i - i0) | An Axiom |
| mod-neg-def | ⊦ i % j < 0 → i |%| j = i % j + j | An Axiom |
| mod-pos-def | ⊦ 0 ≤ i % j → i |%| j = i % j | An Axiom |
| div-neg-def | ⊦ i % j < 0 → i |/| j = i / j - 1 | An Axiom |
| div-pos-def | ⊦ 0 ≤ i % j → i |/| j = i / j | An Axiom |
| Diffie-Hellman | i2 = i ^ i1 |%| j, i4 = i ^ i3 |%| j, prime(j), 1 < i, i < j, 0 < i1, i1 < j, 0 < i3, i3 < j ⊦ i2 ^ i3 |%| j = i4 ^ i1 |%| j | A User Theorem |
| Lagrange-SumOf4Squares | 0 ≤ j ⊦ ∃ i, i0, i1, i2. j = i ^2 + i0 ^2 + i1 ^2 + i2 ^2 | A User Theorem |
| Lagrange-SumOf4Squares-primes | prime(j), j ≠ 2 ⊦ ∃ i, i0, i1, i2. j = i ^2 + i0 ^2 + i1 ^2 + i2 ^2 | A User Theorem |
| RSA-decrypt-ij-vars | prime(i), prime(i0), i1 = i * i0, 2 < i, 2 < i0, i ≠ i0, gcd(i2, (i - 1) * (i0 - 1)) = 1, 0 < i2, i2 < i1, ≡mod(i2 * i3, 1, (i - 1) * (i0 - 1)), 0 ≤ i3, j0 = j ^ i2 |%| i1, 0 ≤ j, j < i1 ⊦ j = j0 ^ i3 |%| i1 | A User Theorem |
| Shor-algorithm | 1 < j, ¬ prime(j), 1 < i, i < j, gcd(i, j) = 1, ≡mod(i ^ i0, 1, j), 0 ≤ i0, even(i0), ¬ ≡mod(i ^ (i0 / 2), ~1, j) ⊦ 1 < gcd(i ^ (i0 / 2) - 1, j) ∧ gcd(i ^ (i0 / 2) - 1, j) | j | A User Theorem |
| cong-add | ⊦ j | j0 → (≡mod(j0 + i, i0, j) ↔ ≡mod(i, i0, j)) | A User Theorem |
| cong-comm | ⊦ ≡mod(i, i0, j) ↔ ≡mod(i0, i, j) | A User Theorem |
| cong-crt | ≡mod(i, 1, j), ≡mod(i, 1, j0), prime(j), prime(j0), 0 < i, j ≠ j0 ⊦ ≡mod(i, 1, j * j0) | A User Theorem |
| cong-crt-01 | ≡mod(i ^ i0, i, j), ≡mod(i ^ i0, i, j0), prime(j), prime(j0), 0 < i, j ≠ j0, 0 ≤ i0 ⊦ ≡mod(i ^ i0, i, j * j0) | A User Theorem |
| cong-mult | ⊦ ≡mod(j0 * j + i, i0, j) ↔ ≡mod(i, i0, j) | A User Theorem |
| cong-mult-02 | ⊦ ≡mod(i0, 1, j) → ≡mod(i * i0, i, j) | A User Theorem |
| cong-mult-03 | ⊦ ≡mod(i0, 1, j) → ≡mod(i0 * i, i, j) | A User Theorem |
| cong-mult-rew | ⊦ ≡mod(i0, i2, j) → (≡mod(i * i0, i1, j) ↔ ≡mod(i * i2, i1, j)) | A User Theorem |
| cong-neg | ⊦ ≡mod(~ i, ~ i0, j) ↔ ≡mod(i, i0, j) | A User Theorem |
| cong-one | ⊦ ≡mod(i, j, 1) | A User Theorem |
| cong-one-01 | ⊦ ≡mod(i, j, ~1) | A User Theorem |
| cong-same | ⊦ ≡mod(i, i, j) | A User Theorem |
| cong-same-add | ⊦ ≡mod(i + i0, i + i1, j) ↔ ≡mod(i0, i1, j) | A User Theorem |
| cong-zero | ⊦ ≡mod(i, j, 0) ↔ i = j | A User Theorem |
| congmod-def-mod | ⊦ 0 < j → (≡mod(i, i0, j) ↔ i |%| j = i0 |%| j) | A User Theorem |
| congmod-def-mod-01 | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ j ≠ 0 → (≡mod(i, i0, j) ↔ i |%| j = i0 |%| j) | A User Theorem |
| congmod-def-mod-02 | ⊦ i < 0 ∧ i0 < 0 ∧ j ≠ 0 → (≡mod(i, i0, j) ↔ i |%| j = i0 |%| j) | A User Theorem |
| congmod-inverse | ⊦ gcd(i, j) = 1 → (∃ i0. ≡mod(i * i0, 1, j)) | A User Theorem |
| congmod-inverse-pos | gcd(i, j) = 1, 0 ≤ i, 0 ≤ j ⊦ ∃ i0. ≡mod(i * i0, 1, j) ∧ 0 ≤ i0 | A User Theorem |
| congmod-inverse-smallest | gcd(i, j) = 1, 0 ≤ i, 0 < j ⊦ ∃ i0. ≡mod(i * i0, 1, j) ∧ 0 ≤ i0 ∧ i0 < j | A User Theorem |
| congmod-mod-abs | ⊦ ≡mod(i, i0, j) ↔ ≡mod(i, i0, abs(j)) | A User Theorem |
| diff-primes | ⊦ prime(j) ∧ j ≠ 2 → ¬ dups(countFun(0, (j - 1) / 2, λ i. i ^2 |%| j)) | A User Theorem |
| diff-primes-dups | ⊦ prime(j) ∧ j ≠ 2 → dups(countFun(0, (j - 1) / 2, λ i. i ^2 |%| j) + countFun(0, (j - 1) / 2, λ i. (~1 - i ^2) |%| j)) | A User Theorem |
| diff-primes-neg | ⊦ prime(j) ∧ j ≠ 2 → ¬ dups(countFun(0, (j - 1) / 2, λ i. (~1 - i ^2) |%| j)) | A User Theorem |
| div-mod-eq | j ≠ 0 ⊦ i |/| j * j + i |%| j = i | A User Theorem |
| even-sum | j = i ^2 + i0 ^2 + i1 ^2 + i2 ^2, even(j) ⊦ ∃ i3, i4, i5, i6. even(i3 + i4) ∧ even(i5 + i6) ∧ i3 ^2 + i4 ^2 + i5 ^2 + i6 ^2 = j | A User Theorem |
| ex-modeq-half | 0 < j ∧ odd(j) ⊦ ∃ i. ≡mod(i, i0, j) ∧ abs(i) ≤ j / 2 | A User Theorem |
| ex-modeq-half-all | 0 < j0, odd(j0), i2 ^2 + i1 ^2 + i0 ^2 + i ^2 = j0 * j ⊦ ∃ i3, i4, i5, i6. ≡mod(i3, i, j0) ∧ abs(i3) ≤ j0 / 2 ∧ ≡mod(i4, i0, j0) ∧ abs(i4) ≤ j0 / 2 ∧ ≡mod(i5, i1, j0) ∧ abs(i5) ≤ j0 / 2 ∧ ≡mod(i6, i2, j0) ∧ abs(i6) ≤ j0 / 2 | A User Theorem |
| fermat-1 | ⊦ prime(j) → ≡mod(i ^ j, i, j) | A User Theorem |
| fermat-1-mod | ⊦ prime(j) → i ^ j |%| j = i |%| j | A User Theorem |
| fermat-2 | ⊦ prime(j) ∧ gcd(j, i) = 1 → ≡mod(i ^ (j - 1), 1, j) | A User Theorem |
| fermat-2-mod | ⊦ prime(j) ∧ gcd(j, i) = 1 → i ^ (j - 1) |%| j = 1 | A User Theorem |
| fermat-for-rsa | ⊦ prime(j) ∧ j - 1 | i0 ∧ 2 < j ∧ 0 ≤ i ∧ 0 ≤ i0 → (i ^ i0 * i) |%| j = i |%| j | A User Theorem |
| fermat-pos | ⊦ prime(j) ∧ 0 < i → ≡mod(i ^ j, i, j) | A User Theorem |
| four-square-congmod | i2 ^2 + i1 ^2 + i0 ^2 + i ^2 = j0 * j, ≡mod(i3, i2, j0), ≡mod(i4, i1, j0), ≡mod(i5, i0, j0), ≡mod(i6, i, j0), 1 < j, 0 < j, 0 < j0, j ≠ 2, j0 ≠ 1, 0 < i3 ^2 + i4 ^2 + i5 ^2 + i6 ^2 ⊦ ≡mod(i3 ^2 + i4 ^2 + i5 ^2 + i6 ^2, 0, j0) | A User Theorem |
| four-square-divides-all | i2 ^2 + i1 ^2 + i0 ^2 + i ^2 = j0 * j, j0 * i7 = i3 ^2 + i4 ^2 + i5 ^2 + i6 ^2, ≡mod(i3, i2, j0), ≡mod(i4, i1, j0), ≡mod(i5, i0, j0), ≡mod(i6, i, j0), i7 < j, 0 < j0, 1 < j0, 0 < i7, j0 * i7 < j0 ^2, 0 < j, j0 < j, 1 < j0 ^2, 0 < j0 ^2, i7 < j0, 1 < j, j ≠ 2, j0 ≠ 1 ⊦ j0 | ((i2 * i3 + i1 * i4) + i0 * i5) + i * i6 ∧ j0 | i * i5 + i2 * i4 - i1 * i3 + i0 * i6 ∧ j0 | i2 * i5 + i1 * i6 - i0 * i3 + i * i4 ∧ j0 | i0 * i4 + i2 * i6 - i1 * i5 + i * i3 | A User Theorem |
| four-square-mod-zero | i2 ^2 + i1 ^2 + i0 ^2 + i ^2 = j0 * j, ≡mod(0, i, j0), ≡mod(0, i1, j0), ≡mod(0, i0, j0), ≡mod(0, i2, j0), prime(j), j0 < j, 1 < j, 0 < j, 0 < j0, 0 ≤ j, j ≠ 2, j0 ≠ 1 ⊦ | A User Theorem |
| four-square-odd-ls | odd(j0), abs(i3) ≤ j0 / 2, abs(i4) ≤ j0 / 2, abs(i5) ≤ j0 / 2, abs(i6) ≤ j0 / 2, 0 < j0, j0 ≠ 1, 0 < i3 ^2 + i4 ^2 + i5 ^2 + i6 ^2 ⊦ i3 ^2 + i4 ^2 + i5 ^2 + i6 ^2 < j0 ^2 | A User Theorem |
| lagrange-lemma | prime(j), j ≠ 2 ⊦ ∃ i, i0, j0. 1 + i ^2 + i0 ^2 = j0 * j ∧ 0 < j0 ∧ j0 < j | A User Theorem |
| lagrange-lemma-smallest | prime(j), j ≠ 2 ⊦ ∃ i, i0, i1, i2, j0. i ^2 + i0 ^2 + i1 ^2 + i2 ^2 = j0 * j ∧ 0 < j0 ∧ j0 < j ∧ (∀ i3, i4, i5, i6, j1. 0 < j1 ∧ j1 < j0 → i3 ^2 + i4 ^2 + i5 ^2 + i6 ^2 ≠ j1 * j) | A User Theorem |
| lagrange-primedivisors | ∀ j. j ∈ ints → (∃ i, i0, i1, i2. j = i ^2 + i0 ^2 + i1 ^2 + i2 ^2) ⊦ ∃ i, i0, i1, i2. Π ints = i ^2 + i0 ^2 + i1 ^2 + i2 ^2 | A User Theorem |
| mod-abs-neg | ⊦ i < 0 ∧ 0 < j → i |%| abs(j) = i |%| j | A User Theorem |
| mod-abs-neg-div | ⊦ i < 0 ∧ j < 0 ∧ i % j = 0 → i |%| abs(j) = i |%| j | A User Theorem |
| mod-abs-neg-neg | ⊦ i < 0 ∧ j < 0 ∧ i % j ≠ 0 → i |%| abs(j) = i |%| j - 2 * j | A User Theorem |
| mod-abs-pos | ⊦ 0 ≤ i ∧ j ≠ 0 → i |%| abs(j) = i |%| j | A User Theorem |
| mod-add-law | ⊦ 0 < j → (i + i0) |%| j = (i |%| j + i0 |%| j) |%| j | A User Theorem |
| mod-crt | ≡mod(i ^ i0, i, j), ≡mod(i ^ i0, i, j0), prime(j), prime(j0), 0 < i, j ≠ j0, 0 ≤ i0 ⊦ i ^ i0 |%| (j * j0) = i |%| (j * j0) | A User Theorem |
| mod-ex-div | ⊦ j ≠ 0 → (∃ j0. i = j * j0 + i |%| j) | A User Theorem |
| mod-i2n | ⊦ 0 ≤ i ∧ 0 < j → i→n(i |%| j) = i→n(i) % i→n(j) | A User Theorem |
| mod-le-same | ⊦ 0 < j → ¬ j ≤ i |%| j | A User Theorem |
| mod-mod | ⊦ 0 < j → (i |%| j) |%| j = i |%| j | A User Theorem |
| mod-mult | ⊦ j ≠ 0 → (i * j) |%| j = 0 | A User Theorem |
| mod-mult-01 | ⊦ 0 < j → (i * j) |%| j = 0 | A User Theorem |
| mod-mult-02 | ⊦ j ≠ 0 → ~(i * j) |%| j = 0 | A User Theorem |
| mod-mult-03 | ⊦ 0 < j → ~(i * j) |%| j = 0 | A User Theorem |
| mod-mult-04 | ⊦ j ≠ 0 → ~ j |%| j = 0 | A User Theorem |
| mod-mult-add | ⊦ 0 < j → (i + i0 * j) |%| j = i |%| j | A User Theorem |
| mod-mult-add-01 | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i + i0 * j) |%| j = i |%| j | A User Theorem |
| mod-mult-law | ⊦ 0 < j → (i * i0) |%| j = (i |%| j * i0 |%| j) |%| j | A User Theorem |
| mod-neg | ⊦ i < 0 ∧ 0 < j ∧ i |%| j ≠ 0 → i |%| j = ~(~ i |%| j - j) | A User Theorem |
| mod-one | ⊦ i |%| 1 = 0 | A User Theorem |
| mod-plus | ⊦ 0 < j → (i + j) |%| j = i |%| j | A User Theorem |
| mod-pos | ⊦ 0 < j → ¬ i |%| j < 0 | A User Theorem |
| mod-pos-rev | ⊦ 0 ≤ i % j → i % j = i |%| j | A User Theorem |
| mod-pot-pot | ⊦ 0 ≤ i0 ∧ 0 < j → (i |%| j) ^ i0 |%| j = i ^ i0 |%| j | A User Theorem |
| mod-rec | ⊦ j ≤ i ∧ 0 < j → i |%| j = (i - j) |%| j | A User Theorem |
| mod-rec-any | ⊦ 0 < j → i |%| j = (i - j) |%| j | A User Theorem |
| mod-rec-neg | ⊦ i < ~ j ∧ 0 < j → i |%| j = (i + j) |%| j | A User Theorem |
| mod-rec-plus | ⊦ 0 < j → i |%| j = (i + j) |%| j | A User Theorem |
| mod-zero | ⊦ 0 ≤ i ∧ i < j → i |%| j = i | A User Theorem |
| mod-zero-01 | ⊦ j ≠ 0 → 0 |%| j = 0 | A User Theorem |
| mod-zero-02 | ⊦ j < 0 → 0 |%| j = 0 | A User Theorem |
| mod-zero-03 | ⊦ 0 < j → 0 |%| j = 0 | A User Theorem |
| mod-zero-04 | ⊦ j < 0 → 0 |%| ~ j = 0 | A User Theorem |
| mod-zero-neg | ⊦ i < 0 ∧ abs(i) < j ∧ 0 < j → i |%| j = i + j | A User Theorem |
| range-cong-dups | 0 < j, j < n→i(# ints), ¬ dups(ints) ⊦ ∃ i1, i2. i1 ≠ i2 ∧ ≡mod(i1, i2, j) | A User Theorem |
| rem-mod-pos | ⊦ 0 ≤ i ∧ 0 < j → i % j = i |%| j | A User Theorem |