コンテンツにスキップ

Mizar/本体部

出典: フリー教科書『ウィキブックス(Wikibooks)』


begin

--------------------------------------
共通変数定義
reserve X, Y, Z, x, y, z for set;
--------------------------------------
定義をする
definition
定義式;
existence 証明式 proof ~ end;
uniqueness 証明式 proof ~ end;
end;
--------------------------------------
定理の証明を行う場合に付ける(absファイルで使えるようにするために必要)
theorem
証明したい式
proof
変数定義
証明
結果
end;
--------------------------------------