def suffix_21

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

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

855def suffix_21() ->
856    {Core.aes_expand.go(39n, 21, 4, words_21()) == words_60() : List<&2, U32>}:
857    Equal.trans(List<&2, U32>, Core.aes_expand.go(39n, 21, 4, words_21()),
858        Core.aes_expand.go(38n, 22, 4, words_22()), words_60(),
859        Trace.expand_step_number_at(38n, 39n, {==}, 21, 4, words_21(), words_22(), 4, 22,
860            next_words_21(), next_rcon_21(), {==}), suffix_22())