~/jendhub

def pm.none_r

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:3255

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

3255def pm.none_r(+a: P.AaPerms) -> {P.AaPerms.union(a, P.AaPerms.none()) == a : P.AaPerms}:
3256  match a:
3257    case P.AaPerms{x}:
3258      Equal.cong(List<&2, Bool>, P.AaPerms, l => P.AaPerms{l}, P.AaBits.or(x, Nil{}), x, bits.or_nil_r(x))

Uses (8)

Used by (1)