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: |
|---|---|---|
| is-aligned-def | ⊦ is-aligned(n, m) ↔ n % m = 0 | An Axiom |
| aligndown-def | 0 ≠ m ⊦ align↓(n, m) = (n % m = 0 ⊃ n;n / m * m) | An Axiom |
| alignup-def | 0 ≠ m ⊦ align↑(n, m) = (n % m = 0 ⊃ n;(n / m)+1 * m) | An Axiom |
| add-n-aligndown | n ≠ 0 ⊦ align↓(n0 + n, n) = n + align↓(n0, n) | A User Theorem |
| aligndown-add-n | n ≠ 0 ⊦ n + align↓(m, n) ≤ m ↔ false | A User Theorem |
| aligndown-add-n-alignup | m ≠ 0 ⊦ ¬ is-aligned(n, m) → align↓(n, m) + m = align↑(n, m) | A User Theorem |
| aligndown-add-not-smaller | m ≠ 0 ⊦ align↓(n0 + n1, m) < align↓(n0, m) ↔ false | A User Theorem |
| aligndown-add-same | m ≠ 0 ⊦ align↓(n0 + n1, m) = align↓(n0, m) ↔ n0 % m + n1 < m | A User Theorem |
| aligndown-add-same0 | m ≠ 0 ⊦ n0 % m + n1 < m → align↓(n0 + n1, m) = align↓(n0, m) | A User Theorem |
| aligndown-aligndown-add | n ≠ 0 ⊦ align↓(align↓(n0, n) + n1, n) = align↓(n0, n) + align↓(n1, n) | A User Theorem |
| aligndown-eq-add | m ≠ 0 ⊦ align↓(n, m) = n + n0 ↔ ¬ ¬(n0 = 0 ∧ is-aligned(n, m)) | A User Theorem |
| aligndown-is-aligned | m ≠ 0 ⊦ is-aligned(align↓(n, m), m) | A User Theorem |
| aligndown-is-aligned-add | n ≠ 0 ⊦ is-aligned(n0, n) → align↓(n0 + n1, n) = n0 + align↓(n1, n) | A User Theorem |
| aligndown-is-aligned0 | m ≠ 0 ⊦ is-aligned(n, m) → align↓(n, m) = n | A User Theorem |
| aligndown-is-n | n ≠ 0 ⊦ n ≤ n0 + n1 ∧ n0 + n1 < 2 * n → align↓(n0 + n1, n) = n | A User Theorem |
| aligndown-is-smaller | m ≠ 0 ⊦ n0 < align↓(n, m) → n0 < n | A User Theorem |
| aligndown-is-smaller-01 | m ≠ 0 ⊦ align↓(n0, m) ≤ n0 | A User Theorem |
| aligndown-is-zero | n ≠ 0 ⊦ align↓(m, n) = 0 ↔ m < n | A User Theorem |
| aligndown-le | m ≠ 0 ⊦ n ≤ align↓(n, m) ↔ is-aligned(n, m) | A User Theorem |
| aligndown-multiplier | n ≠ 0 ⊦ align↓(n0 * n, n) = n0 * n | A User Theorem |
| aligndown-not-smaller | m ≠ 0 ⊦ is-aligned(n1, m) ∧ n0 < n1 → (align↓(n1, m) ≤ align↓(n0, m) ↔ false) | A User Theorem |
| aligndown-plus-remainder | n ≠ 0 ⊦ align↓(m, n) + m % n = m | A User Theorem |
| aligndown-remainder | n ≠ 0 ⊦ m = m0 + align↓(m, n) ↔ m0 = m % n | A User Theorem |
| aligndown-same | n ≠ 0, m % n = 0 ⊦ align↓(m, n) = m | A User Theorem |
| aligndown-same-equiv | n ≠ 0 ⊦ align↓(n0, n) = n0 ↔ is-aligned(n0, n) | A User Theorem |
| aligndown-same0 | n ≠ 0, is-aligned(m, n) ⊦ align↓(m, n) = m | A User Theorem |
| aligndown-sub-add-sub | n ≠ 0 ⊦ n1 ≤ n0 → n0 - n1 + align↓(n0 - n1, n) = (n0 - n1) % n | A User Theorem |
| alignup-add-bounded1 | m ≠ 0 ⊦ n ≤ m → align↑(n, m) = (n = 0 ⊃ 0;m) | A User Theorem |
| alignup-add-mult | m ≠ 0 ⊦ align↑(n * m + n0, m) = n * m + align↑(n0, m) | A User Theorem |
| alignup-calc | m ≠ 0 ⊦ m = n % m + n0 ∧ ¬ is-aligned(n, m) → align↑(n, m) = n + n0 | A User Theorem |
| alignup-is-aligned | m ≠ 0 ⊦ is-aligned(align↑(n, m), m) | A User Theorem |
| alignup-is-bigger | m ≠ 0 ⊦ n0 ≤ align↑(n0, m) | A User Theorem |
| alignup-is-even-bigger | m ≠ 0, n1 ≤ n0 ⊦ ¬ align↑(n0, m) + n2 < n1 | A User Theorem |
| alignup-isnot-smaller | m ≠ 0 ⊦ align↑(n, m) < n ↔ false | A User Theorem |
| alignup-le | n ≠ 0 ⊦ align↑(m0, n) < align↑(m1, n) → (¬ m0 < m1 ↔ false) | A User Theorem |
| alignup-le-is-aligned | n ≠ 0, is-aligned(m, n) ⊦ m < align↑(m0, n) ↔ m < m0 | A User Theorem |
| alignup-lower-bound | n ≠ 0 ⊦ is-aligned(m0, n) ∧ m0 ≤ m → align↑(m, n) ≥ m0 | A User Theorem |
| alignup-multiplier | n ≠ 0 ⊦ align↑(n0 * n, n) = n0 * n | A User Theorem |
| alignup-same | n ≠ 0, m % n = 0 ⊦ align↑(m, n) = m | A User Theorem |
| alignup-same0 | n ≠ 0, is-aligned(m, n) ⊦ align↑(m, n) = m | A User Theorem |
| alignup-upper-bound | n ≠ 0 ⊦ is-aligned(m0, n) ∧ m0 ≥ m → align↑(m, n) ≤ m0 | A User Theorem |
| alignup-upper-bound-01 | m ≠ 0 ⊦ ¬ is-aligned(n, m) ∧ n % m + n0 < m → (align↑(n, m) ≤ n + n0 ↔ false) | A User Theorem |
| between-is-aligned | m ≠ 0 ⊦ is-aligned(m0, m) ∧ m0 < m1 ∧ m1 < m0 + m → (is-aligned(m1, m) ↔ false) | A User Theorem |
| div-mult-to-diff-mod | ⊦ n ≠ 0 → m / n * n = m - m % n | A User Theorem |
| eq1 | ⊦ 0 < m → (n + m) / m * m > n | A User Theorem |
| is-aligned-add | m ≠ 0, is-aligned(n1, m) ⊦ is-aligned(n0 + n1, m) ↔ is-aligned(n0, m) | A User Theorem |
| is-aligned-add-diff-le | n ≠ 0 ⊦ m ≤ n → is-aligned(m + (n - m), n) | A User Theorem |
| is-aligned-add-diff-ls | n ≠ 0 ⊦ m < n → is-aligned(m + (n - m), n) | A User Theorem |
| is-aligned-aligndown-zero | n ≠ 0 ⊦ is-aligned(m, n) → (m < n ↔ m = 0) | A User Theorem |
| is-aligned-elim | m ≠ 0 ⊦ is-aligned(n, m) ↔ (∃ n0. n = n0 * m) | A User Theorem |
| is-aligned-intro | m ≠ 0 ⊦ is-aligned(n0, m) ∧ ¬ is-aligned(n1, m) → n0 ≠ n1 | A User Theorem |
| is-aligned-minus | m ≠ 0 ⊦ n1 ≤ n0 ∧ is-aligned(n0, m) ∧ is-aligned(n1, m) → is-aligned(n0 - n1, m) | A User Theorem |
| is-aligned-mod-alignment | n0 ≠ 0, m ≠ 0 ⊦ is-aligned(n % (n0 * m), m) ↔ is-aligned(n, m) | A User Theorem |
| is-aligned-multiple | m ≠ 0 ⊦ is-aligned(n, m) → (∃ n0. n = n0 * m) | A User Theorem |
| is-aligned-multiple-1 | m ≠ 0, n0 ≠ 0 ⊦ is-aligned(n, n0 * m) → (¬ is-aligned(n, m) ↔ false) | A User Theorem |
| is-aligned-multiplier | n ≠ 0 ⊦ is-aligned(n0 * n, n) | A User Theorem |
| is-aligned-not-multiples | m ≠ 0, n ≠ 0 ⊦ is-aligned(m, n * m) ↔ n = 1 | A User Theorem |
| is-aligned-same | n ≠ 0 ⊦ is-aligned(n, n) | A User Theorem |
| is-aligned-simp | ⊦ (n0 + n1) % n = 0 → (¬ is-aligned(n0 + n1, n) ↔ false) | A User Theorem |
| is-aligned-still-space | n0 ≠ 0, n1 ≠ 0 ⊦ is-aligned(n0, n1) ∧ is-aligned(n, n1) ∧ ¬ is-aligned(n, n0) → (n0 < n % n0 + n1 ↔ false) | A User Theorem |
| is-aligned-zero | n ≠ 0 ⊦ is-aligned(0, n) | A User Theorem |
| not-mod0-not-aligned | m ≠ 0 ⊦ n % m = 0 → (¬ is-aligned(n, m) ↔ false) | A User Theorem |
| rounded-help | ⊦ 0 < m → n < m * n / m + m | A User Theorem |
| rounded-help2 | ⊦ n0 < m2 ∧ m1 < m2 → n0 + m1 < 2 * m2 | A User Theorem |