PROOF.bits.minus_within: def of bend-osdev-caps@0.1.0.0
Import: import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOF
Lines 539-560 of bend-osdev-caps@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&start_line=539&end_line=560

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

def bits.minus_within(+n: Nat, +a: Word(n), +y: Word(n), +p: Word(n)) -> {C.CapBits.subset(n, a, p) == True{} : Bool} -> {C.CapBits.subset(n, Word.and(n, a, Word.not(n, y)), p) == True{} : Bool}:
  match n:
    case 0n:
      h0 => {==}
    case 1n+n1:
      match a y p:
        case WCon{True{}, +at} WCon{True{}, +yt} WCon{True{}, +pt}:
          h0 => bits.minus_within(n1, at, yt, pt)(h0)
        case WCon{True{}, +at} WCon{True{}, +yt} WCon{False{}, +pt}:
          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.and(1n+n1, WCon{True{}, at}, Word.not(1n+n1, WCon{True{}, yt})), WCon{False{}, pt}), h0)
        case WCon{True{}, +at} WCon{False{}, +yt} WCon{True{}, +pt}:
          h0 => bits.minus_within(n1, at, yt, pt)(h0)
        case WCon{True{}, +at} WCon{False{}, +yt} WCon{False{}, +pt}:
          h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.and(1n+n1, WCon{True{}, at}, Word.not(1n+n1, WCon{False{}, yt})), WCon{False{}, pt}), h0)
        case WCon{False{}, +at} WCon{True{}, +yt} WCon{True{}, +pt}:
          h0 => bits.minus_within(n1, at, yt, pt)(h0)
        case WCon{False{}, +at} WCon{True{}, +yt} WCon{False{}, +pt}:
          h0 => bits.minus_within(n1, at, yt, pt)(h0)
        case WCon{False{}, +at} WCon{False{}, +yt} WCon{True{}, +pt}:
          h0 => bits.minus_within(n1, at, yt, pt)(h0)
        case WCon{False{}, +at} WCon{False{}, +yt} WCon{False{}, +pt}:
          h0 => bits.minus_within(n1, at, yt, pt)(h0)

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.not
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.absurd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapBits.subset