def suffix_53

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

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

631def suffix_53() ->
632    {Core.aes_expand.go(7n, 53, 64, words_53()) == words_60() : List<&2, U32>}:
633    Equal.trans(List<&2, U32>, Core.aes_expand.go(7n, 53, 64, words_53()),
634        Core.aes_expand.go(6n, 54, 64, words_54()), words_60(),
635        Trace.expand_step_number_at(6n, 7n, {==}, 53, 64, words_53(), words_54(), 64, 54,
636            next_words_53(), next_rcon_53(), {==}), suffix_54())