def gc.aes.log.bits.s101
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:2370
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
2370def gc.aes.log.bits.s101(+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{}, False{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}))) : U32}:
2371 match b0:
2372 case True{}:
2373 match b1:
2374 case True{}:
2375 match b2:
2376 case True{}:
2377 match b3:
2378 case True{}:
2379 match b4:
2380 case True{}:
2381 {==}
2382 case False{}:
2383 {==}
2384 case False{}:
2385 match b4:
2386 case True{}:
2387 {==}
2388 case False{}:
2389 {==}
2390 case False{}:
2391 match b3:
2392 case True{}:
2393 match b4:
2394 case True{}:
2395 {==}
2396 case False{}:
2397 {==}
2398 case False{}:
2399 match b4:
2400 case True{}:
2401 {==}
2402 case False{}:
2403 {==}
2404 case False{}:
2405 match b2:
2406 case True{}:
2407 match b3:
2408 case True{}:
2409 match b4:
2410 case True{}:
2411 {==}
2412 case False{}:
2413 {==}
2414 case False{}:
2415 match b4:
2416 case True{}:
2417 {==}
2418 case False{}:
2419 {==}
2420 case False{}:
2421 match b3:
2422 case True{}:
2423 match b4:
2424 case True{}:
2425 {==}
2426 case False{}:
2427 {==}
2428 case False{}:
2429 match b4:
2430 case True{}:
2431 {==}
2432 case False{}:
2433 {==}
2434 case False{}:
2435 match b1:
2436 case True{}:
2437 match b2:
2438 case True{}:
2439 match b3:
2440 case True{}:
2441 match b4:
2442 case True{}:
2443 {==}
2444 case False{}:
2445 {==}
2446 case False{}:
2447 match b4:
2448 case True{}:
2449 {==}
2450 case False{}:
2451 {==}
2452 case False{}:
2453 match b3:
2454 case True{}:
2455 match b4:
2456 case True{}:
2457 {==}
2458 case False{}:
2459 {==}
2460 case False{}:
2461 match b4:
2462 case True{}:
2463 {==}
2464 case False{}:
2465 {==}
2466 case False{}:
2467 match b2:
2468 case True{}:
2469 match b3:
2470 case True{}:
2471 match b4:
2472 case True{}:
2473 {==}
2474 case False{}:
2475 {==}
2476 case False{}:
2477 match b4:
2478 case True{}:
2479 {==}
2480 case False{}:
2481 {==}
2482 case False{}:
2483 match b3:
2484 case True{}:
2485 match b4:
2486 case True{}:
2487 {==}
2488 case False{}:
2489 {==}
2490 case False{}:
2491 match b4:
2492 case True{}:
2493 {==}
2494 case False{}:
2495 {==}