def gc.rs.log.bits.s001

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

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

3555def gc.rs.log.bits.s001(+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{}, False{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}))) : U32}:
3556  match b0:
3557    case True{}:
3558      match b1:
3559        case True{}:
3560          match b2:
3561            case True{}:
3562              match b3:
3563                case True{}:
3564                  match b4:
3565                    case True{}:
3566                      {==}
3567                    case False{}:
3568                      {==}
3569                case False{}:
3570                  match b4:
3571                    case True{}:
3572                      {==}
3573                    case False{}:
3574                      {==}
3575            case False{}:
3576              match b3:
3577                case True{}:
3578                  match b4:
3579                    case True{}:
3580                      {==}
3581                    case False{}:
3582                      {==}
3583                case False{}:
3584                  match b4:
3585                    case True{}:
3586                      {==}
3587                    case False{}:
3588                      {==}
3589        case False{}:
3590          match b2:
3591            case True{}:
3592              match b3:
3593                case True{}:
3594                  match b4:
3595                    case True{}:
3596                      {==}
3597                    case False{}:
3598                      {==}
3599                case False{}:
3600                  match b4:
3601                    case True{}:
3602                      {==}
3603                    case False{}:
3604                      {==}
3605            case False{}:
3606              match b3:
3607                case True{}:
3608                  match b4:
3609                    case True{}:
3610                      {==}
3611                    case False{}:
3612                      {==}
3613                case False{}:
3614                  match b4:
3615                    case True{}:
3616                      {==}
3617                    case False{}:
3618                      {==}
3619    case False{}:
3620      match b1:
3621        case True{}:
3622          match b2:
3623            case True{}:
3624              match b3:
3625                case True{}:
3626                  match b4:
3627                    case True{}:
3628                      {==}
3629                    case False{}:
3630                      {==}
3631                case False{}:
3632                  match b4:
3633                    case True{}:
3634                      {==}
3635                    case False{}:
3636                      {==}
3637            case False{}:
3638              match b3:
3639                case True{}:
3640                  match b4:
3641                    case True{}:
3642                      {==}
3643                    case False{}:
3644                      {==}
3645                case False{}:
3646                  match b4:
3647                    case True{}:
3648                      {==}
3649                    case False{}:
3650                      {==}
3651        case False{}:
3652          match b2:
3653            case True{}:
3654              match b3:
3655                case True{}:
3656                  match b4:
3657                    case True{}:
3658                      {==}
3659                    case False{}:
3660                      {==}
3661                case False{}:
3662                  match b4:
3663                    case True{}:
3664                      {==}
3665                    case False{}:
3666                      {==}
3667            case False{}:
3668              match b3:
3669                case True{}:
3670                  match b4:
3671                    case True{}:
3672                      {==}
3673                    case False{}:
3674                      {==}
3675                case False{}:
3676                  match b4:
3677                    case True{}:
3678                      {==}
3679                    case False{}:
3680                      {==}