def bits.minus_within

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

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

539def 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}:
540  match n:
541    case 0n:
542      h0 => {==}
543    case 1n+n1:
544      match a y p:
545        case WCon{True{}, +at} WCon{True{}, +yt} WCon{True{}, +pt}:
546          h0 => bits.minus_within(n1, at, yt, pt)(h0)
547        case WCon{True{}, +at} WCon{True{}, +yt} WCon{False{}, +pt}:
548          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)
549        case WCon{True{}, +at} WCon{False{}, +yt} WCon{True{}, +pt}:
550          h0 => bits.minus_within(n1, at, yt, pt)(h0)
551        case WCon{True{}, +at} WCon{False{}, +yt} WCon{False{}, +pt}:
552          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)
553        case WCon{False{}, +at} WCon{True{}, +yt} WCon{True{}, +pt}:
554          h0 => bits.minus_within(n1, at, yt, pt)(h0)
555        case WCon{False{}, +at} WCon{True{}, +yt} WCon{False{}, +pt}:
556          h0 => bits.minus_within(n1, at, yt, pt)(h0)
557        case WCon{False{}, +at} WCon{False{}, +yt} WCon{True{}, +pt}:
558          h0 => bits.minus_within(n1, at, yt, pt)(h0)
559        case WCon{False{}, +at} WCon{False{}, +yt} WCon{False{}, +pt}:
560          h0 => bits.minus_within(n1, at, yt, pt)(h0)