def pm.assoc

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

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

3241def pm.assoc(+a: P.AaPerms, +b: P.AaPerms, +c: P.AaPerms) -> {P.AaPerms.union(P.AaPerms.union(a, b), c) == P.AaPerms.union(a, P.AaPerms.union(b, c)) : P.AaPerms}:
3242  match a:
3243    case P.AaPerms{x}:
3244      match b:
3245        case P.AaPerms{y}:
3246          match c:
3247            case P.AaPerms{z}:
3248              Equal.cong(List<&2, Bool>, P.AaPerms, l => P.AaPerms{l}, P.AaBits.or(P.AaBits.or(x, y), z), P.AaBits.or(x, P.AaBits.or(y, z)), bits.or_assoc(x, y, z))