def aria_sb31
import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOFimport Base
import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as A
1730# BEGIN GENERATED by gen/proof.py: aria
1731# each S-box and its inverse undo each other on every byte
1732def aria_sb31(w0: Word(8n)) -> {w0 == A.aria.sb3(A.aria.sb1(w0)) : Word(8n)}:
1733 match w0:
1734 case WCon{False{}, w1}:
1735 match w1:
1736 case WCon{False{}, w2}:
1737 match w2:
1738 case WCon{False{}, w3}:
1739 match w3:
1740 case WCon{False{}, w4}:
1741 match w4:
1742 case WCon{False{}, w5}:
1743 match w5:
1744 case WCon{False{}, w6}:
1745 match w6:
1746 case WCon{False{}, w7}:
1747 match w7:
1748 case WCon{False{}, w8}:
1749 match w8:
1750 case WNil{}:
1751 {==}
1752 case WCon{True{}, w8}:
1753 match w8:
1754 case WNil{}:
1755 {==}
1756 case WCon{True{}, w7}:
1757 match w7:
1758 case WCon{False{}, w8}:
1759 match w8:
1760 case WNil{}:
1761 {==}
1762 case WCon{True{}, w8}:
1763 match w8:
1764 case WNil{}:
1765 {==}
1766 case WCon{True{}, w6}:
1767 match w6:
1768 case WCon{False{}, w7}:
1769 match w7:
1770 case WCon{False{}, w8}:
1771 match w8:
1772 case WNil{}:
1773 {==}
1774 case WCon{True{}, w8}:
1775 match w8:
1776 case WNil{}:
1777 {==}
1778 case WCon{True{}, w7}:
1779 match w7:
1780 case WCon{False{}, w8}:
1781 match w8:
1782 case WNil{}:
1783 {==}
1784 case WCon{True{}, w8}:
1785 match w8:
1786 case WNil{}:
1787 {==}
1788 case WCon{True{}, w5}:
1789 match w5:
1790 case WCon{False{}, w6}:
1791 match w6:
1792 case WCon{False{}, w7}:
1793 match w7:
1794 case WCon{False{}, w8}:
1795 match w8:
1796 case WNil{}:
1797 {==}
1798 case WCon{True{}, w8}:
1799 match w8:
1800 case WNil{}:
1801 {==}
1802 case WCon{True{}, w7}:
1803 match w7:
1804 case WCon{False{}, w8}:
1805 match w8:
1806 case WNil{}:
1807 {==}
1808 case WCon{True{}, w8}:
1809 match w8:
1810 case WNil{}:
1811 {==}
1812 case WCon{True{}, w6}:
1813 match w6:
1814 case WCon{False{}, w7}:
1815 match w7:
1816 case WCon{False{}, w8}:
1817 match w8:
1818 case WNil{}:
1819 {==}
1820 case WCon{True{}, w8}:
1821 match w8:
1822 case WNil{}:
1823 {==}
1824 case WCon{True{}, w7}:
1825 match w7:
1826 case WCon{False{}, w8}:
1827 match w8:
1828 case WNil{}:
1829 {==}
1830 case WCon{True{}, w8}:
1831 match w8:
1832 case WNil{}:
1833 {==}
1834 case WCon{True{}, w4}:
1835 match w4:
1836 case WCon{False{}, w5}:
1837 match w5:
1838 case WCon{False{}, w6}:
1839 match w6:
1840 case WCon{False{}, w7}:
1841 match w7:
1842 case WCon{False{}, w8}:
1843 match w8:
1844 case WNil{}:
1845 {==}
1846 case WCon{True{}, w8}:
1847 match w8:
1848 case WNil{}:
1849 {==}
1850 case WCon{True{}, w7}:
1851 match w7:
1852 case WCon{False{}, w8}:
1853 match w8:
1854 case WNil{}:
1855 {==}
1856 case WCon{True{}, w8}:
1857 match w8:
1858 case WNil{}:
1859 {==}
1860 case WCon{True{}, w6}:
1861 match w6:
1862 case WCon{False{}, w7}:
1863 match w7:
1864 case WCon{False{}, w8}:
1865 match w8:
1866 case WNil{}:
1867 {==}
1868 case WCon{True{}, w8}:
1869 match w8:
1870 case WNil{}:
1871 {==}
1872 case WCon{True{}, w7}:
1873 match w7:
1874 case WCon{False{}, w8}:
1875 match w8:
1876 case WNil{}:
1877 {==}
1878 case WCon{True{}, w8}:
1879 match w8:
1880 case WNil{}:
1881 {==}
1882 case WCon{True{}, w5}:
1883 match w5:
1884 case WCon{False{}, w6}:
1885 match w6:
1886 case WCon{False{}, w7}:
1887 match w7:
1888 case WCon{False{}, w8}:
1889 match w8:
1890 case WNil{}:
1891 {==}
1892 case WCon{True{}, w8}:
1893 match w8:
1894 case WNil{}:
1895 {==}
1896 case WCon{True{}, w7}:
1897 match w7:
1898 case WCon{False{}, w8}:
1899 match w8:
1900 case WNil{}:
1901 {==}
1902 case WCon{True{}, w8}:
1903 match w8:
1904 case WNil{}:
1905 {==}
1906 case WCon{True{}, w6}:
1907 match w6:
1908 case WCon{False{}, w7}:
1909 match w7:
1910 case WCon{False{}, w8}:
1911 match w8:
1912 case WNil{}:
1913 {==}
1914 case WCon{True{}, w8}:
1915 match w8:
1916 case WNil{}:
1917 {==}
1918 case WCon{True{}, w7}:
1919 match w7:
1920 case WCon{False{}, w8}:
1921 match w8:
1922 case WNil{}:
1923 {==}
1924 case WCon{True{}, w8}:
1925 match w8:
1926 case WNil{}:
1927 {==}
1928 case WCon{True{}, w3}:
1929 match w3:
1930 case WCon{False{}, w4}:
1931 match w4:
1932 case WCon{False{}, w5}:
1933 match w5:
1934 case WCon{False{}, w6}:
1935 match w6:
1936 case WCon{False{}, w7}:
1937 match w7:
1938 case WCon{False{}, w8}:
1939 match w8:
1940 case WNil{}:
1941 {==}
1942 case WCon{True{}, w8}:
1943 match w8:
1944 case WNil{}:
1945 {==}
1946 case WCon{True{}, w7}:
1947 match w7:
1948 case WCon{False{}, w8}:
1949 match w8:
1950 case WNil{}:
1951 {==}
1952 case WCon{True{}, w8}:
1953 match w8:
1954 case WNil{}:
1955 {==}
1956 case WCon{True{}, w6}:
1957 match w6:
1958 case WCon{False{}, w7}:
1959 match w7:
1960 case WCon{False{}, w8}:
1961 match w8:
1962 case WNil{}:
1963 {==}
1964 case WCon{True{}, w8}:
1965 match w8:
1966 case WNil{}:
1967 {==}
1968 case WCon{True{}, w7}:
1969 match w7:
1970 case WCon{False{}, w8}:
1971 match w8:
1972 case WNil{}:
1973 {==}
1974 case WCon{True{}, w8}:
1975 match w8:
1976 case WNil{}:
1977 {==}
1978 case WCon{True{}, w5}:
1979 match w5:
1980 case WCon{False{}, w6}:
1981 match w6:
1982 case WCon{False{}, w7}:
1983 match w7:
1984 case WCon{False{}, w8}:
1985 match w8:
1986 case WNil{}:
1987 {==}
1988 case WCon{True{}, w8}:
1989 match w8:
1990 case WNil{}:
1991 {==}
1992 case WCon{True{}, w7}:
1993 match w7:
1994 case WCon{False{}, w8}:
1995 match w8:
1996 case WNil{}:
1997 {==}
1998 case WCon{True{}, w8}:
1999 match w8:
2000 case WNil{}:
2001 {==}
2002 case WCon{True{}, w6}:
2003 match w6:
2004 case WCon{False{}, w7}:
2005 match w7:
2006 case WCon{False{}, w8}:
2007 match w8:
2008 case WNil{}:
2009 {==}
2010 case WCon{True{}, w8}:
2011 match w8:
2012 case WNil{}:
2013 {==}
2014 case WCon{True{}, w7}:
2015 match w7:
2016 case WCon{False{}, w8}:
2017 match w8:
2018 case WNil{}:
2019 {==}
2020 case WCon{True{}, w8}:
2021 match w8:
2022 case WNil{}:
2023 {==}
2024 case WCon{True{}, w4}:
2025 match w4:
2026 case WCon{False{}, w5}:
2027 match w5:
2028 case WCon{False{}, w6}:
2029 match w6:
2030 case WCon{False{}, w7}:
2031 match w7:
2032 case WCon{False{}, w8}:
2033 match w8:
2034 case WNil{}:
2035 {==}
2036 case WCon{True{}, w8}:
2037 match w8:
2038 case WNil{}:
2039 {==}
2040 case WCon{True{}, w7}:
2041 match w7:
2042 case WCon{False{}, w8}:
2043 match w8:
2044 case WNil{}:
2045 {==}
2046 case WCon{True{}, w8}:
2047 match w8:
2048 case WNil{}:
2049 {==}
2050 case WCon{True{}, w6}:
2051 match w6:
2052 case WCon{False{}, w7}:
2053 match w7:
2054 case WCon{False{}, w8}:
2055 match w8:
2056 case WNil{}:
2057 {==}
2058 case WCon{True{}, w8}:
2059 match w8:
2060 case WNil{}:
2061 {==}
2062 case WCon{True{}, w7}:
2063 match w7:
2064 case WCon{False{}, w8}:
2065 match w8:
2066 case WNil{}:
2067 {==}
2068 case WCon{True{}, w8}:
2069 match w8:
2070 case WNil{}:
2071 {==}
2072 case WCon{True{}, w5}:
2073 match w5:
2074 case WCon{False{}, w6}:
2075 match w6:
2076 case WCon{False{}, w7}:
2077 match w7:
2078 case WCon{False{}, w8}:
2079 match w8:
2080 case WNil{}:
2081 {==}
2082 case WCon{True{}, w8}:
2083 match w8:
2084 case WNil{}:
2085 {==}
2086 case WCon{True{}, w7}:
2087 match w7:
2088 case WCon{False{}, w8}:
2089 match w8:
2090 case WNil{}:
2091 {==}
2092 case WCon{True{}, w8}:
2093 match w8:
2094 case WNil{}:
2095 {==}
2096 case WCon{True{}, w6}:
2097 match w6:
2098 case WCon{False{}, w7}:
2099 match w7:
2100 case WCon{False{}, w8}:
2101 match w8:
2102 case WNil{}:
2103 {==}
2104 case WCon{True{}, w8}:
2105 match w8:
2106 case WNil{}:
2107 {==}
2108 case WCon{True{}, w7}:
2109 match w7:
2110 case WCon{False{}, w8}:
2111 match w8:
2112 case WNil{}:
2113 {==}
2114 case WCon{True{}, w8}:
2115 match w8:
2116 case WNil{}:
2117 {==}
2118 case WCon{True{}, w2}:
2119 match w2:
2120 case WCon{False{}, w3}:
2121 match w3:
2122 case WCon{False{}, w4}:
2123 match w4:
2124 case WCon{False{}, w5}:
2125 match w5:
2126 case WCon{False{}, w6}:
2127 match w6:
2128 case WCon{False{}, w7}:
2129 match w7:
2130 case WCon{False{}, w8}:
2131 match w8:
2132 case WNil{}:
2133 {==}
2134 case WCon{True{}, w8}:
2135 match w8:
2136 case WNil{}:
2137 {==}
2138 case WCon{True{}, w7}:
2139 match w7:
2140 case WCon{False{}, w8}:
2141 match w8:
2142 case WNil{}:
2143 {==}
2144 case WCon{True{}, w8}:
2145 match w8:
2146 case WNil{}:
2147 {==}
2148 case WCon{True{}, w6}:
2149 match w6:
2150 case WCon{False{}, w7}:
2151 match w7:
2152 case WCon{False{}, w8}:
2153 match w8:
2154 case WNil{}:
2155 {==}
2156 case WCon{True{}, w8}:
2157 match w8:
2158 case WNil{}:
2159 {==}
2160 case WCon{True{}, w7}:
2161 match w7:
2162 case WCon{False{}, w8}:
2163 match w8:
2164 case WNil{}:
2165 {==}
2166 case WCon{True{}, w8}:
2167 match w8:
2168 case WNil{}:
2169 {==}
2170 case WCon{True{}, w5}:
2171 match w5:
2172 case WCon{False{}, w6}:
2173 match w6:
2174 case WCon{False{}, w7}:
2175 match w7:
2176 case WCon{False{}, w8}:
2177 match w8:
2178 case WNil{}:
2179 {==}
2180 case WCon{True{}, w8}:
2181 match w8:
2182 case WNil{}:
2183 {==}
2184 case WCon{True{}, w7}:
2185 match w7:
2186 case WCon{False{}, w8}:
2187 match w8:
2188 case WNil{}:
2189 {==}
2190 case WCon{True{}, w8}:
2191 match w8:
2192 case WNil{}:
2193 {==}
2194 case WCon{True{}, w6}:
2195 match w6:
2196 case WCon{False{}, w7}:
2197 match w7:
2198 case WCon{False{}, w8}:
2199 match w8:
2200 case WNil{}:
2201 {==}
2202 case WCon{True{}, w8}:
2203 match w8:
2204 case WNil{}:
2205 {==}
2206 case WCon{True{}, w7}:
2207 match w7:
2208 case WCon{False{}, w8}:
2209 match w8:
2210 case WNil{}:
2211 {==}
2212 case WCon{True{}, w8}:
2213 match w8:
2214 case WNil{}:
2215 {==}
2216 case WCon{True{}, w4}:
2217 match w4:
2218 case WCon{False{}, w5}:
2219 match w5:
2220 case WCon{False{}, w6}:
2221 match w6:
2222 case WCon{False{}, w7}:
2223 match w7:
2224 case WCon{False{}, w8}:
2225 match w8:
2226 case WNil{}:
2227 {==}
2228 case WCon{True{}, w8}:
2229 match w8:
2230 case WNil{}:
2231 {==}
2232 case WCon{True{}, w7}:
2233 match w7:
2234 case WCon{False{}, w8}:
2235 match w8:
2236 case WNil{}:
2237 {==}
2238 case WCon{True{}, w8}:
2239 match w8:
2240 case WNil{}:
2241 {==}
2242 case WCon{True{}, w6}:
2243 match w6:
2244 case WCon{False{}, w7}:
2245 match w7:
2246 case WCon{False{}, w8}:
2247 match w8:
2248 case WNil{}:
2249 {==}
2250 case WCon{True{}, w8}:
2251 match w8:
2252 case WNil{}:
2253 {==}
2254 case WCon{True{}, w7}:
2255 match w7:
2256 case WCon{False{}, w8}:
2257 match w8:
2258 case WNil{}:
2259 {==}
2260 case WCon{True{}, w8}:
2261 match w8:
2262 case WNil{}:
2263 {==}
2264 case WCon{True{}, w5}:
2265 match w5:
2266 case WCon{False{}, w6}:
2267 match w6:
2268 case WCon{False{}, w7}:
2269 match w7:
2270 case WCon{False{}, w8}:
2271 match w8:
2272 case WNil{}:
2273 {==}
2274 case WCon{True{}, w8}:
2275 match w8:
2276 case WNil{}:
2277 {==}
2278 case WCon{True{}, w7}:
2279 match w7:
2280 case WCon{False{}, w8}:
2281 match w8:
2282 case WNil{}:
2283 {==}
2284 case WCon{True{}, w8}:
2285 match w8:
2286 case WNil{}:
2287 {==}
2288 case WCon{True{}, w6}:
2289 match w6:
2290 case WCon{False{}, w7}:
2291 match w7:
2292 case WCon{False{}, w8}:
2293 match w8:
2294 case WNil{}:
2295 {==}
2296 case WCon{True{}, w8}:
2297 match w8:
2298 case WNil{}:
2299 {==}
2300 case WCon{True{}, w7}:
2301 match w7:
2302 case WCon{False{}, w8}:
2303 match w8:
2304 case WNil{}:
2305 {==}
2306 case WCon{True{}, w8}:
2307 match w8:
2308 case WNil{}:
2309 {==}
2310 case WCon{True{}, w3}:
2311 match w3:
2312 case WCon{False{}, w4}:
2313 match w4:
2314 case WCon{False{}, w5}:
2315 match w5:
2316 case WCon{False{}, w6}:
2317 match w6:
2318 case WCon{False{}, w7}:
2319 match w7:
2320 case WCon{False{}, w8}:
2321 match w8:
2322 case WNil{}:
2323 {==}
2324 case WCon{True{}, w8}:
2325 match w8:
2326 case WNil{}:
2327 {==}
2328 case WCon{True{}, w7}:
2329 match w7:
2330 case WCon{False{}, w8}:
2331 match w8:
2332 case WNil{}:
2333 {==}
2334 case WCon{True{}, w8}:
2335 match w8:
2336 case WNil{}:
2337 {==}
2338 case WCon{True{}, w6}:
2339 match w6:
2340 case WCon{False{}, w7}:
2341 match w7:
2342 case WCon{False{}, w8}:
2343 match w8:
2344 case WNil{}:
2345 {==}
2346 case WCon{True{}, w8}:
2347 match w8:
2348 case WNil{}:
2349 {==}
2350 case WCon{True{}, w7}:
2351 match w7:
2352 case WCon{False{}, w8}:
2353 match w8:
2354 case WNil{}:
2355 {==}
2356 case WCon{True{}, w8}:
2357 match w8:
2358 case WNil{}:
2359 {==}
2360 case WCon{True{}, w5}:
2361 match w5:
2362 case WCon{False{}, w6}:
2363 match w6:
2364 case WCon{False{}, w7}:
2365 match w7:
2366 case WCon{False{}, w8}:
2367 match w8:
2368 case WNil{}:
2369 {==}
2370 case WCon{True{}, w8}:
2371 match w8:
2372 case WNil{}:
2373 {==}
2374 case WCon{True{}, w7}:
2375 match w7:
2376 case WCon{False{}, w8}:
2377 match w8:
2378 case WNil{}:
2379 {==}
2380 case WCon{True{}, w8}:
2381 match w8:
2382 case WNil{}:
2383 {==}
2384 case WCon{True{}, w6}:
2385 match w6:
2386 case WCon{False{}, w7}:
2387 match w7:
2388 case WCon{False{}, w8}:
2389 match w8:
2390 case WNil{}:
2391 {==}
2392 case WCon{True{}, w8}:
2393 match w8:
2394 case WNil{}:
2395 {==}
2396 case WCon{True{}, w7}:
2397 match w7:
2398 case WCon{False{}, w8}:
2399 match w8:
2400 case WNil{}:
2401 {==}
2402 case WCon{True{}, w8}:
2403 match w8:
2404 case WNil{}:
2405 {==}
2406 case WCon{True{}, w4}:
2407 match w4:
2408 case WCon{False{}, w5}:
2409 match w5:
2410 case WCon{False{}, w6}:
2411 match w6:
2412 case WCon{False{}, w7}:
2413 match w7:
2414 case WCon{False{}, w8}:
2415 match w8:
2416 case WNil{}:
2417 {==}
2418 case WCon{True{}, w8}:
2419 match w8:
2420 case WNil{}:
2421 {==}
2422 case WCon{True{}, w7}:
2423 match w7:
2424 case WCon{False{}, w8}:
2425 match w8:
2426 case WNil{}:
2427 {==}
2428 case WCon{True{}, w8}:
2429 match w8:
2430 case WNil{}:
2431 {==}
2432 case WCon{True{}, w6}:
2433 match w6:
2434 case WCon{False{}, w7}:
2435 match w7:
2436 case WCon{False{}, w8}:
2437 match w8:
2438 case WNil{}:
2439 {==}
2440 case WCon{True{}, w8}:
2441 match w8:
2442 case WNil{}:
2443 {==}
2444 case WCon{True{}, w7}:
2445 match w7:
2446 case WCon{False{}, w8}:
2447 match w8:
2448 case WNil{}:
2449 {==}
2450 case WCon{True{}, w8}:
2451 match w8:
2452 case WNil{}:
2453 {==}
2454 case WCon{True{}, w5}:
2455 match w5:
2456 case WCon{False{}, w6}:
2457 match w6:
2458 case WCon{False{}, w7}:
2459 match w7:
2460 case WCon{False{}, w8}:
2461 match w8:
2462 case WNil{}:
2463 {==}
2464 case WCon{True{}, w8}:
2465 match w8:
2466 case WNil{}:
2467 {==}
2468 case WCon{True{}, w7}:
2469 match w7:
2470 case WCon{False{}, w8}:
2471 match w8:
2472 case WNil{}:
2473 {==}
2474 case WCon{True{}, w8}:
2475 match w8:
2476 case WNil{}:
2477 {==}
2478 case WCon{True{}, w6}:
2479 match w6:
2480 case WCon{False{}, w7}:
2481 match w7:
2482 case WCon{False{}, w8}:
2483 match w8:
2484 case WNil{}:
2485 {==}
2486 case WCon{True{}, w8}:
2487 match w8:
2488 case WNil{}:
2489 {==}
2490 case WCon{True{}, w7}:
2491 match w7:
2492 case WCon{False{}, w8}:
2493 match w8:
2494 case WNil{}:
2495 {==}
2496 case WCon{True{}, w8}:
2497 match w8:
2498 case WNil{}:
2499 {==}
2500 case WCon{True{}, w1}:
2501 match w1:
2502 case WCon{False{}, w2}:
2503 match w2:
2504 case WCon{False{}, w3}:
2505 match w3:
2506 case WCon{False{}, w4}:
2507 match w4:
2508 case WCon{False{}, w5}:
2509 match w5:
2510 case WCon{False{}, w6}:
2511 match w6:
2512 case WCon{False{}, w7}:
2513 match w7:
2514 case WCon{False{}, w8}:
2515 match w8:
2516 case WNil{}:
2517 {==}
2518 case WCon{True{}, w8}:
2519 match w8:
2520 case WNil{}:
2521 {==}
2522 case WCon{True{}, w7}:
2523 match w7:
2524 case WCon{False{}, w8}:
2525 match w8:
2526 case WNil{}:
2527 {==}
2528 case WCon{True{}, w8}:
2529 match w8:
2530 case WNil{}:
2531 {==}
2532 case WCon{True{}, w6}:
2533 match w6:
2534 case WCon{False{}, w7}:
2535 match w7:
2536 case WCon{False{}, w8}:
2537 match w8:
2538 case WNil{}:
2539 {==}
2540 case WCon{True{}, w8}:
2541 match w8:
2542 case WNil{}:
2543 {==}
2544 case WCon{True{}, w7}:
2545 match w7:
2546 case WCon{False{}, w8}:
2547 match w8:
2548 case WNil{}:
2549 {==}
2550 case WCon{True{}, w8}:
2551 match w8:
2552 case WNil{}:
2553 {==}
2554 case WCon{True{}, w5}:
2555 match w5:
2556 case WCon{False{}, w6}:
2557 match w6:
2558 case WCon{False{}, w7}:
2559 match w7:
2560 case WCon{False{}, w8}:
2561 match w8:
2562 case WNil{}:
2563 {==}
2564 case WCon{True{}, w8}:
2565 match w8:
2566 case WNil{}:
2567 {==}
2568 case WCon{True{}, w7}:
2569 match w7:
2570 case WCon{False{}, w8}:
2571 match w8:
2572 case WNil{}:
2573 {==}
2574 case WCon{True{}, w8}:
2575 match w8:
2576 case WNil{}:
2577 {==}
2578 case WCon{True{}, w6}:
2579 match w6:
2580 case WCon{False{}, w7}:
2581 match w7:
2582 case WCon{False{}, w8}:
2583 match w8:
2584 case WNil{}:
2585 {==}
2586 case WCon{True{}, w8}:
2587 match w8:
2588 case WNil{}:
2589 {==}
2590 case WCon{True{}, w7}:
2591 match w7:
2592 case WCon{False{}, w8}:
2593 match w8:
2594 case WNil{}:
2595 {==}
2596 case WCon{True{}, w8}:
2597 match w8:
2598 case WNil{}:
2599 {==}
2600 case WCon{True{}, w4}:
2601 match w4:
2602 case WCon{False{}, w5}:
2603 match w5:
2604 case WCon{False{}, w6}:
2605 match w6:
2606 case WCon{False{}, w7}:
2607 match w7:
2608 case WCon{False{}, w8}:
2609 match w8:
2610 case WNil{}:
2611 {==}
2612 case WCon{True{}, w8}:
2613 match w8:
2614 case WNil{}:
2615 {==}
2616 case WCon{True{}, w7}:
2617 match w7:
2618 case WCon{False{}, w8}:
2619 match w8:
2620 case WNil{}:
2621 {==}
2622 case WCon{True{}, w8}:
2623 match w8:
2624 case WNil{}:
2625 {==}
2626 case WCon{True{}, w6}:
2627 match w6:
2628 case WCon{False{}, w7}:
2629 match w7:
2630 case WCon{False{}, w8}:
2631 match w8:
2632 case WNil{}:
2633 {==}
2634 case WCon{True{}, w8}:
2635 match w8:
2636 case WNil{}:
2637 {==}
2638 case WCon{True{}, w7}:
2639 match w7:
2640 case WCon{False{}, w8}:
2641 match w8:
2642 case WNil{}:
2643 {==}
2644 case WCon{True{}, w8}:
2645 match w8:
2646 case WNil{}:
2647 {==}
2648 case WCon{True{}, w5}:
2649 match w5:
2650 case WCon{False{}, w6}:
2651 match w6:
2652 case WCon{False{}, w7}:
2653 match w7:
2654 case WCon{False{}, w8}:
2655 match w8:
2656 case WNil{}:
2657 {==}
2658 case WCon{True{}, w8}:
2659 match w8:
2660 case WNil{}:
2661 {==}
2662 case WCon{True{}, w7}:
2663 match w7:
2664 case WCon{False{}, w8}:
2665 match w8:
2666 case WNil{}:
2667 {==}
2668 case WCon{True{}, w8}:
2669 match w8:
2670 case WNil{}:
2671 {==}
2672 case WCon{True{}, w6}:
2673 match w6:
2674 case WCon{False{}, w7}:
2675 match w7:
2676 case WCon{False{}, w8}:
2677 match w8:
2678 case WNil{}:
2679 {==}
2680 case WCon{True{}, w8}:
2681 match w8:
2682 case WNil{}:
2683 {==}
2684 case WCon{True{}, w7}:
2685 match w7:
2686 case WCon{False{}, w8}:
2687 match w8:
2688 case WNil{}:
2689 {==}
2690 case WCon{True{}, w8}:
2691 match w8:
2692 case WNil{}:
2693 {==}
2694 case WCon{True{}, w3}:
2695 match w3:
2696 case WCon{False{}, w4}:
2697 match w4:
2698 case WCon{False{}, w5}:
2699 match w5:
2700 case WCon{False{}, w6}:
2701 match w6:
2702 case WCon{False{}, w7}:
2703 match w7:
2704 case WCon{False{}, w8}:
2705 match w8:
2706 case WNil{}:
2707 {==}
2708 case WCon{True{}, w8}:
2709 match w8:
2710 case WNil{}:
2711 {==}
2712 case WCon{True{}, w7}:
2713 match w7:
2714 case WCon{False{}, w8}:
2715 match w8:
2716 case WNil{}:
2717 {==}
2718 case WCon{True{}, w8}:
2719 match w8:
2720 case WNil{}:
2721 {==}
2722 case WCon{True{}, w6}:
2723 match w6:
2724 case WCon{False{}, w7}:
2725 match w7:
2726 case WCon{False{}, w8}:
2727 match w8:
2728 case WNil{}:
2729 {==}
2730 case WCon{True{}, w8}:
2731 match w8:
2732 case WNil{}:
2733 {==}
2734 case WCon{True{}, w7}:
2735 match w7:
2736 case WCon{False{}, w8}:
2737 match w8:
2738 case WNil{}:
2739 {==}
2740 case WCon{True{}, w8}:
2741 match w8:
2742 case WNil{}:
2743 {==}
2744 case WCon{True{}, w5}:
2745 match w5:
2746 case WCon{False{}, w6}:
2747 match w6:
2748 case WCon{False{}, w7}:
2749 match w7:
2750 case WCon{False{}, w8}:
2751 match w8:
2752 case WNil{}:
2753 {==}
2754 case WCon{True{}, w8}:
2755 match w8:
2756 case WNil{}:
2757 {==}
2758 case WCon{True{}, w7}:
2759 match w7:
2760 case WCon{False{}, w8}:
2761 match w8:
2762 case WNil{}:
2763 {==}
2764 case WCon{True{}, w8}:
2765 match w8:
2766 case WNil{}:
2767 {==}
2768 case WCon{True{}, w6}:
2769 match w6:
2770 case WCon{False{}, w7}:
2771 match w7:
2772 case WCon{False{}, w8}:
2773 match w8:
2774 case WNil{}:
2775 {==}
2776 case WCon{True{}, w8}:
2777 match w8:
2778 case WNil{}:
2779 {==}
2780 case WCon{True{}, w7}:
2781 match w7:
2782 case WCon{False{}, w8}:
2783 match w8:
2784 case WNil{}:
2785 {==}
2786 case WCon{True{}, w8}:
2787 match w8:
2788 case WNil{}:
2789 {==}
2790 case WCon{True{}, w4}:
2791 match w4:
2792 case WCon{False{}, w5}:
2793 match w5:
2794 case WCon{False{}, w6}:
2795 match w6:
2796 case WCon{False{}, w7}:
2797 match w7:
2798 case WCon{False{}, w8}:
2799 match w8:
2800 case WNil{}:
2801 {==}
2802 case WCon{True{}, w8}:
2803 match w8:
2804 case WNil{}:
2805 {==}
2806 case WCon{True{}, w7}:
2807 match w7:
2808 case WCon{False{}, w8}:
2809 match w8:
2810 case WNil{}:
2811 {==}
2812 case WCon{True{}, w8}:
2813 match w8:
2814 case WNil{}:
2815 {==}
2816 case WCon{True{}, w6}:
2817 match w6:
2818 case WCon{False{}, w7}:
2819 match w7:
2820 case WCon{False{}, w8}:
2821 match w8:
2822 case WNil{}:
2823 {==}
2824 case WCon{True{}, w8}:
2825 match w8:
2826 case WNil{}:
2827 {==}
2828 case WCon{True{}, w7}:
2829 match w7:
2830 case WCon{False{}, w8}:
2831 match w8:
2832 case WNil{}:
2833 {==}
2834 case WCon{True{}, w8}:
2835 match w8:
2836 case WNil{}:
2837 {==}
2838 case WCon{True{}, w5}:
2839 match w5:
2840 case WCon{False{}, w6}:
2841 match w6:
2842 case WCon{False{}, w7}:
2843 match w7:
2844 case WCon{False{}, w8}:
2845 match w8:
2846 case WNil{}:
2847 {==}
2848 case WCon{True{}, w8}:
2849 match w8:
2850 case WNil{}:
2851 {==}
2852 case WCon{True{}, w7}:
2853 match w7:
2854 case WCon{False{}, w8}:
2855 match w8:
2856 case WNil{}:
2857 {==}
2858 case WCon{True{}, w8}:
2859 match w8:
2860 case WNil{}:
2861 {==}
2862 case WCon{True{}, w6}:
2863 match w6:
2864 case WCon{False{}, w7}:
2865 match w7:
2866 case WCon{False{}, w8}:
2867 match w8:
2868 case WNil{}:
2869 {==}
2870 case WCon{True{}, w8}:
2871 match w8:
2872 case WNil{}:
2873 {==}
2874 case WCon{True{}, w7}:
2875 match w7:
2876 case WCon{False{}, w8}:
2877 match w8:
2878 case WNil{}:
2879 {==}
2880 case WCon{True{}, w8}:
2881 match w8:
2882 case WNil{}:
2883 {==}
2884 case WCon{True{}, w2}:
2885 match w2:
2886 case WCon{False{}, w3}:
2887 match w3:
2888 case WCon{False{}, w4}:
2889 match w4:
2890 case WCon{False{}, w5}:
2891 match w5:
2892 case WCon{False{}, w6}:
2893 match w6:
2894 case WCon{False{}, w7}:
2895 match w7:
2896 case WCon{False{}, w8}:
2897 match w8:
2898 case WNil{}:
2899 {==}
2900 case WCon{True{}, w8}:
2901 match w8:
2902 case WNil{}:
2903 {==}
2904 case WCon{True{}, w7}:
2905 match w7:
2906 case WCon{False{}, w8}:
2907 match w8:
2908 case WNil{}:
2909 {==}
2910 case WCon{True{}, w8}:
2911 match w8:
2912 case WNil{}:
2913 {==}
2914 case WCon{True{}, w6}:
2915 match w6:
2916 case WCon{False{}, w7}:
2917 match w7:
2918 case WCon{False{}, w8}:
2919 match w8:
2920 case WNil{}:
2921 {==}
2922 case WCon{True{}, w8}:
2923 match w8:
2924 case WNil{}:
2925 {==}
2926 case WCon{True{}, w7}:
2927 match w7:
2928 case WCon{False{}, w8}:
2929 match w8:
2930 case WNil{}:
2931 {==}
2932 case WCon{True{}, w8}:
2933 match w8:
2934 case WNil{}:
2935 {==}
2936 case WCon{True{}, w5}:
2937 match w5:
2938 case WCon{False{}, w6}:
2939 match w6:
2940 case WCon{False{}, w7}:
2941 match w7:
2942 case WCon{False{}, w8}:
2943 match w8:
2944 case WNil{}:
2945 {==}
2946 case WCon{True{}, w8}:
2947 match w8:
2948 case WNil{}:
2949 {==}
2950 case WCon{True{}, w7}:
2951 match w7:
2952 case WCon{False{}, w8}:
2953 match w8:
2954 case WNil{}:
2955 {==}
2956 case WCon{True{}, w8}:
2957 match w8:
2958 case WNil{}:
2959 {==}
2960 case WCon{True{}, w6}:
2961 match w6:
2962 case WCon{False{}, w7}:
2963 match w7:
2964 case WCon{False{}, w8}:
2965 match w8:
2966 case WNil{}:
2967 {==}
2968 case WCon{True{}, w8}:
2969 match w8:
2970 case WNil{}:
2971 {==}
2972 case WCon{True{}, w7}:
2973 match w7:
2974 case WCon{False{}, w8}:
2975 match w8:
2976 case WNil{}:
2977 {==}
2978 case WCon{True{}, w8}:
2979 match w8:
2980 case WNil{}:
2981 {==}
2982 case WCon{True{}, w4}:
2983 match w4:
2984 case WCon{False{}, w5}:
2985 match w5:
2986 case WCon{False{}, w6}:
2987 match w6:
2988 case WCon{False{}, w7}:
2989 match w7:
2990 case WCon{False{}, w8}:
2991 match w8:
2992 case WNil{}:
2993 {==}
2994 case WCon{True{}, w8}:
2995 match w8:
2996 case WNil{}:
2997 {==}
2998 case WCon{True{}, w7}:
2999 match w7:
3000 case WCon{False{}, w8}:
3001 match w8:
3002 case WNil{}:
3003 {==}
3004 case WCon{True{}, w8}:
3005 match w8:
3006 case WNil{}:
3007 {==}
3008 case WCon{True{}, w6}:
3009 match w6:
3010 case WCon{False{}, w7}:
3011 match w7:
3012 case WCon{False{}, w8}:
3013 match w8:
3014 case WNil{}:
3015 {==}
3016 case WCon{True{}, w8}:
3017 match w8:
3018 case WNil{}:
3019 {==}
3020 case WCon{True{}, w7}:
3021 match w7:
3022 case WCon{False{}, w8}:
3023 match w8:
3024 case WNil{}:
3025 {==}
3026 case WCon{True{}, w8}:
3027 match w8:
3028 case WNil{}:
3029 {==}
3030 case WCon{True{}, w5}:
3031 match w5:
3032 case WCon{False{}, w6}:
3033 match w6:
3034 case WCon{False{}, w7}:
3035 match w7:
3036 case WCon{False{}, w8}:
3037 match w8:
3038 case WNil{}:
3039 {==}
3040 case WCon{True{}, w8}:
3041 match w8:
3042 case WNil{}:
3043 {==}
3044 case WCon{True{}, w7}:
3045 match w7:
3046 case WCon{False{}, w8}:
3047 match w8:
3048 case WNil{}:
3049 {==}
3050 case WCon{True{}, w8}:
3051 match w8:
3052 case WNil{}:
3053 {==}
3054 case WCon{True{}, w6}:
3055 match w6:
3056 case WCon{False{}, w7}:
3057 match w7:
3058 case WCon{False{}, w8}:
3059 match w8:
3060 case WNil{}:
3061 {==}
3062 case WCon{True{}, w8}:
3063 match w8:
3064 case WNil{}:
3065 {==}
3066 case WCon{True{}, w7}:
3067 match w7:
3068 case WCon{False{}, w8}:
3069 match w8:
3070 case WNil{}:
3071 {==}
3072 case WCon{True{}, w8}:
3073 match w8:
3074 case WNil{}:
3075 {==}
3076 case WCon{True{}, w3}:
3077 match w3:
3078 case WCon{False{}, w4}:
3079 match w4:
3080 case WCon{False{}, w5}:
3081 match w5:
3082 case WCon{False{}, w6}:
3083 match w6:
3084 case WCon{False{}, w7}:
3085 match w7:
3086 case WCon{False{}, w8}:
3087 match w8:
3088 case WNil{}:
3089 {==}
3090 case WCon{True{}, w8}:
3091 match w8:
3092 case WNil{}:
3093 {==}
3094 case WCon{True{}, w7}:
3095 match w7:
3096 case WCon{False{}, w8}:
3097 match w8:
3098 case WNil{}:
3099 {==}
3100 case WCon{True{}, w8}:
3101 match w8:
3102 case WNil{}:
3103 {==}
3104 case WCon{True{}, w6}:
3105 match w6:
3106 case WCon{False{}, w7}:
3107 match w7:
3108 case WCon{False{}, w8}:
3109 match w8:
3110 case WNil{}:
3111 {==}
3112 case WCon{True{}, w8}:
3113 match w8:
3114 case WNil{}:
3115 {==}
3116 case WCon{True{}, w7}:
3117 match w7:
3118 case WCon{False{}, w8}:
3119 match w8:
3120 case WNil{}:
3121 {==}
3122 case WCon{True{}, w8}:
3123 match w8:
3124 case WNil{}:
3125 {==}
3126 case WCon{True{}, w5}:
3127 match w5:
3128 case WCon{False{}, w6}:
3129 match w6:
3130 case WCon{False{}, w7}:
3131 match w7:
3132 case WCon{False{}, w8}:
3133 match w8:
3134 case WNil{}:
3135 {==}
3136 case WCon{True{}, w8}:
3137 match w8:
3138 case WNil{}:
3139 {==}
3140 case WCon{True{}, w7}:
3141 match w7:
3142 case WCon{False{}, w8}:
3143 match w8:
3144 case WNil{}:
3145 {==}
3146 case WCon{True{}, w8}:
3147 match w8:
3148 case WNil{}:
3149 {==}
3150 case WCon{True{}, w6}:
3151 match w6:
3152 case WCon{False{}, w7}:
3153 match w7:
3154 case WCon{False{}, w8}:
3155 match w8:
3156 case WNil{}:
3157 {==}
3158 case WCon{True{}, w8}:
3159 match w8:
3160 case WNil{}:
3161 {==}
3162 case WCon{True{}, w7}:
3163 match w7:
3164 case WCon{False{}, w8}:
3165 match w8:
3166 case WNil{}:
3167 {==}
3168 case WCon{True{}, w8}:
3169 match w8:
3170 case WNil{}:
3171 {==}
3172 case WCon{True{}, w4}:
3173 match w4:
3174 case WCon{False{}, w5}:
3175 match w5:
3176 case WCon{False{}, w6}:
3177 match w6:
3178 case WCon{False{}, w7}:
3179 match w7:
3180 case WCon{False{}, w8}:
3181 match w8:
3182 case WNil{}:
3183 {==}
3184 case WCon{True{}, w8}:
3185 match w8:
3186 case WNil{}:
3187 {==}
3188 case WCon{True{}, w7}:
3189 match w7:
3190 case WCon{False{}, w8}:
3191 match w8:
3192 case WNil{}:
3193 {==}
3194 case WCon{True{}, w8}:
3195 match w8:
3196 case WNil{}:
3197 {==}
3198 case WCon{True{}, w6}:
3199 match w6:
3200 case WCon{False{}, w7}:
3201 match w7:
3202 case WCon{False{}, w8}:
3203 match w8:
3204 case WNil{}:
3205 {==}
3206 case WCon{True{}, w8}:
3207 match w8:
3208 case WNil{}:
3209 {==}
3210 case WCon{True{}, w7}:
3211 match w7:
3212 case WCon{False{}, w8}:
3213 match w8:
3214 case WNil{}:
3215 {==}
3216 case WCon{True{}, w8}:
3217 match w8:
3218 case WNil{}:
3219 {==}
3220 case WCon{True{}, w5}:
3221 match w5:
3222 case WCon{False{}, w6}:
3223 match w6:
3224 case WCon{False{}, w7}:
3225 match w7:
3226 case WCon{False{}, w8}:
3227 match w8:
3228 case WNil{}:
3229 {==}
3230 case WCon{True{}, w8}:
3231 match w8:
3232 case WNil{}:
3233 {==}
3234 case WCon{True{}, w7}:
3235 match w7:
3236 case WCon{False{}, w8}:
3237 match w8:
3238 case WNil{}:
3239 {==}
3240 case WCon{True{}, w8}:
3241 match w8:
3242 case WNil{}:
3243 {==}
3244 case WCon{True{}, w6}:
3245 match w6:
3246 case WCon{False{}, w7}:
3247 match w7:
3248 case WCon{False{}, w8}:
3249 match w8:
3250 case WNil{}:
3251 {==}
3252 case WCon{True{}, w8}:
3253 match w8:
3254 case WNil{}:
3255 {==}
3256 case WCon{True{}, w7}:
3257 match w7:
3258 case WCon{False{}, w8}:
3259 match w8:
3260 case WNil{}:
3261 {==}
3262 case WCon{True{}, w8}:
3263 match w8:
3264 case WNil{}:
3265 {==}