law fin_k

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/final.bend:372

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

372law fin_k:
373  for +k: Nat
374  for +a: Nat
375  for +b: Nat
376  for +c: Nat
377  for +m: Nat
378  for +e1: {a == b : Nat}
379  for +e2: {b == C.low(k, c) : Nat}
380  for +e3: {m == c : Nat}
381  {a == C.low(k, m) : Nat}