X_[s']を3ビット(以上)下位へシフトしてずれを消します。これをXX_[s']とおきます。
XX_[s']=x_0*(3/2)^[s']*(1+1/3x_0)…(1+1/3x_[s']-1)/k とします。
[logXX_[s']] - [logY_[s']] = 0 から始めて
[log(x_0*(3/2)^[s'])+log(1+1/3x_0)…(1+1/3x_[s']-1)/k] - [log(x_0*(3/2)^[s'])] = 0
切り上げを外して
-1 < log(1+1/3x_0)…(1+1/3x_[s']-1)/k < 1
logを外して
1/2 < (1+1/3x_0)…(1+1/3x_[s']-1)/k < 2
ここで、
x_0からx_s-1のうちで最小はx_0かつ、(1)より
(1+1/3x_0)…(1+1/3x_[s']-1) < ((1+1/3x_0)^3x_0)^([s']/3x_0) < (1+1/3x_0)^3x_0 < e
なので、
(1+1/3x_0)…(1+1/3x_[s']-1)/k < e/8 ≒ 0.339
となって1/2を下回って矛盾します。
よって、4-2-1ループを除いて、ループする数はない
と言えるのではないかと思うのですが、どうでしょうか。
