def mulx_w
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/ghash_bits.bend:23
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend as GhashBits
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as P
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as D
23def 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 {==}