def suffix_11

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

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

925def suffix_11() ->
926    {Core.aes_expand.go(49n, 11, 2, words_11()) == words_60() : List<&2, U32>}:
927    Equal.trans(List<&2, U32>, Core.aes_expand.go(49n, 11, 2, words_11()),
928        Core.aes_expand.go(48n, 12, 2, words_12()), words_60(),
929        Trace.expand_step_number_at(48n, 49n, {==}, 11, 2, words_11(), words_12(), 2, 12,
930            next_words_11(), next_rcon_11(), {==}), suffix_12())