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