thus 2 to_power 12 = 2 to_power (6 + 6)
.= 64 * 64 by POWER:27, POWER:64
.= 4096 ; :: thesis: verum