ProofValue.wv.bitw_value: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/proof_value.bend as ProofValue
Lines 284-289 of bend-osdev-word64@0.1.1.0/proof_value.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&start_line=284&end_line=289

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

def wv.bitw_value(+p: Nat, b: Bool) -> {Word.to_nat(1n+p, wv.bitw(1n+p, b)) == U.U32Nat.bit(b) : Nat}:
  match b:
    case True{}:
      wn.succ_cong(Nat.double(Word.to_nat(p, Word.zero(p))), 0n, Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.zero(p)), 0n, UL.word_zero_value(p)))
    case False{}:
      Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.zero(p)), 0n, UL.word_zero_value(p))

Uses (10):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_zero_value
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.bit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.succ_cong
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wv.bitw