def bits.bound_z
bend-osdev-caps@0.1.0.0 · PROOF.bend:289
import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C
289def bits.bound_z(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), Word.zero(n)), Word.or(n, b, Word.or(n, i, a))) == True{} : Bool}:
290 match n:
291 case 0n:
292 {==}
293 case 1n+n1:
294 match i fi fp b a:
295 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
296 bits.bound_z(n1, it, fit, fpt, bt, at)
297 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
298 bits.bound_z(n1, it, fit, fpt, bt, at)
299 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
300 bits.bound_z(n1, it, fit, fpt, bt, at)
301 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
302 bits.bound_z(n1, it, fit, fpt, bt, at)
303 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
304 bits.bound_z(n1, it, fit, fpt, bt, at)
305 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
306 bits.bound_z(n1, it, fit, fpt, bt, at)
307 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
308 bits.bound_z(n1, it, fit, fpt, bt, at)
309 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
310 bits.bound_z(n1, it, fit, fpt, bt, at)
311 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
312 bits.bound_z(n1, it, fit, fpt, bt, at)
313 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
314 bits.bound_z(n1, it, fit, fpt, bt, at)
315 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
316 bits.bound_z(n1, it, fit, fpt, bt, at)
317 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
318 bits.bound_z(n1, it, fit, fpt, bt, at)
319 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
320 bits.bound_z(n1, it, fit, fpt, bt, at)
321 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
322 bits.bound_z(n1, it, fit, fpt, bt, at)
323 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
324 bits.bound_z(n1, it, fit, fpt, bt, at)
325 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
326 bits.bound_z(n1, it, fit, fpt, bt, at)
327 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
328 bits.bound_z(n1, it, fit, fpt, bt, at)
329 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
330 bits.bound_z(n1, it, fit, fpt, bt, at)
331 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
332 bits.bound_z(n1, it, fit, fpt, bt, at)
333 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
334 bits.bound_z(n1, it, fit, fpt, bt, at)
335 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
336 bits.bound_z(n1, it, fit, fpt, bt, at)
337 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
338 bits.bound_z(n1, it, fit, fpt, bt, at)
339 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
340 bits.bound_z(n1, it, fit, fpt, bt, at)
341 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
342 bits.bound_z(n1, it, fit, fpt, bt, at)
343 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
344 bits.bound_z(n1, it, fit, fpt, bt, at)
345 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
346 bits.bound_z(n1, it, fit, fpt, bt, at)
347 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
348 bits.bound_z(n1, it, fit, fpt, bt, at)
349 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
350 bits.bound_z(n1, it, fit, fpt, bt, at)
351 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
352 bits.bound_z(n1, it, fit, fpt, bt, at)
353 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
354 bits.bound_z(n1, it, fit, fpt, bt, at)
355 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
356 bits.bound_z(n1, it, fit, fpt, bt, at)
357 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
358 bits.bound_z(n1, it, fit, fpt, bt, at)