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

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

def bits.lub(+n: Nat, +a: Word(n), +s: Word(n), +p: Word(n)) -> {C.CapBits.subset(n, a, p) == True{} : Bool} -> {C.CapBits.subset(n, s, p) == True{} : Bool} -> {C.CapBits.subset(n, Word.or(n, a, s), p) == True{} : Bool}:
  match n:
    case 0n:
      h0 => h1 => {==}
    case 1n+n1:
      match a s p:
        case WCon{True{}, +at} WCon{True{}, +st} WCon{True{}, +pt}:
          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
        case WCon{True{}, +at} WCon{True{}, +st} WCon{False{}, +pt}:
          h0 => h1 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, WCon{True{}, at}, WCon{True{}, st}), WCon{False{}, pt}), h0)
        case WCon{True{}, +at} WCon{False{}, +st} WCon{True{}, +pt}:
          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
        case WCon{True{}, +at} WCon{False{}, +st} WCon{False{}, +pt}:
          h0 => h1 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, WCon{True{}, at}, WCon{False{}, st}), WCon{False{}, pt}), h0)
        case WCon{False{}, +at} WCon{True{}, +st} WCon{True{}, +pt}:
          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
        case WCon{False{}, +at} WCon{True{}, +st} WCon{False{}, +pt}:
          h0 => h1 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, WCon{False{}, at}, WCon{True{}, st}), WCon{False{}, pt}), h1)
        case WCon{False{}, +at} WCon{False{}, +st} WCon{True{}, +pt}:
          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
        case WCon{False{}, +at} WCon{False{}, +st} WCon{False{}, +pt}:
          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)

Uses (7):
  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.or
  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