def comm16.s1101

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

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

6599def comm16.s1101(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{True{}, WCon{True{}, WCon{False{}, 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{True{}, WCon{True{}, WCon{False{}, WCon{True{}, Word.zero(28n)}}}}}) : U32}:
6600  match b0:
6601    case True{}:
6602      match b1:
6603        case True{}:
6604          match b2:
6605            case True{}:
6606              match b3:
6607                case True{}:
6608                  {==}
6609                case False{}:
6610                  {==}
6611            case False{}:
6612              match b3:
6613                case True{}:
6614                  {==}
6615                case False{}:
6616                  {==}
6617        case False{}:
6618          match b2:
6619            case True{}:
6620              match b3:
6621                case True{}:
6622                  {==}
6623                case False{}:
6624                  {==}
6625            case False{}:
6626              match b3:
6627                case True{}:
6628                  {==}
6629                case False{}:
6630                  {==}
6631    case False{}:
6632      match b1:
6633        case True{}:
6634          match b2:
6635            case True{}:
6636              match b3:
6637                case True{}:
6638                  {==}
6639                case False{}:
6640                  {==}
6641            case False{}:
6642              match b3:
6643                case True{}:
6644                  {==}
6645                case False{}:
6646                  {==}
6647        case False{}:
6648          match b2:
6649            case True{}:
6650              match b3:
6651                case True{}:
6652                  {==}
6653                case False{}:
6654                  {==}
6655            case False{}:
6656              match b3:
6657                case True{}:
6658                  {==}
6659                case False{}:
6660                  {==}