def gc.aes.log.bits.s111
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:2115
import bend-osdev-gf@0.1.1.0/proof_tab_cases.bend as ProofTabCases
import Base
import bend-osdev-array@0.1.0.1/array.bend as A
import bend-osdev-gf@0.1.1.0/gf.bend as G
2115
2116def gc.aes.log.bits.s111(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}}))) : U32}:
2117 match b0:
2118 case True{}:
2119 match b1:
2120 case True{}:
2121 match b2:
2122 case True{}:
2123 match b3:
2124 case True{}:
2125 match b4:
2126 case True{}:
2127 {==}
2128 case False{}:
2129 {==}
2130 case False{}:
2131 match b4:
2132 case True{}:
2133 {==}
2134 case False{}:
2135 {==}
2136 case False{}:
2137 match b3:
2138 case True{}:
2139 match b4:
2140 case True{}:
2141 {==}
2142 case False{}:
2143 {==}
2144 case False{}:
2145 match b4:
2146 case True{}:
2147 {==}
2148 case False{}:
2149 {==}
2150 case False{}:
2151 match b2:
2152 case True{}:
2153 match b3:
2154 case True{}:
2155 match b4:
2156 case True{}:
2157 {==}
2158 case False{}:
2159 {==}
2160 case False{}:
2161 match b4:
2162 case True{}:
2163 {==}
2164 case False{}:
2165 {==}
2166 case False{}:
2167 match b3:
2168 case True{}:
2169 match b4:
2170 case True{}:
2171 {==}
2172 case False{}:
2173 {==}
2174 case False{}:
2175 match b4:
2176 case True{}:
2177 {==}
2178 case False{}:
2179 {==}
2180 case False{}:
2181 match b1:
2182 case True{}:
2183 match b2:
2184 case True{}:
2185 match b3:
2186 case True{}:
2187 match b4:
2188 case True{}:
2189 {==}
2190 case False{}:
2191 {==}
2192 case False{}:
2193 match b4:
2194 case True{}:
2195 {==}
2196 case False{}:
2197 {==}
2198 case False{}:
2199 match b3:
2200 case True{}:
2201 match b4:
2202 case True{}:
2203 {==}
2204 case False{}:
2205 {==}
2206 case False{}:
2207 match b4:
2208 case True{}:
2209 {==}
2210 case False{}:
2211 {==}
2212 case False{}:
2213 match b2:
2214 case True{}:
2215 match b3:
2216 case True{}:
2217 match b4:
2218 case True{}:
2219 {==}
2220 case False{}:
2221 {==}
2222 case False{}:
2223 match b4:
2224 case True{}:
2225 {==}
2226 case False{}:
2227 {==}
2228 case False{}:
2229 match b3:
2230 case True{}:
2231 match b4:
2232 case True{}:
2233 {==}
2234 case False{}:
2235 {==}
2236 case False{}:
2237 match b4:
2238 case True{}:
2239 {==}
2240 case False{}:
2241 {==}