def gc.isz.bits.s001

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

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

397def gc.isz.bits.s001(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}) : Bool}:
398  match b0:
399    case True{}:
400      match b1:
401        case True{}:
402          match b2:
403            case True{}:
404              match b3:
405                case True{}:
406                  match b4:
407                    case True{}:
408                      {==}
409                    case False{}:
410                      {==}
411                case False{}:
412                  match b4:
413                    case True{}:
414                      {==}
415                    case False{}:
416                      {==}
417            case False{}:
418              match b3:
419                case True{}:
420                  match b4:
421                    case True{}:
422                      {==}
423                    case False{}:
424                      {==}
425                case False{}:
426                  match b4:
427                    case True{}:
428                      {==}
429                    case False{}:
430                      {==}
431        case False{}:
432          match b2:
433            case True{}:
434              match b3:
435                case True{}:
436                  match b4:
437                    case True{}:
438                      {==}
439                    case False{}:
440                      {==}
441                case False{}:
442                  match b4:
443                    case True{}:
444                      {==}
445                    case False{}:
446                      {==}
447            case False{}:
448              match b3:
449                case True{}:
450                  match b4:
451                    case True{}:
452                      {==}
453                    case False{}:
454                      {==}
455                case False{}:
456                  match b4:
457                    case True{}:
458                      {==}
459                    case False{}:
460                      {==}
461    case False{}:
462      match b1:
463        case True{}:
464          match b2:
465            case True{}:
466              match b3:
467                case True{}:
468                  match b4:
469                    case True{}:
470                      {==}
471                    case False{}:
472                      {==}
473                case False{}:
474                  match b4:
475                    case True{}:
476                      {==}
477                    case False{}:
478                      {==}
479            case False{}:
480              match b3:
481                case True{}:
482                  match b4:
483                    case True{}:
484                      {==}
485                    case False{}:
486                      {==}
487                case False{}:
488                  match b4:
489                    case True{}:
490                      {==}
491                    case False{}:
492                      {==}
493        case False{}:
494          match b2:
495            case True{}:
496              match b3:
497                case True{}:
498                  match b4:
499                    case True{}:
500                      {==}
501                    case False{}:
502                      {==}
503                case False{}:
504                  match b4:
505                    case True{}:
506                      {==}
507                    case False{}:
508                      {==}
509            case False{}:
510              match b3:
511                case True{}:
512                  match b4:
513                    case True{}:
514                      {==}
515                    case False{}:
516                      {==}
517                case False{}:
518                  match b4:
519                    case True{}:
520                      {==}
521                    case False{}:
522                      {==}