PROOFBits.wb.or_bit: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_bits.bend as PROOFBits
Lines 193-196 of bend-osdev-word64@0.1.1.0/PROOF_bits.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&start_line=193&end_line=196

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/word64.bend as W

def wb.or_bit(+x: W.W64, +c: U32, +hc: {Nat.is_lt(U32.to_nat(c), U.U32Nat.dbl(1n, 1n)) == True{} : Bool}) -> {W.W64.to_nat(W.W64.or(W.W64.shl(x, 1n), W.W64.from_u32(c))) == Nat.add(W.W64.to_nat(W.W64.shl(x, 1n)), U32.to_nat(c)) : Nat}:
  match x:
    case W.W64{+h, +l}:
      Equal.trans(Nat, Nat.add(U32.to_nat(U32.or(U32.shln(l, 1n), c)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U32.to_nat(c)), Equal.trans(Nat, Nat.add(U32.to_nat(U32.or(U32.shln(l, 1n), c)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n))), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), U32.to_nat(U32.or(U32.shln(l, 1n), c)), Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), UL.u32_or_split(U32.shln(l, 1n), c, 1n, U.U32Nat.low(31n, U32.to_nat(l)), Equal.trans(Nat, U32.to_nat(U32.shln(l, 1n)), Nat.double(U.U32Nat.low(31n, U32.to_nat(l))), U.U32Nat.dbl(1n, U.U32Nat.low(31n, U32.to_nat(l))), Equal.trans(Nat, U32.to_nat(U32.shln(l, 1n)), U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), Nat.double(U.U32Nat.low(31n, U32.to_nat(l))), Equal.trans(Nat, U32.to_nat(U32.shln(l, 1n)), U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(l))), U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), UL.u32_shln_low(l, 1n), {==}), UL.low_double(31n, U32.to_nat(l))), {==}), hc)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, zz)), U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)), Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n), Equal.trans(Nat, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)), Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), U32.to_nat(0)), Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n), UL.u32_or_split(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0, 0n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), {==}, {==}), {==}))), wr.b5(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c), U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)))))

Uses (23):
  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=U32
  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.shrn
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=low_double
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_or_split
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_shln_low
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.low
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wr.b5
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.from_u32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.or
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.shl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.to_nat