def comm16.s0010

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

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

7292def comm16.s0010(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, 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{False{}, Word.zero(28n)}}}}}) : U32}:
7293  match b0:
7294    case True{}:
7295      match b1:
7296        case True{}:
7297          match b2:
7298            case True{}:
7299              match b3:
7300                case True{}:
7301                  {==}
7302                case False{}:
7303                  {==}
7304            case False{}:
7305              match b3:
7306                case True{}:
7307                  {==}
7308                case False{}:
7309                  {==}
7310        case False{}:
7311          match b2:
7312            case True{}:
7313              match b3:
7314                case True{}:
7315                  {==}
7316                case False{}:
7317                  {==}
7318            case False{}:
7319              match b3:
7320                case True{}:
7321                  {==}
7322                case False{}:
7323                  {==}
7324    case False{}:
7325      match b1:
7326        case True{}:
7327          match b2:
7328            case True{}:
7329              match b3:
7330                case True{}:
7331                  {==}
7332                case False{}:
7333                  {==}
7334            case False{}:
7335              match b3:
7336                case True{}:
7337                  {==}
7338                case False{}:
7339                  {==}
7340        case False{}:
7341          match b2:
7342            case True{}:
7343              match b3:
7344                case True{}:
7345                  {==}
7346                case False{}:
7347                  {==}
7348            case False{}:
7349              match b3:
7350                case True{}:
7351                  {==}
7352                case False{}:
7353                  {==}