def comm16.s1011

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

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

6725def comm16.s1011(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{True{}, WCon{False{}, WCon{True{}, 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{False{}, WCon{True{}, WCon{True{}, Word.zero(28n)}}}}}) : U32}:
6726  match b0:
6727    case True{}:
6728      match b1:
6729        case True{}:
6730          match b2:
6731            case True{}:
6732              match b3:
6733                case True{}:
6734                  {==}
6735                case False{}:
6736                  {==}
6737            case False{}:
6738              match b3:
6739                case True{}:
6740                  {==}
6741                case False{}:
6742                  {==}
6743        case False{}:
6744          match b2:
6745            case True{}:
6746              match b3:
6747                case True{}:
6748                  {==}
6749                case False{}:
6750                  {==}
6751            case False{}:
6752              match b3:
6753                case True{}:
6754                  {==}
6755                case False{}:
6756                  {==}
6757    case False{}:
6758      match b1:
6759        case True{}:
6760          match b2:
6761            case True{}:
6762              match b3:
6763                case True{}:
6764                  {==}
6765                case False{}:
6766                  {==}
6767            case False{}:
6768              match b3:
6769                case True{}:
6770                  {==}
6771                case False{}:
6772                  {==}
6773        case False{}:
6774          match b2:
6775            case True{}:
6776              match b3:
6777                case True{}:
6778                  {==}
6779                case False{}:
6780                  {==}
6781            case False{}:
6782              match b3:
6783                case True{}:
6784                  {==}
6785                case False{}:
6786                  {==}