   To get  into  the  Edit  window  press Enter when  
positioned on the Edit  command in the Main Menu, or  
E when  anywhere  else in that  menu, or  AltE  from  
elsewhere.                                            
                                                      
   In this  window you  see, except  for your  text,  
several  information lines. The top  line is  called  
the Main_menu  line, in  the  bottom line the Hotkey
menu is  listed.  Below the  main menu is the Status 
line, with info on current text settings.             
                                                      
                                                      
                                                      
                                                      
   This Editor is very similar to the Turbo Pascal's  
Editor or SideKick's Notepad,  though there are some  
differences.  To learn them  and for people that are  
unfamiliar with editors listed above, here is         
                                                      
                                                      
              Editing Commands Menu                   
                                                      
        Blocks                Miscellaneous         
        Find\replace          Movement              
        Insert\delete                                
                                                      
                                                      
                                                      
   The  main menu lists the commands you may want to  
use.  You  invoke  one  of  those  commands  just by  
pressing  Alt  and  the  highlighted  letter  of the  
command.  You  can  get to  the  Main  Menu  just by  
pressing the F10 key. Then you invoke the command by  
pressing one of the letters, or by moving the cursor  
onto the  command  and pressing  ENTER. Here are the  
commands :                                            
                                                      
                                                      
              Edit            Options               
              File            Mizar                 
                                                      
                                                      
                   Hotkey List                        
                                                      
 F1  - Help               AltF1  - Last help          
 F2  - Save file          AltF3  - Pick file          
 F3  - Load file          AltF9  - LST file           
 F4  - New mask           AltF10 - Vignette            
 F7  - Previous error     AltX   - Quit               
 F8  - Next error                                     
 F9  - Mizar              CtrlF1 - Mizar word help    
 F10 - Main menu                                      
                                                      
                                                      
                                                      
                                                      
   The status line gives you the following info :     
                                                      
1. Current position of the cursor :                   
    Line n - the cursor is in line n,                 
    Col m  - the cursor in the column m.              
2. Indicates  whether you are in Tab, Insert, and/or  
   Indent mode.                                       
3. Name of the file in the editor :                   
    Drive : \ Filename Extension                      
                                                      
                                                      
                                                      
                                                      
                                                      
                 BLOCK  COMMANDS                      
                                                      
  ^KB  -  Mark the beginning of a block.              
  ^KK  -  Mark the end of a block.                    
  ^KC  -  Copy block.                                 
  ^KV  -  Move block.                                 
  ^KY  -  Delete block.                               
  ^KH  -  Hide/display block.                         
  ^KL  -  Mark line.                                  
  ^KR  -  Read block from file.                       
  ^KW  -  Write block to file.                        
  ^KA  -  Append block to file.                       
  ^QB  -  Move to the beginning of a block.           
  ^QK  -  Move to the end of a block.                 
              FIND & REPLACE COMMANDS                 
                                                      
  ^QF  -  Find given string.                          
  ^QA  -  Find and replace given string.              
  ^L   -  Repeat last search or replace command.      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                     OPTIONS                          
            for Find\Replace Commands                 
                                                      
  B - Search backwards.                               
  G - Global search from the beginning of file.       
  N - No confirmation while replacing.                
  U - Ignore upper/lower case.                        
  W - Search  whole  words  only. Words  consist  of  
      letters (upper and lower case) and digits.      
                                                      
                                                      
                                                      
                                                      
                                                      
             INSERT & DELETE COMMANDS                 
                                                      
  Ins - Insert\overwrite mode toggle.                 
  ^KC - Insert block.                                 
  Del - Delete character under cursor.                
  <-  - Delete character before cursor.               
  ^T  - Delete word right.                            
  ^F  - Delete word left.                             
  ^QY - Delete to the end of line.                    
  ^QG - Delete to the beginning of line.              
  ^<- - Delete line.                                  
  ^KY - Delete block.                                 
                                                      
                                                      
             CURSOR MOVEMENT COMMANDS                 
                                                      
   @   - One character right.                         
      - One character left.                          
      - One line up.                                 
      - One line down.                               
  ^@   - One word right.                              
  ^   - One word left.                               
   + SCROLL - Scroll one line up.                    
   + SCROLL - One line down.                         
  @ + SCROLL - One column left.                       
   + SCROLL - One column right.                      
                                                      
                                                      
             CURSOR MOVEMENT COMMANDS                 
                    extended                          
                                                      
   Home - Beginning of line.                          
   End  - End of line.                                
   PgUp - One page up.                                
   PgDn - One page down.                              
  ^Home - Top of window.                              
  ^End  - Bottom of window.                           
  ^PgUp - Top of file.                                
  ^PgDn - Bottom of file.                             
  ^QB   - Beginning of block.                         
  ^QK   - End of block.                               
                                                      
                  MISCELLANEOUS                       
                                                      
  ^OT   - Tab mode toggle.                            
  Tab   - Tab.                                        
  ^OI   - Autoindent on/off.                          
  ^U    - Abort an operation.                         
  F2    - Save a file.                                
  F3    - Load a file.                                
  F10   - Invoke the main menu.                       
                                                      
                                                      
                                                      
                                                      
                                                      
   To invoke Mizar press M when in the main menu, or  
