def suffix_35

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

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

757def suffix_35() ->
758    {Core.aes_expand.go(25n, 35, 16, words_35()) == words_60() : List<&2, U32>}:
759    Equal.trans(List<&2, U32>, Core.aes_expand.go(25n, 35, 16, words_35()),
760        Core.aes_expand.go(24n, 36, 16, words_36()), words_60(),
761        Trace.expand_step_number_at(24n, 25n, {==}, 35, 16, words_35(), words_36(), 16, 36,
762            next_words_35(), next_rcon_35(), {==}), suffix_36())