def comm16.s1100

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

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

6662def comm16.s1100(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{True{}, 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{True{}, WCon{True{}, WCon{False{}, WCon{False{}, Word.zero(28n)}}}}}) : U32}:
6663  match b0:
6664    case True{}:
6665      match b1:
6666        case True{}:
6667          match b2:
6668            case True{}:
6669              match b3:
6670                case True{}:
6671                  {==}
6672                case False{}:
6673                  {==}
6674            case False{}:
6675              match b3:
6676                case True{}:
6677                  {==}
6678                case False{}:
6679                  {==}
6680        case False{}:
6681          match b2:
6682            case True{}:
6683              match b3:
6684                case True{}:
6685                  {==}
6686                case False{}:
6687                  {==}
6688            case False{}:
6689              match b3:
6690                case True{}:
6691                  {==}
6692                case False{}:
6693                  {==}
6694    case False{}:
6695      match b1:
6696        case True{}:
6697          match b2:
6698            case True{}:
6699              match b3:
6700                case True{}:
6701                  {==}
6702                case False{}:
6703                  {==}
6704            case False{}:
6705              match b3:
6706                case True{}:
6707                  {==}
6708                case False{}:
6709                  {==}
6710        case False{}:
6711          match b2:
6712            case True{}:
6713              match b3:
6714                case True{}:
6715                  {==}
6716                case False{}:
6717                  {==}
6718            case False{}:
6719              match b3:
6720                case True{}:
6721                  {==}
6722                case False{}:
6723                  {==}