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