1 import Base 2 import ../../../src/crypto/aes/types.bend as T 3 import ../../../src/crypto/aes/gcm.bend as I 4 import ../../../spec/crypto/aes/poly.bend as P 5 import ../../../spec/crypto/aes/aes.bend as S 6 import ../../../spec/crypto/aes/gcm.bend as G 7 import ./ghash_defs.bend as D 8 9 # Generated by tools/generators/aes/ghash_bits.py. 10 11 # Z xor (V and (0 - bit)) is Z + c*V. 12 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)}: 13 match c: 14 case True{}: 15 match z v: 16 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_2 17 {==} 18 case False{}: 19 match z v: 20 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_2 21 {==} 22 23 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)}: 24 match x0 y0 z0 u0: 25 case True{} True{} True{} True{}: 26 match xt yt zt ut: 27 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 28 {==} 29 case True{} True{} True{} False{}: 30 match xt yt zt ut: 31 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 32 {==} 33 case True{} True{} False{} True{}: 34 match xt yt zt ut: 35 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 36 {==} 37 case True{} True{} False{} False{}: 38 match xt yt zt ut: 39 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 40 {==} 41 case True{} False{} True{} True{}: 42 match xt yt zt ut: 43 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 44 {==} 45 case True{} False{} True{} False{}: 46 match xt yt zt ut: 47 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 48 {==} 49 case True{} False{} False{} True{}: 50 match xt yt zt ut: 51 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 52 {==} 53 case True{} False{} False{} False{}: 54 match xt yt zt ut: 55 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 56 {==} 57 case False{} True{} True{} True{}: 58 match xt yt zt ut: 59 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 60 {==} 61 case False{} True{} True{} False{}: 62 match xt yt zt ut: 63 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 64 {==} 65 case False{} True{} False{} True{}: 66 match xt yt zt ut: 67 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 68 {==} 69 case False{} True{} False{} False{}: 70 match xt yt zt ut: 71 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 72 {==} 73 case False{} False{} True{} True{}: 74 match xt yt zt ut: 75 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 76 {==} 77 case False{} False{} True{} False{}: 78 match xt yt zt ut: 79 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 80 {==} 81 case False{} False{} False{} True{}: 82 match xt yt zt ut: 83 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 84 {==} 85 case False{} False{} False{} False{}: 86 match xt yt zt ut: 87 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 88 {==} 89 90 # V * x: the shift toward x^127 with the reduction by R. 91 def mulx_ok(+v: I.Block) -> {D.R(I.mulx(v)) == P.times_x(128n, G.low(), D.R(v)) : Word(128n)}: 92 match v: 93 case I.B{U32{WCon{x0, xt}}, U32{WCon{y0, yt}}, U32{WCon{z0, zt}}, U32{WCon{u0, ut}}}: 94 mulx_w(x0, y0, z0, u0, xt, yt, zt, ut) 95 96 def mul_byte_steps(+a: U32, +acc: I.Acc) -> {I.mul_byte(a, acc) == D.steps(G.byte_bits(a), acc) : I.Acc}: 97 match a: 98 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 99 {==} 100 101 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>}: 102 match y0 y1 y2 y3 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15: 103 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, W 104 {==} 105 106 def or_false(+x: Bool) -> {Bool.or(x, False{}) == x : Bool}: 107 match x: 108 case True{}: 109 {==} 110 case False{}: 111 {==} 112 113 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{ 114 %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} 115 %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} 116 %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} 117 %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} 118 %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} 119 %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} 120 %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} 121 %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} 122 %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} 123 %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} 124 %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} 125 %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} 126 %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} 127 %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} 128 %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} 129 %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} 130 %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} 131 %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} 132 %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} 133 %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} 134 %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} 135 %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} 136 %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} 137 %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} 138 %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} 139 %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} 140 %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} 141 %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} 142 %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} 143 %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} 144 %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} 145 %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} 146 {==} 147 148 # The implementation packs four bytes into a big-endian word. 149 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}: 150 match a b c d: 151 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 152 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)) 153 154 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)}: 155 match a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15: 156 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, W 157 {==} 158 159 def bb_ok(+s: I.Block) -> {G.block_bytes(D.R(s)) == I.unpack(s) : List<&2, U32>}: 160 match s: 161 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 162 {==} 163 164 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}: 165 match c: 166 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 167 {==} 168 169 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>}: 170 match c: 171 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 172 {==}