def tt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addv.bend:49

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

49def tt(+z1: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> {SF.pick(F.F64, Bool.not(Bool.xor(sx, sy)), F.nan_or(x, Bool.or(Bool.not(z1), Bool.not(z2))), F.nan()) == spec_g(True{}, z1, True{}, z2, sx, sy, x, y, fin) : F.F64}:
50  match z1 z2 sx sy:
51    case True{} True{} True{} True{}:
52      {==}
53    case True{} True{} True{} False{}:
54      {==}
55    case True{} True{} False{} True{}:
56      {==}
57    case True{} True{} False{} False{}:
58      {==}
59    case True{} False{} True{} True{}:
60      {==}
61    case True{} False{} True{} False{}:
62      {==}
63    case True{} False{} False{} True{}:
64      {==}
65    case True{} False{} False{} False{}:
66      {==}
67    case False{} True{} True{} True{}:
68      {==}
69    case False{} True{} True{} False{}:
70      {==}
71    case False{} True{} False{} True{}:
72      {==}
73    case False{} True{} False{} False{}:
74      {==}
75    case False{} False{} True{} True{}:
76      {==}
77    case False{} False{} True{} False{}:
78      {==}
79    case False{} False{} False{} True{}:
80      {==}
81    case False{} False{} False{} False{}:
82      {==}