def bits.amb_p

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

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

470def bits.amb_p(+n: Nat, +a: Word(n), +p: Word(n), +i: Word(n)) -> {C.CapBits.subset(n, Word.and(n, Word.and(n, a, p), i), p) == True{} : Bool}:
471  match n:
472    case 0n:
473      {==}
474    case 1n+n1:
475      match a p i:
476        case WCon{True{}, +at} WCon{True{}, +pt} WCon{True{}, +it}:
477          bits.amb_p(n1, at, pt, it)
478        case WCon{True{}, +at} WCon{True{}, +pt} WCon{False{}, +it}:
479          bits.amb_p(n1, at, pt, it)
480        case WCon{True{}, +at} WCon{False{}, +pt} WCon{True{}, +it}:
481          bits.amb_p(n1, at, pt, it)
482        case WCon{True{}, +at} WCon{False{}, +pt} WCon{False{}, +it}:
483          bits.amb_p(n1, at, pt, it)
484        case WCon{False{}, +at} WCon{True{}, +pt} WCon{True{}, +it}:
485          bits.amb_p(n1, at, pt, it)
486        case WCon{False{}, +at} WCon{True{}, +pt} WCon{False{}, +it}:
487          bits.amb_p(n1, at, pt, it)
488        case WCon{False{}, +at} WCon{False{}, +pt} WCon{True{}, +it}:
489          bits.amb_p(n1, at, pt, it)
490        case WCon{False{}, +at} WCon{False{}, +pt} WCon{False{}, +it}:
491          bits.amb_p(n1, at, pt, it)