def gc.elt0.s100
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:1820
import bend-osdev-gf@0.1.1.0/proof_tab_cases.bend as ProofTabCases
import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
import bend-osdev-gf@0.1.1.0/proof_tab.bend as GT
1820def gc.elt0.s100(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}}) == 0 : U32}:
1821 match b0:
1822 case True{}:
1823 match b1:
1824 case True{}:
1825 match b2:
1826 case True{}:
1827 match b3:
1828 case True{}:
1829 match b4:
1830 case True{}:
1831 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1832 case False{}:
1833 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1834 case False{}:
1835 match b4:
1836 case True{}:
1837 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1838 case False{}:
1839 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1840 case False{}:
1841 match b3:
1842 case True{}:
1843 match b4:
1844 case True{}:
1845 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1846 case False{}:
1847 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1848 case False{}:
1849 match b4:
1850 case True{}:
1851 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1852 case False{}:
1853 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1854 case False{}:
1855 match b2:
1856 case True{}:
1857 match b3:
1858 case True{}:
1859 match b4:
1860 case True{}:
1861 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1862 case False{}:
1863 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1864 case False{}:
1865 match b4:
1866 case True{}:
1867 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1868 case False{}:
1869 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1870 case False{}:
1871 match b3:
1872 case True{}:
1873 match b4:
1874 case True{}:
1875 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1876 case False{}:
1877 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1878 case False{}:
1879 match b4:
1880 case True{}:
1881 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1882 case False{}:
1883 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1884 case False{}:
1885 match b1:
1886 case True{}:
1887 match b2:
1888 case True{}:
1889 match b3:
1890 case True{}:
1891 match b4:
1892 case True{}:
1893 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1894 case False{}:
1895 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1896 case False{}:
1897 match b4:
1898 case True{}:
1899 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1900 case False{}:
1901 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1902 case False{}:
1903 match b3:
1904 case True{}:
1905 match b4:
1906 case True{}:
1907 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1908 case False{}:
1909 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1910 case False{}:
1911 match b4:
1912 case True{}:
1913 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1914 case False{}:
1915 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1916 case False{}:
1917 match b2:
1918 case True{}:
1919 match b3:
1920 case True{}:
1921 match b4:
1922 case True{}:
1923 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1924 case False{}:
1925 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1926 case False{}:
1927 match b4:
1928 case True{}:
1929 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1930 case False{}:
1931 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1932 case False{}:
1933 match b3:
1934 case True{}:
1935 match b4:
1936 case True{}:
1937 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1938 case False{}:
1939 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1940 case False{}:
1941 match b4:
1942 case True{}:
1943 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1944 case False{}:
1945 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))