8.1 Improvement of an Article

8.1.1 Improvement of the Main Section

First, we need to improve an article. To do this, we need the following commands.

      RELPREM       Checks unnecessary citations.
      CHKLAB         Checks unnecessary labels.
      INACC          Checks unnecessary lines.
      TRIVDEMO     Checks trivial demonstrations.
      RELINFER     Checks unnecessary lines.

    Such commands are provided. All these commands are used in the following way.

      RELPREM TEXT\EXAMPLE1.MIZ

    If we execute the following after carrying out each command, the error number will be written into an article.

      ERRFLAG TEXT\EXAMPLE1.MIZ

    RELPREM checks to see if irrelevant matters in reasoning are cited after "by". It also checks for the same thing for "then". If certain things are not needed for reasoning, an error will appear.
    CHKLAB later on checks for the labels that are not used after labeling.
    INACC later checks for the lines that are not used. If an error occurs from this checker and lines are erased, there may be excess citations and labels due to this; therefore, it needs to be checked again from the beginning.
    TRIVDEMO checks to see if there are trivial proofs. Trivial matters need to be removed. When being as follows,

     A=B
      proof
      To:A=C by T1;
          C=D by T2;
      hence thosis by To;
      end;

it meens that we can simplify them like the following. T1 and T2 are the labels used between the above-mentioned proof and end (external label of proof --- end).

     A=B by T1,T2;


Explanation of RELINFER;
RELINFER checks to see if two lines are summarize to one. For example, When an error (*605) is displayed as follows,

      A=B + C by T1;then
      D=E + (B + C) by T2;
                      *605

it meens that we can manage with the following one line.

　　　D=E + (B + C) by T1,T2;


When the error of the number *604 is as follows,

      S1: A=B + C by T1;
        ----------
        ----------
      D=E+ (B + C) by S1,T2
                     *604

it meens that we can write the following.

      S1: A=B + C by T1;
        ----------
        ----------
      D=E+(B + C) by T1.T2;

    If the line of a label S1 is not used for others, we can delete it, but if used, we cannot delete and cannot reduce a line. We can find out whether it is used or not, using CHKLAB once again, but when it is used, *604 may be disregarded because of troublesome to restore it. Anyway, it is necessary to use a series of check programs repeatedly. As a result, the number of lines may be decreased no less than several 10 percent. Because derivation of a line to a line is powerful, it is natural for Mizar checker, but it may become an oversimplification which cannot be understood when man reads. Therefore, it is not need to necessarily turn the number of lines even into the minimum, and we may stop moderately.