def gc.aes.log.bits.s110
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:2624
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
2624def gc.aes.log.bits.s110(+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, False{}, True{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}}))) : U32}:
2625 match b0:
2626 case True{}:
2627 match b1:
2628 case True{}:
2629 match b2:
2630 case True{}:
2631 match b3:
2632 case True{}:
2633 match b4:
2634 case True{}:
2635 {==}
2636 case False{}:
2637 {==}
2638 case False{}:
2639 match b4:
2640 case True{}:
2641 {==}
2642 case False{}:
2643 {==}
2644 case False{}:
2645 match b3:
2646 case True{}:
2647 match b4:
2648 case True{}:
2649 {==}
2650 case False{}:
2651 {==}
2652 case False{}:
2653 match b4:
2654 case True{}:
2655 {==}
2656 case False{}:
2657 {==}
2658 case False{}:
2659 match b2:
2660 case True{}:
2661 match b3:
2662 case True{}:
2663 match b4:
2664 case True{}:
2665 {==}
2666 case False{}:
2667 {==}
2668 case False{}:
2669 match b4:
2670 case True{}:
2671 {==}
2672 case False{}:
2673 {==}
2674 case False{}:
2675 match b3:
2676 case True{}:
2677 match b4:
2678 case True{}:
2679 {==}
2680 case False{}:
2681 {==}
2682 case False{}:
2683 match b4:
2684 case True{}:
2685 {==}
2686 case False{}:
2687 {==}
2688 case False{}:
2689 match b1:
2690 case True{}:
2691 match b2:
2692 case True{}:
2693 match b3:
2694 case True{}:
2695 match b4:
2696 case True{}:
2697 {==}
2698 case False{}:
2699 {==}
2700 case False{}:
2701 match b4:
2702 case True{}:
2703 {==}
2704 case False{}:
2705 {==}
2706 case False{}:
2707 match b3:
2708 case True{}:
2709 match b4:
2710 case True{}:
2711 {==}
2712 case False{}:
2713 {==}
2714 case False{}:
2715 match b4:
2716 case True{}:
2717 {==}
2718 case False{}:
2719 {==}
2720 case False{}:
2721 match b2:
2722 case True{}:
2723 match b3:
2724 case True{}:
2725 match b4:
2726 case True{}:
2727 {==}
2728 case False{}:
2729 {==}
2730 case False{}:
2731 match b4:
2732 case True{}:
2733 {==}
2734 case False{}:
2735 {==}
2736 case False{}:
2737 match b3:
2738 case True{}:
2739 match b4:
2740 case True{}:
2741 {==}
2742 case False{}:
2743 {==}
2744 case False{}:
2745 match b4:
2746 case True{}:
2747 {==}
2748 case False{}:
2749 {==}