def comm16.s1111

bend-osdev-gf@0.1.1.0 · PROOF.bend:6473

import Base
import bend-osdev-gf@0.1.1.0/gfm.bend as M

6473def comm16.s1111(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, Word.zero(28n)}}}}}, U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, Word.zero(28n)}}}}}) == M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, Word.zero(28n)}}}}}, U32{WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, Word.zero(28n)}}}}}) : U32}:
6474  match b0:
6475    case True{}:
6476      match b1:
6477        case True{}:
6478          match b2:
6479            case True{}:
6480              match b3:
6481                case True{}:
6482                  {==}
6483                case False{}:
6484                  {==}
6485            case False{}:
6486              match b3:
6487                case True{}:
6488                  {==}
6489                case False{}:
6490                  {==}
6491        case False{}:
6492          match b2:
6493            case True{}:
6494              match b3:
6495                case True{}:
6496                  {==}
6497                case False{}:
6498                  {==}
6499            case False{}:
6500              match b3:
6501                case True{}:
6502                  {==}
6503                case False{}:
6504                  {==}
6505    case False{}:
6506      match b1:
6507        case True{}:
6508          match b2:
6509            case True{}:
6510              match b3:
6511                case True{}:
6512                  {==}
6513                case False{}:
6514                  {==}
6515            case False{}:
6516              match b3:
6517                case True{}:
6518                  {==}
6519                case False{}:
6520                  {==}
6521        case False{}:
6522          match b2:
6523            case True{}:
6524              match b3:
6525                case True{}:
6526                  {==}
6527                case False{}:
6528                  {==}
6529            case False{}:
6530              match b3:
6531                case True{}:
6532                  {==}
6533                case False{}:
6534                  {==}