ENTER when positioned on the Mizar  command, or AltM  
or F9  from anywhere. By  pressing the  AltF9 hotkey  
an LST file will be output to the disk.               
                                                      
   Help on the following topics is available:         
                                                      
             Errors_reported_by_Mizar                
                        and                           
          Reserved_words_&_signs_in_Mizar .          
                                                      
                                                      
                                                      
                                                      
               MIZAR RESERVED WORDS                   
                                                      
            Reserved_signs   ex                     
            and              for                    
            assume           given                  
            be               hence                  
            begin            holds                  
            being            iff                    
            by               implies                
            consider         let                    
            contradiction    not                    
            end              now                    
            environ          or                     
                                                      
               MIZAR RESERVED WORDS                   
                    continued                         
                                                      
            proof            that                   
            reserve          then                   
            st               thesis                 
            such             thus                   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
& - Conjunction sign between statements.              
                                                      
Syntax:                                               
 sentence & sentence { & sentence }                  
                                                      
Examples:                                             
 p[] & q[];                                           
 p[] & q[] & r[];                                     
 for a holds p[a] & q[a];                             
                                                      
See also :                                            
 iff         not                                    
 implies     or                                     
                                                      
and - Used  for conclusions  of assumptions when you  
      want  to  have   different  labels  for  every  
      statement (part of an assumption).              
                                                      
Examples:                                             
 assume that a: à[] and b: á[];                       
 given x such that a: à[x] and b: not á[x];           
 consider y such that à = á and a: ä[á,à];            
 let x be ANY such that a: à = à and ä[à];            
                                                      
                                                      
                                                      
                                                      
                                                      
ex - Existential quantifier.                          
                                                      
Syntax:                                               
 ex <list> st statement ";"                           
                                                      
Examples:                                             
 ex à,á st à = á & ä[à,á];                            
 ex à,á being ANY st ä[à,á];                          
                                                      
See also:                                             
 for                                                 
                                                      
                                                      
                                                      
for - This word has two meanings.                     
                                                      
1) General quantifier.                                
                                                      
Syntax:                                               
 for <variable_list>                                  
     1. st statement holds statement ";"              
     2. holds statement ";"                           
                                                      
 Examples:                                            
   for A being Point holds à[A];                      
   for A st P[A] holds Q[A] iff R[A];                 
                                                      
See also: ex                                         
2) "for" is used in  the structure  used for  global  
   reservation of variables.                          
                                                      
Syntax:                                               
 reserve <Variable_list> for <type_identifier> ";"    
                                                      
Example:                                              
 reserve A,B for POINT;                               
                                                      
See also:                                             
 reserve                                             
                                                      
                                                      
                                                      
assume - Assumption                                   
                                                      
Syntax:                                               
 assume [that] [label ":"] statement                  
         { and [label ":"] statement } ";"            
                                                      
Examples:                                             
  assume p[];                                         
  assume that p[];                                    
  assume A: p[] & q[];                                
  assume that A: p[] and q[];                         
  assume that A: p[] and B: q[];                      
                                                      
