1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/fixed.bend as SF 4 import ../../../spec/math/number.bend as SN 5 import ../../../src/math/fixed.bend as F 6 import ../../../src/math/number.bend as NB 7 import ../../lib/nat.bend as N 8 import ../../lib/logic.bend as L 9 import ../../lib/word.bend as WD 10 import ./prime.bend as PR 11 import ../typed/width.bend as WW 12 import ../typed/w64add.bend as WA 13 import ../typed/w64mul.bend as W64M 14 import ../typed/u32laws.bend as LW 15 import ../u64/u64.bend as P64 16 import ../../lib/u32alg.bend as UA 17 import ../../lib/u32.bend as U3 18 19 # is_prime and next_prime at U32 (spec/math/fixed.bend): is_prime is the 20 # proved trial division of proofs/math/number/prime.bend on the value; 21 # next_prime tries n + 1, n + 2, ... as U32s. A candidate is tracked by its 22 # position t == value + 2^32 [wrapped] (the successor of 2^32 - 1 wraps to 23 # 0 at position 2^32), so the loop's None means no prime in [n + 1, 2^32) 24 # and its Some p the least prime there (Mathlib Nat.find / Nat.exists_infinite_primes 25 # stated on the bounded range). 2^32 stays C.shift(32, one): never unfolded. 26 27 def v(+x: U32) -> Nat: 28 U32.to_nat(x) 29 30 def is_prime(+a: U32) -> SF.IsPrime.value(a): 31 PR.is_prime_value(v(a)) 32 33 # ---- the successor's position ---- 34 35 def 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 47 def 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 # the position of m + 1 is 1 + the value of m 57 def 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 68 def 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 # an unwrapped candidate sits at its value 77 def 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 80 def 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 # ---- found: a prime, none before it ---- 84 85 def 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 91 def 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 102 def 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 # is_lt(a, b) is is_le(a + 1, b) 122 def 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 129 def 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 136 def 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 139 def 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 143 def 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 # ---- none: no prime left below 2^32 ---- 149 150 # UA.not_value with the unit kept open (n is 32 at the use) 151 def 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 154 def 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 # 2^32 stays C.shift(32, one) for a symbolic one: with one == 1n the checker 170 # would expand the closed 2^32 in unary 171 def 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 174 def 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 177 def 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 201 def 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 205 def 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)