def suffix_33

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

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

771def suffix_33() ->
772    {Core.aes_expand.go(27n, 33, 16, words_33()) == words_60() : List<&2, U32>}:
773    Equal.trans(List<&2, U32>, Core.aes_expand.go(27n, 33, 16, words_33()),
774        Core.aes_expand.go(26n, 34, 16, words_34()), words_60(),
775        Trace.expand_step_number_at(26n, 27n, {==}, 33, 16, words_33(), words_34(), 16, 34,
776            next_words_33(), next_rcon_33(), {==}), suffix_34())