F64divc.dcase: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divc.bend as F64divc
Lines 150-279 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divc.bend&start_line=150&end_line=279

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/f64round.bend as FR

def dcase(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +r1: F.F64, +r2: F.F64, +a1: Bool, +b1: Bool, +c1: Bool, +a2: Bool, +b2: Bool, +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.or(Bool.not(Bool.and(c1, b1)), Bool.and(c2, b2))), r2, F.zero(s)) == r2 : F.F64}) -> {dimpl(s, a1, b1, c1, a2, b2, c2, r1) == dspec(s, a1, b1, c1, a2, b2, c2, r2) : F.F64}:
  match a1 b1 c1 a2 b2 c2:
    case True{} True{} True{} True{} True{} True{}:
      {==}
    case True{} True{} True{} True{} True{} False{}:
      {==}
    case True{} True{} True{} True{} False{} True{}:
      {==}
    case True{} True{} True{} True{} False{} False{}:
      {==}
    case True{} True{} True{} False{} True{} True{}:
      FR.inf_v(s)
    case True{} True{} True{} False{} True{} False{}:
      FR.inf_v(s)
    case True{} True{} True{} False{} False{} True{}:
      FR.inf_v(s)
    case True{} True{} True{} False{} False{} False{}:
      FR.inf_v(s)
    case True{} True{} False{} True{} True{} True{}:
      {==}
    case True{} True{} False{} True{} True{} False{}:
      {==}
    case True{} True{} False{} True{} False{} True{}:
      {==}
    case True{} True{} False{} True{} False{} False{}:
      {==}
    case True{} True{} False{} False{} True{} True{}:
      FR.inf_v(s)
    case True{} True{} False{} False{} True{} False{}:
      FR.inf_v(s)
    case True{} True{} False{} False{} False{} True{}:
      FR.inf_v(s)
    case True{} True{} False{} False{} False{} False{}:
      FR.inf_v(s)
    case True{} False{} True{} True{} True{} True{}:
      {==}
    case True{} False{} True{} True{} True{} False{}:
      {==}
    case True{} False{} True{} True{} False{} True{}:
      {==}
    case True{} False{} True{} True{} False{} False{}:
      {==}
    case True{} False{} True{} False{} True{} True{}:
      {==}
    case True{} False{} True{} False{} True{} False{}:
      {==}
    case True{} False{} True{} False{} False{} True{}:
      {==}
    case True{} False{} True{} False{} False{} False{}:
      {==}
    case True{} False{} False{} True{} True{} True{}:
      {==}
    case True{} False{} False{} True{} True{} False{}:
      {==}
    case True{} False{} False{} True{} False{} True{}:
      {==}
    case True{} False{} False{} True{} False{} False{}:
      {==}
    case True{} False{} False{} False{} True{} True{}:
      {==}
    case True{} False{} False{} False{} True{} False{}:
      {==}
    case True{} False{} False{} False{} False{} True{}:
      {==}
    case True{} False{} False{} False{} False{} False{}:
      {==}
    case False{} True{} True{} True{} True{} True{}:
      zero_v(s)
    case False{} True{} True{} True{} True{} False{}:
      zero_v(s)
    case False{} True{} True{} True{} False{} True{}:
      {==}
    case False{} True{} True{} True{} False{} False{}:
      {==}
    case False{} True{} True{} False{} True{} True{}:
      {==}
    case False{} True{} True{} False{} True{} False{}:
      hZ
    case False{} True{} True{} False{} False{} True{}:
      hZ
    case False{} True{} True{} False{} False{} False{}:
      hZ
    case False{} True{} False{} True{} True{} True{}:
      zero_v(s)
    case False{} True{} False{} True{} True{} False{}:
      zero_v(s)
    case False{} True{} False{} True{} False{} True{}:
      {==}
    case False{} True{} False{} True{} False{} False{}:
      {==}
    case False{} True{} False{} False{} True{} True{}:
      FR.inf_v(s)
    case False{} True{} False{} False{} True{} False{}:
      hR
    case False{} True{} False{} False{} False{} True{}:
      hR
    case False{} True{} False{} False{} False{} False{}:
      hR
    case False{} False{} True{} True{} True{} True{}:
      zero_v(s)
    case False{} False{} True{} True{} True{} False{}:
      zero_v(s)
    case False{} False{} True{} True{} False{} True{}:
      {==}
    case False{} False{} True{} True{} False{} False{}:
      {==}
    case False{} False{} True{} False{} True{} True{}:
      FR.inf_v(s)
    case False{} False{} True{} False{} True{} False{}:
      hR
    case False{} False{} True{} False{} False{} True{}:
      hR
    case False{} False{} True{} False{} False{} False{}:
      hR
    case False{} False{} False{} True{} True{} True{}:
      zero_v(s)
    case False{} False{} False{} True{} True{} False{}:
      zero_v(s)
    case False{} False{} False{} True{} False{} True{}:
      {==}
    case False{} False{} False{} True{} False{} False{}:
      {==}
    case False{} False{} False{} False{} True{} True{}:
      FR.inf_v(s)
    case False{} False{} False{} False{} True{} False{}:
      hR
    case False{} False{} False{} False{} False{} True{}:
      hR
    case False{} False{} False{} False{} False{} False{}:
      hR

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divc.bend&name=dimpl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divc.bend&name=dspec
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divc.bend&name=zero_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=inf_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=zero