def suffix_55

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

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

617def suffix_55() ->
618    {Core.aes_expand.go(5n, 55, 64, words_55()) == words_60() : List<&2, U32>}:
619    Equal.trans(List<&2, U32>, Core.aes_expand.go(5n, 55, 64, words_55()),
620        Core.aes_expand.go(4n, 56, 64, words_56()), words_60(),
621        Trace.expand_step_number_at(4n, 5n, {==}, 55, 64, words_55(), words_56(), 64, 56,
622            next_words_55(), next_rcon_55(), {==}), suffix_56())