def bits.or_idem

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

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

3207def bits.or_idem(+a: List<&2, Bool>) -> {P.AaBits.or(a, a) == a : List<&2, Bool>}:
3208  match a:
3209    case Nil{}:
3210      {==}
3211    case Con{x, xs}:
3212      %b.or_idem(x) : {Con{Bool.or(x, x), P.AaBits.or(xs, xs)} == Con{_, xs} : List<&2, Bool>}
3213      %bits.or_idem(xs) : {Con{Bool.or(x, x), P.AaBits.or(xs, xs)} == Con{Bool.or(x, x), _} : List<&2, Bool>}
3214      {==}