def ws.ea

bend-osdev-word64@0.1.1.0 · proof_shift.bend:389

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

389# 2^k * (lo + 2^n hi) = 2^k lo + 2^n (2^k hi)
390def ws.ea(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n)) -> {U.U32Nat.dbl(k, P.wv.V(n, hw, lw)) == Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)))) : Nat}:
391  Equal.trans(Nat, U.U32Nat.dbl(k, Nat.add(Word.to_nat(n, lw), U.U32Nat.dbl(n, Word.to_nat(n, hw)))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(k, U.U32Nat.dbl(n, Word.to_nat(n, hw)))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)))), UL.dbl_add(k, Word.to_nat(n, lw), U.U32Nat.dbl(n, Word.to_nat(n, hw))), Equal.cong(Nat, Nat, v => Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), v), U.U32Nat.dbl(k, U.U32Nat.dbl(n, Word.to_nat(n, hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), UL.dbl_comm(k, n, Word.to_nat(n, hw))))