既にこれらのファイルに解答を書きこみはじめた人は,お手数ですが, 下記に従って,各自修正の上,解答してください. もし,まだ,これらのファイルをさわりはじめていない人は, あらためて ~kam/coq/CoreML.v や ~kam/coq/Eval.v をコピーしてください.
なお、これらは、稲川裕太君の指摘によるものです。どうもありがとう!
Theorem e266 : [] |- (_fix z ( x ) _if ((_left x) = %0) then %0 else _if ((_right x) = %0) then _left x else z @ ((_left x) + (%-1), (_right x) + (%-1))) @ (%5, %3) \in int. (* <-- it was "\in bool" in the older file *)
Theorem e267 : [w \in int * int -> int] |- (_fix z ( x ) _if ((_left x) = (_right x)) then _left x else _if ((_left x) > (_right x)) then z @ (w @ x, _right x) else z @ (w @ (_right x, _left x), _left x)) @ (%10, %3) \in int. (* <-- it was "\in bool" in the older file *)
2015/11/25追記: e267 において w の型が int -> int -> int になっていま したが、正しくは、int * int -> int です。 (これは、高橋君の指摘によるものです。どうもありがとう!)
Theorem ex524 : initE >> (_lambda (x) x + %30) @ (% 10 + % (-5)) --> (#35).