def bits.lub

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

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

516def 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}:
517  match n:
518    case 0n:
519      h0 => h1 => {==}
520    case 1n+n1:
521      match a s p:
522        case WCon{True{}, +at} WCon{True{}, +st} WCon{True{}, +pt}:
523          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
524        case WCon{True{}, +at} WCon{True{}, +st} WCon{False{}, +pt}:
525          h0 => h1 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, WCon{True{}, at}, WCon{True{}, st}), WCon{False{}, pt}), h0)
526        case WCon{True{}, +at} WCon{False{}, +st} WCon{True{}, +pt}:
527          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
528        case WCon{True{}, +at} WCon{False{}, +st} WCon{False{}, +pt}:
529          h0 => h1 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, WCon{True{}, at}, WCon{False{}, st}), WCon{False{}, pt}), h0)
530        case WCon{False{}, +at} WCon{True{}, +st} WCon{True{}, +pt}:
531          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
532        case WCon{False{}, +at} WCon{True{}, +st} WCon{False{}, +pt}:
533          h0 => h1 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, WCon{False{}, at}, WCon{True{}, st}), WCon{False{}, pt}), h1)
534        case WCon{False{}, +at} WCon{False{}, +st} WCon{True{}, +pt}:
535          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)
536        case WCon{False{}, +at} WCon{False{}, +st} WCon{False{}, +pt}:
537          h0 => h1 => bits.lub(n1, at, st, pt)(h0)(h1)