def mask_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:53

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

53def mask_v(+k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +m: U32, +pm: {m == U32{WD.mask(32n, k)} : U32}) -> {1n+v(m) == WD.sc(k, one) : Nat}:
54  +e = L.subst(U32, z => {v(z) == WD.uw(32n, WD.mask(32n, k)) : Nat}, U32{WD.mask(32n, k)}, m, Equal.sym(U32, m, U32{WD.mask(32n, k)}, pm), UD.vw(WD.mask(32n, k)))
55  Equal.trans(Nat, 1n+v(m), 1n+WD.uw(32n, WD.mask(32n, k)), WD.sc(k, one), N.succ_cong(v(m), WD.uw(32n, WD.mask(32n, k)), e), mval(32n, k, one, h1, hk))