def acc.join_empty_l

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

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

3432def acc.join_empty_l(+a: V.AaAcc) -> {V.AaAcc.join(V.AaAcc.empty(), a) == a : V.AaAcc}:
3433  match a:
3434    case V.AaAcc{al, de, au, qu}:
3435      match al:
3436        case P.AaPerms{x1}:
3437          match de:
3438            case P.AaPerms{x2}:
3439              match au:
3440                case P.AaPerms{x3}:
3441                  match qu:
3442                    case P.AaPerms{x4}:
3443                      {==}