Package natural-prime-stream: The ordered stream of all prime numbers

Information

namenatural-prime-stream
version1.14
descriptionThe ordered stream of all prime numbers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
requiresbool
list
natural
natural-divides
natural-prime-thm
stream
showData.Bool
Data.List
Data.Stream
Number.Natural

Files

Defined Constants

Theorems

Prime.below 0 = []

Prime.below 1 = []

i. prime (nth Prime.all i)

Prime.below 2 = []

nth Prime.all 0 = 2

i. ¬(nth Prime.all i = 0)

Prime.below 3 = 2 :: []

p. prime p i. nth Prime.all i = p

n. Prime.below n = take Prime.all (minimal i. n nth Prime.all i)

n p. member p (Prime.below n) prime p p < n

n1 n2. nth Prime.all n1 = nth Prime.all n2 n1 = n2

i j. nth Prime.all i < nth Prime.all j i < j

i j. nth Prime.all i nth Prime.all j i j

n1 n2. divides (nth Prime.all n1) (nth Prime.all n2) n1 = n2

n1 n2. nth Prime.all n1 = nth Prime.all n2 n1 = n2

n1 n2. divides (nth Prime.all n1) (nth Prime.all n2) n1 = n2

n. Prime.below (suc n) = Prime.below n @ if prime n then n :: [] else []

n.
    prime n ¬(n = 0) ¬(n = 1) all (λp. ¬divides p n) (Prime.below n)

Input Type Operators

Input Constants

Assumptions

¬prime 0

¬prime 1

prime 2

¬

bit0 0 = 0

t. t t

n. 0 n

n. n n

a. divides a a

p. p

(minimal n. ) = 0

x. ¬member x []

t. t ¬t

m. ¬(m < 0)

n. n < suc n

(¬) = λp. p

() = λp. p ((select) p)

t. (x. t) t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t t

n. 0 + n = n

l. [] @ l = l

l. l @ [] = l

s. take s 0 = []

t. ( t) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

() = λp q. p q p

t. (t ) (t )

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

n. p. n p prime p

n. bit0 (suc n) = suc (suc (bit0 n))

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

() = λp q. (λf. f p q) = λf. f

() = λp. q. (x. p x q) q

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

() = λp q. r. (p r) (q r) r

m n. m n m < n m = n

m n. m n n m m = n

p l. (x. member x l p x) all p l

m n. m < n m n ¬(m = n)

m n. m < suc n m = n m < n

p. (x. y. p x y) y. x. p x (y x)

p1 p2. prime p1 prime p2 divides p1 p2 p1 = p2

p. p 0 (n. p n p (suc n)) n. p n

s n. take s (suc n) = take s n @ nth s n :: []

x h t. member x (h :: t) x = h member x t

p q r. p (q r) p q p r

l1 l2 x. member x (l1 @ l2) member x l1 member x l2

p n. p n (m. m < n ¬p m) (minimal) p = n

p c x y. p (if c then x else y) (c p x) (¬c p y)

n. prime n ¬(n = 0) ¬(n = 1) p. prime p p < n ¬divides p n

p.
    (m. n. m n p n)
    s. (i j. nth s i nth s j i j) n. p n i. nth s i = n