def suffix_39

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

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

729def suffix_39() ->
730    {Core.aes_expand.go(21n, 39, 16, words_39()) == words_60() : List<&2, U32>}:
731    Equal.trans(List<&2, U32>, Core.aes_expand.go(21n, 39, 16, words_39()),
732        Core.aes_expand.go(20n, 40, 16, words_40()), words_60(),
733        Trace.expand_step_number_at(20n, 21n, {==}, 39, 16, words_39(), words_40(), 16, 40,
734            next_words_39(), next_rcon_39(), {==}), suffix_40())