U32.and_low_step: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U32
Lines 232-243 of bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&start_line=232&end_line=243

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

def and_low_step(+m: Nat, +d: Nat, +xb: Bool, +xt: Word(m), +yb: Bool, +yt: Word(m), +hy: {Nat.add(S.bit_value(yb), Nat.double(S.unsigned(m, yt))) == Nat.sub(SC.pow2(d), 1n) : Nat}, +hx: {Nat.is_lt(Nat.add(S.bit_value(xb), Nat.double(S.unsigned(m, xt))), SC.pow2(d)) == True{} : Bool}, +ih: {Word.and(m, xt, yt) == xt : Word(m)}) -> {WCon{Bool.and(xb, yb), Word.and(m, xt, yt)} == WCon{xb, xt} : Word(1n+m)}:
  match d:
    case 0n:
      %Equal.sym(Word(m), Word.and(m, xt, yt), xt, ih) : {WCon{Bool.and(xb, yb), _} == WCon{xb, xt} : Word(1n+m)}
      %Equal.sym(Bool, yb, False{}, and_low_hyb(m, 0n, yb, yt, hy)) : {WCon{Bool.and(xb, _), xt} == WCon{xb, xt} : Word(1n+m)}
      %Equal.sym(Bool, xb, False{}, and_low_hxb(m, xb, xt, hx)) : {WCon{Bool.and(_, False{}), xt} == WCon{_, xt} : Word(1n+m)}
      {==}
    case 1n+k:
      %Equal.sym(Word(m), Word.and(m, xt, yt), xt, ih) : {WCon{Bool.and(xb, yb), _} == WCon{xb, xt} : Word(1n+m)}
      %Equal.sym(Bool, yb, True{}, and_low_hyb(m, 1n+k, yb, yt, hy)) : {WCon{Bool.and(xb, _), xt} == WCon{xb, xt} : Word(1n+m)}
      %Equal.sym(Bool, Bool.and(xb, True{}), xb, and_true(xb)) : {WCon{_, xt} == WCon{xb, xt} : Word(1n+m)}
      {==}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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.sub
  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.and
  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/lemmas/spec/numeric.bend&name=unsigned
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&name=and_low_hxb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&name=and_low_hyb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&name=and_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=pow2