See also: given                                      
given - Introduction  of  global  constants (when in  
        then environment), or existential assumption  
        (when in proof,  instead  of "assume", "then  
        consider").                                   
                                                      
Syntax:                                               
 given <qualified_variables> such that                
  [label ":"] <Conditions> ";"                        
                                                      
Examples:                                             
 given A being POINT such that A: ON[A,L];            
 given A,B such that P[A] and LABEL: ON[A,B];         
                                                      
                                                      
Note: While  proving  a  theorem  you  may  use  the  
      construction  above  which is the shorter form  
      for:                                            
                                                      
 assume ex A being POINT st ON[A,L];                  
 then consider A Being POINT such that A: ON[A,L];    
                                                      
See also: assume                                     
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
be - Used  for the  introduction  of the  type  of a  
     variable when it is unknown.                     
                                                      
Note: "being" is equivalent "be".                     
                                                      
Examples:                                             
 consider A be Any ...                                
 let B be Anything ...                                
 given C be Something ...                             
 for D be Sth holds ...                               
 ex E be Sth st ...                                   
                                                      
                                                      
                                                      
hence - linking  for  conclusion.  You  cannot  link  
        words  like  "now",  "proof"  and   "begin".  
        Linking  to statements that have an "and" in  
        them is also forbidden.                       
                                                      
Syntax:                                               
 hence <statement> {by <identifier_list>} ";"         
                                                      
Example:                                              
 hence thesis by A_label;                             
                                                      
See also:                                             
 by          then                                   
 thus                                                
begin - The   beginning  of  the  text  proper.  The  
        environment  must end with the word "begin".  
        From now on you can prove your theorems.      
                                                      
See also:                                             
 environ                                             
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
holds - Used only  under the general  quantifier. It  
        specifies  what  conditions  are met  by the  
        quantified   variables  (conditions  on  the  
        variable  may be  introduced  before "holds"  
        using the "st" construction).                 
                                                      
Note: Two sentences below have the same meaning.      
                                                      
 for A holds p[A] implies q[A];                       
 for A st p[A] holds q[A];                            
                                                      
See also:                                             
 for                                                 
 st                                                  
being - Used  for the introduction of  the type of a  
        variable when it is unknown.                  
                                                      
Note: "being" is equivalent "be".                     
                                                      
Examples:                                             
 consider A being Any ...                             
 let B being Anything ...                             
 given C being Something ...                          
 for D being Sth holds ...                            
 ex E being Sth st ...                                
                                                      
                                                      
                                                      
iff - The equivalence of statements.                  
                                                      
Syntax:                                               
 <sentence> iff <sentence>                            
                                                      
Example:                                              
 p[] iff q[];                                         
 (p[] iff q[]) implies (q[] iff p[]);                 
                                                      
See also:                                             
 implies                                             
 not                                                 
 or                                                  
 &                                                   
Warning: The associative notation is not allowed for  
         "iff", i.e.                                  
                    p[] iff p[] iff p[]               
         is incorrect syntactically. Here follow the  
         correct notations:                           
                    (p[] iff p[]) iff p[]             
                             or                       
                    p[] iff (p[] iff p[]).            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
by - Simple  justification. It should be followed by  
     references  to labels of  previously introduced  
     propositions from which the current  one can be  
     derived.                                         
                                                      
Syntax:                                               
 [then|hence] <Statement> by <Identifier_list> ";"    
                                                      
Example:                                              
 hence contradiction by A_label;                      
                                                      
See also:                                             
 hence                                               
 then                                                
implies - Implication between statements.             
                                                      
Syntax:                                               
 <sentence> implies <sentence>                        
                                                      
Examples:                                             
 p[] implies q[];                                     
 not p[] & p[] implies p[];                           
                                                      
See also:                                             
 iff                                                 
 not                                                 
 or                                                  
 &                                                   
Warning: The associative notation is not allowed for  
         "implies", i.e.                              
                 p[] implies p[] implies p[]          
         is incorrect syntactically. Here follow the  
         correct notations:                           
                (p[] implies p[]) implies p[]         
                              or                      
                p[] implies (p[] implies p[]).        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
consider - Used for introduction of local constants.  
                                                      
Syntax:                                               
 consider <qualified_list> such that <conditions>";"  
                                                      
Example:                                              
 consider A,B being POINT such that A: A[A,B];        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
let - Used for  generalization of  variables  (while  
      proving general sentences).                     
                                                      
Syntax:                                               
 let <var_list> (be|being) <var_identifier>           
  { "," <var_list> (be|being) <var_identifier>}       
  {<conditions>} ";"                                  
                                                      
Examples:                                             
 let A be POINT;                                      
 let A,B be POINT such that A: P[A,B];                
                                                      
See also:                                             
 be    being                                        
contradiction - the sentence  which is always false.  
                Mostly used as a conclusion when you  
                try    to    prove   something    by  
                contradiction.                        
                                                      
Example:                                              
 thus contradiction by A_label1,A_Label2;             
 consider A such that not contradiction;              
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
not - Negation of a statement.                        
                                                      
Syntax:                                               
 not <sentence>                                       
                                                      
Example:                                              
 not p[];                                             
 not (p[] or q[]) iff not p[] & not q[];              
                                                      
See also:                                             
 iff                                                 
 implies                                             
 or                                                  
 &                                                   
end - Indicates  that  proof  opened by  "proof"  or  
      "now" is closed. This word  must followed by a  
      semicolon.                                      
                                                      
See also:                                             
 proof                                               
 now                                                 
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
now - The  beginning  of a  diffuse  statement.  The  
      Mizar processor  will build a  theorem that is  
      proved from a given proof skeleton.  The proof  
      of this statement must be ended with "end".     
                                                      
Example:                                              
 now                                                  
   let A be POINT;                                    
   assume p[A];                                       
   thus q[A];                                         
 end;                                                 
                                                      
The system will construct the following sentence:     
     for A being POINT st p[A] holds q[A];            
See also:                                             
 end                                                 
 proof                                               
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
environ - The  beginning  of  the  environment.  You  
          cannot  omit this word in your  text, even  
          when  the environment  is empty. This word  
          may occur  only  at the beginning  of  the  
          text (excluding comments).                  
                                                      
See also:                                             
 begin                                               
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
or - Disjunction between statements.                  
                                                      
Syntax:                                               
 <sentence> or <sentence> {or <sentence>}             
                                                      
Example:                                              
 p[] or q[] implies r[];                              
 p[] or q[] or r[];                                   
                                                      
See also:                                             
 iff                                                 
 implies                                             
 not                                                 
 &                                                   
proof - The beginning  of  the proof. Must have  the  
        corresponding "end".                          
                                                      
Example:                                              
 for A holds P[A]                                     
  proof                                               
   let A be ANY;                                      
   thus thesis by A_label;                            
  end;                                                
                                                      
See also:                                             
 end                                                 
 now                                                 
                                                      
that - Begins the conditions group.                   
                                                      
Syntax:                                               
 that [label ":"] formula {and [label ":"] formula}   
                                                      
Used in constructions with:                           
 assume                                              
 consider                                            
 given                                               
 let                                                 
                                                      
See also:                                             
 such                                                
                                                      
reserve - Global  reservation of  variables  allowed  
          only in the environment.                    
                                                      
Syntax:                                               
 reserve <Variable_list> for <Type_identifier> ";"    
                                                      
Example:                                              
 reserve A,B for POINT;                               
                                                      
See also:                                             
 for                                                 
                                                      
                                                      
                                                      
then - Linking  (but not for  conclusions). You  can  
       link only to  statements in which there is no  
       "and", and  of course  you cannot  link words  
       like "now" or "proof".                         
                                                      
Syntax:                                               
 then <statement> {by <Identifier_list>} ";"          
                                                      
Example:                                              
 then p[A] by A_label;                                
 then p[A];                                           
                                                      
See also:                                             
 by    hence                                        
st - It  means  ® such that ¯ and  is  used  under a  
     quantifier.                                      
                                                      
Examples:                                             
 ex A st p[A];                                        
 for A,B st p[A] & p[B] holds q[A,B];                 
                                                      
Note: "st" and "such that" have different  meanings.  
      The  first is  used  only  under a quantifier,  
      while the other in the conditions group.        
                                                      
                                                      
                                                      
                                                      
thesis - This word means  what is left to be proved.  
         May  not be  used  under  a  quantifier  or  
         outside of a proof.                          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Example:                                              
 for A holds p[A] iff O[]                             
  proof                                               
     ::  thesis: for A holds p[A] iff O[]             
   let A be Something;                                
     ::  thesis: p[A] iff O[]                         
   thus p[A] implies O[];                             
     ::  thesis: O[] implies p[A]                     
   assume O[];                                        
     ::  thesis: p[A]                                 
   O[];                                               
     ::  thesis: not contradiction                    
 end;                                                 
                                                      
such - This word must be placed before the condition  
       group, which follows                           
                                                      
 consider                                            
 given                                               
 let                                                 
                                                      
Example:                                              
 let A be Any such that 1: P[A];                      
                                                      
See also:                                             
 that                                                
                                                      
                                                      
thus - Conclusion.                                    
                                                      
Syntax:                                               
 thus <Statement> (by|proof <Proof> end|) ";"         
                                                      
Examples:                                             
 thus p[a];                                           
 thus p[a] by A_label;                                
 thus p[a] proof ... end;                             
                                                      
See also:                                             
 hence                                               
                                                      
                                                      
                RESERVED SIGNS.                       
                                                      
  &                                                  
  ,                                                  
  :                                                  
  ;                                                  
  [_..._]                                            
  (_..._)                                            
  =                                                  
  <>                                                 
  ::                                                 
                                                      
                                                      
                                                      
, - Separator between elements of identifier lists.   
                                                      
Examples:                                             
 reserve à,á,â,ã for Set;                             
 P[à,á];                                              
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
: - Follows the label identifier.                     
                                                      
Example:                                              
 Label: for à holds á[à];                             
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
; - Ends all  statements in Mizar. The use of ";" is  
    forbidden after  "proof", "now", "environ",  and  
    "begin".  It is necessary after "end" and before  
    "end"  and  "begin".  Do  not  place  it  before  
    "proof" - the  system will  report  many errors,  
    especially when the proof is completed.           
                                                      
Example:                                              
 thus thesis by Ax1;                                  
                                                      
                                                      
                                                      
                                                      
                                                      
[] - Used for  writing  predicates. Before the  left  
     bracket there must be the predicate identifier.  
     The right  bracket ends the  predicate. Between  
     them there must be a  variable list  (it may be  
     empty).                                          
                                                      
Examples:                                             
 for à holds á[à];                                    
 for à holds á[à,å,æ];                                
 á[] by Ax2;                                          
                                                      
                                                      
                                                      
                                                      
() - Parentheses are  used to force higher  priority  
     for logical operators in case their priority is  
     lower. The highest priority has "not", then "&"  
     followed  by "or". The priority of "iff" equals  
     to the  priority  of "implies"  and is lower of  
     those  mentioned earlier.  The lowest  priority  
     have the quantifiers "for" and "ex".             
                                                      
Example:                                              
 not (p[A] or q[A]);                                  
 (p[] implies q[]) iff r[];                           
 (for A holds p[a]) & q[];                            
                                                      
                                                      
= - Equality  of  variables.  Only  variables can be  
    compared.                                         
                                                      
Example:                                              
 for à,á holds à = á;                                 
                                                      
See also:                                             
 <>                                                  
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
<> - Inequality of variables. Only  variables can be  
     compared.                                        
                                                      
Example:                                              
 for à,á holds à <> á;                                
                                                      
See also:                                             
 =                                                   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
:: - This  sign is  used  to write comments in Mizar  
     texts. The  comment starts  with this  sign and  
     ends with the end of the line.  This comment is  
     of course ignored by the Mizar processor.        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
          Errors reported by Mizar MSE.               
                                                      
   Below you have the list of error messages divided  
into the following groups:                            
                                                      
 CHECKER                                             
 REASONER                                            
 SCANNER                                             
 Identification                                      
 Global_Recovery                                     
 Syntax                                              
 Overflow                                            
                                                      
                                                      
           Errors reported by CHECKER.                
                                                      
   CHECKER  is   the  unit   that   checks   logical  
correctness of reasoning.                             
                                                      
#4  This inference not accepted by the CHECKER.      
#10 Too many basic sentences.                        
#12 The prefix of a universal sentence is too long.  
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
          Errors reported by REASONER.                
                                                      
#41 Forbidden assumption or conclusion.              
#42 The assumption or conclusion is too long.        
#43 VERUM may not be obtained by generalization.     
#44 Conjunction    may    not    be    obtained   by 
    generalization.                                   
#45 Generalization  is  allowed  only if thesis is a 
    universal sentence.                               
#46 Types of the  generalized variable and the bound 
    variable differ.                                  
#47 There is still something to prove.               
#48 A local constant in the proof skeleton.          
                                                      
            Errors reported by SCANNER.               
                                                      
#130 Forbidden character in the text.                
#132 "<" may only be used to represent an inequality 
     (i.e. "<>").                                     
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
              Identification Errors.                  
                                                      
#65 Unknown label.                                   
#67 Forbidden linking (there is nothing to be linked 
    to).                                              
