Mizarの定義型   意味  使用法必要な証明 
 func  functor  機能を持たせるもの  演算子などexistence,uniqueness 
 cluster    群、まとまり  新しいデータタイプを作成 existence 
 mode    型  existence 
 pred  predicate  述語  因子、要素 
 defpred  (definition)+(predicate)  (定義)+(述語)  だからdefinitionの部分はいらない
 attr  attribute  属性  属性を持たせる 
---------------------------------------------------------------------------
 attr
  synonym(型);  ::同じ意味のシンボル
  antonym(型);  ::反対の意味のシンボル
---------------------------------------------------------------------------
あるmodeと別の属性(attribute)をもつmodeを組み合わせて新しいデータタイプの熟語を作り出せる
 cluster 型1 型2
 existence
 proof
  ～
 end;
---------------------------------------------------------------------------
演算子作成(functor):ｎ個の変数を組み合わせてある変数を作る記号を定義する
 func A 演算子 B
 ※definitionのendまでは、演算子をitで表す