def gc.rs.log.bits.s101

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

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

3428def gc.rs.log.bits.s101(+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{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}))) : U32}:
3429  match b0:
3430    case True{}:
3431      match b1:
3432        case True{}:
3433          match b2:
3434            case True{}:
3435              match b3:
3436                case True{}:
3437                  match b4:
3438                    case True{}:
3439                      {==}
3440                    case False{}:
3441                      {==}
3442                case False{}:
3443                  match b4:
3444                    case True{}:
3445                      {==}
3446                    case False{}:
3447                      {==}
3448            case False{}:
3449              match b3:
3450                case True{}:
3451                  match b4:
3452                    case True{}:
3453                      {==}
3454                    case False{}:
3455                      {==}
3456                case False{}:
3457                  match b4:
3458                    case True{}:
3459                      {==}
3460                    case False{}:
3461                      {==}
3462        case False{}:
3463          match b2:
3464            case True{}:
3465              match b3:
3466                case True{}:
3467                  match b4:
3468                    case True{}:
3469                      {==}
3470                    case False{}:
3471                      {==}
3472                case False{}:
3473                  match b4:
3474                    case True{}:
3475                      {==}
3476                    case False{}:
3477                      {==}
3478            case False{}:
3479              match b3:
3480                case True{}:
3481                  match b4:
3482                    case True{}:
3483                      {==}
3484                    case False{}:
3485                      {==}
3486                case False{}:
3487                  match b4:
3488                    case True{}:
3489                      {==}
3490                    case False{}:
3491                      {==}
3492    case False{}:
3493      match b1:
3494        case True{}:
3495          match b2:
3496            case True{}:
3497              match b3:
3498                case True{}:
3499                  match b4:
3500                    case True{}:
3501                      {==}
3502                    case False{}:
3503                      {==}
3504                case False{}:
3505                  match b4:
3506                    case True{}:
3507                      {==}
3508                    case False{}:
3509                      {==}
3510            case False{}:
3511              match b3:
3512                case True{}:
3513                  match b4:
3514                    case True{}:
3515                      {==}
3516                    case False{}:
3517                      {==}
3518                case False{}:
3519                  match b4:
3520                    case True{}:
3521                      {==}
3522                    case False{}:
3523                      {==}
3524        case False{}:
3525          match b2:
3526            case True{}:
3527              match b3:
3528                case True{}:
3529                  match b4:
3530                    case True{}:
3531                      {==}
3532                    case False{}:
3533                      {==}
3534                case False{}:
3535                  match b4:
3536                    case True{}:
3537                      {==}
3538                    case False{}:
3539                      {==}
3540            case False{}:
3541              match b3:
3542                case True{}:
3543                  match b4:
3544                    case True{}:
3545                      {==}
3546                    case False{}:
3547                      {==}
3548                case False{}:
3549                  match b4:
3550                    case True{}:
3551                      {==}
3552                    case False{}:
3553                      {==}