Exercise 3.5.17の解答（原著499頁目、日本語版394頁目）の誤り

[Eijiro Sumii]

Exercise 3.5.17の解答（原著499頁目）のProposition A.9に

Proof: By induction on the number of steps of small-step evaluation in the given derivation of t -->* v.

とあるのですが、t = succ t1 の場合、tの評価とt1の評価が同じステップ数になるので、帰納法がうまくいきません。
ちょっと頑張ってみても

A.8と同様のLemmaにより v = succ nv1 かつ t1 --> t1' -->* nv1
よって帰納法の仮定より t1' \Downarrow nv1 だからB-Succより succ t1' ==> succ nv1

ぐらいまでは言えるのですが、そこから succ t1 ==> succ nv1 につながりません（別の補題が必要になります）。
日本語版394頁目にも同じ誤りがあります。

正しい証明は、t の構造に関する帰納法を用いれば容易です（他の証明も考えられますが）。

これまでのエラータにもなかったので、住井が管理している英語版のエラータ
https://www.dropbox.com/s/9dkguftad519x0s/errata-trans.txt
に追加しました。

[Eijiro Sumii]

追記ですみません、==> は \Downarrow のことです。統一し損なったので念のため。