def hsp

bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:214

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A

214def hsp(+m: Nat) -> {C.high(10n, Nat.add(m, 512n)) == Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))) : Nat}:
215  Equal.trans(Nat, C.high(10n, Nat.add(m, 512n)), C.high(10n, Nat.add(Nat.add(C.low(10n, m), C.shift(10n, C.high(10n, m))), 512n)), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), Equal.cong(Nat, Nat, z => C.high(10n, Nat.add(z, 512n)), m, Nat.add(C.low(10n, m), C.shift(10n, C.high(10n, m))), WW.low_high(10n, m)), Equal.trans(Nat, C.high(10n, Nat.add(Nat.add(C.low(10n, m), C.shift(10n, C.high(10n, m))), 512n)), C.high(10n, Nat.add(Nat.add(C.low(10n, m), 512n), C.shift(10n, C.high(10n, m)))), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), Equal.cong(Nat, Nat, z => C.high(10n, z), Nat.add(Nat.add(C.low(10n, m), C.shift(10n, C.high(10n, m))), 512n), Nat.add(Nat.add(C.low(10n, m), 512n), C.shift(10n, C.high(10n, m))), A.add_rot(C.low(10n, m), C.shift(10n, C.high(10n, m)), 512n)), Equal.trans(Nat, C.high(10n, Nat.add(Nat.add(C.low(10n, m), 512n), C.shift(10n, C.high(10n, m)))), Nat.add(C.high(10n, Nat.add(C.low(10n, m), 512n)), C.high(10n, m)), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), WW.high_add_shift(10n, Nat.add(C.low(10n, m), 512n), C.high(10n, m)), NA.add_comm(C.high(10n, Nat.add(C.low(10n, m), 512n)), C.high(10n, m)))))