def val_pack
bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64.bend:163
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as U64
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as NUM
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
163def val_pack(+lo: U32, +hi: U32) -> {S.unsigned(64n, W.pack(lo, hi)) == Nat.add(UD.v(lo), WD.sc(32n, UD.v(hi))) : Nat}:
164 NUM.pack_interpretation(lo, hi)