Mizar/本体部/定義式/変数定義
(Mizar/変数定義 から転送)
証明したい式で for x ... を使った場合には proof let x; let x be mode型; ... for x st ~を使った場合には proof let x be set such that ~ ...
証明したい式で ex y ...を使った場合には proof take y; ...
定義定理などで外部ファイルに ex A と書かれている場合には consider a ~ by 外部ファイル名:番号;
証明したい式で x being 型 を使った場合には let x be 型; C言語で表すとすると、beingはポインタ設定、beは値を定義している。 即ち、 int *x; int a; x=&a; とすることで、*xに値を代入できるようになるのと同様である。
変数を使う場合には、$変数名 とする。 defpred P[Nat] means $1 $1は変数、 $~。~は英数字とする。 reserve a for set; $a
Aを仮定する assume A;
A then B such that ... thus 証明済み式; end;
新しい変数を導入する場合には
set r;
いくつかの変数の属性を持った、新しい変数を作る
cluster