#68 Unknown variable identifier.                     
#69 This identifier is not reserved for any type.    
#70 "thesis" may not be used under a quantifier.     
#71 "thesis" may not be used outside a proof.        
#72 Different  types on both  sides of  an  equality 
     (inequality).                                    
                                                      
                                                      
                                                      
              Global Recovery Errors.                 
                                                      
#133 The beginning of the text repeated.             
#134 "environ"  expected.  Wrong  beginning  of  the 
     text.                                            
#135 "begin" expected.                               
#136 The beginning of the article repeated.          
#137 Closing "end" expected.                         
#138 Unexpected "end".                               
#139 Semicolon expected.                             
#140 This "proof" ("now") has no closing "end".      
#141 "begin" expected before "proof" or "now".       
                                                      
                                                      
                  Syntax Errors.                      
                                                      
Note: Most of those errors cause the so called Panic  
      Mode, i.e. when the  error occurs, the text is  
      not analyzed to the closest  semicolon, "end",  
      "proof"  or "now".  This  mode  may  cause the  
      occurrence of some other errors, that would not  
      be reported if the syntax error had not occur.  
                                                      
#150 Wrong beginning of an environment item.         
#151 Wrong beginning of a proof item.                
#152 Wrong beginning of the text proper.             
#153 Wrong beginning of diffuse statement.           
#154 Identifier in a qualified list expected.        
#155 Conclusion must be a compact statement.         
#156 "st" expected.                                  
#157 "holds", "for", or "ex" expected.               
#158 "holds", "for", "ex", or "st" expected.         
#159 Variable identifier reserved for the given type 
     expected.                                        
