新スレがないので、こちらで質問させてください。

PAを算術化する際に、
(1) 0は項である。
(2) tが項のとき、後続関数Sから得られたS(t)は、項である。
(3) tとuが項のとき、+と・から得られた+(t,u)および・(t,u)は、項である。


これらをゲーデル数化を用いて、算術の述語に変換したいのですが、3がいまいち分かりません。
(1)に対応する(1')は、
IsZero(x) : x=/0/
(2') : IsSuc(x) : ヨm,n≦x ［x=suc(n,<m>)かつm=/0/］
であってると思うのですが、、、。

ただし、/x/はPAの記号xのゲーデル数を表す。
succ(n,x)はxのn番目の後続数を得る関数とします。