def found_go

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

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/fixed.bend as SF
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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

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)