GhashBits.mulx_w: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend as GhashBits
Lines 23-88 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend&start_line=23&end_line=88

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

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

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend&name=R
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend&name=times_x
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=Block
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend&name=mulx