| Name | Conclusion | Link |
|---|---|---|
| natural-prime_1 | ~prime 0 | link to proof |
| natural-prime_2 | ~prime 1 | link to proof |
| natural-prime_3 | prime 2 | link to proof |
| natural-prime_4 | prime 3 | link to proof |
| natural-prime_5 | primes_below 0 = [] | link to proof |
| natural-prime_6 | primes = sunfold next_sieve init_sieve | link to proof |
| natural-prime_7 | max_sieve init_sieve = 1 | link to proof |
| natural-prime_8 | primes_below 1 = [] | link to proof |
| natural-prime_9 | sunfold next_sieve init_sieve = primes | link to proof |
| natural-prime_10 | !i. prime (snth primes i) | link to proof |
| natural-prime_11 | ~(snth primes 0 = 0) | link to proof |
| natural-prime_12 | primes_below 2 = [] | link to proof |
| natural-prime_13 | !a. mk_sieve (dest_sieve a) = a | link to proof |
| natural-prime_14 | !n i. is_counters_sieve n i [] | link to proof |
| natural-prime_15 | init_sieve = mk_sieve (1,[]) | link to proof |
| natural-prime_16 | snth primes 0 = 2 | link to proof |
| natural-prime_17 | !i. ~(snth primes i = 0) | link to proof |
| natural-prime_18 | !s. max_sieve s = FST (dest_sieve s) | link to proof |
| natural-prime_19 | !n. ?p. n <= p /\ prime p | link to proof |
| natural-prime_20 | !i. primes_below (snth primes i) = stake primes i | link to proof |
| natural-prime_21 | !s. primes_sieve s = MAP FST (SND (dest_sieve s)) | link to proof |
| natural-prime_22 | !r. is_sieve r <=> dest_sieve (mk_sieve r) = r | link to proof |
| natural-prime_23 | primes_below 3 = [2] | link to proof |
| natural-prime_24 | !s. primes_sieve s = primes_below (max_sieve s + 1) | link to proof |
| natural-prime_25 | !p. prime p <=> (?i. snth primes i = p) | link to proof |
| natural-prime_26 | !p. prime p /\ EVEN p ==> p = 2 | link to proof |
| natural-prime_27 | !n. primes_below n = stake primes (minimal i. n <= snth primes i) | link to proof |
| natural-prime_28 | !i j. i < j ==> snth primes i < snth primes j | link to proof |
| natural-prime_29 | !i j. i <= j ==> snth primes i <= snth primes j | link to proof |
| natural-prime_30 | !n p. MEM p (primes_below n) <=> prime p /\ p < n | link to proof |
| natural-prime_31 | !n1 n2. snth primes n1 = snth primes n2 <=> n1 = n2 | link to proof |
| natural-prime_32 | !i j. snth primes i < snth primes j <=> i < j | link to proof |
| natural-prime_33 | !i j. snth primes i <= snth primes j <=> i <= j | link to proof |
| natural-prime_34 | !n1 n2. divides (snth primes n1) (snth primes n2) <=> n1 = n2 | link to proof |
| natural-prime_35 | !n1 n2. snth primes n1 = snth primes n2 ==> n1 = n2 | link to proof |
| natural-prime_36 | !n1 n2. divides (snth primes n1) (snth primes n2) ==> n1 = n2 | link to proof |
| natural-prime_37 | !n. ~(n = 1) ==> (?p. prime p /\ divides p n) | link to proof |
| natural-prime_38 | !n. primes_below (SUC n) = APPEND (primes_below n) (if prime n then [n] else []) | link to proof |
| natural-prime_39 | !i j. ~divides (snth primes i) (snth primes (i + j + 1)) | link to proof |
| natural-prime_40 | !p1 p2. prime p1 /\ prime p2 /\ divides p1 p2 ==> p1 = p2 | link to proof |
| natural-prime_41 | !p n. prime p ==> (gcd p n = 1 <=> ~divides p n) | link to proof |
| natural-prime_42 | !n i. inc_counters_sieve n i [] = T,[n,0,0] | link to proof |
| natural-prime_43 | !p n. prime p /\ ~divides p n ==> gcd p n = 1 | link to proof |
| natural-prime_44 | !p m n. prime p ==> (divides p (m * n) <=> divides p m \/ divides p n) | link to proof |
| natural-prime_45 | !n. prime n <=> ~(n = 0) /\ ~(n = 1) /\ ALL (\p. ~divides p n) (primes_below n) | link to proof |
| natural-prime_46 | !p m n. prime p /\ ~divides p m /\ ~divides p n ==> ~divides p (m * n) | link to proof |
| natural-prime_47 | !p. prime p <=> ~(p = 1) /\ (!n. divides n p ==> n = 1 \/ n = p) | link to proof |
| natural-prime_48 | !s. next_sieve s = (let b,s' = inc_sieve s in if b then max_sieve s',s' else next_sieve s') | link to proof |
| natural-prime_49 | !n i. EX (\p. divides p (n + 2)) (stake primes i) \/ snth primes i <= n + 2 | link to proof |
| natural-prime_50 | !s b s'. inc_sieve s = b,s' ==> max_sieve s' = max_sieve s + 1 /\ (b <=> prime (max_sieve s')) | link to proof |
| natural-prime_51 | !n ps. is_sieve (n,ps) <=> ~(n = 0) /\ MAP FST ps = primes_below (n + 1) /\ is_counters_sieve n 0 ps | link to proof |
| natural-prime_52 | !n. prime n <=> ~(n = 0) /\ ~(n = 1) /\ (!p. prime p /\ p < n ==> ~divides p n) | link to proof |
| natural-prime_53 | !ps. ps = primes <=> (!i j. snth ps i <= snth ps j <=> i <= j) /\ (!p. prime p <=> (?i. snth ps i = p)) | link to proof |
| natural-prime_54 | inc_sieve = (\s. let n,ps = dest_sieve s in let n' = n + 1 in let b,ps' = inc_counters_sieve n' 1 ps in b,mk_sieve (n',ps')) | link to proof |
| natural-prime_55 | !n i p k j ps. is_counters_sieve n i (CONS (p,k,j) ps) <=> ~(p = 0) /\ (k + i) MOD p = n MOD p /\ is_counters_sieve n (i + j) ps | link to proof |
| natural-prime_56 | !s. inc_sieve s = (let n,ps = dest_sieve s in let n' = n + 1 in let b,ps' = inc_counters_sieve n' 1 ps in b,mk_sieve (n',ps')) | link to proof |
| natural-prime_57 | !n i p k j ps. inc_counters_sieve n i (CONS (p,k,j) ps) = (let k' = (k + i) MOD p in let j' = j + i in if k' = 0 then F,CONS (p,0,j') ps else let b,ps' = inc_counters_sieve n j' ps in b,CONS (p,k',0) ps') | link to proof |
| natural-prime_58 | !ps. ps = primes <=> ~(snth ps 0 = 0) /\ (!i j. snth ps i <= snth ps j <=> i <= j) /\ (!i j. ~divides (snth ps i) (snth ps (i + j + 1))) /\ (!n i. EX (\p. divides p (n + 2)) (stake ps i) \/ snth ps i <= n + 2) | link to proof |
| natural-prime_59 | (!n i. inc_counters_sieve n i [] = T,[n,0,0]) /\ (!n i p k j ps. inc_counters_sieve n i (CONS (p,k,j) ps) = (let k' = (k + i) MOD p in let j' = j + i in if k' = 0 then F,CONS (p,0,j') ps else let b,ps' = inc_counters_sieve n j' ps in b,CONS (p,k',0) ps')) | link to proof |