def comm16.s1000

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

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

6914def comm16.s1000(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{True{}, 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{True{}, WCon{False{}, WCon{False{}, WCon{False{}, Word.zero(28n)}}}}}) : U32}:
6915  match b0:
6916    case True{}:
6917      match b1:
6918        case True{}:
6919          match b2:
6920            case True{}:
6921              match b3:
6922                case True{}:
6923                  {==}
6924                case False{}:
6925                  {==}
6926            case False{}:
6927              match b3:
6928                case True{}:
6929                  {==}
6930                case False{}:
6931                  {==}
6932        case False{}:
6933          match b2:
6934            case True{}:
6935              match b3:
6936                case True{}:
6937                  {==}
6938                case False{}:
6939                  {==}
6940            case False{}:
6941              match b3:
6942                case True{}:
6943                  {==}
6944                case False{}:
6945                  {==}
6946    case False{}:
6947      match b1:
6948        case True{}:
6949          match b2:
6950            case True{}:
6951              match b3:
6952                case True{}:
6953                  {==}
6954                case False{}:
6955                  {==}
6956            case False{}:
6957              match b3:
6958                case True{}:
6959                  {==}
6960                case False{}:
6961                  {==}
6962        case False{}:
6963          match b2:
6964            case True{}:
6965              match b3:
6966                case True{}:
6967                  {==}
6968                case False{}:
6969                  {==}
6970            case False{}:
6971              match b3:
6972                case True{}:
6973                  {==}
6974                case False{}:
6975                  {==}