PROOF.gnd.acc: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3379-3382 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=3379&end_line=3382

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

def gnd.acc(+acc: V.AaAcc) -> {P.AaPerms.meets(V.AaAcc.granted(acc), V.AaAcc.deny(acc)) == False{} : Bool}:
  match acc:
    case V.AaAcc{al, de, au, qu}:
      pm.minus_meets(al, de)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=pm.minus_meets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaAcc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaAcc.deny
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaAcc.granted
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaPerms.meets