proofs/math/number/fixprime.bend
bend-collections-laws-math@1.0.0.0 · 206 lines · 23 definitions
1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
4import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
5import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
6import bend-collections-laws-math@1.0.0.0/src/math/number.bend as NB
7import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
10import bend-collections-laws-math@1.0.0.0/proofs/math/number/prime.bend as PR
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
15import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64
16import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as UA
17import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U3
18
19
20
21
22
23
24
25
26
27def v(+x: U32) -> Nat:
28 U32.to_nat(x)
29
30def is_prime(+a: U32) -> SF.IsPrime.value(a):
31 PR.is_prime_value(v(a))
32
33
34
35def zc_t(+one: Nat, +h1: {one == 1n : Nat}, +r: Nat, +x: Nat, +e: {Nat.add(r, C.shift(32n, one)) == Nat.add(x, 1n) : Nat}, +hx: {C.fits(32n, x) == True{} : Bool}) -> {SF.bn(Nat.is_eq(r, 0n)) == one : Nat}:
36 match r:
37 case 0n:
38 Equal.sym(Nat, one, 1n, h1)
39 case 1n+ +rp:
40 +S = C.shift(32n, one)
41 +e1 = Equal.trans(Nat, 1n+Nat.add(rp, S), Nat.add(x, 1n), 1n+x, e, N.add_comm(x, 1n))
42 +e2 = N.succ_inj(Nat.add(rp, S), x, e1)
43 +hl = Equal.trans(Bool, Nat.is_lt(Nat.add(rp, S), S), Nat.is_lt(x, S), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, S), Nat.add(rp, S), x, e2), WW.lt_one(32n, one, h1, x, hx))
44 +hg = Equal.trans(Bool, Nat.is_le(S, Nat.add(rp, S)), Nat.is_le(S, Nat.add(S, rp)), True{}, Equal.cong(Nat, Bool, t => Nat.is_le(S, t), Nat.add(rp, S), Nat.add(S, rp), N.add_comm(rp, S)), N.le_add_right(S, rp))
45 Empty.absurd({SF.bn(Nat.is_eq(1n+rp, 0n)) == one : Nat}, L.true_false(Equal.trans(Bool, True{}, Nat.is_le(S, Nat.add(rp, S)), False{}, Equal.sym(Bool, Nat.is_le(S, Nat.add(rp, S)), True{}, hg), N.lt_not_le(Nat.add(rp, S), S, hl))))
46
47def zc(+one: Nat, +h1: {one == 1n : Nat}, +r: Nat, +x: Nat, +c: Bool, +e: {Nat.add(r, C.shift(32n, WD.bo(c, one))) == Nat.add(x, 1n) : Nat}, +hx: {C.fits(32n, x) == True{} : Bool}) -> {SF.bn(Nat.is_eq(r, 0n)) == WD.bo(c, one) : Nat}:
48 match c:
49 case True{}:
50 zc_t(one, h1, r, x, e, hx)
51 case False{}:
52 +er = Equal.trans(Nat, r, Nat.add(r, 0n), 1n+x, Equal.sym(Nat, Nat.add(r, 0n), r, N.add_zero(r)), Equal.trans(Nat, Nat.add(r, 0n), Nat.add(x, 1n), 1n+x, e, N.add_comm(x, 1n)))
53 %Equal.sym(Nat, r, 1n+x, er) : {SF.bn(Nat.is_eq(_, 0n)) == 0n : Nat}
54 {==}
55
56
57def bn_bo(+b: Bool, +c: Bool, +one: Nat, +h1: {one == 1n : Nat}, +e: {SF.bn(b) == WD.bo(c, one) : Nat}) -> {WD.bo(b, one) == WD.bo(c, one) : Nat}:
58 match b c:
59 case True{} True{}:
60 {==}
61 case False{} False{}:
62 {==}
63 case True{} False{}:
64 Empty.absurd({one == 0n : Nat}, N.succ_zero(0n, e))
65 case False{} True{}:
66 Empty.absurd({0n == one : Nat}, N.zero_succ(0n, Equal.trans(Nat, 0n, one, 1n, e, h1)))
67
68def succ_t(+one: Nat, +h1: {one == 1n : Nat}, +m: U32) -> {Nat.add(v(U32.add(m, 1)), C.shift(32n, WD.bo(U32.is_zero(U32.add(m, 1)), one))) == 1n+v(m) : Nat}:
69 +m1 = U32.add(m, 1)
70 +c = P64.carry32(m, 1)
71 +e0 = WA.acons_o(one, h1, m, 1)
72 +z = zc(one, h1, v(m1), v(m), c, e0, LW.vb(m))
73 +ez = bn_bo(U32.is_zero(m1), c, one, h1, Equal.trans(Nat, SF.bn(U32.is_zero(m1)), SF.bn(Nat.is_eq(v(m1), 0n)), WD.bo(c, one), Equal.cong(Bool, Nat, t => SF.bn(t), U32.is_zero(m1), Nat.is_eq(v(m1), 0n), LW.zero_nat(m1)), z))
74 Equal.trans(Nat, Nat.add(v(m1), C.shift(32n, WD.bo(U32.is_zero(m1), one))), Nat.add(v(m1), C.shift(32n, WD.bo(c, one))), 1n+v(m), Equal.cong(Nat, Nat, t => Nat.add(v(m1), C.shift(32n, t)), WD.bo(U32.is_zero(m1), one), WD.bo(c, one), ez), Equal.trans(Nat, Nat.add(v(m1), C.shift(32n, WD.bo(c, one))), Nat.add(v(m), 1n), 1n+v(m), e0, N.add_comm(v(m), 1n)))
75
76
77def at_val(+m: U32, +t: Nat, +ht: {Nat.add(v(m), C.shift(32n, 0n)) == t : Nat}) -> {v(m) == t : Nat}:
78 Equal.trans(Nat, v(m), Nat.add(v(m), 0n), t, Equal.sym(Nat, Nat.add(v(m), 0n), v(m), N.add_zero(v(m))), ht)
79
80def prime_of(+m: U32, +pr: Bool, +hpr: {NB.is_prime(v(m)) == pr : Bool}) -> {SN.prime(v(m)) == pr : Bool}:
81 Equal.trans(Bool, SN.prime(v(m)), NB.is_prime(v(m)), pr, Equal.sym(Bool, NB.is_prime(v(m)), SN.prime(v(m)), PR.is_prime_value(v(m))), hpr)
82
83
84
85def here(+n: Nat, +hp: {SN.prime(n) == True{} : Bool}) -> {Bool.and(Bool.and(Nat.is_le(n, n), SN.prime(n)), SF.no_prime(Nat.sub(n, n), n)) == True{} : Bool}:
86 %Equal.sym(Nat, Nat.sub(n, n), 0n, N.sub_self(n)) : {Bool.and(Bool.and(Nat.is_le(n, n), SN.prime(n)), SF.no_prime(_, n)) == True{} : Bool}
87 %Equal.sym(Bool, Nat.is_le(n, n), True{}, N.le_refl(n)) : {Bool.and(Bool.and(_, SN.prime(n)), True{}) == True{} : Bool}
88 %Equal.sym(Bool, SN.prime(n), True{}, hp) : {Bool.and(Bool.and(True{}, _), True{}) == True{} : Bool}
89 {==}
90
91def step_found(+t: Nat, +q: Nat, +pt: {SN.prime(t) == False{} : Bool}, +ih: {Bool.and(Bool.and(Nat.is_le(1n+t, q), SN.prime(q)), SF.no_prime(Nat.sub(q, 1n+t), 1n+t)) == True{} : Bool}) -> {Bool.and(Bool.and(Nat.is_le(t, q), SN.prime(q)), SF.no_prime(Nat.sub(q, t), t)) == True{} : Bool}:
92 +a12 = L.and_left(Bool.and(Nat.is_le(1n+t, q), SN.prime(q)), SF.no_prime(Nat.sub(q, 1n+t), 1n+t), ih)
93 +a1 = L.and_left(Nat.is_le(1n+t, q), SN.prime(q), a12)
94 +a2 = L.and_right(Nat.is_le(1n+t, q), SN.prime(q), a12)
95 +a3 = L.and_right(Bool.and(Nat.is_le(1n+t, q), SN.prime(q)), SF.no_prime(Nat.sub(q, 1n+t), 1n+t), ih)
96 +le = N.le_trans(t, 1n+t, q, N.le_succ(t), a1)
97 +es = PR.sub_split(q, t, N.succ_le_lt(t, q, a1))
98 %Equal.sym(Nat, Nat.sub(q, t), 1n+Nat.sub(q, 1n+t), es) : {Bool.and(Bool.and(Nat.is_le(t, q), SN.prime(q)), SF.no_prime(_, t)) == True{} : Bool}
99 %Equal.sym(Bool, SN.prime(t), False{}, pt) : {Bool.and(Bool.and(Nat.is_le(t, q), SN.prime(q)), Bool.and(Bool.not(_), SF.no_prime(Nat.sub(q, 1n+t), 1n+t))) == True{} : Bool}
100 L.and_intro(Bool.and(Nat.is_le(t, q), SN.prime(q)), Bool.and(True{}, SF.no_prime(Nat.sub(q, 1n+t), 1n+t)), L.and_intro(Nat.is_le(t, q), SN.prime(q), le, a2), a3)
101
102def found_go(fuel: Nat, +one: Nat, +h1: {one == 1n : Nat}, +m: U32, +wr: Bool, +hwr: {U32.is_zero(m) == wr : Bool}, +pr: Bool, +hpr: {NB.is_prime(v(m)) == pr : Bool}, +t: Nat, +ht: {Nat.add(v(m), C.shift(32n, WD.bo(wr, one))) == t : Nat}, +p: U32, +h: {F.u32_np(fuel, m, wr, pr) == Some{p} : Maybe<&2, U32>}) -> {Bool.and(Bool.and(Nat.is_le(t, v(p)), SN.prime(v(p))), SF.no_prime(Nat.sub(v(p), t), t)) == True{} : Bool}:
103 match fuel wr pr:
104 case 0n _ _:
105 Empty.absurd({Bool.and(Bool.and(Nat.is_le(t, v(p)), SN.prime(v(p))), SF.no_prime(Nat.sub(v(p), t), t)) == True{} : Bool}, L.none_some(U32, p, h))
106 case 1n+f True{} _:
107 Empty.absurd({Bool.and(Bool.and(Nat.is_le(t, v(p)), SN.prime(v(p))), SF.no_prime(Nat.sub(v(p), t), t)) == True{} : Bool}, L.none_some(U32, p, h))
108 case 1n+f False{} True{}:
109 +ep = L.some_inj(U32, m, p, h)
110 +et = at_val(m, t, ht)
111 +hm = L.subst(Nat, q => {Bool.and(Bool.and(Nat.is_le(q, v(m)), SN.prime(v(m))), SF.no_prime(Nat.sub(v(m), q), q)) == True{} : Bool}, v(m), t, et, here(v(m), prime_of(m, True{}, hpr)))
112 L.subst(U32, z => {Bool.and(Bool.and(Nat.is_le(t, v(z)), SN.prime(v(z))), SF.no_prime(Nat.sub(v(z), t), t)) == True{} : Bool}, m, p, ep, hm)
113 case 1n+ +f False{} False{}:
114 +m1 = U32.add(m, 1)
115 +et = at_val(m, t, ht)
116 +ht1 = Equal.trans(Nat, Nat.add(v(m1), C.shift(32n, WD.bo(U32.is_zero(m1), one))), 1n+v(m), 1n+t, succ_t(one, h1, m), Equal.cong(Nat, Nat, z => 1n+z, v(m), t, et))
117 +ih = found_go(f, one, h1, m1, U32.is_zero(m1), {==}, NB.is_prime(v(m1)), {==}, 1n+t, ht1, p, h)
118 +pt = Equal.trans(Bool, SN.prime(t), SN.prime(v(m)), False{}, Equal.cong(Nat, Bool, z => SN.prime(z), t, v(m), Equal.sym(Nat, v(m), t, et)), prime_of(m, False{}, hpr))
119 step_found(t, v(p), pt, ih)
120
121
122def le_c(+a: Nat, +b: Nat, +d: Bool, +hd: {Nat.is_le(1n+a, b) == d : Bool}, +hc: {Nat.is_lt(a, b) == False{} : Bool}) -> {False{} == d : Bool}:
123 match d:
124 case False{}:
125 {==}
126 case True{}:
127 Empty.absurd({False{} == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_lt(a, b), False{}, Equal.sym(Bool, Nat.is_lt(a, b), True{}, N.succ_le_lt(a, b, hd)), hc)))
128
129def lt_iff_c(+a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {c == Nat.is_le(1n+a, b) : Bool}:
130 match c:
131 case True{}:
132 Equal.sym(Bool, Nat.is_le(1n+a, b), True{}, N.lt_succ_le_succ(a, b, hc))
133 case False{}:
134 le_c(a, b, Nat.is_le(1n+a, b), {==}, hc)
135
136def lt_iff(+a: Nat, +b: Nat) -> {Nat.is_lt(a, b) == Nat.is_le(1n+a, b) : Bool}:
137 lt_iff_c(a, b, Nat.is_lt(a, b), {==})
138
139def found_one(+one: Nat, +h1: {one == 1n : Nat}, +n: U32, +p: U32, +h: {F.u32_next_prime(n) == Some{p} : Maybe<&2, U32>}) -> {Bool.and(Bool.and(Nat.is_le(1n+v(n), v(p)), SN.prime(v(p))), SF.no_prime(Nat.sub(v(p), 1n+v(n)), 1n+v(n))) == True{} : Bool}:
140 +m1 = U32.add(n, 1)
141 found_go(Nat.add(v(U32.not(n)), 1n), one, h1, m1, U32.is_zero(m1), {==}, NB.is_prime(v(m1)), {==}, 1n+v(n), succ_t(one, h1, n), p, h)
142
143def found(+n: U32, +p: U32, +h: {F.u32_next_prime(n) == Some{p} : Maybe<&2, U32>}) -> SF.NextPrime.found(n, p, h):
144 +g = found_one(1n, {==}, n, p, h)
145 %Equal.sym(Bool, Nat.is_lt(v(n), v(p)), Nat.is_le(1n+v(n), v(p)), lt_iff(v(n), v(p))) : {Bool.and(Bool.and(_, SN.prime(v(p))), SF.no_prime(Nat.sub(v(p), 1n+v(n)), 1n+v(n))) == True{} : Bool}
146 g
147
148
149
150
151def not_value_one(+n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +b: Word(n)) -> {Nat.add(1n, Nat.add(UA.uw(n, Word.not(n, b)), UA.uw(n, b))) == UA.sc(n, one) : Nat}:
152 Equal.trans(Nat, Nat.add(1n, Nat.add(UA.uw(n, Word.not(n, b)), UA.uw(n, b))), UA.sc(n, 1n), UA.sc(n, one), UA.not_value(n, b), Equal.cong(Nat, Nat, z => UA.sc(n, z), 1n, one, Equal.sym(Nat, one, 1n, h1)))
153
154def fuel_ok(+one: Nat, +h1: {one == 1n : Nat}, +n: U32) -> {Nat.is_le(C.shift(32n, one), Nat.add(1n+v(n), 1n+v(U32.not(n)))) == True{} : Bool}:
155 match n:
156 case U32{+w}:
157 +A = UA.uw(32n, Word.not(32n, w))
158 +B = UA.uw(32n, w)
159 +S = C.shift(32n, one)
160 +e1 = Equal.trans(Nat, S, WD.sc(32n, one), UA.sc(32n, one), W64M.shift_sc(32n, one), {==})
161 +eS = Equal.trans(Nat, S, UA.sc(32n, one), Nat.add(1n, Nat.add(A, B)), e1, Equal.sym(Nat, Nat.add(1n, Nat.add(A, B)), UA.sc(32n, one), not_value_one(32n, one, h1, w)))
162 +eR = Equal.trans(Nat, Nat.add(1n+B, 1n+A), 1n+Nat.add(B, 1n+A), 2n+Nat.add(A, B), {==}, Equal.cong(Nat, Nat, z => 1n+z, Nat.add(B, 1n+A), 1n+Nat.add(A, B), Equal.trans(Nat, Nat.add(B, 1n+A), 1n+Nat.add(B, A), 1n+Nat.add(A, B), N.add_succ(B, A), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(B, A), Nat.add(A, B), N.add_comm(B, A)))))
163 %Equal.sym(Nat, U32.to_nat(U32{w}), B, U3.to_nat_word(w)) : {Nat.is_le(S, Nat.add(1n+_, 1n+U32.to_nat(U32{Word.not(32n, w)}))) == True{} : Bool}
164 %Equal.sym(Nat, U32.to_nat(U32{Word.not(32n, w)}), A, U3.to_nat_word(Word.not(32n, w))) : {Nat.is_le(S, Nat.add(1n+B, 1n+_)) == True{} : Bool}
165 %Equal.sym(Nat, S, Nat.add(1n, Nat.add(A, B)), eS) : {Nat.is_le(_, Nat.add(1n+B, 1n+A)) == True{} : Bool}
166 %Equal.sym(Nat, Nat.add(1n+B, 1n+A), 2n+Nat.add(A, B), eR) : {Nat.is_le(Nat.add(1n, Nat.add(A, B)), _) == True{} : Bool}
167 N.le_succ(1n+Nat.add(A, B))
168
169
170
171def fuel_ok2(+one: Nat, +h1: {one == 1n : Nat}, +n: U32) -> {Nat.is_le(C.shift(32n, one), Nat.add(1n+v(n), Nat.add(v(U32.not(n)), 1n))) == True{} : Bool}:
172 L.subst(Nat, z => {Nat.is_le(C.shift(32n, one), Nat.add(1n+v(n), z)) == True{} : Bool}, 1n+v(U32.not(n)), Nat.add(v(U32.not(n)), 1n), Equal.sym(Nat, Nat.add(v(U32.not(n)), 1n), 1n+v(U32.not(n)), WA.plus1(v(U32.not(n)))), fuel_ok(one, h1, n))
173
174def beyond(+one: Nat, +h1: {one == 1n : Nat}, +t: Nat, +q: Nat, +hS: {Nat.is_le(C.shift(32n, one), t) == True{} : Bool}, +hq: {Nat.is_le(t, q) == True{} : Bool}, +hqf: {C.fits(32n, q) == True{} : Bool}) -> Empty:
175 L.true_false(Equal.trans(Bool, True{}, Nat.is_le(C.shift(32n, one), q), False{}, Equal.sym(Bool, Nat.is_le(C.shift(32n, one), q), True{}, N.le_trans(C.shift(32n, one), t, q, hS, hq)), N.lt_not_le(q, C.shift(32n, one), WW.lt_one(32n, one, h1, q, hqf))))
176
177def none_go(fuel: Nat, +one: Nat, +h1: {one == 1n : Nat}, +m: U32, +wr: Bool, +hwr: {U32.is_zero(m) == wr : Bool}, +pr: Bool, +hpr: {NB.is_prime(v(m)) == pr : Bool}, +t: Nat, +ht: {Nat.add(v(m), C.shift(32n, WD.bo(wr, one))) == t : Nat}, +hf: {Nat.is_le(C.shift(32n, one), Nat.add(t, fuel)) == True{} : Bool}, +h: {F.u32_np(fuel, m, wr, pr) == None{} : Maybe<&2, U32>}, +q: Nat, +hq: {Nat.is_le(t, q) == True{} : Bool}, +hqf: {C.fits(32n, q) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(t, q) == c : Bool}) -> {SN.prime(q) == False{} : Bool}:
178 match fuel wr pr c:
179 case 0n _ _ _:
180 +hS = Equal.trans(Bool, Nat.is_le(C.shift(32n, one), t), Nat.is_le(C.shift(32n, one), Nat.add(t, 0n)), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(C.shift(32n, one), z), t, Nat.add(t, 0n), Equal.sym(Nat, Nat.add(t, 0n), t, N.add_zero(t))), hf)
181 Empty.absurd({SN.prime(q) == False{} : Bool}, beyond(one, h1, t, q, hS, hq, hqf))
182 case 1n+f True{} _ _:
183 +S = C.shift(32n, one)
184 +e1 = ht
185 +hS = Equal.trans(Bool, Nat.is_le(S, t), Nat.is_le(S, Nat.add(S, v(m))), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(S, z), t, Nat.add(S, v(m)), Equal.trans(Nat, t, Nat.add(v(m), S), Nat.add(S, v(m)), Equal.sym(Nat, Nat.add(v(m), S), t, e1), N.add_comm(v(m), S))), N.le_add_right(S, v(m)))
186 Empty.absurd({SN.prime(q) == False{} : Bool}, beyond(one, h1, t, q, hS, hq, hqf))
187 case 1n+f False{} True{} _:
188 Empty.absurd({SN.prime(q) == False{} : Bool}, L.none_some(U32, m, Equal.sym(Maybe<&2, U32>, Some{m}, None{}, h)))
189 case 1n+f False{} False{} True{}:
190 +et = at_val(m, t, ht)
191 +eq = N.eq_from_is_eq(t, q, hc)
192 Equal.trans(Bool, SN.prime(q), SN.prime(v(m)), False{}, Equal.cong(Nat, Bool, z => SN.prime(z), q, v(m), Equal.sym(Nat, v(m), q, Equal.trans(Nat, v(m), t, q, et, eq))), prime_of(m, False{}, hpr))
193 case 1n+ +f False{} False{} False{}:
194 +et = at_val(m, t, ht)
195 +m1 = U32.add(m, 1)
196 +ht1 = Equal.trans(Nat, Nat.add(v(m1), C.shift(32n, WD.bo(U32.is_zero(m1), one))), 1n+v(m), 1n+t, succ_t(one, h1, m), Equal.cong(Nat, Nat, z => 1n+z, v(m), t, et))
197 +hf1 = Equal.trans(Bool, Nat.is_le(C.shift(32n, one), Nat.add(1n+t, f)), Nat.is_le(C.shift(32n, one), Nat.add(t, 1n+f)), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(C.shift(32n, one), z), Nat.add(1n+t, f), Nat.add(t, 1n+f), Equal.sym(Nat, Nat.add(t, 1n+f), 1n+Nat.add(t, f), N.add_succ(t, f))), hf)
198 +hq1 = N.lt_succ_le_succ(t, q, N.lt_or_eq(t, q, hq, hc))
199 none_go(f, one, h1, m1, U32.is_zero(m1), {==}, NB.is_prime(v(m1)), {==}, 1n+t, ht1, hf1, h, q, hq1, hqf, Nat.is_eq(1n+t, q), {==})
200
201def none_one(+one: Nat, +h1: {one == 1n : Nat}, +n: U32, +h: {F.u32_next_prime(n) == None{} : Maybe<&2, U32>}, +m: Nat, +hm: {Nat.is_lt(v(n), m) == True{} : Bool}, +hf: {C.fits(32n, m) == True{} : Bool}) -> {SN.prime(m) == False{} : Bool}:
202 +m1 = U32.add(n, 1)
203 none_go(Nat.add(v(U32.not(n)), 1n), one, h1, m1, U32.is_zero(m1), {==}, NB.is_prime(v(m1)), {==}, 1n+v(n), succ_t(one, h1, n), fuel_ok2(one, h1, n), h, m, N.lt_succ_le_succ(v(n), m, hm), hf, Nat.is_eq(1n+v(n), m), {==})
204
205def none(+n: U32, +h: {F.u32_next_prime(n) == None{} : Maybe<&2, U32>}, +m: Nat, +hm: {Nat.is_lt(v(n), m) == True{} : Bool}, +hf: {C.fits(32n, m) == True{} : Bool}) -> SF.NextPrime.none(n, h, m, hm, hf):
206 none_one(1n, {==}, n, h, m, hm, hf)