Word.shl_out1: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as Word
Lines 126-129 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&start_line=126&end_line=129

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

# the same with the out-shifted bit worth `one`
def shl_out1(+n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +c: Bool, +w: Word(n)) -> {Nat.add(uw(n, ow(n, Word.shl.out(n, c, w))), sc(n, bo(ob(n, Word.shl.out(n, c, w)), one))) == Nat.add(S.bit_value(c), Nat.double(uw(n, w))) : Nat}:
  %Equal.sym(Nat, bo(ob(n, Word.shl.out(n, c, w)), one), S.bit_value(ob(n, Word.shl.out(n, c, w))), bo_bit(ob(n, Word.shl.out(n, c, w)), one, h1)) : {Nat.add(uw(n, ow(n, Word.shl.out(n, c, w))), sc(n, _)) == Nat.add(S.bit_value(c), Nat.double(uw(n, w))) : Nat}
  shl_out(n, c, w)

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shl.out
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=bo
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=bo_bit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=ob
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=ow
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=shl_out
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=uw