U32.internal_shl_con: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/u32.bend as U32
Lines 780-789 of bend-mathlib@0.8.1.0/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/u32.bend&start_line=780&end_line=789

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

def internal_shl_con(+p: Nat, +c: Bool, r: Bool & Word(p), -x: Nat, ih: {internal_shl_val(p, Nat.pow(2n, p), r) == x : Nat}) -> {internal_shl_val(1n+p, Nat.pow(2n, 1n+p), Word.shl.out.con(p, c, r)) == Nat.add(internal_bv(c), Nat.double(x)) : Nat}:
  match r:
    case (+hi, +t2):
      +u = Word.to_nat(p, t2)
      +v = Bool.pick(Nat, hi, Nat.pow(2n, p), 0n)
      %ih : {Nat.add(Word.to_nat(1n+p, WCon{c, t2}), Bool.pick(Nat, hi, Nat.pow(2n, 1n+p), 0n)) == Nat.add(internal_bv(c), Nat.double(_)) : Nat}
      %MNat.double_add_sym(u, v) : {Nat.add(Word.to_nat(1n+p, WCon{c, t2}), Bool.pick(Nat, hi, Nat.pow(2n, 1n+p), 0n)) == Nat.add(internal_bv(c), _) : Nat}
      %internal_pick_pow(hi, p) : {Nat.add(Word.to_nat(1n+p, WCon{c, t2}), _) == Nat.add(internal_bv(c), Nat.add(Nat.double(u), Nat.double(v))) : Nat}
      %internal_to_nat_con(p, c, t2) : {Nat.add(_, Nat.double(v)) == Nat.add(internal_bv(c), Nat.add(Nat.double(u), Nat.double(v))) : Nat}
      MNat.add_assoc(internal_bv(c), Nat.double(u), Nat.double(v))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  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.pow
  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.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shl.out.con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=double_add_sym
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_bv
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_pick_pow
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_shl_val
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_to_nat_con