def bits.minus_meets

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

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

3059# what minus leaves never meets what it took away
3060def bits.minus_meets(+a: List<&2, Bool>, +d: List<&2, Bool>) -> {P.AaBits.meets(P.AaBits.minus(a, d), d) == False{} : Bool}:
3061  match a:
3062    case Nil{}:
3063      {==}
3064    case Con{x, xs}:
3065      match x:
3066        case False{}:
3067          match d:
3068            case Nil{}:
3069              {==}
3070            case Con{y, ys}:
3071              bits.minus_meets(xs, ys)
3072        case True{}:
3073          match d:
3074            case Nil{}:
3075              {==}
3076            case Con{y, ys}:
3077              match y:
3078                case True{}:
3079                  bits.minus_meets(xs, ys)
3080                case False{}:
3081                  bits.minus_meets(xs, ys)