PROOF.ud.fin.t: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 1755-1757 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=1755&end_line=1757

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

def ud.fin.t(+p: Nat, +q: Word(p), +bw: Word(32n), +a0: Bool, +rw: Word(32n), +x: Nat, +x2: Nat, +R1: 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}, kp: {Nat.add(R1, Nat.mul(U.U32Nat.bit(True{}), Word.to_nat(32n, bw))) == Nat.add(U.U32Nat.bit(a0), Nat.double(Word.to_nat(32n, rw))) : Nat} & {Nat.is_lt(R1, Word.to_nat(32n, bw)) == True{} : Bool}) -> {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), Word.to_nat(32n, bw)), R1) == x2 : Nat} & {Nat.is_lt(R1, Word.to_nat(32n, bw)) == True{} : Bool}:
  (+k1, +k2) = kp
  (Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), Word.to_nat(32n, bw)), R1), Nat.add(U.U32Nat.bit(a0), Nat.double(x)), x2, Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), Word.to_nat(32n, bw)), R1), Nat.add(U.U32Nat.bit(a0), Nat.double(Nat.add(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)), Word.to_nat(32n, rw)))), Nat.add(U.U32Nat.bit(a0), Nat.double(x)), Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), Word.to_nat(32n, bw)), R1), Nat.add(Nat.add(U.U32Nat.bit(a0), Nat.double(Word.to_nat(32n, rw))), Nat.double(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)))), Nat.add(U.U32Nat.bit(a0), Nat.double(Nat.add(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)), Word.to_nat(32n, rw)))), Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), Word.to_nat(32n, bw)), R1), Nat.add(Nat.add(R1, Nat.mul(1n, Word.to_nat(32n, bw))), Nat.double(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)))), Nat.add(Nat.add(U.U32Nat.bit(a0), Nat.double(Word.to_nat(32n, rw))), Nat.double(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)))), ur.r35(Word.to_nat(p, q), Word.to_nat(32n, bw), R1), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.double(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)))), Nat.add(R1, Nat.mul(1n, Word.to_nat(32n, bw))), Nat.add(U.U32Nat.bit(a0), Nat.double(Word.to_nat(32n, rw))), k1)), ur.r36(U.U32Nat.bit(a0), Word.to_nat(32n, rw), Word.to_nat(p, q), Word.to_nat(32n, bw))), Equal.cong(Nat, Nat, zz => Nat.add(U.U32Nat.bit(a0), Nat.double(zz)), Nat.add(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)), Word.to_nat(32n, rw)), x, i1)), ex), k2)

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.trans
  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=Word
  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=ur.r35
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r36
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.bit