def bits.sub_minus

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

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

203def bits.sub_minus(+n: Nat, +x: Word(n), +y: Word(n)) -> {C.CapBits.subset(n, Word.and(n, x, Word.not(n, y)), x) == True{} : Bool}:
204  match n:
205    case 0n:
206      {==}
207    case 1n+n1:
208      match x y:
209        case WCon{True{}, +xt} WCon{True{}, +yt}:
210          bits.sub_minus(n1, xt, yt)
211        case WCon{True{}, +xt} WCon{False{}, +yt}:
212          bits.sub_minus(n1, xt, yt)
213        case WCon{False{}, +xt} WCon{True{}, +yt}:
214          bits.sub_minus(n1, xt, yt)
215        case WCon{False{}, +xt} WCon{False{}, +yt}:
216          bits.sub_minus(n1, xt, yt)