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: |
|---|---|---|
| Prime | ⊦ prime(n) ↔ 1 < n ∧ (∀ m. m | n → m = 1 ∨ m = n) | An Axiom |
| gcd-rec1 | ⊦ n ≤ m → gcd(m, n) = gcd(m - n, n) | An Axiom |
| gcd-c | ⊦ gcd(m, n) = gcd(n, m) | An Axiom |
| gcd-zero | ⊦ gcd(0, n) = n | An Axiom |
| Divides | ⊦ m | n ↔ (∃ n0. m * n0 = n) | An Axiom |
| dist-snd | ⊦ n < m → dist(m, n) = m - n | An Axiom |
| dist-fst | ⊦ m ≤ n → dist(m, n) = n - m | An Axiom |
| cong-equiv | ⊦ m ≠ 0 → (m | dist(n, n0) ↔ n % m = n0 % m) | A User Theorem |
| dist-add | ⊦ dist(m + n, m) = n | A User Theorem |
| dist-add-01 | ⊦ dist(m + n, m0 + n) = dist(m, m0) | A User Theorem |
| dist-c | ⊦ dist(m, n) = dist(n, m) | A User Theorem |
| dist-eq | ⊦ dist(m, n) = 0 ↔ m = n | A User Theorem |
| dist-mult | ⊦ dist(m * n, m * n0) = m * dist(n, n0) | A User Theorem |
| dist-mult-01 | ⊦ dist(m * (n1 + n0), m * n0) = m * n1 | A User Theorem |
| dist-same | ⊦ dist(m, m) = 0 | A User Theorem |
| dist-snd-01 | ⊦ n ≤ m → dist(m, n) = m - n | A User Theorem |
| dist-zero | ⊦ dist(m, 0) = m | A User Theorem |
| div | ⊦ prime(m) ∧ n ≠ 1 → (n | m ↔ n = m) | A User Theorem |
| div-multadd | ⊦ m | m * n + m * n0 | A User Theorem |
| divi-add | ⊦ m | n → (m | n + n0 ↔ m | n0) | A User Theorem |
| divi-add-01 | ⊦ m | m * n + n0 ↔ m | n0 | A User Theorem |
| divi-dist | ⊦ m | n ∧ m | n0 → m | dist(n, n0) | A User Theorem |
| divi-eq | m | n, n | m ⊦ m = n | A User Theorem |
| divi-ls | ⊦ m < n0 → (n0 | m ↔ m = 0) | A User Theorem |
| divi-mod | m ≠ 0 ⊦ m | n ↔ n % m = 0 | A User Theorem |
| divi-mult | ⊦ m | m * n0 | A User Theorem |
| divi-mult-01 | ⊦ m | n → m | n * n0 | A User Theorem |
| divi-one | ⊦ m | 1 ↔ m = 1 | A User Theorem |
| divi-one-01 | ⊦ 1 | m | A User Theorem |
| divi-primmult | ⊦ ¬ m | n ∧ prime(m) → (m | n * n0 ↔ m | n0) | A User Theorem |
| divi-ref | ⊦ m | m | A User Theorem |
| divi-same | ⊦ m | dist(n, m0) ∧ m | dist(n0, m0) → m | dist(n, n0) | A User Theorem |
| divi-sub | ⊦ m | n ∧ n0 ≤ n → (m | n - n0 ↔ m | n0) | A User Theorem |
| divi-succ | ⊦ m | n → (m | n + 1 ↔ m = 1) | A User Theorem |
| divi-sym | ⊦ m | n → (n | m ↔ m = n) | A User Theorem |
| divi-three | ⊦ m ≠ 1 → (m | 3 ↔ m = 3) | A User Theorem |
| divi-trans | ⊦ n0 | m ∧ m | n → n0 | n | A User Theorem |
| divi-two | ⊦ ¬ 2 | 1 | A User Theorem |
| divi-two-01 | ⊦ 2 | m + 2 ↔ 2 | m | A User Theorem |
| divi-two-02 | ⊦ m ≠ 1 → (m | 2 ↔ m = 2) | A User Theorem |
| divi-two-03 | ⊦ ¬ 2 | n → 2 | n + 1 | A User Theorem |
| divi-zero | ⊦ m | 0 | A User Theorem |
| divi-zero-01 | ⊦ 0 | m ↔ m = 0 | A User Theorem |
| gcd-a | ⊦ gcd(m, gcd(n, n0)) = gcd(gcd(m, n), n0) | A User Theorem |
| gcd-add | ⊦ gcd(n, m + n) = gcd(m, n) | A User Theorem |
| gcd-addrev | ⊦ gcd(m + n, n) = gcd(m, n) | A User Theorem |
| gcd-alldiv | ⊦ n0 | m ∧ n0 | n → n0 | gcd(m, n) | A User Theorem |
| gcd-alldiv-h | m < n, n0 | n, n0 | m ⊦ n0 | gcd(m, n) | A User Theorem |
| gcd-conq-one | gcd(m, n) = 1 ⊦ ∃ m0. n | dist(m * m0, 1) | A User Theorem |
| gcd-div | ⊦ n0 | gcd(m, n) → n0 | m | A User Theorem |
| gcd-div-01 | ⊦ n0 | gcd(m, n) → n0 | n | A User Theorem |
| gcd-div-02 | ⊦ gcd(m, gcd(n, n0)) | gcd(m, n) | A User Theorem |
| gcd-div-03 | ⊦ gcd(m, gcd(n, n0)) | n | A User Theorem |
| gcd-div-04 | ⊦ gcd(m, gcd(n, n0)) | m | A User Theorem |
| gcd-div-both | ⊦ n0 | gcd(m, n) → n0 | n ∧ n0 | m | A User Theorem |
| gcd-div-both-h | m < n, n0 | gcd(m, n) ⊦ n0 | n ∧ n0 | m | A User Theorem |
| gcd-div-one | ⊦ gcd(m, n) = 1 ∧ m | n * n0 → m | n0 | A User Theorem |
| gcd-div-one-01 | ⊦ gcd(m, n) = 1 ∧ ¬ m | n0 → ¬ m | n * n0 | A User Theorem |
| gcd-div-one-02 | ⊦ gcd(m, n) = 1 ∧ ¬ m | n0 → ¬ m | n0 * n | A User Theorem |
| gcd-divs | ⊦ gcd(m, n) | m | A User Theorem |
| gcd-eq | ⊦ n ≠ 0 ∧ gcd(m, n) = m → m ≤ n | A User Theorem |
| gcd-id | ⊦ gcd(m, m) = m | A User Theorem |
| gcd-id-01 | ⊦ gcd(m, gcd(m, n)) = gcd(m, n) | A User Theorem |
| gcd-le | ⊦ m ≠ 0 → gcd(m, n) ≤ m | A User Theorem |
| gcd-le-both | ⊦ m ≠ 0 ∧ n ≠ 0 → gcd(m, n) ≤ m ∧ gcd(m, n) ≤ n | A User Theorem |
| gcd-le-both-h | m < n ⊦ n = 0, m = 0, ¬ m < gcd(m, n) ∧ ¬ n < gcd(m, n) | A User Theorem |
| gcd-max | ⊦ m ≠ 0 ∧ n0 | m ∧ n0 | n → n0 ≤ gcd(m, n) | A User Theorem |
| gcd-mod | n ≠ 0 ⊦ gcd(m, n) = gcd(n, m % n) | A User Theorem |
| gcd-mod-one | gcd(m, n) = 1, 1 < n, m ≠ 0 ⊦ ∃ m0. (m * m0) % n = 1 | A User Theorem |
| gcd-mod-one-01 | gcd(m, n) = 1, 1 < n ⊦ ∃ m0. (m * m0) % n = 1 | A User Theorem |
| gcd-mult | ⊦ gcd(n0 * m, n0 * n) = n0 * gcd(m, n) | A User Theorem |
| gcd-multdiv | ⊦ gcd(m, n) | m * n0 | A User Theorem |
| gcd-one | ⊦ gcd(m, 1) = 1 | A User Theorem |
| gcd-rec2 | ⊦ m ≤ n → gcd(m, n) = gcd(m, n - m) | A User Theorem |
| gcd-sym | ⊦ gcd(m, n) ≠ gcd(n, m) ↔ false | A User Theorem |
| gcd-sym-eq | ⊦ n0 = gcd(m, n) → (n0 ≠ gcd(n, m) ↔ false) | A User Theorem |
| gcd-trans | ⊦ n0 | n → gcd(m, n0) | gcd(m, n) | A User Theorem |
| gcd-twice | ⊦ gcd(n, 2 * n) = n | A User Theorem |
| gcd-twicerev | ⊦ gcd(2 * n, n) = n | A User Theorem |
| gcd-two | ⊦ gcd(2, m) ≠ 1 → gcd(2, m) = 2 | A User Theorem |
| gcd-zero-01 | ⊦ gcd(m, n) = 0 ↔ m = 0 ∧ n = 0 | A User Theorem |
| gcd-zero-01-h | m < n, gcd(m, n) = 0 ⊦ m = 0 ∧ n = 0 | A User Theorem |
| gcd-zero-02 | ⊦ gcd(n, 0) = n | A User Theorem |
| gcdex | ⊦ ∃ m0, n0. m * m0 + gcd(m, n) = n * n0 ∨ n * n0 + gcd(m, n) = m * m0 | A User Theorem |
| gcdex-dist | ⊦ ∃ m0, n0. gcd(m, n) = dist(m * m0, n * n0) | A User Theorem |
| gcdexh | n ≤ m ⊦ ∃ m0, n0. m * m0 + gcd(m, n) = n * n0 ∨ n * n0 + gcd(m, n) = m * m0 | A User Theorem |
| gcdnex | ⊦ gcd(m, m0) = 1 ↔ m + m0 = 1 ∨ ¬(∃ n. 1 < n ∧ n | m ∧ n | m0) | A User Theorem |
| gcdnex-prime | ⊦ gcd(m, m0) = 1 ↔ m + m0 = 1 ∨ ¬(∃ n. prime(n) ∧ 1 < n ∧ n | m ∧ n | m0) | A User Theorem |
| leone | ⊦ m ≤ 1 → ¬ prime(m) | A User Theorem |
| lstwo | ⊦ m < 2 → ¬ prime(m) | A User Theorem |
| mod-zero | ⊦ m % n = 0 ∧ n < m ∧ 2 ≤ n → (prime(m) ↔ m = 2) | A User Theorem |
| mod2 | ⊦ m % 2 = 0 → (prime(m) ↔ m = 2) | A User Theorem |
| modprime | ⊦ prime(n) ↔ 1 < n ∧ (∀ m. 2 ≤ m ∧ m < n → n % m ≠ 0) | A User Theorem |
| mult | ⊦ m ≠ 1 ∧ n ≠ 1 → ¬ prime(m * n) | A User Theorem |
| mult-01 | ⊦ m ≠ 1 ∧ n0 + 1 < n → ¬ prime(m * n) | A User Theorem |
| mult-02 | ⊦ prime(m) → (prime(m * n) ↔ n = 1) | A User Theorem |
| mult-03 | ⊦ 2 ≤ m ∧ 2 ≤ n → ¬ prime(m * n) | A User Theorem |
| not-prime | ¬ prime(n), 2 ≤ n ⊦ ∃ m. m | n ∧ prime(m) ∧ m * m ≤ n | A User Theorem |
| one | ⊦ ¬ prime(1) | A User Theorem |
| prime-prime | ⊦ prime(n) ↔ 1 < n ∧ (∀ m. 2 ≤ m ∧ prime(m) ∧ m * m ≤ n → n % m ≠ 0) | A User Theorem |
| prime-smallest | ⊦ prime(n) ↔ 1 < n ∧ (∀ m. 2 ≤ m ∧ m * m ≤ n → n % m ≠ 0) | A User Theorem |
| rax | ⊦ prime(n) ↔ ¬ ¬(1 < n ∧ (∀ m. m | n → m = 1 ∨ m = n)) | A User Theorem |
| succ | ⊦ prime(m) → (prime(m + 1) ↔ m = 2) | A User Theorem |
| three | ⊦ prime(3) | A User Theorem |
| two | ⊦ prime(2) | A User Theorem |
| two-01 | ⊦ m ≤ 2 → (prime(m) ↔ m = 2) | A User Theorem |
| twodiv | ⊦ 2 | m → (prime(m) ↔ m = 2) | A User Theorem |
| twodiv-01 | ⊦ prime(m + 1) → (2 | m ↔ m ≠ 1) | A User Theorem |
| twodiv-02 | ⊦ prime(m) → (2 | m + 1 ↔ m ≠ 2) | A User Theorem |
| zero | ⊦ ¬ prime(0) | A User Theorem |