theorem :: ASYMPT_1:43

2 to_power 12 = 4096 by Lm26;