8.1　article の改良

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 チェッカーにとっては当然でも，人間が読んだときは理解できないような飛躍したものになってしまうこともあります．従って必ずしも行数を最少にまでする必要はなく，ほどほどに留めてもかまいません．