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

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 acc.join_idem(+a: V.AaAcc) -> {V.AaAcc.join(a, a) == a : V.AaAcc}:
  match a:
    case V.AaAcc{al, de, au, qu}:
      %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}
      %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}
      %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}
      %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}
      {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=pm.idem
  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.join
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaPerms.union