def comm16.s0101

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

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

7103def comm16.s0101(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool) -> {M.gfm.mul.raw(M.Gfm.gf16(), U32{WCon{False{}, 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{False{}, WCon{True{}, WCon{False{}, WCon{True{}, Word.zero(28n)}}}}}) : U32}:
7104  match b0:
7105    case True{}:
7106      match b1:
7107        case True{}:
7108          match b2:
7109            case True{}:
7110              match b3:
7111                case True{}:
7112                  {==}
7113                case False{}:
7114                  {==}
7115            case False{}:
7116              match b3:
7117                case True{}:
7118                  {==}
7119                case False{}:
7120                  {==}
7121        case False{}:
7122          match b2:
7123            case True{}:
7124              match b3:
7125                case True{}:
7126                  {==}
7127                case False{}:
7128                  {==}
7129            case False{}:
7130              match b3:
7131                case True{}:
7132                  {==}
7133                case False{}:
7134                  {==}
7135    case False{}:
7136      match b1:
7137        case True{}:
7138          match b2:
7139            case True{}:
7140              match b3:
7141                case True{}:
7142                  {==}
7143                case False{}:
7144                  {==}
7145            case False{}:
7146              match b3:
7147                case True{}:
7148                  {==}
7149                case False{}:
7150                  {==}
7151        case False{}:
7152          match b2:
7153            case True{}:
7154              match b3:
7155                case True{}:
7156                  {==}
7157                case False{}:
7158                  {==}
7159            case False{}:
7160              match b3:
7161                case True{}:
7162                  {==}
7163                case False{}:
7164                  {==}