def inv32.s0

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

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

7708def inv32.s0(+b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {M.gfm.mul.raw(M.Gfm.gf32(), fixm(U32{WCon{False{}, 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{False{}, WCon{b1, WCon{b2, WCon{b3, WCon{b4, Word.zero(27n)}}}}}}), U32.sub(M.Gfm.mask(M.Gfm.gf32()), 1)))) == 1 : U32}:
7709  match b1:
7710    case True{}:
7711      match b2:
7712        case True{}:
7713          match b3:
7714            case True{}:
7715              match b4:
7716                case True{}:
7717                  {==}
7718                case False{}:
7719                  {==}
7720            case False{}:
7721              match b4:
7722                case True{}:
7723                  {==}
7724                case False{}:
7725                  {==}
7726        case False{}:
7727          match b3:
7728            case True{}:
7729              match b4:
7730                case True{}:
7731                  {==}
7732                case False{}:
7733                  {==}
7734            case False{}:
7735              match b4:
7736                case True{}:
7737                  {==}
7738                case False{}:
7739                  {==}
7740    case False{}:
7741      match b2:
7742        case True{}:
7743          match b3:
7744            case True{}:
7745              match b4:
7746                case True{}:
7747                  {==}
7748                case False{}:
7749                  {==}
7750            case False{}:
7751              match b4:
7752                case True{}:
7753                  {==}
7754                case False{}:
7755                  {==}
7756        case False{}:
7757          match b3:
7758            case True{}:
7759              match b4:
7760                case True{}:
7761                  {==}
7762                case False{}:
7763                  {==}
7764            case False{}:
7765              match b4:
7766                case True{}:
7767                  {==}
7768                case False{}:
7769                  {==}