law pack_interpretation
bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/proofs/numeric.bend:294
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as Numeric
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
294law pack_interpretation:
295 for low: U32
296 for high: U32
297 {N.unsigned(64n, W.pack(low, high)) == Nat.add(U32.to_nat(low), N.scale_binary(32n, U32.to_nat(high))) : Nat}