Оценка кратности выходного символа в обратимом автомате

Доказано, что максимальное количество $\rho$ повторений некоторого выходного символа в таблице выходов автомата с $n$ состояниями и $m$ входными символами, при котором автомат обратим, вычисляется по формуле $\rho=[(n+1)/2][(n+2)/2]$, если $[(n+2)/2]\leq m$, и $\rho=(n-m+1)m$ в противном случае.