def comm16.s1010

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

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

6788def comm16.s1010(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{True{}, WCon{False{}, 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{False{}, WCon{True{}, WCon{False{}, Word.zero(28n)}}}}}) : U32}:
6789  match b0:
6790    case True{}:
6791      match b1:
6792        case True{}:
6793          match b2:
6794            case True{}:
6795              match b3:
6796                case True{}:
6797                  {==}
6798                case False{}:
6799                  {==}
6800            case False{}:
6801              match b3:
6802                case True{}:
6803                  {==}
6804                case False{}:
6805                  {==}
6806        case False{}:
6807          match b2:
6808            case True{}:
6809              match b3:
6810                case True{}:
6811                  {==}
6812                case False{}:
6813                  {==}
6814            case False{}:
6815              match b3:
6816                case True{}:
6817                  {==}
6818                case False{}:
6819                  {==}
6820    case False{}:
6821      match b1:
6822        case True{}:
6823          match b2:
6824            case True{}:
6825              match b3:
6826                case True{}:
6827                  {==}
6828                case False{}:
6829                  {==}
6830            case False{}:
6831              match b3:
6832                case True{}:
6833                  {==}
6834                case False{}:
6835                  {==}
6836        case False{}:
6837          match b2:
6838            case True{}:
6839              match b3:
6840                case True{}:
6841                  {==}
6842                case False{}:
6843                  {==}
6844            case False{}:
6845              match b3:
6846                case True{}:
6847                  {==}
6848                case False{}:
6849                  {==}