#160 "for" or comma expected.                        
#161 Variable identifier expected.                   
#162 Identifier   on  the   atomic   sentence   list 
     expected.                                        
#163 "]" expected.                                   
#164 "[", "=", or "<>" expected.                     
#165 Type identifier expected.                       
#166 Wrong beginning of a formula.                   
#167 Reasoning may not be linked.                    
#168 Label before "consider" is forbidden.           
#169 Parenthesis does not match.                     
#170 Forbidden  associative  notation for  "implies" 
     and "iff".                                       
#171 Label identifier expected.                      
#172 Type identifier after "be" or "being" expected. 
#173 Axiom label expected.                           
#174 "that" in condition group expected.             
#175 Probably a semicolon missing.                   
                                                      
                                                      
                                                      
                                                      
                  Overflow Errors.                    
                                                      
#236 Too many sentences.                             
#237 Too many arguments.                             
#238 Too many conditions.                            
#239 Too many references.                            
#240 Too many reserved identifiers.                  
#241 Too many variables accessible simultaneously.   
#242 Too many predicates.                            
#243 Too many types.                                 
#244 Too many labels accessible simultaneously.      
#245 Too many nestings.                              
#254 Memory overflow.                                
#255 Too many errors.                                
Error #4: This  inference  is not  accepted  by  the  
          CHECKER.                                    
                                                      
This  error  is   reported  when  the  inference  is  
incorrect  or  too complex  for the CHECKER. When it  
seems that the reasoning is all right  you will have  
to try to prove it in another way.                    
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #10: Too many basic sentences.                  
                                                      
The inference may be correct but too complex for the  
CHECKER's  algorithm.  It  should  be  divided  into  
several steps,  but it may  happen to be impossible.  
The inference below is correct but you cannot divide  
it:                                                   
                                                      
 ((p[] iff p[]) iff (p[] iff p[])) iff (p[] iff p[])  
                                                      
                                                      
                                                      
                                                      
                                                      
Error #12: The prefix of a universal sentence is too  
           long.                                      
                                                      
This   error  is  a  consequence  of  the  CHECKER's  
algorithm.  In  the main  reference you cannot  have  
more than 10 free variables.                          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #41: Forbidden assumption or conclusion.        
                                                      
The  assumption  (or conclusion) does not  match the  
current thesis.                                       
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #42: The assumption or conclusion is too long.  
                                                      
The  assumption  (or conclusion) does not  match the  
current thesis (it is extended).                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #43: VERUM   may   not    be    obtained    by  
           generalization.                            
                                                      
The sentence which is to be proved, is not a general  
one, so it cannot be proved by generalization.        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #44: Conjunction   may  not  be  obtained   by  
           generalization.                            
                                                      
In  order to prove  a conjunction  you have to prove  
all   conjuncts.   Conjunction  is   not  a  general  
sentence,  so the generalization is an incorrect way  
to prove it.                                          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #45: Generalization is  allowed only if thesis  
           is a universal sentence.                   
                                                      
The  sentence  which  is  to  be  proved,  must be a  
general one in order to prove it by generalization -  
a construction "let"..."be"...                        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #46: Types of the generalized variable and the  
           bound variable differ.                     
                                                      
Variables in the sentence have  different types from  
those you have introduced in the generalization.      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #47: There is still something to prove.         
                                                      
This proof is incomplete.                             
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #48: A local constant in the proof skeleton.    
                                                      
Only  constants  that  were  introduced  before  the  
beginning of  the proof  may  occur in it's skeleton  
(i.e. be used in assumptions or conclusions).         
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #65: Unknown label.                             
                                                      
This  label cannot be reached. It was not introduced  
or was introduced in the proof that is completed, or  
was not read due to a syntax error.                   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #67: Forbidden linking (there is nothing to be  
           linked to).                                
                                                      
You may link (i.e. use words "then" or "hence") only  
to  formulas  or to "assume" when it is not followed  
by "that".                                            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #68: Unknown variable identifier.               
                                                      
This  variable   cannot  be  reached.  It  was   not  
introduced  or was introduced in  the proof that  is  
completed, or was not read due to a syntax error.     
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #69: This  identifier  is not reserved for any  
           type.                                      
                                                      
The type for this identifier should be introduced in  
the   environment   by   using   the    construction  
                 "reserve"..."for"...                 
