一般たらいまわし関数補足
上の方針で何が嬉しいかというと、tの値が実際になんになるかはあまり真面目に考えなくてもよいということです。値がどうなるかを真面目に考え始めると、後半の8ページが必要になるわけですよ。ぱらぱらめくって"case"を目grepすればわかるとおり、場合分け山積み。それも必死になって削った上でなんですよ。おまけにここの部分は関数が停止することが証明された後なので、「帰納法がまだここまで来てないからダメ」とかいう事態は無視できているんです。ちょっとした工夫で、複雑に見えていたものがすっきりしてくるというのはやはり数学の醍醐味で、つーか数学に知恵を絞る部分が無いってやっぱりすげー違うと思うんですがどうでしょう?*1