pub proof fn lemma_pow2_is_pow2_to64()Expand description
ensures
is_pow2(0x1),is_pow2(0x2),is_pow2(0x4),is_pow2(0x8),is_pow2(0x10),is_pow2(0x20),is_pow2(0x40),is_pow2(0x80),is_pow2(0x100),is_pow2(0x200),is_pow2(0x400),is_pow2(0x800),is_pow2(0x1000),is_pow2(0x2000),is_pow2(0x4000),is_pow2(0x8000),is_pow2(0x10000),is_pow2(0x20000),is_pow2(0x40000),is_pow2(0x80000),is_pow2(0x100000),is_pow2(0x200000),is_pow2(0x400000),is_pow2(0x800000),is_pow2(0x1000000),is_pow2(0x2000000),is_pow2(0x4000000),is_pow2(0x8000000),is_pow2(0x10000000),is_pow2(0x20000000),is_pow2(0x40000000),is_pow2(0x80000000),is_pow2(0x100000000),is_pow2(0x200000000),is_pow2(0x400000000),is_pow2(0x800000000),is_pow2(0x1000000000),is_pow2(0x2000000000),is_pow2(0x4000000000),is_pow2(0x8000000000),is_pow2(0x10000000000),is_pow2(0x20000000000),is_pow2(0x40000000000),is_pow2(0x80000000000),is_pow2(0x100000000000),is_pow2(0x200000000000),is_pow2(0x400000000000),is_pow2(0x800000000000),is_pow2(0x1000000000000),is_pow2(0x2000000000000),is_pow2(0x4000000000000),is_pow2(0x8000000000000),is_pow2(0x10000000000000),is_pow2(0x20000000000000),is_pow2(0x40000000000000),is_pow2(0x80000000000000),is_pow2(0x100000000000000),is_pow2(0x200000000000000),is_pow2(0x400000000000000),is_pow2(0x800000000000000),is_pow2(0x1000000000000000),is_pow2(0x2000000000000000),is_pow2(0x4000000000000000),is_pow2(0x8000000000000000),is_pow2(0x10000000000000000),