or  in  the  statement  by giving the type after the  
identifier (using "being").                           
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #70: "thesis"   may  not   be  used  under   a  
           quantifier.                                
                                                      
"thesis" means "what is left to be proved".           
                                                      
See also:                                             
 thesis                                              
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #71: "thesis" may not be used outside a proof.  
                                                      
"thesis" means "what is left to be proved".           
                                                      
See also:                                             
 thesis                                              
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #72: Different  types  on  both  sides  of  an  
           equality (inequality).                     
                                                      
The types on  both sides of an equality (inequality)  
must of course be the same.                           
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #130: Forbidden character in the text.          
                                                      
In  Mizar texts (excluding the comments) you may use  
letters,   digits,    the   underscore    character,  
apostrophe, colon, semicolon, coma, dot,parentheses,  
brackets,  the equality  sign, the  inequality  sign  
(i.e. "<>") and "&".                                  
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #132: "<"  may only be  used to  represent  an  
            inequality, (i.e. "<>").                  
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #133: The beginning of the text repeated.       
                                                      
This error occurs  when the  word "begin" appears in  
the  text for the second (third and so on) time. The  
error  will  occur  in  the case  when  "begin"  was  
assumptive.                                           
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #134: "environ"  expected. Wrong  beginning of  
            the text.                                 
                                                      
Every  Mizar  text  should  begin   with  the   word  
"environ"  (before  this  word  only   comments  may  
occur).  This error  does not affect the analysis of  
the text ("environ" is assumptive here).              
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #135: "begin" expected.                         
                                                      
"begin" must close the environment.                   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #136: The beginning of the article repeated.    
                                                      
This error  will occur  when the word  "environ"  is  
repeated (also in the case when  it was assumptive).  
This error stops the analysis of the text.            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #137: Closing "end" expected.                   
                                                      
One of the  words "proof" or "now" does not have the  
closing "end".                                        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #138: Unexpected "end".                         
                                                      
This  error  will  occur when "end"  appears in  the  
environment  (it is ignored)  or it  does  no t have  
matching "proof" or "now".                            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #139: Semicolon expected.                       
                                                      
It may be due to another syntax error.                
                                                      
Example: ... by Ax1 Ax2; - there is no comma          
                           between the labels.        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #140: This  "proof"  ("now")  has  no  closing  
            "end".                                    
                                                      
Simultaneously at the  end of the text error_#137 is 
reported.                                             
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #141: "begin"  expected   before  "proof"   or  
            "now".                                    
                                                      
"begin"  closes  the  environment  in  which   words  
"proof"  a nd   "now"  are  forbidden.   "begin"  is  
assumptive before one of those words.                 
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #150: Wrong beginning of an environment item.   
                                                      
Environment  item may  begin with a label identifier  
followed  by  a  colon  and  a  sentence,  the  word  
 "reserve"  (to   make  reservations)  or  the  word  
 "given" (to introduce global constants).             
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #151: Wrong beginning of a proof item.          
                                                      
Proof  item  may  begin  with an  identifier,  words  
"let", "given", "consider", "assume", "now", "then",  
"thus", "hence" or with  the sign (word) that begins  
formula i.e. "thesis", "contradiction", "for", "ex",  
 "not", or "(".                                       
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #152: Wrong beginning of the text proper.       
                                                      
The  statement   must  begin  with  "then" ,  "now",  
"consider", or  with  the  sign (word) that begins a  
formula i.e. "thesis", "contradiction", "for", "ex",  
 "not", or "(".                                       
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #153: Wrong  beginning  of  diffuse  statement  
            item.                                     
                                                      
Diffuse statement item may begin with an identifier,  
words  "let", "given",  "consider", "assume", "now",  
"then", "thus", "hence" or with the sign (word) that  
begins   formula  i.e.   "thesis",  "contradiction",  
"for", "ex",  "not", or "(".                          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #154: Identifier in a qualified list expected.  
                                                      
There must  occur the  list of qualified  variables:  
implicit  - just a list of  identifiers; explicit  -  
list of variables followed by "be"/"being" and  type  
identifier. If in  the construction both of the list  
are  to appear, the first  one have to  be qualified  
explicitly.                                           
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #155: Conclusion must be a compact statement.   
                                                      
The conclusion cannot begin with "now" or "consider"  
(those words cannot occur after "thus" or "hence").   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #156: "st" expected.                            
                                                      
After "ex" and variable list "st" must occur.         
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #157: "holds", "for", or "ex" expected.         
                                                      
After  "for", variable list, "st" and  the sentence,  
"holds" or quantified formula must occur.             
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #158: "holds", "for", "ex", or "st" expected.   
                                                      
After  "for"  and variable  list,  "st", "holds"  or  
quantified formula must occur.                        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #159: Variable  identifier   reserved  for the  
            given type expected.                      
                                                      
After  "reserve"  there   must  be  identifier  list  
(identifiers separated by commas).                    
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #160: "for" or comma expected.                  
                                                      
This  error  occurs   when  after  the   reservation  
identifiers there  is no  "for", or  when there is a  
syntax error before "for".                            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #161: Variable identifier expected.             
                                                      
On  both  sides of  equality (inequality) there must  
appear variable identifiers.                          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #162: Identifier on the  atomic  sentence list  
            expected.                                 
                                                      
Syntax  error  in  the  list of predicate  arguments  
(list  ended  by  comma,   no  comma   between   two  
identifiers).                                         
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #163: "]" expected.                             
                                                      
