def gc.rs.log.bits.s111
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:3173
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
3173
3174def gc.rs.log.bits.s111(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.rs.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.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}}))) : U32}:
3175 match b0:
3176 case True{}:
3177 match b1:
3178 case True{}:
3179 match b2:
3180 case True{}:
3181 match b3:
3182 case True{}:
3183 match b4:
3184 case True{}:
3185 {==}
3186 case False{}:
3187 {==}
3188 case False{}:
3189 match b4:
3190 case True{}:
3191 {==}
3192 case False{}:
3193 {==}
3194 case False{}:
3195 match b3:
3196 case True{}:
3197 match b4:
3198 case True{}:
3199 {==}
3200 case False{}:
3201 {==}
3202 case False{}:
3203 match b4:
3204 case True{}:
3205 {==}
3206 case False{}:
3207 {==}
3208 case False{}:
3209 match b2:
3210 case True{}:
3211 match b3:
3212 case True{}:
3213 match b4:
3214 case True{}:
3215 {==}
3216 case False{}:
3217 {==}
3218 case False{}:
3219 match b4:
3220 case True{}:
3221 {==}
3222 case False{}:
3223 {==}
3224 case False{}:
3225 match b3:
3226 case True{}:
3227 match b4:
3228 case True{}:
3229 {==}
3230 case False{}:
3231 {==}
3232 case False{}:
3233 match b4:
3234 case True{}:
3235 {==}
3236 case False{}:
3237 {==}
3238 case False{}:
3239 match b1:
3240 case True{}:
3241 match b2:
3242 case True{}:
3243 match b3:
3244 case True{}:
3245 match b4:
3246 case True{}:
3247 {==}
3248 case False{}:
3249 {==}
3250 case False{}:
3251 match b4:
3252 case True{}:
3253 {==}
3254 case False{}:
3255 {==}
3256 case False{}:
3257 match b3:
3258 case True{}:
3259 match b4:
3260 case True{}:
3261 {==}
3262 case False{}:
3263 {==}
3264 case False{}:
3265 match b4:
3266 case True{}:
3267 {==}
3268 case False{}:
3269 {==}
3270 case False{}:
3271 match b2:
3272 case True{}:
3273 match b3:
3274 case True{}:
3275 match b4:
3276 case True{}:
3277 {==}
3278 case False{}:
3279 {==}
3280 case False{}:
3281 match b4:
3282 case True{}:
3283 {==}
3284 case False{}:
3285 {==}
3286 case False{}:
3287 match b3:
3288 case True{}:
3289 match b4:
3290 case True{}:
3291 {==}
3292 case False{}:
3293 {==}
3294 case False{}:
3295 match b4:
3296 case True{}:
3297 {==}
3298 case False{}:
3299 {==}