A正規化漬け

(let1 a 3 (+ a (+ 1 2))

はA正規化しても変化しないという理解であっているだろうか?それとも (+ a (+ 1 2)) の部分を正規化するのが正しい?
考えすぎて理解が怪しくなってきた。誰かと議論しながら考えたいと強く思う。
が、くじけないよ。気分転換しよう。

追記

上のlet1 は Figure 7 のEvaluation Contexts のどれにもあてはまらないから。これ以上変換は進まない。と解釈している。
しかしコードを見ると (+ a (+ 1 2)) の中も正規化しているように見える。
どちらが論文的に正しいのか分からなくて途方に暮れる。