predicate must end with "]".                          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #164: "[", "=", or "<>" expected.               
                                                      
After  identifier (in the  beginning of the formula)  
must occur "[" (if  it is a predicate identifier) or  
"=" ("<>") (if it is a variable identifier).          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #165: Type identifier expected.                 
                                                      
In  reservation there  must  occur a type identifier  
after "for".                                          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #166: Wrong beginning of a formula.             
                                                      
In this  place the  beginning of the formula  should  
occur. It may  start with  identifier, "not", "for",  
"ex", "(", "contradiction", or "thesis".              
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #167: Reasoning may not be linked.              
                                                      
It  occurs when the  linked  statement (by "then" or  
"hence")  is  justified  by a proof or is a  diffuse  
statement.                                            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #168: Label before "consider" is forbidden.     
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #169: Parenthesis does not match.               
                                                      
One of the parentheses has not got a pair.            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #170: Forbidden   associative   notation   for  
            "implies" and "iff".                      
                                                      
Priorities  of "iff"  and  "implies" are equal. When  
two of those occur in the sentence,  parentheses are  
to be placed.                                         
                                                      
See also:                                             
 (_..._)                                             
                                                      
                                                      
                                                      
                                                      
                                                      
Error #171: Label identifier expected.                
                                                      
After  "by"  there  must  occur  the  list of  label  
identifiers (may not be empty).                       
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #172: Type  identifier  after "be" or  "being"  
            expected.                                 
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #173: Axiom label expected.                     
                                                      
Axiom must begin with the label  identifier followed  
by colon.                                             
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #174: "that" in condition group expected.       
                                                      
After "such", "that" must occur.                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #175: Probably a semicolon missing.             
                                                      
This  may  also  be any  syntax  error  that is  not  
recognized.                                           
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #236: Too many sentences.                       
                                                      
The maximum number of sentences in the text is 120.   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #237: Too many arguments.                       
                                                      
The maximum number of predicate arguments is 8.        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #238: Too many conditions.                      
                                                      
The maximum number of conditions after "that" is 11.  
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #239: Too many references.                      
                                                      
The maximum number of references is 20.               
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #240: Too many reserved identifiers.            
                                                      
The maximum number of reserved identifiers is 30.     
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #241: Too many variables accessible             
            simultaneously.                           
                                                      
The maximum number of variable is 40.                 
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #242: Too many predicates.                      
                                                      
The maximum number of predicates is 20.                
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #243: Too many types.                           
                                                      
The maximum number of types is 10.                    
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #244: Too many labels accessible                
            simultaneously.                           
                                                      
The maximum number of labels is 100.                  
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #245: Too many nestings.                        
                                                      
Up to 10 proofs may be nested.                        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #255: Too many errors.                          
                                                      
Too many errors in the text (more than 51), from now  
on the text is not analysed.                          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
  To  get into the  File commands press  ENTER when   
positioned on  the File command in the Main Menu, or  
F when  anywhere  else in  that menu,  or  AltF from  
elsewhere.                                            
                                                      
   The File  menu offers  many options that will let  
to  handle  files.  To select  one of  them position  
cursor  on it or press  the  highlighted letter. The  
following commands are available                      
                                                      
           Load              Directory              
           Select            Chng_Dir               
           Print             OS_Shell               
           Write             Quit                   
   Most of those commands will prompt you for a file  
name or a path. You may use the DOS wildcards i.e. *  
and ?. This will  cause the Directory_box to  appear 
on the screen.                                        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
   Load  command  lets you  load the file you  would  
like to edit.                                         
                                                      
Note: F3 is a shortcut for the Load command.          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
   Select  command  lets you  select one of the last  
eight loaded files. The first name on the list is of  
the file  currently in editor,  and the second is of  
the file that was loaded before the current one.      
                                                      
Note #1: AltF3 is a shortcut for the Select command.  
Note #2: Pressing ENTER on the last line of the  box  
         lets  you load any  file just like the Load 
         command.                                     
                                                      
                                                      
                                                      
                                                      
                                                      
   Print command lets you print the file.             
                                                      
Warning: This  command takes the file from the disk,  
         not from the editor, thus to print the file  
         in the editor you must save it first.        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
   Write  command  lets you  write  the file in  the  
editor to disk giving it  a new name. By default the  
current name is assigned to the disk file.            
                                                      
Note: Pressing  ENTER at the  Write  command  prompt  
      works  exactly  like  pressing  the  F2 hotkey  
      while in the editor.                            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
   Directory command lets you  see the file names in  
the  specified  directory. While giving the mask you  
can use DOS wildcards i.e. * and ?.                   
                                                      
Note: The F4 hotkey is used to enter a new mask.      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
   Chng Dir command lets  you  change the  directory  
without the tedious exiting to DOS. You are prompted  
for a path  of the  new directory. (You may do it in  
the same way as in DOS).                              
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
   OS Shell  command lets you exit  to the operating  
system  with  PC-MSE residing in memory. Now any DOS  
command may be executed. Type EXIT at the DOS prompt  
in order to return to the system.                     
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
   Quit  command lets you quit PC-MSE. When the file  
you are  editing  is  not saved you  are prompted to  
confirm its saving.                                   
                                                      
Note: AltX is a shortcut for the Quit command.        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Directory box  will appear  on  the screen  when the  
file name  contains DOS wildcards, i.e. * or  ?. You  
may  choose a  file  by  moving  to  it's  name  and  
pressing Enter. You may move to another directory in  
the same way.                                         
                                                      
Note1: The  names   of  directories   have  the  "\"  
       attached to them.                              
                                                      
