def suffix_13

qasim-bend-kit@0.1.0.2 · proof/AES_NistKeyScheduleProof.bend:911

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

911def suffix_13() ->
912    {Core.aes_expand.go(47n, 13, 2, words_13()) == words_60() : List<&2, U32>}:
913    Equal.trans(List<&2, U32>, Core.aes_expand.go(47n, 13, 2, words_13()),
914        Core.aes_expand.go(46n, 14, 2, words_14()), words_60(),
915        Trace.expand_step_number_at(46n, 47n, {==}, 13, 2, words_13(), words_14(), 2, 14,
916            next_words_13(), next_rcon_13(), {==}), suffix_14())