The largest 60-bit natural, all ones.
Theorem: logbitp-of-60-bit-mask
(defthm logbitp-of-60-bit-mask (implies (natp i) (equal (logbitp i *60-bit-mask*) (< i 60))))
