ProofFastFind2.FG2: def of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_fast_find2.bend as ProofFastFind2
Lines 31-39 of lawful-bytes@0.1.1.0/proof_fast_find2.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_find2.bend&start_line=31&end_line=39

import Base
import lawful-bytes@0.1.1.0/fast.bend as FA
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-arrays@0.1.0.0/proof_tree.bend as P

def FG2(n: Nat, z: Bool, +wi: U32, +m: U32, +r1: U32, +r2: U32, +t: P.Tree<U32>) -> U32:
  match n z:
    case 0n _:
      4294967295
    case 1n+k True{}:
      +m2 = (FA.zb((C.WD(t, (wi + 1 : U32)) .^. r1 : U32)) .|. FA.zb((C.WD(t, (wi + 1 : U32)) .^. r2 : U32)) : U32)
      FG2(k, U32.is_zero(m2), (wi + 1 : U32), m2, r1, r2, t)
    case 1n+k False{}:
      ((wi << 2n : U32) + FA.bidx(m) : U32)

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=Base/base.bend&name=U32.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/fast.bend&name=bidx
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/fast.bend&name=zb
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=WD