def ef_g

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:212

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/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

212# the exponent field
213def ef_g(+one: Nat, +h1: {one == 1n : Nat}, +h: U32, +c20: U32, +hc20: {c20 == U32{WD.pw(32n, 20n)} : U32}, +m11: U32, +hm11: {m11 == U32{WD.mask(32n, 11n)} : U32}) -> {v(U32.and(U32.div(h, c20), m11)) == C.low(11n, C.high(20n, v(h))) : Nat}:
214  +hz = L.subst(U32, z => {U32.is_zero(z) == False{} : Bool}, U32{WD.pw(32n, 20n)}, c20, Equal.sym(U32, c20, U32{WD.pw(32n, 20n)}, hc20), {==})
215  +d = U32.div(h, c20)
216  +e3 = Equal.trans(Nat, v(d), Nat.div(v(h), v(c20)), Nat.div(v(h), C.shift(20n, one)), UD.div_nat(h, c20, hz), Equal.cong(Nat, Nat, z => Nat.div(v(h), z), v(c20), C.shift(20n, one), pwv(20n, {==}, one, h1, c20, hc20)))
217  +e4 = Equal.trans(Nat, v(d), Nat.div(v(h), C.shift(20n, one)), C.high(20n, v(h)), e3, div_sh(20n, one, h1, v(h)))
218  Equal.trans(Nat, v(U32.and(d, m11)), C.low(11n, v(d)), C.low(11n, C.high(20n, v(h))), andm(d, 11n, m11, hm11), Equal.cong(Nat, Nat, z => C.low(11n, z), v(d), C.high(20n, v(h)), e4))