def comm16.s0001

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

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

7355def comm16.s0001(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{False{}, WCon{False{}, 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{False{}, WCon{False{}, WCon{False{}, WCon{True{}, Word.zero(28n)}}}}}) : U32}:
7356  match b0:
7357    case True{}:
7358      match b1:
7359        case True{}:
7360          match b2:
7361            case True{}:
7362              match b3:
7363                case True{}:
7364                  {==}
7365                case False{}:
7366                  {==}
7367            case False{}:
7368              match b3:
7369                case True{}:
7370                  {==}
7371                case False{}:
7372                  {==}
7373        case False{}:
7374          match b2:
7375            case True{}:
7376              match b3:
7377                case True{}:
7378                  {==}
7379                case False{}:
7380                  {==}
7381            case False{}:
7382              match b3:
7383                case True{}:
7384                  {==}
7385                case False{}:
7386                  {==}
7387    case False{}:
7388      match b1:
7389        case True{}:
7390          match b2:
7391            case True{}:
7392              match b3:
7393                case True{}:
7394                  {==}
7395                case False{}:
7396                  {==}
7397            case False{}:
7398              match b3:
7399                case True{}:
7400                  {==}
7401                case False{}:
7402                  {==}
7403        case False{}:
7404          match b2:
7405            case True{}:
7406              match b3:
7407                case True{}:
7408                  {==}
7409                case False{}:
7410                  {==}
7411            case False{}:
7412              match b3:
7413                case True{}:
7414                  {==}
7415                case False{}:
7416                  {==}