def inv32.s1

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

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

7645def inv32.s1(+b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {M.gfm.mul.raw(M.Gfm.gf32(), fixm(U32{WCon{True{}, WCon{b1, WCon{b2, WCon{b3, WCon{b4, Word.zero(27n)}}}}}}), M.Gfm.elt(M.Gfm.gf32(), M.gfm.pow.start(M.Gfm.gf32(), fixm(U32{WCon{True{}, WCon{b1, WCon{b2, WCon{b3, WCon{b4, Word.zero(27n)}}}}}}), U32.sub(M.Gfm.mask(M.Gfm.gf32()), 1)))) == 1 : U32}:
7646  match b1:
7647    case True{}:
7648      match b2:
7649        case True{}:
7650          match b3:
7651            case True{}:
7652              match b4:
7653                case True{}:
7654                  {==}
7655                case False{}:
7656                  {==}
7657            case False{}:
7658              match b4:
7659                case True{}:
7660                  {==}
7661                case False{}:
7662                  {==}
7663        case False{}:
7664          match b3:
7665            case True{}:
7666              match b4:
7667                case True{}:
7668                  {==}
7669                case False{}:
7670                  {==}
7671            case False{}:
7672              match b4:
7673                case True{}:
7674                  {==}
7675                case False{}:
7676                  {==}
7677    case False{}:
7678      match b2:
7679        case True{}:
7680          match b3:
7681            case True{}:
7682              match b4:
7683                case True{}:
7684                  {==}
7685                case False{}:
7686                  {==}
7687            case False{}:
7688              match b4:
7689                case True{}:
7690                  {==}
7691                case False{}:
7692                  {==}
7693        case False{}:
7694          match b3:
7695            case True{}:
7696              match b4:
7697                case True{}:
7698                  {==}
7699                case False{}:
7700                  {==}
7701            case False{}:
7702              match b4:
7703                case True{}:
7704                  {==}
7705                case False{}:
7706                  {==}