def suffix_46

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

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

680def suffix_46() ->
681    {Core.aes_expand.go(14n, 46, 32, words_46()) == words_60() : List<&2, U32>}:
682    Equal.trans(List<&2, U32>, Core.aes_expand.go(14n, 46, 32, words_46()),
683        Core.aes_expand.go(13n, 47, 32, words_47()), words_60(),
684        Trace.expand_step_number_at(13n, 14n, {==}, 46, 32, words_46(), words_47(), 32, 47,
685            next_words_46(), next_rcon_46(), {==}), suffix_47())