Note2: The  current  path and  mask is  given on the  
       upper edge on the box.                         
                                                      
Note3: F4 is used to enter a new mask.                
                                                      
    To get  into the  Options  commands press  ENTER  
when  positioned  on the  Option command in the Main  
Menu, or O when  anywhere else in that menu, or AltO  
from elsewhere.                                       
                                                      
    This command contains setting that determine how  
the integrated environment works.                     
                                                      
   Mizar                                             
   Environment                                       
   Save_Options                                      
                                                      
                                                      
                                                      
   Mizar command lets you set the following options:  
                                                      
   If the LST_File option is set to On, a listing of  
the  checked text  will be created on the disk. This  
file will have the extension LST.                     
                                                      
   Check option let you set checking to first error,  
or to the end of the text.                            
                                                      
   Error File option  lets  you load a file of error  
comments that are to appear on the  screen. An error  
explanation  cannot  exceed 67  characters in length  
and  each comment must  occupied one  line. You  may  
write your own error file.                            
   Environment  command  lets you  set the following  
just by pressing Enter:                               
                                                      
Files Backup - On/Off (Backup copy has the extension  
 .OLD).                                               
Blanks - Insert/Delete (Recognizes blanks at the end  
 of the line).                                        
Tab Size - From 1 to 20 (By pressing Grey + or -).    
Get Info - Gives you info about the file.             
Config Auto Save - On/Off  ( Automatic   saving   of  
 configuration while exiting  or suspending PC-MSE).  
Edit Auto Save - On/Off  (Automatic   saving   while  
 exiting or suspending PC-MSE).                       
                                                      
   Save Options command  lets you  save the  options  
you have set on the disk. They will be automatically  
read when entering PC-MSE.                            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                    Help Index                        
                                                      
 Editor commands          Pulldown menus              
  blocks                   Edit_menu                
  cursor_movements         File_menu                
  find\replace             Mizar_menu               
  insert\delete            Options_menu             
  miscellaneous                                      
                                                      
  Hotkeys                                            
  Mizar_error_messages                               
  Mizar_reserved_words_&_signs                       
                                                      
                                                      
In this box you have the information about the  file  
in the editor, time  of your work, available memory,  
disk  free (in  bytes) and  about last the mizaring,  
i.e. last error position and  their number, and time  
of mizaring (N/A if not available).                   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
In the Mizaring box the  program shows its  name and  
version  number, name  of your  file, which line  is  
being checked, how much (in percent)  did the system  
already  check, time of analysis, how many lines per  
minute were  analyzed, and  the  number  of detected  
errors. You  can   stop  the  checking  by  pressing  
Ctrl-Break.                                           
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
The  file  was too  long to fit into  the  available  
memory  and  was  cut.  The  file  on  disk  remains  
untouched.                                            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
The  file  on  disk  is  read-only  and  cannot   be  
overwritten. You should have changed its attributes,  
when PC-MSE asked about it.                           
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
The  currently  active disk is to  small to save the  
whole file. You can use the File/Write option in the  
main menu. Another way is to exit to DOS through the  
File/OS Shell option, and remove some files from the  
disk.                                                 
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
The specified file was not found on the given path.   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
An illegal file  name was  given. A proper  name has  
the same syntax as in DOS.                            
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
There is no such path on the disk.                    
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
PC-MSE could  not  find  the file  COMMAND.COM. This  
means that  the option  File/OS  Shell will  not  be  
executed.                                             
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
The program  had trouble  executing the  COMMAND.COM  
which means that probably PC-MSE reserve  all of the  
memory. Large  memory resident programs shouldn't be  
installed while  working with  PC-MSE and it  should  
have at least 456 KB to work with.                    
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
The  system could  not find  the  error file on  the  
current directory or on the PC-MSE directory.         
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
DOS allows  only for à files to be open at any given  
time.  You  can  change  this  number  in  the   DOS  
environment   entering   the   following   line   in  
CONFIG.SYS:                                           
      Files = á                                       
where á > à.                                          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
PC-MSE cannot for some reason  access the  specified  
file. Probably the directory is full, or the name is  
of a read-only file or directory.                     
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
No writing to  disk is  possible. Take the disk  out  
and remove the protection tab if you  really want to  
write to it.                                          
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
There is no disk in the specified drive.              
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
A DOS error occurred for which PC-MSE has no comment.  
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
To  execute this  command, the  system  needed  more  
memory than is available  or the maximum file length  
was reached (in lines).                               
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
To copy or move a block, the memory would have to be  
a bit larger.                                         
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
While inserting a block from file (^KR) the  maximum  
file length was reached, and the block was cut.       
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
The disk is too small to write the whole block. Exit  
to DOS via the File/OS Shell and delete some files.   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
For some reason, PC-MSE cannot make a backup copy of  
a file.                                               
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
The system has  problems making the  LST file  (i.e.  
the file divided into  pages,  with errors and their  
explanations).                                        
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Access to file PC-MSE.CFG was  denied on the current  
directory and the PC-MSE directory.                   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
The systems cannot save options to PC-MSE.CFG. Maybe  
the file is read-only?                                
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
There are no  files of the  given format  (using DOS  
wildcards) on the disk.                               
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
Error #254: Memory overflow.                          
                                                      
A memory overflow  has  occurred  while  checking the  
article (there  is too little memory for Mizar). Try  
to shorten the text or remove resident programs from  
memory and try running Mizar again.                   
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
This is the last line of HELP!!!!                     
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                                                      
                        