Word.shl_con: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as Word
Lines 103-109 of bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&start_line=103&end_line=109

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

def shl_con(+p: Nat, +c: Bool, +b: Bool, +tl: Word(p), r: Bool & Word(p), ih: {Nat.add(S.unsigned(p, ow(p, r)), S.scale_binary(p, S.bit_value(ob(p, r)))) == Nat.add(S.bit_value(b), Nat.double(S.unsigned(p, tl))) : Nat}) -> {Nat.add(S.unsigned(1n+p, ow(1n+p, Word.shl.out.con(p, c, r))), S.scale_binary(1n+p, S.bit_value(ob(1n+p, Word.shl.out.con(p, c, r))))) == Nat.add(S.bit_value(c), Nat.double(S.unsigned(1n+p, WCon{b, tl}))) : Nat}:
  match r:
    case (+hi, +t2):
      %ih : {Nat.add(Nat.add(S.bit_value(c), Nat.double(S.unsigned(p, t2))), Nat.double(S.scale_binary(p, S.bit_value(hi)))) == Nat.add(S.bit_value(c), Nat.double(_)) : Nat}
      Equal.trans(Nat, Nat.add(Nat.add(S.bit_value(c), Nat.double(S.unsigned(p, t2))), Nat.double(S.scale_binary(p, S.bit_value(hi)))), Nat.add(S.bit_value(c), Nat.add(Nat.double(S.unsigned(p, t2)), Nat.double(S.scale_binary(p, S.bit_value(hi))))), Nat.add(S.bit_value(c), Nat.double(Nat.add(S.unsigned(p, t2), S.scale_binary(p, S.bit_value(hi))))),
        N.add_assoc(S.bit_value(c), Nat.double(S.unsigned(p, t2)), Nat.double(S.scale_binary(p, S.bit_value(hi)))),
        Equal.cong(Nat, Nat, z => Nat.add(S.bit_value(c), z), Nat.add(Nat.double(S.unsigned(p, t2)), Nat.double(S.scale_binary(p, S.bit_value(hi)))), Nat.double(Nat.add(S.unsigned(p, t2), S.scale_binary(p, S.bit_value(hi)))), N.add_double(S.unsigned(p, t2), S.scale_binary(p, S.bit_value(hi)))))

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=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=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=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=scale_binary
  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/nat.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_double
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=ob
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=ow