def bits.or_assoc

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

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

3183def 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>}:
3184  match a:
3185    case Nil{}:
3186      {==}
3187    case Con{x, xs}:
3188      match b:
3189        case Nil{}:
3190          {==}
3191        case Con{y, ys}:
3192          match c:
3193            case Nil{}:
3194              {==}
3195            case Con{z, zs}:
3196              %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>}
3197              %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>}
3198              {==}