def dcase

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divc.bend:150

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

150def 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}:
151  match a1 b1 c1 a2 b2 c2:
152    case True{} True{} True{} True{} True{} True{}:
153      {==}
154    case True{} True{} True{} True{} True{} False{}:
155      {==}
156    case True{} True{} True{} True{} False{} True{}:
157      {==}
158    case True{} True{} True{} True{} False{} False{}:
159      {==}
160    case True{} True{} True{} False{} True{} True{}:
161      FR.inf_v(s)
162    case True{} True{} True{} False{} True{} False{}:
163      FR.inf_v(s)
164    case True{} True{} True{} False{} False{} True{}:
165      FR.inf_v(s)
166    case True{} True{} True{} False{} False{} False{}:
167      FR.inf_v(s)
168    case True{} True{} False{} True{} True{} True{}:
169      {==}
170    case True{} True{} False{} True{} True{} False{}:
171      {==}
172    case True{} True{} False{} True{} False{} True{}:
173      {==}
174    case True{} True{} False{} True{} False{} False{}:
175      {==}
176    case True{} True{} False{} False{} True{} True{}:
177      FR.inf_v(s)
178    case True{} True{} False{} False{} True{} False{}:
179      FR.inf_v(s)
180    case True{} True{} False{} False{} False{} True{}:
181      FR.inf_v(s)
182    case True{} True{} False{} False{} False{} False{}:
183      FR.inf_v(s)
184    case True{} False{} True{} True{} True{} True{}:
185      {==}
186    case True{} False{} True{} True{} True{} False{}:
187      {==}
188    case True{} False{} True{} True{} False{} True{}:
189      {==}
190    case True{} False{} True{} True{} False{} False{}:
191      {==}
192    case True{} False{} True{} False{} True{} True{}:
193      {==}
194    case True{} False{} True{} False{} True{} False{}:
195      {==}
196    case True{} False{} True{} False{} False{} True{}:
197      {==}
198    case True{} False{} True{} False{} False{} False{}:
199      {==}
200    case True{} False{} False{} True{} True{} True{}:
201      {==}
202    case True{} False{} False{} True{} True{} False{}:
203      {==}
204    case True{} False{} False{} True{} False{} True{}:
205      {==}
206    case True{} False{} False{} True{} False{} False{}:
207      {==}
208    case True{} False{} False{} False{} True{} True{}:
209      {==}
210    case True{} False{} False{} False{} True{} False{}:
211      {==}
212    case True{} False{} False{} False{} False{} True{}:
213      {==}
214    case True{} False{} False{} False{} False{} False{}:
215      {==}
216    case False{} True{} True{} True{} True{} True{}:
217      zero_v(s)
218    case False{} True{} True{} True{} True{} False{}:
219      zero_v(s)
220    case False{} True{} True{} True{} False{} True{}:
221      {==}
222    case False{} True{} True{} True{} False{} False{}:
223      {==}
224    case False{} True{} True{} False{} True{} True{}:
225      {==}
226    case False{} True{} True{} False{} True{} False{}:
227      hZ
228    case False{} True{} True{} False{} False{} True{}:
229      hZ
230    case False{} True{} True{} False{} False{} False{}:
231      hZ
232    case False{} True{} False{} True{} True{} True{}:
233      zero_v(s)
234    case False{} True{} False{} True{} True{} False{}:
235      zero_v(s)
236    case False{} True{} False{} True{} False{} True{}:
237      {==}
238    case False{} True{} False{} True{} False{} False{}:
239      {==}
240    case False{} True{} False{} False{} True{} True{}:
241      FR.inf_v(s)
242    case False{} True{} False{} False{} True{} False{}:
243      hR
244    case False{} True{} False{} False{} False{} True{}:
245      hR
246    case False{} True{} False{} False{} False{} False{}:
247      hR
248    case False{} False{} True{} True{} True{} True{}:
249      zero_v(s)
250    case False{} False{} True{} True{} True{} False{}:
251      zero_v(s)
252    case False{} False{} True{} True{} False{} True{}:
253      {==}
254    case False{} False{} True{} True{} False{} False{}:
255      {==}
256    case False{} False{} True{} False{} True{} True{}:
257      FR.inf_v(s)
258    case False{} False{} True{} False{} True{} False{}:
259      hR
260    case False{} False{} True{} False{} False{} True{}:
261      hR
262    case False{} False{} True{} False{} False{} False{}:
263      hR
264    case False{} False{} False{} True{} True{} True{}:
265      zero_v(s)
266    case False{} False{} False{} True{} True{} False{}:
267      zero_v(s)
268    case False{} False{} False{} True{} False{} True{}:
269      {==}
270    case False{} False{} False{} True{} False{} False{}:
271      {==}
272    case False{} False{} False{} False{} True{} True{}:
273      FR.inf_v(s)
274    case False{} False{} False{} False{} True{} False{}:
275      hR
276    case False{} False{} False{} False{} False{} True{}:
277      hR
278    case False{} False{} False{} False{} False{} False{}:
279      hR