def comm16.s0000

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

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

7418def comm16.s0000(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{False{}, WCon{False{}, WCon{False{}, 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{False{}, WCon{False{}, Word.zero(28n)}}}}}) : U32}:
7419  match b0:
7420    case True{}:
7421      match b1:
7422        case True{}:
7423          match b2:
7424            case True{}:
7425              match b3:
7426                case True{}:
7427                  {==}
7428                case False{}:
7429                  {==}
7430            case False{}:
7431              match b3:
7432                case True{}:
7433                  {==}
7434                case False{}:
7435                  {==}
7436        case False{}:
7437          match b2:
7438            case True{}:
7439              match b3:
7440                case True{}:
7441                  {==}
7442                case False{}:
7443                  {==}
7444            case False{}:
7445              match b3:
7446                case True{}:
7447                  {==}
7448                case False{}:
7449                  {==}
7450    case False{}:
7451      match b1:
7452        case True{}:
7453          match b2:
7454            case True{}:
7455              match b3:
7456                case True{}:
7457                  {==}
7458                case False{}:
7459                  {==}
7460            case False{}:
7461              match b3:
7462                case True{}:
7463                  {==}
7464                case False{}:
7465                  {==}
7466        case False{}:
7467          match b2:
7468            case True{}:
7469              match b3:
7470                case True{}:
7471                  {==}
7472                case False{}:
7473                  {==}
7474            case False{}:
7475              match b3:
7476                case True{}:
7477                  {==}
7478                case False{}:
7479                  {==}