-
Notifications
You must be signed in to change notification settings - Fork 0
/
matita-arithmetics-chebyshev-bertrand256.agda
105 lines (69 loc) · 54.4 KB
/
matita-arithmetics-chebyshev-bertrand256.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
open import Agda.Primitive
open import matita-basics-types
open import matita-arithmetics-div-and-mod
open import matita-arithmetics-primes
open import matita-basics-bool
open import matita-basics-lists-list
open import matita-arithmetics-chebyshev-bertrand
open import matita-arithmetics-exp
open import matita-basics-logic
open import matita-arithmetics-nat
list-divides : (X---v : list lzero nat) -> (X--1-v : nat) -> bool
list-divides nil' n-v = false
list-divides (cons' m-v tl-v) n-v = orb (dividesb m-v n-v) (list-divides tl-v n-v)
list-divides-true : (l : list lzero nat) -> (n : nat) -> (X-- : eq lzero bool (list-divides l n) true) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p l) (divides p n))
list-divides-true = λ (l : list lzero nat) -> list-ind lzero lzero nat (λ (X-x-716 : list lzero nat) -> (n : nat) -> (X-- : eq lzero bool (list-divides X-x-716 n) true) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p X-x-716) (divides p n))) (λ (n : nat) -> λ (H : eq lzero bool false true) -> bool-discr lzero false true H (ex lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p (nil lzero nat)) (divides p n)))) (λ (a : nat) -> λ (tl : list lzero nat) -> λ (Hind : (n : nat) -> (X-- : eq lzero bool (list-divides tl n) true) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p tl) (divides p n))) -> λ (b : nat) -> match-Or lzero lzero (eq lzero bool (dividesb a b) true) (eq lzero bool (dividesb a b) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (dividesb a b) true) (eq lzero bool (dividesb a b) false)) -> (X--1 : eq lzero bool (list-divides (cons lzero nat a tl) b) true) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p (cons lzero nat a tl)) (divides p b))) (λ (Hcase : eq lzero bool (dividesb a b) true) -> λ (X-- : eq lzero bool (list-divides (cons lzero nat a tl) b) true) -> ex-intro lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p (cons lzero nat a tl)) (divides p b)) a (conj lzero lzero (mem lzero nat a (cons lzero nat a tl)) (divides a b) (or-introl lzero lzero (eq lzero nat a a) (mem lzero nat a tl) (refl lzero nat a)) (dividesb-true-to-divides a b (rewrite-r lzero lzero bool true (λ (X--1 : bool) -> eq lzero bool X--1 true) (refl lzero bool true) (dividesb a b) Hcase)))) (λ (Hcase : eq lzero bool (dividesb a b) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> (X--1 : eq lzero bool (match-bool lzero (λ (X-0 : bool) -> bool) true (list-divides tl b) x) true) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p (cons lzero nat a tl)) (divides p b))) (λ (Htl : eq lzero bool (list-divides tl b) true) -> match-ex lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p tl) (divides p b)) lzero (λ (X-- : ex lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p tl) (divides p b))) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p (cons lzero nat a tl)) (divides p b))) (λ (d : nat) -> λ (X-clearme : And lzero lzero (mem lzero nat d tl) (divides d b)) -> match-And lzero lzero (mem lzero nat d tl) (divides d b) lzero (λ (X-- : And lzero lzero (mem lzero nat d tl) (divides d b)) -> ex lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p (cons lzero nat a tl)) (divides p b))) (λ (memd : mem lzero nat d tl) -> λ (divd : divides d b) -> ex-intro lzero lzero nat (λ (p : nat) -> And lzero lzero (mem lzero nat p (cons lzero nat a tl)) (divides p b)) d (conj lzero lzero (mem lzero nat d (cons lzero nat a tl)) (divides d b) (or-intror lzero lzero (eq lzero nat d a) (mem lzero nat d tl) memd) divd)) X-clearme) (Hind b Htl)) (dividesb a b) Hcase) (true-or-false (dividesb a b))) l
list-divides-false : (l : list lzero nat) -> (n : nat) -> (X-- : eq lzero bool (list-divides l n) false) -> (p : nat) -> (X--1 : mem lzero nat p l) -> Not lzero (divides p n)
list-divides-false = λ (l : list lzero nat) -> list-ind lzero lzero nat (λ (X-x-716 : list lzero nat) -> (n : nat) -> (X-- : eq lzero bool (list-divides X-x-716 n) false) -> (p : nat) -> (X--1 : mem lzero nat p X-x-716) -> Not lzero (divides p n)) (λ (n : nat) -> λ (X-- : eq lzero bool (list-divides (nil lzero nat) n) false) -> λ (p : nat) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> Not lzero (divides p n))) (λ (a : nat) -> λ (tl : list lzero nat) -> λ (Hind : (n : nat) -> (X-- : eq lzero bool (list-divides tl n) false) -> (p : nat) -> (X--1 : mem lzero nat p tl) -> Not lzero (divides p n)) -> λ (b : nat) -> match-Or lzero lzero (eq lzero bool (dividesb a b) true) (eq lzero bool (dividesb a b) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (dividesb a b) true) (eq lzero bool (dividesb a b) false)) -> (X--1 : eq lzero bool (list-divides (cons lzero nat a tl) b) false) -> (p : nat) -> (X--2 : mem lzero nat p (cons lzero nat a tl)) -> Not lzero (divides p b)) (λ (Hcase : eq lzero bool (dividesb a b) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> (X--1 : eq lzero bool (match-bool lzero (λ (X-0 : bool) -> bool) true (list-divides tl b) x) false) -> (p : nat) -> (X--2 : mem lzero nat p (cons lzero nat a tl)) -> Not lzero (divides p b)) (λ (H : eq lzero bool true false) -> bool-discr lzero true false H ((p : nat) -> (X-- : mem lzero nat p (cons lzero nat a tl)) -> Not lzero (divides p b))) (dividesb a b) Hcase) (λ (Hcase : eq lzero bool (dividesb a b) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> (X--1 : eq lzero bool (match-bool lzero (λ (X-0 : bool) -> bool) true (list-divides tl b) x) false) -> (p : nat) -> (X--2 : mem lzero nat p (cons lzero nat a tl)) -> Not lzero (divides p b)) (λ (Htl : eq lzero bool (list-divides tl b) false) -> λ (d : nat) -> λ (X-clearme : mem lzero nat d (cons lzero nat a tl)) -> match-Or lzero lzero (eq lzero nat d a) (mem lzero nat d tl) lzero (λ (X-- : Or lzero lzero (eq lzero nat d a) (mem lzero nat d tl)) -> Not lzero (divides d b)) (λ (eqda : eq lzero nat d a) -> eq-ind-r lzero lzero nat a (λ (x : nat) -> λ (X-- : eq lzero nat x a) -> Not lzero (divides x b)) (dividesb-false-to-not-divides a b (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (dividesb a b) Hcase)) d eqda) (λ (memd : mem lzero nat d tl) -> Hind b (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (list-divides tl b) Htl) d memd) X-clearme) (dividesb a b) Hcase) (true-or-false (dividesb a b))) l
lprim : (X---v : nat) -> (X--1-v : nat) -> (X--2-v : list lzero nat) -> list lzero nat
lprim O i-v acc-v = acc-v
lprim (S m1-v) i-v acc-v = match-bool lzero (λ (X--1-v : bool) -> list lzero nat) (lprim m1-v (S i-v) acc-v) (lprim m1-v (S i-v) (append lzero nat acc-v (cons lzero nat i-v (nil lzero nat)))) (list-divides acc-v i-v)
list-of-primes : (X-n : nat) -> list lzero nat
list-of-primes = λ (n : nat) -> lprim n (S (S O)) (nil lzero nat)
lop-Strue : (m : nat) -> (i : nat) -> (acc : list lzero nat) -> (X-- : eq lzero bool (list-divides acc i) true) -> eq lzero (list lzero nat) (lprim (S m) i acc) (lprim m (S i) acc)
lop-Strue = λ (m : nat) -> λ (i : nat) -> λ (acc : list lzero nat) -> λ (Hdiv : eq lzero bool (list-divides acc i) true) -> eq-ind-r lzero lzero bool true (λ (x : bool) -> λ (X-- : eq lzero bool x true) -> eq lzero (list lzero nat) (match-bool lzero (λ (X-0 : bool) -> list lzero nat) (lprim m (S i) acc) (lprim m (S i) (append lzero nat acc (cons lzero nat i (nil lzero nat)))) x) (lprim m (S i) acc)) (refl lzero (list lzero nat) (match-bool lzero (λ (X-- : bool) -> list lzero nat) (lprim m (S i) acc) (lprim m (S i) (append lzero nat acc (cons lzero nat i (nil lzero nat)))) true)) (list-divides acc i) Hdiv
lop-Sfalse : (m : nat) -> (i : nat) -> (acc : list lzero nat) -> (X-- : eq lzero bool (list-divides acc i) false) -> eq lzero (list lzero nat) (lprim (S m) i acc) (lprim m (S i) (append lzero nat acc (cons lzero nat i (nil lzero nat))))
lop-Sfalse = λ (m : nat) -> λ (i : nat) -> λ (acc : list lzero nat) -> λ (Hdiv : eq lzero bool (list-divides acc i) false) -> eq-ind-r lzero lzero bool false (λ (x : bool) -> λ (X-- : eq lzero bool x false) -> eq lzero (list lzero nat) (match-bool lzero (λ (X-0 : bool) -> list lzero nat) (lprim m (S i) acc) (lprim m (S i) (append lzero nat acc (cons lzero nat i (nil lzero nat)))) x) (lprim m (S i) (append lzero nat acc (cons lzero nat i (nil lzero nat))))) (refl lzero (list lzero nat) (match-bool lzero (λ (X-- : bool) -> list lzero nat) (lprim m (S i) acc) (lprim m (S i) (append lzero nat acc (cons lzero nat i (nil lzero nat)))) false)) (list-divides acc i) Hdiv
list-of-primes-def : (n : nat) -> eq lzero (list lzero nat) (list-of-primes n) (lprim n (S (S O)) (nil lzero nat))
list-of-primes-def = λ (n : nat) -> refl lzero (list lzero nat) (list-of-primes n)
lprim-ex : eq lzero (list lzero nat) (lprim (S (S (S (S (S (S (S (S O)))))))) (S (S O)) (nil lzero nat)) (cons lzero nat (S (S O)) (cons lzero nat (S (S (S O))) (cons lzero nat (S (S (S (S (S O))))) (cons lzero nat (S (S (S (S (S (S (S O))))))) (nil lzero nat)))))
lprim-ex = refl lzero (list lzero nat) (lprim (S (S (S (S (S (S (S (S O)))))))) (S (S O)) (nil lzero nat))
start-lprim : (n : nat) -> (m : nat) -> (a : nat) -> (acc : list lzero nat) -> eq lzero (option lzero nat) (option-hd lzero nat (lprim n m (cons lzero nat a acc))) (Some lzero nat a)
start-lprim = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (m : nat) -> (a : nat) -> (acc : list lzero nat) -> eq lzero (option lzero nat) (option-hd lzero nat (lprim X-x-365 m (cons lzero nat a acc))) (Some lzero nat a)) (λ (m : nat) -> λ (a : nat) -> λ (acc : list lzero nat) -> refl lzero (option lzero nat) (option-hd lzero nat (lprim O m (cons lzero nat a acc)))) (λ (n1 : nat) -> λ (Hind : (m : nat) -> (a : nat) -> (acc : list lzero nat) -> eq lzero (option lzero nat) (option-hd lzero nat (lprim n1 m (cons lzero nat a acc))) (Some lzero nat a)) -> λ (m : nat) -> λ (a : nat) -> λ (acc : list lzero nat) -> match-Or lzero lzero (eq lzero bool (list-divides (cons lzero nat a acc) m) true) (eq lzero bool (list-divides (cons lzero nat a acc) m) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (list-divides (cons lzero nat a acc) m) true) (eq lzero bool (list-divides (cons lzero nat a acc) m) false)) -> eq lzero (option lzero nat) (option-hd lzero nat (lprim (S n1) m (cons lzero nat a acc))) (Some lzero nat a)) (λ (Hc : eq lzero bool (list-divides (cons lzero nat a acc) m) true) -> eq-ind-r lzero lzero (list lzero nat) (lprim n1 (S m) (cons lzero nat a acc)) (λ (x : list lzero nat) -> λ (X-- : eq lzero (list lzero nat) x (lprim n1 (S m) (cons lzero nat a acc))) -> eq lzero (option lzero nat) (option-hd lzero nat x) (Some lzero nat a)) (Hind (S m) a acc) (lprim (S n1) m (cons lzero nat a acc)) (lop-Strue n1 m (cons lzero nat a acc) (rewrite-r lzero lzero bool true (λ (X-- : bool) -> eq lzero bool X-- true) (refl lzero bool true) (list-divides (cons lzero nat a acc) m) Hc))) (λ (Hc : eq lzero bool (list-divides (cons lzero nat a acc) m) false) -> eq-ind-r lzero lzero (list lzero nat) (lprim n1 (S m) (append lzero nat (cons lzero nat a acc) (cons lzero nat m (nil lzero nat)))) (λ (x : list lzero nat) -> λ (X-- : eq lzero (list lzero nat) x (lprim n1 (S m) (append lzero nat (cons lzero nat a acc) (cons lzero nat m (nil lzero nat))))) -> eq lzero (option lzero nat) (option-hd lzero nat x) (Some lzero nat a)) (Hind (S m) a (append lzero nat acc (cons lzero nat m (nil lzero nat)))) (lprim (S n1) m (cons lzero nat a acc)) (lop-Sfalse n1 m (cons lzero nat a acc) (rewrite-r lzero lzero bool false (λ (X-- : bool) -> eq lzero bool X-- false) (refl lzero bool false) (list-divides (cons lzero nat a acc) m) Hc))) (true-or-false (list-divides (cons lzero nat a acc) m))) n
start-lop : (n : nat) -> (X-- : le (S O) n) -> eq lzero (option lzero nat) (option-hd lzero nat (list-of-primes n)) (Some lzero nat (S (S O)))
start-lop = λ (n : nat) -> λ (posn : le (S O) n) -> match-le (S O) lzero (λ (X-- : nat) -> λ (X-0 : le (S O) X--) -> eq lzero (option lzero nat) (option-hd lzero nat (list-of-primes X--)) (Some lzero nat (S (S O)))) (refl lzero (option lzero nat) (option-hd lzero nat (list-of-primes (S O)))) (λ (m : nat) -> λ (lem : le (S O) m) -> eq-ind-r lzero lzero (list lzero nat) (lprim (S m) (S (S O)) (nil lzero nat)) (λ (x : list lzero nat) -> λ (X-- : eq lzero (list lzero nat) x (lprim (S m) (S (S O)) (nil lzero nat))) -> eq lzero (option lzero nat) (option-hd lzero nat x) (Some lzero nat (S (S O)))) (eq-ind-r lzero lzero (option lzero nat) (Some lzero nat (S (S O))) (λ (x : option lzero nat) -> λ (X-- : eq lzero (option lzero nat) x (Some lzero nat (S (S O)))) -> eq lzero (option lzero nat) x (Some lzero nat (S (S O)))) (refl lzero (option lzero nat) (Some lzero nat (S (S O)))) (option-hd lzero nat (lprim m (S (S (S O))) (cons lzero nat (S (S O)) (nil lzero nat)))) (start-lprim m (S (S (S O))) (S (S O)) (nil lzero nat))) (list-of-primes (S m)) (list-of-primes-def (S m))) n posn
eq-lop : (n : nat) -> (X-- : le (S O) n) -> eq lzero (list lzero nat) (list-of-primes n) (cons lzero nat (S (S O)) (tail lzero nat (list-of-primes n)))
eq-lop = λ (n : nat) -> λ (posn : le (S O) n) -> match-list lzero nat lzero (λ (X-- : list lzero nat) -> (X--1 : eq lzero (option lzero nat) (option-hd lzero nat X--) (Some lzero nat (S (S O)))) -> eq lzero (list lzero nat) X-- (cons lzero nat (S (S O)) (tail lzero nat X--))) (λ (H : eq lzero (option lzero nat) (None lzero nat) (Some lzero nat (S (S O)))) -> option-discr lzero nat (None lzero nat) (Some lzero nat (S (S O))) H (eq lzero (list lzero nat) (nil lzero nat) (cons lzero nat (S (S O)) (tail lzero nat (nil lzero nat))))) (λ (a : nat) -> λ (l : list lzero nat) -> λ (H : eq lzero (option lzero nat) (Some lzero nat a) (Some lzero nat (S (S O)))) -> option-discr lzero nat (Some lzero nat a) (Some lzero nat (S (S O))) H (eq lzero (list lzero nat) (cons lzero nat a l) (cons lzero nat (S (S O)) l)) (λ (e0 : eq lzero nat (R0 lzero nat a) (S (S O))) -> eq-ind-r lzero lzero nat (S (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (S (S O))) -> (X--1 : eq lzero (option lzero nat) (Some lzero nat x) (Some lzero nat (S (S O)))) -> eq lzero (list lzero nat) (cons lzero nat x l) (cons lzero nat (S (S O)) l)) (λ (H0 : eq lzero (option lzero nat) (Some lzero nat (S (S O))) (Some lzero nat (S (S O)))) -> streicherK lzero lzero (option lzero nat) (Some lzero nat (S (S O))) (λ (X-- : eq lzero (option lzero nat) (Some lzero nat (S (S O))) (Some lzero nat (S (S O)))) -> eq lzero (list lzero nat) (cons lzero nat (S (S O)) l) (cons lzero nat (S (S O)) l)) (refl lzero (list lzero nat) (cons lzero nat (S (S O)) l)) H0) a e0 H)) (list-of-primes n) (start-lop n posn)
all-primes : (X-l : list lzero nat) -> Set (lzero)
all-primes = λ (l : list lzero nat) -> (p : nat) -> (X-- : mem lzero nat p l) -> prime p
all-below : (X-l : list lzero nat) -> (X-n : nat) -> Set (lzero)
all-below = λ (l : list lzero nat) -> λ (n : nat) -> (p : nat) -> (X-- : mem lzero nat p l) -> lt p n
primes-all : (X-l : list lzero nat) -> (X-n : nat) -> Set (lzero)
primes-all = λ (l : list lzero nat) -> λ (n : nat) -> (p : nat) -> (X-- : prime p) -> (X--1 : lt p n) -> mem lzero nat p l
primes-below : (X-l : list lzero nat) -> (X-n : nat) -> Set (lzero)
primes-below = λ (l : list lzero nat) -> λ (n : nat) -> And lzero lzero (And lzero lzero (all-primes l) (all-below l n)) (primes-all l n)
ld-to-prime : (i : nat) -> (acc : list lzero nat) -> (X-- : lt (S O) i) -> (X--1 : primes-below acc i) -> (X--2 : eq lzero bool (list-divides acc i) false) -> prime i
ld-to-prime = λ (i : nat) -> λ (acc : list lzero nat) -> λ (posi : lt (S O) i) -> λ (X-clearme : primes-below acc i) -> match-And lzero lzero (And lzero lzero (all-primes acc) (all-below acc i)) (primes-all acc i) lzero (λ (X-- : And lzero lzero (And lzero lzero (all-primes acc) (all-below acc i)) (primes-all acc i)) -> (X--1 : eq lzero bool (list-divides acc i) false) -> prime i) (λ (X-clearme0 : And lzero lzero (all-primes acc) (all-below acc i)) -> match-And lzero lzero (all-primes acc) (all-below acc i) lzero (λ (X-- : And lzero lzero (all-primes acc) (all-below acc i)) -> (X--1 : primes-all acc i) -> (X--2 : eq lzero bool (list-divides acc i) false) -> prime i) (λ (Hall : all-primes acc) -> λ (Hbelow : all-below acc i) -> λ (Hcomplete : primes-all acc i) -> λ (Hfalse : eq lzero bool (list-divides acc i) false) -> conj lzero lzero (lt (S O) i) ((m : nat) -> (X-- : divides m i) -> (X--1 : lt (S O) m) -> eq lzero nat m i) posi (λ (m : nat) -> λ (mdivi : divides m i) -> match-Or lzero lzero (lt m i) (eq lzero nat m i) lzero (λ (X-- : Or lzero lzero (lt m i) (eq lzero nat m i)) -> (X--1 : lt (S O) m) -> eq lzero nat m i) (λ (ltmi : lt m i) -> λ (lt1m : lt (S O) m) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> eq lzero nat m i) (absurd lzero (divides (smallest-factor m) i) (transitive-divides (smallest-factor m) m i (divides-smallest-factor-n m (lt-to-le (S O) m lt1m)) mdivi) (list-divides-false acc i Hfalse (smallest-factor m) (Hcomplete (smallest-factor m) (prime-smallest-factor-n m lt1m) (le-to-lt-to-lt (smallest-factor m) m i (le-smallest-factor-n m) ltmi))))) (λ (auto : eq lzero nat m i) -> λ (auto' : lt (S O) m) -> rewrite-r lzero lzero nat i (λ (X-- : nat) -> eq lzero nat X-- i) (refl lzero nat i) m auto) (le-to-or-lt-eq m i (divides-to-le m i (lt-to-le (S O) i posi) mdivi)))) X-clearme0) X-clearme
lprim-invariant : (n : nat) -> (i : nat) -> (acc : list lzero nat) -> (X-- : lt (S O) i) -> (X--1 : primes-below acc i) -> primes-below (lprim n i acc) (plus n i)
lprim-invariant = λ (n : nat) -> nat-ind lzero (λ (X-x-365 : nat) -> (i : nat) -> (acc : list lzero nat) -> (X-- : lt (S O) i) -> (X--1 : primes-below acc i) -> primes-below (lprim X-x-365 i acc) (plus X-x-365 i)) (λ (i : nat) -> λ (acc : list lzero nat) -> λ (lt1i : lt (S O) i) -> λ (H : primes-below acc i) -> H) (λ (m : nat) -> λ (Hind : (i : nat) -> (acc : list lzero nat) -> (X-- : lt (S O) i) -> (X--1 : primes-below acc i) -> primes-below (lprim m i acc) (plus m i)) -> λ (i : nat) -> λ (acc : list lzero nat) -> λ (lt1i : lt (S O) i) -> λ (X-clearme : primes-below acc i) -> match-And lzero lzero (And lzero lzero (all-primes acc) (all-below acc i)) (primes-all acc i) lzero (λ (X-- : And lzero lzero (And lzero lzero (all-primes acc) (all-below acc i)) (primes-all acc i)) -> primes-below (lprim (S m) i acc) (plus (S m) i)) (λ (X-clearme0 : And lzero lzero (all-primes acc) (all-below acc i)) -> match-And lzero lzero (all-primes acc) (all-below acc i) lzero (λ (X-- : And lzero lzero (all-primes acc) (all-below acc i)) -> (X--1 : primes-all acc i) -> primes-below (lprim (S m) i acc) (plus (S m) i)) (λ (Hall : all-primes acc) -> λ (Hbelow : all-below acc i) -> λ (Hcomplete : primes-all acc i) -> match-Or lzero lzero (eq lzero bool (list-divides acc i) true) (eq lzero bool (list-divides acc i) false) lzero (λ (X-- : Or lzero lzero (eq lzero bool (list-divides acc i) true) (eq lzero bool (list-divides acc i) false)) -> primes-below (lprim (S m) i acc) (plus (S m) i)) (λ (Hc : eq lzero bool (list-divides acc i) true) -> eq-ind-r lzero lzero (list lzero nat) (lprim m (S i) acc) (λ (x : list lzero nat) -> λ (X-- : eq lzero (list lzero nat) x (lprim m (S i) acc)) -> primes-below x (plus (S m) i)) (eq-ind-r lzero lzero nat (plus m (S i)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m (S i))) -> primes-below (lprim m (S i) acc) x) (Hind (S i) acc (le-S (S (S O)) i lt1i) (conj lzero lzero (And lzero lzero (all-primes acc) (all-below acc (S i))) (primes-all acc (S i)) (conj lzero lzero (all-primes acc) (all-below acc (S i)) Hall (λ (p : nat) -> λ (memp : mem lzero nat p acc) -> le-S (S p) i (Hbelow p memp))) (λ (p : nat) -> λ (primep : prime p) -> λ (lepi : lt p (S i)) -> match-Or lzero lzero (lt p i) (eq lzero nat p i) lzero (λ (X-- : Or lzero lzero (lt p i) (eq lzero nat p i)) -> mem lzero nat p acc) (λ (ltpi : lt p i) -> Hcomplete p primep ltpi) (λ (eqpi : eq lzero nat p i) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> mem lzero nat p acc) (match-ex lzero lzero nat (λ (p1 : nat) -> And lzero lzero (mem lzero nat p1 acc) (divides p1 i)) lzero (λ (X-- : ex lzero lzero nat (λ (p0 : nat) -> And lzero lzero (mem lzero nat p0 acc) (divides p0 i))) -> False lzero) (λ (q : nat) -> λ (X-clearme1 : And lzero lzero (mem lzero nat q acc) (divides q i)) -> match-And lzero lzero (mem lzero nat q acc) (divides q i) lzero (λ (X-- : And lzero lzero (mem lzero nat q acc) (divides q i)) -> False lzero) (λ (memq : mem lzero nat q acc) -> λ (divqi : divides q i) -> match-And lzero lzero (lt (S O) p) ((m1 : nat) -> (X-- : divides m1 p) -> (X--1 : lt (S O) m1) -> eq lzero nat m1 p) lzero (λ (X-- : And lzero lzero (lt (S O) p) ((m0 : nat) -> (X-- : divides m0 p) -> (X--1 : lt (S O) m0) -> eq lzero nat m0 p)) -> False lzero) (λ (lt1p : lt (S O) p) -> eq-ind-r lzero lzero nat i (λ (x : nat) -> λ (X-- : eq lzero nat x i) -> (X--1 : (m0 : nat) -> (X--1 : divides m0 x) -> (X--2 : lt (S O) m0) -> eq lzero nat m0 x) -> False lzero) (λ (Hi : (m0 : nat) -> (X-- : divides m0 i) -> (X--1 : lt (S O) m0) -> eq lzero nat m0 i) -> absurd lzero (eq lzero nat q i) (Hi q divqi (prime-to-lt-SO q (Hall q memq))) (lt-to-not-eq q i (Hbelow q memq))) p eqpi) primep) X-clearme1) (list-divides-true acc i Hc))) (le-to-or-lt-eq p i (le-S-S-to-le p i lepi))))) (S (plus m i)) (plus-n-Sm m i)) (lprim (S m) i acc) (lop-Strue m i acc Hc)) (λ (Hc : eq lzero bool (list-divides acc i) false) -> eq-ind-r lzero lzero (list lzero nat) (lprim m (S i) (append lzero nat acc (cons lzero nat i (nil lzero nat)))) (λ (x : list lzero nat) -> λ (X-- : eq lzero (list lzero nat) x (lprim m (S i) (append lzero nat acc (cons lzero nat i (nil lzero nat))))) -> primes-below x (plus (S m) i)) (eq-ind-r lzero lzero nat (plus m (S i)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus m (S i))) -> primes-below (lprim m (S i) (append lzero nat acc (cons lzero nat i (nil lzero nat)))) x) (Hind (S i) (append lzero nat acc (cons lzero nat i (nil lzero nat))) (le-S (S (S O)) i lt1i) (conj lzero lzero (And lzero lzero (all-primes (append lzero nat acc (cons lzero nat i (nil lzero nat)))) (all-below (append lzero nat acc (cons lzero nat i (nil lzero nat))) (S i))) (primes-all (append lzero nat acc (cons lzero nat i (nil lzero nat))) (S i)) (conj lzero lzero (all-primes (append lzero nat acc (cons lzero nat i (nil lzero nat)))) (all-below (append lzero nat acc (cons lzero nat i (nil lzero nat))) (S i)) (λ (p : nat) -> λ (memp : mem lzero nat p (append lzero nat acc (cons lzero nat i (nil lzero nat)))) -> match-Or lzero lzero (mem lzero nat p acc) (mem lzero nat p (cons lzero nat i (nil lzero nat))) lzero (λ (X-- : Or lzero lzero (mem lzero nat p acc) (mem lzero nat p (cons lzero nat i (nil lzero nat)))) -> prime p) (λ (memp0 : mem lzero nat p acc) -> Hall p memp0) (λ (memp0 : mem lzero nat p (cons lzero nat i (nil lzero nat))) -> eq-ind-r lzero lzero nat i (λ (x : nat) -> λ (X-- : eq lzero nat x i) -> prime x) (ld-to-prime i acc lt1i (conj lzero lzero (And lzero lzero (all-primes acc) (all-below acc i)) (primes-all acc i) (conj lzero lzero (all-primes acc) (all-below acc i) Hall Hbelow) Hcomplete) Hc) p (mem-single lzero nat p i memp0)) (mem-append lzero nat p acc (cons lzero nat i (nil lzero nat)) memp)) (λ (p : nat) -> λ (memp : mem lzero nat p (append lzero nat acc (cons lzero nat i (nil lzero nat)))) -> match-Or lzero lzero (mem lzero nat p acc) (mem lzero nat p (cons lzero nat i (nil lzero nat))) lzero (λ (X-- : Or lzero lzero (mem lzero nat p acc) (mem lzero nat p (cons lzero nat i (nil lzero nat)))) -> lt p (S i)) (λ (memp0 : mem lzero nat p acc) -> le-S (S p) i (Hbelow p memp0)) (λ (memp0 : mem lzero nat p (cons lzero nat i (nil lzero nat))) -> eq-ind lzero lzero nat p (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat p x-1) -> lt p (S x-1)) (le-n (S p)) i (mem-single lzero nat p i memp0)) (mem-append lzero nat p acc (cons lzero nat i (nil lzero nat)) memp))) (λ (p : nat) -> λ (memp : prime p) -> λ (ltp : lt p (S i)) -> match-Or lzero lzero (lt p i) (eq lzero nat p i) lzero (λ (X-- : Or lzero lzero (lt p i) (eq lzero nat p i)) -> mem lzero nat p (append lzero nat acc (cons lzero nat i (nil lzero nat)))) (λ (ltpi : lt p i) -> mem-append-l1 lzero nat p acc (cons lzero nat i (nil lzero nat)) (Hcomplete p memp ltpi)) (λ (eqpi : eq lzero nat p i) -> mem-append-l2 lzero nat p acc (cons lzero nat i (nil lzero nat)) (eq-ind lzero lzero nat p (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat p x-1) -> mem lzero nat p (cons lzero nat x-1 (nil lzero nat))) (or-introl lzero lzero (eq lzero nat p p) (mem lzero nat p (nil lzero nat)) (rewrite-r lzero lzero nat i (λ (X-- : nat) -> eq lzero nat X-- p) (rewrite-r lzero lzero nat i (λ (X-- : nat) -> eq lzero nat i X--) (refl lzero nat i) p eqpi) p eqpi)) i eqpi)) (le-to-or-lt-eq p i (le-S-S-to-le p i ltp))))) (S (plus m i)) (plus-n-Sm m i)) (lprim (S m) i acc) (lop-Sfalse m i acc Hc)) (true-or-false (list-divides acc i))) X-clearme0) X-clearme) n
primes-below2 : primes-below (nil lzero nat) (S (S O))
primes-below2 = conj lzero lzero (And lzero lzero (all-primes (nil lzero nat)) (all-below (nil lzero nat) (S (S O)))) (primes-all (nil lzero nat) (S (S O))) (conj lzero lzero (all-primes (nil lzero nat)) (all-below (nil lzero nat) (S (S O))) (λ (p : nat) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> prime p)) (λ (p : nat) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> lt p (S (S O))))) (λ (p : nat) -> λ (primep : prime p) -> λ (ltp2 : lt p (S (S O))) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> mem lzero nat p (nil lzero nat)) (absurd lzero (lt p (S (S O))) ltp2 (le-to-not-lt (S (S O)) p (prime-to-lt-SO p primep))))
let-clause-1033'''''''' : (n : nat) -> (x2515 : nat) -> (x2516 : nat) -> eq lzero nat x2515 (plus (times x2516 (div x2515 x2516)) (mod x2515 x2516))
let-clause-1033'''''''' = λ (n : nat) -> λ (x2515 : nat) -> λ (x2516 : nat) -> rewrite-l lzero lzero nat (times (div x2515 x2516) x2516) (λ (X-- : nat) -> eq lzero nat x2515 (plus X-- (mod x2515 x2516))) (div-mod x2515 x2516) (times x2516 (div x2515 x2516)) (commutative-times (div x2515 x2516) x2516)
primes-below-lop : (n : nat) -> primes-below (list-of-primes n) (plus n (S (S O)))
primes-below-lop = λ (n : nat) -> lprim-invariant n (S (S O)) (nil lzero nat) (eq-coerc lzero (lt (mod (S O) O) (plus (plus (mod (S O) O) (times O (div (S O) O))) (S O))) (lt (S O) (S (S O))) (lt-plus-Sn-r (mod (S O) O) (times O (div (S O) O)) O) (rewrite-l lzero (lsuc lzero) nat (S O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (mod (S O) O) (plus X-- (S O))) (lt (S O) (S (S O)))) (rewrite-l lzero (lsuc lzero) nat (S O) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt X-- (plus (S O) (S O))) (lt (S O) (S (S O)))) (rewrite-r lzero (lsuc lzero) nat (S (S O)) (λ (X-- : nat) -> eq (lsuc lzero) (Set (lzero)) (lt (S O) X--) (lt (S O) (S (S O)))) (refl (lsuc lzero) (Set (lzero)) (lt (S O) (S (S O)))) (plus (S O) (S O)) (rewrite-r lzero lzero nat (times (S O) (S O)) (λ (X-- : nat) -> eq lzero nat (plus (S O) X--) (S (S O))) (rewrite-r lzero lzero nat (times (S (S O)) (S O)) (λ (X-- : nat) -> eq lzero nat (plus (S O) (times (S O) (S O))) X--) (times-Sn-m (S O) (S O)) (S (S O)) (times-n-1 (S (S O)))) (S O) (times-n-1 (S O)))) (mod (S O) O) (rewrite-r lzero lzero nat (plus O (mod (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) X--) (rewrite-l lzero lzero nat (plus (mod (S O) O) O) (λ (X-- : nat) -> eq lzero nat (S O) X--) (rewrite-r lzero lzero nat (times O (div (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) (plus (mod (S O) O) X--)) (rewrite-l lzero lzero nat (plus (times O (div (S O) O)) (mod (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) X--) (let-clause-1033'''''''' n (S O) O) (plus (mod (S O) O) (times O (div (S O) O))) (commutative-plus (times O (div (S O) O)) (mod (S O) O))) O (times-O-n (div (S O) O))) (plus O (mod (S O) O)) (commutative-plus (mod (S O) O) O)) (mod (S O) O) (plus-O-n (mod (S O) O)))) (plus (mod (S O) O) (times O (div (S O) O))) (rewrite-l lzero lzero nat (plus (times O (div (S O) O)) (mod (S O) O)) (λ (X-- : nat) -> eq lzero nat (S O) X--) (let-clause-1033'''''''' n (S O) O) (plus (mod (S O) O) (times O (div (S O) O))) (commutative-plus (times O (div (S O) O)) (mod (S O) O))))) primes-below2
primes-below-to-bertrand : (pm : nat) -> (l : list lzero nat) -> (X-- : prime pm) -> (X--1 : primes-below l (S pm)) -> (X--2 : (p : nat) -> (X--2 : mem lzero nat p l) -> (X--3 : lt (S (S O)) p) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp l) (lt pp p)) (le p (times (S (S O)) pp)))) -> (n : nat) -> (X--3 : lt O n) -> (X--4 : lt n pm) -> bertrand n
primes-below-to-bertrand = λ (pm : nat) -> λ (l : list lzero nat) -> λ (primepm : prime pm) -> λ (X-clearme : primes-below l (S pm)) -> match-And lzero lzero (And lzero lzero (all-primes l) (all-below l (S pm))) (primes-all l (S pm)) lzero (λ (X-- : And lzero lzero (And lzero lzero (all-primes l) (all-below l (S pm))) (primes-all l (S pm))) -> (X--1 : (p : nat) -> (X--1 : mem lzero nat p l) -> (X--2 : lt (S (S O)) p) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp l) (lt pp p)) (le p (times (S (S O)) pp)))) -> (n : nat) -> (X--2 : lt O n) -> (X--3 : lt n pm) -> bertrand n) (λ (X-clearme0 : And lzero lzero (all-primes l) (all-below l (S pm))) -> match-And lzero lzero (all-primes l) (all-below l (S pm)) lzero (λ (X-- : And lzero lzero (all-primes l) (all-below l (S pm))) -> (X--1 : primes-all l (S pm)) -> (X--2 : (p : nat) -> (X--2 : mem lzero nat p l) -> (X--3 : lt (S (S O)) p) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp l) (lt pp p)) (le p (times (S (S O)) pp)))) -> (n : nat) -> (X--3 : lt O n) -> (X--4 : lt n pm) -> bertrand n) (λ (Hall : all-primes l) -> λ (Hbelow : all-below l (S pm)) -> λ (Hcomplete : primes-all l (S pm)) -> λ (H : (p : nat) -> (X-- : mem lzero nat p l) -> (X--1 : lt (S (S O)) p) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp l) (lt pp p)) (le p (times (S (S O)) pp)))) -> λ (n : nat) -> λ (posn : lt O n) -> λ (ltn : lt n pm) -> match-ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (prime p)) ((q : nat) -> (X-- : prime q) -> (X--1 : lt q p) -> le q n)) lzero (λ (X-- : ex lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (prime p)) ((q : nat) -> (X-- : prime q) -> (X--1 : lt q p) -> le q n))) -> bertrand n) (λ (p1 : nat) -> λ (X-clearme1 : And lzero lzero (And lzero lzero (lt n p1) (prime p1)) ((q : nat) -> (X-- : prime q) -> (X--1 : lt q p1) -> le q n)) -> match-And lzero lzero (And lzero lzero (lt n p1) (prime p1)) ((q : nat) -> (X-- : prime q) -> (X--1 : lt q p1) -> le q n) lzero (λ (X-- : And lzero lzero (And lzero lzero (lt n p1) (prime p1)) ((q : nat) -> (X-- : prime q) -> (X--1 : lt q p1) -> le q n)) -> bertrand n) (λ (X-clearme2 : And lzero lzero (lt n p1) (prime p1)) -> match-And lzero lzero (lt n p1) (prime p1) lzero (λ (X-- : And lzero lzero (lt n p1) (prime p1)) -> (X--1 : (q : nat) -> (X--1 : prime q) -> (X--2 : lt q p1) -> le q n) -> bertrand n) (λ (ltnp1 : lt n p1) -> λ (primep1 : prime p1) -> λ (Hmin : (q : nat) -> (X-- : prime q) -> (X--1 : lt q p1) -> le q n) -> ex-intro lzero lzero nat (λ (p : nat) -> And lzero lzero (And lzero lzero (lt n p) (le p (times (S (S O)) n))) (prime p)) p1 (conj lzero lzero (And lzero lzero (lt n p1) (le p1 (times (S (S O)) n))) (prime p1) (conj lzero lzero (lt n p1) (le p1 (times (S (S O)) n)) ltnp1 (match-Or lzero lzero (lt (S (S O)) p1) (eq lzero nat (S (S O)) p1) lzero (λ (X-- : Or lzero lzero (lt (S (S O)) p1) (eq lzero nat (S (S O)) p1)) -> le p1 (times (S (S O)) n)) (λ (Hp1 : lt (S (S O)) p1) -> match-ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp l) (lt pp p1)) (le p1 (times (S (S O)) pp))) lzero (λ (X-- : ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp l) (lt pp p1)) (le p1 (times (S (S O)) pp)))) -> le p1 (times (S (S O)) n)) (λ (x : nat) -> λ (X-clearme3 : And lzero lzero (And lzero lzero (mem lzero nat x l) (lt x p1)) (le p1 (times (S (S O)) x))) -> match-And lzero lzero (And lzero lzero (mem lzero nat x l) (lt x p1)) (le p1 (times (S (S O)) x)) lzero (λ (X-- : And lzero lzero (And lzero lzero (mem lzero nat x l) (lt x p1)) (le p1 (times (S (S O)) x))) -> le p1 (times (S (S O)) n)) (λ (X-clearme4 : And lzero lzero (mem lzero nat x l) (lt x p1)) -> match-And lzero lzero (mem lzero nat x l) (lt x p1) lzero (λ (X-- : And lzero lzero (mem lzero nat x l) (lt x p1)) -> (X--1 : le p1 (times (S (S O)) x)) -> le p1 (times (S (S O)) n)) (λ (memxl : mem lzero nat x l) -> λ (ltxp1 : lt x p1) -> λ (Hp10 : le p1 (times (S (S O)) x)) -> transitive-le p1 (times (S (S O)) x) (times (S (S O)) n) Hp10 (monotonic-le-times-r (S (S O)) x n (Hmin x (Hall x memxl) ltxp1))) X-clearme4) X-clearme3) (H p1 (Hcomplete p1 primep1 (le-S-S p1 pm (not-lt-to-le pm p1 (nmk lzero (lt pm p1) (λ (ltpm : lt pm p1) -> absurd lzero (lt n pm) ltn (le-to-not-lt pm n (Hmin pm primepm ltpm))))))) Hp1)) (λ (Hp1 : eq lzero nat (S (S O)) p1) -> eq-ind lzero lzero nat (S (S O)) (λ (x-1 : nat) -> λ (X-x-2 : eq lzero nat (S (S O)) x-1) -> le x-1 (times (S (S O)) n)) (eq-ind-r lzero lzero nat (times (S (S O)) (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (times (S (S O)) (S O))) -> le x (times (S (S O)) n)) (monotonic-le-times-r (S (S O)) (S O) n posn) (S (S O)) (times-n-1 (S (S O)))) p1 Hp1) (le-to-or-lt-eq (S (S O)) p1 (prime-to-lt-SO p1 primep1)))) primep1)) X-clearme2) X-clearme1) (min-prim n)) X-clearme0) X-clearme
checker : (X---v : list lzero nat) -> bool
checker nil' = true
checker (cons' hd-v tl-v) = match-list lzero nat lzero (λ (X--1-v : list lzero nat) -> bool) true (λ (hd1-v : nat) -> λ (tl1-v : list lzero nat) -> andb (andb (leb (S hd-v) hd1-v) (leb hd1-v (times (S (S O)) hd-v))) (checker tl-v)) tl-v
checker-ab : (a : nat) -> (b : nat) -> (l : list lzero nat) -> eq lzero bool (checker (cons lzero nat a (cons lzero nat b l))) (andb (andb (leb (S a) b) (leb b (times (S (S O)) a))) (checker (cons lzero nat b l)))
checker-ab = λ (a : nat) -> λ (b : nat) -> λ (l : list lzero nat) -> refl lzero bool (checker (cons lzero nat a (cons lzero nat b l)))
checker-abl : (a : nat) -> (b : nat) -> (l : list lzero nat) -> (X-- : eq lzero bool (checker (cons lzero nat a (cons lzero nat b l))) true) -> And lzero lzero (And lzero lzero (lt a b) (le b (times (S (S O)) a))) (eq lzero bool (checker (cons lzero nat b l)) true)
checker-abl = λ (a : nat) -> λ (b : nat) -> λ (l : list lzero nat) -> eq-ind-r lzero lzero bool (andb (andb (leb (S a) b) (leb b (times (S (S O)) a))) (checker (cons lzero nat b l))) (λ (x : bool) -> λ (X-- : eq lzero bool x (andb (andb (leb (S a) b) (leb b (times (S (S O)) a))) (checker (cons lzero nat b l)))) -> (X--1 : eq lzero bool x true) -> And lzero lzero (And lzero lzero (lt a b) (le b (times (S (S O)) a))) (eq lzero bool (checker (cons lzero nat b l)) true)) (λ (H : eq lzero bool (andb (andb (leb (S a) b) (leb b (times (S (S O)) a))) (checker (cons lzero nat b l))) true) -> conj lzero lzero (And lzero lzero (lt a b) (le b (times (S (S O)) a))) (eq lzero bool (checker (cons lzero nat b l)) true) (conj lzero lzero (lt a b) (le b (times (S (S O)) a)) (leb-true-to-le (S a) b (andb-true-l (leb (S a) b) (leb b (times (S (S O)) a)) (andb-true-l (andb (leb (S a) b) (leb b (times (S (S O)) a))) (checker (cons lzero nat b l)) H))) (leb-true-to-le b (times (S (S O)) a) (andb-true-r (leb (S a) b) (leb b (times (S (S O)) a)) (andb-true-l (andb (leb (S a) b) (leb b (times (S (S O)) a))) (checker (cons lzero nat b l)) H)))) (andb-true-r (andb (leb (S a) b) (leb b (times (S (S O)) a))) (checker (cons lzero nat b l)) H)) (checker (cons lzero nat a (cons lzero nat b l))) (checker-ab a b l)
checker-spec : (tl : list lzero nat) -> (a : nat) -> (l : list lzero nat) -> (X-- : eq lzero bool (checker l) true) -> (X--1 : eq lzero (list lzero nat) l (cons lzero nat a tl)) -> (p : nat) -> (X--2 : mem lzero nat p tl) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp l) (lt pp p)) (le p (times (S (S O)) pp)))
checker-spec = λ (tl : list lzero nat) -> list-ind lzero lzero nat (λ (X-x-716 : list lzero nat) -> (a : nat) -> (l : list lzero nat) -> (X-- : eq lzero bool (checker l) true) -> (X--1 : eq lzero (list lzero nat) l (cons lzero nat a X-x-716)) -> (p : nat) -> (X--2 : mem lzero nat p X-x-716) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp l) (lt pp p)) (le p (times (S (S O)) pp)))) (λ (a : nat) -> λ (l : list lzero nat) -> λ (X-- : eq lzero bool (checker l) true) -> λ (X-0 : eq lzero (list lzero nat) l (cons lzero nat a (nil lzero nat))) -> λ (p : nat) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp l) (lt pp p)) (le p (times (S (S O)) pp))))) (λ (b : nat) -> λ (tl0 : list lzero nat) -> λ (Hind : (a : nat) -> (l : list lzero nat) -> (X-- : eq lzero bool (checker l) true) -> (X--1 : eq lzero (list lzero nat) l (cons lzero nat a tl0)) -> (p : nat) -> (X--2 : mem lzero nat p tl0) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp l) (lt pp p)) (le p (times (S (S O)) pp)))) -> λ (a : nat) -> λ (l : list lzero nat) -> λ (Hc : eq lzero bool (checker l) true) -> λ (Hl : eq lzero (list lzero nat) l (cons lzero nat a (cons lzero nat b tl0))) -> λ (p : nat) -> λ (Hmem : mem lzero nat p (cons lzero nat b tl0)) -> eq-ind-r lzero lzero (list lzero nat) (cons lzero nat a (cons lzero nat b tl0)) (λ (x : list lzero nat) -> λ (X-- : eq lzero (list lzero nat) x (cons lzero nat a (cons lzero nat b tl0))) -> (X--1 : eq lzero bool (checker x) true) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp x) (lt pp p)) (le p (times (S (S O)) pp)))) (λ (Hc0 : eq lzero bool (checker (cons lzero nat a (cons lzero nat b tl0))) true) -> match-And lzero lzero (And lzero lzero (lt a b) (le b (times (S (S O)) a))) (eq lzero bool (checker (cons lzero nat b tl0)) true) lzero (λ (X-- : And lzero lzero (And lzero lzero (lt a b) (le b (times (S (S O)) a))) (eq lzero bool (checker (cons lzero nat b tl0)) true)) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat a (cons lzero nat b tl0))) (lt pp p)) (le p (times (S (S O)) pp)))) (λ (X-clearme : And lzero lzero (lt a b) (le b (times (S (S O)) a))) -> match-And lzero lzero (lt a b) (le b (times (S (S O)) a)) lzero (λ (X-- : And lzero lzero (lt a b) (le b (times (S (S O)) a))) -> (X--1 : eq lzero bool (checker (cons lzero nat b tl0)) true) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat a (cons lzero nat b tl0))) (lt pp p)) (le p (times (S (S O)) pp)))) (λ (ltab : lt a b) -> λ (leb-v : le b (times (S (S O)) a)) -> λ (Hc2 : eq lzero bool (checker (cons lzero nat b tl0)) true) -> match-Or lzero lzero (eq lzero nat p b) (mem lzero nat p tl0) lzero (λ (X-- : Or lzero lzero (eq lzero nat p b) (mem lzero nat p tl0)) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat a (cons lzero nat b tl0))) (lt pp p)) (le p (times (S (S O)) pp)))) (λ (Hc1 : eq lzero nat p b) -> eq-ind-r lzero lzero nat b (λ (x : nat) -> λ (X-- : eq lzero nat x b) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat a (cons lzero nat b tl0))) (lt pp x)) (le x (times (S (S O)) pp)))) (ex-intro lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat a (cons lzero nat b tl0))) (lt pp b)) (le b (times (S (S O)) pp))) a (conj lzero lzero (And lzero lzero (mem lzero nat a (cons lzero nat a (cons lzero nat b tl0))) (lt a b)) (le b (times (S (S O)) a)) (conj lzero lzero (mem lzero nat a (cons lzero nat a (cons lzero nat b tl0))) (lt a b) (or-introl lzero lzero (eq lzero nat a a) (mem lzero nat a (cons lzero nat b tl0)) (refl lzero nat a)) ltab) leb-v)) p Hc1) (λ (Hc1 : mem lzero nat p tl0) -> match-ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat b tl0)) (lt pp p)) (le p (times (S (S O)) pp))) lzero (λ (X-- : ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat b tl0)) (lt pp p)) (le p (times (S (S O)) pp)))) -> ex lzero lzero nat (λ (pp : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat a (cons lzero nat b tl0))) (lt pp p)) (le p (times (S (S O)) pp)))) (λ (pp : nat) -> λ (X-clearme0 : And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat b tl0)) (lt pp p)) (le p (times (S (S O)) pp))) -> match-And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat b tl0)) (lt pp p)) (le p (times (S (S O)) pp)) lzero (λ (X-- : And lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat b tl0)) (lt pp p)) (le p (times (S (S O)) pp))) -> ex lzero lzero nat (λ (pp0 : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp0 (cons lzero nat a (cons lzero nat b tl0))) (lt pp0 p)) (le p (times (S (S O)) pp0)))) (λ (X-clearme1 : And lzero lzero (mem lzero nat pp (cons lzero nat b tl0)) (lt pp p)) -> match-And lzero lzero (mem lzero nat pp (cons lzero nat b tl0)) (lt pp p) lzero (λ (X-- : And lzero lzero (mem lzero nat pp (cons lzero nat b tl0)) (lt pp p)) -> (X--1 : le p (times (S (S O)) pp)) -> ex lzero lzero nat (λ (pp0 : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp0 (cons lzero nat a (cons lzero nat b tl0))) (lt pp0 p)) (le p (times (S (S O)) pp0)))) (λ (Hmemnp : mem lzero nat pp (cons lzero nat b tl0)) -> λ (ltpp : lt pp p) -> λ (lepp : le p (times (S (S O)) pp)) -> ex-intro lzero lzero nat (λ (pp0 : nat) -> And lzero lzero (And lzero lzero (mem lzero nat pp0 (cons lzero nat a (cons lzero nat b tl0))) (lt pp0 p)) (le p (times (S (S O)) pp0))) pp (conj lzero lzero (And lzero lzero (mem lzero nat pp (cons lzero nat a (cons lzero nat b tl0))) (lt pp p)) (le p (times (S (S O)) pp)) (conj lzero lzero (mem lzero nat pp (cons lzero nat a (cons lzero nat b tl0))) (lt pp p) (or-intror lzero lzero (eq lzero nat pp a) (mem lzero nat pp (cons lzero nat b tl0)) Hmemnp) ltpp) lepp)) X-clearme1) X-clearme0) (Hind b (cons lzero nat b tl0) Hc2 (refl lzero (list lzero nat) (cons lzero nat b tl0)) p Hc1)) Hmem) X-clearme) (checker-abl a b tl0 Hc0)) l Hl Hc) tl
bertrand-down : (n : nat) -> (X-- : lt O n) -> (X--1 : le n (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) -> bertrand n
bertrand-down = λ (n : nat) -> λ (posn : lt O n) -> λ (len : le n (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) -> match-ex lzero lzero nat (λ (it-v : nat) -> eq lzero nat it-v (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) lzero (λ (X-- : ex lzero lzero nat (λ (it-v : nat) -> eq lzero nat it-v (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))))) -> bertrand n) (λ (it-v : nat) -> λ (itdef : eq lzero nat it-v (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) -> match-And lzero lzero (And lzero lzero (all-primes (list-of-primes it-v)) (all-below (list-of-primes it-v) (plus it-v (S (S O))))) (primes-all (list-of-primes it-v) (plus it-v (S (S O)))) lzero (λ (X-- : And lzero lzero (And lzero lzero (all-primes (list-of-primes it-v)) (all-below (list-of-primes it-v) (plus it-v (S (S O))))) (primes-all (list-of-primes it-v) (plus it-v (S (S O))))) -> bertrand n) (λ (X-clearme : And lzero lzero (all-primes (list-of-primes it-v)) (all-below (list-of-primes it-v) (plus it-v (S (S O))))) -> match-And lzero lzero (all-primes (list-of-primes it-v)) (all-below (list-of-primes it-v) (plus it-v (S (S O)))) lzero (λ (X-- : And lzero lzero (all-primes (list-of-primes it-v)) (all-below (list-of-primes it-v) (plus it-v (S (S O))))) -> (X--1 : primes-all (list-of-primes it-v) (plus it-v (S (S O)))) -> bertrand n) (λ (Hall : all-primes (list-of-primes it-v)) -> λ (Hbelow : all-below (list-of-primes it-v) (plus it-v (S (S O)))) -> λ (Hcomplete : primes-all (list-of-primes it-v) (plus it-v (S (S O)))) -> primes-below-to-bertrand (S it-v) (list-of-primes it-v) (primeb-true-to-prime (S it-v) (eq-ind-r lzero lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) -> eq lzero bool (primeb (S x)) true) (refl lzero bool (primeb (S (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) it-v itdef)) (eq-ind-r lzero lzero nat (plus it-v O) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus it-v O)) -> primes-below (list-of-primes it-v) (S (S x))) (eq-ind-r lzero lzero nat (plus it-v (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus it-v (S O))) -> primes-below (list-of-primes it-v) (S x)) (eq-ind-r lzero lzero nat (plus it-v (S (S O))) (λ (x : nat) -> λ (X-- : eq lzero nat x (plus it-v (S (S O)))) -> primes-below (list-of-primes it-v) x) (primes-below-lop it-v) (S (plus it-v (S O))) (plus-n-Sm it-v (S O))) (S (plus it-v O)) (plus-n-Sm it-v O)) it-v (plus-n-O it-v)) (λ (p : nat) -> λ (memp : mem lzero nat p (list-of-primes it-v)) -> λ (lt2p : lt (S (S O)) p) -> checker-spec (tail lzero nat (list-of-primes it-v)) (S (S O)) (list-of-primes it-v) (eq-ind-r lzero lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) -> eq lzero bool (checker (list-of-primes x)) true) (refl lzero bool (checker (list-of-primes (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))) it-v itdef) (eq-ind-r lzero lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) -> eq lzero (list lzero nat) (list-of-primes x) (cons lzero nat (S (S O)) (tail lzero nat (list-of-primes x)))) (eq-lop (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (lt-O-S (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times O (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))))) it-v itdef) p (eq-ind-r lzero lzero (list lzero nat) (cons lzero nat (S (S O)) (tail lzero nat (list-of-primes it-v))) (λ (x : list lzero nat) -> λ (X-- : eq lzero (list lzero nat) x (cons lzero nat (S (S O)) (tail lzero nat (list-of-primes it-v)))) -> (X--1 : mem lzero nat p x) -> mem lzero nat p (tail lzero nat x)) (λ (X-clearme0 : mem lzero nat p (cons lzero nat (S (S O)) (tail lzero nat (list-of-primes it-v)))) -> match-Or lzero lzero (eq lzero nat p (S (S O))) (mem lzero nat p (tail lzero nat (list-of-primes it-v))) lzero (λ (X-- : Or lzero lzero (eq lzero nat p (S (S O))) (mem lzero nat p (tail lzero nat (list-of-primes it-v)))) -> mem lzero nat p (tail lzero nat (cons lzero nat (S (S O)) (tail lzero nat (list-of-primes it-v))))) (λ (eqp2 : eq lzero nat p (S (S O))) -> False-ind lzero lzero (λ (X-x-66 : False lzero) -> mem lzero nat p (tail lzero nat (cons lzero nat (S (S O)) (tail lzero nat (list-of-primes it-v))))) (absurd lzero (lt (S (S O)) p) lt2p (le-to-not-lt p (S (S O)) (eq-ind-r lzero lzero nat (S (S O)) (λ (x : nat) -> λ (X-- : eq lzero nat x (S (S O))) -> le x (S (S O))) (le-n (S (S O))) p eqp2)))) (λ (H : mem lzero nat p (tail lzero nat (list-of-primes it-v))) -> H) X-clearme0) (list-of-primes it-v) (eq-lop it-v (eq-ind-r lzero lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) -> le (S O) x) (lt-O-S (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times (plus (S O) (times O (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O)))) (S (S O))))) it-v itdef)) memp)) n posn (le-S-S n it-v (eq-ind-r lzero lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (λ (x : nat) -> λ (X-- : eq lzero nat x (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) -> le n x) len it-v itdef))) X-clearme) (primes-below-lop it-v)) (ex-intro lzero lzero nat (λ (it-v : nat) -> eq lzero nat it-v (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))) (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) (refl lzero nat (exp (S (S O)) (S (S (S (S (S (S (S (S O)))))))))))
bertrand' : (n : nat) -> (X-- : lt O n) -> bertrand n
bertrand' = λ (n : nat) -> λ (posn : lt O n) -> Or-ind lzero lzero lzero (le n (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Not lzero (le n (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (λ (X-x-170 : Or lzero lzero (le n (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Not lzero (le n (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -> bertrand n) (bertrand-down n posn) (λ (len : Not lzero (le n (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -> bertrand-up n (lt-to-le (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) n (not-le-to-lt n (exp (S (S O)) (S (S (S (S (S (S (S (S O))))))))) len))) (decidable-le n (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))