law next_ok
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/cipher.bend:322
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend as Cipher
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
322law next_ok:
323 for +nk: Nat
324 for +i: Nat
325 for +h: List<&2, T.Quad>
326 {I.next_word(nk, i, h) == S.next_word(nk, i, h) : T.Quad}