def comm16.s1110

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

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

6536def comm16.s1110(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{True{}, 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{True{}, WCon{True{}, WCon{True{}, WCon{False{}, Word.zero(28n)}}}}}) : U32}:
6537  match b0:
6538    case True{}:
6539      match b1:
6540        case True{}:
6541          match b2:
6542            case True{}:
6543              match b3:
6544                case True{}:
6545                  {==}
6546                case False{}:
6547                  {==}
6548            case False{}:
6549              match b3:
6550                case True{}:
6551                  {==}
6552                case False{}:
6553                  {==}
6554        case False{}:
6555          match b2:
6556            case True{}:
6557              match b3:
6558                case True{}:
6559                  {==}
6560                case False{}:
6561                  {==}
6562            case False{}:
6563              match b3:
6564                case True{}:
6565                  {==}
6566                case False{}:
6567                  {==}
6568    case False{}:
6569      match b1:
6570        case True{}:
6571          match b2:
6572            case True{}:
6573              match b3:
6574                case True{}:
6575                  {==}
6576                case False{}:
6577                  {==}
6578            case False{}:
6579              match b3:
6580                case True{}:
6581                  {==}
6582                case False{}:
6583                  {==}
6584        case False{}:
6585          match b2:
6586            case True{}:
6587              match b3:
6588                case True{}:
6589                  {==}
6590                case False{}:
6591                  {==}
6592            case False{}:
6593              match b3:
6594                case True{}:
6595                  {==}
6596                case False{}:
6597                  {==}