def comm16.s1001

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

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

6851def comm16.s1001(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{True{}, WCon{False{}, WCon{False{}, 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{False{}, WCon{False{}, WCon{True{}, Word.zero(28n)}}}}}) : U32}:
6852  match b0:
6853    case True{}:
6854      match b1:
6855        case True{}:
6856          match b2:
6857            case True{}:
6858              match b3:
6859                case True{}:
6860                  {==}
6861                case False{}:
6862                  {==}
6863            case False{}:
6864              match b3:
6865                case True{}:
6866                  {==}
6867                case False{}:
6868                  {==}
6869        case False{}:
6870          match b2:
6871            case True{}:
6872              match b3:
6873                case True{}:
6874                  {==}
6875                case False{}:
6876                  {==}
6877            case False{}:
6878              match b3:
6879                case True{}:
6880                  {==}
6881                case False{}:
6882                  {==}
6883    case False{}:
6884      match b1:
6885        case True{}:
6886          match b2:
6887            case True{}:
6888              match b3:
6889                case True{}:
6890                  {==}
6891                case False{}:
6892                  {==}
6893            case False{}:
6894              match b3:
6895                case True{}:
6896                  {==}
6897                case False{}:
6898                  {==}
6899        case False{}:
6900          match b2:
6901            case True{}:
6902              match b3:
6903                case True{}:
6904                  {==}
6905                case False{}:
6906                  {==}
6907            case False{}:
6908              match b3:
6909                case True{}:
6910                  {==}
6911                case False{}:
6912                  {==}