8.1.1 本体部の改良
まず，article の改良をしなければなりません．このためのコマンドとしては，
RELPREM 余計な引用をチェックする. CHKLAB 余計なラベルをチェックする. INACC 余計な行をチェックする.
TRIVDEMO トリビアルな証明をチェックする. RELINFER 余分な行をチェックする.
というコマンドが用意されています．いずれのコマンドも，
RELPREM TEXT\EXAMPLE1.MIZ
のように使い，それぞれのコマンドを実行した後に，
ERRFLAG TEXT\EXAMPLE1.MIZ
を実行すると，先ほどと同様に，articleにエラー番号が書きこまれます．
RELPREM は，by の後ろに推論に関係ないものが引用されているかをチェックします．
また，thenについても，それが必要であるかどうかチェックします．もし，それがな くても推論できるようなものがあると，エラーになります．
CHKLABは，ラベルをつけたが，あとで使ってないラベルをチェックします．
INACCは，あとで引用されてない行をチェックします．もし，このチェックでエラーが
でて，行を削除した場合，それにより余計な引用やラベルができるかもしれませんので，
また最初からチェックしなければいけません．
TRIVDEMOは，トリビアルな証明があるかどうかチェックします．これは，
A=B proof
To:A=C by T1;
C=D by T2;
hence thosis by To;
end;
となっているような場合に，
A=B by T1,T2;
と簡単化できることを示します． T1とT2は上のproofとendの間で使われているラ ベルです( proof --- endの外部のラベル)．
RELINFERの説明
RELINFERは 2 つの行を 1 つにまとめるかどうかをチェックします．例えば，
A=B + C by T1;then
D=E + (B + C) by T2;
*605
などとエラー(*605)が表示されたときは，
D=E + (B + C) by T1,T2;
とすると，一行で済ませられることを示します．
*604 という番号のエラーは，
S1: A=B + C by T1;
--- ---
D=E+ (B + C) by S1,T2
*604
となるとき,
S1: A=B + C by T1;
--- ---
D=E+(B + C) by T1.T2;
と書けるということを示します．もしラベルS1の行が他に使われていなければ，それ を削除することができますが，使われていれば，削除できず，行を減らすことはできま せん．使われているかどうかは，もう一度 CHKLAB を使えばわかるのですが，使われ ている時，また元へ戻すのはやっかいなので，*604
は無視してもよいでしょう．いず
れにしても，一連のチェックプログラムを何度も用いる必要があります．その結果何割 も行数が減ってしまうこともあります．行から行の導出が強力で MIZAR チェッカーに とっては当然でも，人間が読んだときは理解できないような飛躍したものになってしま うこともあります．従って必ずしも行数を最少にまでする必要はなく，ほどほどに留め てもかまいません．8.1.2 環境部のチェック
そのほか環境部のチェックがあります．このためのコマンドとしては，
IRRVOC 不要なvocabularyをチェックする．
IRRTHS 不要なtheoremsをチェックする．
があります．使い方は本体部のチェックのコマンドと同様です．NOTATIONや
CONSTRUSTORSに関しては，良い方法がないので，NOTATIONやCONSTRUSTORSは最 初からたくさん使わないで，なるべく最低限のもの，最初は