>>561
strong normalization の証明。

v(0)=0
v(S(t))=v(t)+1
v(A(s,t))=v(s)+v(t)
v(M(s,t))=v(s)v(t)

と定めると、s→t のとき v(s)=v(t) となることが容易に証明できる。

l(0)=0
l(S(t))=l(t)
l(A(s,t))=l(s)+l(t)+v(t)+1
l(M(s,t))=(l(s)+2)v(t)+l(t)+v(s)v(t)(v(t)+1)/2+1

と定めると、s→t のとき l(s)<l(t) となることが証明できる。

たとえば、M(s,S(t)) のときを考えると、
l(M(s,S(t)))=(l(s)+2)(v(t)+1)+l(t)+v(s)(v(t)+1)(v(t)+2)/2+1
l(A(s,M(s,t)))=l(s)+(l(s)+2)v(t)+l(t)+v(s)v(t)(v(t)+1)/2+2
より、l(M(s,S(t)))-l(A(s,M(s,t)))=v(s)v(t)+1>0.

したがって、項 s に項書換え規則は高々 l(s) 回しか適用できない。