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: |
|---|---|---|
| sum-empty | ⊦ Σ [] = 0 | An Axiom |
| sum-rec | ⊦ Σ(i ' + ints) = i + Σ ints | An Axiom |
| prod-empty | ⊦ Π [] = 1 | An Axiom |
| prod-rec | ⊦ Π(i ' + ints) = i * Π ints | An Axiom |
| max-empty | ⊦ max([]) = 0 | An Axiom |
| max-def | ⊦ ints ≠ [] → max(ints) ∈ ints ∧ (∀ i. i ∈ ints → i ≤ max(ints)) | An Axiom |
| counti2j-empty | ⊦ j < i → count-i2j(i, j) = [] | An Axiom |
| counti2j-rec | ⊦ i ≤ j → count-i2j(i, j) = count-i2j(i, j - 1) + j | An Axiom |
| countFun-rec | ⊦ i ≤ j → countFun(i, j, intfun) = intfun(i) ' + countFun(i + 1, j, intfun) | An Axiom |
| countFun-base | ⊦ j < i → countFun(i, j, intfun) = [] | An Axiom |
| mapFun-rec | ⊦ mapFun(intfun, i ' + ints) = intfun(i) ' + mapFun(intfun, ints) | An Axiom |
| mapFun-base | ⊦ mapFun(intfun, []) = [] | An Axiom |
| all_prime_divisors-rec | ⊦ 2 ≤ i ∧ ¬ prime(i) → all_prime_divisors(i) = all_prime_divisors(i / max_prime_divisor(i)) + max_prime_divisor(i) ' | An Axiom |
| all_prime_divisors-prime | ⊦ prime(i) → all_prime_divisors(i) = i ' | An Axiom |
| all_prime_divisors-base | ⊦ i < 2 → all_prime_divisors(i) = [] | An Axiom |
| primes-def | ⊦ primes(ints) ↔ (∀ i. i ∈ ints → prime(i)) | An Axiom |
| min-def | ⊦ ints ≠ [] → min(ints) ∈ ints ∧ (∀ i. i ∈ ints → min(ints) ≤ i) | An Axiom |
| min-empty | ⊦ min([]) = 0 | An Axiom |
| filterFun-remove | ⊦ ¬ intboolfun(i) → filterFun(intboolfun, i ' + ints) = filterFun(intboolfun, ints) | An Axiom |
| filterFun-keep | ⊦ intboolfun(i) → filterFun(intboolfun, i ' + ints) = i ' + filterFun(intboolfun, ints) | An Axiom |
| filterFun-base | ⊦ filterFun(intboolfun, []) = [] | An Axiom |
| coprimes-def | ⊦ coprimes(i) = filterFun(λ j. gcd(i, j) = 1, count-i2j(1, i)) | An Axiom |
| euler-phi-def | ⊦ euler-phi(i) = n→i(# coprimes(i)) | An Axiom |
| all_prime_divisors-div | ⊦ 0 < j ∧ i | j ∧ prime(i) → all_prime_divisors(j / i) = all_prime_divisors(j) -1l i | A User Theorem |
| all_prime_divisors-in | ⊦ j ∈ all_prime_divisors(i) → prime(j) ∧ j ≤ i | A User Theorem |
| all_prime_divisors-in-01 | ⊦ j ∈ all_prime_divisors(i) ↔ prime(j) ∧ j | i ∧ 2 ≤ i | A User Theorem |
| all_prime_divisors-last | ⊦ all_prime_divisors(i) ≠ [] ∧ ¬ prime(i) → all_prime_divisors(i).last = max_prime_divisor(i) | A User Theorem |
| all_prime_divisors-ordered | ⊦ ordered≤(all_prime_divisors(i)) | A User Theorem |
| all_prime_divisors-product | ⊦ 0 < i → Π all_prime_divisors(i) = i | A User Theorem |
| all_prime_divisors-product-del | ⊦ prime(i) → ¬ i | Π(all_prime_divisors(j) -l i) | A User Theorem |
| all_prime_divisors-rec-01 | ⊦ i | j ∧ prime(i) ∧ 0 < j → #oc(i, all_prime_divisors(j)) = #oc(i, all_prime_divisors(j / i)) + 1 | A User Theorem |
| all_prime_divisors-rec-02 | ⊦ prime(i) ∧ 0 < j → #oc(i, all_prime_divisors(i * j)) = #oc(i, all_prime_divisors(j)) + 1 | A User Theorem |
| coprimes-coprimes | ⊦ j ∈ coprimes(i) → gcd(i, j) = 1 | A User Theorem |
| coprimes-empty | ⊦ i < 1 → coprimes(i) = [] | A User Theorem |
| coprimes-max | ⊦ 1 < i → max(coprimes(i)) < i | A User Theorem |
| coprimes-min | ⊦ 0 < i → min(coprimes(i)) = 1 | A User Theorem |
| coprimes-no-dups | ⊦ ¬ dups(coprimes(i)) | A User Theorem |
| coprimes-one | ⊦ coprimes(1) = 1 ' | A User Theorem |
| coprimes-ordered | ⊦ ordered≤(coprimes(i)) | A User Theorem |
| coprimes-prime | ⊦ prime(i) → coprimes(i) = count-i2j(1, i - 1) | A User Theorem |
| count-empty | ⊦ count-i2j(j, j - 1) = [] | A User Theorem |
| count-i2j-empty-01 | ⊦ count-i2j(i + 1, i) = [] | A User Theorem |
| count-i2j-empty-02 | ⊦ count-i2j(i, j) = [] ↔ j < i | A User Theorem |
| count-i2j-in | ⊦ i0 ∈ count-i2j(i, j) ↔ i ≤ i0 ∧ i0 ≤ j | A User Theorem |
| count-i2j-length | ⊦ i ≤ j → # count-i2j(i, j) = i→n(j - i) + 1 | A User Theorem |
| count-i2j-max | ⊦ i ≤ j → max(count-i2j(i, j)) = j | A User Theorem |
| count-i2j-min | ⊦ i ≤ j → min(count-i2j(i, j)) = i | A User Theorem |
| count-i2j-no-dups | ⊦ ¬ dups(count-i2j(i, j)) | A User Theorem |
| count-i2j-ordered | ⊦ ordered≤(count-i2j(i, j)) | A User Theorem |
| count-one | ⊦ count-i2j(j, j) = j ' | A User Theorem |
| count-rec | ⊦ i ≤ j → count-i2j(i, j) = i ' + count-i2j(i + 1, j) | A User Theorem |
| countFun-at | ⊦ n→i(n) ≤ j - i ∧ 0 ≤ i ∧ i ≤ j → countFun(i, j, intfun)[n] = intfun(i + n→i(n)) | A User Theorem |
| countFun-base-01 | ⊦ countFun(i + 1, i, intfun) = [] | A User Theorem |
| countFun-base-02 | ⊦ countFun(j, j - 1, intfun) = [] | A User Theorem |
| countFun-base-03 | ⊦ countFun(0, ~1, intfun) = [] | A User Theorem |
| countFun-dist | ⊦ 0 ≤ i ∧ i ≤ j → Σ countFun(i, j, λ j0. intfun1(j0) + intfun2(j0)) = Σ countFun(i, j, λ j0. intfun1(j0)) + Σ countFun(i, j, λ j0. intfun2(j0)) | A User Theorem |
| countFun-in | ⊦ i0 ∈ countFun(i, j, intfun) ↔ (∃ j0. i ≤ j0 ∧ j0 ≤ j ∧ intfun(j0) = i0) | A User Theorem |
| countFun-in-01 | ⊦ i ≤ i0 ∧ i0 ≤ j → intfun(i0) ∈ countFun(i, j, intfun) | A User Theorem |
| countFun-last | ⊦ i ≤ j → countFun(i, j, intfun) = countFun(i, j - 1, intfun) + intfun(j) ' | A User Theorem |
| countFun-last-01 | ⊦ i ≤ j ∧ 0 ≤ i → countFun(i, j, intfun) = countFun(i, j - 1, intfun) + intfun(j) ' | A User Theorem |
| countFun-length | ⊦ 0 ≤ i ∧ i ≤ j → # countFun(i, j, intfun) = i→n(1 + j - i) | A User Theorem |
| countFun-mult | ⊦ i0 * Σ countFun(i, j, intfun) = Σ countFun(i, j, λ j0. i0 * intfun(j0)) | A User Theorem |
| countFun-one | ⊦ countFun(i, i, intfun) = intfun(i) ' | A User Theorem |
| divide-list-at-value | ⊦ ∃ ints0, ints1. perm(ints, ints0 + ints1) ∧ (ints0 = [] ∨ max(ints0) ≤ j) ∧ (ints1 = [] ∨ j < min(ints1)) | A User Theorem |
| euler-phi-prime | ⊦ prime(i) → euler-phi(i) = i - 1 | A User Theorem |
| filterFun-all | ∀ i. i ∈ ints → intboolfun(i) ⊦ filterFun(intboolfun, ints) = ints | A User Theorem |
| filterFun-append | ⊦ filterFun(intboolfun, ints + ints0) = filterFun(intboolfun, ints) + filterFun(intboolfun, ints0) | A User Theorem |
| filterFun-in | ⊦ i ∈ filterFun(intboolfun, ints) ↔ i ∈ ints ∧ intboolfun(i) | A User Theorem |
| filterFun-max | ⊦ filterFun(intboolfun, ints) ≠ [] → max(filterFun(intboolfun, ints)) ≤ max(ints) | A User Theorem |
| filterFun-min | ⊦ filterFun(intboolfun, ints) ≠ [] → min(ints) ≤ min(filterFun(intboolfun, ints)) | A User Theorem |
| filterFun-no-dups | ⊦ ¬ dups(ints) → ¬ dups(filterFun(intboolfun, ints)) | A User Theorem |
| filterFun-no-dups-01 | ⊦ ¬ dups(filterFun(intboolfun, count-i2j(1, j))) | A User Theorem |
| filterFun-not-in | ⊦ ¬ i ∈ ints → ¬ i ∈ filterFun(intboolfun, ints) | A User Theorem |
| filterFun-one | ⊦ filterFun(intboolfun, i ') = (intboolfun(i) ⊃ i ';[]) | A User Theorem |
| filterFun-ordered | ⊦ ordered≤(ints) → ordered≤(filterFun(intboolfun, ints)) | A User Theorem |
| map-at | ⊦ n < # ints → mapFun(intfun, ints)[n] = intfun(ints[n]) | A User Theorem |
| map-in | ⊦ i ∈ mapFun(intfun, ints) ↔ (∃ j. j ∈ ints ∧ intfun(j) = i) | A User Theorem |
| map-length | ⊦ # mapFun(intfun, ints) = # ints | A User Theorem |
| max-app | ⊦ ints ≠ [] ∧ ints0 ≠ [] → max(ints + ints0) = max(max(ints), max(ints0)) | A User Theorem |
| max-app-ls | ⊦ max(ints1 + ints0) < max(ints0) ↔ ints0 = [] ∧ max(ints1) < 0 | A User Theorem |
| max-app-ls-01 | ⊦ max(ints1 + ints0) < max(ints1) ↔ ints1 = [] ∧ max(ints0) < 0 | A User Theorem |
| max-del1 | ⊦ i < max(ints) → max(ints -1l i) = max(ints) | A User Theorem |
| max-del1-01 | ⊦ ints ≠ [] → (max(ints) < max(ints -1l i) ↔ ints = i ' ∧ i < 0) | A User Theorem |
| max-in | ⊦ ints ≠ [] → (¬ max(ints) ∈ ints ↔ false) | A User Theorem |
| max-in-01 | ⊦ max(ints) ∈ ints ↔ ints ≠ [] | A User Theorem |
| max-in-not-ls | ⊦ i ∈ ints → ¬ max(ints) < i | A User Theorem |
| max-is-max | ⊦ ints ≠ [] ∧ i ∈ ints → ¬ max(ints) < i | A User Theorem |
| max-last-max | ⊦ max(ints) < i ∧ ints ≠ [] → max(ints + i ') = i | A User Theorem |
| max-last-not-max | ⊦ i ≤ max(ints) ∧ ints ≠ [] → max(ints + i ') = max(ints) | A User Theorem |
| max-le-rec | ⊦ 0 < j → (max(i ' + ints) ≤ j ↔ i ≤ j ∧ max(ints) ≤ j) | A User Theorem |
| max-one | ⊦ max(i ') = i | A User Theorem |
| max-perm | ⊦ max(ints) ≠ max(ints0) → ¬ perm(ints, ints0) | A User Theorem |
| max-perm-ls | ⊦ max(ints) < max(ints0) ∧ ints0 ≠ [] → ¬ perm(ints, ints1 + ints0) | A User Theorem |
| max-rec | ⊦ ints ≠ [] → max(i ' + ints) = max(i, max(ints)) | A User Theorem |
| min-del-nlz | ⊦ 0 < min(i ' + ints) → ¬ min(ints -l i0) < 0 | A User Theorem |
| min-del-nlz-01 | ⊦ 0 < min(ints) → ¬ min(ints -l i0) < 0 | A User Theorem |
| min-in | ⊦ min(ints) ∈ ints ↔ ints ≠ [] | A User Theorem |
| min-in-nle | ⊦ i < j → ¬ j ≤ min(i ' + ints) | A User Theorem |
| min-in-nls | ⊦ i < j → ¬ j < min(i ' + ints) | A User Theorem |
| min-in-not-ls | ⊦ i ∈ ints → ¬ i < min(ints) | A User Theorem |
| min-one | ⊦ min(i ') = i | A User Theorem |
| min-rec | ⊦ ints ≠ [] → min(i ' + ints) = min(i, min(ints)) | A User Theorem |
| nodups-interval-size | ¬ dups(ints), ∀ i. i ∈ ints → j0 < i ∧ i ≤ j1, ints ≠ [] ⊦ n→i(# ints) ≤ j1 - j0 | A User Theorem |
| primes-in | ⊦ primes(ints) ∧ i ∈ ints → (¬ prime(i) ↔ false) | A User Theorem |
| primes-le-2 | ⊦ primes(ints) ∧ ¬ dups(ints) ∧ ints ≠ [] → (max(ints) ≤ 2 ↔ ints = 2 ') | A User Theorem |
| primes-max-even | ⊦ primes(ints) ∧ ints ≠ [] → (even(max(ints)) ↔ max(ints) = 2) | A User Theorem |
| primes-not-neg | ⊦ i < 0 ∧ i ∈ ints → ¬ primes(ints) | A User Theorem |
| primes-one | ⊦ primes(i ') ↔ prime(i) | A User Theorem |
| primes-perm | ⊦ ¬ primes(ints0) ∧ primes(ints) → ¬ perm(ints, ints0) | A User Theorem |
| primes-perm-01 | ⊦ ¬ primes(ints1) ∧ primes(ints) → ¬ perm(ints, ints1 + ints0) | A User Theorem |
| primes-perm-02 | ⊦ ¬ primes(ints0) ∧ primes(ints) → ¬ perm(ints, ints1 + ints0) | A User Theorem |
| primes-product-not-neg | ⊦ primes(ints) → ¬ Π ints < 0 | A User Theorem |
| primes-rec | ⊦ primes(i ' + ints) ↔ prime(i) ∧ primes(ints) | A User Theorem |
| product-app | ⊦ Π(ints + ints0) = Π ints * Π ints0 | A User Theorem |
| product-del1 | ⊦ i ∈ ints ∧ i ≠ 0 → Π(ints -1l i) * i = Π ints | A User Theorem |
| product-del1-01 | ⊦ i ∈ ints ∧ i ≠ 0 → Π(ints -1l i) = Π ints / i | A User Theorem |
| product-del1-02 | ⊦ i ∈ ints → i * Π(ints -1l i) = Π ints | A User Theorem |
| product-divide | ⊦ perm(ints, ints0 + ints1) → Π ints = Π ints0 * Π ints1 | A User Theorem |
| product-equal-01 | ¬ dups(ints), ¬ dups(ints0), ∀ i. i ∈ ints ↔ i ∈ ints0 ⊦ Π ints = Π ints0 | A User Theorem |
| product-last | ⊦ Π(ints + i ') = i * Π ints | A User Theorem |
| product-min-nlz | ⊦ 0 < min(i ' + ints) → ¬ Π(ints -l i0) < 0 | A User Theorem |
| product-min-not-ls-zero | ⊦ 0 ≤ min(ints) → ¬ Π ints < 0 | A User Theorem |
| product-mult | ⊦ Π ints * Π ints0 = Π(ints + ints0) | A User Theorem |
| product-negative | ∀ i. i ∈ ints → 0 ≤ i ⊦ ¬ Π ints < 0 | A User Theorem |
| product-one | ⊦ Π i ' = i | A User Theorem |
| product-perm-equal | ⊦ perm(ints, ints0) → Π ints = Π ints0 | A User Theorem |
| product-positive | ∀ i. i ∈ ints → 0 < i ⊦ ¬ Π ints ≤ 0 | A User Theorem |
| product-prime-divides | ⊦ prime(i) → (i | Π ints ↔ (∃ j. j ∈ ints ∧ i | j)) | A User Theorem |
| product-zero | ⊦ 0 ∈ ints → Π ints = 0 | A User Theorem |
| range-dups | ∀ i. i ∈ ints → 0 ≤ i ∧ i < j, 0 ≤ j, j < n→i(# ints) ⊦ dups(ints) | A User Theorem |
| sum-all-elems-le | ∀ i. i ∈ ints → i ≤ i0 ⊦ Σ ints ≤ i0 * n→i(# ints) | A User Theorem |
| sum-all-indices-le | ∀ n. 0 ≤ n ∧ n < # ints → ints[n] ≤ ints0[n], # ints = # ints0 ⊦ Σ ints ≤ Σ ints0 | A User Theorem |
| sum-app | ⊦ Σ(ints + ints0) = Σ ints + Σ ints0 | A User Theorem |
| sum-constant-countFun | ∀ i1. i ≤ i1 ∧ i1 ≤ j → intfun(i1) = i0, i ≤ j, 0 ≤ i ⊦ Σ countFun(i, j, intfun) = (1 + j - i) * i0 | A User Theorem |
| sum-countFun-sub | ⊦ 0 ≤ i → Σ countFun(i, j, intfun) - Σ countFun(i, j, intfun0) = Σ countFun(i, j, λ i0. intfun(i0) - intfun0(i0)) | A User Theorem |
| sum-countfun-not-ls | ∃ i1, j1. i0 ≤ i1 ∧ i1 ≤ j0 ∧ intfun(i1) = i ∧ i0 ≤ j1 ∧ j1 ≤ j0 ∧ intfun(j1) = j ∧ i1 ≠ j1, ∀ i1. i0 ≤ i1 ∧ i1 ≤ j0 → 0 ≤ intfun(i1), 0 ≤ i0 ⊦ ¬ Σ countFun(i0, j0, intfun) < i + j | A User Theorem |
| sum-equal | # ints = # ints0, ∀ n. n < # ints → ints[n] = ints0[n] ⊦ Σ ints = Σ ints0 ↔ true | A User Theorem |
| sum-in-not-ls | j ∈ ints, ∀ i. i ∈ ints → 0 ≤ i ⊦ ¬ Σ ints < j | A User Theorem |
| sum-not-ls-zero | ∀ i. i ∈ ints → 0 ≤ i ⊦ ¬ Σ ints < 0 | A User Theorem |
| sum-one | ⊦ Σ i ' = i | A User Theorem |
| sum-positive | ∀ i. i ∈ ints → 0 ≤ i ⊦ 0 ≤ Σ ints | A User Theorem |
| sum-rec-01 | ⊦ ints ≠ [] → Σ ints = ints.first + Σ ints.rest | A User Theorem |