def comm16.s0011

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

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

7229def comm16.s0011(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{False{}, WCon{False{}, 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{False{}, WCon{False{}, WCon{True{}, WCon{True{}, Word.zero(28n)}}}}}) : U32}:
7230  match b0:
7231    case True{}:
7232      match b1:
7233        case True{}:
7234          match b2:
7235            case True{}:
7236              match b3:
7237                case True{}:
7238                  {==}
7239                case False{}:
7240                  {==}
7241            case False{}:
7242              match b3:
7243                case True{}:
7244                  {==}
7245                case False{}:
7246                  {==}
7247        case False{}:
7248          match b2:
7249            case True{}:
7250              match b3:
7251                case True{}:
7252                  {==}
7253                case False{}:
7254                  {==}
7255            case False{}:
7256              match b3:
7257                case True{}:
7258                  {==}
7259                case False{}:
7260                  {==}
7261    case False{}:
7262      match b1:
7263        case True{}:
7264          match b2:
7265            case True{}:
7266              match b3:
7267                case True{}:
7268                  {==}
7269                case False{}:
7270                  {==}
7271            case False{}:
7272              match b3:
7273                case True{}:
7274                  {==}
7275                case False{}:
7276                  {==}
7277        case False{}:
7278          match b2:
7279            case True{}:
7280              match b3:
7281                case True{}:
7282                  {==}
7283                case False{}:
7284                  {==}
7285            case False{}:
7286              match b3:
7287                case True{}:
7288                  {==}
7289                case False{}:
7290                  {==}