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

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_empty_r(+a: V.AaAcc) -> {V.AaAcc.join(a, V.AaAcc.empty()) == a : V.AaAcc}:
  match a:
    case V.AaAcc{al, de, au, qu}:
      %pm.none_r(al) : {V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), P.AaPerms.union(au, P.AaPerms.none()), P.AaPerms.union(qu, P.AaPerms.none())} == V.AaAcc{_, de, au, qu} : V.AaAcc}
      %pm.none_r(de) : {V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), P.AaPerms.union(au, P.AaPerms.none()), P.AaPerms.union(qu, P.AaPerms.none())} == V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), _, au, qu} : V.AaAcc}
      %pm.none_r(au) : {V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), P.AaPerms.union(au, P.AaPerms.none()), P.AaPerms.union(qu, P.AaPerms.none())} == V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), _, qu} : V.AaAcc}
      %pm.none_r(qu) : {V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), P.AaPerms.union(au, P.AaPerms.none()), P.AaPerms.union(qu, P.AaPerms.none())} == V.AaAcc{P.AaPerms.union(al, P.AaPerms.none()), P.AaPerms.union(de, P.AaPerms.none()), P.AaPerms.union(au, P.AaPerms.none()), _} : V.AaAcc}
      {==}

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