def scase
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqc.bend:307
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend as F64sqc
import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
307def scase(+xl: U32, +xh: U32, +r1: F.F64, +r2: F.F64, +aq: Bool, +ha: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n) == aq : Bool}, +bq: Bool, +cq: Bool, +hc: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n) == cq : Bool}, +ngv: Bool, +hR: {SF.pick(F.F64, Bool.or(Bool.or(aq, Bool.and(cq, bq)), ngv), r2, r1) == r2 : F.F64}) -> {simpl(ngv, aq, bq, cq, F.Bits{xl, xh}, r1) == sspec(ngv, aq, bq, cq, F.Bits{xl, xh}, r2) : F.F64}:
308 match aq bq cq ngv:
309 case True{} True{} True{} True{}:
310 NC.absurd_tf({simpl(True{}, True{}, True{}, True{}, F.Bits{xl, xh}, r1) == sspec(True{}, True{}, True{}, True{}, F.Bits{xl, xh}, r2) : F.F64}, Equal.trans(Bool, False{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, 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)), False{}, ne2047(SF.efield(F.Bits{xl, xh}))), 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, t => Bool.and(t, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha), hc)))
311 case True{} True{} True{} False{}:
312 NC.absurd_tf({simpl(False{}, True{}, True{}, True{}, F.Bits{xl, xh}, r1) == sspec(False{}, True{}, True{}, True{}, F.Bits{xl, xh}, r2) : F.F64}, Equal.trans(Bool, False{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, 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)), False{}, ne2047(SF.efield(F.Bits{xl, xh}))), 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, t => Bool.and(t, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha), hc)))
313 case True{} True{} False{} True{}:
314 {==}
315 case True{} True{} False{} False{}:
316 {==}
317 case True{} False{} True{} True{}:
318 NC.absurd_tf({simpl(True{}, True{}, False{}, True{}, F.Bits{xl, xh}, r1) == sspec(True{}, True{}, False{}, True{}, F.Bits{xl, xh}, r2) : F.F64}, Equal.trans(Bool, False{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, 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)), False{}, ne2047(SF.efield(F.Bits{xl, xh}))), 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, t => Bool.and(t, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha), hc)))
319 case True{} False{} True{} False{}:
320 NC.absurd_tf({simpl(False{}, True{}, False{}, True{}, F.Bits{xl, xh}, r1) == sspec(False{}, True{}, False{}, True{}, F.Bits{xl, xh}, r2) : F.F64}, Equal.trans(Bool, False{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, 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)), False{}, ne2047(SF.efield(F.Bits{xl, xh}))), 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, t => Bool.and(t, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha), hc)))
321 case True{} False{} False{} True{}:
322 {==}
323 case True{} False{} False{} False{}:
324 {==}
325 case False{} True{} True{} True{}:
326 {==}
327 case False{} True{} True{} False{}:
328 {==}
329 case False{} True{} False{} True{}:
330 {==}
331 case False{} True{} False{} False{}:
332 hR
333 case False{} False{} True{} True{}:
334 {==}
335 case False{} False{} True{} False{}:
336 hR
337 case False{} False{} False{} True{}:
338 {==}
339 case False{} False{} False{} False{}:
340 hR