def gc.rs.log.bits.s011
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:3301
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
3301def gc.rs.log.bits.s011(+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{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}))) : U32}:
3302 match b0:
3303 case True{}:
3304 match b1:
3305 case True{}:
3306 match b2:
3307 case True{}:
3308 match b3:
3309 case True{}:
3310 match b4:
3311 case True{}:
3312 {==}
3313 case False{}:
3314 {==}
3315 case False{}:
3316 match b4:
3317 case True{}:
3318 {==}
3319 case False{}:
3320 {==}
3321 case False{}:
3322 match b3:
3323 case True{}:
3324 match b4:
3325 case True{}:
3326 {==}
3327 case False{}:
3328 {==}
3329 case False{}:
3330 match b4:
3331 case True{}:
3332 {==}
3333 case False{}:
3334 {==}
3335 case False{}:
3336 match b2:
3337 case True{}:
3338 match b3:
3339 case True{}:
3340 match b4:
3341 case True{}:
3342 {==}
3343 case False{}:
3344 {==}
3345 case False{}:
3346 match b4:
3347 case True{}:
3348 {==}
3349 case False{}:
3350 {==}
3351 case False{}:
3352 match b3:
3353 case True{}:
3354 match b4:
3355 case True{}:
3356 {==}
3357 case False{}:
3358 {==}
3359 case False{}:
3360 match b4:
3361 case True{}:
3362 {==}
3363 case False{}:
3364 {==}
3365 case False{}:
3366 match b1:
3367 case True{}:
3368 match b2:
3369 case True{}:
3370 match b3:
3371 case True{}:
3372 match b4:
3373 case True{}:
3374 {==}
3375 case False{}:
3376 {==}
3377 case False{}:
3378 match b4:
3379 case True{}:
3380 {==}
3381 case False{}:
3382 {==}
3383 case False{}:
3384 match b3:
3385 case True{}:
3386 match b4:
3387 case True{}:
3388 {==}
3389 case False{}:
3390 {==}
3391 case False{}:
3392 match b4:
3393 case True{}:
3394 {==}
3395 case False{}:
3396 {==}
3397 case False{}:
3398 match b2:
3399 case True{}:
3400 match b3:
3401 case True{}:
3402 match b4:
3403 case True{}:
3404 {==}
3405 case False{}:
3406 {==}
3407 case False{}:
3408 match b4:
3409 case True{}:
3410 {==}
3411 case False{}:
3412 {==}
3413 case False{}:
3414 match b3:
3415 case True{}:
3416 match b4:
3417 case True{}:
3418 {==}
3419 case False{}:
3420 {==}
3421 case False{}:
3422 match b4:
3423 case True{}:
3424 {==}
3425 case False{}:
3426 {==}