t のサイズについての帰納法で解く。
自由変数の定義(5.3.2)に場合分けして証明する。
-
t = xの場合自明
|FV(t)| = |{x}| = 1 = size(t). -
t = λx.t1の場合定義(5.3.2)でラムダ項の自由変数のsetが導ける
|FV(t)| = |FV(t1)\{x}|差集合の定義により
|FV(t1) \ {x}| ≦ |FV(t1)|仮定により
|FV(t)| ≦ size(t)なので|FV(t1)| ≦ size(t1)定義3.3.2よりsizeは小さくなることがわかる(*1)
size(t1) < size(t)よって
|FV(t)| ≦ size(t) -
t = t1 t2の場合t = λx.t1とほとんど同じです...|FV(t)| = |FV(t1) ∪ FV(t2)||FV(t1)| ∪ FV(t2)| ≦ |FV(t1)| + |FV(t2)||FV(t1)| + |FV(t2)| ≦ size(t1) + size(t2)size(t1) + size(t2) ≦ < size(t)よって
|FV(t)| ≦ size(t)
*1 : ラムダ項に包まれてるるのでsizeが減るって事なのだと思いますが、ラムダ項のsizeについて定義が与えられて無い気が...