law fin_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/subtle/word.bend:43

import Base

43# A comparison is EQ exactly when the tails compare EQ and the heads agree.
44law fin_eq:
45  for +ab: Bool
46  for +bb: Bool
47  for +t: Cmp
48  {Cmp.is_eq(Word.cmp.fin(ab, bb, t)) == Bool.and(Cmp.is_eq(t), Cmp.is_eq(Bool.cmp(ab, bb))) : Bool}