PROOF.bits.or_assoc: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3183-3198 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=3183&end_line=3198

import Base
import bend-osdev-apparmor@0.1.0.0/perm.bend as P

def bits.or_assoc(+a: List<&2, Bool>, +b: List<&2, Bool>, +c: List<&2, Bool>) -> {P.AaBits.or(P.AaBits.or(a, b), c) == P.AaBits.or(a, P.AaBits.or(b, c)) : List<&2, Bool>}:
  match a:
    case Nil{}:
      {==}
    case Con{x, xs}:
      match b:
        case Nil{}:
          {==}
        case Con{y, ys}:
          match c:
            case Nil{}:
              {==}
            case Con{z, zs}:
              %b.or_assoc(x, y, z) : {Con{Bool.or(Bool.or(x, y), z), P.AaBits.or(P.AaBits.or(xs, ys), zs)} == Con{_, P.AaBits.or(xs, P.AaBits.or(ys, zs))} : List<&2, Bool>}
              %bits.or_assoc(xs, ys, zs) : {Con{Bool.or(Bool.or(x, y), z), P.AaBits.or(P.AaBits.or(xs, ys), zs)} == Con{Bool.or(Bool.or(x, y), z), _} : List<&2, Bool>}
              {==}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.or_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaBits.or