Constructors, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. aid optionally specifies its article's name in uppercase. Notations, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature and vocabularies have to be specified. aid optionally specifies article's name in uppercase. Registrations, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. aid optionally specifies its article's name in uppercase. Identifications, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. aid optionally specifies its article's name in uppercase. Definientia, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. aid optionally specifies article's name in uppercase. Theorems, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. They can be either ordinary or definitional. The article number and order in article can be given, otherwise it belongs to the current article and order is implicit. Optional aid attribute specifies article name. constrkind and constrnr determine for def. theorems the defined constructor. If they do not appear (and kind='D'), then this is a canceled (verum) deftheorem. M V R K T D Schemes, either imported from other articles ( after accommodation) - the signature is implicit in that case, or exported from the current article - then the signature has to be specified. aid optionally specifies article's name in uppercase. Format keeps the kind of a given symbol and arities. For bracket formats (K) this keeps both symbols. Optionally a nr (of the format) is kept, to which patterns may refer, This implementation might change in some time. G K J L M O R U V Format info contains symbol formats and priorities. Priorities are used only for functor symbols. This implementation might change in some time. O K L Requirement is a constructor specially treated by the system. We give its internal number and optionally its name and the article id (aid) and order in article (absnr). M L V R K U G Requirements (now only the exported form). Adjective is a possibly negated (and paramaterized) attribute Optionally the article id (aid) and order in article (absnr) can be given. If available, presentational info (number of the Pattern) is given in pid. The heuristic for for displaying clusters is that attributes without pid have been added automatically by cluster mechanisms. The attribute kind (kind) 'V' can be added explicitly. V Cluster of adjectives Parameterized type - either mode or structure The kinds "L" and "G" are equivalent, "G" is going to be replaced by more correct "L" in Mizar gradually. First goes the LowerCluster, than UpperCluster Optionally the article id (aid) and order in article (absnr) can be given. If available, presentational info (number of the Pattern) is given in pid, and presentational info about variable introduced (e.g. in Fraenkel) may be given in vid. M G L errortyp Qualification formula (claims that a term has certaing type) Universally quantified formula If available, presentational info is given in pid. If available, numbere of the variable identifier is given in vid. Conjunctive formula. If available, presentational info is given in pid. Negation. If available, presentational info is given in pid. Atomic predicate formulas - schematic, attributive and normal Optionally the article id (aid) and order in article (absnr) can be given. If available, presentational info (number of the Pattern) is given in pid. P V R Private predicate with arguments is a shorthand for another formula Verum (true formula) Incorrect (erroneous formula) - e.g. containing undefined symbols Normal bound variable (deBruijn index). Their types are given in quantification - see For, Fraenkel Locus variable used usually for pattern matching. Their types are given elsewhere in data using them - see e.g. Constructor Free variable - used only internally in checker Lambda variable - unused now Normal local constant introduced e.g. by Let or Consider presentational info may be given in vid. Inference constant - used for internal term sharing Numeral Functor terms - schematic, aggregates, normal and selectors Optionally the article id (aid) and order in article (absnr) can be given. If available, presentational info (number of the Pattern) is given in pid. F G K U Private functor with arguments is a shorthand for another term. The first (mandatory) term is the expansion, arguments follow. Fraenkel term is defined by the types of its lambda arguments, its lambda term and the separating formula. Each type may optionally have presentational info about the variable (vid) inside. Choice term is defined by the type of its argument, Qua terms capture the retyping term qua type construct, but they are probably no longer used on this level. _It_ is a special term used in definitions. Probably no longer used on this level. Incorrect (erroneous term) - e.g. containing undefined symbols Proposition is a sentence with position and possible label (and its identifier). Argument types of constructors, patterns, clusters, etc. This encodes error during cluster processing Existential (registration) cluster. This says that exists Typ with Cluster (optionally followed by its extended version created by rounding up in current environment). Optionally the article id (aid) and order in article (nr) can be given. Conditional cluster. This says that Typ with the first cluster has also the second (optionally followed by its extended version created by rounding up in current environment). Optionally the article id (aid) and order in article (nr) can be given. Functor (term) cluster. This says that Term with ArgTypes has Cluster (optionally followed by its extended version created by rounding up in current environment), optionally with explicit Typ. Optionally the article id (aid) and order in article (nr) can be given. Identification (unoriented, this is not used currently, see identifyWithExp instead). This says that two terms with the two constructors at the top are equal when the pairs of their arguments specified in EqArgs are equal. Optionally the article id (aid) and order in article (nr) can be given. K U G V R This encodes error during identification processing Identification (oriented, currently used version). This says to identify anything matching the first term or formula pattern (with ConstrKind and ConstrNr as the top constructor) with the second pattern (instantiated by the matching). The type requirements for the matching (i.e. the loci) are given first. Note that this works only one way, if you want it also the other way, the symmetrical variant has to be explicitly stated as another identification. Optionally the article id (aid) and order in article (nr) can be given. K U G V R Schemes keep types of their second-order variables. First comes the scheme thesis, then the premises. The article number and order in article can be given, otherwise it belongs to the current article and order is implicit. Optional aid attribute specifies article name. This is now only the unique name of an article. Signature is a list of articles from which we import constructors. Constructor counts are used probably for renumerating. The article named can be given if not implicit. This implementation might change in some time. M L V R K U G Vocabularies keep for each article its symbol numbers. This implementation might change in some time. G K L M O R U V Single integer This is a pair of integers Structural loci are not used yet (that is all I know about them). Specify fields of aggregates and structmodes by their relative nr. Optionally the article id (aid) and order in article (absnr) can be given. The selector kind (kind) 'U' can can be added explicitly. U Properties of constructors; if some given, the first and the second argument to which they apply must be specified. Constructors are functors, predicates, attributes, etc. nr, kind and aid (article id) determine the constructor absolutely in MML, relnr optionally gives its serial number in environment for a particular article (it is not in prels). All have (possibly empty) properties, argtypes and some have one or more mother types. The optional final Fields are selectors for agrregates and structmodes. aggregbase is for aggregates (maybe OVER-arguments), structmodeaggrnr is for structmodes (nr of corresponding aggregate). absredefnr and redefaid optionally give absolute address of a redefinition. M L V R K U G Ending position (e.g. of blocks). Patterns map formats with argtypes to constructors. The format is either specified as a number (then it must be available in some table), or is given explicitely. Visible are indeces of visible (nonhidden) arguments. If antonymic, its constructor has to be negated. Mode patterns can have expansion instead of just a constructor - this might be done for other patterns too, or replaced by the _equals_ mechanism. The J (forgetful functor) patterns are actually an example of another expanded patterns, but the expansion is uniform for all of them, so it does not have to be given. The invalid ConstrKind J is now used for forgetful functors, this should be changed. Optionally the article id (aid) and order in article (nr) can be given. relnr optionally gives its serial number in environment for a particular article (it is not in prels). redefnr optonally gives the relative number of the original pattern to which the current is defined as synonym/antonym. M L V R K U G J M L V R K U G J ConstrDef holds a term together with types of its variables and the top-level functor. Used now mainly for identify. K U G DefMeaning consists of the formulas and terms defining a constructor. It can be either defined by _equals_ (terms) or by _means_ (formulas). It may contain several partial (case) definitions - first in them comes the definition (term or formula) valid in that case and second comes the case formula. The final term or formula specifies the default case, it is mandatory if no partial definitions are given. If no default is given, the disjunction of all case formulas must be true (this have to be proved using the _consistency_ condition). e m Definiens of a constructor. This overlaps a bit with Constructor. defnr is the number of the corresponding definitional theorem, and vid optionally its label's identifier. First come the argument types and possibly also the result type. The optional formula is conjunction of all assumptions if any given. If this is a redefinition, essentials are indeces of arguments corresponding to the arguments of original, otherwise it is just identity. This could be now encode with just one number like the superfluous does for Constructor. Optionally the article id (aid) and order in article (nr) can be given. relnr optionally gives its serial number in environment for a particular article (it is not in prels). vid gives a number of the label identifier if present. M L V R K U G Reference can be either private (coming from the current article) - their number is the position at the stack of accessible references (so it is not unique), or library - these additionally contain their kind (theorem or definition) and article nr. The position in the inference is kept for error messaging. For a private inference, the vid attribute optionally tells its identifier's number. T D By encodes one simple justification. From encodes one scheme justification, it cannot be linked. This is one step in an iterative equation. Local dictionary for an article. The symbol kinds still use very internal notation. Reports from the Mizar checker, now only arithmetical evaluations. They are now only available when the verifier is compiled with a special directive - this should be changed to a user option eventually. Reports from the Mizar schematizer - scheme instantioations. They are now only available when the verifier is compiled with a special directive - this should be changed to a user option eventually. The complete article after analyzer. aid specifies its name in uppercase, and mizfiles optionally gives a location of the local MIZFILES directory used during processing the article (needed to know for browsing of locally installed html in MIZFILES/html). Numbers of Definiens used in expanding the thesis, together with their counts. Introduction of local constants, the numbering is automatic, so only types are needed. For easier presentation, nr optionally contains the number of the first local constant created here. Each type may optionally have presentational info about the variable (vid) inside. One assumption may consist of several propositions. This is existential assumption, it may be used when the normal assumption starts with existential quantifier, and emulates the use of assume followed by consider. First comes the reconstructed assumed existential statement, then the newly introduced local constant(s), and finally the proposition(s) containing the new local constant(s). For easier presentation, nr optionally contains the number of the first local constant created here. Each type may optionally have presentational info about the variable (vid) inside. Take without equality. This does not introduce a new local constant, just changes the thesis. Take with equality. This introduces a new local constant, whose type is given here. For easier presentation, nr optionally contains the number of the first local constant created here. The type may optionally have presentational info about the variable (vid) inside. Justified conclusion. In text, this can appear as _hence_, _thus_ or _hereby_ (which starts diffuse conclusion). First comes the reconstructed existential statement and its justification, then the new local constants and zero or more propositions about them. For easier presentation, nr optionally contains the number of the first local constant created here. Each type may optionally have presentational info about the variable (vid) inside. First comes the series of target types and reconsidered terms. For all these terms a new local variable with its target type is created, and its equality to the corresponding term is remembered. Finally the proposition about the typing is given and justified. For easier presentation, nr optionally contains the number of the first local constant created here. Each type may optionally have presentational info about the variable (vid) inside. This is e.g.: set a = f(b); . The type of the new local constant is given. This local constant is now always expanded to its definition, and should not directly appear in any expression, but it is now needed for some implementation reasons. For easier presentation, nr optionally contains the number of the first local constant created here. The type may optionally have presentational info about the variable (vid) inside. Private functor. First come the types of arguments, then its definition and the result type. For easier presentation, nr optionally contains number of the private functor created here, and its identifier's number (vid). Private predicate. First come the types of arguments, then its definition. For easier presentation, nr optionally contains number of the private predicate created here, and its identifier's number (vid). The changed thesis is printed after skeleton items in proofs, together with the numbers of definientia used for its expansion. Case of one or more propositions. Supposition of one or more propositions. The block thesis is printed for proofs in the beginning and for diffuse reasoning in the end. For diffuse reasoning, the series of temporary subthesis corresponding to all skeleton items is printed before the main theses (in the same order as the skeleton items in the block). Block starting with one case, the direct and diffuse version (this depends on the kind of its parent block). The block thesis is printed for proofs in the beginning and for diffuse reasoning in the end. Block starting with one supposition, the direct and diffuse version (this depends on the kind of its parent block). The block thesis is printed for proofs in the beginning and for diffuse reasoning in the end. This means that the author has skipped the proof. Articles with such items are not yet fully completed. This justifies the case split (the disjunction of all Suppose or Case items in direct subblocks) in PerCasesReasoning. The case split is only known after all subblocks are known, so this is the last item in its block, not like in the Mizar text. Reasoning per cases. It only contains CaseBlock or SupposeBlock subblocks, with the exception of the mandatory last PerCases justifying the case split. Direct and diffuse versions are possible (this depends on the kind of its parent block). The block thesis is printed for proofs in the beginning and for diffuse reasoning in the end. Skeleton items change the InFile.Current thesis, for Proof the changed Thesis together with used expansions is printed explicitely after them. PerCasesReasoning is not included here. Reasoning is a series of skeleton and auxiliary items, finished by optional per cases reasoning. Direct proof of some proposition (which is the proof's thesis). Label (nr) of proof (if any) is label of its thesis, vid is then the identifier nr of this label. Diffuse statement - its thesis is reconstructed in the end. Label (nr) and its identifier (vid) of diffuse statement (if any) is label of its thesis. Direct justification. Iterative equality. The optional numbers (nr) is serial label numbering, and original label identifier (vid). Auxiliary items are items which do not change thesis. Reservation of a new variable for a type. The type may optionally have presentational info about the variable (vid) inside. Theorem as a proposition with justification. Theorems created from definitions are now printed as separate top-level items after definitional blocks, constrkind and constrnr determine the defined constructor. If they do not appear, this is a canceled (verum) deftheorem. M V R K A property of a constructor, the proposition expreesing it, and its justification. The possible correctness conditions are following. They can either be only stated in the Correctness, which conjugates them and proves them all, or come separately as a proposition with a justification. This is a way how to state all correctness conditions in one keyword. The relevant conditions are computed by the analyzer and printed here, their conjunction has to be justified. Canceled theorem ( if on top-level), definition or registration (if inside such blocks). We should add to this the number of canceled items as an attribute. Declaration of a scheme functor, possibly with its identifier number. Declaration of a scheme predicate, possibly with its identifier number. Scheme blocks are used for declaring the types of second-order variables appearing in a scheme, and for its justification. This could be a bit unified with Scheme later. schemenr is its serial nr in the article, while vid is its identifier number. Definition of a functor, predicate, mode, attribute or structure. with optional label, properties and correctness conditions. Sometimes no constructor is created (e.g. for expandable modes). The second optional form creating three or more constructors is for structure definitions, which define the aggregate functor, the structure mode, the strict attribute and zero or more selectors, and create existential registration for the strict attribute. If any definientia and definitional theorems are created, they follow immediately after the enclosing definitional block (this might be changed in the future). Number, position, and identifier number of the definiens (vid) can be optionally given. M V R K G A block of one or more (possibly canceled) (re)definitions, possibly with assumptions. If any definientia and definitional theorems are created, they follow immediately after this block. One justified cluster registration. The correctness conditions could be made more specific for each. One justified identification registration. The correctness conditions could be made more specific. Block of cluster registrations. Block of synonyms or antonyms. The patterns are semantically irrelevant and are not printed yet - fix this. Builtin numerical evaluations of arithmetical functors and predicates. For predicates, the value can be false. Arguments are generally polynoms with complex coefficients. For functors, the last polynom is the result value. Rational numbers Complex rational numbers used in Mizar Monomial has a coefficient and a series of variables with their exponents. Polynomial consists of several monomials. Instantions of scheme functors and predicates. and predicates. Scheme functors can be instantiated to other functors or terms (if zero arity). Scheme predicates can be instantiated to other predicates F H G K U P S V R