Mizar Errors Explanation File # # 1 It is not true # 4 This inference is not accepted # 8 Too many instantiations # 9 Too many instantiations # 10 Too many basic sentences in an inference # 11 Too many constants in an inference # 12 Too long universal prefix # 13 Too many complexes # 14 Too many terms in an inference # 15 Too many equalities in an inference # 16 Collection overflow # 20 The structure of the sentences disagrees with the scheme # 21 Invalid instantiation of a scheme functor # 22 Invalid instantiation of a scheme predicate # 23 Invalid order of arguments in the instantiated predicate # 24 Instantiations of the same scheme predicate do not match # 25 Instantiations of the same scheme constant do not match # 26 Substituted constant does not expand properly # 27 Invalid instantiation of a scheme constant # 28 Invalid list of arguments of a functor # 29 Instantiations of the same scheme functor do not match # 30 Invalid type of the instantiated functor # 31 Disagreement of correspondents of a constant # 32 Too many fillings of a functor # 33 Too many fillings of a predicate # 40 Non-unique matching of a locus of the substitute of a predicate variable # 41 Non-unique matching of a locus of the substitute of a functor variable # 42 Non-unique matching of a locus of the substitute of a functor variable # 43 Cannot decompose a conjunction of formal sentences # 44 Formal predicate in a Fraenkel operator of formal construction # 45 Wrong order of the declarations of scheme functor or nested functor # 46 Probably the incorporation of an argument # 50 Nongeneralizable variable in the skeleton of a reasoning # 51 Invalid conclusion # 52 Invalid assumption # 53 Invalid case # 54 The cases are not exhausted # 55 Invalid generalization # 56 Disagreement of types # 57 The type of the instatiated term doesn't widen properly # 58 Mixing "case" with "suppose" is not allowed in one "per cases" reasoning # 59 The theses in each case should be equal formulae # 60 Something remains to be proved in this case # 62 Free variables not allowed in an iterative equality # 63 Unexpected proof # 64 Invalid exemplification in a diffuse statement # 65 "thesis" is only allowed inside a proof # 66 "axiom" is only allowed in an axiomatic file # 68 Nongeneralizable variable in the skeleton of a reasoning # 69 Nongeneralizable variable in a definiens # 70 Something remains to be proved # 72 Unexpected correctness condition # 73 Correctness condition missing # 76 Registration correctness condition mismatch # 77 Still not implemented # 78 The type of the argument must widen to the result type # 79 Types of arguments must be equal # 80 Cannot be used in a permissive definition # 81 It is only meaningful for binary predicates # 82 It is only meaningful for binary functors # 83 It is only meaningful for unary functors # 84 The result type is not invariant under swapping the arguments # 85 The result type must widen to the type of the argument # 89 As yet not implemented for redefined functors # 90 Attributes are not allowed in a prefix # 91 Homonymic fields in structure declaration # 92 Type of the field must be equal to the type in prefix # 93 Missing field of a prefix # 94 Prefix must be a structure # 95 Inconsistent cluster # 96 Only standard functors and selectors can be used in a functorial cluster registration # 97 Non clusterable attribute # 98 Cannot mix left and right pattern arguments # 99 The argument(s) must belong to the left or right pattern # 100 Unused locus # 101 Unknown mode # 102 Unknown predicate # 103 Unknown functor # 104 Unknown structure # 105 Illegal projection # 106 Unknown attribute # 107 Invalid list of arguments of redefined constructor # 108 Invalid list of arguments of redefined constructor # 109 Invalid order of arguments of redefined constructor # 110 Only nullary prefixes are allowed # 111 Non registered attribute cluster # 112 Unknown predicate # 113 Unknown functor # 114 Unknown mode # 115 Unknown attribute # 116 Invalid "qua" # 117 Invalid specification # 118 Invalid specification # 119 Illegal cluster # 120 Disagreement of argument types # 121 Disagreement of argument types # 122 Disagreement of argument types # 123 Disagreement of argument types # 124 Disagreement of argument types # 125 Argument of a selector must be a structure # 126 Unknown selector functor # 127 Argument must be an elementary type # 128 Arguments must be elementary types # 129 Invalid free variables in a Fraenkel operator # 130 Redefinition of an attribute with predicate pattern is not allowed # 131 No reserved type for a variable, free in the default type # 132 Invalid "exactly" # 133 Cannot cluster attribute with arguments # 134 Cannot redefine expandable mode # 135 Inaccessible selector # 136 Non registered cluster # 137 "SUBSET" missing in the "requirements" directive # 138 Cannot identify a local constant, free in the default type # 139 Invalid type of an argument. # 140 Unknown variable # 141 Locus repeated # 142 Unknown locus # 143 No implicit qualification # 144 Unknown label # 145 Inaccessible label # 146 Theorem number must be greater than 0 # 147 Unknown theorems file # 148 Unknown private functor # 149 Unknown private predicate # 150 A variable free in default type has explicit qualification # 151 Unknown mode format # 152 Unknown functor format # 153 Unknown predicate format # 154 Unknown field # 155 Unknown prefix # 156 Invalid equality format # 157 Exactly one term is expected before "is" # 158 Two different formats for a structure symbol # 159 Invalid iterative equality # 160 This variable still cannot be accessed # 161 Fixed variables cannot be postqualified # 162 A free variable identified with a new implicit qualification # 163 Disagreement of reservations of a free variable # 164 Nothing to link # 165 Unknown functor format # 166 Unknown functor format # 167 Unknown functor format # 168 Unknown functor format # 169 Unknown functor format # 170 Unknown functor format # 171 Unknown functor format # 172 Unknown functor format # 173 Unknown functor format # 174 Unknown functor format # 175 Unknown attribute format # 176 Unknown structure format # 177 Link assumes a straightforward justification # 178 Link assumes a straightforward justification # 179 It is not a locus # 180 Too many arguments # 181 Not so many arguments in this definition # 182 Unknown selector format # 183 Accessible mode format has empty list of arguments # 184 Accessible structure format has empty list of arguments # 185 Unknown structured mode format # 186 "equals" is only allowed for functors # 189 Left and right pattern must have the same number of arguments # 190 Inaccessible theorem # 191 Unknown scheme # 192 Inaccessible theorem # 193 Inaccessible scheme # 194 Wrong number of premises # 195 Scheme uses constructors which are not in your environment # 196 Unknown scheme # 197 Scheme definition repeated # 198 It is meaningless to define an antonym to a functor or a mode # 199 Inaccessible definitional theorem # 200 Too long source line # 201 Only characters with decimal ASCII codes between 32 and 126 are allowed # 202 Too large numeral # 203 Unknown token, maybe an illegal character used in an identifier # 210 Wrong item in environment declaration # 211 Unexpected "environ" # 212 "environ" expected # 213 "begin" missing # 214 "end" missing # 215 No pairing "end" for this word # 216 Unexpected "end" # 217 ";" missing # 218 Unexpected "(" - parenthesizing attributes is not allowed # 219 Unexpected "proof" # 220 Local predicates are not allowed in library items # 221 Local functors are not allowed in library items # 222 Local constants are not allowed in library items # 223 Adjective cluster expected # 228 Unexpected "reconsider" # 229 "redefine" repeated # 230 Only one "per cases" is allowed in a reasoning # 231 "per cases" missing # 232 "case" or "suppose" expected # 240 Definition blocks must not be nested # 241 Directives are not allowed in the text proper # 242 "reserve", "struct", "scheme" and "theorem" not allowed in a definition block # 250 "$1",...,"$10" are only allowed inside the definiens of a private constructor # 251 "it" is only allowed inside the definiens of a public functor or mode # 253 "means" or "equals" expected # 255 It is not allowed for expandable modes # 256 "of" expected #257 Right term must be a subterm of the left term #258 Choice and Fraenkel terms are not allowed in reductions # 271 Redefined mode cannot be expandable # 272 It is meaningless to redefine a cluster # 273 "redefine" is not allowed here # 274 "means" not allowed in a definition of an expandable mode # 300 Identifier expected # 301 Predicate symbol expected # 302 Functor symbol expected # 303 Mode symbol expected # 304 Structure symbol expected # 305 Selector symbol expected # 306 Attribute symbol expected # 307 Numeral expected # 308 Identifier or theorem file name expected # 309 Mode symbol or attribute symbol expected # 310 Right functor bracket expected # 311 Paired functor brackets must be of the same kind # 312 Scheme reference is not allowed in a simple justification # 313 "sch" expected # 314 Incorrect beginning of a pattern # 315 Mode "set" cannot be parametrized # 320 Selector or structure symbol expected # 321 Predicate symbol or "is" expected # 329 Selector without arguments is only allowed inside a structure pattern # 330 Unexpected end of an item (perhaps ";" missing) # 336 Associative notation must not be used for "iff" and "implies" # 340 "holds", "for" or "ex" expected # 350 "that" expected # 351 "cases" expected # 360 "(" expected # 361 "[" expected # 362 "{" expected # 363 "(#" expected # 364 "(" or "[" expected # 370 ")" expected # 371 "]" expected # 372 "}" expected # 373 "#)" expected # 374 Incorrect order of arguments in an attribute definition # 375 Wrong beginning of a cluster registration # 376 Incorrect functorial registration - addjectives expected # 377 Incorrect conditional registration - type expected # 378 Parenthesizing adjective clusters is not allowed # 379 Term list is not allowed here # 380 "=" expected # 381 "if" expected # 382 "for" expected # 383 "is" expected # 384 ":" expected # 385 "->" expected # 386 "means" or "equals" expected # 387 "st" expected # 388 "as" expected # 389 "proof" expected # 390 "and" expected # 391 Incorrect beginning of a text item # 392 Incorrect beginning of a definition item # 393 Incorrect beginning of a reasoning item # 394 Statement expected # 395 Justification expected # 396 Formula expected # 397 Term expected # 398 Type expected # 399 Functor pattern expected # 400 Still not implemented # 401 "not" expected # 402 A bare infinitive expected # 403 "such" expected # 404 "to" expected # 405 "for" expected # 406 "for" or "->" expected # 450 Too many variables # 451 Too many predicate formats # 452 Too many functor formats # 453 Too many mode formats # 454 Too large theorem number # 455 Too many labels in a definition block # 456 Too many references in an inference # 458 Too many private predicates # 459 Too many private functors # 460 Too many reserved identifiers # 461 Too many free variables # 462 Too many modes # 465 Too many predicates # 466 Too many functors # 467 Too many structures # 468 Too many selectors # 469 Too many loci # 470 Too complicated term # 471 Too many selectors in one structure definition # 472 Too many references # 473 Too many premisses in a simple justification # 474 Too complicated term # 476 Too many default signature files # 477 Too many predicate, mode or functor symbols # 478 Too many labels # 479 Too many loci in one definition block # 480 Too many default vocabulary files # 481 Too many functor symbols in default vocabulary files # 482 Too many free variable scopes # 483 Too many variables # 484 Too many reservations # 485 Too nested reasoning # 486 Too many functor formats # 487 Too many scheme identifiers # 488 Too many unreserved free variables # 489 Memory handling in unifier failed # 490 Too many free variables in reservations # 491 Too many structure formats # 492 Too many functor formats # 493 Too many parameters in one scheme # 494 Too complicated scheme (too many external variables) # 495 Too complicated scheme (too many occurrences of a functor variable) # 496 Too complicated scheme (too many occurrences of a predicate variable) # 497 Too many functor symbols # 498 Too many occurrences of arguments of a second order variable # 499 Too many errors # 601 Irrelevant label # 602 Irrelevant reference # 603 Irrelevant linking # 604 Irrelevant inference # 605 Irrelevant linked inference # 607 Justification can be straightforward # 608 Linkable statement # 609 Irrelevant "that" # 610 Beginning of an inaccessible item # 611 End of an inaccessible item # 612 Beginning of inaccessible conditions # 613 End of inaccessible conditions # 614 Duplicated label identifier # 615 Unexpected "@proof" # 616 "be" recommended # 703 Unnecessary "proof thus thesis; end;" # 704 Irrelevant signature directive # 706 Unnecessary item in the "theorems" directive # 707 Unnecessary item in the "schemes" directive # 708 Theorem should be replaced by an equal one # 709 Irrelevant item in the "vocabularies" directive # 710 Irrelevant item in the "definitions" directive # 711 Identity functor definition # 712 Synonym of a functor definition # 713 Irrelevant redefinition of a functor # 714 Irrelevant redefinition of a mode # 715 Irrelevant "reconsider" of a variable # 716 Irrelevant "reconsider" of a term # 717 Irrelevant reconsider # 720 The first two arguments of the iterative equality are equal # 721 The first argument of the iterative equality is equal to the next one # 722 The second argument of the iterative equality is equal to the next one # 724 This argument of the iterative equality is equal to the next one # 725 This argument of the iterative equality is equal to the previous one # 730 Redundant reconsidering of variables # 731 Redundant reconsidering of terms # 732 Redundant reconsidering of a variable # 733 Redundant reconsidering of a term # 734 Redundant considering # 735 Irrelevant variable reservation # 736 Unused private functor # 737 Unused private predicate # 738 Unused variable introduced by "set" # 739 The variable introduced by "set" used only once # 740 Unused variable introduced by "given" # 742 Unused variable introduced by "take" # 743 Unused variable introduced by "consider" # 746 References can be moved to the next step of this iterative equality # 800 Library corrupted # 801 Cannot find vocabulary file # 802 Cannot find formats file # 803 Cannot find notations file # 804 Cannot find signature file # 805 Cannot find definitions file # 806 Cannot find theorems file # 807 Cannot find schemes file # 808 Cannot find constructors file # 809 Cannot find registrations file # 810 Directive name repeated # 811 Invalid priority of a functor symbol on a vocabulary file # 812 An empty line on a vocabulary file # 813 Invalid qualifier on a vocabulary file # 814 Invalid character or space in a symbol # 815 A vocabulary symbol repeated # 816 Invalid priority # 817 An empty symbol # 821 A scheme identifier repeated # 825 Cannot find constructors name on constructor list # 830 Nothing imported from notations # 831 Nothing imported from registrations # 832 Nothing imported from definitions # 833 Nothing imported from theorems # 834 Nothing imported from schemes # 855 Cannot find requirements file # 856 Inaccessible requirements directive # 891 MML identifier should be written in capitals # 892 MML identifier should be at most eight characters long # 900 Too complex skeleton # 911 Too long term without parentheses # 912 Too long right nesting of a term # 913 Too many labels (simultaneously accessible) # 914 Too many references in an inference # 915 Too many ranges of free variables # 916 Too many reservations # 917 Too many free variables in reservations # 918 Too many variables (simultaneously accessible) # 919 Too many reserved identifiers # 920 Too many private functors # 921 Too many private predicates # 923 Too many different clusters # 924 Common number of loci exceeded # 925 Too many predicate patterns # 926 Too many functors # 927 Too many functor patterns # 928 Too many modes # 929 Too many mode patterns # 930 Too many attributes # 931 Too many attribute patterns # 933 Too many structures # 935 Too many selectors # 936 Too many registered clusters # 937 Too many arguments # 938 Too many terms # 950 Too many schemes # 951 Too many imported files # 1001 -------> Turbo Pascal Errors ( ErrNr = PascalErrNr+1000 ) Invalid function number # 1002 File not found # 1003 Path not found # 1004 Too many open files # 1005 File access denied # 1006 Invalid file handle # 1012 Invalid file access code # 1015 Invalid drive number # 1016 Cannot remove current directory # 1017 Cannot rename across drives # 1018 No more files # 1100 Disk read error # 1101 Disk write error # 1102 File not assigned # 1103 File not open # 1104 File not open for input # 1105 File not open for output # 1106 Invalid numeric format # 1150 Disk is write-protected # 1151 Bad drive request struct length # 1152 Drive not ready # 1154 CRC error in data # 1156 Disk seek error # 1157 Unknown media type # 1158 Sector Not Found # 1159 Printer out of paper # 1160 Device write fault # 1161 Device read fault # 1162 Hardware failure # 1200 Division by zero # 1201 Range check error # 1202 Stack overflow error # 1203 Heap overflow error # 1204 Invalid pointer operation # 1205 Floating point overflow # 1206 Floating point underflow # 1207 Invalid floating point operation # 1208 Overlay manager not installed # 1209 Overlay file read error # 1210 Object not initialized # 1211 Call to abstract method # 1212 Stream registration error # 1213 Collection index out of range # 1214 Collection overflow error # 1215 Arithmetic overflow error # 1216 General Protection fault # 1217 Segmentation fault # 1255 Ctrl Break # 1994 -------> I/O stream errors I/O stream error: Put of unregistered object type # 1995 I/O stream error: Get of unregistered object type # 1996 I/O stream error: Cannot expand stream # 1997 I/O stream error: Read beyond end of stream # 1998 I/O stream error: Cannot initialize stream # 1999 I/O stream error: Access error #