law other_idx

lawful-words@0.1.0.0 · proof_bytes.bend:931

import Base

931# Byte i of a word whose byte j (j != i) was set: bit k < 8 is beyond byte j.
932law other_idx:
933  for +i: Nat
934  for +j: Nat
935  for +k: Nat
936  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
937  for +hg: {Nat.is_le(Nat.mul(8n, j), Nat.add(Nat.mul(8n, i), k)) == True{} : Bool}
938  for +hne: {Nat.is_eq(i, j) == False{} : Bool}
939  {Nat.is_le(8n, Nat.sub(Nat.add(Nat.mul(8n, i), k), Nat.mul(8n, j))) == True{} : Bool}