def nfa.taut_adv
import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOFimport Base
377def nfa.taut_adv(+hb: Bool, +cin: Bool, +ain: Bool, +e: Bool, +p: Bool, +q: Bool, +r: Bool, +z: Bool) -> {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(hb, cin), False{}), ain), p), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), e), q), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), False{}), r), z))) == Bool.or(Bool.and(ain, p), Bool.or(Bool.and(cin, Bool.and(e, q)), Bool.or(Bool.and(hb, Bool.and(e, q)), z))) : Bool}:
378 match hb:
379 case True{}:
380 match cin:
381 case True{}:
382 match ain:
383 case True{}:
384 match e:
385 case True{}:
386 match p:
387 case True{}:
388 match q:
389 case True{}:
390 match r:
391 case True{}:
392 match z:
393 case True{}:
394 {==}
395 case False{}:
396 {==}
397 case False{}:
398 match z:
399 case True{}:
400 {==}
401 case False{}:
402 {==}
403 case False{}:
404 match r:
405 case True{}:
406 match z:
407 case True{}:
408 {==}
409 case False{}:
410 {==}
411 case False{}:
412 match z:
413 case True{}:
414 {==}
415 case False{}:
416 {==}
417 case False{}:
418 match q:
419 case True{}:
420 match r:
421 case True{}:
422 match z:
423 case True{}:
424 {==}
425 case False{}:
426 {==}
427 case False{}:
428 match z:
429 case True{}:
430 {==}
431 case False{}:
432 {==}
433 case False{}:
434 match r:
435 case True{}:
436 match z:
437 case True{}:
438 {==}
439 case False{}:
440 {==}
441 case False{}:
442 match z:
443 case True{}:
444 {==}
445 case False{}:
446 {==}
447 case False{}:
448 match p:
449 case True{}:
450 match q:
451 case True{}:
452 match r:
453 case True{}:
454 match z:
455 case True{}:
456 {==}
457 case False{}:
458 {==}
459 case False{}:
460 match z:
461 case True{}:
462 {==}
463 case False{}:
464 {==}
465 case False{}:
466 match r:
467 case True{}:
468 match z:
469 case True{}:
470 {==}
471 case False{}:
472 {==}
473 case False{}:
474 match z:
475 case True{}:
476 {==}
477 case False{}:
478 {==}
479 case False{}:
480 match q:
481 case True{}:
482 match r:
483 case True{}:
484 match z:
485 case True{}:
486 {==}
487 case False{}:
488 {==}
489 case False{}:
490 match z:
491 case True{}:
492 {==}
493 case False{}:
494 {==}
495 case False{}:
496 match r:
497 case True{}:
498 match z:
499 case True{}:
500 {==}
501 case False{}:
502 {==}
503 case False{}:
504 match z:
505 case True{}:
506 {==}
507 case False{}:
508 {==}
509 case False{}:
510 match e:
511 case True{}:
512 match p:
513 case True{}:
514 match q:
515 case True{}:
516 match r:
517 case True{}:
518 match z:
519 case True{}:
520 {==}
521 case False{}:
522 {==}
523 case False{}:
524 match z:
525 case True{}:
526 {==}
527 case False{}:
528 {==}
529 case False{}:
530 match r:
531 case True{}:
532 match z:
533 case True{}:
534 {==}
535 case False{}:
536 {==}
537 case False{}:
538 match z:
539 case True{}:
540 {==}
541 case False{}:
542 {==}
543 case False{}:
544 match q:
545 case True{}:
546 match r:
547 case True{}:
548 match z:
549 case True{}:
550 {==}
551 case False{}:
552 {==}
553 case False{}:
554 match z:
555 case True{}:
556 {==}
557 case False{}:
558 {==}
559 case False{}:
560 match r:
561 case True{}:
562 match z:
563 case True{}:
564 {==}
565 case False{}:
566 {==}
567 case False{}:
568 match z:
569 case True{}:
570 {==}
571 case False{}:
572 {==}
573 case False{}:
574 match p:
575 case True{}:
576 match q:
577 case True{}:
578 match r:
579 case True{}:
580 match z:
581 case True{}:
582 {==}
583 case False{}:
584 {==}
585 case False{}:
586 match z:
587 case True{}:
588 {==}
589 case False{}:
590 {==}
591 case False{}:
592 match r:
593 case True{}:
594 match z:
595 case True{}:
596 {==}
597 case False{}:
598 {==}
599 case False{}:
600 match z:
601 case True{}:
602 {==}
603 case False{}:
604 {==}
605 case False{}:
606 match q:
607 case True{}:
608 match r:
609 case True{}:
610 match z:
611 case True{}:
612 {==}
613 case False{}:
614 {==}
615 case False{}:
616 match z:
617 case True{}:
618 {==}
619 case False{}:
620 {==}
621 case False{}:
622 match r:
623 case True{}:
624 match z:
625 case True{}:
626 {==}
627 case False{}:
628 {==}
629 case False{}:
630 match z:
631 case True{}:
632 {==}
633 case False{}:
634 {==}
635 case False{}:
636 match ain:
637 case True{}:
638 match e:
639 case True{}:
640 match p:
641 case True{}:
642 match q:
643 case True{}:
644 match r:
645 case True{}:
646 match z:
647 case True{}:
648 {==}
649 case False{}:
650 {==}
651 case False{}:
652 match z:
653 case True{}:
654 {==}
655 case False{}:
656 {==}
657 case False{}:
658 match r:
659 case True{}:
660 match z:
661 case True{}:
662 {==}
663 case False{}:
664 {==}
665 case False{}:
666 match z:
667 case True{}:
668 {==}
669 case False{}:
670 {==}
671 case False{}:
672 match q:
673 case True{}:
674 match r:
675 case True{}:
676 match z:
677 case True{}:
678 {==}
679 case False{}:
680 {==}
681 case False{}:
682 match z:
683 case True{}:
684 {==}
685 case False{}:
686 {==}
687 case False{}:
688 match r:
689 case True{}:
690 match z:
691 case True{}:
692 {==}
693 case False{}:
694 {==}
695 case False{}:
696 match z:
697 case True{}:
698 {==}
699 case False{}:
700 {==}
701 case False{}:
702 match p:
703 case True{}:
704 match q:
705 case True{}:
706 match r:
707 case True{}:
708 match z:
709 case True{}:
710 {==}
711 case False{}:
712 {==}
713 case False{}:
714 match z:
715 case True{}:
716 {==}
717 case False{}:
718 {==}
719 case False{}:
720 match r:
721 case True{}:
722 match z:
723 case True{}:
724 {==}
725 case False{}:
726 {==}
727 case False{}:
728 match z:
729 case True{}:
730 {==}
731 case False{}:
732 {==}
733 case False{}:
734 match q:
735 case True{}:
736 match r:
737 case True{}:
738 match z:
739 case True{}:
740 {==}
741 case False{}:
742 {==}
743 case False{}:
744 match z:
745 case True{}:
746 {==}
747 case False{}:
748 {==}
749 case False{}:
750 match r:
751 case True{}:
752 match z:
753 case True{}:
754 {==}
755 case False{}:
756 {==}
757 case False{}:
758 match z:
759 case True{}:
760 {==}
761 case False{}:
762 {==}
763 case False{}:
764 match e:
765 case True{}:
766 match p:
767 case True{}:
768 match q:
769 case True{}:
770 match r:
771 case True{}:
772 match z:
773 case True{}:
774 {==}
775 case False{}:
776 {==}
777 case False{}:
778 match z:
779 case True{}:
780 {==}
781 case False{}:
782 {==}
783 case False{}:
784 match r:
785 case True{}:
786 match z:
787 case True{}:
788 {==}
789 case False{}:
790 {==}
791 case False{}:
792 match z:
793 case True{}:
794 {==}
795 case False{}:
796 {==}
797 case False{}:
798 match q:
799 case True{}:
800 match r:
801 case True{}:
802 match z:
803 case True{}:
804 {==}
805 case False{}:
806 {==}
807 case False{}:
808 match z:
809 case True{}:
810 {==}
811 case False{}:
812 {==}
813 case False{}:
814 match r:
815 case True{}:
816 match z:
817 case True{}:
818 {==}
819 case False{}:
820 {==}
821 case False{}:
822 match z:
823 case True{}:
824 {==}
825 case False{}:
826 {==}
827 case False{}:
828 match p:
829 case True{}:
830 match q:
831 case True{}:
832 match r:
833 case True{}:
834 match z:
835 case True{}:
836 {==}
837 case False{}:
838 {==}
839 case False{}:
840 match z:
841 case True{}:
842 {==}
843 case False{}:
844 {==}
845 case False{}:
846 match r:
847 case True{}:
848 match z:
849 case True{}:
850 {==}
851 case False{}:
852 {==}
853 case False{}:
854 match z:
855 case True{}:
856 {==}
857 case False{}:
858 {==}
859 case False{}:
860 match q:
861 case True{}:
862 match r:
863 case True{}:
864 match z:
865 case True{}:
866 {==}
867 case False{}:
868 {==}
869 case False{}:
870 match z:
871 case True{}:
872 {==}
873 case False{}:
874 {==}
875 case False{}:
876 match r:
877 case True{}:
878 match z:
879 case True{}:
880 {==}
881 case False{}:
882 {==}
883 case False{}:
884 match z:
885 case True{}:
886 {==}
887 case False{}:
888 {==}
889 case False{}:
890 match cin:
891 case True{}:
892 match ain:
893 case True{}:
894 match e:
895 case True{}:
896 match p:
897 case True{}:
898 match q:
899 case True{}:
900 match r:
901 case True{}:
902 match z:
903 case True{}:
904 {==}
905 case False{}:
906 {==}
907 case False{}:
908 match z:
909 case True{}:
910 {==}
911 case False{}:
912 {==}
913 case False{}:
914 match r:
915 case True{}:
916 match z:
917 case True{}:
918 {==}
919 case False{}:
920 {==}
921 case False{}:
922 match z:
923 case True{}:
924 {==}
925 case False{}:
926 {==}
927 case False{}:
928 match q:
929 case True{}:
930 match r:
931 case True{}:
932 match z:
933 case True{}:
934 {==}
935 case False{}:
936 {==}
937 case False{}:
938 match z:
939 case True{}:
940 {==}
941 case False{}:
942 {==}
943 case False{}:
944 match r:
945 case True{}:
946 match z:
947 case True{}:
948 {==}
949 case False{}:
950 {==}
951 case False{}:
952 match z:
953 case True{}:
954 {==}
955 case False{}:
956 {==}
957 case False{}:
958 match p:
959 case True{}:
960 match q:
961 case True{}:
962 match r:
963 case True{}:
964 match z:
965 case True{}:
966 {==}
967 case False{}:
968 {==}
969 case False{}:
970 match z:
971 case True{}:
972 {==}
973 case False{}:
974 {==}
975 case False{}:
976 match r:
977 case True{}:
978 match z:
979 case True{}:
980 {==}
981 case False{}:
982 {==}
983 case False{}:
984 match z:
985 case True{}:
986 {==}
987 case False{}:
988 {==}
989 case False{}:
990 match q:
991 case True{}:
992 match r:
993 case True{}:
994 match z:
995 case True{}:
996 {==}
997 case False{}:
998 {==}
999 case False{}:
1000 match z:
1001 case True{}:
1002 {==}
1003 case False{}:
1004 {==}
1005 case False{}:
1006 match r:
1007 case True{}:
1008 match z:
1009 case True{}:
1010 {==}
1011 case False{}:
1012 {==}
1013 case False{}:
1014 match z:
1015 case True{}:
1016 {==}
1017 case False{}:
1018 {==}
1019 case False{}:
1020 match e:
1021 case True{}:
1022 match p:
1023 case True{}:
1024 match q:
1025 case True{}:
1026 match r:
1027 case True{}:
1028 match z:
1029 case True{}:
1030 {==}
1031 case False{}:
1032 {==}
1033 case False{}:
1034 match z:
1035 case True{}:
1036 {==}
1037 case False{}:
1038 {==}
1039 case False{}:
1040 match r:
1041 case True{}:
1042 match z:
1043 case True{}:
1044 {==}
1045 case False{}:
1046 {==}
1047 case False{}:
1048 match z:
1049 case True{}:
1050 {==}
1051 case False{}:
1052 {==}
1053 case False{}:
1054 match q:
1055 case True{}:
1056 match r:
1057 case True{}:
1058 match z:
1059 case True{}:
1060 {==}
1061 case False{}:
1062 {==}
1063 case False{}:
1064 match z:
1065 case True{}:
1066 {==}
1067 case False{}:
1068 {==}
1069 case False{}:
1070 match r:
1071 case True{}:
1072 match z:
1073 case True{}:
1074 {==}
1075 case False{}:
1076 {==}
1077 case False{}:
1078 match z:
1079 case True{}:
1080 {==}
1081 case False{}:
1082 {==}
1083 case False{}:
1084 match p:
1085 case True{}:
1086 match q:
1087 case True{}:
1088 match r:
1089 case True{}:
1090 match z:
1091 case True{}:
1092 {==}
1093 case False{}:
1094 {==}
1095 case False{}:
1096 match z:
1097 case True{}:
1098 {==}
1099 case False{}:
1100 {==}
1101 case False{}:
1102 match r:
1103 case True{}:
1104 match z:
1105 case True{}:
1106 {==}
1107 case False{}:
1108 {==}
1109 case False{}:
1110 match z:
1111 case True{}:
1112 {==}
1113 case False{}:
1114 {==}
1115 case False{}:
1116 match q:
1117 case True{}:
1118 match r:
1119 case True{}:
1120 match z:
1121 case True{}:
1122 {==}
1123 case False{}:
1124 {==}
1125 case False{}:
1126 match z:
1127 case True{}:
1128 {==}
1129 case False{}:
1130 {==}
1131 case False{}:
1132 match r:
1133 case True{}:
1134 match z:
1135 case True{}:
1136 {==}
1137 case False{}:
1138 {==}
1139 case False{}:
1140 match z:
1141 case True{}:
1142 {==}
1143 case False{}:
1144 {==}
1145 case False{}:
1146 match ain:
1147 case True{}:
1148 match e:
1149 case True{}:
1150 match p:
1151 case True{}:
1152 match q:
1153 case True{}:
1154 match r:
1155 case True{}:
1156 match z:
1157 case True{}:
1158 {==}
1159 case False{}:
1160 {==}
1161 case False{}:
1162 match z:
1163 case True{}:
1164 {==}
1165 case False{}:
1166 {==}
1167 case False{}:
1168 match r:
1169 case True{}:
1170 match z:
1171 case True{}:
1172 {==}
1173 case False{}:
1174 {==}
1175 case False{}:
1176 match z:
1177 case True{}:
1178 {==}
1179 case False{}:
1180 {==}
1181 case False{}:
1182 match q:
1183 case True{}:
1184 match r:
1185 case True{}:
1186 match z:
1187 case True{}:
1188 {==}
1189 case False{}:
1190 {==}
1191 case False{}:
1192 match z:
1193 case True{}:
1194 {==}
1195 case False{}:
1196 {==}
1197 case False{}:
1198 match r:
1199 case True{}:
1200 match z:
1201 case True{}:
1202 {==}
1203 case False{}:
1204 {==}
1205 case False{}:
1206 match z:
1207 case True{}:
1208 {==}
1209 case False{}:
1210 {==}
1211 case False{}:
1212 match p:
1213 case True{}:
1214 match q:
1215 case True{}:
1216 match r:
1217 case True{}:
1218 match z:
1219 case True{}:
1220 {==}
1221 case False{}:
1222 {==}
1223 case False{}:
1224 match z:
1225 case True{}:
1226 {==}
1227 case False{}:
1228 {==}
1229 case False{}:
1230 match r:
1231 case True{}:
1232 match z:
1233 case True{}:
1234 {==}
1235 case False{}:
1236 {==}
1237 case False{}:
1238 match z:
1239 case True{}:
1240 {==}
1241 case False{}:
1242 {==}
1243 case False{}:
1244 match q:
1245 case True{}:
1246 match r:
1247 case True{}:
1248 match z:
1249 case True{}:
1250 {==}
1251 case False{}:
1252 {==}
1253 case False{}:
1254 match z:
1255 case True{}:
1256 {==}
1257 case False{}:
1258 {==}
1259 case False{}:
1260 match r:
1261 case True{}:
1262 match z:
1263 case True{}:
1264 {==}
1265 case False{}:
1266 {==}
1267 case False{}:
1268 match z:
1269 case True{}:
1270 {==}
1271 case False{}:
1272 {==}
1273 case False{}:
1274 match e:
1275 case True{}:
1276 match p:
1277 case True{}:
1278 match q:
1279 case True{}:
1280 match r:
1281 case True{}:
1282 match z:
1283 case True{}:
1284 {==}
1285 case False{}:
1286 {==}
1287 case False{}:
1288 match z:
1289 case True{}:
1290 {==}
1291 case False{}:
1292 {==}
1293 case False{}:
1294 match r:
1295 case True{}:
1296 match z:
1297 case True{}:
1298 {==}
1299 case False{}:
1300 {==}
1301 case False{}:
1302 match z:
1303 case True{}:
1304 {==}
1305 case False{}:
1306 {==}
1307 case False{}:
1308 match q:
1309 case True{}:
1310 match r:
1311 case True{}:
1312 match z:
1313 case True{}:
1314 {==}
1315 case False{}:
1316 {==}
1317 case False{}:
1318 match z:
1319 case True{}:
1320 {==}
1321 case False{}:
1322 {==}
1323 case False{}:
1324 match r:
1325 case True{}:
1326 match z:
1327 case True{}:
1328 {==}
1329 case False{}:
1330 {==}
1331 case False{}:
1332 match z:
1333 case True{}:
1334 {==}
1335 case False{}:
1336 {==}
1337 case False{}:
1338 match p:
1339 case True{}:
1340 match q:
1341 case True{}:
1342 match r:
1343 case True{}:
1344 match z:
1345 case True{}:
1346 {==}
1347 case False{}:
1348 {==}
1349 case False{}:
1350 match z:
1351 case True{}:
1352 {==}
1353 case False{}:
1354 {==}
1355 case False{}:
1356 match r:
1357 case True{}:
1358 match z:
1359 case True{}:
1360 {==}
1361 case False{}:
1362 {==}
1363 case False{}:
1364 match z:
1365 case True{}:
1366 {==}
1367 case False{}:
1368 {==}
1369 case False{}:
1370 match q:
1371 case True{}:
1372 match r:
1373 case True{}:
1374 match z:
1375 case True{}:
1376 {==}
1377 case False{}:
1378 {==}
1379 case False{}:
1380 match z:
1381 case True{}:
1382 {==}
1383 case False{}:
1384 {==}
1385 case False{}:
1386 match r:
1387 case True{}:
1388 match z:
1389 case True{}:
1390 {==}
1391 case False{}:
1392 {==}
1393 case False{}:
1394 match z:
1395 case True{}:
1396 {==}
1397 case False{}:
1398 {==}