%\documentstyle[a4]{article}
\documentclass{article}
\usepackage{a4}

\title{\bf Mizar: An Impression}

\author{Freek Wiedijk\\
Nijmegen University\\
{\tt <freek@cs.kun.nl>}}

\date{}

\begin{document}
\maketitle

\begin{abstract}
\noindent
This note presents an introduction to the Mizar system,
followed by a brief comparison between Mizar and Coq.
Appended are a Mizar grammar and an annotated example of
a complete Mizar article.
\end{abstract}

\section{What It Is}

Mizar is a system for representing mathematical proof in a
computer such that a program can check the correctness.  It has
been developed by Andrzej Trybulec and his team in Bialystok,
Poland since about 1973.  The Mizar language is quite close to
the language of informal mathematics (`the mathematical
vernacular').  Mizar is based on a ZF-like set theory with
classical first order logic.  Part of the Mizar project is the
development of a large database of mathematics which currently
numbers 587 `articles' taking 41 megabytes (even without the
proofs it's 6 megabytes).  A major project currently underway is
the translation to Mizar (under direction of Grzegorz Bancerek)
of a real mathematics book: `A Compendium of Continuous
Lattices' \cite{gie:hof:kei:law:mis:sco:80}.

Mizar has had a number of dialects.  `Mizar MSE' (also called
`baby Mizar') is a toy language not meant for real
applications.  The current implementation of the full Mizar
language is called `PC Mizar'.  It's written in Turbo/Borland
Pascal and runs only under DOS/Windows.  Functionally it's
basically one program, `\verb|mizf|', that non-interactively checks a
Mizar file for its correctness.

The Mizar system doesn't have much documentation.  The text
that most resembles a manual%
\footnote{An electronic version of this manual is available on the World Wide Web at
the address
{\tt <http://www.cs.kun.nl/\~{}freek/mizar/mizarmanual.ps.gz>}}
is `An Outline of PC Mizar'
by Micha{\l} Muzalewski \cite{muz:93}.

A way to explore the Mizar language that works surprisingly
well is to study the Mizar syntax
(see appendix \ref{grammar} on page \pageref{grammar} for a context free grammar)
and for specific constructions
to search the Mizar library for examples.


\section{Definitions}

A Mizar article consists of an `\verb|environ|' header which
indicates what other articles from the Mizar library it refers
to, followed by a sequence of definitions and theorems.

A definition has the general shape:

\begin{verse}
\verb|definition|\\
\verb|  let |{\it arguments\/}\verb|;|\\
\verb|  assume |{\it preconditions\/}\verb|;|\\
\verb|  func |{\it pattern\/}\verb| -> |{\it type\/}\verb| means :|{\it label\/}\verb|: |{\it statement\/}\verb|;|\\
\verb|  |{\it correctness proof\/}\\
\verb|end;|
\end{verse}

The {\it pattern\/} presents the way the operation is written (both
normal function notation and operator notation are possible; and
not all arguments need to be present in the pattern: Mizar
supports implicit arguments).  In the defining {\it statement\/} the
defined object is referred to as `\verb|it|'.  The correctness proof
has to show existence and uniqueness of the defined object given
the preconditions.

A definition of the form:

\begin{verse}
\verb|func |{\it pattern\/}\verb| -> |{\it type\/}\verb| means :|{\it label\/}\verb|:|\\
\verb|  it = |{\it expression\/}\verb|;|
\end{verse}

\noindent
can be abbreviated as:

\begin{verse}
\verb|func |{\it pattern\/}\verb| -> |{\it type\/}\verb| equals :|{\it label\/}\verb|: |{\it expression\/}\verb|;|
\end{verse}

Here is an example of a definition, the definition of `\verb|log|'
(from article `\verb|POWER|'):

\begin{verse}
\verb|reserve a,b for Real;|\\
\verb|definition|\\
\verb|  let a,b;|\\
\verb|  assume A1: a>0 & a<>1 and A2: b>0;|\\
\verb|  func log(a,b) -> Real means|\\
\verb|:Def3: a to_power it = b;|\\
\verb|  existence|\\
{\it 251 lines of existence proof omitted\/}\\
\verb|  uniqueness by A1,Th57;|\\
\verb|end;|
\end{verse}

\noindent
(The `\verb|reserve|' statement reserves variables for a certain
type: the type of a reserved variable needn't be given.  So
because of the `\verb|reserve|' statement in the first line, the
`\verb|let a,b|' means `\verb|let a,b be Real|'.)

And here is the definition of subtraction (from `\verb|REAL_1|'):

\begin{verse}
\verb|reserve x,y for Real;|\\
\verb|definition|\\
\verb|  let x,y;|\\
\verb|  func x-y -> Real equals :Def3: x+(-y);|\\
\verb|  correctness;|\\
\verb|end;|
\end{verse}

\noindent
(The `\verb|correctness|' at the end is an abbreviation of all
elements of the correctness proof that are left to be proved:
for a definition with `\verb|means|' these are `\verb|existence|' and
`\verb|uniqueness|'; and for a definition with `\verb|equals|' it's
`{\tt co\-her\-ence}', which says that the object has the correct type. 
In this example correctness is obvious, so there's no `\verb|by|'
justification needed.)

Apart from `\verb|func|' definitions for functions, Mizar has `\verb|pred|'
definitions for predicates and `\verb|mode|' and `\verb|attr|' definitions for
types (for an explanation of Mizar types, see section \ref{types} below). 
These are syntactically rather similar to the `\verb|func|' definitions
and will not be explained in detail.

In the definition of functions and predicates synonyms and
antonyms can be given and properties like commutativity,
symmetry, reflexivity and irreflexivity can be indicated.  The
Mizar system will magically `know' about these things, and
variations on the same expression will behave like  they are
merely syntactic variants.  For instance because the definition
of $\leq$ (in `\verb|ARYTM|') is:

\begin{verse}
\verb|definition|\\
\verb|  let x,y be Element of REAL;|\\
\verb|  pred x |$\leq$\verb| y means|\\
{\it 6 lines of definition\/}\\
{\it 89 lines of correctness proof\/}\\
\verb|  synonym y |$\geq$\verb| x;|\\
\verb|  antonym y < x;|\\
\verb|  antonym x > y;|\\
\verb|end;|
\end{verse}

\noindent
it doesn't matter whether one writes \verb|x < y| or \verb|y > x|.  Also it
means that theorems about \verb|<| often also are usable (probably
with a contraposition of an implication) to prove statements
about $\geq$.


\section{Theorems}

The major part of a Mizar article consists of theorems (just
like the major part of a computer program source consists of
procedures/functions).  A theorem has the shape:

\begin{verse}
\verb|theorem |{\it label\/}\verb|: |{\it statement\/}\\
\verb|proof|\\
\verb|  |{\it proof steps\/}\\
\verb|end;|
\end{verse}

An example of a theorem (from article `\verb|IRRAT_1|'):

\begin{verse}
\verb|theorem T2:|\\
\verb|  ex x, y st x is irrational & y is irrational &|\\
\verb|    x.^.y is rational|\\
\verb|proof|\\
\verb|  set w = |$\surd$\verb|2;|\\
\verb|  H1: w is irrational by INT_2:44,T1;|\\
\verb|  w>0 by AXIOMS:22,SQUARE_1:84;|\\
\verb|  then (w.^.w).^.w = w.^.(w|$\bullet$\verb|w) by POWER:38|\\
\verb|    .= w.^.(w|${}^2$\verb|) by SQUARE_1:58|\\
\verb|    .= w.^.2 by SQUARE_1:88|\\
\verb|    .= w|${}^2$\verb| by POWER:53|\\
\verb|    .= 2 by SQUARE_1:88;|\\
\verb|  then H2: (w.^.w).^.w is rational by RAT_1:8;|\\
\verb|  per cases;|\\
\verb|  suppose H3: w.^.w is rational;|\\
\verb|    take w, w;|\\
\verb|    thus thesis by H1,H3;|\\
\verb|  suppose H4: w.^.w is irrational;|\\
\verb|    take w.^.w, w;|\\
\verb|    thus thesis by H1,H2,H4;|\\
\verb|end;|
\end{verse}

(Note that Mizar uses `high ASCII'
characters, like `$\surd$', `$\bullet$' and `${}^2$'
which in the DOS character set have ASCII codes 251, 249 and 253.) 
Various elements in this example will be discussed below.

Mizar statements are those of the language of first order
logic (using the keywords `\verb|contradiction|', `\verb|not|', `\verb|&|', `\verb|or|',
`\verb|implies|', `\verb|iff|', `{\tt for }{\ldots} {\tt holds}' and `{\tt ex }{\ldots} {\tt st}').  The atomic
formulas of this language either are instances of predicates
(often written as an infix operator, with `\verb|=|' being one of the
most important), or statements stating that an expression `\verb|is|' a
type or adjective.

The only slight deviation from this is that a combination of a
universal quantification and an implication is usually not
written as:

\begin{verse}
\verb|for |{\it variable\/}\verb| holds (|{\it statement\/}\verb| implies |{\it statement\/}\verb|)|
\end{verse}

\noindent
but as:

\begin{verse}
\verb|for |{\it variable\/}\verb| st |{\it statement\/}\verb| holds |{\it statement\/}
\end{verse}

A source of confusion might be that Mizar has both `\verb|&|' versus
`\verb|and|' and `\verb|st|' versus `{\tt such that}'.  The first variants are
syntax of first order formulas, the second variants are keywords that are part of
Mizar statements.

Another `duplication' is that Mizar has
defined `\verb|func|' functions (Mizar calls those defined operations
`functors'), versus functions in the underlying set theory (sets
of Kuratowski pairs).  An application of the first kind of
function is written \verb|f(x)| while that of the second kind is \verb|f.x|
(with an infix dot operator).

A third such `duplication' is between `{\tt x $\in$ X}'
and `{\tt x is Element of X}'.  The first is the primitive binary predicate from set
theory, the second is a typing statement (saying that `\verb|x|' has type
`{\tt Element of X}').  For each set, `{\tt Element of}' gives
the type of its elements.
For instance: `\verb|REAL|' is a
set, but `\verb|Real|' which is defined to be `{\tt Element of REAL}'
is a type.  So it is `{\tt x $\in$ REAL}', but `{\tt x is Real}' or
`{\tt x is Element of REAL}'.

A Mizar proof consists of a list of proof steps.  Such a proof
step basically has the shape:

\begin{verse}
{\it label\/}\verb|: |{\it statement\/}\verb| by |{\it labels\/}\verb|;|
\end{verse}

For instance, an example of a Mizar proof step is:

\begin{verse}
\verb|H1: w is irrational by INT_2:44,T1;|
\end{verse}

Here the statement is `{\tt w is irrational}', it's labeled `\verb|H1|',
and it's a consequence of the statements labeled `\verb|INT_2:44|'
and `\verb|T1|', which are:

\begin{verse}
\verb|:: INT_2:44|\\
\verb|  2 is prime|
\end{verse}

\noindent
(the 44th theorem from article `\verb|INT_2|') and:

\begin{verse}
\verb|T1: p is prime implies sqrt p is irrational|
\end{verse}

\noindent
(which was proved earlier in the same file).

A label in the list after the `\verb|by|' keyword either is a label
from an earlier theorem or proof step in the same file, or it's
a reference to a theorem from a different Mizar article.  In the
latter case it looks like:

\begin{verse}
{\it article name\/}\verb|:|{\it sequence number\/}
\end{verse}

\noindent
(so while `local' references are by name, `outside' references
are by number).  One can look up these sequence numbers by
browsing the `abstract' files of the library, which are the
articles in which automatically proofs have been removed and
sequence numbers have been inserted.

Instead of referring to the label of the immediately preceding
step, one may also prefix the proof step with the keyword
`\verb|then|'.  So:

\begin{verse}
\verb|A: |{\it statement\/}\verb| by |{\it labels\/}\verb|;|\\
\verb|B: |{\it next statement\/}\verb| by A,|{\it more labels\/}\verb|;|
\end{verse}

\noindent
can be written as:

\begin{verse}
{\it statement\/}\verb| by |{\it labels\/}\verb|;|\\
\verb|then B: |{\it next statement\/}\verb| by |{\it more labels\/}\verb|;|
\end{verse}

Apart from these kind of steps (called `diffuse' reasoning
steps) there are steps that relate to the statement that's being
proved (`skeleton' steps).  At each moment there is a `current'
statement that has to be proved: the skeleton steps transform
that statement.  For instance suppose that the statement to be
proved looks like:

\begin{verse}
\verb|A implies B & C|
\end{verse}

Then the following skeleton proves it, using the `\verb|assume|' and
`\verb|thus|' skeleton steps:

\begin{verse}
\verb|assume |{\it label\/}\verb|: A;|\\
{\it diffuse steps\/}\\
\verb|thus B by |{\it labels\/}\verb|;|\\
{\it more diffuse steps\/}\\
\verb|thus C by |{\it labels\/}\verb|;|
\end{verse}

After the `\verb|assume|' step the statement to be proved has been
reduced to \verb|B & C|.  And after the first `\verb|thus|' it has become
\verb|C|.

The combination `{\tt then thus}' isn't syntactically correct: it
is written as `\verb|hence|'.  So `\verb|hence|' means that the statement
follows from the previous step (`\verb|then|') and that it is part of
what was to be proved (`\verb|thus|').

So at each moment in a Mizar proof there's a statement that's
left to be proved.  This statement may be referred to by the
keyword `\verb|thesis|'.  Often a proof or subproof ends with `{\tt hence
thesis}' (the Mizar library contains this construction 36885
times).

The `\verb|assume|' and `\verb|thus|' steps correspond in the system of
natural deduction to implication introduction and conjunction
introduction.  Other skeleton steps are:

\begin{itemize}
\item{`\verb|let|'} for universal introduction:

\begin{verse}
\verb|let |{\it variable\/}\verb| be |{\it type\/}\verb|;|
\end{verse}

\item{`\verb|consider|'} for existential elimination:

\begin{verse}
\verb|consider |{\it variable\/}\verb| being |{\it type\/}\verb| such that |{\it properties\/}\\
\verb|  by |{\it labels\/}\verb|;|
\end{verse}

\noindent
(the statements referred to by the {\it labels\/} have to justify
the appropriate existential statement)

\item{`\verb|take|'} for existential introduction:

\begin{verse}
\verb|take |{\it expression\/}\verb|;|
\end{verse}

\item{`{\tt per cases}'} for disjunction elimination:

\begin{verse}
\verb|per cases by |{\it labels\/}\verb|;|\\
\verb|suppose |{\it label\/}\verb|: |{\it statement\/}\verb|;|\\
\verb|  |{\it proof for the first case\/}\\
\verb|suppose |{\it label\/}\verb|: |{\it another statement\/}\verb|;|\\
\verb|  |{\it proof for the second case\/}\\
{\it more cases\/}
\end{verse}

\end{itemize}

Not all natural deduction rules have a Mizar skeleton step for
a counterpart: some are handled as a diffuse step.

In Mizar a proof can contain subproofs.  The part of a proof
step of the form:

\begin{verse}
{\it \ldots\/}\verb| by |{\it labels\/}\verb|;|
\end{verse}

\noindent
is called its justification.  It is not full first order
provability, but some weaker variant that can be decided quickly
(approximately: in only one of the premises universal quantors
may be instantiated; on the other hand it's quite good at
reasoning from type information, at applying equalities, and at
deducing existential statements).  This `\verb|by|' justification
sometimes isn't sufficient: so a statement also may also be
justified by a full proof in the form:

\begin{verse}
{\it label\/}\verb|: |{\it statement\/}\\
\verb|proof|\\
\verb|  |{\it proof steps\/}\\
\verb|end;|
\end{verse}

Note that there is no semicolon after the {\it statement\/} (that
semicolon would count for an `empty' justification).  In the
case that a full proof like this is given, the statement can be
omitted with the `\verb|now| \ldots \verb|end|' construction:

\begin{verse}
{\it label\/}\verb|:|\\
\verb|now|\\
\verb|  |{\it proof steps\/}\\
\verb|end;|
\end{verse}

In that case the statement that is proved (that the {\it label\/}
refers to) is `calculated' from the proof.

Mizar also has support for equational reasoning.  One can
write:

\begin{verse}
{\it label\/}\verb|: |{\it expression\/}\verb| = |{\it expression\/}\verb| by |{\it labels\/}\\
\verb|  .= |{\it expression\/}\verb| by |{\it labels\/}\\
\verb|  |{\it more steps\/}\\
\verb|  .= |{\it expression\/}\verb| by |{\it labels\/}\verb|;|
\end{verse}

The transitivity of these equalities is handled automatically:
the {\it label\/} will refer to the equality of the initial and final
expressions.

And Mizar supports higher order statements.  When invoking
such a `\verb|scheme|' its name is not put after the keyword `\verb|by|' but
after the keyword `\verb|from|', and it takes arguments.  These
arguments are {\it not\/} the `higher order parameters' which are
between braces in the definition of the scheme (those are
determined automatically), but instead the `conditions' after
the `\verb|provided|'.

The \verb|scheme| for doing induction on natural numbers is defined
(in article `\verb|NAT_1|') by:

\begin{verse}
\verb|scheme Ind { P[Nat] } :|\\
\verb|  for k holds P[k]|\\
\verb|provided|\\
\verb|  A1: P[0] and|\\
\verb|  A2: for k st P[k] holds P[k+1]|\\
{\it 16 lines of proof omitted\/}
\end{verse}

\noindent
(the square brackets mean that P is a predicate: functions are
written with round brackets; even when such a parameter function
is a constant those brackets have to be written).  The `\verb|Ind|'
scheme then is applied like:

\begin{verse}
{\it label\/}\verb|: |{\it statement\/}\verb| from Ind(|{\it label\/}\verb|,|{\it label\/}\verb|);|
\end{verse}

\noindent
in which the two labels refer to the instances of the two
`\verb|provided|' statements that this scheme needs (which of course
are the base and induction step cases).


\section{Syntax}

Expressions in a Mizar text look rather mathematical.  This is
caused by two things: the Mizar library uses the high ASCII part
of the DOS character set (which contains lots of `mathematical'
symbols) and in Mizar-expressions various styles of operators
are allowed (prefix, postfix, infix and `bracket-like').

The Mizar lexical syntax isn't fixed.  In fact, a Mizar
article generally consists of two files: the article file (with
a name ending with `\verb|.miz|') and the vocabulary file (ending with
`\verb|.voc|'; which has to be in a subdirectory called `\verb|dict|' in order
for the system to be able to find it).  This last kind of file
presents lexical elements.  It contains both the `identifiers'
from the definitions as well as the operator symbols.  Such a
vocabulary file contains for each lexical element a line that
starts with a capital letter giving the lexical category of the
symbol (the symbols for functions, predicates, modes, etc. all
have {\it different\/} lexical categories), then the symbol itself and
then possibly a priority.

So the Mizar library really consists of a number of articles
together with a number of vocabularies.  The articles can be
browsed in source format, but the vocabularies are only present
in `compiled' form.  The program `{\tt findvoc -w}' is used to find
out from which vocabulary a specific symbol comes.  For instance
the command:

\begin{verse}
\verb|findvoc -w .|
\end{verse}

\noindent
has as output:

\begin{verse}
\verb|vocabulary: FUNC|\\
\verb|O.  100|
\end{verse}

\noindent
which tells us that `\verb|.|' is an operator symbol (at the lexical
level there's no difference between infix, prefix or postfix
operators, so it can be used in all three ways) from the
vocabulary `\verb|FUNC|' and that it has priority $100$ (if there are
multiple definitions of a `\verb|.|' operator they {\it all\/} have this
priority).

For the analysis of the expression:

\begin{verse}
\verb|f.x|
\end{verse}

\noindent
three aspects can be distinguished: the lexical analysis
(there are three tokens: `\verb|f|', `\verb|.|' and `\verb|x|'), the way the
expression has to be parsed (the pattern from:

\begin{verse}
\verb|reserve x for set;|\\
\verb|reserve f for Function;|\\
\verb|definition|\\
\verb|  let f,x;|\\
\verb|  func f.x -> set means|\\
\verb|:: FUNCT_1:def 4|\\
\verb|  [x,it] |$\in$\verb| f if x |$\in$\verb| dom f otherwise it = 0;|\\
\verb|end;|
\end{verse}

\noindent
is the one that applies here) and the `notion' that it refers
to (the `meaning' of the `\verb|.|' operator).  These three aspects
correspond exactly to the `\verb|vocabulary|', `\verb|notation|' and
`\verb|constructors|' directives in the `\verb|environ|' header of an
article.  So in order to be able to process this `\verb|f.x|'
expression correctly, the directives:

\begin{verse}
\verb|vocabulary FUNC;|\\
\verb|notation FUNCT_1;|\\
\verb|constructors FUNCT_1;|
\end{verse}

\noindent
have to be present.  Note that, although often the names of a
vocabulary and the article it belongs to are identical, this
need not be the case (here it's \verb|FUNC| versus \verb|FUNCT_1|): the
`name spaces' of article names and vocabulary names are
separate.

Although it's quite hard to get the `\verb|environ|' header of an
article right, these three directives are the ones that are most
difficult to understand.  The `\verb|theorems|', `\verb|schemes|' and
`\verb|clusters|' directives are straightforward: in order to be able
to use a theorem, scheme or cluster from an article, the name of
that article has to be present in the appropriate directive.

The `\verb|definitions|' directive is {\it only\/} about definitional
expansion (what in type theory is called `delta reduction'). 
This directive says that the Mizar system is allowed to `unfold'
all definitions from the articles that are listed.  The theorems
(with `\verb|def|' in front of the number) that stem from definitions
are {\it theorems\/}, and the relevant directive for them is the
`\verb|theorems|' directive.  The `\verb|definitions|' directive is used
rarely.

The `\verb|requirements|' directive currently has only one possible
instance:

\begin{verse}
\verb|requirements ARYTM;|
\end{verse}

It means that the Mizar system will `know' about natural
numbers and about some identities and inequalities between them.

For instance the inequality

\begin{verse}
\verb|1<>0;|
\end{verse}

\noindent
doesn't need any justification when the \verb|ARYTM| requirement is
present.

A Mizar operator can take more than two arguments, but in that
case brackets have to be around them and commas in between.  So
legal postfix operators are:

\begin{verse}
\verb|x f|\\
\verb|(x) f|\\
\verb|(x,y) f|\\
{\it \ldots\/}
\end{verse}

\noindent
and for instance a legal infix operator is:

\begin{verse}
\verb|(x,y) f (z,v,w)|
\end{verse}

Note that the `ordinary' function application notation fits
this para\-digm.

Function identifiers and operator symbols have type `\verb|O|' in a
vocabulary file.  In Mizar also bracket-like notation is
allowed: for this the vocabulary types `\verb|K|' and `\verb|L|' are present. 
Because `\verb|<*|' has type `\verb|K|' and `\verb|*>|' has type `\verb|L|' (both
from vocabulary `\verb|FINSEQ|'), the expression:

\begin{verse}
\verb|<* x *>|
\end{verse}

\noindent
is a legal pattern (it denotes a one element finite sequence).


\section{Types}\label{types}

Although the semantics of Mizar is untyped set theory (the
axioms of Mizar are the ZF axioms plus a rather strong axiom --
which implies the axiom of choice -- about the existence of
arbitrarily large unreachable cardinals), the language itself is
typed.  But the types are a property of the expressions of the
language, not of the objects (the sets) which those expressions
refer to, so the language is not based on `type theory'.  Types
are used to disambiguate expressions (operators can be
overloaded and are determined by the types of their arguments)
and for reasoning.

Mizar typings are either written as:

\begin{verse}
{\it variable\/}\verb| be |{\it type\/}
\end{verse}

\noindent
or as:

\begin{verse}
{\it variable\/}\verb| being |{\it type\/}
\end{verse}

\noindent
(in a `\verb|let|' one probably would use the first and in a `\verb|for|'
one would use the second: but both variants may be used
everywhere).

Mizar types are built from `modes' and `attributes'.  A Mizar
type is an instance of a mode (which is a parametrised type),
possibly prefixed with a number of adjectives (an adjective is
an attribute or the negation of an attribute).

For instance, in the type:

\begin{verse}
\verb|non empty Subset of NAT|
\end{verse}

\noindent
the mode `\verb|Subset|' is applied to the expression `\verb|NAT|' (which
denotes the set of natural numbers) giving the type
`{\tt Subset of NAT}'.  To this type then the adjective `{\tt non empty}' has been
added, which is the negation of the attribute `\verb|empty|'.

Every Mizar type has an ancestor type.  This leads to a
tree-like type hierarchy of which the root type is `\verb|Any|' (or its
synonym `\verb|set|').  At every node of this tree there is a `Boolean
algebra'-like structure given by the adjectives.  The Mizar
system knows how to `widen' types following this structure.

In Mizar it's possible to give an expression some explicit
type.  For this there is the `\verb|reconsider|' construction, which is
a variant of the `\verb|set|' statement.  The way to locally name an
expression in Mizar is:

\begin{verse}
\verb|set |{\it variable\/}\verb| = |{\it expression\/}\verb|;|
\end{verse}

After this, {\it variable\/} behaves like {\it expression\/} has been
substituted for it everywhere.  A `\verb|reconsider|' is like that,
only then the {\it expression\/} gets a different type.  It looks
like:

\begin{verse}
\verb|reconsider |{\it variable\/}\verb| = |{\it expression\/}\verb| as |{\it type\/}\\
\verb|  by |{\it labels\/}\verb|;|
\end{verse}

(Note that the `\verb|consider|' and `\verb|reconsider|' statements are not
related: the first uses an existential statement to find a new
object with some properties, the second `\verb|casts|' an already known
object given by an expression to some type.)

The type machinery of Mizar is rather well developed.  In
particular Mizar has so-called `clusters' to be able to
automatically deduce extra type information: clusters allow the
Mizar system to manipulate sets of adjectives.  There are three
kind of cluster definitions: the first kind states that some
combination of adjectives gives a non-empty type (this needs to
be known to the system, because Mizar types all have to be provably
non-empty), the second kind tells that some combination of
adjectives implies other adjectives, and the third kind tells
that an expression of some shape has some adjectives.

An example of the first kind of cluster (from article
`\verb|HIDDEN|') is:

\begin{verse}
\verb|definition|\\
\verb|  cluster non empty set;|\\
\verb|end;|
\end{verse}

\noindent
(there's no proof because `\verb|HIDDEN|' and `\verb|TARSKI|' are the two
`special' articles which supply the axiomatics of Mizar).  It
states that the type `{\tt non empty set}' is inhabited.  If this
cluster weren't known, something like:

\begin{verse}
\verb|let X be non empty set;|
\end{verse}

\noindent
wouldn't be allowed, because in that case the system wouldn't
know that `{\tt non empty set}' is a properly non-empty type.

An example of the second kind of cluster statement (from
`\verb|BINTREE1|') is:

\begin{verse}
\verb|definition|\\
\verb|  cluster binary -> finite-order Tree;|\\
{\it 28 lines of proof omitted\/}\\
\verb|end;|
\end{verse}

This says that every expression that has type `{\tt binary Tree}'
has the adjective `\verb|finite-order|' as well (so it really has the
more informative type `{\tt binary finite-order Tree}').

A third kind of cluster (from `\verb|ABIAN|'):

\begin{verse}
\verb|definition|\\
\verb|  let i be even Integer;|\\
\verb|  cluster i+1 -> odd;|\\
{\it 5 lines of proof omitted\/}\\
\verb|end;|
\end{verse}

This last kind of cluster is very powerful, because lots of
properties of expressions can be derived automatically with it,
but it sometimes significantly slows down the system.

Mizar has the `\verb|redefine|' statement, which means that an
operation can have multiple definitions in which all but the
first one have a `\verb|redefine|' keyword added.  Those redefinitions
may be underspecified (all other information is copied from the
original definition), they may be defined on a smaller set of
arguments, but they do have to be proved `compatible' with the
original definition.

This can be used to give the same operation multiple types. 
For instance because of (from `\verb|NAT_1|'):

\begin{verse}
\verb|reserve k,n for Nat;|\\
\verb|definition|\\
\verb|  let n,k;|\\
\verb|  redefine func n+k -> Nat;|\\
{\it 18 lines of proof omitted\/}\\
\verb|end;|
\end{verse}

\noindent
the Mizar system knows that the sum of two natural numbers
will be a natural number (because the `redefined' version of the
operation is syntactically selected when the arguments are
natural numbers: for that the articles in the `\verb|notation|'
directive have to be in the proper order) even although the
addition operation originally was defined for real numbers (and
in that definition has type \verb|Real|).  But because of the
`\verb|redefine|', although the redefinition has type \verb|Nat|, all existing
theorems about the original operation of type \verb|Real| still apply
for it as well.


\section{Semantics}

The semantics of Mizar is fairly straightforward.  Mizar is
about ZF style set theory with first order logic.

However, there is the subtlety of undefined expressions.  The
semantics of Mizar `solves' the problem of undefined expressions
in a way that leads to some unexpected properties.  Firstly it
means that types are {\it not\/} only `syntactic sugar' coding
predicates (instead they `mean' something on the level of the
semantics).  And secondly it means that the axiom of choice is
provable from the way Mizar implements first order logic.

A Mizar `\verb|func|' operation can have preconditions.  The proof
that the operation is well defined uses these preconditions. 
However, when {\it applying\/} such an operation there is no need to
prove that the preconditions hold: they may be false.  So, while
for instance a precondition of division is that the denominator
has to be unequal to zero, one is allowed to write expressions
like \verb|1/0|.

The semantics of Mizar doesn't tell anything about the result
of applying an operation for which the preconditions fail.  If
the preconditions are true, the defining statement from the
definition is guaranteed to hold; but when the preconditions are
false, you don't know anything.  So \verb|1/0| is an unknown object.  A
different way of looking at this is that the function that maps
Mizar expressions to their meaning isn't unique: on `undefined'
expressions it can take any value.

The one exception to this rule is that the {\it type\/} of an
undefined expression still has to apply.  So, although we don't
know what \verb|1/0| is, we {\it do\/} know that it has to be a real number
(as the division operation has type `\verb|Real|').  So the defining
statement (which is a predicate on the object that's being
defined) is not relevant when the preconditions fail, but the
type is.

This difference in semantical treatment of unary predicates
and types coding those predicates is clear from the following
example.  Let `{\tt some\-thing}' be some (irrelevant) statement.  Then
write:

\begin{verse}
\verb|reserve X for set;|
\end{verse}

\begin{verse}
\verb|definition|\\
\verb|  let X;|\\
\verb|  assume A: contradiction;|\\
\verb|  func choice(X) -> Element of X means|\\
\verb|:Def_choice: something;|\\
\verb|  correctness by A;|\\
\verb|end;|
\end{verse}

\begin{verse}
\verb|definition|\\
\verb|  let X;|\\
\verb|  assume A: contradiction;|\\
\verb|  func choice1(X) means|\\
\verb|:Def_choice1: it is Element of X & something;|\\
\verb|  correctness by A;|\\
\verb|end;|
\end{verse}

(Because the precondition is `\verb|contradiction|' of course these
operations are well defined whenever the preconditions hold.) 
The `\verb|choice|' and `\verb|choice1|' functions seem minor variations of
each other.  But because of the way the semantics treats
undefined expressions we can prove:

\begin{verse}
\verb|theorem AC:|\\
\verb|  choice(X) is Element of X;|
\end{verse}

\noindent
but we {\it can't\/} prove:

\begin{verse}
\verb|theorem AC1:|\\
\verb|  choice1(X) is Element of X|\\
\verb|proof|\\
\verb|  thus thesis by Def_choice1;|\\
\verb|::>            *4|\\
\verb|end;|
\end{verse}

\noindent
(The \verb|*4| line is the error message that the `\verb|mizf|' checker
inserts in the file, number \verb|4| meaning that the `\verb|by|' inference
doesn't hold.  It is explained by the Mizar checker as
`{\tt This inference is not accepted}'.)

Note that theorem `\verb|AC|' gives a `uniform' axiom of choice.  (The axiom of
choice also follows from Mizar's set-theoretical axioms,
but it clearly already is `hard wired'
in the way Mizar treats first order logic.)

The meaning of the type `{\tt Element of X}' when \verb|X| is an empty set,
is some unknown but non-empty class (all Mizar types are non-empty).
In Mizar the statement:

\begin{verse}
\verb|ex x st x is Element of |$\emptyset$\\
\end{verse}

\noindent
(stating that there exists some {\tt `Element of $\emptyset$'}) is provable
(`{\tt consider x be\-ing El\-e\-ment of $\emptyset$; take x;}').
But the seemingly contradictory statement:

\begin{verse}
\verb|not ex x st x |$\in$\verb| |$\emptyset$
\end{verse}

\noindent
is provable as well, because it's a theorem of ZF.  (This does {\it not\/}
mean that the semantics of Mizar isn't sound, but just that `{\tt Element of}' has
a strange interpretation.)  One would expect
the definition of the `\verb|Element|' mode (in `\verb|HIDDEN|') to have
precondition `{\tt X is non empty}', but this is not the case.

In order to `build' mathematical structures, Mizar also has
`\verb|struct|' types.  They are defined like:

\begin{verse}
\verb|struct(|{\it ancestor struct\/}\verb|) |{\it struct name\/}\verb| (#|\\
\verb|  |{\it field name\/}\verb| -> |{\it type\/}\verb|,|\\
\verb|  |{\it field name\/}\verb| -> |{\it type\/}\verb|,|\\
\verb|  |{\it more fields\/}\\
\verb|  |{\it field name\/}\verb| -> |{\it type\/}\\
\verb|#)|
\end{verse}

\noindent
(The `\verb|(#|' and `\verb|#)|' brackets may be replaced with high ASCII
characters looking like `\verb|<|$\!$\verb|<|' and `\verb|>|$\!$\verb|>|': in fact this
notation is the more common one.)

An object of such a \verb|struct| type is then written like:

\begin{verse}
{\it struct name\/}\verb| (# |{\it value\/}\verb|,|{\it value\/}\verb|, |{\it \ldots\/}\verb| |{\it value\/}\verb| #)|
\end{verse}

\noindent
and a field is selected from a \verb|struct| by:

\begin{verse}
\verb|the |{\it field name\/}\verb| of |{\it struct expression\/}
\end{verse}

As an example of a \verb|struct|, here is the way topological spaces
are introduced in Mizar (from articles `\verb|STRUCT_0|' and
`\verb|PRE_TOPC|'):

\begin{verse}
\verb|struct 1-sorted (#|\\
\verb|  carrier -> set|\\
\verb|#);|
\end{verse}

\begin{verse}
\verb|struct(1-sorted) TopStruct (#|\\
\verb|  carrier -> set,|\\
\verb|  topology -> Subset-Family of the carrier|\\
\verb|#);|
\end{verse}

\begin{verse}
\verb|definition|\\
\verb|  let IT be TopStruct;|\\
\verb|  attr IT is TopSpace-like means|\\
\verb|    the carrier of IT |$\in$\verb| the topology of IT &|\\
\verb|    (for a being Subset-Family of the carrier of IT|\\
\verb|      st a c= the topology of IT|\\
\verb|      holds union a |$\in$\verb| the topology of IT) &|\\
\verb|    (for a,b being Subset of the carrier of IT st|\\
\verb|      a |$\in$\verb| the topology of IT & b |$\in$\verb| the topology of IT|\\
\verb|      holds a |$\cap$\verb| b |$\in$\verb| the topology of IT); |\\
\verb|end;|
\end{verse}

\begin{verse}
\verb|definition|\\
\verb|  mode TopSpace is TopSpace-like TopStruct;|\\
\verb|end;|
\end{verse}

The {\it specific\/} semantics of structs in terms of the underlying
set theory is not really interesting: some ad hoc coding will do
the job (choosing some set for the field names and interpreting
the \verb|struct| as a partial function from that set will work). 
Because of the way \verb|struct| types widen, an object will also be of
a \verb|struct| type if it has {\it more\/} fields than is required by the
definition.  The adjective `\verb|strict|' means that such extra fields
should be absent.


\section{Comparison To Coq}

The Mizar system is quite dissimilar to systems from the LCF
tradition like Coq.  We here will compare Mizar specifically to
Coq, but a similar comparison holds to other LCF-like systems
like HOL, Nuprl, Isabelle, etc.

The most striking difference between Mizar and Coq is that
Mizar is a batch checker which checks a whole file at a time
(the `\verb|@proof|' keyword gives some control in this respect by
allowing one to suppress the checking of specific proofs), while
Coq is an interactive system (this is similar to the difference
in spirit between compiled and interpreted programming
languages).  One of the places that this shows is in the
readability of the formalizations: a Coq file is just a long
list of `commands', so it has a linear structure and the
commands aren't designed for readability, while a Mizar text has
much more structure and is quite accessible without having to
`run' the file.

Another difference is that Mizar doesn't have `proof objects':
the system doesn't reduce its correctness to the correctness of
a small `kernel' that only knows about a few primitives.  There
also is a difference in the kind of logic in the two systems:
Coq's kernel is based on `type theory' which naturally has a
constructive logic, while Mizar is very much a classical system.

The Mizar project has {\it more\/} automation than Coq and it has
{\it less\/} automation.  The step used most in Mizar is the `\verb|by|'
inference; in Coq the common tactics are more elementary than
that.  The `\verb|by|' inference knows how to reason with types, it is
able to use equalities and it's able to logically combine the
information from many statements (the maximum: 22 statements in
`\verb|GENEALG1|').  While it's not full first order inference its
power is close to the kind of reasoning steps a human would take
(the Mizar system has the `\verb|relinfer|' program to eliminate
superfluous steps, and running it shows that `\verb|by|' is more
powerful than one tends to expect).  So for the majority of the
steps Mizar is more powerful than Coq.  On the other hand, the
Coq system isn't `closed', it can be extended with arbitrarily
powerful `tactics'.  These tactics, like `\verb|Omega|' and `\verb|Ring|', are
able to solve involved domain specific tasks and don't have a
Mizar counterpart.  Also, the Coq system is able to `reflect' on
algorithms: it's able to state an algorithm {\it inside\/} the system,
to prove that it is correct, and then to execute it, making it
possible to extend the system `from within'.  This also is a
reason that Coq is, in a sense, more powerful than Mizar.

Another difference between Mizar and Coq is that Coq mainly
reasons backwards from the statement that is to be proved, while
Mizar reasons forwards.  Basically the Mizar `skeleton' steps
correspond to the Coq tactics and reduce the statement that's to
be proved, while the `diffuse' steps reason forward from already
known statements.  Most of the steps in a Mizar proof are
diffuse steps.

A difference that's not so much a difference between the
languages or systems, as well as a difference between the
projects, is that the Mizar project has given a big priority to
the development of a large and organized library.  The Mizar
system intentionally makes it hard to create projects of more
than a few files (it is possible, but the system gets slow),
stimulating Mizar users to submit their work for integration
into the Mizar library.  And the Mizar library is continuously
being reorganized and changed by the Mizar group (the `library
committee'), turning it into a structured and consistent whole. 
This wouldn't be possible if they didn't `own' the files.

Here's an example of a change that has been made to the Mizar
library at some time.  In the Mizar library the real numbers are
constructed from the rational numbers as Dedekind cuts.  But in
the construction of the set `\verb|REAL|' it `cuts out' the copy of the
rationals and `glues in' the `original' rationals (similarly the
integers are glued inside the rationals and the natural numbers
glued inside the integers).  That way the natural numbers are a
subset of the reals but also the natural numbers are the
{\it natural\/} natural numbers, i.e., the finite ordinals.  So the
real number $0$ is the natural number $0$ is the empty set.  This
cutting-and-pasting of sets of numbers is a `hack', but it also
is quite nice.  The complex numbers don't contain the real
numbers in this fashion yet, but a change like this `to put the
real numbers inside the complex numbers' has been planned.

So the Mizar library is significantly more well developed than
the Coq library.  For instance it already contains a full
construction of the real numbers (the Coq library only has the
real numbers axiomatically) with lots of properties proved.  (On
the other hand, the Mizar library currently doesn't yet contain
a definition of the rather elementary notion of `polynomial' so
it's not {\it that\/} rich yet.)  Also Mizar is much more mathematical
than Coq.  Mizar is primarily about abstract mathematics while
Coq has much more a focus on topics from computer science like
proving functional programs correct.

Yet another difference: Coq is much more `mainstream science'
than Mizar.  Mizar is an old-fashioned system that not many
people know (if we take the fair assumption that every Mizar
user has written an article for the Mizar library then there are
117 people in the world knowing Mizar), there is hardly any
documentation about it and it doesn't run on the usual platform
for this kind of system (which is a Sun running Unix).  On the
other hand Coq actively follows the theoretical developments
from the type theory community, it's well known, has many users,
is well documented and is available for all major platforms.

John Harrrison has written a `Mizar mode' for HOL.  To create
a Mizar interface for a LCF style prover like HOL or Coq, one
has to write a tactic that is able to do `\verb|by|' inference
(Harrison decided to implement full first order provability,
which is more powerful but less efficient), and one has to write
a parser for the Mizar syntax.  Because the semantics and the
type systems of Mizar and Coq are not the same, there are
differences there to be bridged too.  Having a system that
combines the strengths of Mizar and Coq will be nice (it will be
a `Mizar' that has proof objects) but doing it by `enhancing'
Coq will be rather inelegant (there will be duplications of
functionality) and inefficient.  And really, from the point of
view of the mathematically inclined user Mizar already contains
everything that one needs.


\begin{thebibliography}{1}

\bibitem{gie:hof:kei:law:mis:sco:80}
G.~Gierz, K.H. Hofmann, K.~Keimel, J.D. Lawson, M.~Mislove, and D.S. Scott.
\newblock {\em A Compendium of Continuous Lattices}.
\newblock Springer-Verlag, Berlin, Heidelberg, New York, 1980.

\bibitem{kot:mad:kor:92}
J.~Kotowicz, B.~Madras, and M.~Korolkiewicz.
\newblock Basic notation of universal algebra.
\newblock {\em Journal of Formalized Mathematics}, 4, 1992.

\bibitem{muz:93}
M.~Muzalewski.
\newblock {\em An Outline of PC Mizar}.
\newblock Fondation Philippe le Hodey, Brussels, 1993.

\end{thebibliography}


\appendix
\section{How To Run Mizar}

Select three directories:

\begin{itemize}
\item {\it distdir\/}: to unzip the Mizar distribution in
\item {\it mizardir\/}: for the installed Mizar system
\item {\it workdir\/}: for your articles
\end{itemize}

\noindent
The recommended choice for {\it mizardir\/}
is `{\tt C:\verb|\|MIZAR}', although everything works fine if you
put it elsewhere.

To install the Mizar system, get the zipped installation files from:

\begin{verse}
{\tt <ftp://ftp.mizar.org/ver{\it version\/}/disks.zip/>}
\end{verse}

\noindent
(the `{\it version\/}' of the system described in this note is `\verb|5-3.07|').
Unzip them all inside {\it distdir\/}.  Then run the \verb|install| command:

\begin{verse}
{\tt {\it distdir\/}\verb|\|install {\it distdir\/}\verb|\| {\it mizardir\/}}
\end{verse}

\noindent
This installs everything apart from the sources of the Mizar library in
`{\tt {\it mizar\-dir\/}\verb|\|MML}'.  These sources are really not very important (not even
for reference to the library: the abstracts in `{\tt {\it mizardir\/}\verb|\|ABSTR}' are
much more suitable for that).  To unpack the sources of the Mizar library too, run the
`{\tt FM{\it number\/}.EXE}' files from
{\it distdir\/} inside `{\tt {\it mizardir\/}\verb|\|MML}'.

Now add:

\begin{verse}
{\tt set mizfiles={\it mizardir\/}}
\end{verse}

\noindent
to the appropriate `{\tt AUTOEXEC.BAT}' file, add {\it mizardir\/} to the
DOS search \verb|PATH|, and the installation will be complete.

To write an article create two subdirectories:
\begin{itemize}
\item {\tt {\it workdir\/}\verb|\|TEXT}
\item {\tt {\it workdir\/}\verb|\|DICT}
\end{itemize}
Supposing the name of the article you'll be going
to work on is `\verb|FOO|', then create:
\begin{itemize}
\item {\tt {\it workdir\/}\verb|\|TEXT\verb|\|FOO.MIZ}
\item {\tt {\it workdir\/}\verb|\|DICT\verb|\|FOO.VOC}
\end{itemize}
which are your article and vocabulary files.

To check the article for correctness, \verb|cd| to {\it workdir\/} and run the
command:

\begin{verse}
\verb|mizf text\foo|
\end{verse}

\noindent
(the \verb|mizf| checker will add the suffix `\verb|.miz|' by itself).
This will check the file, and will put the error messages {\it inside\/} the checked file
(so it might be necessary to close the file in the editor before running the `\verb|mizf|'
command).


\section{Grammar}\label{grammar}

\begin{flushleft}

{\it Mizar-Article\/} =\\*
\quad `\verb|environ|'\\*
\quad\quad \{ `\verb|vocabulary|' {\it File-Name-List\/} `\verb|;|' $|$\\*
\quad\quad\quad ( `\verb|notation|' $|$\\*
\quad\quad\quad\quad `\verb|constructors|' $|$\\*
\quad\quad\quad\quad `\verb|clusters|' $|$\\*
\quad\quad\quad\quad `\verb|definitions|' $|$\\*
\quad\quad\quad\quad `\verb|theorems|' $|$\\*
\quad\quad\quad\quad `\verb|schemes|' ) {\it File-Name-List\/} `\verb|;|' $|$\\*
\quad\quad\quad `\verb|requirements|' {\it File-Name-List\/} `\verb|;|' \}\\*
\quad ( `\verb|begin|' \{ {\it Text-Item\/} \} ) \{ \ldots \} .\smallskip

{\it Text-Item\/} =\\*
\quad `\verb|reserve|' {\it Identifier-List\/} `\verb|for|' {\it Type-Expression-List\/} `\verb|;|' $|$\\
\quad `\verb|definition|'\\*
\quad\quad \{ {\it Definition-Item\/} \}\\*
\quad\quad [ `\verb|redefine|' \{ {\it Definition-Item\/} \} ]\\*
\quad\quad `\verb|end|' `\verb|;|' $|$\\
\quad {\it Structure-Definition\/} $|$\\
\quad `\verb|theorem|' {\it Proposition\/} {\it Justification\/} `\verb|;|' $|$\\
\quad [ `\verb|scheme|' ] {\it Identifier\/}\\*
\quad\quad `\verb|{|' ( {\it Identifier-List\/} `\verb|[|' {\it Type-Expression-List\/} `\verb|]|' $|$\\*
\quad\quad\quad\quad {\it Identifier-List\/} `\verb|(|' {\it Type-Expression-List\/} `\verb|)|' `\verb|->|' {\it Type-Expression\/} )\\*
\quad\quad\quad\quad \{ `\verb|,|' \ldots \} `\verb|}|'\\*
\quad\quad `\verb|:|' {\it Formula-Expression\/}\\*
\quad\quad [ `\verb|provided|' {\it Proposition\/} \{ `\verb|and|' \ldots \} ]\\*
\quad\quad {\it Justification\/} `\verb|;|' $|$\\
\quad {\it Auxiliary-Item\/} $|$\\
\quad `\verb|canceled|' [ {\it Numeral\/} ] `\verb|;|' .\smallskip

{\it Definition-Item\/} =\\*
\quad {\it Assumption\/} $|$\\
\quad {\it Auxiliary-Item\/} $|$\\
\quad {\it Structure-Definition\/} $|$\\
\quad `\verb|mode|' \verb|M|{\it -Symbol\/} [ `\verb|of|' {\it Identifier-List\/} ]\\*
\quad\quad ( [ `\verb|->|' {\it Type-Expression\/} ] [ `\verb|means|' {\it Definiens\/} ] `\verb|;|'\\*
\quad\quad\quad\quad {\it Correctness-Conditions\/} $|$\\*
\quad\quad\quad `\verb|is|' {\it Type-Expression\/} `\verb|;|' )\\*
\quad\quad \{ `\verb|synonym|' \verb|M|{\it -Symbol\/} [ `\verb|of|' {\it Identifier-List\/} ] `\verb|;|' \} $|$\\
\quad `\verb|func|' {\it Functor-Pattern\/} [ `\verb|->|' {\it Type-Expression\/} ]\\*
\quad\quad [ ( `\verb|means|' $|$ `\verb|equals|' ) {\it Definiens\/} ] `\verb|;|'\\*
\quad\quad {\it Correctness-Conditions\/}\\*
\quad\quad \{ `\verb|commutativity|' {\it Justification\/} `\verb|;|' \}\\*
\quad\quad \{ `\verb|synonym|' {\it Functor-Pattern\/} `\verb|;|' \} $|$\\
\quad `\verb|pred|' {\it Predicate-Pattern\/} [ `\verb|means|' {\it Definiens\/} ] `\verb|;|'\\*
\quad\quad {\it Correctness-Conditions\/}\\*
\quad\quad \{ `\verb|symmetry|' {\it Justification\/} `\verb|;|' $|$\\*
\quad\quad\quad `\verb|connectedness|' {\it Justification\/} `\verb|;|' $|$\\*
\quad\quad\quad `\verb|reflexivity|' {\it Justification\/} `\verb|;|' $|$\\*
\quad\quad\quad `\verb|irreflexivity|' {\it Justification\/} `\verb|;|' \}\\*
\quad\quad \{ ( `\verb|synonym|' $|$ `\verb|antonym|' ) {\it Predicate-Pattern\/} `\verb|;|' \} $|$\\
\quad `\verb|attr|' {\it Identifier\/} `\verb|is|' \verb|V|{\it -Symbol\/} `\verb|means|' {\it Definiens\/} `\verb|;|'\\*
\quad\quad [ {\it Correctness-Conditions\/} ]\\*
\quad\quad \{ ( `\verb|synonym|' $|$ `\verb|antonym|' )\\*
\quad\quad\quad ( {\it Identifier\/} `\verb|is|' \verb|V|{\it -Symbol\/} $|$ {\it Predicate-Pattern\/} ) `\verb|;|' \} $|$\\
\quad `\verb|canceled|' [ {\it Numeral\/} ] $|$\\
\quad `\verb|cluster|' {\it Adjective-Cluster\/} {\it Type-Expression\/} `\verb|;|' {\it Correctness-Conditions\/} $|$\\
\quad `\verb|cluster|' {\it Adjective-Cluster\/} `\verb|->|' {\it Adjective-Cluster\/} {\it Type-Expression\/} `\verb|;|'\\*
\quad\quad {\it Correctness-Conditions\/} $|$\\
\quad `\verb|cluster|' {\it Term-Expression\/} `\verb|->|' {\it Adjective-Cluster\/} `\verb|;|'\\*
\quad\quad {\it Correctness-Conditions\/} .\smallskip

{\it Structure-Definition\/} =\\*
\quad `\verb|struct|' [ `\verb|(|' {\it Type-Expression-List\/} `\verb|)|' ] \verb|G|{\it -Symbol\/} [ `\verb|over|' {\it Identifier-List\/} ]\\*
\quad\quad `\verb|(#|' ( \verb|U|{\it -Symbol\/} \{ `\verb|,|' \ldots \} `\verb|->|' {\it Type-Expression\/} ) \{ `\verb|,|' \ldots \} `\verb|#)|' `\verb|;|' .\smallskip

{\it Definiens\/} =\\*
\quad [ `\verb|:|' {\it Identifier\/} `\verb|:|' ] ( {\it Formula-Expression\/} $|$ {\it Term-Expression\/} ) $|$\\
\quad [ `\verb|:|' {\it Identifier\/} `\verb|:|' ]\\*
\quad\quad ( ( {\it Formula-Expression\/} $|$ {\it Term-Expression\/} ) `\verb|if|' {\it Formula-Expression\/} )\\*
\quad\quad \{ `\verb|,|' \ldots \}\\*
\quad\quad [ `\verb|otherwise|' ( {\it Formula-Expression\/} $|$ {\it Term-Expression\/} ) ] .\smallskip

{\it Functor-Pattern\/} =\\*
\quad [ {\it Functor-Loci\/} ] \verb|O|{\it -Symbol\/} [ {\it Functor-Loci\/} ] $|$\\
\quad \verb|K|{\it -Symbol\/} {\it Identifier-List\/} \verb|L|{\it -Symbol\/} .\smallskip

{\it Functor-Loci\/} =\\*
\quad {\it Identifier\/} $|$\\
\quad `\verb|(|' {\it Identifier-List\/} `\verb|)|' .\smallskip

{\it Predicate-Pattern\/} = [ {\it Identifier-List\/} ] \verb|R|{\it -Symbol\/} [ {\it Identifier-List\/} ] .\smallskip

{\it Correctness-Conditions\/} =\\*
\quad \{ `\verb|existence|' {\it Justification\/} `\verb|;|' $|$\\*
\quad\quad `\verb|uniqueness|' {\it Justification\/} `\verb|;|' $|$\\*
\quad\quad `\verb|coherence|' {\it Justification\/} `\verb|;|' $|$\\*
\quad\quad `\verb|compatibility|' {\it Justification\/} `\verb|;|' $|$\\*
\quad\quad `\verb|consistency|' {\it Justification\/} `\verb|;|' \}\\*
\quad [ `\verb|correctness|' {\it Justification\/} `\verb|;|' ] .\smallskip

{\it Justification\/} =\\*
\quad {\it Simple-Justification\/} $|$\\
\quad ( `\verb|proof|' $|$ `\verb|@proof|' ) {\it Reasoning\/} `\verb|end|' .\smallskip

{\it Reasoning\/} =\\*
\quad \{ {\it Reasoning-Item\/} \}\\*
\quad\quad [ `\verb|per|' `\verb|cases|' {\it Simple-Justification\/} `\verb|;|'\\*
\quad\quad ( ( `\verb|case|' ( {\it Proposition\/} $|$ {\it Conditions\/} ) `\verb|;|' \{ {\it Reasoning-Item\/} \} )\\*
\quad\quad\quad\quad \{ \ldots \} $|$\\*
\quad\quad\quad ( `\verb|suppose|' ( {\it Proposition\/} $|$ {\it Conditions\/} ) `\verb|;|' \{ {\it Reasoning-Item\/} \} )\\*
\quad\quad\quad\quad \{ \ldots \} ) ] .\smallskip

{\it Reasoning-Item\/} =\\*
\quad {\it Auxiliary-Item\/} $|$\\
\quad {\it Assumption\/} $|$\\
\quad ( `\verb|thus|' $|$ `\verb|hence|' ) {\it Statement\/} $|$\\
\quad `\verb|take|' ( {\it Term-Expression\/} $|$ {\it Identifier\/} `\verb|=|' {\it Term-Expression\/} ) \{ `\verb|,|' \ldots \} `\verb|;|' .\smallskip

{\it Auxiliary-Item\/} =\\*
\quad [ `\verb|then|' ] {\it Statement\/} $|$\\
\quad `\verb|set|' ( {\it Identifier\/} `\verb|=|' {\it Term-Expression\/} ) \{ `\verb|,|' \ldots \} `\verb|;|' $|$\\
\quad `\verb|deffunc|' {\it Identifier\/} `\verb|(|' [ {\it Type-Expression-List\/} ] `\verb|)|' `\verb|=|' {\it Term-Expression\/} $|$\\
\quad `\verb|defpred|' {\it Identifier\/} `\verb|[|' [ {\it Type-Expression-List\/} ] `\verb|]|' `\verb|means|'\\*
\quad\quad {\it Formula-Expression\/} .\smallskip

{\it Assumption\/} =\\*
\quad ( `\verb|let|' $|$ `\verb|given|' ) {\it Qualified-Variables\/} [ `\verb|such|' {\it Conditions\/} ] `\verb|;|' $|$\\
\quad `\verb|assume|' ( {\it Proposition\/} $|$ {\it Conditions\/} ) `\verb|;|' .\smallskip

{\it Statement\/} =\\*
\quad [ `\verb|then|' ]\\*
\quad\quad ( {\it Proposition\/} {\it Justification\/} `\verb|;|' $|$\\*
\quad\quad\quad `\verb|consider|' {\it Qualified-Variables\/} [ `\verb|such|' {\it Conditions\/} ]\\*
\quad\quad\quad\quad {\it Simple-Justification\/} `\verb|;|' $|$\\*
\quad\quad\quad `\verb|reconsider|'\\*
\quad\quad\quad\quad ( {\it Identifier\/} `\verb|=|' {\it Term-Expression\/} $|$ {\it Identifier\/} ) \{ `\verb|,|' \ldots \}\\*
\quad\quad\quad\quad `\verb|as|' {\it Type-Expression\/} {\it Simple-Justification\/} `\verb|;|' $|$\\*
\quad\quad\quad {\it Term-Expression\/} `\verb|=|' {\it Term-Expression\/} {\it Simple-Justification\/}\\*
\quad\quad\quad\quad `\verb|.=|' ( {\it Term-Expression\/} {\it Simple-Justification\/} ) \{ `\verb|.=|' \ldots \} ) $|$\\
\quad [ {\it Identifier\/} `\verb|:|' ] `\verb|now|' {\it Reasoning\/} `\verb|end|' `\verb|;|' .\smallskip

{\it Simple-Justification\/} =\\*
\quad [ `\verb|by|' {\it Reference\/} \{ `\verb|,|' \ldots \} ] $|$\\
\quad `\verb|from|' {\it Identifier\/} [ `\verb|(|' {\it Reference\/} \{ `\verb|,|' \ldots \} `\verb|)|' ] .\smallskip

{\it Reference\/} =\\*
\quad {\it Identifier\/} $|$\\
\quad {\it File-Name\/} `\verb|:|' ( {\it Numeral\/} $|$ `\verb|def|' {\it Numeral\/} ) \{ `\verb|,|' \ldots \} .\smallskip

{\it Conditions\/} = `\verb|that|' {\it Proposition\/} \{ `\verb|and|' \ldots \} .\smallskip

{\it Proposition\/} = [ {\it Identifier\/} `\verb|:|' ] {\it Formula-Expression\/} .\smallskip

{\it Formula-Expression\/} =\\*
\quad `\verb|(|' {\it Formula-Expression\/} `\verb|)|' $|$\\
\quad [ {\it Term-Expression-List\/} ] \verb|R|{\it -Symbol\/} [ {\it Term-Expression-List\/} ] $|$\\
\quad {\it Identifier\/} [ `\verb|[|' {\it Term-Expression-List\/} `\verb|]|' ] $|$\\
\quad {\it Term-Expression\/} `\verb|is|' \{ [ `\verb|non|' ] \verb|V|{\it -Symbol\/} \} $|$\\
\quad {\it Term-Expression\/} `\verb|is|' {\it Type-Expression\/} $|$\\
\quad {\it Quantified-Formula-Expression\/} $|$\\
\quad {\it Formula-Expression\/} `\verb|&|' {\it Formula-Expression\/} $|$\\
\quad {\it Formula-Expression\/} `\verb|or|' {\it Formula-Expression\/} $|$\\
\quad {\it Formula-Expression\/} `\verb|implies|' {\it Formula-Expression\/} $|$\\
\quad {\it Formula-Expression\/} `\verb|iff|' {\it Formula-Expression\/} $|$\\
\quad `\verb|not|' {\it Formula-Expression\/} $|$\\
\quad `\verb|contradiction|' $|$\\
\quad `\verb|thesis|' .\smallskip

{\it Quantified-Formula-Expression\/} =\\*
\quad `\verb|for|' {\it Qualified-Variables\/} [ `\verb|st|' {\it Formula-Expression\/} ]\\*
\quad\quad ( `\verb|holds|' {\it Formula-Expression\/} $|$ {\it Quantified-Formula-Expression\/} ) $|$\\
\quad `\verb|ex|' {\it Qualified-Variables\/} `\verb|st|' {\it Formula-Expression\/} .\smallskip

{\it Qualified-Variables\/} =\\*
\quad {\it Identifier-List\/} $|$\\
\quad ( {\it Identifier-List\/} ( `\verb|being|' $|$ `\verb|be|' ) {\it Type-Expression\/} ) \{ `\verb|,|' \ldots \}\\*
\quad\quad [ `\verb|,|' {\it Identifier-List\/} ] .\smallskip

{\it Type-Expression\/} =\\*
\quad `\verb|(|' {\it Type-Expression\/} `\verb|)|' $|$\\
\quad {\it Adjective-Cluster\/} \verb|M|{\it -Symbol\/} [ `\verb|of|' {\it Term-Expression-List\/} ] $|$\\
\quad {\it Adjective-Cluster\/} \verb|G|{\it -Symbol\/} [ `\verb|over|' {\it Term-Expression-List\/} ] .\smallskip

{\it Adjective-Cluster\/} = \{ [ `\verb|non|' ] \verb|V|{\it -Symbol\/} \} .\smallskip

{\it Term-Expression\/} =\\*
\quad `\verb|(|' {\it Term-Expression\/} `\verb|)|' $|$\\
\quad [ {\it Arguments\/} ] \verb|O|{\it -Symbol\/} [ {\it Arguments\/} ] $|$\\
\quad \verb|K|{\it -Symbol\/} {\it Term-Expression-List\/} \verb|L|{\it -Symbol\/} $|$\\
\quad {\it Identifier\/} `\verb|(|' [ {\it Term-Expression-List\/} ] `\verb|)|' $|$\\
\quad \verb|G|{\it -Symbol\/} `\verb|(#|' {\it Term-Expression-List\/} `\verb|#)|' $|$\\
\quad {\it Identifier\/} $|$\\
\quad `\verb|{|' {\it Term-Expression\/}\\*
\quad\quad\quad [ ( `\verb|where|' {\it Identifier-List\/} `\verb|is|' {\it Type-Expression\/} ) \{ `\verb|,|' \ldots \} ]\\*
\quad\quad\quad `\verb|:|' {\it Formula-Expression\/} `\verb|}|' $|$\\
\quad {\it Numeral\/} $|$\\
\quad {\it Term-Expression\/} `\verb|qua|' {\it Type-Expression\/} $|$\\
\quad `\verb|the|' \verb|U|{\it -Symbol\/} `\verb|of|' {\it Term-Expression\/} $|$\\
\quad `\verb|the|' \verb|U|{\it -Symbol\/} $|$\\
\quad `\verb|$1|' $|$ `\verb|$2|' $|$ `\verb|$3|' $|$ `\verb|$4|' $|$ `\verb|$5|' $|$ `\verb|$6|' $|$ `\verb|$7|' $|$ `\verb|$8|' $|$\\
\quad `\verb|it|' .\smallskip

{\it Arguments\/} =\\*
\quad {\it Term-Expression\/} $|$\\
\quad `\verb|(|' {\it Term-Expression-List\/} `\verb|)|' .\bigskip


{\it File-Name-List\/} = {\it File-Name\/} \{ `\verb|,|' \ldots \} .\smallskip

{\it Identifier-List\/} = {\it Identifier\/} \{ `\verb|,|' \ldots \} .\smallskip

{\it Type-Expression-List\/} = {\it Type-Expression\/} \{ `\verb|,|' \ldots \} .\smallskip

{\it Term-Expression-List\/} = {\it Term-Expression\/} \{ `\verb|,|' \ldots \} .

\end{flushleft}


\section{Axioms}

Here are the undefined notions and axioms of the Mizar system:
everything in the Mizar library is defined and proved from just this.
(This is the content of articles `\verb|HIDDEN|' and `\verb|TARSKI|'.
Axiom `\verb|TARSKI:8|' was omitted because it's derivable from `{\tt TARSKI:def 5}'.)

\begin{flushleft}\footnotesize\smallskip

\verb|definition mode Any; synonym set; end;|\\
\verb|reserve x,y,z,u for Any, N,M,X,Y,Z for set;|
\smallskip

\verb|definition let x,y; pred x = y; reflexivity; symmetry; antonym x <> y; end;|
\smallskip

\verb|definition let x,X; pred x |$\in$\verb| X; antisymmetry; end;|
\smallskip

\verb|definition let X; attr X is empty; end;|\\
\verb|definition cluster empty set; cluster non empty set; end;|
\smallskip

\verb|definition func |$\emptyset$\verb| -> empty set; end;|
\smallskip

\verb|definition let X; mode Element of X; end;|
\smallskip

\verb|definition let X; func bool X -> non empty set; end;|
\smallskip

\verb|definition let X; mode Subset of X is Element of bool X; end;|
\smallskip

\verb|definition let X be non empty set; cluster non empty Subset of X; end;|
\smallskip

\verb|definition let X,Y; pred X c= Y; reflexivity; end;|
\smallskip

\verb|definition let D be non empty set, X be non empty Subset of D;|\\
\verb|  redefine mode Element of X -> Element of D;|\\
\verb|end;|
\bigskip

\verb|theorem (for x holds x |$\in$\verb| X iff x |$\in$\verb| Y) implies X = Y;|
\smallskip

\verb|definition let y; func {y} -> set means x |$\in$\verb| it iff x = y;|\\
\verb|  let z; func {y,z} -> set means x |$\in$\verb| it iff x = y or x = z;|\\
\verb|  commutativity;|\\
\verb|end;|\\
\verb|definition let y; cluster {y} -> non empty;|\\
\verb|  let z; cluster {y,z} -> non empty;|\\
\verb|end;|
\smallskip

\verb|definition let X,Y; redefine pred X c= Y means x |$\in$\verb| X implies x |$\in$\verb| Y; end;|
\smallskip

\verb|definition let X;|\\
\verb|  func union X -> set means x |$\in$\verb| it iff ex Y st x |$\in$\verb| Y & Y |$\in$\verb| X;|\\
\verb|end;|
\smallskip

\verb|theorem X = bool Y iff for Z holds Z |$\in$\verb| X iff Z c= Y;|
\smallskip

\verb|theorem x |$\in$\verb| X implies ex Y st Y |$\in$\verb| X & not ex x st x |$\in$\verb| X & x |$\in$\verb| Y;|
\smallskip

\verb|scheme Fraenkel {A()->set, P[Any,Any]}:|\\
\verb|    ex X st for x holds x |$\in$\verb| X iff ex y st y |$\in$\verb| A() & P[y,x]|\\
\verb|  provided|\\
\verb|    for x,y,z st P[x,y] & P[x,z] holds y = z;|
\smallskip

\verb|definition let x,y; func [x,y] equals {{x,y},{x}}; end;|\\
%\verb|theorem [x,y] = {{x,y},{x}};|
\smallskip

\verb|definition let X,Y;|\\
\verb|  pred X |$\approx$\verb| Y means ex Z st|\\
\verb|    (for x st x |$\in$\verb| X ex y st y |$\in$\verb| Y & [x,y] |$\in$\verb| Z) &|\\
\verb|    (for y st y |$\in$\verb| Y ex x st x |$\in$\verb| X & [x,y] |$\in$\verb| Z) &|\\
\verb|    for x,y,z,u st [x,y] |$\in$\verb| Z & [z,u] |$\in$\verb| Z holds x = z iff y = u;|\\
\verb|end;|
\smallskip

\verb|:: |{\it Axiom der unerreichbaren Mengen\/}\\
\verb|theorem ex M st N |$\in$\verb| M &|\\
\verb|  (for X,Y holds X |$\in$\verb| M & Y c= X implies Y |$\in$\verb| M) &|\\
\verb|  (for X holds X |$\in$\verb| M implies bool X |$\in$\verb| M) &|\\
\verb|  (for X holds X c= M implies X |$\approx$\verb| M or X |$\in$\verb| M);|\\

\end{flushleft}


\newcounter{lineno}
\newcommand{\lineno}{\addtocounter{lineno}{1}%
  \makebox[0pt][l]{%
    %\hspace{\textwidth}\qquad
    \makebox[0pt][r]{\tiny\bf\thelineno
    \quad
    }}%
  %\quad
  }
\newcommand{\lineinc}{\addtocounter{lineno}{1}}

\section{Complete Example}

Here is an example of a complete Mizar text: it's the article
`\verb|UNIALG_1|' from the Mizar library, article number 303
by Jaros{\l}aw Kotowicz, Beata Madras and
Ma{\l}gorzata Korolkiewicz \cite{kot:mad:kor:92}.  It defines the type
`{\tt Univer\-sal\verb|_Algebra|}' (together
with the notions of `\verb|arity|' and `\verb|signature|')
which is the Mizar implementation of
`one-sorted algebras' from the theory of universal algebra.

We both give here the
`abstract' file `\verb|UNIALG_1.ABS|'
as well as the full Mizar article `\verb|UNIALG_1.MIZ|'. 
Interspersed are explanations.  Sometimes the explanations
contain Mizar text from other articles: the main text of the
`\verb|UNIALG_1|' article can be recognized because it
is not indented and because it has line numbers in the left margin.

\subsection{Abstract}

In order to find out what's in an article from the Mizar library, one generally
only looks at its `abstract' file.  This is generated automatically from the
full article.  In it all proofs have been removed and
`sequence numbers' like `\verb|UNIALG_1:5|' for the theorems and
`\verb|UNIALG_1:def 11|' for the definitions have been
inserted automatically.

\begin{flushleft}\footnotesize
\lineno\verb|:: Basic Notation of Universal Algebra|\\
\lineno\verb|::  by Jaros{\l}aw Kotowicz, Beata Madras and Ma{\l}gorzata Korolkiewicz|\\
\lineno\verb|::|\\
\lineno\verb|:: Received December 29, 1992|\\
\lineno\verb|:: Copyright (c) 1992 Association of Mizar Users|
\lineinc
\medskip

\lineno\verb|environ|
\lineinc
\medskip

\lineno\verb| vocabulary UNIALG, PFUNC1, FINSEQ, FUNC_REL, FUNC, FINITER2, PBOOLE, UNIALG_D;|\\
\lineno\verb| notation ARYTM, NAT_1, STRUCT_0, TARSKI, RELAT_1, FUNCT_1, FINSEQ_1, FUNCOP_1,|\\
\lineno\verb|      PARTFUN1, ZF_REFLE;|\\
\lineno\verb| clusters TARSKI, FINSEQ_1, RELSET_1, STRUCT_0, ARYTM, PARTFUN1, FUNCOP_1;|\\
\lineno\verb| constructors FINSEQ_4, STRUCT_0, ZF_REFLE, FUNCOP_1, PARTFUN1;|\\
\lineno\verb| requirements ARYTM;|
\lineinc
\lineinc
\end{flushleft}

This is the `\verb|environ|' header of the article.  It mentions the various
vocabularies (in the `\verb|vocabulary|' directive)\
and articles (in the `\verb|notation|', `\verb|clusters|' and
`\verb|constructors|' directives) from the Mizar library that the article uses. 
The only special items in this header are the vocabulary `\verb|UNIALG|'
which is the one that's `special' to this article, and the
`\verb|ARYTM|' label, which is neither a vocabulary name
nor an article name.

The vocabulary file `\verb|UNIALG.VOC|' is not
explicitely present in the Mizar distribution but only as part of the
`compiled' vocabulary library `\verb|MML.VCB|'.  However, it can be printed
with the command `{\tt listvoc UNIALG}':

\begin{verse}\footnotesize
\verb|GUAStr|\\
\verb|Ucharact|\\
\verb|Vhomogeneous|\\
\verb|Vquasi_total|\\
\verb|Vpartial|\\
\verb|OOpers 128|\\
\verb|MUniversal_Algebra|\\
\verb|Oarity 128|\\
\verb|Osignature|
\end{verse}

These are the `\verb|func|' (`\verb|O|'), `\verb|mode|' (`\verb|M|'),
`\verb|attr|' (`\verb|V|'), `\verb|struct|' (`\verb|G|') and
`\verb|struct| field' (`\verb|U|') symbols which are `new' to this article.
These symbols correspond to the definitions from lines
62, 63, 75, 82, 105, /, 142, 150 and 161 of the abstract, and lines
153, 154, 176, 182, 257, /, 343, 351 and 395
of the full article.  The operation `\verb|Opers|' does not appear
in this article,
but is defined in article `\verb|UNIALG_2|' (both articles share the
vocabulary).

\begin{flushleft}\footnotesize\medskip
\lineno\verb|begin|
\lineinc
\lineinc
\end{flushleft}

A Mizar article consists of one or more `sections', each of which starts with
`\verb|begin|' (there is no corresponding `\verb|end|').
This article only has one section.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|reserve A for set,|\\
\lineno\verb|        a for Element of A,|\\
\lineno\verb|        x,y for FinSequence of A,|\\
\lineno\verb|        h for PartFunc of A*,A ,|\\
\lineno\verb|        n,m for Nat,|\\
\lineno\verb|        z for set;|
\lineinc
\end{flushleft}

These reservations are straight-forward:
note that some of them only can be used when there's an
`\verb|A|' in scope.

The most interesting type from this list is that of `\verb|h|':

\begin{verse}\footnotesize
\verb|PartFunc of A*,A|
\end{verse}

The postfix operator `\verb|*|' is defined in article `\verb|FINSEQ_1|'
(the easiest way to determine this is to click on it in the web version%
\footnote{{\tt <http://www.mizar.org/JFM/mmlident.html>}}
of the Mizar library) as:

\begin{verse}\footnotesize
\verb|definition let D be set;|\\
\verb|  func D* -> set means x |$\in$\verb| it iff x is FinSequence of D;|\\
\verb|end;|
\end{verse}

\noindent
(definitions as presented here are
taken from the abstracts and so don't contain proofs),
with the operator symbol `\verb|*|' defined in \verb|vocabulary| `\verb|FINSEQ|'
as:

\begin{verse}\footnotesize
\verb|O*  128|
\end{verse}

\noindent
while the \verb|mode| `\verb|FinSequence|' comes from the same article:

\begin{verse}\footnotesize
\verb|definition let n;|\\
\verb|  func Seg n -> set equals { k : 1 |$\le$\verb| k & k |$\le$\verb| n };|\\
\verb|end;|

\verb|definition let IT be Relation;|\\
\verb|  attr IT is FinSequence-like means ex n st dom IT = Seg n;|\\
\verb|end;|

\verb|definition|\\
\verb|  mode FinSequence is FinSequence-like Function;|\\
\verb|end;|

\verb|definition let D be set;|\\
\verb|  mode FinSequence of D -> FinSequence means rng it c= D;|\\
\verb|end;|
\end{verse}

The `\verb|PartFunc|' \verb|mode| is defined in article `\verb|PARTFUN1|' as:

\begin{verse}\footnotesize
\verb|definition let X,Y;|\\
\verb|  mode PartFunc of X,Y is Function-like Relation of X,Y;|\\
\verb|end;|
\end{verse}

\noindent
so `\verb|PartFunc of A*,A|' means `partial function from
\verb|A*| to \verb|A|'.  The general way to name a mode is:

\begin{verse}\footnotesize
{\it mode-name\/}{\tt{} of }{\it parameter\/}\verb|,|{\it parameter\/}\verb|,|\ldots
\end{verse}

\noindent
which explains the slightly unnatural syntax.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|definition let A;|\\
\lineno\verb|  let IT be PartFunc of A*,A;|\\
\lineno\verb|attr IT is homogeneous means|\\
\lineno\verb|:: UNIALG_1:def 1                 |\\
\lineno\verb| for x,y st x |$\in$\verb| dom IT & y |$\in$\verb| dom IT holds len x = len y;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let A;|\\
\lineno\verb| let IT be PartFunc of A*,A;|\\
\lineno\verb|attr IT is quasi_total means|\\
\lineno\verb|:: UNIALG_1:def 2|\\
\lineno\verb| for x,y st len x = len y & x |$\in$\verb| dom IT holds y |$\in$\verb| dom IT;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let A be non empty set;|\\
\lineno\verb|cluster homogeneous quasi_total non empty PartFunc of A*,A;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

This cluster states that the type:

\begin{verse}\footnotesize
\verb|homogeneous quasi_total non empty PartFunc of A*,A|
\end{verse}

\noindent
is inhabited.  It is needed (because Mizar types have to be non-empty)
to be allowed to use the adjectives `\verb|homogeneous|',
`\verb|quasi_total|' and `{\tt non empty}'
(alone or in combination) with types of the form `{\tt PartFunc of A*,A}'.
Without it for instance the types:

\begin{verse}\footnotesize
\verb|homogeneous quasi_total non empty PartFunc of A*,A|

\verb|homogeneous non empty PartFunc of A*,A|

\verb|homogeneous non empty|\\
\verb|  PartFunc of (the carrier of U)*,the carrier of U|
\end{verse}

\noindent
in lines 50, 149 and 165-166 of this abstract wouldn't be legal
(in the proofs there appear 11 more types like this).

\begin{flushleft}\footnotesize\medskip
\lineno\verb|theorem :: UNIALG_1:1 |\\
\lineno\verb|h is non empty iff dom h <> |$\emptyset$\verb|;|
\lineinc
\medskip

\lineno\verb|theorem :: UNIALG_1:2 |\\
\lineno\verb|for A being non empty set, a being Element of A|\\
\lineno\verb|holds {<|$\emptyset$\verb|>A} -->a is homogeneous quasi_total non empty PartFunc of A*,A;|
\lineinc
\end{flushleft}

The operator \verb|<|$\emptyset$\verb|>A| denotes the empty finite sequence
with elements of type
\verb|A|.  It is defined in article `\verb|FINSEQ_1|' as:

\begin{verse}\footnotesize
\verb|definition redefine func |$\emptyset$\verb|; synonym <|$\emptyset$\verb|>; end;|

\verb|definition let D be set;|\\
\verb|  func <|$\emptyset$\verb|>(D) -> empty FinSequence of D equals <|$\emptyset$\verb|>;|\\
\verb|end;|
\end{verse}

\noindent
where the operator symbol `\verb|<|$\emptyset$\verb|>|' is from
vocabulary `\verb|FINSEQ|':

\begin{verse}\footnotesize
\verb|O<|$\emptyset$\verb|> 254|
\end{verse}

In this, `$\emptyset$' is the name of the empty set as introduced in article `\verb|HIDDEN|':

\begin{verse}\footnotesize
\verb|definition|\\
\verb|  func |$\emptyset$\verb| -> empty set;|\\
\verb|end;|
\end{verse}

\noindent
and vocabulary `\verb|HIDDEN|':

\begin{verse}\footnotesize
\verb|O|$\emptyset$\verb| 128|
\end{verse}

\noindent
(Because `\verb|HIDDEN|' is one of the two files presenting the axioms
of the Mizar system there is no `\verb|means|' or `\verb|equals|' in this
definition.
Also, the
`\verb|HIDDEN|' article and the `\verb|HIDDEN|' vocabulary are always
present and so they don't need
to be listed in the `\verb|environ|' header of the article.)

The braces `\verb|{| \ldots\verb|}|' denote the one element set.
It is defined in article `\verb|TARSKI|':

\begin{verse}\footnotesize
\verb|definition let y;|\\
\verb|  func {y} -> set means x |$\in$\verb| it iff x = y;|\\
\verb|end;|
\end{verse}

\noindent
The symbols `\verb|{|' and `\verb|}|' occur on their own in
the Mizar syntax too, and are not in a vocabulary.

The infix operator `\verb|-->|' creates a constant function on a set.
It is defined in article `\verb|FUNCOP_1|':

\begin{verse}\footnotesize
\verb|definition let A, a be set;|\\
\verb|  func A --> a -> set equals [:A, {a}:];|\\
\verb|end;|
\end{verse}

\noindent
and vocabulary `\verb|FINITER2|':

\begin{verse}\footnotesize
\verb|O-->  16|
\end{verse}

\noindent
Here \verb|[:| \ldots\verb|:]| is the Cartesian product from
article `\verb|ZFMISC_1|':

\begin{verse}\footnotesize
\verb|definition let X1,X2;|\\
\verb|  func [: X1,X2 :] means|\\
\verb|    z |$\in$\verb| it iff ex x,y st x |$\in$\verb| X1 & y |$\in$\verb| X2 & z = [x,y];|\\
\verb|end;|
\end{verse}

\noindent
and `\verb|[| \ldots\verb|]|' is the Kuratowski pair from article
`\verb|TARSKI|':

\begin{verse}\footnotesize
\verb|definition|\\
\verb|  func [x,y] equals {{x,y},{x}};|\\
\verb|end;|
\end{verse}

\begin{flushleft}\footnotesize\medskip
\lineno\verb|theorem :: UNIALG_1:3 |\\
\lineno\verb|for A being non empty set, a being Element of A|\\
\lineno\verb| holds {<|$\emptyset$\verb|>A} -->a is Element of PFuncs(A*,A);|
\lineinc
\end{flushleft}

The \verb|func| `\verb|PFuncs|' is defined in article `\verb|PARTFUN1|':

\begin{verse}\footnotesize
\verb|definition let X,Y;|\\
\verb|  func PFuncs(X,Y) -> set means|\\
\verb|    x |$\in$\verb| it iff|\\
\verb|      ex f being Function st x = f & dom f c= X & rng f c= Y;|\\
\verb|end;|
\end{verse}

\begin{flushleft}\footnotesize\medskip
\lineno\verb|definition let A;|\\
\lineno\verb| mode PFuncFinSequence of A -> FinSequence of PFuncs(A*,A) means|\\
\lineno\verb|:: UNIALG_1:def 3|\\
\lineno\verb| not contradiction;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

Despite what the official Mizar grammar (appendix \ref{grammar} on page \pageref{grammar})
suggests, the redundant characterization
`{\tt means not contradiction}' may not be omitted.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|struct (1-sorted) UAStr |$\langle\!\langle$\verb| carrier -> set,|\\
\lineno\verb|      charact -> PFuncFinSequence of the carrier|$\rangle\!\rangle$\verb|;|
\lineinc
\end{flushleft}

So the \verb|struct| `\verb|UAStr|' that underlies the implementation of the notion of `algebra'
in Mizar has two fields: `\verb|carrier|' which is the `sort' of the algebra,
and `\verb|charact|' which is the sequence of `functions' of the algebra.

The ancestor \verb|struct| `\verb|1-sorted|' is defined in article `\verb|STRUCT_0|':

\begin{verse}\footnotesize
\verb|definition|\\
\verb|  struct 1-sorted |$\langle\!\langle$\verb|carrier -> set|$\rangle\!\rangle$\verb|;|\\
\verb|end;|
\end{verse}

\begin{flushleft}\footnotesize\medskip
\lineno\verb|definition|\\
\lineno\verb| cluster non empty strict UAStr;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

This cluster states that there exists a {\tt non empty strict UAStr}.  It is
not used in this article.

Note that because the type `\verb|UAStr|' widens to
`\verb|1-sorted|', which is narrower than `\verb|set|',
the adjective `{\tt non empty}' refers to the definition:

\begin{verse}\footnotesize
\verb|definition let S be 1-sorted;|\\
\verb|  attr S is empty means the carrier of S is empty;|\\
\verb|end;|
\end{verse}

\noindent
from article `\verb|STRUCT_0|', instead of to the definition:

\begin{verse}\footnotesize
\verb|definition let X be set;|\\
\verb|  attr X is empty;|\\
\verb|end;|
\end{verse}

\noindent
from article `\verb|HIDDEN|'.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|definition let D be non empty set, c be PFuncFinSequence of D;|\\
\lineno\verb| cluster UAStr |$\langle\!\langle$\verb|D,c |$\rangle\!\rangle$\verb| -> non empty;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

This cluster causes expressions of the shape
`\verb|UAStr|$\langle\!\langle$\verb|D,c|$\rangle\!\rangle$', with \verb|D|
having the
adjective `{\tt non empty}', to gain the
adjective `{\tt non empty}' too.  It is used in line 323 of the article.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|definition let A;|\\
\lineno\verb| let IT be PFuncFinSequence of A;|\\
\lineno\verb|attr IT is homogeneous means|\\
\lineno\verb|:: UNIALG_1:def 4      |\\
\lineno\verb|   for n,h st n |$\in$\verb| dom IT & h = IT.n holds h is homogeneous;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let A;|\\
\lineno\verb| let IT be PFuncFinSequence of A;|\\
\lineno\verb|attr IT is quasi_total means|\\
\lineno\verb|:: UNIALG_1:def 5     |\\
\lineno\verb|   for n,h st n |$\in$\verb| dom IT & h = IT.n holds h is quasi_total;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let F be Function;|\\
\lineno\verb|redefine attr F is non-empty means|\\
\lineno\verb|:: UNIALG_1:def 6       |\\
\lineno\verb| for n being set st n |$\in$\verb| dom F holds F.n is non empty;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

The \verb|attr| `\verb|non-empty|' was defined in article `\verb|ZF_REFLE|' as:

\begin{verse}\footnotesize
\verb|definition let F be Function;|\\
\verb|  attr F is non-empty means not |$\emptyset$\verb| |$\in$\verb| rng F;|\\
\verb|end;|
\end{verse}

The redefinition that's given here has to be equivalent to this (it is allowed to have a more
specific parameter type though, although here that's not the case).

Both the original definition and the redefinition
are used in exactly the same way.  This new definition is used in lines 242--250 of the
full article (because the proof there is of the `expanded' form of the
definition: Mizar expands definitions from the article itself, and from
articles in the `\verb|definitions|' \verb|environ| directive).  Also its
`definitional theorem' (`\verb|Def6|')
is referred to in lines 301, 413 and 452 of the full article.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|definition let A be non empty set; let x be Element of PFuncs(A*,A);|\\
\lineno\verb| redefine|\\
\lineno\verb|  func <*x*> -> PFuncFinSequence of A;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

This redefines the
`\verb|<*| \ldots\verb|*>|' operator from
article `\verb|FINSEQ_1|':

\begin{verse}\footnotesize
\verb|definition let x;|\\
\verb|  func <*x*> -> set equals { [1,x] };|\\
\verb|end;|
\end{verse}

This operator is used to write sequences of length one.
The redefinition doesn't give a new characterization of this \verb|func| (so it
`inherits' the
original one), but it does change its {\it type.\/}  Without it, adjectives
like `\verb|homogeneous|' and `\verb|quasi_total|' wouldn't be applicable to
expressions of the form `\verb|<*x*>|', like for instance in line 123 of the
abstract.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|definition let A be non empty set;|\\
\lineno\verb|cluster homogeneous quasi_total non-empty PFuncFinSequence of A;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

This cluster is not used in this article.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|reserve U for UAStr;|
\lineinc
\medskip

\lineno\verb|definition let IT be UAStr;|\\
\lineno\verb|attr IT is partial means|\\
\lineno\verb|:: UNIALG_1:def 7                                |\\
\lineno\verb| the charact of IT is homogeneous;|\\
\lineno\verb|attr IT is quasi_total means|\\
\lineno\verb|:: UNIALG_1:def 8                            |\\
\lineno\verb| the charact of IT is quasi_total;|\\
\lineno\verb|attr IT is non-empty means|\\
\lineno\verb|:: UNIALG_1:def 9                              |\\
\lineno\verb| the charact of IT <> <|$\emptyset$\verb|> & the charact of IT is non-empty;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|reserve A for non empty set,|\\
\lineno\verb|        h for PartFunc of A*,A ,|\\
\lineno\verb|        x,y for FinSequence of A,|\\
\lineno\verb|        a for Element of A;|
\lineinc
\end{flushleft}

These reservations are identical to those from lines 20--23,
apart that after this, `\verb|A|' has the adjective `{\tt non empty}'.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|theorem :: UNIALG_1:4 |\\
\lineno\verb|for x be Element of PFuncs(A*,A) st x = {<|$\emptyset$\verb|>A} --> a holds|\\
\lineno\verb|  <*x*> is homogeneous quasi_total non-empty;|
\lineinc
\medskip

\lineno\verb|definition|\\
\lineno\verb| cluster quasi_total partial non-empty strict non empty UAStr;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

This cluster is used five times in this article to establish the correctness
of a type.  For example it's used in the definition of the \verb|mode|
`\verb|Universal_Algebra|' in line 142 of this abstract.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|definition let U be partial UAStr;|\\
\lineno\verb| cluster the charact of U -> homogeneous;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let U be quasi_total UAStr;|\\
\lineno\verb| cluster the charact of U -> quasi_total;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let U be non-empty UAStr;|\\
\lineno\verb| cluster the charact of U -> non-empty non empty;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

The `{\tt non empty}' means that there is at least one function in an
algebra,
the `\verb|non-empty|' means that these functions all are not empty.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|definition|\\
\lineno\verb|mode Universal_Algebra is quasi_total partial non-empty non empty UAStr;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|reserve U for partial non-empty non empty UAStr;|
\lineinc
\medskip

\lineno\verb|definition|\\
\lineno\verb|  let A;|\\
\lineno\verb|  let f be homogeneous non empty PartFunc of A*,A;|\\
\lineno\verb|func arity(f) -> Nat means|\\
\lineno\verb|:: UNIALG_1:def 10|\\
\lineno\verb| x |$\in$\verb| dom f implies it = len x;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

Note that the argument `\verb|A|' of this \verb|func| is an implicit
argument: it's not
present in the {\tt no\-ta\-tion} `{\tt arity f}'.

\begin{flushleft}\footnotesize\medskip
\lineno\verb|theorem :: UNIALG_1:5 |\\
\lineno\verb|for U holds for n st n|$\in$\verb|dom the charact of(U) holds|\\
\lineno\verb|  (the charact of(U)).n is|\\
\lineno\verb|   PartFunc of (the carrier of U)*,the carrier of U;|
\lineinc
\medskip

\lineno\verb|definition let U;|\\
\lineno\verb|func signature(U) ->FinSequence of NAT means|\\
\lineno\verb|:: UNIALG_1:def 11|\\
\lineno\verb| len it = len the charact of(U) &|\\
\lineno\verb| for n st n |$\in$\verb| dom it holds|\\
\lineno\verb|   for h be homogeneous non empty|\\
\lineno\verb|   PartFunc of (the carrier of U )*,the carrier of U|\\
\lineno\verb|     st h = (the charact of(U)).n|\\
\lineno\verb|    holds it.n = arity(h);|\\
\lineno\verb|end;|
\end{flushleft}

\subsection{Article}

\setcounter{lineno}{0}
\begin{flushleft}\footnotesize
\lineno\verb|:: Basic Notation of Universal Algebra|\\
\lineno\verb|::  by Jaros{\l}aw Kotowicz, Beata Madras and Ma{\l}gorzata Korolkiewicz|\\
\lineno\verb|::|\\
\lineno\verb|:: Received December 29, 1992|\\
\lineno\verb|:: Copyright (c) 1992 Association of Mizar Users|
\lineinc
\medskip

\lineno\verb|environ|
\lineinc
\medskip

\lineno\verb| vocabulary UNIALG, PFUNC1, FINSEQ, FUNC_REL, FUNC, FINITER2, PBOOLE, UNIALG_D;|\\
\lineno\verb| constructors FINSEQ_4, STRUCT_0, ZF_REFLE, FUNCOP_1, PARTFUN1;|\\
\lineno\verb| requirements ARYTM;|\\
\lineno\verb| notation ARYTM, NAT_1, STRUCT_0, TARSKI, RELAT_1, FUNCT_1, FINSEQ_1, FUNCOP_1,|\\
\lineno\verb|      PARTFUN1, ZF_REFLE;|\\
\lineno\verb| clusters TARSKI, FINSEQ_1, RELSET_1, STRUCT_0, ARYTM, PARTFUN1, FUNCOP_1;|\\
\lineno\verb| definitions TARSKI, STRUCT_0, ZF_REFLE;|\\
\lineno\verb| theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, RELAT_1, RELSET_1,|\\
\lineno\verb|      FINSEQ_3, ZF_REFLE;|\\
\lineno\verb| schemes MATRIX_2;|
\lineinc
\end{flushleft}

The `\verb|definitions|', `\verb|theorems|' and `\verb|schemes|' directives
were not in the abstract because they are only relevant to the proofs.
They also contain names of articles from the library.  The last two list articles
from which \verb|theorems| and \verb|schemes| are used.

The `\verb|definitions|' directive from line 15 applies to 9 places in the article:

\begin{itemize}
\item The proofs in lines 50--54, 56--60, 93--97, 99--103, 131--135 and 137--141.
These proofs are of statements involving the inclusion
operator `\verb|c=|', but the proofs prove a universally
quantified formula.   The `\verb|c=|' operator is defined
in article `\verb|TARSKI|' ({\it re\/}defined really, because
the `\verb|c=|' operator is originally introduced without definition in article
`\verb|HIDDEN|') as:

\begin{verse}\footnotesize
\verb|definition let X,Y;|\\
\verb|  redefine pred X c= Y means x |$\in$\verb| X implies x |$\in$\verb| Y;|\\
\verb|end;|
\end{verse}

\noindent
and so with a `{\tt definitions TARSKI;}' directive the `\verb|c=|' statement
will be expanded to a suitable universal formula.

\item The
`{\tt thus the carrier of UAStr$\langle\!\langle$D,c$\rangle\!\rangle$ is non empty;}'
in lines 161 and 170.  Here the statement to be proved is about a \verb|struct|,
but the statement that is supplied is about {\tt the carrier of} that \verb|struct|.
In order for this to be correct a `{\tt definitions STRUCT\verb|_|0;}' has to make
the definition of `\verb|empty|' on structs transparent:

\begin{verse}\footnotesize
\verb|definition let S be 1-sorted;|\\
\verb|  attr S is empty means the carrier of S is empty;|\\
\verb|end;|
\end{verse}

\item The proof `{\tt assume $\emptyset$ $\in$ rng F;} {\dots}
{\tt hence contradiction by A2;}' in lines 199--201.  It proves
`{\tt not $\emptyset$ $\in$ rng F}', but the statement it
is supposed to prove really is `{\tt F is non-empty}'.  So the directive
`{\tt definitions ZF\verb|_|REFLE;}' is needed to make the definition:

\begin{verse}\footnotesize
\verb|definition let F be Function;|\\
\verb|  attr F is non-empty means not |$\emptyset$\verb| |$\in$\verb| rng F;|\\
\verb|end;|
\end{verse}

transparent. 

\end{itemize}

\noindent
It is `\verb|Analyzer|'
(the type checking phase of the Mizar checker) that needs these definitional
expansions, instead of `\verb|Checker|'
(which checks the logical correctness of the inferences).

\begin{flushleft}\footnotesize\medskip
\lineno\verb|begin|
\lineinc
\lineinc
\medskip

\lineno\verb|reserve A for set,|\\
\lineno\verb|        a for Element of A,|\\
\lineno\verb|        x,y for FinSequence of A,|\\
\lineno\verb|        h for PartFunc of A*,A ,|\\
\lineno\verb|        n,m for Nat,|\\
\lineno\verb|        z for set;|
\lineinc
\medskip

\lineno\verb|definition let A;|\\
\lineno\verb|  let IT be PartFunc of A*,A;|\\
\lineno\verb|attr IT is homogeneous means                 :Def1:|\\
\lineno\verb| for x,y st x |$\in$\verb| dom IT & y |$\in$\verb| dom IT holds len x = len y;|\\
\lineno\verb|end;|
\lineinc
\end{flushleft}

Note that this \verb|definition| is referred to (because of the label on line 32)
as `\verb|Def1|' in this article (on line 364), but (the label on line
30 of the abstract) as `{\tt UNIALG\verb|_|1:def 1}' in the other articles
(specifically: articles `\verb|ALG_1|', `\verb|FREEALG|' and `\verb|PRALG_1|').
Similarly the \verb|theorem| from lines 83--84 is referred to
as `\verb|Th1|' in this article (lines 121, 357 and 372), but as
`{\tt UNIALG\verb|_|1:1}' (line 45 of the abstract) in the
others (`\verb|ALG_1|', `\verb|MSSUBLAT|', `\verb|PRALG_1|' and `\verb|UNIALG_2|').

\begin{flushleft}\footnotesize\medskip
\lineno\verb|definition let A;|\\
\lineno\verb| let IT be PartFunc of A*,A;|\\
\lineno\verb|attr IT is quasi_total means|\\
\lineno\verb| for x,y st len x = len y & x |$\in$\verb| dom IT holds y |$\in$\verb| dom IT;|\\
\lineno\verb|end;|
\lineinc
\medskip
\end{flushleft}

The following definition and its proof will be annotated in more detail than
the remainder of the Mizar text.  The proof (lines 45--80) is the really same as the proof of \verb|theorem|
`\verb|Th2|' (lines 89--122 on page \pageref{th2}), so it can be read there without interruptions.

\begin{flushleft}\footnotesize
\lineno\verb|definition let A be non empty set;|\\
\lineno\verb|cluster homogeneous quasi_total non empty PartFunc of A*,A;|
\end{flushleft}

This cluster states that the type:

\begin{verse}\footnotesize
\verb|homogeneous quasi_total non empty PartFunc of A*,A|
\end{verse}

\noindent
is inhabited.  It should be present if one wants to use the adjectives
`{\tt ho\-mo\-ge\-neous}', `{\tt quasi\verb|_|total}' or `{\tt non empty}' with
types of the form `{\tt PartFunc of A*,A}'.

\begin{flushleft}\footnotesize
\lineno\verb| existence|
\end{flushleft}

Because a `\verb|cluster|' of this kind states the non-emptyness of a
type, its
correctness condition is an `\verb|existence|' statement.  This statement is:

\begin{verse}\footnotesize
\verb|ex f being PartFunc of A*,A st|\\
\verb|  f is homogeneous & f is quasi_total & f is non empty|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|  proof|\\
\lineno\verb|   consider a be Element of A;|
\end{flushleft}

A `\verb|consider|' step needs an existential statement as a justification.
In this case it is:

\begin{verse}\footnotesize
\verb|ex a be Element of A|
\end{verse}

\noindent
(this isn't a full Mizar formula: append
`{\tt st not contradiction}' to complete it).
Because Mizar types all are non-empty an existential statement of
this kind is evident: so the `\verb|consider|' needs no justification.

The property of `\verb|A|' that (from line 42):

\begin{verse}\footnotesize
\verb|A is non empty|
\end{verse}

\noindent
isn't used here: the
`\verb|consider|' step also would have been valid if `\verb|A|'
had just been a `\verb|set|'.  However, in that case:

\begin{verse}\footnotesize
\verb|a |$\in$\verb| A|
\end{verse}

\noindent
would not have been true (it is built into the Mizar system that
when `{\tt A is non empty}' it follows from `{\tt a is Element of A}'
that `{\tt a $\in$ A}'), and then the `\verb|hence|' step in line 59
would have failed.

\begin{flushleft}\footnotesize
\lineno\verb|   set f = {<|$\emptyset$\verb|>A} -->a;|
\end{flushleft}

This is a local definition of a constant `\verb|f|': all occurrences of `\verb|f|'
after this will be expanded to `{\tt \verb|{|<$\emptyset$>A\verb|}|-->a}'.

The `\verb|f|' that's defined here is a function that has as domain the set
`{\tt \verb|{|<$\emptyset$>A\verb|}|}' which it maps to the constant `\verb|a|'.
This domain consist of just the sequence of zero length: it is the set
$\verb|A|^0$.  So we have that:
$$\verb|f|: \verb|A|^0 \rightarrow \verb|A|,\quad \langle\rangle \mapsto \verb|a|$$
and so this \verb|f| is the `nullary' function on \verb|A| which represents
the constant \verb|a|. 

\begin{flushleft}\footnotesize
\lineno\verb|   A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a} by FUNCOP_1:14;|
\end{flushleft}

This statement expands to:

\begin{verse}\footnotesize
\verb|A1: dom ({<|$\emptyset$\verb|>A}-->a) = {<|$\emptyset$\verb|>A} & rng ({<|$\emptyset$\verb|>A}-->a) = {a}|
\end{verse}

\noindent
which follows from the type of `\verb|A|' from line 42:

\begin{verse}\footnotesize
\verb|A is non empty set|
\end{verse}

\noindent
the type of `$\emptyset$' from article `\verb|HIDDEN|':

\begin{verse}\footnotesize
\verb|definition|\\
\verb|  func |$\emptyset$\verb| -> empty set;|\\
\verb|end;|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|theorem :: FUNCOP_1:14|\\
\verb|  A <> |$\emptyset$\verb| implies dom (A --> x) = A & rng (A --> x) = {x};|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|   A2: dom f c= A*|
\end{flushleft}

Because of the `\verb|definitions TARSKI;|' directive from line 15,
this expands according to:

\begin{verse}\footnotesize
\verb|definition let X,Y; redefine pred X c= Y means|\\
\verb|:: TARSKI:def 3|\\
\verb|  x |$\in$\verb| X implies x |$\in$\verb| Y;|\\
\verb|end;|
\end{verse}

\noindent
to:

\begin{verse}\footnotesize
\verb|A2: for z being set st z |$\in$\verb| dom f holds z |$\in$\verb| A*|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|    proof|
\end{flushleft}

Here starts a `local' subproof of the statement `\verb|A2|'.

\begin{flushleft}\footnotesize
\lineno\verb|     let z; assume z |$\in$\verb| dom f; then|
\end{flushleft}

The `\verb|let|' and `\verb|assume|' skeleton steps correspond to the
`\verb|for| {\ldots}' and
`\verb|st| {\ldots} \verb|holds|' parts of the statement.
After these steps:

\begin{verse}\footnotesize
\verb|z |$\in$\verb| A*|
\end{verse}

\noindent
is left to be proved.

\begin{flushleft}\footnotesize
\lineno\verb|     z = <|$\emptyset$\verb|>A by TARSKI:def 1,A1;|
\end{flushleft}

The statement:

\begin{verse}\footnotesize
\verb|z = <|$\emptyset$\verb|>A|
\end{verse}

\noindent
follows from (because of the `\verb|then|' at the end of line 51):

\begin{verse}\footnotesize
\verb|z |$\in$\verb| dom f|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a}|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|definition let y; func {y} -> set means|\\
\verb|:: TARSKI:def 1|\\
\verb|  x |$\in$\verb| it iff x = y;|\\
\verb|end|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|     hence thesis by FINSEQ_1:65;|
\end{flushleft}

The statement that is left to be proved:

\begin{verse}\footnotesize
\verb|z |$\in$\verb| A*|
\end{verse}

\noindent
now follows from (the `\verb|hence|' includes a `\verb|then|'):

\begin{verse}\footnotesize
\verb|z = <|$\emptyset$\verb|>A|
\end{verse}

\noindent
and the type of \verb|<|$\emptyset$\verb|>A| given by:

\begin{verse}\footnotesize
\verb|definition let D be set;|\\
\verb|  func <|$\emptyset$\verb|>(D) -> empty FinSequence of D equals|\\
\verb|  :: FINSEQ_1:def 6|\\
\verb|    <|$\emptyset$\verb|>;|\\
\verb|end;|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|theorem :: FINSEQ_1:65|\\
\verb|  x |$\in$\verb| D* iff x is FinSequence of D;|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|    end;|
\end{flushleft}

{\ldots} and that completes the subproof.

\begin{flushleft}\footnotesize
\lineno\verb|  rng f c= A|\\
\lineno\verb|   proof|\\
\lineno\verb|    let z; assume z |$\in$\verb| rng f; then|\\
\lineno\verb|    z = a by A1,TARSKI:def 1;|\\
\lineno\verb|    hence thesis;|\\
\lineno\verb|   end; then|
\end{flushleft}

This subproof is similar to the previous one.  The step in
line 59 uses that:

\begin{verse}\footnotesize
\verb|a |$\in$\verb| A|
\end{verse}

\noindent
This was explained in the text following the `\verb|consider|' in line 46.

\begin{flushleft}\footnotesize
\lineno\verb|  reconsider f as PartFunc of A*,A by RELSET_1:11,A2;|
\end{flushleft}

After this \verb|reconsider| `\verb|f|' will keep the same meaning
(it will still expand to `{\tt \verb|{|<$\emptyset$>A\verb|}|-->a}'), but
its {\it type\/} will have become `{\tt PartFunc of A*,A}'.

In order to justify this, one has to prove:

\begin{verse}\footnotesize
\verb|f is PartFunc of A*,A|
\end{verse}

\noindent
 which because of the definition of `\verb|f|' and the
definition of \verb|mode| `\verb|PartFunc|':

\begin{verse}\footnotesize
\verb|definition let X,Y;|\\
\verb|  mode PartFunc of X,Y is Function-like Relation of X,Y;|\\
\verb|end;|
\end{verse}

\noindent
`expands' to:

\begin{verse}\footnotesize
\verb|{<|$\emptyset$\verb|>A}-->a is Function-like Relation of A*,A|
\end{verse}

\noindent
This follows from:

\begin{verse}\footnotesize
\verb|A2: dom f c= A*|
\end{verse}

\noindent
and (`\verb|then|' on line 60):

\begin{verse}\footnotesize
\verb|rng f c= A|
\end{verse}

\noindent
and (from article `\verb|FUNCOP_1|'):

\begin{verse}\footnotesize
\verb|definition let A, z be set;|\\
\verb|  cluster A --> z -> Function-like Relation-like;|\\
\verb|end;|
\end{verse}

\noindent
and (from article `\verb|RELAT_1|'):

\begin{verse}\footnotesize
\verb|definition|\\
\verb|  mode Relation is Relation-like set;|\\
\verb|end;|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|theorem :: RELSET_1:11|\\
\verb|  for R being Relation st dom R c= X & rng R c= Y holds|\\
\verb|    R is Relation of X,Y;|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|  A3: f is homogeneous|
\end{flushleft}

This statement expands, because of the definition in lines 30--34, to:

\begin{verse}\footnotesize
\verb|A3: for x,y being FinSequence of A st x |$\in$\verb| dom f & y |$\in$\verb| dom f holds|\\
\verb|  len x = len y|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|   proof|\\
\lineno\verb|    let x,y be FinSequence of A; assume|\\
\lineno\verb|    x |$\in$\verb| dom f & y |$\in$\verb| dom f; then|
\end{flushleft}

After this, the statement left to be proved is:

\begin{verse}\footnotesize
\verb|len x = len y|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|    x = <|$\emptyset$\verb|>A & y = <|$\emptyset$\verb|>A by TARSKI:def 1,A1;|\\
\end{flushleft}

The statement:

\begin{verse}\footnotesize
\verb|x = <|$\emptyset$\verb|>A & y = <|$\emptyset$\verb|>A|
\end{verse}

\noindent
follows from (`\verb|then|' in line 65):

\begin{verse}\footnotesize
\verb|x |$\in$\verb| dom f & y |$\in$\verb| dom f|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a}|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|definition let y; func {y} -> set means|\\
\verb|:: TARSKI:def 1|\\
\verb|  x |$\in$\verb| it iff x = y;|\\
\verb|end|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|    hence thesis;|
\end{flushleft}

Because (`\verb|hence|' refers to the previous statement):

\begin{verse}\footnotesize
\verb|x = <|$\emptyset$\verb|>A & y = <|$\emptyset$\verb|>A|
\end{verse}

\noindent
the \verb|thesis| left to be proved:

\begin{verse}\footnotesize
\verb|len x = len y|
\end{verse}

\noindent
is equivalent to:

\begin{verse}\footnotesize
\verb|len <|$\emptyset$\verb|>A = len <|$\emptyset$\verb|>A|
\end{verse}

\noindent
which is true by reflexivity (equational reasoning is built into the Mizar system).

\begin{flushleft}\footnotesize
\lineno\verb|   end;|\\
\lineno\verb|  A4: f is quasi_total|
\end{flushleft}

This statement expands, because of the definition in lines 36--40, to:

\begin{verse}\footnotesize
\verb|for x,y being FinSequence of A st len x = len y & x |$\in$\verb| dom f holds|\\
\verb|  y |$\in$\verb| dom f|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|   proof|\\
\lineno\verb|    let x,y be FinSequence of A; assume|\\
\lineno\verb|    A5: len x = len y & x |$\in$\verb| dom f; then|
\end{flushleft}

After this, the statement left to be proved is:

\begin{verse}\footnotesize
\verb|y |$\in$\verb| dom f|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|    x = <|$\emptyset$\verb|>A by TARSKI:def 1,A1; then|
\end{flushleft}

The statement:

\begin{verse}\footnotesize
\verb|x = <|$\emptyset$\verb|>A|
\end{verse}

\noindent
follows from:

\begin{verse}\footnotesize
\verb|A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a}|
\end{verse}

\noindent
and (`\verb|then|' in line 72):

\begin{verse}\footnotesize
\verb|len x = len y & x |$\in$\verb| dom f|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|definition let y; func {y} -> set means|\\
\verb|:: TARSKI:def 1|\\
\verb|  x |$\in$\verb| it iff x = y;|\\
\verb|end|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|    len x = 0 by FINSEQ_1:32; then|
\end{flushleft}

The statement:

\begin{verse}\footnotesize
\verb|len x = 0|
\end{verse}

\noindent
follows from (`\verb|then|' in line 73):

\begin{verse}\footnotesize
\verb|x = <|$\emptyset$\verb|>A|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|theorem :: FINSEQ_1:32|\\
\verb|  p=<|$\emptyset$\verb|>(D) iff len p = 0;|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|    y = <|$\emptyset$\verb|>A by FINSEQ_1:32,A5;|
\end{flushleft}

The statement:

\begin{verse}\footnotesize
\verb|y = <|$\emptyset$\verb|>A|
\end{verse}

\noindent
follows from:

\begin{verse}\footnotesize
\verb|A5: len x = len y & x |$\in$\verb| dom f|
\end{verse}

\noindent
and (`\verb|then|' in line 74):

\begin{verse}\footnotesize
\verb|len x = 0|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|theorem :: FINSEQ_1:32|\\
\verb|  p=<|$\emptyset$\verb|>(D) iff len p = 0;|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|    hence thesis by A1,TARSKI:def 1;|
\end{flushleft}

The \verb|thesis| left to be proved:

\begin{verse}\footnotesize
\verb|y |$\in$\verb| dom f|
\end{verse}

\noindent
follows from (`\verb|hence|'):

\begin{verse}\footnotesize
\verb|y = <|$\emptyset$\verb|>A|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a}|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|definition let y; func {y} -> set means|\\
\verb|:: TARSKI:def 1|\\
\verb|  x |$\in$\verb| it iff x = y;|\\
\verb|end|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|   end;|\\
\lineno\verb|  f is non empty by RELAT_1:60,FUNCOP_1:14;|
\end{flushleft}

The statement:

\begin{verse}\footnotesize
\verb|f is non empty|
\end{verse}

\noindent
expands to:

\begin{verse}\footnotesize
\verb|{<|$\emptyset$\verb|>A}-->a is non empty|
\end{verse}

\noindent
which follows from:

\begin{verse}\footnotesize
\verb|theorem :: RELAT_1:60|\\
\verb|  dom |$\emptyset$\verb| = |$\emptyset$\verb| & rng |$\emptyset$\verb| = |$\emptyset$\verb|;|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|theorem :: FUNCOP_1:14|\\
\verb|  A <> |$\emptyset$\verb| implies dom (A --> x) = A & rng (A --> x) = {x};|
\end{verse}

\noindent
and the cluster (from article `\verb|TARSKI|'):

\begin{verse}\footnotesize
\verb|definition let y;|\\
\verb|  cluster {y} -> non empty;|\\
\verb|end;|
\end{verse}

The knowledge that:

\begin{verse}\footnotesize
\verb|A is empty implies A = |$\emptyset$
\end{verse}

\noindent
is built into the Mizar reasoner.

\begin{flushleft}\footnotesize
\lineno\verb|  hence thesis by A3,A4;|
\end{flushleft}

The \verb|thesis| to be proved is:

\begin{verse}\footnotesize
\verb|ex f being PartFunc of A*,A st|\\
\verb|  f is homogeneous & f is quasi_total & f is non empty|
\end{verse}

This follows from the fact that for the specific `defined' \verb|f|
from lines 47 and 61 we know that:

\begin{verse}\footnotesize
\verb|f is homogeneous & f is quasi_total & f is non empty|
\end{verse}

\noindent
which follows from:

\begin{verse}\footnotesize
\verb|A3: f is homogeneous|
\end{verse}

\noindent
and:

\begin{verse}\footnotesize
\verb|A4: f is quasi_total|
\end{verse}

\noindent
and (`\verb|hence|'):

\begin{verse}\footnotesize
\verb|f is non empty|
\end{verse}

Note that Mizar is able to figure out the introduction of the
existential quantifier \verb|ex| by itself, without having to be
told that `\verb|f|' is the witnessing object.

\begin{flushleft}\footnotesize
\lineno\verb| end;|
\end{flushleft}

This finishes the annotated proof.

\begin{flushleft}\footnotesize
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|theorem Th1:|\\
\lineno\verb|h is non empty iff dom h <> |$\emptyset$\verb| by RELAT_1:64,RELAT_1:60;|
\lineinc
\medskip

\lineno\verb|theorem Th2:|\\
\lineno\verb|for A being non empty set, a being Element of A|\\
\lineno\verb|holds {<|$\emptyset$\verb|>A} -->a is homogeneous quasi_total non empty PartFunc of A*,A|
\end{flushleft}

Note that this theorem already has been proved inside the proof of the
\verb|cluster| (lines 47, 61, 62, 69 and 78),
but that the \verb|cluster| has to be present in order to state
the theorem.

\begin{flushleft}\footnotesize
\lineno\verb| proof let A be non empty set, a be Element of A;|\label{th2}\\
\lineno\verb|   set f = {<|$\emptyset$\verb|>A} -->a;|\\
\lineno\verb|   A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a} by FUNCOP_1:14;|\\
\lineno\verb|   A2: dom f c= A*|\\
\lineno\verb|    proof|\\
\lineno\verb|     let z; assume z |$\in$\verb| dom f; then|\\
\lineno\verb|     z = <|$\emptyset$\verb|>A by TARSKI:def 1,A1;|\\
\lineno\verb|     hence thesis by FINSEQ_1:65;|\\
\lineno\verb|    end;|\\
\lineno\verb|  rng f c= A|\\
\lineno\verb|   proof|\\
\lineno\verb|    let z; assume z |$\in$\verb| rng f; then|\\
\lineno\verb|    z = a by A1,TARSKI:def 1;|\\
\lineno\verb|    hence thesis;|\\
\lineno\verb|   end; then|\\
\lineno\verb|  reconsider f as PartFunc of A*,A by RELSET_1:11,A2;|\\
\lineno\verb|  A3: f is homogeneous|\\
\lineno\verb|   proof|\\
\lineno\verb|    let x,y be FinSequence of A; assume|\\
\lineno\verb|    x |$\in$\verb| dom f & y |$\in$\verb| dom f; then|\\
\lineno\verb|    x = <|$\emptyset$\verb|>A & y = <|$\emptyset$\verb|>A by TARSKI:def 1,A1;|\\
\lineno\verb|    hence thesis;|\\
\lineno\verb|   end;|\\
\lineno\verb|  A4: f is quasi_total|\\
\lineno\verb|   proof|\\
\lineno\verb|    let x,y be FinSequence of A; assume|\\
\lineno\verb|    A5: len x = len y & x |$\in$\verb| dom f; then|\\
\lineno\verb|    x = <|$\emptyset$\verb|>A by TARSKI:def 1,A1; then|\\
\lineno\verb|    len x = 0 by FINSEQ_1:32; then|\\
\lineno\verb|    y = <|$\emptyset$\verb|>A by FINSEQ_1:32,A5;|\\
\lineno\verb|    hence thesis by A1,TARSKI:def 1;|\\
\lineno\verb|   end;|\\
\lineno\verb|  thus thesis by A3,A4,A1,Th1;|\\
\lineno\verb| end;|
\lineinc
\medskip

\lineno\verb|theorem Th3:|\\
\lineno\verb|for A being non empty set, a being Element of A|\\
\lineno\verb| holds {<|$\emptyset$\verb|>A} -->a is Element of PFuncs(A*,A)|\\
\lineno\verb| proof let A be non empty set, a be Element of A;|\\
\lineno\verb|   set f = {<|$\emptyset$\verb|>A} -->a;|\\
\lineno\verb|   A1: dom f = {<|$\emptyset$\verb|>A} & rng f = {a} by FUNCOP_1:14;|\\
\lineno\verb|   A2: dom f c= A*|\\
\lineno\verb|    proof|\\
\lineno\verb|     let z; assume z |$\in$\verb| dom f; then|\\
\lineno\verb|     z = <|$\emptyset$\verb|>A by TARSKI:def 1,A1;|\\
\lineno\verb|     hence thesis by FINSEQ_1:65;|\\
\lineno\verb|    end;|\\
\lineno\verb|  rng f c= A|\\
\lineno\verb|   proof|\\
\lineno\verb|    let z; assume z |$\in$\verb| rng f; then|\\
\lineno\verb|    z = a by A1,TARSKI:def 1;|\\
\lineno\verb|    hence thesis;|\\
\lineno\verb|   end; then|\\
\lineno\verb|  reconsider f as PartFunc of A*,A by RELSET_1:11,A2;|\\
\lineno\verb|  f |$\in$\verb| PFuncs(A*,A) by PARTFUN1:119;|\\
\lineno\verb|  hence {<|$\emptyset$\verb|>A} -->a is Element of PFuncs(A*,A);|\\
\lineno\verb| end;|
\lineinc
\medskip

\lineno\verb|definition let A;|\\
\lineno\verb| mode PFuncFinSequence of A -> FinSequence of PFuncs(A*,A) means|\\
\lineno\verb|:Def3: not contradiction;|\\
\lineno\verb| existence;|
\end{flushleft}

The correctness condition of a \verb|mode| definition is the non-emptiness
of the defined type, which is an `\verb|existence|' statement.  In this case this
statement becomes:

\begin{verse}\footnotesize
\verb|ex c being FinSequence of PFuncs(A*,A) st not contradiction|
\end{verse}

Because Mizar types all are non-empty, the existence of a `\verb|c|' of
the appropriate type is obvious, and of course it satisfies `{\tt not contradiction}'.
So this statement needs no justification.

\begin{flushleft}\footnotesize
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|struct (1-sorted) UAStr |$\langle\!\langle$\verb| carrier -> set,|\\
\lineno\verb|      charact -> PFuncFinSequence of the carrier|$\rangle\!\rangle$\verb|;|
\lineinc
\medskip

\lineno\verb|definition|\\
\lineno\verb| cluster non empty strict UAStr;|\\
\lineno\verb| existence|\\
\lineno\verb| proof consider D being non empty set, c being PFuncFinSequence of D;|\\
\lineno\verb|  take UAStr |$\langle\!\langle$\verb|D,c |$\rangle\!\rangle$\verb|;|\\
\lineno\verb|  thus the carrier of UAStr |$\langle\!\langle$\verb|D,c |$\rangle\!\rangle$\verb| is non empty;|\\
\lineno\verb|  thus thesis;|\\
\lineno\verb| end;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let D be non empty set, c be PFuncFinSequence of D;|\\
\lineno\verb| cluster UAStr |$\langle\!\langle$\verb|D,c |$\rangle\!\rangle$\verb| -> non empty;|\\
\lineno\verb| coherence|
\end{flushleft}

The \verb|correctness| condition of a \verb|cluster| of this kind is called
`\verb|coherence|'.  Here, of course, it is:

\begin{verse}\footnotesize
\verb|UAStr|$\langle\!\langle$\verb|D,c|$\rangle\!\rangle$\verb| is non empty|
\end{verse}

Because of the `\verb|definitions STRUCT_0;|' directive in line 15 this expands
to:

\begin{verse}\footnotesize
\verb|the carrier of UAStr|$\langle\!\langle$\verb|D,c|$\rangle\!\rangle$\verb| is non empty|
\end{verse}

\noindent
which reduces to:

\begin{verse}\footnotesize
\verb|D is non empty|
\end{verse}

\noindent
which follows from the type of `\verb|D|' in line 166.

\begin{flushleft}\footnotesize
\lineno\verb| proof|\\
\lineno\verb|  thus the carrier of UAStr |$\langle\!\langle$\verb|D,c |$\rangle\!\rangle$\verb| is non empty;|\\
\lineno\verb| end;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let A;|\\
\lineno\verb| let IT be PFuncFinSequence of A;|\\
\lineno\verb|attr IT is homogeneous means      :Def4:|\\
\lineno\verb|   for n,h st n |$\in$\verb| dom IT & h = IT.n holds h is homogeneous;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let A;|\\
\lineno\verb| let IT be PFuncFinSequence of A;|\\
\lineno\verb|attr IT is quasi_total means     :Def5:|\\
\lineno\verb|   for n,h st n |$\in$\verb| dom IT & h = IT.n holds h is quasi_total;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let F be Function;|\\
\lineno\verb|redefine attr F is non-empty means       :Def6:|\\
\lineno\verb| for n being set st n |$\in$\verb| dom F holds F.n is non empty;|\\
\lineno\verb| compatibility|
\end{flushleft}

The \verb|correctness| condition for the redefinition of a `\verb|pred|' or
`\verb|attr|' is called `\verb|compatibility|'.  In this case, it is:

\begin{verse}\footnotesize
\verb|F is non empty iff |\\
\verb|  for n being set st n |$\in$\verb| dom F holds F.n is non empty|
\end{verse}

In this statement and its proof `{\tt non empty}' still has the `old' definition,
which is:

\begin{verse}\footnotesize
\verb|definition let F be Function;|\\
\verb|  attr F is non-empty means|\\
\verb|  :: ZF_REFLE:def 4|\\
\verb|    not |$\emptyset$\verb| |$\in$\verb| rng F;|\\
\verb|end;|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|   proof|\\
\lineno\verb|    hereby assume F is non-empty; then|
\end{flushleft}

The `\verb|hereby|' keyword behaves like the combination of `\verb|thus|' and
`\verb|now|' (this construction is not in the official Mizar grammar from appendix
\ref{grammar} on page \pageref{grammar}).

\begin{flushleft}\footnotesize
\lineno\verb|A1:    not |$\emptyset$\verb| |$\in$\verb| rng F by ZF_REFLE:def 4;|\\
\lineno\verb|     let i be set;|\\
\lineno\verb|     assume i |$\in$\verb| dom F;|\\
\lineno\verb|     hence F.i is non empty by A1,FUNCT_1:11;|\\
\lineno\verb|    end;|\\
\lineno\verb|    assume |\\
\lineno\verb|A2:    for n being set st n |$\in$\verb| dom F holds F.n is non empty;|\\
\lineno\verb|     assume |$\emptyset$\verb| |$\in$\verb| rng F;|\\
\lineno\verb|      then ex i being set st i |$\in$\verb| dom F & F.i = |$\emptyset$\verb| by FUNCT_1:11;|\\
\lineno\verb|     hence contradiction by A2;|\\
\lineno\verb|   end;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let A be non empty set; let x be Element of PFuncs(A*,A);|\\
\lineno\verb| redefine|\\
\lineno\verb|  func <*x*> -> PFuncFinSequence of A;|\\
\lineno\verb| coherence|
\end{flushleft}

The \verb|correctness| conditions for the redefinition of a `\verb|func|',
are `\verb|coherence|' in case the type changes, and
`\verb|compatibility|' in case the `definition' changes.
In this case only the first applies and the condition of course is:

\begin{verse}\footnotesize
\verb|<*x*> is PFuncFinSequence|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|  proof|\\
\lineno\verb|    <*x*> is FinSequence of PFuncs(A*,A);|\\
\lineno\verb|   hence thesis by Def3;|\\
\lineno\verb|  end;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let A be non empty set;|\\
\lineno\verb|cluster homogeneous quasi_total non-empty PFuncFinSequence of A;|\\
\lineno\verb| existence|\\
\lineno\verb|  proof|\\
\lineno\verb|   consider a being Element of A;|\\
\lineno\verb|   reconsider f = {<|$\emptyset$\verb|>A} -->a as PartFunc of A*,A by Th2;|\\
\lineno\verb|   reconsider f as Element of PFuncs(A*,A) by PARTFUN1:119;|\\
\lineno\verb|   take <*f*>;|\\
\lineno\verb|   thus <*f*> is homogeneous|\\
\lineno\verb|    proof|\\
\lineno\verb|     let n; let h be PartFunc of A*,A; assume|\\
\lineno\verb|     A1: n |$\in$\verb| dom <*f*> & h =<*f*>.n; |\\
\lineno\verb|     then n |$\in$\verb| {1} by FINSEQ_1:4,FINSEQ_1:def 8; then|\\
\lineno\verb|      h = <*f*>.1 by A1,TARSKI:def 1; |\\
\lineno\verb|     then h = f & f is homogeneous PartFunc of A*,A by Th2,FINSEQ_1:def 8;|\\
\lineno\verb|     hence thesis;|\\
\lineno\verb|    end;|\\
\lineno\verb|   thus <*f*> is quasi_total|\\
\lineno\verb|    proof|\\
\lineno\verb|     let n; let h be PartFunc of A*,A; assume|\\
\lineno\verb|     A2: n |$\in$\verb| dom <*f*> & h =<*f*>.n; |\\
\lineno\verb|     then n |$\in$\verb| {1} by FINSEQ_1:4,FINSEQ_1:def 8; then|\\
\lineno\verb|      h = <*f*>.1 by A2,TARSKI:def 1; |\\
\lineno\verb|     then h = f & f is quasi_total PartFunc of A*,A by Th2,FINSEQ_1:def 8;|\\
\lineno\verb|     hence thesis;|\\
\lineno\verb|    end;|\\
\lineno\verb|   thus <*f*> is non-empty|\\
\lineno\verb|    proof|\\
\lineno\verb|     let n be set; assume|\\
\lineno\verb|     A3: n |$\in$\verb| dom <*f*>;|\\
\lineno\verb|     then reconsider n as Nat; |\\
\lineno\verb|     n |$\in$\verb| {1} by FINSEQ_1:4,A3,FINSEQ_1:def 8; then|\\
\lineno\verb|     n = 1 by TARSKI:def 1; then|\\
\lineno\verb|   <*f*>.n=f by FINSEQ_1:def 8; |\\
\lineno\verb|      hence thesis by Th2;|\\
\lineno\verb|    end;|\\
\lineno\verb|  end;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|reserve U for UAStr;|
\lineinc
\medskip

\lineno\verb|definition let IT be UAStr;|\\
\lineno\verb|attr IT is partial means                                :Def7:|\\
\lineno\verb| the charact of IT is homogeneous;|\\
\lineno\verb|attr IT is quasi_total means                            :Def8:|\\
\lineno\verb| the charact of IT is quasi_total;|\\
\lineno\verb|attr IT is non-empty means                              :Def9:|\\
\lineno\verb| the charact of IT <> <|$\emptyset$\verb|> & the charact of IT is non-empty;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|reserve A for non empty set,|\\
\lineno\verb|        h for PartFunc of A*,A ,|\\
\lineno\verb|        x,y for FinSequence of A,|\\
\lineno\verb|        a for Element of A;|
\lineinc
\medskip

\lineno\verb|theorem Th4:|\\
\lineno\verb|for x be Element of PFuncs(A*,A) st x = {<|$\emptyset$\verb|>A} --> a holds|\\
\lineno\verb|  <*x*> is homogeneous quasi_total non-empty|\\
\lineno\verb| proof  let x be Element of PFuncs(A*,A) such that|\\
\lineno\verb|  A1: x = {<|$\emptyset$\verb|>A} --> a;|\\
\end{flushleft}

The `\verb|let| {\ldots} \verb|such that|' construction corresponds to a `\verb|for| {\ldots} \verb|st|'
in the statement, so it is equivalent to a `\verb|let|' followed by an `\verb|assume|'.

\begin{flushleft}\footnotesize
\lineno\verb|  reconsider f=x as PartFunc of A*,A by PARTFUN1:121;|\\
\lineno\verb|  A2: for n,h st n |$\in$\verb| dom <*x*> & h = <*x*>.n holds h is homogeneous|\\
\lineno\verb|   proof let n,h; assume|\\
\lineno\verb|    A3: n |$\in$\verb| dom <*x*> & h =<*x*>.n;|\\
\lineno\verb|    then n |$\in$\verb| {1} by FINSEQ_1:4,FINSEQ_1:def 8; then|\\
\lineno\verb|     h = <*x*>.1 by A3,TARSKI:def 1;|\\
\lineno\verb|    then h = x & f is homogeneous PartFunc of A*,A by Th2,A1,FINSEQ_1:def 8;|\\
\lineno\verb|    hence thesis;|\\
\lineno\verb|   end;|\\
\lineno\verb|  A4: for n,h st n |$\in$\verb| dom <*x*> & h = <*x*>.n holds h is quasi_total|\\
\lineno\verb|   proof let n,h; assume|\\
\lineno\verb|    A5: n |$\in$\verb| dom <*x*> & h =<*x*>.n;|\\
\lineno\verb|    then n |$\in$\verb| {1} by FINSEQ_1:4,FINSEQ_1:def 8; then|\\
\lineno\verb|     h = <*x*>.1 by A5,TARSKI:def 1;|\\
\lineno\verb|    then h = x & f is quasi_total PartFunc of A*,A by Th2,A1,FINSEQ_1:def 8;|\\
\lineno\verb|    hence thesis;|\\
\lineno\verb|   end;|\\
\lineno\verb|  for n being set st n |$\in$\verb| dom <*x*> holds <*x*>.n is non empty|\\
\lineno\verb|   proof let n be set; assume|\\
\lineno\verb|     n |$\in$\verb| dom <*x*>;|\\
\lineno\verb|    then n |$\in$\verb| {1} by FINSEQ_1:4,FINSEQ_1:def 8; then|\\
\lineno\verb|     <*x*>.n = <*x*>.1 by TARSKI:def 1;|\\
\lineno\verb|    then <*x*>.n = x & f is non empty PartFunc of A*,A by Th2,A1|\\
\lineno\verb|,FINSEQ_1:def 8;|\\
\lineno\verb|    hence thesis;|\\
\lineno\verb|   end;|\\
\lineno\verb|  hence thesis by A2,A4,Def6,Def5,Def4;|\\
\lineno\verb| end;|
\lineinc
\medskip

\lineno\verb|definition|\\
\lineno\verb| cluster quasi_total partial non-empty strict non empty UAStr;|\\
\lineno\verb| existence|\\
\lineno\verb|  proof|\\
\lineno\verb|   consider A be non empty set;|\\
\lineno\verb|   consider a be Element of A;|\\
\lineno\verb|   set f = {<|$\emptyset$\verb|>A} --> a;|\\
\lineno\verb|   reconsider w = f as Element of PFuncs(A*,A) by Th3;|\\
\lineno\verb|   set U = UAStr |$\langle\!\langle$\verb| A, <*w*> |$\rangle\!\rangle$\verb|;|\\
\lineno\verb|   take U;|\\
\lineno\verb|   A1: the charact of(U) is quasi_total &|\\
\lineno\verb|      the charact of(U) is homogeneous & the charact of(U) is non-empty|\\
\lineno\verb|    by Th4;|\\
\lineno\verb|   the charact of(U) <> <|$\emptyset$\verb|>|\\
\lineno\verb|    proof assume A2: the charact of(U) = <|$\emptyset$\verb|>;|\\
\lineno\verb|     A3: len(the charact of(U)) = 1 by FINSEQ_1:56;|\\
\lineno\verb|     len (<|$\emptyset$\verb|>) = 0 by FINSEQ_1:25;|\\
\lineno\verb|     hence contradiction by A3,A2;|\\
\lineno\verb|    end;|\\
\lineno\verb|   hence thesis by A1,Def9,Def8,Def7;|\\
\lineno\verb|  end;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let U be partial UAStr;|\\
\lineno\verb| cluster the charact of U -> homogeneous;|\\
\lineno\verb| coherence by Def7;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let U be quasi_total UAStr;|\\
\lineno\verb| cluster the charact of U -> quasi_total;|\\
\lineno\verb| coherence by Def8;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition let U be non-empty UAStr;|\\
\lineno\verb| cluster the charact of U -> non-empty non empty;|\\
\lineno\verb| coherence by Def9;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|definition|\\
\lineno\verb|mode Universal_Algebra is quasi_total partial non-empty non empty UAStr;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|reserve U for partial non-empty non empty UAStr;|
\lineinc
\medskip

\lineno\verb|definition|\\
\lineno\verb|  let A;|\\
\lineno\verb|  let f be homogeneous non empty PartFunc of A*,A;|\\
\lineno\verb|func arity(f) -> Nat means|\\
\lineno\verb| x |$\in$\verb| dom f implies it = len x;|\\
\lineno\verb| existence|
\end{flushleft}

The \verb|correctness| conditions of the \verb|definition| of a \verb|func|
consists of an `{\tt ex\-is\-tence}' and a `\verb|uniqueness|' part.
In this case the `{\tt existence}' condition is:

\begin{verse}\footnotesize
\verb|ex n st|\\
\verb|  for x st x |$\in$\verb| dom f holds n = len x|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|  proof|\\
\lineno\verb|   ex n st for x st x |$\in$\verb| dom f holds n = len x|\\
\lineno\verb|    proof|\\
\lineno\verb|A1:   dom f <> |$\emptyset$\verb| by Th1;|\\
\lineno\verb|     consider x being Element of dom f;|\\
\lineno\verb|     dom f c= A* by RELSET_1:12; then|\\
\lineno\verb|     x |$\in$\verb| A* by A1,TARSKI:def 3; then|\\
\lineno\verb|     reconsider x as FinSequence of A by FINSEQ_1:65;|\\
\lineno\verb|     take n = len x;|\\
\lineno\verb|     let y; assume y |$\in$\verb| dom f;|\\
\lineno\verb|     hence n = len y by Def1;|\\
\lineno\verb|    end;|\\
\lineno\verb|   hence thesis;|\\
\lineno\verb|  end;|\\
\lineno\verb| uniqueness|
\end{flushleft}

The `\verb|uniqueness|' condition is:

\begin{verse}\footnotesize
\verb|for n,m st|\\
\verb|  (for x st x |$\in$\verb| dom f holds n = len x) &|\\
\verb|  (for x st x |$\in$\verb| dom f holds m = len x) holds|\\
\verb|    n = m|
\end{verse}

\begin{flushleft}\footnotesize
\lineno\verb|  proof|\\
\lineno\verb|     let n,m such that A2: (for x st x |$\in$\verb| dom f holds n = len x) &|\\
\lineno\verb|                     for x st x |$\in$\verb| dom f holds m = len x;|\\
\lineno\verb|A3:   dom f <> |$\emptyset$\verb| by Th1;|\\
\lineno\verb|     consider x being Element of dom f;|\\
\lineno\verb|     dom f c= A* by RELSET_1:12; then|\\
\lineno\verb|     x |$\in$\verb| A* by A3,TARSKI:def 3; then|\\
\lineno\verb|     reconsider x as FinSequence of A by FINSEQ_1:65;|\\
\lineno\verb|     n = len x & m = len x by A3,A2;|\\
\lineno\verb|     hence thesis;|\\
\lineno\verb|  end;|\\
\lineno\verb|end;|
\lineinc
\medskip

\lineno\verb|theorem Th5:|\\
\lineno\verb|for U holds for n st n|$\in$\verb|dom the charact of(U) holds|\\
\lineno\verb|  (the charact of(U)).n is|\\
\lineno\verb|   PartFunc of (the carrier of U)*,the carrier of U|\\
\lineno\verb| proof let U,n;|\\
\lineno\verb|  set pu = PFuncs((the carrier of U)*, the carrier of U),|\\
\lineno\verb|      o = the charact of(U); assume|\\
\lineno\verb|   n|$\in$\verb|dom o; then|\\
\lineno\verb|  o.n |$\in$\verb| rng o & rng o c= pu by FUNCT_1:12,FINSEQ_1:def 4;  |\\
\lineno\verb|hence thesis by PARTFUN1:121;|\\
\lineno\verb| end;|
\lineinc
\medskip

\lineno\verb|definition let U;|\\
\lineno\verb|func signature(U) ->FinSequence of NAT means|\\
\lineno\verb| len it = len the charact of(U) &|\\
\lineno\verb| for n st n |$\in$\verb| dom it holds|\\
\lineno\verb|   for h be homogeneous non empty|\\
\lineno\verb|   PartFunc of (the carrier of U )*,the carrier of U|\\
\lineno\verb|     st h = (the charact of(U)).n|\\
\lineno\verb|    holds it.n = arity(h);|\\
\lineno\verb| existence|\\
\lineno\verb|  proof|\\
\lineno\verb|   defpred P[Nat,set] means|\\
\lineno\verb|   for h be homogeneous non empty|\\
\lineno\verb|      PartFunc of (the carrier of U )*,the carrier of U|\\
\lineno\verb|       st h = (the charact of(U)).$1|\\
\lineno\verb|        holds $2 = arity(h);|
\end{flushleft}

A `\verb|defpred|' defines a `local' predicate: it's like
`\verb|set|', but for predicates instead of expressions.
It's expanded everywhere (this one
is used in lines 415 and 419).  The arguments are in the `body'
referred to as `\verb|$1|', `\verb|$2|', {\ldots}  Because the highest
index allowed
is `\verb|$8|', a `\verb|deffunc|' or `\verb|defpred|' takes at most
eight arguments.

\begin{flushleft}\footnotesize
\lineno\verb|   A1: now let m; assume|\\
\lineno\verb|        m|$\in$\verb| Seg len the charact of(U); then|\\
\lineno\verb|        m|$\in$\verb| dom the charact of(U) by FINSEQ_1:def 3; then|\\
\lineno\verb|        reconsider H=(the charact of(U)).m as homogeneous non empty|\\
\lineno\verb|         PartFunc of (the carrier of U )*,the carrier of U by Th5,Def4,Def6;|\\
\lineno\verb|        take n=arity(H);|\\
\lineno\verb|        thus P[m,n];|\\
\lineno\verb|       end;|\\
\lineno\verb|   consider p be FinSequence of NAT such that|\\
\lineno\verb|   A2: dom p = Seg(len the charact of(U)) and|\\
\lineno\verb|   A3: for m st m |$\in$\verb| Seg(len the charact of(U)) holds P[m,p.m] from SeqDEx(A1);|
\end{flushleft}

The `\verb|SeqDEx|' \verb|scheme| from article `\verb|MATRIX_2|' is defined as:

\begin{verse}\footnotesize
\verb|scheme SeqDEx{D()->non empty set,A()->Nat,P[set,set]}:|

\verb|  ex p being FinSequence of D() st dom p = Seg A() &|\\
\verb|    for k st k |$\in$\verb| Seg A() holds P[k,p.k]|

\verb|provided|

\verb|  for k st k |$\in$\verb| Seg A() ex x being Element of D() st P[k,x];|
\end{verse}

\noindent
(Note that references to schemes are by name instead of by number: the
Mizar library contains 546 schemes, less than the number of
articles.)
It is used here to derive:

\begin{verse}\footnotesize
\verb|ex p be FinSequence of NAT st|\\
\verb|  dom p = Seg(len the charact of(U)) &|\\
\verb|  for m st m |$\in$\verb| Seg(len the charact of(U)) holds P[m,p.m]|
\end{verse}

\noindent
(which is needed for the `\verb|consider|' statement), from:

\begin{verse}\footnotesize
\verb|A1: for m st m|$\in$\verb| Seg len the charact of(U) holds ex n st P[m,n]|
\end{verse}

\noindent
So in this case the instantiation of the \verb|scheme| is:

\begin{verse}\footnotesize
\makebox[6em][r]{{\tt D()}}\quad$\rightarrow$\quad\verb|NAT|\\
\makebox[6em][r]{{\tt A()}}\quad$\rightarrow$\quad\verb|len the charact of U|\\
\makebox[6em][r]{{\tt P[k,x]}}\quad$\rightarrow$\quad\verb|P[k,x]|
\end{verse}

\noindent
This substitution is not given explicitely, but is found by matching
the `argument' `\verb|A1|' with the `condition' after the `\verb|provided|'
in the \verb|scheme|, and the statement to be proved with the `conclusion' of
the scheme.

\begin{flushleft}\footnotesize
\lineno\verb|   take p;|\\
\lineno\verb|Seg len the charact of(U) = dom the charact of(U) by FINSEQ_1: def 3;|\\
\lineno\verb|   hence A4: len p = len the charact of(U) by A2,FINSEQ_3:31;|\\
\lineno\verb|   let n; assume|\\
\lineno\verb|   n |$\in$\verb| dom p; then|\\
\lineno\verb|   A5: n |$\in$\verb| Seg(len the charact of(U)) by FINSEQ_1:def 3,A4;|\\
\lineno\verb|   let h be homogeneous non empty|\\
\lineno\verb|          PartFunc of (the carrier of U )*,the carrier of U; assume|\\
\lineno\verb|   h = (the charact of U).n;|\\
\lineno\verb|   hence p.n = arity(h) by A5,A3;|\\
\lineno\verb|  end;|\\
\lineno\verb| uniqueness|\\
\lineno\verb|  proof|\\
\lineno\verb|   let x,y be FinSequence of NAT; assume that|\\
\lineno\verb|   A6: len x = len the charact of(U) and|\\
\lineno\verb|   A7: for n st n |$\in$\verb| dom x holds for h be homogeneous non empty|\\
\lineno\verb|        PartFunc of (the carrier of U )*,the carrier of U|\\
\lineno\verb|         st h = (the charact of(U)).n|\\
\lineno\verb|         holds x.n = arity(h) and|\\
\lineno\verb|   A8: len y = len the charact of(U) and|\\
\lineno\verb|   A9: for n st n |$\in$\verb| dom y holds for h be homogeneous non empty|\\
\lineno\verb|         PartFunc of (the carrier of U )*,the carrier of U|\\
\lineno\verb|          st h = (the charact of(U)).n|\\
\lineno\verb|          holds y.n = arity(h);|\\
\lineno\verb|    now let m; assume|\\
\lineno\verb|     1|$\le$\verb|m & m|$\le$\verb|len x; then|\\
\lineno\verb|     m |$\in$\verb| Seg len x by FINSEQ_1:3; then|\\
\lineno\verb|  m |$\in$\verb| dom x by FINSEQ_1:def 3;|\\
\lineno\verb|     then A10: m |$\in$\verb| dom the charact of(U) & m|$\in$\verb|dom x & m|$\in$\verb|dom y|\\
\lineno\verb|                                             by A6,A8,FINSEQ_3:31;|\\
\lineno\verb|     then reconsider h=(the charact of(U)).m|\\
\lineno\verb|       as homogeneous non empty|\\
\lineno\verb|        PartFunc of (the carrier of U )*,the carrier of U by Th5,Def4,Def6;|\\
\lineno\verb|     x.m=arity(h) & y.m=arity(h) by A7,A9,A10;|\\
\lineno\verb|     hence x.m=y.m;|\\
\lineno\verb|    end;|\\
\lineno\verb|   hence thesis by A6,A8,FINSEQ_1:18;|\\
\lineno\verb|  end;|\\
\lineno\verb|end;|
\end{flushleft}


\end{document}
