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):n個の変数を組み合わせてある変数を作る記号を定義する

func A 演算子 B
※definitionのendまでは、演算子をitで表す