PROOF.bits.minus_meets: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3059-3081 of bend-osdev-apparmor@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&start_line=3059&end_line=3081

import Base
import bend-osdev-apparmor@0.1.0.0/perm.bend as P

# what minus leaves never meets what it took away
def bits.minus_meets(+a: List<&2, Bool>, +d: List<&2, Bool>) -> {P.AaBits.meets(P.AaBits.minus(a, d), d) == False{} : Bool}:
  match a:
    case Nil{}:
      {==}
    case Con{x, xs}:
      match x:
        case False{}:
          match d:
            case Nil{}:
              {==}
            case Con{y, ys}:
              bits.minus_meets(xs, ys)
        case True{}:
          match d:
            case Nil{}:
              {==}
            case Con{y, ys}:
              match y:
                case True{}:
                  bits.minus_meets(xs, ys)
                case False{}:
                  bits.minus_meets(xs, ys)

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaBits.meets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaBits.minus