def acc.join_assoc

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

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

3454def 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}:
3455  match a:
3456    case V.AaAcc{al1, de1, au1, qu1}:
3457      match b:
3458        case V.AaAcc{al2, de2, au2, qu2}:
3459          match c:
3460            case V.AaAcc{al3, de3, au3, qu3}:
3461              %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}
3462              %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}
3463              %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}
3464              %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}
3465              {==}