練習問題 3.2.6

verb|~|を以下のように定義する． 



Zero   |~| n       = Zero
Succ m |~| Zero    = Zero
Succ m |~| Succ n  = Succ (m |~| n)


|~|

は整数上のどのような演算に対応しているか．

Nat

のすべての値，すなわち，有限値，擬値，無限値の

m

に対して

m |~| infinity = m

であることを証明せよ．





自然数|m|，|n|に対して小さい方を返す関数．

m

上の帰納法．




⊥ の場合
    ⊥ |~| infinity
=   { |~|の定義．場合の枯渇 }
    ⊥

Zero の場合
    Zero |~| ininity
=   { |~|の定義 }
    Zero

Succ m |~| infinity の場合
    Succ m |~| infinity
=   { infinity の定義 }
    Succ m |~| Succ infinity
=   { |~| の定義 }
    Succ (m |~| infinity)
=   { 帰納法の仮定 }
    Succ m