停止性の証明？

http://d.hatena.ne.jp/a-san/20090729#p1
VDMのmeasure関数の定義の仕方が少しずつわかってきました。

• measure関数の引数は、元の関数の引数と一致しなければならない。
• measure関数の戻り値は、nat、または natのタプルでなければならない。
• 再帰関数が以下の形のとき、

func(引数列) ==
	... 
	if (条件) func(次引数列) ...
        ...;

どのような引数列に対しても以下の式が成り立つようなmeasure関数を定義しなければならない。

条件 => id(引数列) > id(次引数列)