import Base
import ../../../src/crypto/aes/types.bend as T
import ../../../src/crypto/aes/gcm.bend as I
import ../../../spec/crypto/aes/poly.bend as P
import ../../../spec/crypto/aes/aes.bend as S
import ../../../spec/crypto/aes/gcm.bend as G
import ./ghash_defs.bend as D

# Generated by tools/generators/aes/ghash_bits.py.

# Z xor (V and (0 - bit)) is Z + c*V.
def zstep_ok(+c: Bool, +z: I.Block, +v: I.Block) -> {D.R(I.add_masked(D.bit(c), z, v)) == Word.xor(128n, D.R(z), P.wscale(128n, c, D.R(v))) : Word(128n)}:
  match c:
    case True{}:
      match z v:
        case I.B{U32{WCon{z0_0, WCon{z0_1, WCon{z0_2, WCon{z0_3, WCon{z0_4, WCon{z0_5, WCon{z0_6, WCon{z0_7, WCon{z0_8, WCon{z0_9, WCon{z0_10, WCon{z0_11, WCon{z0_12, WCon{z0_13, WCon{z0_14, WCon{z0_15, WCon{z0_16, WCon{z0_17, WCon{z0_18, WCon{z0_19, WCon{z0_20, WCon{z0_21, WCon{z0_22, WCon{z0_23, WCon{z0_24, WCon{z0_25, WCon{z0_26, WCon{z0_27, WCon{z0_28, WCon{z0_29, WCon{z0_30, WCon{z0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{z1_0, WCon{z1_1, WCon{z1_2, WCon{z1_3, WCon{z1_4, WCon{z1_5, WCon{z1_6, WCon{z1_7, WCon{z1_8, WCon{z1_9, WCon{z1_10, WCon{z1_11, WCon{z1_12, WCon{z1_13, WCon{z1_14, WCon{z1_15, WCon{z1_16, WCon{z1_17, WCon{z1_18, WCon{z1_19, WCon{z1_20, WCon{z1_21, WCon{z1_22, WCon{z1_23, WCon{z1_24, WCon{z1_25, WCon{z1_26, WCon{z1_27, WCon{z1_28, WCon{z1_29, WCon{z1_30, WCon{z1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{z2_0, WCon{z2_1, WCon{z2_2, WCon{z2_3, WCon{z2_4, WCon{z2_5, WCon{z2_6, WCon{z2_7, WCon{z2_8, WCon{z2_9, WCon{z2_10, WCon{z2_11, WCon{z2_12, WCon{z2_13, WCon{z2_14, WCon{z2_15, WCon{z2_16, WCon{z2_17, WCon{z2_18, WCon{z2_19, WCon{z2_20, WCon{z2_21, WCon{z2_22, WCon{z2_23, WCon{z2_24, WCon{z2_25, WCon{z2_26, WCon{z2_27, WCon{z2_28, WCon{z2_29, WCon{z2_30, WCon{z2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{z3_0, WCon{z3_1, WCon{z3_2, WCon{z3_3, WCon{z3_4, WCon{z3_5, WCon{z3_6, WCon{z3_7, WCon{z3_8, WCon{z3_9, WCon{z3_10, WCon{z3_11, WCon{z3_12, WCon{z3_13, WCon{z3_14, WCon{z3_15, WCon{z3_16, WCon{z3_17, WCon{z3_18, WCon{z3_19, WCon{z3_20, WCon{z3_21, WCon{z3_22, WCon{z3_23, WCon{z3_24, WCon{z3_25, WCon{z3_26, WCon{z3_27, WCon{z3_28, WCon{z3_29, WCon{z3_30, WCon{z3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} I.B{U32{WCon{v0_0, WCon{v0_1, WCon{v0_2, WCon{v0_3, WCon{v0_4, WCon{v0_5, WCon{v0_6, WCon{v0_7, WCon{v0_8, WCon{v0_9, WCon{v0_10, WCon{v0_11, WCon{v0_12, WCon{v0_13, WCon{v0_14, WCon{v0_15, WCon{v0_16, WCon{v0_17, WCon{v0_18, WCon{v0_19, WCon{v0_20, WCon{v0_21, WCon{v0_22, WCon{v0_23, WCon{v0_24, WCon{v0_25, WCon{v0_26, WCon{v0_27, WCon{v0_28, WCon{v0_29, WCon{v0_30, WCon{v0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{v1_0, WCon{v1_1, WCon{v1_2, WCon{v1_3, WCon{v1_4, WCon{v1_5, WCon{v1_6, WCon{v1_7, WCon{v1_8, WCon{v1_9, WCon{v1_10, WCon{v1_11, WCon{v1_12, WCon{v1_13, WCon{v1_14, WCon{v1_15, WCon{v1_16, WCon{v1_17, WCon{v1_18, WCon{v1_19, WCon{v1_20, WCon{v1_21, WCon{v1_22, WCon{v1_23, WCon{v1_24, WCon{v1_25, WCon{v1_26, WCon{v1_27, WCon{v1_28, WCon{v1_29, WCon{v1_30, WCon{v1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{v2_0, WCon{v2_1, WCon{v2_2, WCon{v2_3, WCon{v2_4, WCon{v2_5, WCon{v2_6, WCon{v2_7, WCon{v2_8, WCon{v2_9, WCon{v2_10, WCon{v2_11, WCon{v2_12, WCon{v2_13, WCon{v2_14, WCon{v2_15, WCon{v2_16, WCon{v2_17, WCon{v2_18, WCon{v2_19, WCon{v2_20, WCon{v2_21, WCon{v2_22, WCon{v2_23, WCon{v2_24, WCon{v2_25, WCon{v2_26, WCon{v2_27, WCon{v2_28, WCon{v2_29, WCon{v2_30, WCon{v2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{v3_0, WCon{v3_1, WCon{v3_2, WCon{v3_3, WCon{v3_4, WCon{v3_5, WCon{v3_6, WCon{v3_7, WCon{v3_8, WCon{v3_9, WCon{v3_10, WCon{v3_11, WCon{v3_12, WCon{v3_13, WCon{v3_14, WCon{v3_15, WCon{v3_16, WCon{v3_17, WCon{v3_18, WCon{v3_19, WCon{v3_20, WCon{v3_21, WCon{v3_22, WCon{v3_23, WCon{v3_24, WCon{v3_25, WCon{v3_26, WCon{v3_27, WCon{v3_28, WCon{v3_29, WCon{v3_30, WCon{v3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case False{}:
      match z v:
        case I.B{U32{WCon{z0_0, WCon{z0_1, WCon{z0_2, WCon{z0_3, WCon{z0_4, WCon{z0_5, WCon{z0_6, WCon{z0_7, WCon{z0_8, WCon{z0_9, WCon{z0_10, WCon{z0_11, WCon{z0_12, WCon{z0_13, WCon{z0_14, WCon{z0_15, WCon{z0_16, WCon{z0_17, WCon{z0_18, WCon{z0_19, WCon{z0_20, WCon{z0_21, WCon{z0_22, WCon{z0_23, WCon{z0_24, WCon{z0_25, WCon{z0_26, WCon{z0_27, WCon{z0_28, WCon{z0_29, WCon{z0_30, WCon{z0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{z1_0, WCon{z1_1, WCon{z1_2, WCon{z1_3, WCon{z1_4, WCon{z1_5, WCon{z1_6, WCon{z1_7, WCon{z1_8, WCon{z1_9, WCon{z1_10, WCon{z1_11, WCon{z1_12, WCon{z1_13, WCon{z1_14, WCon{z1_15, WCon{z1_16, WCon{z1_17, WCon{z1_18, WCon{z1_19, WCon{z1_20, WCon{z1_21, WCon{z1_22, WCon{z1_23, WCon{z1_24, WCon{z1_25, WCon{z1_26, WCon{z1_27, WCon{z1_28, WCon{z1_29, WCon{z1_30, WCon{z1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{z2_0, WCon{z2_1, WCon{z2_2, WCon{z2_3, WCon{z2_4, WCon{z2_5, WCon{z2_6, WCon{z2_7, WCon{z2_8, WCon{z2_9, WCon{z2_10, WCon{z2_11, WCon{z2_12, WCon{z2_13, WCon{z2_14, WCon{z2_15, WCon{z2_16, WCon{z2_17, WCon{z2_18, WCon{z2_19, WCon{z2_20, WCon{z2_21, WCon{z2_22, WCon{z2_23, WCon{z2_24, WCon{z2_25, WCon{z2_26, WCon{z2_27, WCon{z2_28, WCon{z2_29, WCon{z2_30, WCon{z2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{z3_0, WCon{z3_1, WCon{z3_2, WCon{z3_3, WCon{z3_4, WCon{z3_5, WCon{z3_6, WCon{z3_7, WCon{z3_8, WCon{z3_9, WCon{z3_10, WCon{z3_11, WCon{z3_12, WCon{z3_13, WCon{z3_14, WCon{z3_15, WCon{z3_16, WCon{z3_17, WCon{z3_18, WCon{z3_19, WCon{z3_20, WCon{z3_21, WCon{z3_22, WCon{z3_23, WCon{z3_24, WCon{z3_25, WCon{z3_26, WCon{z3_27, WCon{z3_28, WCon{z3_29, WCon{z3_30, WCon{z3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} I.B{U32{WCon{v0_0, WCon{v0_1, WCon{v0_2, WCon{v0_3, WCon{v0_4, WCon{v0_5, WCon{v0_6, WCon{v0_7, WCon{v0_8, WCon{v0_9, WCon{v0_10, WCon{v0_11, WCon{v0_12, WCon{v0_13, WCon{v0_14, WCon{v0_15, WCon{v0_16, WCon{v0_17, WCon{v0_18, WCon{v0_19, WCon{v0_20, WCon{v0_21, WCon{v0_22, WCon{v0_23, WCon{v0_24, WCon{v0_25, WCon{v0_26, WCon{v0_27, WCon{v0_28, WCon{v0_29, WCon{v0_30, WCon{v0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{v1_0, WCon{v1_1, WCon{v1_2, WCon{v1_3, WCon{v1_4, WCon{v1_5, WCon{v1_6, WCon{v1_7, WCon{v1_8, WCon{v1_9, WCon{v1_10, WCon{v1_11, WCon{v1_12, WCon{v1_13, WCon{v1_14, WCon{v1_15, WCon{v1_16, WCon{v1_17, WCon{v1_18, WCon{v1_19, WCon{v1_20, WCon{v1_21, WCon{v1_22, WCon{v1_23, WCon{v1_24, WCon{v1_25, WCon{v1_26, WCon{v1_27, WCon{v1_28, WCon{v1_29, WCon{v1_30, WCon{v1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{v2_0, WCon{v2_1, WCon{v2_2, WCon{v2_3, WCon{v2_4, WCon{v2_5, WCon{v2_6, WCon{v2_7, WCon{v2_8, WCon{v2_9, WCon{v2_10, WCon{v2_11, WCon{v2_12, WCon{v2_13, WCon{v2_14, WCon{v2_15, WCon{v2_16, WCon{v2_17, WCon{v2_18, WCon{v2_19, WCon{v2_20, WCon{v2_21, WCon{v2_22, WCon{v2_23, WCon{v2_24, WCon{v2_25, WCon{v2_26, WCon{v2_27, WCon{v2_28, WCon{v2_29, WCon{v2_30, WCon{v2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{v3_0, WCon{v3_1, WCon{v3_2, WCon{v3_3, WCon{v3_4, WCon{v3_5, WCon{v3_6, WCon{v3_7, WCon{v3_8, WCon{v3_9, WCon{v3_10, WCon{v3_11, WCon{v3_12, WCon{v3_13, WCon{v3_14, WCon{v3_15, WCon{v3_16, WCon{v3_17, WCon{v3_18, WCon{v3_19, WCon{v3_20, WCon{v3_21, WCon{v3_22, WCon{v3_23, WCon{v3_24, WCon{v3_25, WCon{v3_26, WCon{v3_27, WCon{v3_28, WCon{v3_29, WCon{v3_30, WCon{v3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}

def mulx_w(+x0: Bool, +y0: Bool, +z0: Bool, +u0: Bool, +xt: Word(31n), +yt: Word(31n), +zt: Word(31n), +ut: Word(31n)) -> {D.R(I.mulx(I.B{U32{WCon{x0, xt}}, U32{WCon{y0, yt}}, U32{WCon{z0, zt}}, U32{WCon{u0, ut}}})) == P.times_x(128n, G.low(), D.R(I.B{U32{WCon{x0, xt}}, U32{WCon{y0, yt}}, U32{WCon{z0, zt}}, U32{WCon{u0, ut}}})) : Word(128n)}:
  match x0 y0 z0 u0:
    case True{} True{} True{} True{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case True{} True{} True{} False{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case True{} True{} False{} True{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case True{} True{} False{} False{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case True{} False{} True{} True{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case True{} False{} True{} False{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case True{} False{} False{} True{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case True{} False{} False{} False{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case False{} True{} True{} True{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case False{} True{} True{} False{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case False{} True{} False{} True{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case False{} True{} False{} False{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case False{} False{} True{} True{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case False{} False{} True{} False{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case False{} False{} False{} True{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}
    case False{} False{} False{} False{}:
      match xt yt zt ut:
        case WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
          {==}

# V * x: the shift toward x^127 with the reduction by R.
def mulx_ok(+v: I.Block) -> {D.R(I.mulx(v)) == P.times_x(128n, G.low(), D.R(v)) : Word(128n)}:
  match v:
    case I.B{U32{WCon{x0, xt}}, U32{WCon{y0, yt}}, U32{WCon{z0, zt}}, U32{WCon{u0, ut}}}:
      mulx_w(x0, y0, z0, u0, xt, yt, zt, ut)

def mul_byte_steps(+a: U32, +acc: I.Acc) -> {I.mul_byte(a, acc) == D.steps(G.byte_bits(a), acc) : I.Acc}:
  match a:
    case U32{WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WCon{a_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
      {==}

def block_xor_ok(+y0: U32, +y1: U32, +y2: U32, +y3: U32, +x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +x8: U32, +x9: U32, +x10: U32, +x11: U32, +x12: U32, +x13: U32, +x14: U32, +x15: U32) -> {P.coefficients(128n, Word.xor(128n, D.R(I.B{y0, y1, y2, y3}), G.block([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]))) == G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])) : List<&2, Bool>}:
  match y0 y1 y2 y3 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15:
    case U32{WCon{y0_0, WCon{y0_1, WCon{y0_2, WCon{y0_3, WCon{y0_4, WCon{y0_5, WCon{y0_6, WCon{y0_7, WCon{y0_8, WCon{y0_9, WCon{y0_10, WCon{y0_11, WCon{y0_12, WCon{y0_13, WCon{y0_14, WCon{y0_15, WCon{y0_16, WCon{y0_17, WCon{y0_18, WCon{y0_19, WCon{y0_20, WCon{y0_21, WCon{y0_22, WCon{y0_23, WCon{y0_24, WCon{y0_25, WCon{y0_26, WCon{y0_27, WCon{y0_28, WCon{y0_29, WCon{y0_30, WCon{y0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y1_0, WCon{y1_1, WCon{y1_2, WCon{y1_3, WCon{y1_4, WCon{y1_5, WCon{y1_6, WCon{y1_7, WCon{y1_8, WCon{y1_9, WCon{y1_10, WCon{y1_11, WCon{y1_12, WCon{y1_13, WCon{y1_14, WCon{y1_15, WCon{y1_16, WCon{y1_17, WCon{y1_18, WCon{y1_19, WCon{y1_20, WCon{y1_21, WCon{y1_22, WCon{y1_23, WCon{y1_24, WCon{y1_25, WCon{y1_26, WCon{y1_27, WCon{y1_28, WCon{y1_29, WCon{y1_30, WCon{y1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y2_0, WCon{y2_1, WCon{y2_2, WCon{y2_3, WCon{y2_4, WCon{y2_5, WCon{y2_6, WCon{y2_7, WCon{y2_8, WCon{y2_9, WCon{y2_10, WCon{y2_11, WCon{y2_12, WCon{y2_13, WCon{y2_14, WCon{y2_15, WCon{y2_16, WCon{y2_17, WCon{y2_18, WCon{y2_19, WCon{y2_20, WCon{y2_21, WCon{y2_22, WCon{y2_23, WCon{y2_24, WCon{y2_25, WCon{y2_26, WCon{y2_27, WCon{y2_28, WCon{y2_29, WCon{y2_30, WCon{y2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y3_0, WCon{y3_1, WCon{y3_2, WCon{y3_3, WCon{y3_4, WCon{y3_5, WCon{y3_6, WCon{y3_7, WCon{y3_8, WCon{y3_9, WCon{y3_10, WCon{y3_11, WCon{y3_12, WCon{y3_13, WCon{y3_14, WCon{y3_15, WCon{y3_16, WCon{y3_17, WCon{y3_18, WCon{y3_19, WCon{y3_20, WCon{y3_21, WCon{y3_22, WCon{y3_23, WCon{y3_24, WCon{y3_25, WCon{y3_26, WCon{y3_27, WCon{y3_28, WCon{y3_29, WCon{y3_30, WCon{y3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x0_0, WCon{x0_1, WCon{x0_2, WCon{x0_3, WCon{x0_4, WCon{x0_5, WCon{x0_6, WCon{x0_7, WCon{x0_8, WCon{x0_9, WCon{x0_10, WCon{x0_11, WCon{x0_12, WCon{x0_13, WCon{x0_14, WCon{x0_15, WCon{x0_16, WCon{x0_17, WCon{x0_18, WCon{x0_19, WCon{x0_20, WCon{x0_21, WCon{x0_22, WCon{x0_23, WCon{x0_24, WCon{x0_25, WCon{x0_26, WCon{x0_27, WCon{x0_28, WCon{x0_29, WCon{x0_30, WCon{x0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x1_0, WCon{x1_1, WCon{x1_2, WCon{x1_3, WCon{x1_4, WCon{x1_5, WCon{x1_6, WCon{x1_7, WCon{x1_8, WCon{x1_9, WCon{x1_10, WCon{x1_11, WCon{x1_12, WCon{x1_13, WCon{x1_14, WCon{x1_15, WCon{x1_16, WCon{x1_17, WCon{x1_18, WCon{x1_19, WCon{x1_20, WCon{x1_21, WCon{x1_22, WCon{x1_23, WCon{x1_24, WCon{x1_25, WCon{x1_26, WCon{x1_27, WCon{x1_28, WCon{x1_29, WCon{x1_30, WCon{x1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x2_0, WCon{x2_1, WCon{x2_2, WCon{x2_3, WCon{x2_4, WCon{x2_5, WCon{x2_6, WCon{x2_7, WCon{x2_8, WCon{x2_9, WCon{x2_10, WCon{x2_11, WCon{x2_12, WCon{x2_13, WCon{x2_14, WCon{x2_15, WCon{x2_16, WCon{x2_17, WCon{x2_18, WCon{x2_19, WCon{x2_20, WCon{x2_21, WCon{x2_22, WCon{x2_23, WCon{x2_24, WCon{x2_25, WCon{x2_26, WCon{x2_27, WCon{x2_28, WCon{x2_29, WCon{x2_30, WCon{x2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x3_0, WCon{x3_1, WCon{x3_2, WCon{x3_3, WCon{x3_4, WCon{x3_5, WCon{x3_6, WCon{x3_7, WCon{x3_8, WCon{x3_9, WCon{x3_10, WCon{x3_11, WCon{x3_12, WCon{x3_13, WCon{x3_14, WCon{x3_15, WCon{x3_16, WCon{x3_17, WCon{x3_18, WCon{x3_19, WCon{x3_20, WCon{x3_21, WCon{x3_22, WCon{x3_23, WCon{x3_24, WCon{x3_25, WCon{x3_26, WCon{x3_27, WCon{x3_28, WCon{x3_29, WCon{x3_30, WCon{x3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x4_0, WCon{x4_1, WCon{x4_2, WCon{x4_3, WCon{x4_4, WCon{x4_5, WCon{x4_6, WCon{x4_7, WCon{x4_8, WCon{x4_9, WCon{x4_10, WCon{x4_11, WCon{x4_12, WCon{x4_13, WCon{x4_14, WCon{x4_15, WCon{x4_16, WCon{x4_17, WCon{x4_18, WCon{x4_19, WCon{x4_20, WCon{x4_21, WCon{x4_22, WCon{x4_23, WCon{x4_24, WCon{x4_25, WCon{x4_26, WCon{x4_27, WCon{x4_28, WCon{x4_29, WCon{x4_30, WCon{x4_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x5_0, WCon{x5_1, WCon{x5_2, WCon{x5_3, WCon{x5_4, WCon{x5_5, WCon{x5_6, WCon{x5_7, WCon{x5_8, WCon{x5_9, WCon{x5_10, WCon{x5_11, WCon{x5_12, WCon{x5_13, WCon{x5_14, WCon{x5_15, WCon{x5_16, WCon{x5_17, WCon{x5_18, WCon{x5_19, WCon{x5_20, WCon{x5_21, WCon{x5_22, WCon{x5_23, WCon{x5_24, WCon{x5_25, WCon{x5_26, WCon{x5_27, WCon{x5_28, WCon{x5_29, WCon{x5_30, WCon{x5_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x6_0, WCon{x6_1, WCon{x6_2, WCon{x6_3, WCon{x6_4, WCon{x6_5, WCon{x6_6, WCon{x6_7, WCon{x6_8, WCon{x6_9, WCon{x6_10, WCon{x6_11, WCon{x6_12, WCon{x6_13, WCon{x6_14, WCon{x6_15, WCon{x6_16, WCon{x6_17, WCon{x6_18, WCon{x6_19, WCon{x6_20, WCon{x6_21, WCon{x6_22, WCon{x6_23, WCon{x6_24, WCon{x6_25, WCon{x6_26, WCon{x6_27, WCon{x6_28, WCon{x6_29, WCon{x6_30, WCon{x6_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x7_0, WCon{x7_1, WCon{x7_2, WCon{x7_3, WCon{x7_4, WCon{x7_5, WCon{x7_6, WCon{x7_7, WCon{x7_8, WCon{x7_9, WCon{x7_10, WCon{x7_11, WCon{x7_12, WCon{x7_13, WCon{x7_14, WCon{x7_15, WCon{x7_16, WCon{x7_17, WCon{x7_18, WCon{x7_19, WCon{x7_20, WCon{x7_21, WCon{x7_22, WCon{x7_23, WCon{x7_24, WCon{x7_25, WCon{x7_26, WCon{x7_27, WCon{x7_28, WCon{x7_29, WCon{x7_30, WCon{x7_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x8_0, WCon{x8_1, WCon{x8_2, WCon{x8_3, WCon{x8_4, WCon{x8_5, WCon{x8_6, WCon{x8_7, WCon{x8_8, WCon{x8_9, WCon{x8_10, WCon{x8_11, WCon{x8_12, WCon{x8_13, WCon{x8_14, WCon{x8_15, WCon{x8_16, WCon{x8_17, WCon{x8_18, WCon{x8_19, WCon{x8_20, WCon{x8_21, WCon{x8_22, WCon{x8_23, WCon{x8_24, WCon{x8_25, WCon{x8_26, WCon{x8_27, WCon{x8_28, WCon{x8_29, WCon{x8_30, WCon{x8_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x9_0, WCon{x9_1, WCon{x9_2, WCon{x9_3, WCon{x9_4, WCon{x9_5, WCon{x9_6, WCon{x9_7, WCon{x9_8, WCon{x9_9, WCon{x9_10, WCon{x9_11, WCon{x9_12, WCon{x9_13, WCon{x9_14, WCon{x9_15, WCon{x9_16, WCon{x9_17, WCon{x9_18, WCon{x9_19, WCon{x9_20, WCon{x9_21, WCon{x9_22, WCon{x9_23, WCon{x9_24, WCon{x9_25, WCon{x9_26, WCon{x9_27, WCon{x9_28, WCon{x9_29, WCon{x9_30, WCon{x9_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x10_0, WCon{x10_1, WCon{x10_2, WCon{x10_3, WCon{x10_4, WCon{x10_5, WCon{x10_6, WCon{x10_7, WCon{x10_8, WCon{x10_9, WCon{x10_10, WCon{x10_11, WCon{x10_12, WCon{x10_13, WCon{x10_14, WCon{x10_15, WCon{x10_16, WCon{x10_17, WCon{x10_18, WCon{x10_19, WCon{x10_20, WCon{x10_21, WCon{x10_22, WCon{x10_23, WCon{x10_24, WCon{x10_25, WCon{x10_26, WCon{x10_27, WCon{x10_28, WCon{x10_29, WCon{x10_30, WCon{x10_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x11_0, WCon{x11_1, WCon{x11_2, WCon{x11_3, WCon{x11_4, WCon{x11_5, WCon{x11_6, WCon{x11_7, WCon{x11_8, WCon{x11_9, WCon{x11_10, WCon{x11_11, WCon{x11_12, WCon{x11_13, WCon{x11_14, WCon{x11_15, WCon{x11_16, WCon{x11_17, WCon{x11_18, WCon{x11_19, WCon{x11_20, WCon{x11_21, WCon{x11_22, WCon{x11_23, WCon{x11_24, WCon{x11_25, WCon{x11_26, WCon{x11_27, WCon{x11_28, WCon{x11_29, WCon{x11_30, WCon{x11_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x12_0, WCon{x12_1, WCon{x12_2, WCon{x12_3, WCon{x12_4, WCon{x12_5, WCon{x12_6, WCon{x12_7, WCon{x12_8, WCon{x12_9, WCon{x12_10, WCon{x12_11, WCon{x12_12, WCon{x12_13, WCon{x12_14, WCon{x12_15, WCon{x12_16, WCon{x12_17, WCon{x12_18, WCon{x12_19, WCon{x12_20, WCon{x12_21, WCon{x12_22, WCon{x12_23, WCon{x12_24, WCon{x12_25, WCon{x12_26, WCon{x12_27, WCon{x12_28, WCon{x12_29, WCon{x12_30, WCon{x12_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x13_0, WCon{x13_1, WCon{x13_2, WCon{x13_3, WCon{x13_4, WCon{x13_5, WCon{x13_6, WCon{x13_7, WCon{x13_8, WCon{x13_9, WCon{x13_10, WCon{x13_11, WCon{x13_12, WCon{x13_13, WCon{x13_14, WCon{x13_15, WCon{x13_16, WCon{x13_17, WCon{x13_18, WCon{x13_19, WCon{x13_20, WCon{x13_21, WCon{x13_22, WCon{x13_23, WCon{x13_24, WCon{x13_25, WCon{x13_26, WCon{x13_27, WCon{x13_28, WCon{x13_29, WCon{x13_30, WCon{x13_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x14_0, WCon{x14_1, WCon{x14_2, WCon{x14_3, WCon{x14_4, WCon{x14_5, WCon{x14_6, WCon{x14_7, WCon{x14_8, WCon{x14_9, WCon{x14_10, WCon{x14_11, WCon{x14_12, WCon{x14_13, WCon{x14_14, WCon{x14_15, WCon{x14_16, WCon{x14_17, WCon{x14_18, WCon{x14_19, WCon{x14_20, WCon{x14_21, WCon{x14_22, WCon{x14_23, WCon{x14_24, WCon{x14_25, WCon{x14_26, WCon{x14_27, WCon{x14_28, WCon{x14_29, WCon{x14_30, WCon{x14_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x15_0, WCon{x15_1, WCon{x15_2, WCon{x15_3, WCon{x15_4, WCon{x15_5, WCon{x15_6, WCon{x15_7, WCon{x15_8, WCon{x15_9, WCon{x15_10, WCon{x15_11, WCon{x15_12, WCon{x15_13, WCon{x15_14, WCon{x15_15, WCon{x15_16, WCon{x15_17, WCon{x15_18, WCon{x15_19, WCon{x15_20, WCon{x15_21, WCon{x15_22, WCon{x15_23, WCon{x15_24, WCon{x15_25, WCon{x15_26, WCon{x15_27, WCon{x15_28, WCon{x15_29, WCon{x15_30, WCon{x15_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
      {==}

def or_false(+x: Bool) -> {Bool.or(x, False{}) == x : Bool}:
  match x:
    case True{}:
      {==}
    case False{}:
      {==}

def u32_ext(+x_0: Bool, +x_1: Bool, +x_2: Bool, +x_3: Bool, +x_4: Bool, +x_5: Bool, +x_6: Bool, +x_7: Bool, +x_8: Bool, +x_9: Bool, +x_10: Bool, +x_11: Bool, +x_12: Bool, +x_13: Bool, +x_14: Bool, +x_15: Bool, +x_16: Bool, +x_17: Bool, +x_18: Bool, +x_19: Bool, +x_20: Bool, +x_21: Bool, +x_22: Bool, +x_23: Bool, +x_24: Bool, +x_25: Bool, +x_26: Bool, +x_27: Bool, +x_28: Bool, +x_29: Bool, +x_30: Bool, +x_31: Bool, +y_0: Bool, +y_1: Bool, +y_2: Bool, +y_3: Bool, +y_4: Bool, +y_5: Bool, +y_6: Bool, +y_7: Bool, +y_8: Bool, +y_9: Bool, +y_10: Bool, +y_11: Bool, +y_12: Bool, +y_13: Bool, +y_14: Bool, +y_15: Bool, +y_16: Bool, +y_17: Bool, +y_18: Bool, +y_19: Bool, +y_20: Bool, +y_21: Bool, +y_22: Bool, +y_23: Bool, +y_24: Bool, +y_25: Bool, +y_26: Bool, +y_27: Bool, +y_28: Bool, +y_29: Bool, +y_30: Bool, +y_31: Bool, +e0: {x_0 == y_0 : Bool}, +e1: {x_1 == y_1 : Bool}, +e2: {x_2 == y_2 : Bool}, +e3: {x_3 == y_3 : Bool}, +e4: {x_4 == y_4 : Bool}, +e5: {x_5 == y_5 : Bool}, +e6: {x_6 == y_6 : Bool}, +e7: {x_7 == y_7 : Bool}, +e8: {x_8 == y_8 : Bool}, +e9: {x_9 == y_9 : Bool}, +e10: {x_10 == y_10 : Bool}, +e11: {x_11 == y_11 : Bool}, +e12: {x_12 == y_12 : Bool}, +e13: {x_13 == y_13 : Bool}, +e14: {x_14 == y_14 : Bool}, +e15: {x_15 == y_15 : Bool}, +e16: {x_16 == y_16 : Bool}, +e17: {x_17 == y_17 : Bool}, +e18: {x_18 == y_18 : Bool}, +e19: {x_19 == y_19 : Bool}, +e20: {x_20 == y_20 : Bool}, +e21: {x_21 == y_21 : Bool}, +e22: {x_22 == y_22 : Bool}, +e23: {x_23 == y_23 : Bool}, +e24: {x_24 == y_24 : Bool}, +e25: {x_25 == y_25 : Bool}, +e26: {x_26 == y_26 : Bool}, +e27: {x_27 == y_27 : Bool}, +e28: {x_28 == y_28 : Bool}, +e29: {x_29 == y_29 : Bool}, +e30: {x_30 == y_30 : Bool}, +e31: {x_31 == y_31 : Bool}) -> {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{y_0, WCon{y_1, WCon{y_2, WCon{y_3, WCon{y_4, WCon{y_5, WCon{y_6, WCon{y_7, WCon{y_8, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}:
  %e0 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{_, WCon{y_1, WCon{y_2, WCon{y_3, WCon{y_4, WCon{y_5, WCon{y_6, WCon{y_7, WCon{y_8, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e1 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{_, WCon{y_2, WCon{y_3, WCon{y_4, WCon{y_5, WCon{y_6, WCon{y_7, WCon{y_8, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e2 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{_, WCon{y_3, WCon{y_4, WCon{y_5, WCon{y_6, WCon{y_7, WCon{y_8, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e3 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{_, WCon{y_4, WCon{y_5, WCon{y_6, WCon{y_7, WCon{y_8, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e4 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{_, WCon{y_5, WCon{y_6, WCon{y_7, WCon{y_8, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e5 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{_, WCon{y_6, WCon{y_7, WCon{y_8, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e6 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{_, WCon{y_7, WCon{y_8, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e7 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{_, WCon{y_8, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e8 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{_, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e9 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{_, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e10 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{_, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e11 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{_, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e12 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{_, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e13 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{_, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e14 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{_, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e15 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{_, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e16 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{_, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e17 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{_, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e18 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{_, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e19 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{_, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e20 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{_, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e21 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{_, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e22 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{_, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e23 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{_, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e24 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{_, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e25 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{_, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e26 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{_, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e27 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{_, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e28 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{_, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e29 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{_, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e30 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{_, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  %e31 : {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{_, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}
  {==}

# The implementation packs four bytes into a big-endian word.
def word_ok(+a: U32, +b: U32, +c: U32, +d: U32) -> {I.word(T.W{a, b, c, d}) == G.int32(a, b, c, d) : U32}:
  match a b c d:
    case U32{WCon{a_0, WCon{a_1, WCon{a_2, WCon{a_3, WCon{a_4, WCon{a_5, WCon{a_6, WCon{a_7, WCon{a_8, WCon{a_9, WCon{a_10, WCon{a_11, WCon{a_12, WCon{a_13, WCon{a_14, WCon{a_15, WCon{a_16, WCon{a_17, WCon{a_18, WCon{a_19, WCon{a_20, WCon{a_21, WCon{a_22, WCon{a_23, WCon{a_24, WCon{a_25, WCon{a_26, WCon{a_27, WCon{a_28, WCon{a_29, WCon{a_30, WCon{a_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b_0, WCon{b_1, WCon{b_2, WCon{b_3, WCon{b_4, WCon{b_5, WCon{b_6, WCon{b_7, WCon{b_8, WCon{b_9, WCon{b_10, WCon{b_11, WCon{b_12, WCon{b_13, WCon{b_14, WCon{b_15, WCon{b_16, WCon{b_17, WCon{b_18, WCon{b_19, WCon{b_20, WCon{b_21, WCon{b_22, WCon{b_23, WCon{b_24, WCon{b_25, WCon{b_26, WCon{b_27, WCon{b_28, WCon{b_29, WCon{b_30, WCon{b_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WCon{c_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{d_0, WCon{d_1, WCon{d_2, WCon{d_3, WCon{d_4, WCon{d_5, WCon{d_6, WCon{d_7, WCon{d_8, WCon{d_9, WCon{d_10, WCon{d_11, WCon{d_12, WCon{d_13, WCon{d_14, WCon{d_15, WCon{d_16, WCon{d_17, WCon{d_18, WCon{d_19, WCon{d_20, WCon{d_21, WCon{d_22, WCon{d_23, WCon{d_24, WCon{d_25, WCon{d_26, WCon{d_27, WCon{d_28, WCon{d_29, WCon{d_30, WCon{d_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
      u32_ext(d_0, d_1, d_2, d_3, d_4, d_5, d_6, d_7, Bool.or(c_0, False{}), Bool.or(c_1, False{}), Bool.or(c_2, False{}), Bool.or(c_3, False{}), Bool.or(c_4, False{}), Bool.or(c_5, False{}), Bool.or(c_6, False{}), Bool.or(c_7, False{}), Bool.or(b_0, False{}), Bool.or(b_1, False{}), Bool.or(b_2, False{}), Bool.or(b_3, False{}), Bool.or(b_4, False{}), Bool.or(b_5, False{}), Bool.or(b_6, False{}), Bool.or(b_7, False{}), Bool.or(a_0, False{}), Bool.or(a_1, False{}), Bool.or(a_2, False{}), Bool.or(a_3, False{}), Bool.or(a_4, False{}), Bool.or(a_5, False{}), Bool.or(a_6, False{}), Bool.or(a_7, False{}), d_0, d_1, d_2, d_3, d_4, d_5, d_6, d_7, c_0, c_1, c_2, c_3, c_4, c_5, c_6, c_7, b_0, b_1, b_2, b_3, b_4, b_5, b_6, b_7, a_0, a_1, a_2, a_3, a_4, a_5, a_6, a_7, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, or_false(c_0), or_false(c_1), or_false(c_2), or_false(c_3), or_false(c_4), or_false(c_5), or_false(c_6), or_false(c_7), or_false(b_0), or_false(b_1), or_false(b_2), or_false(b_3), or_false(b_4), or_false(b_5), or_false(b_6), or_false(b_7), or_false(a_0), or_false(a_1), or_false(a_2), or_false(a_3), or_false(a_4), or_false(a_5), or_false(a_6), or_false(a_7))

def pack_int(+a0: U32, +a1: U32, +a2: U32, +a3: U32, +a4: U32, +a5: U32, +a6: U32, +a7: U32, +a8: U32, +a9: U32, +a10: U32, +a11: U32, +a12: U32, +a13: U32, +a14: U32, +a15: U32) -> {D.R(I.B{G.int32(a0, a1, a2, a3), G.int32(a4, a5, a6, a7), G.int32(a8, a9, a10, a11), G.int32(a12, a13, a14, a15)}) == G.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}:
  match a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15:
    case U32{WCon{a0_0, WCon{a0_1, WCon{a0_2, WCon{a0_3, WCon{a0_4, WCon{a0_5, WCon{a0_6, WCon{a0_7, WCon{a0_8, WCon{a0_9, WCon{a0_10, WCon{a0_11, WCon{a0_12, WCon{a0_13, WCon{a0_14, WCon{a0_15, WCon{a0_16, WCon{a0_17, WCon{a0_18, WCon{a0_19, WCon{a0_20, WCon{a0_21, WCon{a0_22, WCon{a0_23, WCon{a0_24, WCon{a0_25, WCon{a0_26, WCon{a0_27, WCon{a0_28, WCon{a0_29, WCon{a0_30, WCon{a0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a1_0, WCon{a1_1, WCon{a1_2, WCon{a1_3, WCon{a1_4, WCon{a1_5, WCon{a1_6, WCon{a1_7, WCon{a1_8, WCon{a1_9, WCon{a1_10, WCon{a1_11, WCon{a1_12, WCon{a1_13, WCon{a1_14, WCon{a1_15, WCon{a1_16, WCon{a1_17, WCon{a1_18, WCon{a1_19, WCon{a1_20, WCon{a1_21, WCon{a1_22, WCon{a1_23, WCon{a1_24, WCon{a1_25, WCon{a1_26, WCon{a1_27, WCon{a1_28, WCon{a1_29, WCon{a1_30, WCon{a1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a2_0, WCon{a2_1, WCon{a2_2, WCon{a2_3, WCon{a2_4, WCon{a2_5, WCon{a2_6, WCon{a2_7, WCon{a2_8, WCon{a2_9, WCon{a2_10, WCon{a2_11, WCon{a2_12, WCon{a2_13, WCon{a2_14, WCon{a2_15, WCon{a2_16, WCon{a2_17, WCon{a2_18, WCon{a2_19, WCon{a2_20, WCon{a2_21, WCon{a2_22, WCon{a2_23, WCon{a2_24, WCon{a2_25, WCon{a2_26, WCon{a2_27, WCon{a2_28, WCon{a2_29, WCon{a2_30, WCon{a2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a3_0, WCon{a3_1, WCon{a3_2, WCon{a3_3, WCon{a3_4, WCon{a3_5, WCon{a3_6, WCon{a3_7, WCon{a3_8, WCon{a3_9, WCon{a3_10, WCon{a3_11, WCon{a3_12, WCon{a3_13, WCon{a3_14, WCon{a3_15, WCon{a3_16, WCon{a3_17, WCon{a3_18, WCon{a3_19, WCon{a3_20, WCon{a3_21, WCon{a3_22, WCon{a3_23, WCon{a3_24, WCon{a3_25, WCon{a3_26, WCon{a3_27, WCon{a3_28, WCon{a3_29, WCon{a3_30, WCon{a3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a4_0, WCon{a4_1, WCon{a4_2, WCon{a4_3, WCon{a4_4, WCon{a4_5, WCon{a4_6, WCon{a4_7, WCon{a4_8, WCon{a4_9, WCon{a4_10, WCon{a4_11, WCon{a4_12, WCon{a4_13, WCon{a4_14, WCon{a4_15, WCon{a4_16, WCon{a4_17, WCon{a4_18, WCon{a4_19, WCon{a4_20, WCon{a4_21, WCon{a4_22, WCon{a4_23, WCon{a4_24, WCon{a4_25, WCon{a4_26, WCon{a4_27, WCon{a4_28, WCon{a4_29, WCon{a4_30, WCon{a4_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a5_0, WCon{a5_1, WCon{a5_2, WCon{a5_3, WCon{a5_4, WCon{a5_5, WCon{a5_6, WCon{a5_7, WCon{a5_8, WCon{a5_9, WCon{a5_10, WCon{a5_11, WCon{a5_12, WCon{a5_13, WCon{a5_14, WCon{a5_15, WCon{a5_16, WCon{a5_17, WCon{a5_18, WCon{a5_19, WCon{a5_20, WCon{a5_21, WCon{a5_22, WCon{a5_23, WCon{a5_24, WCon{a5_25, WCon{a5_26, WCon{a5_27, WCon{a5_28, WCon{a5_29, WCon{a5_30, WCon{a5_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a6_0, WCon{a6_1, WCon{a6_2, WCon{a6_3, WCon{a6_4, WCon{a6_5, WCon{a6_6, WCon{a6_7, WCon{a6_8, WCon{a6_9, WCon{a6_10, WCon{a6_11, WCon{a6_12, WCon{a6_13, WCon{a6_14, WCon{a6_15, WCon{a6_16, WCon{a6_17, WCon{a6_18, WCon{a6_19, WCon{a6_20, WCon{a6_21, WCon{a6_22, WCon{a6_23, WCon{a6_24, WCon{a6_25, WCon{a6_26, WCon{a6_27, WCon{a6_28, WCon{a6_29, WCon{a6_30, WCon{a6_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a7_0, WCon{a7_1, WCon{a7_2, WCon{a7_3, WCon{a7_4, WCon{a7_5, WCon{a7_6, WCon{a7_7, WCon{a7_8, WCon{a7_9, WCon{a7_10, WCon{a7_11, WCon{a7_12, WCon{a7_13, WCon{a7_14, WCon{a7_15, WCon{a7_16, WCon{a7_17, WCon{a7_18, WCon{a7_19, WCon{a7_20, WCon{a7_21, WCon{a7_22, WCon{a7_23, WCon{a7_24, WCon{a7_25, WCon{a7_26, WCon{a7_27, WCon{a7_28, WCon{a7_29, WCon{a7_30, WCon{a7_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a8_0, WCon{a8_1, WCon{a8_2, WCon{a8_3, WCon{a8_4, WCon{a8_5, WCon{a8_6, WCon{a8_7, WCon{a8_8, WCon{a8_9, WCon{a8_10, WCon{a8_11, WCon{a8_12, WCon{a8_13, WCon{a8_14, WCon{a8_15, WCon{a8_16, WCon{a8_17, WCon{a8_18, WCon{a8_19, WCon{a8_20, WCon{a8_21, WCon{a8_22, WCon{a8_23, WCon{a8_24, WCon{a8_25, WCon{a8_26, WCon{a8_27, WCon{a8_28, WCon{a8_29, WCon{a8_30, WCon{a8_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a9_0, WCon{a9_1, WCon{a9_2, WCon{a9_3, WCon{a9_4, WCon{a9_5, WCon{a9_6, WCon{a9_7, WCon{a9_8, WCon{a9_9, WCon{a9_10, WCon{a9_11, WCon{a9_12, WCon{a9_13, WCon{a9_14, WCon{a9_15, WCon{a9_16, WCon{a9_17, WCon{a9_18, WCon{a9_19, WCon{a9_20, WCon{a9_21, WCon{a9_22, WCon{a9_23, WCon{a9_24, WCon{a9_25, WCon{a9_26, WCon{a9_27, WCon{a9_28, WCon{a9_29, WCon{a9_30, WCon{a9_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a10_0, WCon{a10_1, WCon{a10_2, WCon{a10_3, WCon{a10_4, WCon{a10_5, WCon{a10_6, WCon{a10_7, WCon{a10_8, WCon{a10_9, WCon{a10_10, WCon{a10_11, WCon{a10_12, WCon{a10_13, WCon{a10_14, WCon{a10_15, WCon{a10_16, WCon{a10_17, WCon{a10_18, WCon{a10_19, WCon{a10_20, WCon{a10_21, WCon{a10_22, WCon{a10_23, WCon{a10_24, WCon{a10_25, WCon{a10_26, WCon{a10_27, WCon{a10_28, WCon{a10_29, WCon{a10_30, WCon{a10_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a11_0, WCon{a11_1, WCon{a11_2, WCon{a11_3, WCon{a11_4, WCon{a11_5, WCon{a11_6, WCon{a11_7, WCon{a11_8, WCon{a11_9, WCon{a11_10, WCon{a11_11, WCon{a11_12, WCon{a11_13, WCon{a11_14, WCon{a11_15, WCon{a11_16, WCon{a11_17, WCon{a11_18, WCon{a11_19, WCon{a11_20, WCon{a11_21, WCon{a11_22, WCon{a11_23, WCon{a11_24, WCon{a11_25, WCon{a11_26, WCon{a11_27, WCon{a11_28, WCon{a11_29, WCon{a11_30, WCon{a11_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a12_0, WCon{a12_1, WCon{a12_2, WCon{a12_3, WCon{a12_4, WCon{a12_5, WCon{a12_6, WCon{a12_7, WCon{a12_8, WCon{a12_9, WCon{a12_10, WCon{a12_11, WCon{a12_12, WCon{a12_13, WCon{a12_14, WCon{a12_15, WCon{a12_16, WCon{a12_17, WCon{a12_18, WCon{a12_19, WCon{a12_20, WCon{a12_21, WCon{a12_22, WCon{a12_23, WCon{a12_24, WCon{a12_25, WCon{a12_26, WCon{a12_27, WCon{a12_28, WCon{a12_29, WCon{a12_30, WCon{a12_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a13_0, WCon{a13_1, WCon{a13_2, WCon{a13_3, WCon{a13_4, WCon{a13_5, WCon{a13_6, WCon{a13_7, WCon{a13_8, WCon{a13_9, WCon{a13_10, WCon{a13_11, WCon{a13_12, WCon{a13_13, WCon{a13_14, WCon{a13_15, WCon{a13_16, WCon{a13_17, WCon{a13_18, WCon{a13_19, WCon{a13_20, WCon{a13_21, WCon{a13_22, WCon{a13_23, WCon{a13_24, WCon{a13_25, WCon{a13_26, WCon{a13_27, WCon{a13_28, WCon{a13_29, WCon{a13_30, WCon{a13_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a14_0, WCon{a14_1, WCon{a14_2, WCon{a14_3, WCon{a14_4, WCon{a14_5, WCon{a14_6, WCon{a14_7, WCon{a14_8, WCon{a14_9, WCon{a14_10, WCon{a14_11, WCon{a14_12, WCon{a14_13, WCon{a14_14, WCon{a14_15, WCon{a14_16, WCon{a14_17, WCon{a14_18, WCon{a14_19, WCon{a14_20, WCon{a14_21, WCon{a14_22, WCon{a14_23, WCon{a14_24, WCon{a14_25, WCon{a14_26, WCon{a14_27, WCon{a14_28, WCon{a14_29, WCon{a14_30, WCon{a14_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a15_0, WCon{a15_1, WCon{a15_2, WCon{a15_3, WCon{a15_4, WCon{a15_5, WCon{a15_6, WCon{a15_7, WCon{a15_8, WCon{a15_9, WCon{a15_10, WCon{a15_11, WCon{a15_12, WCon{a15_13, WCon{a15_14, WCon{a15_15, WCon{a15_16, WCon{a15_17, WCon{a15_18, WCon{a15_19, WCon{a15_20, WCon{a15_21, WCon{a15_22, WCon{a15_23, WCon{a15_24, WCon{a15_25, WCon{a15_26, WCon{a15_27, WCon{a15_28, WCon{a15_29, WCon{a15_30, WCon{a15_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
      {==}

def bb_ok(+s: I.Block) -> {G.block_bytes(D.R(s)) == I.unpack(s) : List<&2, U32>}:
  match s:
    case I.B{U32{WCon{s0_0, WCon{s0_1, WCon{s0_2, WCon{s0_3, WCon{s0_4, WCon{s0_5, WCon{s0_6, WCon{s0_7, WCon{s0_8, WCon{s0_9, WCon{s0_10, WCon{s0_11, WCon{s0_12, WCon{s0_13, WCon{s0_14, WCon{s0_15, WCon{s0_16, WCon{s0_17, WCon{s0_18, WCon{s0_19, WCon{s0_20, WCon{s0_21, WCon{s0_22, WCon{s0_23, WCon{s0_24, WCon{s0_25, WCon{s0_26, WCon{s0_27, WCon{s0_28, WCon{s0_29, WCon{s0_30, WCon{s0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{s1_0, WCon{s1_1, WCon{s1_2, WCon{s1_3, WCon{s1_4, WCon{s1_5, WCon{s1_6, WCon{s1_7, WCon{s1_8, WCon{s1_9, WCon{s1_10, WCon{s1_11, WCon{s1_12, WCon{s1_13, WCon{s1_14, WCon{s1_15, WCon{s1_16, WCon{s1_17, WCon{s1_18, WCon{s1_19, WCon{s1_20, WCon{s1_21, WCon{s1_22, WCon{s1_23, WCon{s1_24, WCon{s1_25, WCon{s1_26, WCon{s1_27, WCon{s1_28, WCon{s1_29, WCon{s1_30, WCon{s1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{s2_0, WCon{s2_1, WCon{s2_2, WCon{s2_3, WCon{s2_4, WCon{s2_5, WCon{s2_6, WCon{s2_7, WCon{s2_8, WCon{s2_9, WCon{s2_10, WCon{s2_11, WCon{s2_12, WCon{s2_13, WCon{s2_14, WCon{s2_15, WCon{s2_16, WCon{s2_17, WCon{s2_18, WCon{s2_19, WCon{s2_20, WCon{s2_21, WCon{s2_22, WCon{s2_23, WCon{s2_24, WCon{s2_25, WCon{s2_26, WCon{s2_27, WCon{s2_28, WCon{s2_29, WCon{s2_30, WCon{s2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{s3_0, WCon{s3_1, WCon{s3_2, WCon{s3_3, WCon{s3_4, WCon{s3_5, WCon{s3_6, WCon{s3_7, WCon{s3_8, WCon{s3_9, WCon{s3_10, WCon{s3_11, WCon{s3_12, WCon{s3_13, WCon{s3_14, WCon{s3_15, WCon{s3_16, WCon{s3_17, WCon{s3_18, WCon{s3_19, WCon{s3_20, WCon{s3_21, WCon{s3_22, WCon{s3_23, WCon{s3_24, WCon{s3_25, WCon{s3_26, WCon{s3_27, WCon{s3_28, WCon{s3_29, WCon{s3_30, WCon{s3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
      {==}

def int32_ctr(+c: U32) -> {G.int32(U32.and(255, U32.shrn(c, 24n)), U32.and(255, U32.shrn(c, 16n)), U32.and(255, U32.shrn(c, 8n)), U32.and(255, c)) == c : U32}:
  match c:
    case U32{WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WCon{c_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
      {==}

def str32_ctr(+c: U32) -> {G.str32(c) == [U32.and(255, U32.shrn(c, 24n)), U32.and(255, U32.shrn(c, 16n)), U32.and(255, U32.shrn(c, 8n)), U32.and(255, c)] : List<&2, U32>}:
  match c:
    case U32{WCon{c_0, WCon{c_1, WCon{c_2, WCon{c_3, WCon{c_4, WCon{c_5, WCon{c_6, WCon{c_7, WCon{c_8, WCon{c_9, WCon{c_10, WCon{c_11, WCon{c_12, WCon{c_13, WCon{c_14, WCon{c_15, WCon{c_16, WCon{c_17, WCon{c_18, WCon{c_19, WCon{c_20, WCon{c_21, WCon{c_22, WCon{c_23, WCon{c_24, WCon{c_25, WCon{c_26, WCon{c_27, WCon{c_28, WCon{c_29, WCon{c_30, WCon{c_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
      {==}