def nfa.taut_star2
import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOFimport Base
2423def nfa.taut_star2(+hb: Bool, +cin: Bool, +ain: Bool, +p: Bool, +q: Bool, +r: Bool, +z: Bool) -> {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(hb, cin), True{}), ain), p), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), False{}), q), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), True{}), r), z))) == Bool.or(Bool.and(ain, p), Bool.or(Bool.and(cin, Bool.or(r, p)), Bool.or(Bool.and(hb, Bool.or(r, p)), z))) : Bool}:
2424 match hb:
2425 case True{}:
2426 match cin:
2427 case True{}:
2428 match ain:
2429 case True{}:
2430 match p:
2431 case True{}:
2432 match q:
2433 case True{}:
2434 match r:
2435 case True{}:
2436 match z:
2437 case True{}:
2438 {==}
2439 case False{}:
2440 {==}
2441 case False{}:
2442 match z:
2443 case True{}:
2444 {==}
2445 case False{}:
2446 {==}
2447 case False{}:
2448 match r:
2449 case True{}:
2450 match z:
2451 case True{}:
2452 {==}
2453 case False{}:
2454 {==}
2455 case False{}:
2456 match z:
2457 case True{}:
2458 {==}
2459 case False{}:
2460 {==}
2461 case False{}:
2462 match q:
2463 case True{}:
2464 match r:
2465 case True{}:
2466 match z:
2467 case True{}:
2468 {==}
2469 case False{}:
2470 {==}
2471 case False{}:
2472 match z:
2473 case True{}:
2474 {==}
2475 case False{}:
2476 {==}
2477 case False{}:
2478 match r:
2479 case True{}:
2480 match z:
2481 case True{}:
2482 {==}
2483 case False{}:
2484 {==}
2485 case False{}:
2486 match z:
2487 case True{}:
2488 {==}
2489 case False{}:
2490 {==}
2491 case False{}:
2492 match p:
2493 case True{}:
2494 match q:
2495 case True{}:
2496 match r:
2497 case True{}:
2498 match z:
2499 case True{}:
2500 {==}
2501 case False{}:
2502 {==}
2503 case False{}:
2504 match z:
2505 case True{}:
2506 {==}
2507 case False{}:
2508 {==}
2509 case False{}:
2510 match r:
2511 case True{}:
2512 match z:
2513 case True{}:
2514 {==}
2515 case False{}:
2516 {==}
2517 case False{}:
2518 match z:
2519 case True{}:
2520 {==}
2521 case False{}:
2522 {==}
2523 case False{}:
2524 match q:
2525 case True{}:
2526 match r:
2527 case True{}:
2528 match z:
2529 case True{}:
2530 {==}
2531 case False{}:
2532 {==}
2533 case False{}:
2534 match z:
2535 case True{}:
2536 {==}
2537 case False{}:
2538 {==}
2539 case False{}:
2540 match r:
2541 case True{}:
2542 match z:
2543 case True{}:
2544 {==}
2545 case False{}:
2546 {==}
2547 case False{}:
2548 match z:
2549 case True{}:
2550 {==}
2551 case False{}:
2552 {==}
2553 case False{}:
2554 match ain:
2555 case True{}:
2556 match p:
2557 case True{}:
2558 match q:
2559 case True{}:
2560 match r:
2561 case True{}:
2562 match z:
2563 case True{}:
2564 {==}
2565 case False{}:
2566 {==}
2567 case False{}:
2568 match z:
2569 case True{}:
2570 {==}
2571 case False{}:
2572 {==}
2573 case False{}:
2574 match r:
2575 case True{}:
2576 match z:
2577 case True{}:
2578 {==}
2579 case False{}:
2580 {==}
2581 case False{}:
2582 match z:
2583 case True{}:
2584 {==}
2585 case False{}:
2586 {==}
2587 case False{}:
2588 match q:
2589 case True{}:
2590 match r:
2591 case True{}:
2592 match z:
2593 case True{}:
2594 {==}
2595 case False{}:
2596 {==}
2597 case False{}:
2598 match z:
2599 case True{}:
2600 {==}
2601 case False{}:
2602 {==}
2603 case False{}:
2604 match r:
2605 case True{}:
2606 match z:
2607 case True{}:
2608 {==}
2609 case False{}:
2610 {==}
2611 case False{}:
2612 match z:
2613 case True{}:
2614 {==}
2615 case False{}:
2616 {==}
2617 case False{}:
2618 match p:
2619 case True{}:
2620 match q:
2621 case True{}:
2622 match r:
2623 case True{}:
2624 match z:
2625 case True{}:
2626 {==}
2627 case False{}:
2628 {==}
2629 case False{}:
2630 match z:
2631 case True{}:
2632 {==}
2633 case False{}:
2634 {==}
2635 case False{}:
2636 match r:
2637 case True{}:
2638 match z:
2639 case True{}:
2640 {==}
2641 case False{}:
2642 {==}
2643 case False{}:
2644 match z:
2645 case True{}:
2646 {==}
2647 case False{}:
2648 {==}
2649 case False{}:
2650 match q:
2651 case True{}:
2652 match r:
2653 case True{}:
2654 match z:
2655 case True{}:
2656 {==}
2657 case False{}:
2658 {==}
2659 case False{}:
2660 match z:
2661 case True{}:
2662 {==}
2663 case False{}:
2664 {==}
2665 case False{}:
2666 match r:
2667 case True{}:
2668 match z:
2669 case True{}:
2670 {==}
2671 case False{}:
2672 {==}
2673 case False{}:
2674 match z:
2675 case True{}:
2676 {==}
2677 case False{}:
2678 {==}
2679 case False{}:
2680 match cin:
2681 case True{}:
2682 match ain:
2683 case True{}:
2684 match p:
2685 case True{}:
2686 match q:
2687 case True{}:
2688 match r:
2689 case True{}:
2690 match z:
2691 case True{}:
2692 {==}
2693 case False{}:
2694 {==}
2695 case False{}:
2696 match z:
2697 case True{}:
2698 {==}
2699 case False{}:
2700 {==}
2701 case False{}:
2702 match r:
2703 case True{}:
2704 match z:
2705 case True{}:
2706 {==}
2707 case False{}:
2708 {==}
2709 case False{}:
2710 match z:
2711 case True{}:
2712 {==}
2713 case False{}:
2714 {==}
2715 case False{}:
2716 match q:
2717 case True{}:
2718 match r:
2719 case True{}:
2720 match z:
2721 case True{}:
2722 {==}
2723 case False{}:
2724 {==}
2725 case False{}:
2726 match z:
2727 case True{}:
2728 {==}
2729 case False{}:
2730 {==}
2731 case False{}:
2732 match r:
2733 case True{}:
2734 match z:
2735 case True{}:
2736 {==}
2737 case False{}:
2738 {==}
2739 case False{}:
2740 match z:
2741 case True{}:
2742 {==}
2743 case False{}:
2744 {==}
2745 case False{}:
2746 match p:
2747 case True{}:
2748 match q:
2749 case True{}:
2750 match r:
2751 case True{}:
2752 match z:
2753 case True{}:
2754 {==}
2755 case False{}:
2756 {==}
2757 case False{}:
2758 match z:
2759 case True{}:
2760 {==}
2761 case False{}:
2762 {==}
2763 case False{}:
2764 match r:
2765 case True{}:
2766 match z:
2767 case True{}:
2768 {==}
2769 case False{}:
2770 {==}
2771 case False{}:
2772 match z:
2773 case True{}:
2774 {==}
2775 case False{}:
2776 {==}
2777 case False{}:
2778 match q:
2779 case True{}:
2780 match r:
2781 case True{}:
2782 match z:
2783 case True{}:
2784 {==}
2785 case False{}:
2786 {==}
2787 case False{}:
2788 match z:
2789 case True{}:
2790 {==}
2791 case False{}:
2792 {==}
2793 case False{}:
2794 match r:
2795 case True{}:
2796 match z:
2797 case True{}:
2798 {==}
2799 case False{}:
2800 {==}
2801 case False{}:
2802 match z:
2803 case True{}:
2804 {==}
2805 case False{}:
2806 {==}
2807 case False{}:
2808 match ain:
2809 case True{}:
2810 match p:
2811 case True{}:
2812 match q:
2813 case True{}:
2814 match r:
2815 case True{}:
2816 match z:
2817 case True{}:
2818 {==}
2819 case False{}:
2820 {==}
2821 case False{}:
2822 match z:
2823 case True{}:
2824 {==}
2825 case False{}:
2826 {==}
2827 case False{}:
2828 match r:
2829 case True{}:
2830 match z:
2831 case True{}:
2832 {==}
2833 case False{}:
2834 {==}
2835 case False{}:
2836 match z:
2837 case True{}:
2838 {==}
2839 case False{}:
2840 {==}
2841 case False{}:
2842 match q:
2843 case True{}:
2844 match r:
2845 case True{}:
2846 match z:
2847 case True{}:
2848 {==}
2849 case False{}:
2850 {==}
2851 case False{}:
2852 match z:
2853 case True{}:
2854 {==}
2855 case False{}:
2856 {==}
2857 case False{}:
2858 match r:
2859 case True{}:
2860 match z:
2861 case True{}:
2862 {==}
2863 case False{}:
2864 {==}
2865 case False{}:
2866 match z:
2867 case True{}:
2868 {==}
2869 case False{}:
2870 {==}
2871 case False{}:
2872 match p:
2873 case True{}:
2874 match q:
2875 case True{}:
2876 match r:
2877 case True{}:
2878 match z:
2879 case True{}:
2880 {==}
2881 case False{}:
2882 {==}
2883 case False{}:
2884 match z:
2885 case True{}:
2886 {==}
2887 case False{}:
2888 {==}
2889 case False{}:
2890 match r:
2891 case True{}:
2892 match z:
2893 case True{}:
2894 {==}
2895 case False{}:
2896 {==}
2897 case False{}:
2898 match z:
2899 case True{}:
2900 {==}
2901 case False{}:
2902 {==}
2903 case False{}:
2904 match q:
2905 case True{}:
2906 match r:
2907 case True{}:
2908 match z:
2909 case True{}:
2910 {==}
2911 case False{}:
2912 {==}
2913 case False{}:
2914 match z:
2915 case True{}:
2916 {==}
2917 case False{}:
2918 {==}
2919 case False{}:
2920 match r:
2921 case True{}:
2922 match z:
2923 case True{}:
2924 {==}
2925 case False{}:
2926 {==}
2927 case False{}:
2928 match z:
2929 case True{}:
2930 {==}
2931 case False{}:
2932 {==}