~/jendhub

def internal_shl_out32

bend-mathlib@0.8.1.0 · u32.bend:809

import bend-mathlib@0.8.1.0/u32.bend as U32
import Base

809def internal_shl_out32(-md: Nat, em: {Nat.pow(2n, 32n) == md : Nat}, x: Bool, rw: Word(32n)) -> {internal_shl_val(32n, md, Word.shl.out(32n, x, rw)) == Nat.add(internal_bv(x), Nat.double(Word.to_nat(32n, rw))) : Nat}:
810  %em : {internal_shl_val(32n, _, Word.shl.out(32n, x, rw)) == Nat.add(internal_bv(x), Nat.double(Word.to_nat(32n, rw))) : Nat}
811  internal_shl_out(32n, x, rw)

Uses (11)

Used by (1)