def comm16.s0111

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

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

6977def comm16.s0111(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{False{}, WCon{True{}, WCon{True{}, 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{False{}, WCon{True{}, WCon{True{}, WCon{True{}, Word.zero(28n)}}}}}) : U32}:
6978  match b0:
6979    case True{}:
6980      match b1:
6981        case True{}:
6982          match b2:
6983            case True{}:
6984              match b3:
6985                case True{}:
6986                  {==}
6987                case False{}:
6988                  {==}
6989            case False{}:
6990              match b3:
6991                case True{}:
6992                  {==}
6993                case False{}:
6994                  {==}
6995        case False{}:
6996          match b2:
6997            case True{}:
6998              match b3:
6999                case True{}:
7000                  {==}
7001                case False{}:
7002                  {==}
7003            case False{}:
7004              match b3:
7005                case True{}:
7006                  {==}
7007                case False{}:
7008                  {==}
7009    case False{}:
7010      match b1:
7011        case True{}:
7012          match b2:
7013            case True{}:
7014              match b3:
7015                case True{}:
7016                  {==}
7017                case False{}:
7018                  {==}
7019            case False{}:
7020              match b3:
7021                case True{}:
7022                  {==}
7023                case False{}:
7024                  {==}
7025        case False{}:
7026          match b2:
7027            case True{}:
7028              match b3:
7029                case True{}:
7030                  {==}
7031                case False{}:
7032                  {==}
7033            case False{}:
7034              match b3:
7035                case True{}:
7036                  {==}
7037                case False{}:
7038                  {==}