発表前。

研究所の発表会が近づいてきた。
しゃべる構成は全然決めていないけど、
スライドだけはできた。

明日の仕事にしよう。
今日は、yaccとlex。
変数を宣言する方法がさっぱりわからない。
変数ってどうやって参照するんだろうか。

ネットで調べてもさっぱりわからない。
はてなで質問しようかな。

オライリーの本を買えばいいんだろうが、買いに行ってる暇はなし。

lex&yaccプログラミング (NUTSHELL HANDBOOKS)

というわけで、Mizarのページが直ったか、試してみる。
今度は、別のページに飛ばされた・・。

Ztonさんのおかげで、何とかMizarのエラーが出されずにすんだ。
というわけで、Mizarの講義のPDFファイルを閲覧しようとするが、
やっぱりリクエストタイムアウト。で、Googleのキャッシュで無理矢理見て、勉強。

第二回まで勉強して、意味がさっぱりわからなかったが、とりあえず終わった。
分かったこと

for	任意の. holdと一緒につかう
begin Nat	Nat型変数
holds	holds以降が実体.

したがって、
for n being Nat holds 2 divides n*(n-1)
は、
ある任意の数nに対して、2は、n(n-1)を割り切る。
という命題となるらしい。

これの証明が、proof;〜end;らしい。
XX:で、ラベルとなる。だから
AAA:for n being Nat st P[n] holds P[n+1]
というのは、:以降をAAAとする。といいたいわけかな。
stの説明がなかったけど、多分 such thatの略でしょう。

defpred	定義する。 defineと、〜〜する。のpredの合体
let n be Nat	nをNat型の任意の変数としよう
assume 〜	P[n]が成り立つと仮定する
hence	ゆえに。 thereforeじゃないの?

やっぱり全然わからなかった。
どうも、たとえ入学しても卒業できない気がする・・。