def bits.bound_vz

bend-osdev-caps@0.1.0.0 · PROOF.bend:431

import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C

431def bits.bound_vz(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: 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, i)) == True{} : Bool}:
432  match n:
433    case 0n:
434      {==}
435    case 1n+n1:
436      match i fi fp b:
437        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt}:
438          bits.bound_vz(n1, it, fit, fpt, bt)
439        case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt}:
440          bits.bound_vz(n1, it, fit, fpt, bt)
441        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt}:
442          bits.bound_vz(n1, it, fit, fpt, bt)
443        case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt}:
444          bits.bound_vz(n1, it, fit, fpt, bt)
445        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt}:
446          bits.bound_vz(n1, it, fit, fpt, bt)
447        case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt}:
448          bits.bound_vz(n1, it, fit, fpt, bt)
449        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt}:
450          bits.bound_vz(n1, it, fit, fpt, bt)
451        case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt}:
452          bits.bound_vz(n1, it, fit, fpt, bt)
453        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt}:
454          bits.bound_vz(n1, it, fit, fpt, bt)
455        case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt}:
456          bits.bound_vz(n1, it, fit, fpt, bt)
457        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt}:
458          bits.bound_vz(n1, it, fit, fpt, bt)
459        case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt}:
460          bits.bound_vz(n1, it, fit, fpt, bt)
461        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt}:
462          bits.bound_vz(n1, it, fit, fpt, bt)
463        case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt}:
464          bits.bound_vz(n1, it, fit, fpt, bt)
465        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt}:
466          bits.bound_vz(n1, it, fit, fpt, bt)
467        case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt}:
468          bits.bound_vz(n1, it, fit, fpt, bt)