def suffix_9

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

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

939def suffix_9() ->
940    {Core.aes_expand.go(51n, 9, 2, words_9()) == words_60() : List<&2, U32>}:
941    Equal.trans(List<&2, U32>, Core.aes_expand.go(51n, 9, 2, words_9()),
942        Core.aes_expand.go(50n, 10, 2, words_10()), words_60(),
943        Trace.expand_step_number_at(50n, 51n, {==}, 9, 2, words_9(), words_10(), 2, 10,
944            next_words_9(), next_rcon_9(), {==}), suffix_10())