Mizar/本体部/流れ

基本的に定義、定理、仮定、結果それぞれから、式を満たすということを積み重ねて証明を行う。 定義、定理、仮定、結果はラベル名で示す。ラベル名は同じファイル内ならば、ラベル名のみで良いが、 違うファイルの場合には、

式 by ファイル名:ラベル番号;

で表し、式の後にby～と記す。 一つのラベルの指す処理から、一つの結果を表す場合には

式 by ラベル名;

n個のラベルの指す処理から、一つの結果を表す場合には

式 by ラベル名1,ラベル名2,...,ラベル名n;

となる

※このラベルで表さなければならない為にMizarで行う証明は正確であるが、Wikipediaにあるように、 「同等の内容を持つ通常の数学論文に比べ、長さにおいて4倍程度になると評価された」 と言われ、実際には４倍以上手間がかかってしまう。

then consider X being 型 such that
 ...
 ラベルA:式
 ...
 thus theis by ラベルA;
end;

reserve X for Element of 型;
reserve X for 型;

型の再定義
reconsider X as 型

a = b .= c;
は以下と同等である
a = b; then b=c;