def sqn_c
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqc.bend:168
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend as F64sqc
import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
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/f64.bend as SF
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/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
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/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
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/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend as NM
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend as EX
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqf.bend as QF
168def sqn_c(+xl: U32, +xh: U32, +hzx: {Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)) == False{} : Bool}, +o: Bool, +ho: {Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n) == o : Bool}, +ev: Bool, +hev: {Nat.is_eq(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n) == ev : Bool}) -> {F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), o) == SF.pick(F.F64, ev, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))) : F.F64}:
169 match o ev:
170 case True{} True{}:
171 +n1x = NM.n1(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
172 +n2x = NM.n2(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
173 +a53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
174 +a52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
175 +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))
176 +mEN = N.eq_from_is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n, ho)
177 +mXX = N.eq_from_is_eq(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n, hev)
178 +eEN = Equal.trans(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), half_eq(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), z), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n, mEN))
179 +eXX = Equal.trans(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), half_eq(SF.xexp(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), z), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n, mXX))
180 +hj = jf10(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), 2171n), Equal.cong(Nat, Nat, z => Nat.add(z, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.sym(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), eEN)), Equal.trans(Nat, Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(SF.xexp(F.Bits{xl, xh}), 2171n), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), 2171n), n2x, Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), eXX))), hsa)
181 +sv = FL.shl_v(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n, 53n, {==}, {==}, a53)
182 +hnh = Equal.trans(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh}))), sv, Equal.cong(Nat, Nat, z => C.shift(8n, z), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh})), Equal.trans(Nat, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh})), n1x, Equal.cong(Nat, Nat, z => C.shift(z, SF.mant(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), Equal.sym(Nat, Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), N.add_zero(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))))
183 +h62 = L.subst(Nat, z => {C.fits(62n, z) == True{} : Bool}, C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), Equal.sym(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(8n, 54n), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), True{}, RT.fits_sh(8n, 54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SH.fits_mono(53n, 54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), {==}, a53)))
184 +h60 = L.subst(Nat, z => {C.fits(60n, z) == False{} : Bool}, C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), Equal.sym(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(8n, 52n), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), False{}, RT.fits_sh(8n, 52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), a52))
185 +hE = N.add_zero(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))
186 +hp = sqn_c_g1(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN)
187 +hpe = sqn_c_g2(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)
188 +hq = Equal.sym(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), eXX)
189 +hqd = Equal.trans(Nat, Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), {==}, {==})
190 +hMq = Equal.trans(Nat, C.shift(200n, SF.mant(F.Bits{xl, xh})), C.shift(200n, SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(200n, 0n), SF.mant(F.Bits{xl, xh})), {==}, {==})
191 Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), True{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_t(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n, 0n, hnh, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1511n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, SF.mant(F.Bits{xl, xh}), hMq, SF.xexp(F.Bits{xl, xh}), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1021n), hj), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), FR.pk_t(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))
192 case True{} False{}:
193 +n1x = NM.n1(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
194 +n2x = NM.n2(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
195 +a53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
196 +a52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
197 +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))
198 +mEN = N.eq_from_is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n, ho)
199 +mXX = m10(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), NR.dm_lt(1n, SF.xexp(F.Bits{xl, xh})), hev)
200 +eEN = Equal.trans(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), half_eq(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), z), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n, mEN))
201 +eXX = Equal.trans(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), half_eq(SF.xexp(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), z), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 1n, mXX))
202 +hj = jf11(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 2171n), Equal.cong(Nat, Nat, z => Nat.add(z, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.sym(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), eEN)), Equal.trans(Nat, Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(SF.xexp(F.Bits{xl, xh}), 2171n), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 2171n), n2x, Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX))), hsa)
203 +sv = FL.shl_v(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n, 53n, {==}, {==}, a53)
204 +hnh = Equal.trans(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh}))), sv, Equal.cong(Nat, Nat, z => C.shift(8n, z), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh})), Equal.trans(Nat, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh})), n1x, Equal.cong(Nat, Nat, z => C.shift(z, SF.mant(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), Equal.sym(Nat, Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), N.add_zero(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))))
205 +h62 = L.subst(Nat, z => {C.fits(62n, z) == True{} : Bool}, C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), Equal.sym(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(8n, 54n), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), True{}, RT.fits_sh(8n, 54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SH.fits_mono(53n, 54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), {==}, a53)))
206 +h60 = L.subst(Nat, z => {C.fits(60n, z) == False{} : Bool}, C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), Equal.sym(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(8n, 52n), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), False{}, RT.fits_sh(8n, 52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), a52))
207 +hE = N.add_zero(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))
208 +hp = sqn_c_g1(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN)
209 +hpe = sqn_c_g2(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)
210 +hq = Equal.sym(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX)
211 +hqd = Equal.trans(Nat, Nat.div(Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), 2n), Nat.div(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Equal.cong(Nat, Nat, z => Nat.div(z, 2n), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Equal.trans(Nat, Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.sub(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 1n), Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX), FR.sub_add_l(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n))), div_dbl(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)))
212 +hMq = Equal.trans(Nat, C.shift(200n, Nat.mul(2n, SF.mant(F.Bits{xl, xh}))), C.shift(200n, Nat.double(SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(200n, 1n), SF.mant(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => C.shift(200n, z), Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.double(SF.mant(F.Bits{xl, xh})), Equal.sym(Nat, Nat.double(SF.mant(F.Bits{xl, xh})), Nat.mul(2n, SF.mant(F.Bits{xl, xh})), NA.double_mul(SF.mant(F.Bits{xl, xh})))), Equal.sym(Nat, C.shift(Nat.add(200n, 1n), SF.mant(F.Bits{xl, xh})), C.shift(200n, C.shift(1n, SF.mant(F.Bits{xl, xh}))), WW.shift_comp(200n, 1n, SF.mant(F.Bits{xl, xh}))))
213 Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), True{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_t(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n, 1n, hnh, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1511n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, Nat.mul(2n, SF.mant(F.Bits{xl, xh})), hMq, Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1021n), hj), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), FR.pk_f(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))
214 case False{} True{}:
215 +n1x = NM.n1(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
216 +n2x = NM.n2(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
217 +a53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
218 +a52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
219 +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))
220 +mEN = m01(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), NR.dm_lt(1n, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), ho)
221 +mXX = N.eq_from_is_eq(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n, hev)
222 +eEN = Equal.trans(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), half_eq(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), z), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 0n, mEN))
223 +eXX = Equal.trans(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), half_eq(SF.xexp(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), z), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n, mXX))
224 +hj = jf00(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), 2171n), Equal.cong(Nat, Nat, z => Nat.add(z, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.sym(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), eEN)), Equal.trans(Nat, Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(SF.xexp(F.Bits{xl, xh}), 2171n), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), 2171n), n2x, Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), eXX))), hsa)
225 +vAA = Equal.trans(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.low(64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), WA.add_value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), WW.low_fit(64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SH.fits_mono(54n, 64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), {==}, FR.fits_add1(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), a53, a53))))
226 +f54 = L.subst(Nat, z => {C.fits(54n, z) == True{} : Bool}, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.sym(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), vAA), FR.fits_add1(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), a53, a53))
227 +sv0 = FL.shl_v(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n, 54n, {==}, {==}, f54)
228 +sv = Equal.trans(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(8n, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv0, Equal.trans(Nat, C.shift(8n, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(8n, Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.cong(Nat, Nat, z => C.shift(8n, z), SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.trans(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), vAA, Equal.sym(Nat, Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), NA.double_self(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))), WW.shift_dbl(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))
229 +hnh = Equal.trans(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), sv, Equal.trans(Nat, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(8n, 1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.cong(Nat, Nat, z => C.shift(8n, z), C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.trans(Nat, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => C.shift(1n, z), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), n1x), Equal.trans(Nat, C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.sym(Nat, C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => C.shift(z, SF.mant(F.Bits{xl, xh})), Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), NA.add_comm(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))))))))
230 +h62 = L.subst(Nat, z => {C.fits(62n, z) == True{} : Bool}, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), Equal.sym(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(9n, 53n), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), True{}, RT.fits_sh(9n, 53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), a53))
231 +h60 = L.subst(Nat, z => {C.fits(60n, z) == False{} : Bool}, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), Equal.sym(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(9n, 51n), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(51n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), False{}, RT.fits_sh(9n, 51n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), FL.nfit_mono(51n, 52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), {==}, a52)))
232 +eg = EX.eg(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.xexp(F.Bits{xl, xh}), n2x, hsa, EX.xexp_ge(SF.efield(F.Bits{xl, xh})))
233 +hE = Equal.trans(Nat, Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), 1n), Nat.add(1n, Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n)), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NA.add_comm(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), 1n), N.sub_add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n, N.le_trans(1n, 4044n, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), {==}, eg)))
234 +hp = sqn_c_g3(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN, hE)
235 +hpe = sqn_c_g4(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)
236 +hq = Equal.sym(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), eXX)
237 +hqd = Equal.trans(Nat, Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), {==}, {==})
238 +hMq = Equal.trans(Nat, C.shift(200n, SF.mant(F.Bits{xl, xh})), C.shift(200n, SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(200n, 0n), SF.mant(F.Bits{xl, xh})), {==}, {==})
239 Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), False{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_f(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n, 0n, hnh, Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1510n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, SF.mant(F.Bits{xl, xh}), hMq, SF.xexp(F.Bits{xl, xh}), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1022n), hj), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), FR.pk_t(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))
240 case False{} False{}:
241 +n1x = NM.n1(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
242 +n2x = NM.n2(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
243 +a53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
244 +a52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
245 +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))
246 +mEN = m01(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), NR.dm_lt(1n, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), ho)
247 +mXX = m10(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), NR.dm_lt(1n, SF.xexp(F.Bits{xl, xh})), hev)
248 +eEN = Equal.trans(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), half_eq(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), z), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 0n, mEN))
249 +eXX = Equal.trans(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), half_eq(SF.xexp(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), z), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 1n, mXX))
250 +hj = jf01(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 2171n), Equal.cong(Nat, Nat, z => Nat.add(z, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.sym(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), eEN)), Equal.trans(Nat, Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(SF.xexp(F.Bits{xl, xh}), 2171n), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 2171n), n2x, Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX))), hsa)
251 +vAA = Equal.trans(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.low(64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), WA.add_value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), WW.low_fit(64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SH.fits_mono(54n, 64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), {==}, FR.fits_add1(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), a53, a53))))
252 +f54 = L.subst(Nat, z => {C.fits(54n, z) == True{} : Bool}, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.sym(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), vAA), FR.fits_add1(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), a53, a53))
253 +sv0 = FL.shl_v(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n, 54n, {==}, {==}, f54)
254 +sv = Equal.trans(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(8n, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv0, Equal.trans(Nat, C.shift(8n, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(8n, Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.cong(Nat, Nat, z => C.shift(8n, z), SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.trans(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), vAA, Equal.sym(Nat, Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), NA.double_self(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))), WW.shift_dbl(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))
255 +hnh = Equal.trans(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), sv, Equal.trans(Nat, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(8n, 1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.cong(Nat, Nat, z => C.shift(8n, z), C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.trans(Nat, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => C.shift(1n, z), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), n1x), Equal.trans(Nat, C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.sym(Nat, C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => C.shift(z, SF.mant(F.Bits{xl, xh})), Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), NA.add_comm(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))))))))
256 +h62 = L.subst(Nat, z => {C.fits(62n, z) == True{} : Bool}, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), Equal.sym(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(9n, 53n), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), True{}, RT.fits_sh(9n, 53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), a53))
257 +h60 = L.subst(Nat, z => {C.fits(60n, z) == False{} : Bool}, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), Equal.sym(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(9n, 51n), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(51n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), False{}, RT.fits_sh(9n, 51n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), FL.nfit_mono(51n, 52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), {==}, a52)))
258 +eg = EX.eg(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.xexp(F.Bits{xl, xh}), n2x, hsa, EX.xexp_ge(SF.efield(F.Bits{xl, xh})))
259 +hE = Equal.trans(Nat, Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), 1n), Nat.add(1n, Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n)), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NA.add_comm(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), 1n), N.sub_add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n, N.le_trans(1n, 4044n, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), {==}, eg)))
260 +hp = sqn_c_g3(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN, hE)
261 +hpe = sqn_c_g4(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)
262 +hq = Equal.sym(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX)
263 +hqd = Equal.trans(Nat, Nat.div(Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), 2n), Nat.div(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Equal.cong(Nat, Nat, z => Nat.div(z, 2n), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Equal.trans(Nat, Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.sub(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 1n), Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX), FR.sub_add_l(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n))), div_dbl(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)))
264 +hMq = Equal.trans(Nat, C.shift(200n, Nat.mul(2n, SF.mant(F.Bits{xl, xh}))), C.shift(200n, Nat.double(SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(200n, 1n), SF.mant(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => C.shift(200n, z), Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.double(SF.mant(F.Bits{xl, xh})), Equal.sym(Nat, Nat.double(SF.mant(F.Bits{xl, xh})), Nat.mul(2n, SF.mant(F.Bits{xl, xh})), NA.double_mul(SF.mant(F.Bits{xl, xh})))), Equal.sym(Nat, C.shift(Nat.add(200n, 1n), SF.mant(F.Bits{xl, xh})), C.shift(200n, C.shift(1n, SF.mant(F.Bits{xl, xh}))), WW.shift_comp(200n, 1n, SF.mant(F.Bits{xl, xh}))))
265 Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), False{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_f(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n, 1n, hnh, Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1510n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, Nat.mul(2n, SF.mant(F.Bits{xl, xh})), hMq, Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1022n), hj), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), FR.pk_f(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))