def suffix_37

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

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

743def suffix_37() ->
744    {Core.aes_expand.go(23n, 37, 16, words_37()) == words_60() : List<&2, U32>}:
745    Equal.trans(List<&2, U32>, Core.aes_expand.go(23n, 37, 16, words_37()),
746        Core.aes_expand.go(22n, 38, 16, words_38()), words_60(),
747        Trace.expand_step_number_at(22n, 23n, {==}, 37, 16, words_37(), words_38(), 16, 38,
748            next_words_37(), next_rcon_37(), {==}), suffix_38())