def suffix_51

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

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

645def suffix_51() ->
646    {Core.aes_expand.go(9n, 51, 64, words_51()) == words_60() : List<&2, U32>}:
647    Equal.trans(List<&2, U32>, Core.aes_expand.go(9n, 51, 64, words_51()),
648        Core.aes_expand.go(8n, 52, 64, words_52()), words_60(),
649        Trace.expand_step_number_at(8n, 9n, {==}, 51, 64, words_51(), words_52(), 64, 52,
650            next_words_51(), next_rcon_51(), {==}), suffix_52())