def suffix_14

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

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

904def suffix_14() ->
905    {Core.aes_expand.go(46n, 14, 2, words_14()) == words_60() : List<&2, U32>}:
906    Equal.trans(List<&2, U32>, Core.aes_expand.go(46n, 14, 2, words_14()),
907        Core.aes_expand.go(45n, 15, 2, words_15()), words_60(),
908        Trace.expand_step_number_at(45n, 46n, {==}, 14, 2, words_14(), words_15(), 2, 15,
909            next_words_14(), next_rcon_14(), {==}), suffix_15())