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

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_l(+a: V.AaAcc) -> {V.AaAcc.join(V.AaAcc.empty(), a) == a : V.AaAcc}:
  match a:
    case V.AaAcc{al, de, au, qu}:
      match al:
        case P.AaPerms{x1}:
          match de:
            case P.AaPerms{x2}:
              match au:
                case P.AaPerms{x3}:
                  match qu:
                    case P.AaPerms{x4}:
                      {==}

Uses (4):
  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