def gc.rs.log.bits.s110

bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:3682

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

3682def gc.rs.log.bits.s110(+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, False{}, True{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}}))) : U32}:
3683  match b0:
3684    case True{}:
3685      match b1:
3686        case True{}:
3687          match b2:
3688            case True{}:
3689              match b3:
3690                case True{}:
3691                  match b4:
3692                    case True{}:
3693                      {==}
3694                    case False{}:
3695                      {==}
3696                case False{}:
3697                  match b4:
3698                    case True{}:
3699                      {==}
3700                    case False{}:
3701                      {==}
3702            case False{}:
3703              match b3:
3704                case True{}:
3705                  match b4:
3706                    case True{}:
3707                      {==}
3708                    case False{}:
3709                      {==}
3710                case False{}:
3711                  match b4:
3712                    case True{}:
3713                      {==}
3714                    case False{}:
3715                      {==}
3716        case False{}:
3717          match b2:
3718            case True{}:
3719              match b3:
3720                case True{}:
3721                  match b4:
3722                    case True{}:
3723                      {==}
3724                    case False{}:
3725                      {==}
3726                case False{}:
3727                  match b4:
3728                    case True{}:
3729                      {==}
3730                    case False{}:
3731                      {==}
3732            case False{}:
3733              match b3:
3734                case True{}:
3735                  match b4:
3736                    case True{}:
3737                      {==}
3738                    case False{}:
3739                      {==}
3740                case False{}:
3741                  match b4:
3742                    case True{}:
3743                      {==}
3744                    case False{}:
3745                      {==}
3746    case False{}:
3747      match b1:
3748        case True{}:
3749          match b2:
3750            case True{}:
3751              match b3:
3752                case True{}:
3753                  match b4:
3754                    case True{}:
3755                      {==}
3756                    case False{}:
3757                      {==}
3758                case False{}:
3759                  match b4:
3760                    case True{}:
3761                      {==}
3762                    case False{}:
3763                      {==}
3764            case False{}:
3765              match b3:
3766                case True{}:
3767                  match b4:
3768                    case True{}:
3769                      {==}
3770                    case False{}:
3771                      {==}
3772                case False{}:
3773                  match b4:
3774                    case True{}:
3775                      {==}
3776                    case False{}:
3777                      {==}
3778        case False{}:
3779          match b2:
3780            case True{}:
3781              match b3:
3782                case True{}:
3783                  match b4:
3784                    case True{}:
3785                      {==}
3786                    case False{}:
3787                      {==}
3788                case False{}:
3789                  match b4:
3790                    case True{}:
3791                      {==}
3792                    case False{}:
3793                      {==}
3794            case False{}:
3795              match b3:
3796                case True{}:
3797                  match b4:
3798                    case True{}:
3799                      {==}
3800                    case False{}:
3801                      {==}
3802                case False{}:
3803                  match b4:
3804                    case True{}:
3805                      {==}
3806                    case False{}:
3807                      {==}