~/jendhub

def AP.shln_pw

bend-osdev-array@0.1.0.1 · PROOF.bend:384

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base

384# shln(1, d) is 2^d
385def AP.shln_pw(d: Nat) -> {U32.shln(1, d) == U32{AP.pw(32n, d)} : U32}:
386  match d:
387    case 0n:
388      {==}
389    case 1n+ +e:
390      %Equal.sym(U32, U32.shln(1, e), U32{AP.pw(32n, e)}, AP.shln_pw(e)) : {U32.shl(_) == U32{AP.pw(32n, 1n+e)} : U32}
391      AP.u32_cong(Word.shl(32n, AP.pw(32n, e)), AP.pw(32n, 1n+e), Equal.trans(Word(32n), Word.shl(32n, AP.pw(32n, e)), Word.shl.put(32n, False{}, AP.pw(32n, e)), AP.pw(32n, 1n+e), AP.shl_put(32n, AP.pw(32n, e)), AP.sp(32n, e)))

Uses (14)

Used by (1)