Fixprime.found_go: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend as Fixprime
Lines 102-119 of bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend&start_line=102&end_line=119

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

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}:
  match fuel wr pr:
    case 0n _ _:
      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))
    case 1n+f True{} _:
      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))
    case 1n+f False{} True{}:
      +ep = L.some_inj(U32, m, p, h)
      +et = at_val(m, t, ht)
      +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)))
      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)
    case 1n+ +f False{} False{}:
      +m1 = U32.add(m, 1)
      +et = at_val(m, t, ht)
      +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))
      +ih = found_go(f, one, h1, m1, U32.is_zero(m1), {==}, NB.is_prime(v(m1)), {==}, 1n+t, ht1, p, h)
      +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))
      step_found(t, v(p), pt, ih)

Uses (29):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=none_some
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=some_inj
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=bo
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend&name=at_val
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend&name=here
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend&name=prime_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend&name=step_found
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend&name=succ_t
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend&name=no_prime
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/number.bend&name=prime
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/fixed.bend&name=u32_np
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/number.bend&name=is_prime