def lowq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divq.bend:30

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

30# the low two bits of Q come from its low digit
31def lowq(+d1: U32, +d2: U32) -> {C.low(2n, v(d2)) == C.low(2n, SW.value(WU.U64{d2, d1})) : Nat}:
32  +e1 = Equal.cong(Nat, Nat, z => Nat.add(v(d2), z), C.shift(32n, v(d1)), C.shift(2n, C.shift(30n, v(d1))), WW.shift_comp(2n, 30n, v(d1)))
33  +e2 = WW.low_add_shift(2n, v(d2), C.shift(30n, v(d1)))
34  Equal.sym(Nat, C.low(2n, SW.value(WU.U64{d2, d1})), C.low(2n, v(d2)), Equal.trans(Nat, C.low(2n, SW.value(WU.U64{d2, d1})), C.low(2n, Nat.add(v(d2), C.shift(2n, C.shift(30n, v(d1))))), C.low(2n, v(d2)), Equal.cong(Nat, Nat, z => C.low(2n, z), SW.value(WU.U64{d2, d1}), Nat.add(v(d2), C.shift(2n, C.shift(30n, v(d1)))), e1), e2))