def suffix_41

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

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

715def suffix_41() ->
716    {Core.aes_expand.go(19n, 41, 32, words_41()) == words_60() : List<&2, U32>}:
717    Equal.trans(List<&2, U32>, Core.aes_expand.go(19n, 41, 32, words_41()),
718        Core.aes_expand.go(18n, 42, 32, words_42()), words_60(),
719        Trace.expand_step_number_at(18n, 19n, {==}, 41, 32, words_41(), words_42(), 32, 42,
720            next_words_41(), next_rcon_41(), {==}), suffix_42())