О длине вычислений арифметических программ

Рассматриваются программы над полным базисом, вычисляющие двоичные всюду определенные функции. Доказывается, что если функция, вычисляемая программой, обладают энтропией $H$, то имеется, по меньшей мере, одно вычисление программы длины $2_{dH}$ для некоторой положительной константы $d$.