def bits.amb_i

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

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

493def bits.amb_i(+n: Nat, +a: Word(n), +p: Word(n), +i: Word(n)) -> {C.CapBits.subset(n, Word.and(n, Word.and(n, a, p), i), i) == True{} : Bool}:
494  match n:
495    case 0n:
496      {==}
497    case 1n+n1:
498      match a p i:
499        case WCon{True{}, +at} WCon{True{}, +pt} WCon{True{}, +it}:
500          bits.amb_i(n1, at, pt, it)
501        case WCon{True{}, +at} WCon{True{}, +pt} WCon{False{}, +it}:
502          bits.amb_i(n1, at, pt, it)
503        case WCon{True{}, +at} WCon{False{}, +pt} WCon{True{}, +it}:
504          bits.amb_i(n1, at, pt, it)
505        case WCon{True{}, +at} WCon{False{}, +pt} WCon{False{}, +it}:
506          bits.amb_i(n1, at, pt, it)
507        case WCon{False{}, +at} WCon{True{}, +pt} WCon{True{}, +it}:
508          bits.amb_i(n1, at, pt, it)
509        case WCon{False{}, +at} WCon{True{}, +pt} WCon{False{}, +it}:
510          bits.amb_i(n1, at, pt, it)
511        case WCon{False{}, +at} WCon{False{}, +pt} WCon{True{}, +it}:
512          bits.amb_i(n1, at, pt, it)
513        case WCon{False{}, +at} WCon{False{}, +pt} WCon{False{}, +it}:
514          bits.amb_i(n1, at, pt, it)