W64sh.or1: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as W64sh
Lines 285-295 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&start_line=285&end_line=295

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

# setting bit 0: 1 + 2 half(x)
def or1(+x: U32) -> {v(U32.or(x, 1)) == 1n+Nat.double(C.half(v(x))) : Nat}:
  match x:
    case U32{+w}:
      match w:
        case WCon{+b, +t}:
          +e1 = Equal.cong(Word(31n), Nat, z => v(U32{WCon{True{}, z}}), Word.or(31n, t, WD.mask(31n, 0n)), t, or_zero(31n, t))
          +ev = Equal.trans(Nat, v(U32{WCon{b, t}}), WD.uw(32n, WCon{b, t}), Nat.add(S.bit_value(b), Nat.double(WD.uw(31n, t))), UD.vw(WCon{b, t}), {==})
          +eh = Equal.trans(Nat, C.half(v(U32{WCon{b, t}})), C.half(Nat.add(S.bit_value(b), Nat.double(WD.uw(31n, t)))), WD.uw(31n, t), Equal.cong(Nat, Nat, z => C.half(z), v(U32{WCon{b, t}}), Nat.add(S.bit_value(b), Nat.double(WD.uw(31n, t))), ev), half_bv(b, WD.uw(31n, t)))
          +e0 = Equal.cong(Bool, Nat, z => v(U32{WCon{z, Word.or(31n, t, WD.mask(31n, 0n))}}), Bool.or(b, True{}), True{}, or_t(b))
          Equal.trans(Nat, v(U32{WCon{Bool.or(b, True{}), Word.or(31n, t, WD.mask(31n, 0n))}}), v(U32{WCon{True{}, Word.or(31n, t, WD.mask(31n, 0n))}}), 1n+Nat.double(C.half(v(U32{WCon{b, t}}))), e0, Equal.trans(Nat, v(U32{WCon{True{}, Word.or(31n, t, WD.mask(31n, 0n))}}), v(U32{WCon{True{}, t}}), 1n+Nat.double(C.half(v(U32{WCon{b, t}}))), e1, Equal.trans(Nat, v(U32{WCon{True{}, t}}), 1n+Nat.double(WD.uw(31n, t)), 1n+Nat.double(C.half(v(U32{WCon{b, t}}))), UD.vw(WCon{True{}, t}), Equal.cong(Nat, Nat, z => 1n+Nat.double(z), WD.uw(31n, t), C.half(v(U32{WCon{b, t}})), Equal.sym(Nat, C.half(v(U32{WCon{b, t}})), WD.uw(31n, t), eh)))))

Uses (22):
  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.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.or
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&name=vw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=mask
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=uw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=half_bv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=or_t
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=or_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=half