def suffix_47

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

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

673def suffix_47() ->
674    {Core.aes_expand.go(13n, 47, 32, words_47()) == words_60() : List<&2, U32>}:
675    Equal.trans(List<&2, U32>, Core.aes_expand.go(13n, 47, 32, words_47()),
676        Core.aes_expand.go(12n, 48, 32, words_48()), words_60(),
677        Trace.expand_step_number_at(12n, 13n, {==}, 47, 32, words_47(), words_48(), 32, 48,
678            next_words_47(), next_rcon_47(), {==}), suffix_48())