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/natural.bend as M
8	import ../../lib/nat.bend as N
9	import ../../lib/logic.bend as L
10	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
11	import ./width.bend as WW
12	import ./w64sh.bend as SH
13	import ./w64clz.bend as CZ
14	import ./f64bits.bend as FB
15	import ./f64round.bend as FR
16	import ./u32laws.bend as LW
17	import ../../lib/word.bend as WD
18	import ./f64bl.bend as BL
19	import ./f64rtools.bend as RT
20	import ./f64tools.bend as T
21	import ./f64rint.bend as RI
22	
23	# frexp and ldexp (python_style_math_stdlib_design.pdf 4.4; C99 7.12.6.4,
24	# 7.12.6.6 and F.9.3.4, F.9.3.6): Frexp.value, Ldexp.value. frexp rounds
25	# the significand at the scale Z - bit_length (exact: f64tools.rw_value with
26	# Clz.value for the bit length); ldexp rounds the significand at the moved
27	# scale, and a scale below the subnormal range by more than the significand
28	# is a zero of x's sign (tiny below: Flocq's round_NE of a value under half
29	# the smallest subnormal).
30	
31	# ---- underflow to zero ----
32	
33	def sub_le_self(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}:
34	  match a b:
35	    case 0n 0n:
36	      {==}
37	    case 0n 1n+ +bp:
38	      {==}
39	    case 1n+ +ap 0n:
40	      N.le_refl(1n+ap)
41	    case 1n+ +ap 1n+ +bp:
42	      N.le_trans(Nat.sub(ap, bp), ap, 1n+ap, sub_le_self(ap, bp), N.le_succ(ap))
43	
44	# m < 2^53 divided by 2^(1+j) >= 2^54 rounds to 0
45	def rne_zero(+m: Nat, +j: Nat, +hm: {C.fits(53n, m) == True{} : Bool}, +hj: {Nat.is_le(53n, j) == True{} : Bool}) -> {SF.rne(m, 1n+j) == 0n : Nat}:
46	  +hj1 = N.le_trans(53n, j, 1n+j, hj, N.le_succ(j))
47	  +f1 = SH.fits_mono(53n, 1n+j, m, hj1, hm)
48	  +eh = N.eq_from_is_eq(C.high(1n+j, m), 0n, f1)
49	  +el = WW.low_fit(1n+j, m, SH.fits_mono(53n, 1n+j, m, N.le_trans(53n, j, 1n+j, hj, N.le_succ(j)), hm))
50	  +fj = SH.fits_mono(53n, j, m, hj, hm)
51	  +hl = Equal.trans(Bool, Nat.is_lt(m, C.shift(j, 1n)), C.fits(j, m), True{}, FR.lt_fit(j, 1n, {==}, m), fj)
52	  +la = RI.nlt(j, 1n, {==}, m, SH.fits_mono(53n, j, m, hj, hm))
53	  +le = N.is_eq_lt(m, C.shift(j, 1n), hl)
54	  +H = C.shift(j, 1n)
55	  +e1 = Equal.cong(Nat, Nat, t => SF.rne_up(t, C.low(1n+j, m), H), C.high(1n+j, m), 0n, eh)
56	  +e2 = Equal.cong(Nat, Nat, t => SF.rne_up(0n, t, H), C.low(1n+j, m), m, el)
57	  +e3 = Equal.cong(Bool, Nat, b => Nat.add(0n, SF.b2n(Bool.or(b, Bool.and(Nat.is_eq(m, H), False{})))), Nat.is_lt(H, m), False{}, la)
58	  +e4 = Equal.cong(Bool, Nat, b => SF.b2n(Bool.and(b, False{})), Nat.is_eq(m, H), False{}, le)
59	  Equal.trans(Nat, SF.rne(m, 1n+j), SF.rne_up(0n, C.low(1n+j, m), H), 0n, e1, Equal.trans(Nat, SF.rne_up(0n, C.low(1n+j, m), H), SF.rne_up(0n, m, H), 0n, e2, Equal.trans(Nat, SF.rne_up(0n, m, H), SF.b2n(Bool.and(Nat.is_eq(m, H), False{})), 0n, e3, e4)))
60	
61	def max_le(+a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.max(a, b) == b : Nat}:
62	  match a b:
63	    case 0n _:
64	      {==}
65	    case 1n+ +ap 0n:
66	      Empty.absurd({Nat.max(1n+ap, 0n) == 0n : Nat}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
67	    case 1n+ +ap 1n+ +bp:
68	      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(ap, bp), bp, max_le(ap, bp, h))
69	
70	# a zero pattern with sign s (as f64addc.bz)
71	def bz0(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {F.Bits{0, U32.from_nat(C.shift(31n, SF.pick(Nat, s, one, 0n)))} == SF.pick(F.F64, s, F.Bits{0, c}, F.Bits{0, 0}) : F.F64}:
72	  match s:
73	    case True{}:
74	      Equal.cong(U32, F.F64, z => F.Bits{0, z}, U32.from_nat(C.shift(31n, one)), c, Equal.trans(U32, U32.from_nat(C.shift(31n, one)), U32.from_nat(U32.to_nat(c)), c, Equal.cong(Nat, U32, z => U32.from_nat(z), C.shift(31n, one), U32.to_nat(c), Equal.sym(Nat, U32.to_nat(c), C.shift(31n, one), FB.pwv(31n, {==}, one, h1, c, hc))), LW.rt(c)))
75	    case False{}:
76	      {==}
77	
78	def bz(+s: Bool) -> {FR.bits(s, 0n) == SF.zero(s) : F.F64}:
79	  Equal.trans(F.F64, F.Bits{0, U32.from_nat(C.shift(31n, SF.b2n(s)))}, F.Bits{0, U32.from_nat(C.shift(31n, SF.pick(Nat, s, 1n, 0n)))}, SF.zero(s), Equal.cong(Nat, F.F64, z => F.Bits{0, U32.from_nat(C.shift(31n, z))}, SF.b2n(s), SF.pick(Nat, s, 1n, 0n), Equal.sym(Nat, SF.pick(Nat, s, 1n, 0n), SF.b2n(s), FR.pb(s, 1n, {==}))), bz0(1n, {==}, s, 2147483648, {==}))
80	
81	# round_u unfolded at an abstract ulp u: instantiated at a literal u, the
82	# checker never evaluates pack's closed exponent arithmetic
83	def ru(+s: Bool, +m: Nat, +x: Nat, +u: Nat) -> {SF.round_u(s, m, x, u) == SF.pack(s, SF.pick(Nat, Nat.is_le(x, u), SF.rne(m, Nat.sub(u, x)), C.shift(Nat.sub(x, u), m)), u) : F.F64}:
84	  {==}
85	
86	def tiny_c(+s: Bool, +m: Nat, +x: Nat, +hm: {C.fits(53n, m) == True{} : Bool}, +hx: {Nat.is_lt(x, 63n) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(m, 0n) == z : Bool}) -> {SF.round(s, m, x) == SF.zero(s) : F.F64}:
87	  match z:
88	    case True{}:
89	      Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.zero(s), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), 1926n))), Nat.is_eq(m, 0n), True{}, hz)
90	    case False{}:
91	      +B = M.bit_length(m)
92	      +A = Nat.sub(Nat.add(x, B), 53n)
93	      +hB = BL.bl_le(53n, m, hm, Nat.is_le(B, 53n), {==})
94	      +hx62 = N.lt_succ_le(x, 62n, hx)
95	      +h1 = Equal.trans(Bool, Nat.is_le(Nat.add(x, B), Nat.add(62n, B)), Nat.is_le(x, 62n), True{}, FR.le_cancel_r(x, 62n, B), hx62)
96	      +h2 = N.le_trans(B, 53n, 1864n, hB, {==})
97	      +hA = N.le_trans(A, Nat.add(x, B), 1926n, sub_le_self(Nat.add(x, B), 53n), N.le_trans(Nat.add(x, B), Nat.add(62n, B), 1926n, h1, h2))
98	      +emax = max_le(A, 1926n, hA)
99	      +hxa = N.le_trans(x, 62n, 1926n, N.lt_succ_le(x, 62n, hx), {==})
100	      +hxb = N.le_trans(x, 62n, 1925n, N.lt_succ_le(x, 62n, hx), {==})
101	      +j = Nat.sub(1925n, x)
102	      +hj = RT.le_sub(53n, x, 1925n, N.le_trans(x, 62n, 1872n, N.lt_succ_le(x, 62n, hx), {==}))
103	      +P = SF.pick(Nat, Nat.is_le(x, 1926n), SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m))
104	      +e1 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.zero(s), SF.round_u(s, m, x, Nat.max(A, 1926n))), Nat.is_eq(m, 0n), False{}, hz)
105	      +e2 = Equal.cong(Nat, F.F64, u => SF.round_u(s, m, x, u), Nat.max(A, 1926n), 1926n, emax)
106	      # the pick reduces under pack's argument, so the checker never unfolds pack
107	      +e3p = Equal.cong(Bool, Nat, b => SF.pick(Nat, b, SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m)), Nat.is_le(x, 1926n), True{}, hxa)
108	      +e3 = Equal.cong(Nat, F.F64, t => SF.pack(s, t, 1926n), SF.pick(Nat, Nat.is_le(x, 1926n), SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m)), SF.rne(m, Nat.sub(1926n, x)), e3p)
109	      +e4 = Equal.cong(Nat, F.F64, t => SF.pack(s, SF.rne(m, t), 1926n), Nat.sub(1926n, x), 1n+j, N.sub_succ_left(1925n, x, hxb))
110	      +e5 = Equal.cong(Nat, F.F64, t => SF.pack(s, t, 1926n), SF.rne(m, 1n+j), 0n, rne_zero(m, j, hm, hj))
111	      +e6 = FR.enc_bits(s, 0n, 0n)
112	      +r1 = SF.round_u(s, m, x, Nat.max(A, 1926n))
113	      +r2 = SF.round_u(s, m, x, 1926n)
114	      +r3 = SF.pack(s, SF.rne(m, Nat.sub(1926n, x)), 1926n)
115	      +r4 = SF.pack(s, SF.rne(m, 1n+j), 1926n)
116	      +r5 = SF.pack(s, 0n, 1926n)
117	      +r6 = FR.bits(s, 0n)
118	      +r2p = SF.pack(s, SF.pick(Nat, Nat.is_le(x, 1926n), SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m)), 1926n)
119	      Equal.trans(F.F64, SF.round(s, m, x), r1, SF.zero(s), e1, Equal.trans(F.F64, r1, r2, SF.zero(s), e2, Equal.trans(F.F64, r2, r2p, SF.zero(s), ru(s, m, x, 1926n), Equal.trans(F.F64, r2p, r3, SF.zero(s), e3, Equal.trans(F.F64, r3, r4, SF.zero(s), e4, Equal.trans(F.F64, r4, r5, SF.zero(s), e5, Equal.trans(F.F64, r5, r6, SF.zero(s), e6, bz(s))))))))
120	
121	def tiny(+s: Bool, +m: Nat, +x: Nat, +hm: {C.fits(53n, m) == True{} : Bool}, +hx: {Nat.is_lt(x, 63n) == True{} : Bool}) -> {SF.round(s, m, x) == SF.zero(s) : F.F64}:
122	  tiny_c(s, m, x, hm, hx, Nat.is_eq(m, 0n), {==})
123	
124	# ---- frexp ----
125	
126	def ee_c(+t: Nat, +c: Bool) -> {F.exp_pick(t, c) == SF.pick(F.Exp, c, F.Exp{False{}, Nat.sub(t, 3000n)}, F.Exp{True{}, Nat.sub(3000n, t)}) : F.Exp}:
127	  match c:
128	    case True{}:
129	      {==}
130	    case False{}:
131	      {==}
132	
133	def exp_eq(+t: Nat) -> {F.exp_of(t) == SF.exp_of(t) : F.Exp}:
134	  ee_c(t, Nat.is_le(3000n, t))
135	
136	def FIN(+x: F.F64) -> F.F64 & F.Exp:
137	  (SF.round(SF.sign(x), SF.mant(x), Nat.sub(SF.zb(), M.bit_length(SF.mant(x)))), SF.exp_of(Nat.add(SF.xexp(x), M.bit_length(SF.mant(x)))))
138	
139	def fx_nz(+x: F.F64) -> {F.fx_fin(x, F.dmant(x), Nat.sub(64n, X.clz(F.dmant(x)))) == FIN(x) : F.F64 & F.Exp}:
140	  +w = F.dmant(x)
141	  +V = SW.value(w)
142	  +B = M.bit_length(V)
143	  +hB = BL.bl_le(53n, V, T.mw53(x), Nat.is_le(B, 53n), {==})
144	  +eb = Equal.trans(Nat, Nat.sub(64n, X.clz(w)), Nat.sub(64n, Nat.sub(64n, B)), B, Equal.cong(Nat, Nat, t => Nat.sub(64n, t), X.clz(w), Nat.sub(64n, B), CZ.clz_value(w)), T.subsub(64n, B, N.le_trans(B, 53n, 64n, hB, {==})))
145	  +e0 = Equal.cong(Nat, F.F64 & F.Exp, b => F.fx_fin(x, w, b), Nat.sub(64n, X.clz(w)), B, eb)
146	  +hx = RT.le_sub(63n, B, 3000n, N.le_trans(B, 53n, 2937n, BL.bl_le(53n, V, T.mw53(x), Nat.is_le(B, 53n), {==}), {==}))
147	  +a1 = T.rw_value(F.signbit(x), Nat.sub(3000n, B), w, hx)
148	  +a2 = Equal.cong(Bool, F.F64, t => SF.round(t, V, Nat.sub(3000n, B)), F.signbit(x), SF.sign(x), FB.signbit_value(x))
149	  +a3 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), t, Nat.sub(3000n, M.bit_length(t))), V, SF.mant(x), T.dmant_value(x))
150	  +A0 = F.round_w(F.signbit(x), Nat.sub(3000n, B), w)
151	  +A1 = SF.round(F.signbit(x), V, Nat.sub(3000n, B))
152	  +A2 = SF.round(SF.sign(x), V, Nat.sub(3000n, B))
153	  +A3 = SF.round(SF.sign(x), SF.mant(x), Nat.sub(SF.zb(), M.bit_length(SF.mant(x))))
154	  +ea = Equal.trans(F.F64, A0, A1, A3, a1, Equal.trans(F.F64, A1, A2, A3, a2, a3))
155	  +b1 = exp_eq(Nat.add(F.dexp(x), B))
156	  +b2 = Equal.cong(Nat, F.Exp, t => SF.exp_of(Nat.add(t, B)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
157	  +b3 = Equal.cong(Nat, F.Exp, t => SF.exp_of(Nat.add(SF.xexp(x), M.bit_length(t))), V, SF.mant(x), T.dmant_value(x))
158	  +B0 = F.exp_of(Nat.add(F.dexp(x), B))
159	  +B1 = SF.exp_of(Nat.add(F.dexp(x), B))
160	  +B2 = SF.exp_of(Nat.add(SF.xexp(x), B))
161	  +B3 = SF.exp_of(Nat.add(SF.xexp(x), M.bit_length(SF.mant(x))))
162	  +eb2 = Equal.trans(F.Exp, B0, B1, B3, b1, Equal.trans(F.Exp, B1, B2, B3, b2, b3))
163	  +p1 = Equal.cong(F.F64, F.F64 & F.Exp, t => (t, B0), A0, A3, ea)
164	  +p2 = Equal.cong(F.Exp, F.F64 & F.Exp, t => (A3, t), B0, B3, eb2)
165	  Equal.trans(F.F64 & F.Exp, F.fx_fin(x, w, Nat.sub(64n, X.clz(w))), F.fx_fin(x, w, B), FIN(x), e0, Equal.trans(F.F64 & F.Exp, (A0, B0), (A3, B0), FIN(x), p1, p2))
166	
167	def fxz_c(+x: F.F64, +iz: Bool) -> {F.fx_z(x, iz) == SF.pickt(F.F64 & F.Exp, iz, (x, F.Exp{False{}, 0n}), FIN(x)) : F.F64 & F.Exp}:
168	  match iz:
169	    case True{}:
170	      {==}
171	    case False{}:
172	      fx_nz(x)
173	
174	def fx_c(+x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {F.fx_cls(x, t) == SF.pickt(F.F64 & F.Exp, Bool.and(t, Bool.not(z)), (SF.qnan(), F.Exp{False{}, 0n}), SF.pickt(F.F64 & F.Exp, Bool.or(Bool.and(t, z), SF.is_zero(x)), (x, F.Exp{False{}, 0n}), FIN(x))) : F.F64 & F.Exp}:
175	  match t z:
176	    case True{} True{}:
177	      Equal.cong(Bool, F.F64 & F.Exp, b => (F.nan_or(x, Bool.not(b)), F.Exp{False{}, 0n}), X.is_zero(F.frac(x)), True{}, hz)
178	    case True{} False{}:
179	      Equal.cong(Bool, F.F64 & F.Exp, b => (F.nan_or(x, Bool.not(b)), F.Exp{False{}, 0n}), X.is_zero(F.frac(x)), False{}, hz)
180	    case False{} _:
181	      +e1 = Equal.cong(Bool, F.F64 & F.Exp, b => F.fx_z(x, b), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x))
182	      Equal.trans(F.F64 & F.Exp, F.fx_z(x, F.is_zero(x)), F.fx_z(x, SF.is_zero(x)), SF.pickt(F.F64 & F.Exp, SF.is_zero(x), (x, F.Exp{False{}, 0n}), FIN(x)), e1, fxz_c(x, SF.is_zero(x)))
183	
184	def frexp_value(+x: F.F64) -> SF.Frexp.value(x):
185	  +e1 = Equal.cong(Nat, F.F64 & F.Exp, u => F.fx_cls(x, Nat.is_eq(u, 2047n)), F.exp_field(x), SF.efield(x), T.ea(x))
186	  Equal.trans(F.F64 & F.Exp, F.frexp(x), F.fx_cls(x, Nat.is_eq(SF.efield(x), 2047n)), SF.frexp(x), e1, fx_c(x, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x)))
187	
188	# ---- ldexp ----
189	
190	def LD(+x: F.F64, +neg: Bool, +k: Nat) -> F.F64:
191	  SF.round(SF.sign(x), SF.mant(x), SF.pick(Nat, neg, Nat.sub(SF.xexp(x), k), Nat.add(SF.xexp(x), k)))
192	
193	# the round_w of the significand at scale u is the spec's round at u
194	def rwx(+x: F.F64, +u: Nat, +hu: {Nat.is_le(63n, u) == True{} : Bool}) -> {F.round_w(F.signbit(x), u, F.dmant(x)) == SF.round(SF.sign(x), SF.mant(x), u) : F.F64}:
195	  +a1 = T.rw_value(F.signbit(x), u, F.dmant(x), hu)
196	  +a2 = Equal.cong(Bool, F.F64, t => SF.round(t, SW.value(F.dmant(x)), u), F.signbit(x), SF.sign(x), FB.signbit_value(x))
197	  +a3 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), t, u), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x))
198	  Equal.trans(F.F64, F.round_w(F.signbit(x), u, F.dmant(x)), SF.round(F.signbit(x), SW.value(F.dmant(x)), u), SF.round(SF.sign(x), SF.mant(x), u), a1, Equal.trans(F.F64, SF.round(F.signbit(x), SW.value(F.dmant(x)), u), SF.round(SF.sign(x), SW.value(F.dmant(x)), u), SF.round(SF.sign(x), SF.mant(x), u), a2, a3))
199	
200	# a - k < 63 when a < k + 63
201	def slt(+a: Nat, +k: Nat, +h: {Nat.is_lt(a, Nat.add(k, 63n)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a, k), 63n) == True{} : Bool}:
202	  match a k:
203	    case 0n 0n:
204	      {==}
205	    case 0n 1n+ +kp:
206	      {==}
207	    case 1n+ +ap 0n:
208	      h
209	    case 1n+ +ap 1n+ +kp:
210	      slt(ap, kp, h)
211	
212	def ldn_c(+x: F.F64, +k: Nat, +c: Bool, +hc: {Nat.is_lt(F.dexp(x), Nat.add(k, 63n)) == c : Bool}) -> {F.ld_neg(x, k, c) == LD(x, True{}, k) : F.F64}:
213	  match c:
214	    case True{}:
215	      +h1 = L.subst(Nat, t => {Nat.is_lt(t, Nat.add(k, 63n)) == True{} : Bool}, F.dexp(x), SF.xexp(x), T.dexp_value(x), hc)
216	      +et = tiny(SF.sign(x), SF.mant(x), Nat.sub(SF.xexp(x), k), T.mant_fits(x), slt(SF.xexp(x), k, h1))
217	      +ez = Equal.trans(F.F64, F.zero(F.signbit(x)), SF.zero(F.signbit(x)), SF.zero(SF.sign(x)), T.zero_v(F.signbit(x)), Equal.cong(Bool, F.F64, t => SF.zero(t), F.signbit(x), SF.sign(x), FB.signbit_value(x)))
218	      Equal.trans(F.F64, F.zero(F.signbit(x)), SF.zero(SF.sign(x)), LD(x, True{}, k), ez, Equal.sym(F.F64, LD(x, True{}, k), SF.zero(SF.sign(x)), et))
219	    case False{}:
220	      +h0 = N.not_lt_le(F.dexp(x), Nat.add(k, 63n), hc)
221	      +h1 = L.subst(Nat, t => {Nat.is_le(t, F.dexp(x)) == True{} : Bool}, Nat.add(k, 63n), Nat.add(63n, k), NA.add_comm(k, 63n), h0)
222	      +hu = RT.le_sub(63n, k, F.dexp(x), h1)
223	      +e1 = rwx(x, Nat.sub(F.dexp(x), k), hu)
224	      +e2 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), SF.mant(x), Nat.sub(t, k)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
225	      Equal.trans(F.F64, F.round_w(F.signbit(x), Nat.sub(F.dexp(x), k), F.dmant(x)), SF.round(SF.sign(x), SF.mant(x), Nat.sub(F.dexp(x), k)), LD(x, True{}, k), e1, e2)
226	
227	def ldf_c(+x: F.F64, +neg: Bool, +k: Nat) -> {F.ld_fin(x, neg, k) == LD(x, neg, k) : F.F64}:
228	  match neg:
229	    case True{}:
230	      ldn_c(x, k, Nat.is_lt(F.dexp(x), Nat.add(k, 63n)), {==})
231	    case False{}:
232	      +hu = N.le_trans(63n, F.dexp(x), Nat.add(F.dexp(x), k), T.dexp_ge(x), N.le_add_right(F.dexp(x), k))
233	      +e1 = rwx(x, Nat.add(F.dexp(x), k), hu)
234	      +e2 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), SF.mant(x), Nat.add(t, k)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
235	      Equal.trans(F.F64, F.round_w(F.signbit(x), Nat.add(F.dexp(x), k), F.dmant(x)), SF.round(SF.sign(x), SF.mant(x), Nat.add(F.dexp(x), k)), LD(x, False{}, k), e1, e2)
236	
237	def ldz_c(+x: F.F64, +neg: Bool, +k: Nat, +iz: Bool) -> {F.ld_z(x, F.Exp{neg, k}, iz) == SF.pick(F.F64, iz, x, LD(x, neg, k)) : F.F64}:
238	  match iz:
239	    case True{}:
240	      {==}
241	    case False{}:
242	      ldf_c(x, neg, k)
243	
244	def ld_c(+x: F.F64, +neg: Bool, +k: Nat, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {F.ld_cls(x, F.Exp{neg, k}, t) == SF.pick(F.F64, Bool.and(t, Bool.not(z)), SF.qnan(), SF.pick(F.F64, Bool.or(Bool.and(t, z), SF.is_zero(x)), x, LD(x, neg, k))) : F.F64}:
245	  match t z:
246	    case True{} True{}:
247	      Equal.cong(Bool, F.F64, b => F.nan_or(x, Bool.not(b)), X.is_zero(F.frac(x)), True{}, hz)
248	    case True{} False{}:
249	      Equal.cong(Bool, F.F64, b => F.nan_or(x, Bool.not(b)), X.is_zero(F.frac(x)), False{}, hz)
250	    case False{} _:
251	      +e1 = Equal.cong(Bool, F.F64, b => F.ld_z(x, F.Exp{neg, k}, b), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x))
252	      Equal.trans(F.F64, F.ld_z(x, F.Exp{neg, k}, F.is_zero(x)), F.ld_z(x, F.Exp{neg, k}, SF.is_zero(x)), SF.pick(F.F64, SF.is_zero(x), x, LD(x, neg, k)), e1, ldz_c(x, neg, k, SF.is_zero(x)))
253	
254	def ldexp_value(+x: F.F64, +neg: Bool, +k: Nat) -> SF.Ldexp.value(x, neg, k):
255	  +e1 = Equal.cong(Nat, F.F64, u => F.ld_cls(x, F.Exp{neg, k}, Nat.is_eq(u, 2047n)), F.exp_field(x), SF.efield(x), T.ea(x))
256	  Equal.trans(F.F64, F.ldexp(x, F.Exp{neg, k}), F.ld_cls(x, F.Exp{neg, k}, Nat.is_eq(SF.efield(x), 2047n)), SF.ldexp(x, neg, k), e1, ld_c(x, neg, k, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x)))