PROOF.set.lub: def of bend-osdev-caps@0.1.0.0
Import: import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOF
Lines 682-685 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=682&end_line=685

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

def set.lub(+a: C.CapSet(), +s: C.CapSet(), +p: C.CapSet()) -> {C.CapSet.subset(a, p) == True{} : Bool} -> {C.CapSet.subset(s, p) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.union(a, s), p) == True{} : Bool}:
  match a s p:
    case C.CapSetW{U32{+al}, +ah} C.CapSetW{U32{+sl}, +sh} C.CapSetW{U32{+pl}, +ph}:
      +h0 => +h1 => set.sub_intro(Word.or(32n, al, sl), pl, Word.or(9n, ah, sh), ph)(bits.lub(32n, al, sl, pl)(set.sub_lo(al, pl, ah, ph)(h0))(set.sub_lo(sl, pl, sh, ph)(h1)))(bits.lub(9n, ah, sh, ph)(set.sub_hi(al, pl, ah, ph)(h0))(set.sub_hi(sl, pl, sh, ph)(h1)))

Uses (11):
  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.or
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.lub
  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.subset
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapSet.union
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapSetW