Function lemma_u64_ilog2_to64 Copy item path

(0x1 as u64).ilog2() == 0,

(0x2 as u64).ilog2() == 1,

(0x4 as u64).ilog2() == 2,

(0x8 as u64).ilog2() == 3,

(0x10 as u64).ilog2() == 4,

(0x20 as u64).ilog2() == 5,

(0x40 as u64).ilog2() == 6,

(0x80 as u64).ilog2() == 7,

(0x100 as u64).ilog2() == 8,

(0x200 as u64).ilog2() == 9,

(0x400 as u64).ilog2() == 10,

(0x800 as u64).ilog2() == 11,

(0x1000 as u64).ilog2() == 12,

(0x2000 as u64).ilog2() == 13,

(0x4000 as u64).ilog2() == 14,

(0x8000 as u64).ilog2() == 15,

(0x10000 as u64).ilog2() == 16,

(0x20000 as u64).ilog2() == 17,

(0x40000 as u64).ilog2() == 18,

(0x80000 as u64).ilog2() == 19,

(0x100000 as u64).ilog2() == 20,

(0x200000 as u64).ilog2() == 21,

(0x400000 as u64).ilog2() == 22,

(0x800000 as u64).ilog2() == 23,

(0x1000000 as u64).ilog2() == 24,

(0x2000000 as u64).ilog2() == 25,

(0x4000000 as u64).ilog2() == 26,

(0x8000000 as u64).ilog2() == 27,

(0x10000000 as u64).ilog2() == 28,

(0x20000000 as u64).ilog2() == 29,

(0x40000000 as u64).ilog2() == 30,

(0x80000000 as u64).ilog2() == 31,

(0x100000000 as u64).ilog2() == 32,

(0x200000000 as u64).ilog2() == 33,

(0x400000000 as u64).ilog2() == 34,

(0x800000000 as u64).ilog2() == 35,

(0x1000000000 as u64).ilog2() == 36,

(0x2000000000 as u64).ilog2() == 37,

(0x4000000000 as u64).ilog2() == 38,

(0x8000000000 as u64).ilog2() == 39,

(0x10000000000 as u64).ilog2() == 40,

(0x20000000000 as u64).ilog2() == 41,

(0x40000000000 as u64).ilog2() == 42,

(0x80000000000 as u64).ilog2() == 43,

(0x100000000000 as u64).ilog2() == 44,

(0x200000000000 as u64).ilog2() == 45,

(0x400000000000 as u64).ilog2() == 46,

(0x800000000000 as u64).ilog2() == 47,

(0x1000000000000 as u64).ilog2() == 48,

(0x2000000000000 as u64).ilog2() == 49,

(0x4000000000000 as u64).ilog2() == 50,

(0x8000000000000 as u64).ilog2() == 51,

(0x10000000000000 as u64).ilog2() == 52,

(0x20000000000000 as u64).ilog2() == 53,

(0x40000000000000 as u64).ilog2() == 54,

(0x80000000000000 as u64).ilog2() == 55,

(0x100000000000000 as u64).ilog2() == 56,

(0x200000000000000 as u64).ilog2() == 57,

(0x400000000000000 as u64).ilog2() == 58,

(0x800000000000000 as u64).ilog2() == 59,

(0x1000000000000000 as u64).ilog2() == 60,

(0x2000000000000000 as u64).ilog2() == 61,

(0x4000000000000000 as u64).ilog2() == 62,

(0x8000000000000000 as u64).ilog2() == 63,