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