PROOF.ud.step2: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 1770-1772 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=1770&end_line=1772

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

def ud.step2(+p: Nat, +a0: Bool, +bw: Word(32n), +q: Word(p), +rw: Word(32n), +x: Nat, +x2: Nat, +ex: {Nat.add(U.U32Nat.bit(a0), Nat.double(x)) == x2 : Nat}, +i1: {Nat.add(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)), Word.to_nat(32n, rw)) == x : Nat}, +i2: {Nat.is_lt(Word.to_nat(32n, rw), Word.to_nat(32n, bw)) == True{} : Bool}) -> {Nat.add(Nat.mul(ud.q(1n+p, U32.divmod.go.shl(p, q, U32{bw}, Word.shl.out(32n, a0, rw))), U32.to_nat(U32{bw})), ud.r(1n+p, U32.divmod.go.shl(p, q, U32{bw}, Word.shl.out(32n, a0, rw)))) == x2 : Nat} & {Nat.is_lt(ud.r(1n+p, U32.divmod.go.shl(p, q, U32{bw}, Word.shl.out(32n, a0, rw))), U32.to_nat(U32{bw})) == True{} : Bool}:
  %Equal.sym(Bool & Word(32n), Word.shl.out(32n, a0, rw), (un.topc(32n, a0, rw), Word.shl.put(32n, a0, rw)), un.so(32n, a0, rw)) : {Nat.add(Nat.mul(ud.q(1n+p, U32.divmod.go.shl(p, q, U32{bw}, _)), U32.to_nat(U32{bw})), ud.r(1n+p, U32.divmod.go.shl(p, q, U32{bw}, _))) == x2 : Nat} & {Nat.is_lt(ud.r(1n+p, U32.divmod.go.shl(p, q, U32{bw}, _)), U32.to_nat(U32{bw})) == True{} : Bool}
  ud.fin(p, q, Word.shl.put(32n, a0, rw), bw, un.topc(32n, a0, rw), Bool.or(un.topc(32n, a0, rw), U32.is_ge(U32{Word.shl.put(32n, a0, rw)}, U32{bw})), a0, rw, x, x2, {==}, un.putv(32n, a0, rw), ex, i1, i2)

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.divmod.go.shl
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_ge
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shl.out
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shl.put
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ud.fin
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ud.q
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ud.r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.putv
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.so
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.topc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.bit