law hkmax

lawful-fields@0.1.1.0 · proof_digits.bend:574

import Base

574# Every word is at most the largest one, BK(k) from k = 9 on.
575law hkmax:
576  for +n: U32
577  {Nat.is_le(U32.to_nat(n), U32.to_nat(U32.not(0))) == True{} : Bool}