def nfa.taut_star
import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOFimport Base
1400def nfa.taut_star(+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), e), 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, Bool.and(e, p))), Bool.or(Bool.and(hb, Bool.or(r, Bool.and(e, p))), z))) : Bool}:
1401 match hb:
1402 case True{}:
1403 match cin:
1404 case True{}:
1405 match ain:
1406 case True{}:
1407 match e:
1408 case True{}:
1409 match p:
1410 case True{}:
1411 match q:
1412 case True{}:
1413 match r:
1414 case True{}:
1415 match z:
1416 case True{}:
1417 {==}
1418 case False{}:
1419 {==}
1420 case False{}:
1421 match z:
1422 case True{}:
1423 {==}
1424 case False{}:
1425 {==}
1426 case False{}:
1427 match r:
1428 case True{}:
1429 match z:
1430 case True{}:
1431 {==}
1432 case False{}:
1433 {==}
1434 case False{}:
1435 match z:
1436 case True{}:
1437 {==}
1438 case False{}:
1439 {==}
1440 case False{}:
1441 match q:
1442 case True{}:
1443 match r:
1444 case True{}:
1445 match z:
1446 case True{}:
1447 {==}
1448 case False{}:
1449 {==}
1450 case False{}:
1451 match z:
1452 case True{}:
1453 {==}
1454 case False{}:
1455 {==}
1456 case False{}:
1457 match r:
1458 case True{}:
1459 match z:
1460 case True{}:
1461 {==}
1462 case False{}:
1463 {==}
1464 case False{}:
1465 match z:
1466 case True{}:
1467 {==}
1468 case False{}:
1469 {==}
1470 case False{}:
1471 match p:
1472 case True{}:
1473 match q:
1474 case True{}:
1475 match r:
1476 case True{}:
1477 match z:
1478 case True{}:
1479 {==}
1480 case False{}:
1481 {==}
1482 case False{}:
1483 match z:
1484 case True{}:
1485 {==}
1486 case False{}:
1487 {==}
1488 case False{}:
1489 match r:
1490 case True{}:
1491 match z:
1492 case True{}:
1493 {==}
1494 case False{}:
1495 {==}
1496 case False{}:
1497 match z:
1498 case True{}:
1499 {==}
1500 case False{}:
1501 {==}
1502 case False{}:
1503 match q:
1504 case True{}:
1505 match r:
1506 case True{}:
1507 match z:
1508 case True{}:
1509 {==}
1510 case False{}:
1511 {==}
1512 case False{}:
1513 match z:
1514 case True{}:
1515 {==}
1516 case False{}:
1517 {==}
1518 case False{}:
1519 match r:
1520 case True{}:
1521 match z:
1522 case True{}:
1523 {==}
1524 case False{}:
1525 {==}
1526 case False{}:
1527 match z:
1528 case True{}:
1529 {==}
1530 case False{}:
1531 {==}
1532 case False{}:
1533 match e:
1534 case True{}:
1535 match p:
1536 case True{}:
1537 match q:
1538 case True{}:
1539 match r:
1540 case True{}:
1541 match z:
1542 case True{}:
1543 {==}
1544 case False{}:
1545 {==}
1546 case False{}:
1547 match z:
1548 case True{}:
1549 {==}
1550 case False{}:
1551 {==}
1552 case False{}:
1553 match r:
1554 case True{}:
1555 match z:
1556 case True{}:
1557 {==}
1558 case False{}:
1559 {==}
1560 case False{}:
1561 match z:
1562 case True{}:
1563 {==}
1564 case False{}:
1565 {==}
1566 case False{}:
1567 match q:
1568 case True{}:
1569 match r:
1570 case True{}:
1571 match z:
1572 case True{}:
1573 {==}
1574 case False{}:
1575 {==}
1576 case False{}:
1577 match z:
1578 case True{}:
1579 {==}
1580 case False{}:
1581 {==}
1582 case False{}:
1583 match r:
1584 case True{}:
1585 match z:
1586 case True{}:
1587 {==}
1588 case False{}:
1589 {==}
1590 case False{}:
1591 match z:
1592 case True{}:
1593 {==}
1594 case False{}:
1595 {==}
1596 case False{}:
1597 match p:
1598 case True{}:
1599 match q:
1600 case True{}:
1601 match r:
1602 case True{}:
1603 match z:
1604 case True{}:
1605 {==}
1606 case False{}:
1607 {==}
1608 case False{}:
1609 match z:
1610 case True{}:
1611 {==}
1612 case False{}:
1613 {==}
1614 case False{}:
1615 match r:
1616 case True{}:
1617 match z:
1618 case True{}:
1619 {==}
1620 case False{}:
1621 {==}
1622 case False{}:
1623 match z:
1624 case True{}:
1625 {==}
1626 case False{}:
1627 {==}
1628 case False{}:
1629 match q:
1630 case True{}:
1631 match r:
1632 case True{}:
1633 match z:
1634 case True{}:
1635 {==}
1636 case False{}:
1637 {==}
1638 case False{}:
1639 match z:
1640 case True{}:
1641 {==}
1642 case False{}:
1643 {==}
1644 case False{}:
1645 match r:
1646 case True{}:
1647 match z:
1648 case True{}:
1649 {==}
1650 case False{}:
1651 {==}
1652 case False{}:
1653 match z:
1654 case True{}:
1655 {==}
1656 case False{}:
1657 {==}
1658 case False{}:
1659 match ain:
1660 case True{}:
1661 match e:
1662 case True{}:
1663 match p:
1664 case True{}:
1665 match q:
1666 case True{}:
1667 match r:
1668 case True{}:
1669 match z:
1670 case True{}:
1671 {==}
1672 case False{}:
1673 {==}
1674 case False{}:
1675 match z:
1676 case True{}:
1677 {==}
1678 case False{}:
1679 {==}
1680 case False{}:
1681 match r:
1682 case True{}:
1683 match z:
1684 case True{}:
1685 {==}
1686 case False{}:
1687 {==}
1688 case False{}:
1689 match z:
1690 case True{}:
1691 {==}
1692 case False{}:
1693 {==}
1694 case False{}:
1695 match q:
1696 case True{}:
1697 match r:
1698 case True{}:
1699 match z:
1700 case True{}:
1701 {==}
1702 case False{}:
1703 {==}
1704 case False{}:
1705 match z:
1706 case True{}:
1707 {==}
1708 case False{}:
1709 {==}
1710 case False{}:
1711 match r:
1712 case True{}:
1713 match z:
1714 case True{}:
1715 {==}
1716 case False{}:
1717 {==}
1718 case False{}:
1719 match z:
1720 case True{}:
1721 {==}
1722 case False{}:
1723 {==}
1724 case False{}:
1725 match p:
1726 case True{}:
1727 match q:
1728 case True{}:
1729 match r:
1730 case True{}:
1731 match z:
1732 case True{}:
1733 {==}
1734 case False{}:
1735 {==}
1736 case False{}:
1737 match z:
1738 case True{}:
1739 {==}
1740 case False{}:
1741 {==}
1742 case False{}:
1743 match r:
1744 case True{}:
1745 match z:
1746 case True{}:
1747 {==}
1748 case False{}:
1749 {==}
1750 case False{}:
1751 match z:
1752 case True{}:
1753 {==}
1754 case False{}:
1755 {==}
1756 case False{}:
1757 match q:
1758 case True{}:
1759 match r:
1760 case True{}:
1761 match z:
1762 case True{}:
1763 {==}
1764 case False{}:
1765 {==}
1766 case False{}:
1767 match z:
1768 case True{}:
1769 {==}
1770 case False{}:
1771 {==}
1772 case False{}:
1773 match r:
1774 case True{}:
1775 match z:
1776 case True{}:
1777 {==}
1778 case False{}:
1779 {==}
1780 case False{}:
1781 match z:
1782 case True{}:
1783 {==}
1784 case False{}:
1785 {==}
1786 case False{}:
1787 match e:
1788 case True{}:
1789 match p:
1790 case True{}:
1791 match q:
1792 case True{}:
1793 match r:
1794 case True{}:
1795 match z:
1796 case True{}:
1797 {==}
1798 case False{}:
1799 {==}
1800 case False{}:
1801 match z:
1802 case True{}:
1803 {==}
1804 case False{}:
1805 {==}
1806 case False{}:
1807 match r:
1808 case True{}:
1809 match z:
1810 case True{}:
1811 {==}
1812 case False{}:
1813 {==}
1814 case False{}:
1815 match z:
1816 case True{}:
1817 {==}
1818 case False{}:
1819 {==}
1820 case False{}:
1821 match q:
1822 case True{}:
1823 match r:
1824 case True{}:
1825 match z:
1826 case True{}:
1827 {==}
1828 case False{}:
1829 {==}
1830 case False{}:
1831 match z:
1832 case True{}:
1833 {==}
1834 case False{}:
1835 {==}
1836 case False{}:
1837 match r:
1838 case True{}:
1839 match z:
1840 case True{}:
1841 {==}
1842 case False{}:
1843 {==}
1844 case False{}:
1845 match z:
1846 case True{}:
1847 {==}
1848 case False{}:
1849 {==}
1850 case False{}:
1851 match p:
1852 case True{}:
1853 match q:
1854 case True{}:
1855 match r:
1856 case True{}:
1857 match z:
1858 case True{}:
1859 {==}
1860 case False{}:
1861 {==}
1862 case False{}:
1863 match z:
1864 case True{}:
1865 {==}
1866 case False{}:
1867 {==}
1868 case False{}:
1869 match r:
1870 case True{}:
1871 match z:
1872 case True{}:
1873 {==}
1874 case False{}:
1875 {==}
1876 case False{}:
1877 match z:
1878 case True{}:
1879 {==}
1880 case False{}:
1881 {==}
1882 case False{}:
1883 match q:
1884 case True{}:
1885 match r:
1886 case True{}:
1887 match z:
1888 case True{}:
1889 {==}
1890 case False{}:
1891 {==}
1892 case False{}:
1893 match z:
1894 case True{}:
1895 {==}
1896 case False{}:
1897 {==}
1898 case False{}:
1899 match r:
1900 case True{}:
1901 match z:
1902 case True{}:
1903 {==}
1904 case False{}:
1905 {==}
1906 case False{}:
1907 match z:
1908 case True{}:
1909 {==}
1910 case False{}:
1911 {==}
1912 case False{}:
1913 match cin:
1914 case True{}:
1915 match ain:
1916 case True{}:
1917 match e:
1918 case True{}:
1919 match p:
1920 case True{}:
1921 match q:
1922 case True{}:
1923 match r:
1924 case True{}:
1925 match z:
1926 case True{}:
1927 {==}
1928 case False{}:
1929 {==}
1930 case False{}:
1931 match z:
1932 case True{}:
1933 {==}
1934 case False{}:
1935 {==}
1936 case False{}:
1937 match r:
1938 case True{}:
1939 match z:
1940 case True{}:
1941 {==}
1942 case False{}:
1943 {==}
1944 case False{}:
1945 match z:
1946 case True{}:
1947 {==}
1948 case False{}:
1949 {==}
1950 case False{}:
1951 match q:
1952 case True{}:
1953 match r:
1954 case True{}:
1955 match z:
1956 case True{}:
1957 {==}
1958 case False{}:
1959 {==}
1960 case False{}:
1961 match z:
1962 case True{}:
1963 {==}
1964 case False{}:
1965 {==}
1966 case False{}:
1967 match r:
1968 case True{}:
1969 match z:
1970 case True{}:
1971 {==}
1972 case False{}:
1973 {==}
1974 case False{}:
1975 match z:
1976 case True{}:
1977 {==}
1978 case False{}:
1979 {==}
1980 case False{}:
1981 match p:
1982 case True{}:
1983 match q:
1984 case True{}:
1985 match r:
1986 case True{}:
1987 match z:
1988 case True{}:
1989 {==}
1990 case False{}:
1991 {==}
1992 case False{}:
1993 match z:
1994 case True{}:
1995 {==}
1996 case False{}:
1997 {==}
1998 case False{}:
1999 match r:
2000 case True{}:
2001 match z:
2002 case True{}:
2003 {==}
2004 case False{}:
2005 {==}
2006 case False{}:
2007 match z:
2008 case True{}:
2009 {==}
2010 case False{}:
2011 {==}
2012 case False{}:
2013 match q:
2014 case True{}:
2015 match r:
2016 case True{}:
2017 match z:
2018 case True{}:
2019 {==}
2020 case False{}:
2021 {==}
2022 case False{}:
2023 match z:
2024 case True{}:
2025 {==}
2026 case False{}:
2027 {==}
2028 case False{}:
2029 match r:
2030 case True{}:
2031 match z:
2032 case True{}:
2033 {==}
2034 case False{}:
2035 {==}
2036 case False{}:
2037 match z:
2038 case True{}:
2039 {==}
2040 case False{}:
2041 {==}
2042 case False{}:
2043 match e:
2044 case True{}:
2045 match p:
2046 case True{}:
2047 match q:
2048 case True{}:
2049 match r:
2050 case True{}:
2051 match z:
2052 case True{}:
2053 {==}
2054 case False{}:
2055 {==}
2056 case False{}:
2057 match z:
2058 case True{}:
2059 {==}
2060 case False{}:
2061 {==}
2062 case False{}:
2063 match r:
2064 case True{}:
2065 match z:
2066 case True{}:
2067 {==}
2068 case False{}:
2069 {==}
2070 case False{}:
2071 match z:
2072 case True{}:
2073 {==}
2074 case False{}:
2075 {==}
2076 case False{}:
2077 match q:
2078 case True{}:
2079 match r:
2080 case True{}:
2081 match z:
2082 case True{}:
2083 {==}
2084 case False{}:
2085 {==}
2086 case False{}:
2087 match z:
2088 case True{}:
2089 {==}
2090 case False{}:
2091 {==}
2092 case False{}:
2093 match r:
2094 case True{}:
2095 match z:
2096 case True{}:
2097 {==}
2098 case False{}:
2099 {==}
2100 case False{}:
2101 match z:
2102 case True{}:
2103 {==}
2104 case False{}:
2105 {==}
2106 case False{}:
2107 match p:
2108 case True{}:
2109 match q:
2110 case True{}:
2111 match r:
2112 case True{}:
2113 match z:
2114 case True{}:
2115 {==}
2116 case False{}:
2117 {==}
2118 case False{}:
2119 match z:
2120 case True{}:
2121 {==}
2122 case False{}:
2123 {==}
2124 case False{}:
2125 match r:
2126 case True{}:
2127 match z:
2128 case True{}:
2129 {==}
2130 case False{}:
2131 {==}
2132 case False{}:
2133 match z:
2134 case True{}:
2135 {==}
2136 case False{}:
2137 {==}
2138 case False{}:
2139 match q:
2140 case True{}:
2141 match r:
2142 case True{}:
2143 match z:
2144 case True{}:
2145 {==}
2146 case False{}:
2147 {==}
2148 case False{}:
2149 match z:
2150 case True{}:
2151 {==}
2152 case False{}:
2153 {==}
2154 case False{}:
2155 match r:
2156 case True{}:
2157 match z:
2158 case True{}:
2159 {==}
2160 case False{}:
2161 {==}
2162 case False{}:
2163 match z:
2164 case True{}:
2165 {==}
2166 case False{}:
2167 {==}
2168 case False{}:
2169 match ain:
2170 case True{}:
2171 match e:
2172 case True{}:
2173 match p:
2174 case True{}:
2175 match q:
2176 case True{}:
2177 match r:
2178 case True{}:
2179 match z:
2180 case True{}:
2181 {==}
2182 case False{}:
2183 {==}
2184 case False{}:
2185 match z:
2186 case True{}:
2187 {==}
2188 case False{}:
2189 {==}
2190 case False{}:
2191 match r:
2192 case True{}:
2193 match z:
2194 case True{}:
2195 {==}
2196 case False{}:
2197 {==}
2198 case False{}:
2199 match z:
2200 case True{}:
2201 {==}
2202 case False{}:
2203 {==}
2204 case False{}:
2205 match q:
2206 case True{}:
2207 match r:
2208 case True{}:
2209 match z:
2210 case True{}:
2211 {==}
2212 case False{}:
2213 {==}
2214 case False{}:
2215 match z:
2216 case True{}:
2217 {==}
2218 case False{}:
2219 {==}
2220 case False{}:
2221 match r:
2222 case True{}:
2223 match z:
2224 case True{}:
2225 {==}
2226 case False{}:
2227 {==}
2228 case False{}:
2229 match z:
2230 case True{}:
2231 {==}
2232 case False{}:
2233 {==}
2234 case False{}:
2235 match p:
2236 case True{}:
2237 match q:
2238 case True{}:
2239 match r:
2240 case True{}:
2241 match z:
2242 case True{}:
2243 {==}
2244 case False{}:
2245 {==}
2246 case False{}:
2247 match z:
2248 case True{}:
2249 {==}
2250 case False{}:
2251 {==}
2252 case False{}:
2253 match r:
2254 case True{}:
2255 match z:
2256 case True{}:
2257 {==}
2258 case False{}:
2259 {==}
2260 case False{}:
2261 match z:
2262 case True{}:
2263 {==}
2264 case False{}:
2265 {==}
2266 case False{}:
2267 match q:
2268 case True{}:
2269 match r:
2270 case True{}:
2271 match z:
2272 case True{}:
2273 {==}
2274 case False{}:
2275 {==}
2276 case False{}:
2277 match z:
2278 case True{}:
2279 {==}
2280 case False{}:
2281 {==}
2282 case False{}:
2283 match r:
2284 case True{}:
2285 match z:
2286 case True{}:
2287 {==}
2288 case False{}:
2289 {==}
2290 case False{}:
2291 match z:
2292 case True{}:
2293 {==}
2294 case False{}:
2295 {==}
2296 case False{}:
2297 match e:
2298 case True{}:
2299 match p:
2300 case True{}:
2301 match q:
2302 case True{}:
2303 match r:
2304 case True{}:
2305 match z:
2306 case True{}:
2307 {==}
2308 case False{}:
2309 {==}
2310 case False{}:
2311 match z:
2312 case True{}:
2313 {==}
2314 case False{}:
2315 {==}
2316 case False{}:
2317 match r:
2318 case True{}:
2319 match z:
2320 case True{}:
2321 {==}
2322 case False{}:
2323 {==}
2324 case False{}:
2325 match z:
2326 case True{}:
2327 {==}
2328 case False{}:
2329 {==}
2330 case False{}:
2331 match q:
2332 case True{}:
2333 match r:
2334 case True{}:
2335 match z:
2336 case True{}:
2337 {==}
2338 case False{}:
2339 {==}
2340 case False{}:
2341 match z:
2342 case True{}:
2343 {==}
2344 case False{}:
2345 {==}
2346 case False{}:
2347 match r:
2348 case True{}:
2349 match z:
2350 case True{}:
2351 {==}
2352 case False{}:
2353 {==}
2354 case False{}:
2355 match z:
2356 case True{}:
2357 {==}
2358 case False{}:
2359 {==}
2360 case False{}:
2361 match p:
2362 case True{}:
2363 match q:
2364 case True{}:
2365 match r:
2366 case True{}:
2367 match z:
2368 case True{}:
2369 {==}
2370 case False{}:
2371 {==}
2372 case False{}:
2373 match z:
2374 case True{}:
2375 {==}
2376 case False{}:
2377 {==}
2378 case False{}:
2379 match r:
2380 case True{}:
2381 match z:
2382 case True{}:
2383 {==}
2384 case False{}:
2385 {==}
2386 case False{}:
2387 match z:
2388 case True{}:
2389 {==}
2390 case False{}:
2391 {==}
2392 case False{}:
2393 match q:
2394 case True{}:
2395 match r:
2396 case True{}:
2397 match z:
2398 case True{}:
2399 {==}
2400 case False{}:
2401 {==}
2402 case False{}:
2403 match z:
2404 case True{}:
2405 {==}
2406 case False{}:
2407 {==}
2408 case False{}:
2409 match r:
2410 case True{}:
2411 match z:
2412 case True{}:
2413 {==}
2414 case False{}:
2415 {==}
2416 case False{}:
2417 match z:
2418 case True{}:
2419 {==}
2420 case False{}:
2421 {==}