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

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_assoc(+a: V.AaAcc, +b: V.AaAcc, +c: V.AaAcc) -> {V.AaAcc.join(V.AaAcc.join(a, b), c) == V.AaAcc.join(a, V.AaAcc.join(b, c)) : V.AaAcc}:
  match a:
    case V.AaAcc{al1, de1, au1, qu1}:
      match b:
        case V.AaAcc{al2, de2, au2, qu2}:
          match c:
            case V.AaAcc{al3, de3, au3, qu3}:
              %pm.assoc(al1, al2, al3) : {V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), P.AaPerms.union(P.AaPerms.union(au1, au2), au3), P.AaPerms.union(P.AaPerms.union(qu1, qu2), qu3)} == V.AaAcc{_, P.AaPerms.union(de1, P.AaPerms.union(de2, de3)), P.AaPerms.union(au1, P.AaPerms.union(au2, au3)), P.AaPerms.union(qu1, P.AaPerms.union(qu2, qu3))} : V.AaAcc}
              %pm.assoc(de1, de2, de3) : {V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), P.AaPerms.union(P.AaPerms.union(au1, au2), au3), P.AaPerms.union(P.AaPerms.union(qu1, qu2), qu3)} == V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), _, P.AaPerms.union(au1, P.AaPerms.union(au2, au3)), P.AaPerms.union(qu1, P.AaPerms.union(qu2, qu3))} : V.AaAcc}
              %pm.assoc(au1, au2, au3) : {V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), P.AaPerms.union(P.AaPerms.union(au1, au2), au3), P.AaPerms.union(P.AaPerms.union(qu1, qu2), qu3)} == V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), _, P.AaPerms.union(qu1, P.AaPerms.union(qu2, qu3))} : V.AaAcc}
              %pm.assoc(qu1, qu2, qu3) : {V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), P.AaPerms.union(P.AaPerms.union(au1, au2), au3), P.AaPerms.union(P.AaPerms.union(qu1, qu2), qu3)} == V.AaAcc{P.AaPerms.union(P.AaPerms.union(al1, al2), al3), P.AaPerms.union(P.AaPerms.union(de1, de2), de3), P.AaPerms.union(P.AaPerms.union(au1, au2), au3), _} : V.AaAcc}
              {==}

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