def acc.join_idem

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

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

3467def acc.join_idem(+a: V.AaAcc) -> {V.AaAcc.join(a, a) == a : V.AaAcc}:
3468  match a:
3469    case V.AaAcc{al, de, au, qu}:
3470      %pm.idem(al) : {V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), P.AaPerms.union(au, au), P.AaPerms.union(qu, qu)} == V.AaAcc{_, de, au, qu} : V.AaAcc}
3471      %pm.idem(de) : {V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), P.AaPerms.union(au, au), P.AaPerms.union(qu, qu)} == V.AaAcc{P.AaPerms.union(al, al), _, au, qu} : V.AaAcc}
3472      %pm.idem(au) : {V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), P.AaPerms.union(au, au), P.AaPerms.union(qu, qu)} == V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), _, qu} : V.AaAcc}
3473      %pm.idem(qu) : {V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), P.AaPerms.union(au, au), P.AaPerms.union(qu, qu)} == V.AaAcc{P.AaPerms.union(al, al), P.AaPerms.union(de, de), P.AaPerms.union(au, au), _} : V.AaAcc}
3474      {==}