1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/f64.bend as SF 4 import ../../../src/math/f64.bend as F 5 import ../../../src/math/w64.bend as X 6 import ../../../src/math/u64.bend as WU 7 import ../../lib/nat.bend as N 8 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 9 import ./u32laws.bend as LW 10 import ./f64bits.bend as FB 11 import ./f64round.bend as FR 12 13 # Mul.value of spec/math/f64.bend: the special-case analysis. 14 15 def v(+x: U32) -> Nat: 16 U32.to_nat(x) 17 18 # ---- fields of the operands ---- 19 20 def 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 23 def 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 26 def 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 29 def 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 36 def zero_v(+s: Bool) -> {F.zero(s) == SF.zero(s) : F.F64}: 37 match s: 38 case True{}: 39 {==} 40 case False{}: 41 {==} 42 43 def 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 50 def 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 57 def 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 64 def 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 71 def 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 75 def 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 78 def 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 82 def 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