def comm16.s0100

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

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

7166def comm16.s0100(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{False{}, WCon{True{}, 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{True{}, WCon{False{}, WCon{False{}, Word.zero(28n)}}}}}) : U32}:
7167  match b0:
7168    case True{}:
7169      match b1:
7170        case True{}:
7171          match b2:
7172            case True{}:
7173              match b3:
7174                case True{}:
7175                  {==}
7176                case False{}:
7177                  {==}
7178            case False{}:
7179              match b3:
7180                case True{}:
7181                  {==}
7182                case False{}:
7183                  {==}
7184        case False{}:
7185          match b2:
7186            case True{}:
7187              match b3:
7188                case True{}:
7189                  {==}
7190                case False{}:
7191                  {==}
7192            case False{}:
7193              match b3:
7194                case True{}:
7195                  {==}
7196                case False{}:
7197                  {==}
7198    case False{}:
7199      match b1:
7200        case True{}:
7201          match b2:
7202            case True{}:
7203              match b3:
7204                case True{}:
7205                  {==}
7206                case False{}:
7207                  {==}
7208            case False{}:
7209              match b3:
7210                case True{}:
7211                  {==}
7212                case False{}:
7213                  {==}
7214        case False{}:
7215          match b2:
7216            case True{}:
7217              match b3:
7218                case True{}:
7219                  {==}
7220                case False{}:
7221                  {==}
7222            case False{}:
7223              match b3:
7224                case True{}:
7225                  {==}
7226                case False{}:
7227                  {==}