def suffix_29

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

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

799def suffix_29() ->
800    {Core.aes_expand.go(31n, 29, 8, words_29()) == words_60() : List<&2, U32>}:
801    Equal.trans(List<&2, U32>, Core.aes_expand.go(31n, 29, 8, words_29()),
802        Core.aes_expand.go(30n, 30, 8, words_30()), words_60(),
803        Trace.expand_step_number_at(30n, 31n, {==}, 29, 8, words_29(), words_30(), 8, 30,
804            next_words_29(), next_rcon_29(), {==}), suffix_30())