def gc.elt0.s000
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:1947
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
1947def gc.elt0.s000(+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{}, False{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}}) == 0 : U32}:
1948 match b0:
1949 case True{}:
1950 match b1:
1951 case True{}:
1952 match b2:
1953 case True{}:
1954 match b3:
1955 case True{}:
1956 match b4:
1957 case True{}:
1958 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1959 case False{}:
1960 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1961 case False{}:
1962 match b4:
1963 case True{}:
1964 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1965 case False{}:
1966 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1967 case False{}:
1968 match b3:
1969 case True{}:
1970 match b4:
1971 case True{}:
1972 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1973 case False{}:
1974 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1975 case False{}:
1976 match b4:
1977 case True{}:
1978 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1979 case False{}:
1980 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1981 case False{}:
1982 match b2:
1983 case True{}:
1984 match b3:
1985 case True{}:
1986 match b4:
1987 case True{}:
1988 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1989 case False{}:
1990 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1991 case False{}:
1992 match b4:
1993 case True{}:
1994 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1995 case False{}:
1996 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1997 case False{}:
1998 match b3:
1999 case True{}:
2000 match b4:
2001 case True{}:
2002 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2003 case False{}:
2004 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2005 case False{}:
2006 match b4:
2007 case True{}:
2008 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2009 case False{}:
2010 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2011 case False{}:
2012 match b1:
2013 case True{}:
2014 match b2:
2015 case True{}:
2016 match b3:
2017 case True{}:
2018 match b4:
2019 case True{}:
2020 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2021 case False{}:
2022 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2023 case False{}:
2024 match b4:
2025 case True{}:
2026 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2027 case False{}:
2028 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2029 case False{}:
2030 match b3:
2031 case True{}:
2032 match b4:
2033 case True{}:
2034 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2035 case False{}:
2036 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2037 case False{}:
2038 match b4:
2039 case True{}:
2040 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2041 case False{}:
2042 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2043 case False{}:
2044 match b2:
2045 case True{}:
2046 match b3:
2047 case True{}:
2048 match b4:
2049 case True{}:
2050 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2051 case False{}:
2052 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2053 case False{}:
2054 match b4:
2055 case True{}:
2056 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2057 case False{}:
2058 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2059 case False{}:
2060 match b3:
2061 case True{}:
2062 match b4:
2063 case True{}:
2064 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2065 case False{}:
2066 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2067 case False{}:
2068 match b4:
2069 case True{}:
2070 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2071 case False{}:
2072 {==}