~/jendhub

def pm.idem

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

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

3250def pm.idem(+a: P.AaPerms) -> {P.AaPerms.union(a, a) == a : P.AaPerms}:
3251  match a:
3252    case P.AaPerms{x}:
3253      Equal.cong(List<&2, Bool>, P.AaPerms, l => P.AaPerms{l}, P.AaBits.or(x, x), x, bits.or_idem(x))

Uses (7)

Used by (1)