PROOF.set.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 687-690 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=687&end_line=690

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

def set.minus_within(+a: C.CapSet(), +y: C.CapSet(), +p: C.CapSet()) -> {C.CapSet.subset(a, p) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.minus(a, y), p) == True{} : Bool}:
  match a y p:
    case C.CapSetW{U32{+al}, +ah} C.CapSetW{U32{+yl}, +yh} C.CapSetW{U32{+pl}, +ph}:
      +h0 => set.sub_intro(Word.and(32n, al, Word.not(32n, yl)), pl, Word.and(9n, ah, Word.not(9n, yh)), ph)(bits.minus_within(32n, al, yl, pl)(set.sub_lo(al, pl, ah, ph)(h0)))(bits.minus_within(9n, ah, yh, ph)(set.sub_hi(al, pl, ah, ph)(h0)))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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.minus_within
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.sub_hi
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.sub_intro
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.sub_lo
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapSet
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapSet.minus
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapSet.subset
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapSetW