law gtop

lawful-bytes@0.1.1.0 · proof_fast_find.bend:410

import Base

410# With the bound m abstract (m stands for 2^32).
411law gtop:
412  for +x: Nat
413  for +tt: Nat
414  for +m: Nat
415  for +hx: {x == Nat.sub(Nat.sub(m, 1n), U32.to_nat(0)) : Nat}
416  for +ht: {Nat.is_lt(tt, m) == True{} : Bool}
417  {Nat.is_lt(x, tt) == False{} : Bool}