def suffix_22

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

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

848def suffix_22() ->
849    {Core.aes_expand.go(38n, 22, 4, words_22()) == words_60() : List<&2, U32>}:
850    Equal.trans(List<&2, U32>, Core.aes_expand.go(38n, 22, 4, words_22()),
851        Core.aes_expand.go(37n, 23, 4, words_23()), words_60(),
852        Trace.expand_step_number_at(37n, 38n, {==}, 22, 4, words_22(), words_23(), 4, 23,
853            next_words_22(), next_rcon_22(), {==}), suffix_23())