proofs/math/typed/f64mulc.bend
bend-collections-laws-math@1.0.0.0 · 212 lines · 14 definitions
1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
4import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
5import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
6import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
7import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
10import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
12
13
14
15def v(+x: U32) -> Nat:
16 U32.to_nat(x)
17
18
19
20def hea(+xl: U32, +xh: U32) -> {F.exp_field(F.Bits{xl, xh}) == SF.efield(F.Bits{xl, xh}) : Nat}:
21 FB.ef_g(1n, {==}, xh, 1048576, {==}, 2047, {==})
22
23def mimpl(+s: Bool, +a1: Bool, +b1: Bool, +c1: Bool, +a2: Bool, +b2: Bool, +c2: Bool, +r: F.F64) -> F.F64:
24 SF.pick(F.F64, a1, SF.pick(F.F64, Bool.or(Bool.or(Bool.not(b1), Bool.and(a2, Bool.not(b2))), Bool.and(c2, b2)), F.nan(), F.inf(s)), SF.pick(F.F64, a2, SF.pick(F.F64, Bool.or(Bool.not(b2), Bool.and(c1, b1)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.or(Bool.and(c1, b1), Bool.and(c2, b2)), F.zero(s), r)))
25
26def mspec(+s: Bool, +a1: Bool, +b1: Bool, +c1: Bool, +a2: Bool, +b2: Bool, +c2: Bool, +r: F.F64) -> F.F64:
27 SF.pick(F.F64, Bool.or(Bool.and(a1, Bool.not(b1)), Bool.and(a2, Bool.not(b2))), SF.qnan(), SF.pick(F.F64, Bool.or(Bool.and(a1, b1), Bool.and(a2, b2)), SF.pick(F.F64, Bool.or(Bool.and(c1, b1), Bool.and(c2, b2)), SF.qnan(), SF.inf(s)), r))
28
29def ion(+s: Bool, +b: Bool) -> {F.inf_or_nan(s, b) == SF.pick(F.F64, b, F.nan(), F.inf(s)) : F.F64}:
30 match b:
31 case True{}:
32 Equal.trans(F.F64, F.inf_or_nan(s, True{}), F.nan(), SF.pick(F.F64, True{}, F.nan(), F.inf(s)), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.nan(), F.inf(s)), F.nan(), FR.pk_t(F.F64, F.nan(), F.inf(s))))
33 case False{}:
34 Equal.trans(F.F64, F.inf_or_nan(s, False{}), F.inf(s), SF.pick(F.F64, False{}, F.nan(), F.inf(s)), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.nan(), F.inf(s)), F.inf(s), FR.pk_f(F.F64, F.nan(), F.inf(s))))
35
36def zero_v(+s: Bool) -> {F.zero(s) == SF.zero(s) : F.F64}:
37 match s:
38 case True{}:
39 {==}
40 case False{}:
41 {==}
42
43def ne2047(+E: Nat) -> {Bool.and(Nat.is_eq(E, 2047n), Nat.is_eq(E, 0n)) == False{} : Bool}:
44 match E:
45 case 0n:
46 {==}
47 case 1n+ +p:
48 FR.and_f(Nat.is_eq(1n+p, 2047n))
49
50def sh3(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +z: Bool) -> {F.mul_z(s, ea, fa, eb, fb, z) == SF.pick(F.F64, z, F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))) : F.F64}:
51 match z:
52 case True{}:
53 Equal.trans(F.F64, F.mul_z(s, ea, fa, eb, fb, True{}), F.zero(s), SF.pick(F.F64, True{}, F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), F.zero(s), FR.pk_t(F.F64, F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))))
54 case False{}:
55 Equal.trans(F.F64, F.mul_z(s, ea, fa, eb, fb, False{}), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)), SF.pick(F.F64, False{}, F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)), FR.pk_f(F.F64, F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))))
56
57def sh2(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +t: Bool) -> {F.mul_b(s, ea, fa, eb, fb, t) == SF.pick(F.F64, t, SF.pick(F.F64, Bool.or(Bool.not(X.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.or(Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))) : F.F64}:
58 match t:
59 case True{}:
60 Equal.trans(F.F64, F.mul_b(s, ea, fa, eb, fb, True{}), SF.pick(F.F64, Bool.or(Bool.not(X.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), F.nan(), F.inf(s)), SF.pick(F.F64, True{}, SF.pick(F.F64, Bool.or(Bool.not(X.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.or(Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), ion(s, Bool.or(Bool.not(X.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)))), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.pick(F.F64, Bool.or(Bool.not(X.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.or(Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), SF.pick(F.F64, Bool.or(Bool.not(X.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), F.nan(), F.inf(s)), FR.pk_t(F.F64, SF.pick(F.F64, Bool.or(Bool.not(X.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.or(Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))))
61 case False{}:
62 Equal.trans(F.F64, F.mul_b(s, ea, fa, eb, fb, False{}), SF.pick(F.F64, Bool.or(Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), SF.pick(F.F64, False{}, SF.pick(F.F64, Bool.or(Bool.not(X.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.or(Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), sh3(s, ea, fa, eb, fb, Bool.or(Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)))), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.pick(F.F64, Bool.or(Bool.not(X.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.or(Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), SF.pick(F.F64, Bool.or(Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), FR.pk_f(F.F64, SF.pick(F.F64, Bool.or(Bool.not(X.is_zero(fb)), Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.or(Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), F.zero(s), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))))
63
64def sh1(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +t: Bool) -> {F.mul_cls(s, ea, fa, eb, fb, t) == mimpl(s, t, X.is_zero(fa), Nat.is_eq(ea, 0n), Nat.is_eq(eb, 2047n), X.is_zero(fb), Nat.is_eq(eb, 0n), F.mul_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))) : F.F64}:
65 match t:
66 case True{}:
67 ion(s, Bool.or(Bool.or(Bool.not(X.is_zero(fa)), Bool.and(Nat.is_eq(eb, 2047n), Bool.not(X.is_zero(fb)))), Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))))
68 case False{}:
69 sh2(s, ea, fa, eb, fb, Nat.is_eq(eb, 2047n))
70
71def mant0(+xl: U32, +xh: U32, +hc: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n) == True{} : Bool}, +hb: {Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n) == True{} : Bool}) -> {SF.mant(F.Bits{xl, xh}) == 0n : Nat}:
72 +e1 = Equal.cong(Bool, Nat, t => Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.b2n(Bool.not(t)))), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), True{}, hc)
73 Equal.trans(Nat, SF.mant(F.Bits{xl, xh}), Nat.add(SF.frac(F.Bits{xl, xh}), 0n), 0n, e1, Equal.trans(Nat, Nat.add(SF.frac(F.Bits{xl, xh}), 0n), SF.frac(F.Bits{xl, xh}), 0n, N.add_zero(SF.frac(F.Bits{xl, xh})), N.eq_from_is_eq(SF.frac(F.Bits{xl, xh}), 0n, hb)))
74
75def zx(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +hc: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n) == True{} : Bool}, +hb: {Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n) == True{} : Bool}) -> {F.zero(s) == SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())) : F.F64}:
76 Equal.trans(F.F64, F.zero(s), SF.zero(s), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), zero_v(s), Equal.sym(F.F64, SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), SF.zero(s), Equal.cong(Nat, F.F64, z => SF.round(s, Nat.mul(z, SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), SF.mant(F.Bits{xl, xh}), 0n, mant0(xl, xh, hc, hb))))
77
78def zy(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +hc: {Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n) == True{} : Bool}, +hb: {Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n) == True{} : Bool}) -> {F.zero(s) == SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())) : F.F64}:
79 +em = Equal.trans(Nat, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.mul(SF.mant(F.Bits{xl, xh}), 0n), 0n, Equal.cong(Nat, Nat, z => Nat.mul(SF.mant(F.Bits{xl, xh}), z), SF.mant(F.Bits{yl, yh}), 0n, mant0(yl, yh, hc, hb)), NA.mul_zero(SF.mant(F.Bits{xl, xh})))
80 Equal.trans(F.F64, F.zero(s), SF.zero(s), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), zero_v(s), Equal.sym(F.F64, SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), SF.zero(s), Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), 0n, em)))
81
82def mcase(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +r1: F.F64, +r2: F.F64, +a1: Bool, +ha1: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n) == a1 : Bool}, +b1: Bool, +hb1: {Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n) == b1 : Bool}, +c1: Bool, +hc1: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n) == c1 : Bool}, +a2: Bool, +ha2: {Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n) == a2 : Bool}, +b2: Bool, +hb2: {Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n) == b2 : Bool}, +c2: Bool, +hc2: {Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n) == c2 : Bool}, +hR: {SF.pick(F.F64, Bool.or(Bool.or(a1, a2), Bool.or(Bool.and(c1, b1), Bool.and(c2, b2))), r2, r1) == r2 : F.F64}, +hZ: {SF.pick(F.F64, Bool.or(Bool.or(a1, a2), Bool.not(Bool.or(Bool.and(c1, b1), Bool.and(c2, b2)))), r2, F.zero(s)) == r2 : F.F64}) -> {mimpl(s, a1, b1, c1, a2, b2, c2, r1) == mspec(s, a1, b1, c1, a2, b2, c2, r2) : F.F64}:
83 match a1 b1 c1 a2 b2 c2:
84 case True{} True{} True{} True{} True{} True{}:
85 Empty.absurd({mimpl(s, True{}, True{}, True{}, True{}, True{}, True{}, r1) == mspec(s, True{}, True{}, True{}, True{}, True{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
86 case True{} True{} True{} True{} True{} False{}:
87 Empty.absurd({mimpl(s, True{}, True{}, True{}, True{}, True{}, False{}, r1) == mspec(s, True{}, True{}, True{}, True{}, True{}, False{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
88 case True{} True{} True{} True{} False{} True{}:
89 Empty.absurd({mimpl(s, True{}, True{}, True{}, True{}, False{}, True{}, r1) == mspec(s, True{}, True{}, True{}, True{}, False{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
90 case True{} True{} True{} True{} False{} False{}:
91 Empty.absurd({mimpl(s, True{}, True{}, True{}, True{}, False{}, False{}, r1) == mspec(s, True{}, True{}, True{}, True{}, False{}, False{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
92 case True{} True{} True{} False{} True{} True{}:
93 Empty.absurd({mimpl(s, True{}, True{}, True{}, False{}, True{}, True{}, r1) == mspec(s, True{}, True{}, True{}, False{}, True{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
94 case True{} True{} True{} False{} True{} False{}:
95 Empty.absurd({mimpl(s, True{}, True{}, True{}, False{}, True{}, False{}, r1) == mspec(s, True{}, True{}, True{}, False{}, True{}, False{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
96 case True{} True{} True{} False{} False{} True{}:
97 Empty.absurd({mimpl(s, True{}, True{}, True{}, False{}, False{}, True{}, r1) == mspec(s, True{}, True{}, True{}, False{}, False{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
98 case True{} True{} True{} False{} False{} False{}:
99 Empty.absurd({mimpl(s, True{}, True{}, True{}, False{}, False{}, False{}, r1) == mspec(s, True{}, True{}, True{}, False{}, False{}, False{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
100 case True{} True{} False{} True{} True{} True{}:
101 Empty.absurd({mimpl(s, True{}, True{}, False{}, True{}, True{}, True{}, r1) == mspec(s, True{}, True{}, False{}, True{}, True{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
102 case True{} True{} False{} True{} True{} False{}:
103 FR.inf_v(s)
104 case True{} True{} False{} True{} False{} True{}:
105 Empty.absurd({mimpl(s, True{}, True{}, False{}, True{}, False{}, True{}, r1) == mspec(s, True{}, True{}, False{}, True{}, False{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
106 case True{} True{} False{} True{} False{} False{}:
107 {==}
108 case True{} True{} False{} False{} True{} True{}:
109 {==}
110 case True{} True{} False{} False{} True{} False{}:
111 FR.inf_v(s)
112 case True{} True{} False{} False{} False{} True{}:
113 FR.inf_v(s)
114 case True{} True{} False{} False{} False{} False{}:
115 FR.inf_v(s)
116 case True{} False{} True{} True{} True{} True{}:
117 Empty.absurd({mimpl(s, True{}, False{}, True{}, True{}, True{}, True{}, r1) == mspec(s, True{}, False{}, True{}, True{}, True{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
118 case True{} False{} True{} True{} True{} False{}:
119 Empty.absurd({mimpl(s, True{}, False{}, True{}, True{}, True{}, False{}, r1) == mspec(s, True{}, False{}, True{}, True{}, True{}, False{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
120 case True{} False{} True{} True{} False{} True{}:
121 Empty.absurd({mimpl(s, True{}, False{}, True{}, True{}, False{}, True{}, r1) == mspec(s, True{}, False{}, True{}, True{}, False{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
122 case True{} False{} True{} True{} False{} False{}:
123 Empty.absurd({mimpl(s, True{}, False{}, True{}, True{}, False{}, False{}, r1) == mspec(s, True{}, False{}, True{}, True{}, False{}, False{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
124 case True{} False{} True{} False{} True{} True{}:
125 Empty.absurd({mimpl(s, True{}, False{}, True{}, False{}, True{}, True{}, r1) == mspec(s, True{}, False{}, True{}, False{}, True{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
126 case True{} False{} True{} False{} True{} False{}:
127 Empty.absurd({mimpl(s, True{}, False{}, True{}, False{}, True{}, False{}, r1) == mspec(s, True{}, False{}, True{}, False{}, True{}, False{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
128 case True{} False{} True{} False{} False{} True{}:
129 Empty.absurd({mimpl(s, True{}, False{}, True{}, False{}, False{}, True{}, r1) == mspec(s, True{}, False{}, True{}, False{}, False{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
130 case True{} False{} True{} False{} False{} False{}:
131 Empty.absurd({mimpl(s, True{}, False{}, True{}, False{}, False{}, False{}, r1) == mspec(s, True{}, False{}, True{}, False{}, False{}, False{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1), hc1)), ne2047(SF.efield(F.Bits{xl, xh})))))
132 case True{} False{} False{} True{} True{} True{}:
133 Empty.absurd({mimpl(s, True{}, False{}, False{}, True{}, True{}, True{}, r1) == mspec(s, True{}, False{}, False{}, True{}, True{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
134 case True{} False{} False{} True{} True{} False{}:
135 {==}
136 case True{} False{} False{} True{} False{} True{}:
137 Empty.absurd({mimpl(s, True{}, False{}, False{}, True{}, False{}, True{}, r1) == mspec(s, True{}, False{}, False{}, True{}, False{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
138 case True{} False{} False{} True{} False{} False{}:
139 {==}
140 case True{} False{} False{} False{} True{} True{}:
141 {==}
142 case True{} False{} False{} False{} True{} False{}:
143 {==}
144 case True{} False{} False{} False{} False{} True{}:
145 {==}
146 case True{} False{} False{} False{} False{} False{}:
147 {==}
148 case False{} True{} True{} True{} True{} True{}:
149 Empty.absurd({mimpl(s, False{}, True{}, True{}, True{}, True{}, True{}, r1) == mspec(s, False{}, True{}, True{}, True{}, True{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
150 case False{} True{} True{} True{} True{} False{}:
151 {==}
152 case False{} True{} True{} True{} False{} True{}:
153 Empty.absurd({mimpl(s, False{}, True{}, True{}, True{}, False{}, True{}, r1) == mspec(s, False{}, True{}, True{}, True{}, False{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
154 case False{} True{} True{} True{} False{} False{}:
155 {==}
156 case False{} True{} True{} False{} True{} True{}:
157 hZ
158 case False{} True{} True{} False{} True{} False{}:
159 hZ
160 case False{} True{} True{} False{} False{} True{}:
161 hZ
162 case False{} True{} True{} False{} False{} False{}:
163 hZ
164 case False{} True{} False{} True{} True{} True{}:
165 Empty.absurd({mimpl(s, False{}, True{}, False{}, True{}, True{}, True{}, r1) == mspec(s, False{}, True{}, False{}, True{}, True{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
166 case False{} True{} False{} True{} True{} False{}:
167 FR.inf_v(s)
168 case False{} True{} False{} True{} False{} True{}:
169 Empty.absurd({mimpl(s, False{}, True{}, False{}, True{}, False{}, True{}, r1) == mspec(s, False{}, True{}, False{}, True{}, False{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
170 case False{} True{} False{} True{} False{} False{}:
171 {==}
172 case False{} True{} False{} False{} True{} True{}:
173 hZ
174 case False{} True{} False{} False{} True{} False{}:
175 hR
176 case False{} True{} False{} False{} False{} True{}:
177 hR
178 case False{} True{} False{} False{} False{} False{}:
179 hR
180 case False{} False{} True{} True{} True{} True{}:
181 Empty.absurd({mimpl(s, False{}, False{}, True{}, True{}, True{}, True{}, r1) == mspec(s, False{}, False{}, True{}, True{}, True{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
182 case False{} False{} True{} True{} True{} False{}:
183 FR.inf_v(s)
184 case False{} False{} True{} True{} False{} True{}:
185 Empty.absurd({mimpl(s, False{}, False{}, True{}, True{}, False{}, True{}, r1) == mspec(s, False{}, False{}, True{}, True{}, False{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
186 case False{} False{} True{} True{} False{} False{}:
187 {==}
188 case False{} False{} True{} False{} True{} True{}:
189 hZ
190 case False{} False{} True{} False{} True{} False{}:
191 hR
192 case False{} False{} True{} False{} False{} True{}:
193 hR
194 case False{} False{} True{} False{} False{} False{}:
195 hR
196 case False{} False{} False{} True{} True{} True{}:
197 Empty.absurd({mimpl(s, False{}, False{}, False{}, True{}, True{}, True{}, r1) == mspec(s, False{}, False{}, False{}, True{}, True{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
198 case False{} False{} False{} True{} True{} False{}:
199 FR.inf_v(s)
200 case False{} False{} False{} True{} False{} True{}:
201 Empty.absurd({mimpl(s, False{}, False{}, False{}, True{}, False{}, True{}, r1) == mspec(s, False{}, False{}, False{}, True{}, False{}, True{}, r2) : F.F64}, LW.true_ne_false(Equal.trans(Bool, True{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), False{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), True{}, Equal.cong(Bool, Bool, z => Bool.and(z, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n)), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2), hc2)), ne2047(SF.efield(F.Bits{yl, yh})))))
202 case False{} False{} False{} True{} False{} False{}:
203 {==}
204 case False{} False{} False{} False{} True{} True{}:
205 hZ
206 case False{} False{} False{} False{} True{} False{}:
207 hR
208 case False{} False{} False{} False{} False{} True{}:
209 hR
210 case False{} False{} False{} False{} False{} False{}:
211 hR
212