def nfa.taut_nil

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

import Base

314def nfa.taut_nil(+a: Bool, +n: Bool, +c: Bool, +b: Bool) -> {Bool.and(a, n) == Bool.or(Bool.and(a, n), Bool.or(Bool.and(c, False{}), Bool.and(b, False{}))) : Bool}:
315  match a:
316    case True{}:
317      match n:
318        case True{}:
319          match c:
320            case True{}:
321              match b:
322                case True{}:
323                  {==}
324                case False{}:
325                  {==}
326            case False{}:
327              match b:
328                case True{}:
329                  {==}
330                case False{}:
331                  {==}
332        case False{}:
333          match c:
334            case True{}:
335              match b:
336                case True{}:
337                  {==}
338                case False{}:
339                  {==}
340            case False{}:
341              match b:
342                case True{}:
343                  {==}
344                case False{}:
345                  {==}
346    case False{}:
347      match n:
348        case True{}:
349          match c:
350            case True{}:
351              match b:
352                case True{}:
353                  {==}
354                case False{}:
355                  {==}
356            case False{}:
357              match b:
358                case True{}:
359                  {==}
360                case False{}:
361                  {==}
362        case False{}:
363          match c:
364            case True{}:
365              match b:
366                case True{}:
367                  {==}
368                case False{}:
369                  {==}
370            case False{}:
371              match b:
372                case True{}:
373                  {==}
374                case False{}:
375                  {==}