def suffix_34

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

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

764def suffix_34() ->
765    {Core.aes_expand.go(26n, 34, 16, words_34()) == words_60() : List<&2, U32>}:
766    Equal.trans(List<&2, U32>, Core.aes_expand.go(26n, 34, 16, words_34()),
767        Core.aes_expand.go(25n, 35, 16, words_35()), words_60(),
768        Trace.expand_step_number_at(25n, 26n, {==}, 34, 16, words_34(), words_35(), 16, 35,
769            next_words_34(), next_rcon_34(), {==}), suffix_35())