1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/math/f64.bend as SF
4	import ../../../spec/math/w64.bend as SW
5	import ../../../src/math/f64.bend as F
6	import ../../../src/math/w64.bend as X
7	import ../../../src/math/u64.bend as WU
8	import ../../../src/math/natural.bend as M
9	import ../../lib/nat.bend as N
10	import ../../lib/logic.bend as L
11	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
12	import ../../lib/u32half.bend as UH
13	import ../../lib/word.bend as WD
14	import ../natural/bits.bend as BT
15	import ./width.bend as WW
16	import ./w64add.bend as WA
17	import ./w64sh.bend as SH
18	import ./w64clz.bend as CLZ
19	import ./f64bits.bend as FB
20	import ./f64round.bend as FR
21	import ./f64rtools.bend as RT
22	import ./f64bl.bend as BL
23	import ./f64cmp.bend as FC
24	
25	# SoftFloat's normSubnormalF64Sig and the hidden bit: a finite nonzero
26	# double's significand as a 53-bit A = m * 2^sa (m the spec's mant) at the
27	# offset exponent norm_e, with norm_e + sa = xexp + 2171.
28	
29	def v(+x: U32) -> Nat:
30	  U32.to_nat(x)
31	
32	def sa(+ea: Nat, +fa: WU.U64) -> Nat:
33	  match ea:
34	    case 0n:
35	      Nat.sub(X.clz(fa), 11n)
36	    case _:
37	      0n
38	
39	# the hidden bit: f + 2^52 for a fraction below 2^52
40	def hid(+one: Nat, +h1: {one == 1n : Nat}, +fa: WU.U64, +hF: {C.fits(52n, SW.value(fa)) == True{} : Bool}, +c: U32, +hc: {c == U32{WD.pw(32n, 20n)} : U32}) -> {SW.value(X.add(fa, WU.U64{0, c})) == Nat.add(SW.value(fa), C.shift(52n, one)) : Nat}:
41	  a1 = WA.add_value(fa, WU.U64{0, c})
42	  +ec = Equal.trans(Nat, C.shift(32n, v(c)), C.shift(32n, C.shift(20n, one)), C.shift(52n, one), Equal.cong(Nat, Nat, z => C.shift(32n, z), v(c), C.shift(20n, one), FB.pwv(20n, {==}, one, h1, c, hc)), Equal.sym(Nat, C.shift(52n, one), C.shift(32n, C.shift(20n, one)), WW.shift_comp(32n, 20n, one)))
43	  +f53 = WW.limbs_fit(52n, 1n, SW.value(fa), one, hF, L.subst(Nat, z => {C.fits(1n, z) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==}))
44	  +f64 = SH.fits_mono(53n, 64n, Nat.add(SW.value(fa), C.shift(52n, one)), {==}, f53)
45	  Equal.trans(Nat, SW.value(X.add(fa, WU.U64{0, c})), C.low(64n, Nat.add(SW.value(fa), C.shift(32n, v(c)))), Nat.add(SW.value(fa), C.shift(52n, one)), a1, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(fa), C.shift(32n, v(c)))), C.low(64n, Nat.add(SW.value(fa), C.shift(52n, one))), Nat.add(SW.value(fa), C.shift(52n, one)), Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(SW.value(fa), z)), C.shift(32n, v(c)), C.shift(52n, one), ec), WW.low_fit(64n, Nat.add(SW.value(fa), C.shift(52n, one)), f64)))
46	
47	# ---- a subnormal fraction shifted up to bit 52 ----
48	
49	def clz_t(+fa: WU.U64, +Fr: Nat, +hfa: {SW.value(fa) == Fr : Nat}, +hb: {Nat.is_le(M.bit_length(Fr), 52n) == True{} : Bool}) -> {Nat.sub(X.clz(fa), 11n) == Nat.sub(53n, M.bit_length(Fr)) : Nat}:
50	  +ec = Equal.trans(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(SW.value(fa))), Nat.sub(64n, M.bit_length(Fr)), CLZ.clz_value(fa), Equal.cong(Nat, Nat, z => Nat.sub(64n, M.bit_length(z)), SW.value(fa), Fr, hfa))
51	  +hb53 = N.le_trans(M.bit_length(Fr), 52n, 53n, hb, {==})
52	  +e1 = Equal.cong(Nat, Nat, z => Nat.sub(z, 11n), X.clz(fa), Nat.sub(64n, M.bit_length(Fr)), ec)
53	  +e2 = Equal.cong(Nat, Nat, z => Nat.sub(z, 11n), Nat.sub(64n, M.bit_length(Fr)), Nat.add(11n, Nat.sub(53n, M.bit_length(Fr))), FR.sub_add_a(11n, 53n, M.bit_length(Fr), hb53))
54	  Equal.trans(Nat, Nat.sub(X.clz(fa), 11n), Nat.sub(Nat.sub(64n, M.bit_length(Fr)), 11n), Nat.sub(53n, M.bit_length(Fr)), e1, Equal.trans(Nat, Nat.sub(Nat.sub(64n, M.bit_length(Fr)), 11n), Nat.sub(Nat.add(11n, Nat.sub(53n, M.bit_length(Fr))), 11n), Nat.sub(53n, M.bit_length(Fr)), e2, N.add_sub_cancel(11n, Nat.sub(53n, M.bit_length(Fr)))))
55	
56	def sub_fit(+fa: WU.U64, +Fr: Nat, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hz: {Nat.is_eq(Fr, 0n) == False{} : Bool}) -> {C.fits(53n, C.shift(Nat.sub(X.clz(fa), 11n), Fr)) == True{} : Bool}:
57	  +hb = BL.bl_le(52n, Fr, hF, Nat.is_le(M.bit_length(Fr), 52n), {==})
58	  +et = clz_t(fa, Fr, hfa, hb)
59	  +k = Nat.sub(53n, M.bit_length(Fr))
60	  +hb53 = N.le_trans(M.bit_length(Fr), 52n, 53n, hb, {==})
61	  +ek = Equal.trans(Nat, Nat.add(k, M.bit_length(Fr)), Nat.add(M.bit_length(Fr), k), 53n, NA.add_comm(k, M.bit_length(Fr)), N.sub_add(53n, M.bit_length(Fr), hb53))
62	  +hqu = L.subst(Nat, z => {Nat.is_lt(C.shift(k, Fr), z) == True{} : Bool}, C.shift(k, C.pow2(M.bit_length(Fr))), C.pow2(Nat.add(k, M.bit_length(Fr))), WW.shift_pow2(k, M.bit_length(Fr)), WW.shift_lt(k, Fr, C.pow2(M.bit_length(Fr)), BT.bit_length_lt(Fr)))
63	  +f53 = L.subst(Nat, z => {C.fits(z, C.shift(k, Fr)) == True{} : Bool}, Nat.add(k, M.bit_length(Fr)), 53n, ek, WW.fits_of_lt(Nat.add(k, M.bit_length(Fr)), C.shift(k, Fr), hqu))
64	  L.subst(Nat, z => {C.fits(53n, C.shift(z, Fr)) == True{} : Bool}, k, Nat.sub(X.clz(fa), 11n), Equal.sym(Nat, Nat.sub(X.clz(fa), 11n), k, et), f53)
65	
66	def sub_nfit(+fa: WU.U64, +Fr: Nat, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hz: {Nat.is_eq(Fr, 0n) == False{} : Bool}) -> {C.fits(52n, C.shift(Nat.sub(X.clz(fa), 11n), Fr)) == False{} : Bool}:
67	  +hb = BL.bl_le(52n, Fr, hF, Nat.is_le(M.bit_length(Fr), 52n), {==})
68	  +et = clz_t(fa, Fr, hfa, hb)
69	  +k = Nat.sub(53n, M.bit_length(Fr))
70	  +hb53 = N.le_trans(M.bit_length(Fr), 52n, 53n, hb, {==})
71	  +ek = Equal.trans(Nat, Nat.add(k, M.bit_length(Fr)), Nat.add(M.bit_length(Fr), k), 53n, NA.add_comm(k, M.bit_length(Fr)), N.sub_add(53n, M.bit_length(Fr), hb53))
72	  +pb = Nat.sub(M.bit_length(Fr), 1n)
73	  +epb = N.sub_add(M.bit_length(Fr), 1n, BL.bl_pos(Fr, hz, M.bit_length(Fr), {==}))
74	  +K2 = Nat.add(k, pb)
75	  +e52 = N.succ_inj(K2, 52n, Equal.trans(Nat, 1n+K2, Nat.add(k, 1n+pb), 53n, Equal.sym(Nat, Nat.add(k, 1n+pb), 1n+K2, N.add_succ(k, pb)), Equal.trans(Nat, Nat.add(k, 1n+pb), Nat.add(k, M.bit_length(Fr)), 53n, Equal.cong(Nat, Nat, z => Nat.add(k, z), 1n+pb, M.bit_length(Fr), epb), ek)))
76	  +hql = L.subst(Nat, z => {Nat.is_le(z, C.shift(k, Fr)) == True{} : Bool}, C.shift(k, C.pow2(pb)), C.pow2(K2), WW.shift_pow2(k, pb), WW.shift_mono(k, C.pow2(pb), Fr, BL.lower(Fr, hz)))
77	  +nf = Equal.trans(Bool, C.fits(K2, C.pow2(K2)), Nat.is_lt(C.pow2(K2), C.pow2(K2)), False{}, WW.fits_lt(K2, C.pow2(K2)), N.lt_irrefl(C.pow2(K2)))
78	  +f52 = L.subst(Nat, z => {C.fits(z, C.shift(k, Fr)) == False{} : Bool}, K2, 52n, e52, FR.nfit(K2, C.pow2(K2), C.shift(k, Fr), hql, nf))
79	  L.subst(Nat, z => {C.fits(52n, C.shift(z, Fr)) == False{} : Bool}, k, Nat.sub(X.clz(fa), 11n), Equal.sym(Nat, Nat.sub(X.clz(fa), 11n), k, et), f52)
80	
81	def sub_val(+fa: WU.U64, +Fr: Nat, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hz: {Nat.is_eq(Fr, 0n) == False{} : Bool}) -> {SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))) == C.shift(Nat.sub(X.clz(fa), 11n), Fr) : Nat}:
82	  +hb = BL.bl_le(52n, Fr, hF, Nat.is_le(M.bit_length(Fr), 52n), {==})
83	  +et = clz_t(fa, Fr, hfa, hb)
84	  +hk = N.le_lt_trans(Nat.sub(X.clz(fa), 11n), 53n, 64n, L.subst(Nat, z => {Nat.is_le(z, 53n) == True{} : Bool}, Nat.sub(53n, M.bit_length(Fr)), Nat.sub(X.clz(fa), 11n), Equal.sym(Nat, Nat.sub(X.clz(fa), 11n), Nat.sub(53n, M.bit_length(Fr)), et), UH.sub_le(53n, M.bit_length(Fr))), {==})
85	  sv = SH.shl_value(fa, Nat.sub(X.clz(fa), 11n), hk)
86	  Equal.trans(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), SW.value(fa))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), sv, Equal.trans(Nat, C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), SW.value(fa))), C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), Fr)), C.shift(Nat.sub(X.clz(fa), 11n), Fr), Equal.cong(Nat, Nat, z => C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), z)), SW.value(fa), Fr, hfa), WW.low_fit(64n, C.shift(Nat.sub(X.clz(fa), 11n), Fr), SH.fits_mono(53n, 64n, C.shift(Nat.sub(X.clz(fa), 11n), Fr), {==}, sub_fit(fa, Fr, hfa, hF, hz)))))
87	
88	def sub_sum(+A: Nat, +t: Nat, +B: Nat, +hB: {Nat.is_le(B, t) == True{} : Bool}, +hA: {Nat.is_le(t, A) == True{} : Bool}) -> {Nat.add(Nat.sub(A, t), Nat.sub(t, B)) == Nat.sub(A, B) : Nat}:
89	  +r = Nat.sub(t, B)
90	  +q = Nat.sub(A, t)
91	  +et = N.sub_add(t, B, hB)
92	  +eA = N.sub_add(A, t, hA)
93	  +e1 = Equal.trans(Nat, Nat.sub(A, B), Nat.sub(Nat.add(t, q), B), Nat.add(q, r), Equal.cong(Nat, Nat, z => Nat.sub(z, B), A, Nat.add(t, q), Equal.sym(Nat, Nat.add(t, q), A, eA)), Equal.trans(Nat, Nat.sub(Nat.add(t, q), B), Nat.sub(Nat.add(Nat.add(B, r), q), B), Nat.add(q, r), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, q), B), t, Nat.add(B, r), Equal.sym(Nat, Nat.add(B, r), t, et)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(B, r), q), B), Nat.sub(Nat.add(B, Nat.add(r, q)), B), Nat.add(q, r), Equal.cong(Nat, Nat, z => Nat.sub(z, B), Nat.add(Nat.add(B, r), q), Nat.add(B, Nat.add(r, q)), NA.add_assoc(B, r, q)), Equal.trans(Nat, Nat.sub(Nat.add(B, Nat.add(r, q)), B), Nat.add(r, q), Nat.add(q, r), N.add_sub_cancel(B, Nat.add(r, q)), NA.add_comm(r, q)))))
94	  Equal.sym(Nat, Nat.sub(A, B), Nat.add(q, r), e1)
95	
96	def ez0(+E: Nat, +hea: {0n == E : Nat}) -> {Nat.is_eq(E, 0n) == True{} : Bool}:
97	  Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), E, 0n, Equal.sym(Nat, 0n, E, hea))
98	
99	def ezs(+p: Nat, +E: Nat, +hea: {1n+p == E : Nat}) -> {Nat.is_eq(E, 0n) == False{} : Bool}:
100	  Equal.sym(Bool, False{}, Nat.is_eq(E, 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), 1n+p, E, hea))
101	
102	# the normalized significand
103	def n1(+one: Nat, +h1: {one == 1n : Nat}, +ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {SW.value(F.norm_f(ea, fa)) == C.shift(sa(ea, fa), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n)))))) : Nat}:
104	  match ea:
105	    case 0n:
106	      +ez = ez0(E, hea)
107	      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
108	      +em = Equal.trans(Nat, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Nat.add(Fr, 0n), Fr, Equal.cong(Bool, Nat, t => Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(t)))), Nat.is_eq(E, 0n), True{}, ez), N.add_zero(Fr))
109	      Equal.trans(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), C.shift(Nat.sub(X.clz(fa), 11n), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n)))))), sub_val(fa, Fr, hfa, hF, hz), Equal.cong(Nat, Nat, z => C.shift(Nat.sub(X.clz(fa), 11n), z), Fr, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Equal.sym(Nat, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Fr, em)))
110	    case 1n+ +p:
111	      +ez = ezs(p, E, hea)
112	      +ec = Equal.trans(Nat, SF.b2n(Bool.not(Nat.is_eq(E, 0n))), 1n, one, Equal.cong(Bool, Nat, t => SF.b2n(Bool.not(t)), Nat.is_eq(E, 0n), False{}, ez), Equal.sym(Nat, one, 1n, h1))
113	      +em = Equal.cong(Nat, Nat, z => Nat.add(Fr, C.shift(52n, z)), SF.b2n(Bool.not(Nat.is_eq(E, 0n))), one, ec)
114	      +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fr, SW.value(fa), Equal.sym(Nat, SW.value(fa), Fr, hfa), hF)
115	      Equal.trans(Nat, SW.value(X.add(fa, WU.U64{0, 1048576})), Nat.add(SW.value(fa), C.shift(52n, one)), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), hid(one, h1, fa, hFv, 1048576, {==}), Equal.trans(Nat, Nat.add(SW.value(fa), C.shift(52n, one)), Nat.add(Fr, C.shift(52n, one)), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, one)), SW.value(fa), Fr, hfa), Equal.sym(Nat, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Nat.add(Fr, C.shift(52n, one)), em)))
116	
117	# the exponent: norm_e + sa = xexp + 2171
118	def n2(+ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {Nat.add(F.norm_e(ea, fa), sa(ea, fa)) == Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n) : Nat}:
119	  match ea:
120	    case 0n:
121	      +ez = ez0(E, hea)
122	      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
123	      +hb = BL.bl_le(52n, Fr, hF, Nat.is_le(M.bit_length(Fr), 52n), {==})
124	      +ec = Equal.trans(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(SW.value(fa))), Nat.sub(64n, M.bit_length(Fr)), CLZ.clz_value(fa), Equal.cong(Nat, Nat, z => Nat.sub(64n, M.bit_length(z)), SW.value(fa), Fr, hfa))
125	      +h11 = L.subst(Nat, z => {Nat.is_le(11n, z) == True{} : Bool}, Nat.sub(64n, M.bit_length(Fr)), X.clz(fa), Equal.sym(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(Fr)), ec), RT.le_sub(11n, M.bit_length(Fr), 64n, N.le_add_left(M.bit_length(Fr), 53n, 11n, N.le_trans(M.bit_length(Fr), 52n, 53n, hb, {==}))))
126	      +h4108 = L.subst(Nat, z => {Nat.is_le(z, 4108n) == True{} : Bool}, Nat.sub(64n, M.bit_length(Fr)), X.clz(fa), Equal.sym(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(Fr)), ec), N.le_trans(Nat.sub(64n, M.bit_length(Fr)), 64n, 4108n, UH.sub_le(64n, M.bit_length(Fr)), {==}))
127	      +l1 = sub_sum(4108n, X.clz(fa), 11n, h11, h4108)
128	      +r1 = Equal.cong(Bool, Nat, t => Nat.add(SF.pick(Nat, t, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.is_eq(E, 0n), True{}, ez)
129	      Equal.trans(Nat, Nat.add(Nat.sub(4108n, X.clz(fa)), Nat.sub(X.clz(fa), 11n)), 4097n, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), l1, Equal.sym(Nat, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), 4097n, r1))
130	    case 1n+ +p:
131	      +ez = ezs(p, E, hea)
132	      +r1 = Equal.cong(Bool, Nat, t => Nat.add(SF.pick(Nat, t, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.is_eq(E, 0n), False{}, ez)
133	      +r2 = Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), Nat.sub(Nat.add(E, SF.zb()), 1075n), Nat.add(1925n, E), FC.esub(E))
134	      +r3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(1925n, z), 2171n), E, 1n+p, Equal.sym(Nat, 1n+p, E, hea))
135	      +r4 = Equal.cong(Nat, Nat, z => Nat.add(1926n, z), Nat.add(p, 2171n), Nat.add(2171n, p), NA.add_comm(p, 2171n))
136	      +rr = Equal.trans(Nat, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.add(Nat.sub(Nat.add(E, SF.zb()), 1075n), 2171n), Nat.add(4096n, 1n+p), r1, Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(E, SF.zb()), 1075n), 2171n), Nat.add(Nat.add(1925n, E), 2171n), Nat.add(4096n, 1n+p), r2, Equal.trans(Nat, Nat.add(Nat.add(1925n, E), 2171n), Nat.add(Nat.add(1925n, 1n+p), 2171n), Nat.add(4096n, 1n+p), r3, r4)))
137	      Equal.trans(Nat, Nat.add(Nat.add(F.off(), 1n+p), 0n), Nat.add(4096n, 1n+p), Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), N.add_zero(Nat.add(F.off(), 1n+p)), Equal.sym(Nat, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.add(4096n, 1n+p), rr))
138	
139	# the normalized significand has its top bit at 52
140	def n3a(+one: Nat, +h1: {one == 1n : Nat}, +ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {C.fits(53n, SW.value(F.norm_f(ea, fa))) == True{} : Bool}:
141	  match ea:
142	    case 0n:
143	      +ez = ez0(E, hea)
144	      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
145	      L.subst(Nat, z => {C.fits(53n, z) == True{} : Bool}, C.shift(Nat.sub(X.clz(fa), 11n), Fr), SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), Equal.sym(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), sub_val(fa, Fr, hfa, hF, hz)), sub_fit(fa, Fr, hfa, hF, hz))
146	    case 1n+ +p:
147	      +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fr, SW.value(fa), Equal.sym(Nat, SW.value(fa), Fr, hfa), hF)
148	      +f = WW.limbs_fit(52n, 1n, SW.value(fa), one, hFv, L.subst(Nat, z => {C.fits(1n, z) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==}))
149	      L.subst(Nat, z => {C.fits(53n, z) == True{} : Bool}, Nat.add(SW.value(fa), C.shift(52n, one)), SW.value(X.add(fa, WU.U64{0, 1048576})), Equal.sym(Nat, SW.value(X.add(fa, WU.U64{0, 1048576})), Nat.add(SW.value(fa), C.shift(52n, one)), hid(one, h1, fa, hFv, 1048576, {==})), f)
150	
151	def n3b(+one: Nat, +h1: {one == 1n : Nat}, +ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {C.fits(52n, SW.value(F.norm_f(ea, fa))) == False{} : Bool}:
152	  match ea:
153	    case 0n:
154	      +ez = ez0(E, hea)
155	      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
156	      L.subst(Nat, z => {C.fits(52n, z) == False{} : Bool}, C.shift(Nat.sub(X.clz(fa), 11n), Fr), SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), Equal.sym(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), sub_val(fa, Fr, hfa, hF, hz)), sub_nfit(fa, Fr, hfa, hF, hz))
157	    case 1n+ +p:
158	      +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fr, SW.value(fa), Equal.sym(Nat, SW.value(fa), Fr, hfa), hF)
159	      +nf = Equal.trans(Bool, C.fits(52n, C.shift(52n, one)), Nat.is_lt(C.shift(52n, one), C.shift(52n, one)), False{}, Equal.sym(Bool, Nat.is_lt(C.shift(52n, one), C.shift(52n, one)), C.fits(52n, C.shift(52n, one)), FR.lt_fit(52n, one, h1, C.shift(52n, one))), N.lt_irrefl(C.shift(52n, one)))
160	      +hle = L.subst(Nat, z => {Nat.is_le(C.shift(52n, one), z) == True{} : Bool}, Nat.add(C.shift(52n, one), SW.value(fa)), Nat.add(SW.value(fa), C.shift(52n, one)), NA.add_comm(C.shift(52n, one), SW.value(fa)), N.le_add_right(C.shift(52n, one), SW.value(fa)))
161	      L.subst(Nat, z => {C.fits(52n, z) == False{} : Bool}, Nat.add(SW.value(fa), C.shift(52n, one)), SW.value(X.add(fa, WU.U64{0, 1048576})), Equal.sym(Nat, SW.value(X.add(fa, WU.U64{0, 1048576})), Nat.add(SW.value(fa), C.shift(52n, one)), hid(one, h1, fa, hFv, 1048576, {==})), FR.nfit(52n, C.shift(52n, one), Nat.add(SW.value(fa), C.shift(52n, one)), hle, nf))