law cmp_bit

bend-kit-lemmas@0.1.1.0 · lemmas.bend:34

import Base

34law cmp_bit:
35  for a: Nat
36  for b: Nat
37  for x: Bool
38  for y: Bool
39  {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(bit(x, a), bit(y, b)) : Cmp}