def acc.join_empty_r

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

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

3445def acc.join_empty_r(+a: V.AaAcc) -> {V.AaAcc.join(a, V.AaAcc.empty()) == a : V.AaAcc}:
3446  match a:
3447    case V.AaAcc{al, de, au, qu}:
3448      %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}
3449      %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}
3450      %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}
3451      %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}
3452      {==}