AESTraceProof.expand_step_at: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend as AESTraceProof
Lines 38-50 of qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend&start_line=38&end_line=50

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

def expand_step_at(+fuel: Nat, +i: U32, +rcon: U32, +words: List<&2, U32>,
    +next_words: List<&2, U32>, +next_rcon: U32, +next_i: U32,
    words_match: {List.append(&2, U32, words, [next_word(i, rcon, words)]) == next_words : List<&2, U32>},
    rcon_match: {Core.aes_rcon_kind(rcon, U32.is_eq(U32.mod(i, 8), 0)) == next_rcon : U32},
    index_match: {U32.add(i, 1) == next_i : U32}) ->
    {Core.aes_expand.go(1n+fuel, i, rcon, words) ==
     Core.aes_expand.go(fuel, next_i, next_rcon, next_words) : List<&2, U32>}:
    Equal.trans(List<&2, U32>, Core.aes_expand.go(1n+fuel, i, rcon, words),
        Core.aes_expand.go(fuel, U32.add(i, 1), next_rcon, next_words),
        Core.aes_expand.go(fuel, next_i, next_rcon, next_words),
        expand_step(fuel, i, rcon, words, next_words, next_rcon, words_match, rcon_match),
        Equal.cong(U32, List<&2, U32>, value => Core.aes_expand.go(fuel, value, next_rcon, next_words),
            U32.add(i, 1), next_i, index_match))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  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.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=aes_expand.go
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=aes_rcon_kind
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend&name=expand_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend&name=next_word