Aead.gctr_inv: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend as Aead
Lines 304-372 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&start_line=304&end_line=372

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G

# Counter mode is an involution (the keystream is XORed twice).
def gctr_inv(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +xs: List<&2, U32>, +cb: List<&2, U32>) -> {G.gctr(nk, nr, key, G.gctr(nk, nr, key, xs, cb), cb) == xs : List<&2, U32>}:
  match xs:
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> rest:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> rest, cb), U32.xor(x0, kb(nk, nr, key, cb, 0n)) <> U32.xor(x1, kb(nk, nr, key, cb, 1n)) <> U32.xor(x2, kb(nk, nr, key, cb, 2n)) <> U32.xor(x3, kb(nk, nr, key, cb, 3n)) <> U32.xor(x4, kb(nk, nr, key, cb, 4n)) <> U32.xor(x5, kb(nk, nr, key, cb, 5n)) <> U32.xor(x6, kb(nk, nr, key, cb, 6n)) <> U32.xor(x7, kb(nk, nr, key, cb, 7n)) <> U32.xor(x8, kb(nk, nr, key, cb, 8n)) <> U32.xor(x9, kb(nk, nr, key, cb, 9n)) <> U32.xor(x10, kb(nk, nr, key, cb, 10n)) <> U32.xor(x11, kb(nk, nr, key, cb, 11n)) <> U32.xor(x12, kb(nk, nr, key, cb, 12n)) <> U32.xor(x13, kb(nk, nr, key, cb, 13n)) <> U32.xor(x14, kb(nk, nr, key, cb, 14n)) <> U32.xor(x15, kb(nk, nr, key, cb, 15n)) <> G.gctr(nk, nr, key, rest, G.inc32(cb)), gctr_block(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, rest, cb)) : {G.gctr(nk, nr, key, _, cb) == x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> rest : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)) <> U32.xor(x1, kb(nk, nr, key, cb, 1n)) <> U32.xor(x2, kb(nk, nr, key, cb, 2n)) <> U32.xor(x3, kb(nk, nr, key, cb, 3n)) <> U32.xor(x4, kb(nk, nr, key, cb, 4n)) <> U32.xor(x5, kb(nk, nr, key, cb, 5n)) <> U32.xor(x6, kb(nk, nr, key, cb, 6n)) <> U32.xor(x7, kb(nk, nr, key, cb, 7n)) <> U32.xor(x8, kb(nk, nr, key, cb, 8n)) <> U32.xor(x9, kb(nk, nr, key, cb, 9n)) <> U32.xor(x10, kb(nk, nr, key, cb, 10n)) <> U32.xor(x11, kb(nk, nr, key, cb, 11n)) <> U32.xor(x12, kb(nk, nr, key, cb, 12n)) <> U32.xor(x13, kb(nk, nr, key, cb, 13n)) <> U32.xor(x14, kb(nk, nr, key, cb, 14n)) <> U32.xor(x15, kb(nk, nr, key, cb, 15n)) <> G.gctr(nk, nr, key, rest, G.inc32(cb)), cb), U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)) <> U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)) <> U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)) <> U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)) <> U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)) <> U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)) <> U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)) <> U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)) <> U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)) <> U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)) <> U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n)) <> U32.xor(U32.xor(x11, kb(nk, nr, key, cb, 11n)), kb(nk, nr, key, cb, 11n)) <> U32.xor(U32.xor(x12, kb(nk, nr, key, cb, 12n)), kb(nk, nr, key, cb, 12n)) <> U32.xor(U32.xor(x13, kb(nk, nr, key, cb, 13n)), kb(nk, nr, key, cb, 13n)) <> U32.xor(U32.xor(x14, kb(nk, nr, key, cb, 14n)), kb(nk, nr, key, cb, 14n)) <> U32.xor(U32.xor(x15, kb(nk, nr, key, cb, 15n)), kb(nk, nr, key, cb, 15n)) <> G.gctr(nk, nr, key, G.gctr(nk, nr, key, rest, G.inc32(cb)), G.inc32(cb)), gctr_block(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n)), U32.xor(x15, kb(nk, nr, key, cb, 15n)), G.gctr(nk, nr, key, rest, G.inc32(cb)), cb)) : {_ == x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> rest : List<&2, U32>}
      cancel16(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n), kb(nk, nr, key, cb, 11n), kb(nk, nr, key, cb, 12n), kb(nk, nr, key, cb, 13n), kb(nk, nr, key, cb, 14n), kb(nk, nr, key, cb, 15n), G.gctr(nk, nr, key, G.gctr(nk, nr, key, rest, G.inc32(cb)), G.inc32(cb)), rest, gctr_inv(nk, nr, key, rest, G.inc32(cb)))
    case Nil{}:
      {==}
    case x0 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n))], gctr_part1(nk, nr, key, x0, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n))], gctr_part1(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), cb)) : {_ == [x0] : List<&2, U32>}
      cancel1(x0, kb(nk, nr, key, cb, 0n))
    case x0 <> x1 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n))], gctr_part2(nk, nr, key, x0, x1, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n))], gctr_part2(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), cb)) : {_ == [x0, x1] : List<&2, U32>}
      cancel2(x0, x1, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n))
    case x0 <> x1 <> x2 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n))], gctr_part3(nk, nr, key, x0, x1, x2, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n))], gctr_part3(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), cb)) : {_ == [x0, x1, x2] : List<&2, U32>}
      cancel3(x0, x1, x2, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n))
    case x0 <> x1 <> x2 <> x3 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n))], gctr_part4(nk, nr, key, x0, x1, x2, x3, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n))], gctr_part4(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), cb)) : {_ == [x0, x1, x2, x3] : List<&2, U32>}
      cancel4(x0, x1, x2, x3, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n))], gctr_part5(nk, nr, key, x0, x1, x2, x3, x4, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n))], gctr_part5(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), cb)) : {_ == [x0, x1, x2, x3, x4] : List<&2, U32>}
      cancel5(x0, x1, x2, x3, x4, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n))], gctr_part6(nk, nr, key, x0, x1, x2, x3, x4, x5, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n))], gctr_part6(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5] : List<&2, U32>}
      cancel6(x0, x1, x2, x3, x4, x5, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n))], gctr_part7(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n))], gctr_part7(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6] : List<&2, U32>}
      cancel7(x0, x1, x2, x3, x4, x5, x6, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n))], gctr_part8(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n))], gctr_part8(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7] : List<&2, U32>}
      cancel8(x0, x1, x2, x3, x4, x5, x6, x7, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n))], gctr_part9(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n))], gctr_part9(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8] : List<&2, U32>}
      cancel9(x0, x1, x2, x3, x4, x5, x6, x7, x8, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n))], gctr_part10(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n))], gctr_part10(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9] : List<&2, U32>}
      cancel10(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n))], gctr_part11(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)), U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n))], gctr_part11(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10] : List<&2, U32>}
      cancel11(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n))], gctr_part12(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)), U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n)), U32.xor(U32.xor(x11, kb(nk, nr, key, cb, 11n)), kb(nk, nr, key, cb, 11n))], gctr_part12(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}
      cancel12(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n), kb(nk, nr, key, cb, 11n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n))], gctr_part13(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)), U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n)), U32.xor(U32.xor(x11, kb(nk, nr, key, cb, 11n)), kb(nk, nr, key, cb, 11n)), U32.xor(U32.xor(x12, kb(nk, nr, key, cb, 12n)), kb(nk, nr, key, cb, 12n))], gctr_part13(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] : List<&2, U32>}
      cancel13(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n), kb(nk, nr, key, cb, 11n), kb(nk, nr, key, cb, 12n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n))], gctr_part14(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)), U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n)), U32.xor(U32.xor(x11, kb(nk, nr, key, cb, 11n)), kb(nk, nr, key, cb, 11n)), U32.xor(U32.xor(x12, kb(nk, nr, key, cb, 12n)), kb(nk, nr, key, cb, 12n)), U32.xor(U32.xor(x13, kb(nk, nr, key, cb, 13n)), kb(nk, nr, key, cb, 13n))], gctr_part14(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13] : List<&2, U32>}
      cancel14(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n), kb(nk, nr, key, cb, 11n), kb(nk, nr, key, cb, 12n), kb(nk, nr, key, cb, 13n))
    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> Nil{}:
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n))], gctr_part15(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14] : List<&2, U32>}
      %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)), U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n)), U32.xor(U32.xor(x11, kb(nk, nr, key, cb, 11n)), kb(nk, nr, key, cb, 11n)), U32.xor(U32.xor(x12, kb(nk, nr, key, cb, 12n)), kb(nk, nr, key, cb, 12n)), U32.xor(U32.xor(x13, kb(nk, nr, key, cb, 13n)), kb(nk, nr, key, cb, 13n)), U32.xor(U32.xor(x14, kb(nk, nr, key, cb, 14n)), kb(nk, nr, key, cb, 14n))], gctr_part15(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14] : List<&2, U32>}
      cancel15(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n), kb(nk, nr, key, cb, 11n), kb(nk, nr, key, cb, 12n), kb(nk, nr, key, cb, 13n), kb(nk, nr, key, cb, 14n))

Uses (40):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel10
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel11
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel12
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel13
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel14
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel15
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel4
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel5
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel6
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel7
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel8
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel9
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_block
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part10
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part11
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part12
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part13
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part14
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part15
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part4
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part5
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part6
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part7
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part8
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=gctr_part9
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=kb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=gctr
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=inc32