def bits.sub_or_r

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

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

188def bits.sub_or_r(+n: Nat, +x: Word(n), +c: Word(n)) -> {C.CapBits.subset(n, c, Word.or(n, x, c)) == True{} : Bool}:
189  match n:
190    case 0n:
191      {==}
192    case 1n+n1:
193      match x c:
194        case WCon{True{}, +xt} WCon{True{}, +ct}:
195          bits.sub_or_r(n1, xt, ct)
196        case WCon{True{}, +xt} WCon{False{}, +ct}:
197          bits.sub_or_r(n1, xt, ct)
198        case WCon{False{}, +xt} WCon{True{}, +ct}:
199          bits.sub_or_r(n1, xt, ct)
200        case WCon{False{}, +xt} WCon{False{}, +ct}:
201          bits.sub_or_r(n1, xt, ct)