Mizar Lecture Notes 4th Edition

<BODY> <P><FONT size="6">Table of Contents</FONT></P> <TABLE> <TBODY> <TR> <TD colspan="4"><A href="preface.html">Preface</A></TD> <TD></TD> </TR> <TR> <TD colspan="4"><A href="preface2.html">Concerning the Revised Edition</A></TD> <TD></TD> </TR> <TR> <TD><BR> </TD> <TD colspan="3"><BR> </TD> <TD></TD> </TR> <TR> <TD>1</TD> <TD colspan="3"><A href="chapter1.html">A Summary of Mizar</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD colspan="3"><BR> </TD> <TD></TD> </TR> <TR> <TD>2</TD> <TD colspan="3"><A href="chapter2.html">An Outline of the Mizar Language</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD colspan="3"><BR> </TD> <TD></TD> </TR> <TR> <TD>3</TD> <TD colspan="3"><A href="chapter3_1.html">The Structure of the Mizar Article</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>3.1</TD> <TD colspan="2"><A href="chapter3_1.html">The Structure of the Mizar</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>3.2</TD> <TD colspan="2"><A href="chapter3_2.html">The Environ Section</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.1</TD> <TD><A href="chapter3_2_1.html">Vocabulary Section</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.2</TD> <TD><A href="chapter3_2_2.html">Notation Section，Constructions Section</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.3</TD> <TD><A href="chapter3_2_3.html">Requirements Section</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.4</TD> <TD><A href="chapter3_2_4.html">Definitions Section</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.5</TD> <TD><A href="chapter3_2_5.html">Theorems Section</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.2.6</TD> <TD><A href="chapter3_2_6.html">Schemes Section</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>3.3</TD> <TD colspan="2"><A href="chapter3_3_1.html">The Main Section</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.3.1</TD> <TD><A href="chapter3_3_1.html">Sentences</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>3.3.2</TD> <TD><A href="chapter3_3_2.html">Theorem</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>4</TD> <TD colspan="3"><A href="chapter4_1.html">Method for Demonstration</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.1</TD> <TD colspan="2"><A href="chapter4_1.html">Basic Method for Demonstration</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.2</TD> <TD colspan="2"><A href="chapter4_2.html">Irrational Method</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.3</TD> <TD colspan="2"><A href="chapter4_3.html">Dividing the Demonstrations</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.4</TD> <TD colspan="2"><A href="chapter4_4.html">Demonstration of the Equivalence</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.5</TD> <TD colspan="2"><A href="chapter4_5.html">Method for Using Now</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.5.1</TD> <TD><A href="chapter4_5_1.html">Caution About End</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.6</TD> <TD colspan="2"><A href="chapter4_6.html">All Symbols</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.6.1</TD> <TD><A href="chapter4_6_2.html">When There Are Two Variables</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.6.2</TD> <TD><A href="chapter4_6_2.html">Method for Writing With such that</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.6.3</TD> <TD><A href="chapter4_6_3.html">Division of Sentences</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.6.4</TD> <TD><A href="chapter4_6_4.html">Dividing Sentences With Assume</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.6.5</TD> <TD><A href="chapter4_6_5.html">Caution Following that</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.7</TD> <TD colspan="2"><A href="chapter4_7.html">Existing Symbols</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.7.1</TD> <TD><A href="chapter4_7_1.html">Method for Using Consider</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.7.2</TD> <TD><A href="chapter4_7_2.html">Method for Using Given</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.8</TD> <TD colspan="2"><A href="chapter4_8.html">Dividing Into Cases</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.8.1</TD> <TD><A href="chapter4_8_1.html">Premise for Dividing Into Cases</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.8.2</TD> <TD><A href="chapter4_8_2.html">Labels for Dividing Into Labels</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>4.8.3</TD> <TD><A href="chapter4_8_3.html">Warning About Labels</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.9</TD> <TD colspan="2"><A href="chapter4_9.html">Method for Using @proof</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.10</TD> <TD colspan="2"><A href="chapter4_10.html">Introduction of New Variable (Set, reconsider)</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.11</TD> <TD colspan="2"><A href="chapter4_11.html">About Take</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>4.12</TD> <TD colspan="2"><A href="chapter4_12.html">Hereby</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>5</TD> <TD colspan="3"><A href="chapter5_1.html">About Mode</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>5.1</TD> <TD colspan="2"><A href="chapter5_1.html">Mode</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>5.2</TD> <TD colspan="2"><A href="chapter5_2.html">Structure Level</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>5.3</TD> <TD colspan="2"><A href="chapter5_3.html">Mode change</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>5.4</TD> <TD colspan="2"><A href="chapter5_4.html">Declaration of Mode During a Demonstration</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>5.4.1</TD> <TD><A href="chapter5_4_1.html">Warning About c=</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>5.4.2</TD> <TD><A href="chapter5_4_2.html">Example of Actually Using a Definition</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>6</TD> <TD colspan="3"><A href="chapter6_1.html">Definition</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.1</TD> <TD colspan="2"><A href="chapter6_1.html">Definition</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.2</TD> <TD colspan="2"><A href="chapter6_2.html">Method for Writing the Vocabulary File</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.3</TD> <TD colspan="2"><A href="chapter6_3.html">Predicate Definition</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.4</TD> <TD colspan="2"><A href="chapter6_4.html">Functor Definition</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.5</TD> <TD colspan="2"><A href="chapter6_5.html">Equqls Definition</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.6</TD> <TD colspan="2"><A href="chapter6_6.html">Mode Definition</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.7</TD> <TD colspan="2"><A href="chapter6_7.html">Cluster Definition</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>6.8</TD> <TD colspan="2"><A href="chapter6_8.html">Introduction of structure</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>7</TD> <TD colspan="3"><A href="chapter7.html">Practice Environment</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>7.1</TD> <TD colspan="2"><A href="chapter7_1.html">Installation</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.1.1</TD> <TD><A href="chapter7_1_1.html">MS-DOS version</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.1.2</TD> <TD><A href="chapter7_1_2.html">Linux version</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>7.2</TD> <TD colspan="2"><A href="chapter7_2.html">Preparation for Using Mizar</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>7.3</TD> <TD colspan="2"><A href="chapter7_3.html">Mizar System</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>7.4</TD> <TD colspan="2"><A href="chapter7_4_1.html">The Mizar Usage</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.4.1</TD> <TD><A href="chapter7_1.html">Accommodate</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.4.2</TD> <TD><A href="chapter7_4_2.html">Mizar Checker</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.4.3</TD> <TD><A href="chapter7_4_3.html">When There Is An Error</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>7.4.4</TD> <TD><A href="chapter7_4_4.html">Useful Command</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>8</TD> <TD colspan="3"><A href="chapter8.html">Registering to the Library</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>8.1</TD> <TD colspan="2"><A href="chapter8_1_1.html">Improvement of an Article</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>8.1.1</TD> <TD><A href="chapter8_1_1.html">Improvement of the Main Section</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>8.1.2</TD> <TD><A href="chapter8_1_2.html">Checking the Environ Section</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>8.2</TD> <TD colspan="2"><A href="chapter8_2.html">Preparation for Registration</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>9</TD> <TD colspan="3"><A href="chapter9_1.html">Useful tools</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>9.1</TD> <TD colspan="2"><A href="chapter9_1.html">To find VOC files containing a terminology (findvoc)</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>9.2</TD> <TD colspan="2"><A href="chapter9_2.html">To check the contents of the VOC file</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>9.3</TD> <TD colspan="2"><A href="chapter9_3_1.html">To serach for the ABS file which the terminology appears</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>9.3.1</TD> <TD><A href="chapter9_3_1.html">Method for Using grep</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>9.3.2</TD> <TD><A href="chapter9_3_2.html">Method for serach on the Web</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>10</TD> <TD colspan="3"><A href="chapter10.html">About renewing the version</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>A</TD> <TD colspan="3"><A href="appendix_A.html">List of Reserved Words</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>B</TD> <TD colspan="3"><A href="appendix_B.html">A Compilation of Mizar Library Theorems</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.1</TD> <TD colspan="2"><A href="appendix_B_1.html">TARSKI</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.2</TD> <TD colspan="2"><A href="appendix_B_2.html">AXIOMS</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.3</TD> <TD colspan="2"><A href="appendix_B_3.html">BOOLE</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.4</TD> <TD colspan="2"><A href="appendix_B_4.html">XBOOL_0</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.5</TD> <TD colspan="2"><A href="appendix_B_5.html">XBOOL_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.6</TD> <TD colspan="2"><A href="appendix_B_6.html">REAL_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.7</TD> <TD colspan="2"><A href="appendix_B_7.html">NAT_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.8</TD> <TD colspan="2"><A href="appendix_B_8.html">FUNCT_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.9</TD> <TD colspan="2"><A href="appendix_B_9.html">SUBSET_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.10</TD> <TD colspan="2"><A href="appendix_B_10.html">FINSEQ_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.11</TD> <TD colspan="2"><A href="appendix_B_11.html">FUNCT_2</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.12</TD> <TD colspan="2"><A href="appendix_B_12.html">SQUARE_1</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>B.13</TD> <TD colspan="2"><A href="appendix_B_13.html">REAL_2</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD>C</TD> <TD>C.1</TD> <TD colspan="2"><A href="appendix_C_1.html">Contacting the Mizar Society</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>C.1.1</TD> <TD><A href="appendix_C_1.html">Mizar Society</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD></TD> <TD>C.1.2</TD> <TD><A href="appendix_C_1.html">Mizar Society Nagano Circle</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>C.2</TD> <TD colspan="2"><A href="appendix_C_2.html">Acquisition of Mizar by ftp</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>C.3</TD> <TD colspan="2"><A href="appendix_C_3.html">How to submit Articles via the Internet</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>C.4</TD> <TD colspan="2"><A href="appendix_C_4.html">WWW Homepage</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD>C.5</TD> <TD colspan="2"><A href="appendix_C_5.html">Formalized Mathematics</A></TD> <TD></TD> </TR> <TR> <TD></TD> <TD><BR> </TD> <TD></TD> <TD></TD> <TD></TD> </TR> <TR> <TD colspan="4"><A href="postface.html">Conclusion</A></TD> <TD></TD> </TR> <TR> <TD colspan="4"><A href="postface.html">Reference</A></TD> <TD></TD> </TR> </TBODY> </TABLE> </BODY>