def shl_out1

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:126

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

126# the same with the out-shifted bit worth `one`
127def 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}:
128  %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}
129  shl_out(n, c, w)