def none_go

bend-collections-laws-math@1.0.0.0 · proofs/math/number/fixprime.bend:177

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/number.bend as NB
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

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), {==})