def comm16.s0110

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

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

7040def comm16.s0110(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{False{}, WCon{True{}, WCon{True{}, 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{True{}, WCon{False{}, Word.zero(28n)}}}}}) : U32}:
7041  match b0:
7042    case True{}:
7043      match b1:
7044        case True{}:
7045          match b2:
7046            case True{}:
7047              match b3:
7048                case True{}:
7049                  {==}
7050                case False{}:
7051                  {==}
7052            case False{}:
7053              match b3:
7054                case True{}:
7055                  {==}
7056                case False{}:
7057                  {==}
7058        case False{}:
7059          match b2:
7060            case True{}:
7061              match b3:
7062                case True{}:
7063                  {==}
7064                case False{}:
7065                  {==}
7066            case False{}:
7067              match b3:
7068                case True{}:
7069                  {==}
7070                case False{}:
7071                  {==}
7072    case False{}:
7073      match b1:
7074        case True{}:
7075          match b2:
7076            case True{}:
7077              match b3:
7078                case True{}:
7079                  {==}
7080                case False{}:
7081                  {==}
7082            case False{}:
7083              match b3:
7084                case True{}:
7085                  {==}
7086                case False{}:
7087                  {==}
7088        case False{}:
7089          match b2:
7090            case True{}:
7091              match b3:
7092                case True{}:
7093                  {==}
7094                case False{}:
7095                  {==}
7096            case False{}:
7097              match b3:
7098                case True{}:
7099                  {==}
7100                case False{}:
7101                  {==}