Journal of Formalized Mathematics, Index of MML Identifiers

[A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z]

ABCMIZ_0,: Grzegorz Bancerek.; On Semilattice Structure of Mizar Types.
ABIAN,: Piotr Rudnicki and Andrzej Trybulec.; Abian's Fixed Point Theorem.
ABSVALUE,: Jan Popiolek.; Some Properties of Functions Modul and Signum.
AFF_1,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; Parallelity and Lines in Affine Spaces.
AFF_2,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; Classical Configurations in Affine Planes.
AFF_3,: Eugeniusz Kusak, Henryk Oryszczyszyn, and Krzysztof Prazmowski.; Affine Localizations of Desargues Axiom.
AFF_4,: Wojciech Leonczuk, Henryk Oryszczyszyn, and Krzysztof Prazmowski.; Planes in Affine Spaces.
AFINSQ_1,: Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura.; Zero-Based Finite Sequences.
AFPROJ,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; A Projective Closure and Projective Horizon of an Affine Space.
AFVECT0,: Grzegorz Lewandowski, Krzysztof Prazmowski, and Bozena Lewandowska.; Directed Geometrical Bundles and Their Analytical Representation.
AFVECT01,: Barbara Konstanta, Urszula Kowieska, Grzegorz Lewandowski, and Krzysztof Prazmowski.; One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation.
ALG_1,: Malgorzata Korolkiewicz.; Homomorphisms of Algebras. Quotient Universal Algebra.
ALGSEQ_1,: Michal Muzalewski and Leslaw W. Szczerba.; Construction of Finite Sequence over Ring and Left-, Right-, and Bi-Modules over a Ring.
ALGSPEC1,: Grzegorz Bancerek.; Technical Preliminaries to Algebraic Specifications.
ALGSTR_1,: Michal Muzalewski and Wojciech Skaba.; From Loops to Abelian Multiplicative Groups with Zero.
ALGSTR_2,: Wojciech Skaba and Michal Muzalewski.; From Double Loops to Fields.
ALGSTR_3,: Michal Muzalewski and Wojciech Skaba.; Ternary Fields.
ALI2,: Alicia de la Cruz.; Fix Point Theorem for Compact Spaces.
ALTCAT_1,: Andrzej Trybulec.; Categories without Uniqueness of \rm cod and \rm dom.
ALTCAT_2,: Andrzej Trybulec.; Examples of Category Structures.
ALTCAT_3,: Beata Madras-Kobus.; Basic Properties of Objects and Morphisms.
ALTCAT_4,: Artur Kornilowicz.; On the Categories Without Uniqueness of \bf cod and \bf dom . Some Properties of the Morphisms and the Functors.
AMI_1,: Yatsuka Nakamura and Andrzej Trybulec.; A Mathematical Model of CPU.
AMI_2,: Yatsuka Nakamura and Andrzej Trybulec.; On a Mathematical Model of Programs.
AMI_3,: Andrzej Trybulec and Yatsuka Nakamura.; Some Remarks on the Simple Concrete Model of Computer.
AMI_4,: Andrzej Trybulec and Yatsuka Nakamura.; Euclid's Algorithm.
AMI_5,: Yasushi Tanaka.; On the Decomposition of the States of SCM.
AMI_6,: Artur Kornilowicz.; On the Instructions of SCM.
AMI_7,: Artur Kornilowicz.; Input and Output of Instructions.
AMISTD_1,: Andrzej Trybulec, Piotr Rudnicki, and Artur Kornilowicz.; Standard Ordering of Instruction Locations.
AMISTD_2,: Artur Kornilowicz.; On the Composition of Macro Instructions of Standard Computers.
AMISTD_3,: Artur Kornilowicz.; A Tree of Execution of a Macroinstruction.
ANALMETR,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; Analytical Metric Affine Spaces and Planes.
ANALOAF,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; Analytical Ordered Affine Spaces.
ANALORT,: Jaroslaw Zajkowski.; Oriented Metric-Affine Plane --- Part I.
ANPROJ_1,: Wojciech Leonczuk and Krzysztof Prazmowski.; A Construction of Analytical Projective Space.
ANPROJ_2,: Wojciech Leonczuk and Krzysztof Prazmowski.; Projective Spaces.
ARITHM,: Library Committee.; Field Properties of Complex Numbers --- Requirements.
ARMSTRNG,: William W. Armstrong, Yatsuka Nakamura, and Piotr Rudnicki.; Armstrong's Axioms.
ARYTM_0,: Andrzej Trybulec.; Introduction to Arithmetics.
ARYTM_1,: Andrzej Trybulec.; Non-Negative Real Numbers. Part II.
ARYTM_2,: Andrzej Trybulec.; Non-Negative Real Numbers. Part I.
ARYTM_3,: Grzegorz Bancerek.; Arithmetic of Non-Negative Rational Numbers.
ASYMPT_0,: Richard Krueger, Piotr Rudnicki, and Paul Shelley.; Asymptotic Notation. Part I: Theory.
ASYMPT_1,: Richard Krueger, Piotr Rudnicki, and Paul Shelley.; Asymptotic Notation. Part II: Examples and Problems.
AUTALG_1,: Artur Kornilowicz.; On the Group of Automorphisms of Universal Algebra and Many Sorted Algebra.
AUTGROUP,: Artur Kornilowicz.; On the Group of Inner Automorphisms.
AXIOMS,: Andrzej Trybulec.; Strong Arithmetic of Real Numbers.

BAGORDER,: Gilbert Lee and Piotr Rudnicki.; On Ordering of Bags.
BHSP_1,: Jan Popiolek.; Introduction to Banach and Hilbert Spaces --- Part I.
BHSP_2,: Jan Popiolek.; Introduction to Banach and Hilbert Spaces --- Part II.
BHSP_3,: Jan Popiolek.; Introduction to Banach and Hilbert Spaces --- Part III.
BHSP_4,: Elzbieta Kraszewska and Jan Popiolek.; Series in Banach and Hilbert Spaces.
BHSP_5,: Hiroshi Yamazaki, Yasunari Shidama, and Yatsuka Nakamura.; Bessel's Inequality.
BHSP_6,: Hiroshi Yamazaki, Yasumasa Suzuki, Takao Inoue, and Yasunari Shidama.; On Some Properties of Real Hilbert Space. Part I.
BHSP_7,: Hiroshi Yamazaki, Yasumasa Suzuki, Takao Inoue, and Yasunari Shidama.; On Some Properties of Real Hilbert Space. Part II.
BILINEAR,: Jaroslaw Kotowicz.; Bilinear Functionals in Vector Spaces.
BINARI_2,: Yasuho Mizuhara and Takaya Nishiyama.; Binary Arithmetics, Addition and Subtraction of Integers.
BINARI_3,: Robert Milewski.; Binary Arithmetics. Binary Sequences.
BINARI_4,: Hisayoshi Kunimune and Yatsuka Nakamura.; A Representation of Integers by Binary Arithmetics and Addition of Integers.
BINARI_5,: Shunichi Kobayashi.; On the Calculus of Binary Arithmetics.
BINARITH,: Takaya Nishiyama and Yasuho Mizuhara.; Binary Arithmetics.
BINOM,: Christoph Schwarzweller.; The Binomial Theorem for Algebraic Structures.
BINOP_1,: Czeslaw Bylinski.; Binary Operations.
BINTREE1,: Grzegorz Bancerek and Piotr Rudnicki.; On Defining Functions on Binary Trees.
BINTREE2,: Robert Milewski.; Full Trees.
BIRKHOFF,: Artur Kornilowicz.; Birkhoff Theorem for Many Sorted Algebras.
BOOLE,: Library Committee.; Boolean Properties of Sets --- Requirements.
BOOLEALG,: Agnieszka Julia Marasik.; Boolean Properties of Lattices.
BOOLMARK,: Pauline N. Kawamoto, Yasushi Fuwa, and Yatsuka Nakamura.; Basic Concepts for Petri Nets with Boolean Markings.
BORSUK_1,: Andrzej Trybulec.; A Borsuk Theorem on Homotopy Types.
BORSUK_2,: Adam Grabowski.; Introduction to the Homotopy Theory.
BORSUK_3,: Adam Grabowski.; Properties of the Product of Compact Topological Spaces.
BORSUK_4,: Adam Grabowski.; On the Decompositions of Intervals and Simple Closed Curves.
BORSUK_5,: Adam Grabowski.; On the Subcontinua of a Real Line.
BVFUNC10,: Shunichi Kobayashi.; Propositional Calculus for Boolean Valued Functions. Part VI.
BVFUNC11,: Shunichi Kobayashi and Yatsuka Nakamura.; Predicate Calculus for Boolean Valued Functions. Part III.
BVFUNC12,: Shunichi Kobayashi and Yatsuka Nakamura.; Predicate Calculus for Boolean Valued Functions. Part IV.
BVFUNC13,: Shunichi Kobayashi and Yatsuka Nakamura.; Predicate Calculus for Boolean Valued Functions. Part V.
BVFUNC14,: Shunichi Kobayashi.; Predicate Calculus for Boolean Valued Functions. Part VI.
BVFUNC22,: Shunichi Kobayashi.; Five Variable Predicate Calculus for Boolean Valued Functions. Part I.
BVFUNC23,: Shunichi Kobayashi.; Six Variable Predicate Calculus for Boolean Valued Functions. Part I.
BVFUNC24,: Shunichi Kobayashi.; Predicate Calculus for Boolean Valued Functions. Part XII.
BVFUNC25,: Shunichi Kobayashi.; Propositional Calculus for Boolean Valued Functions. Part VII.
BVFUNC_1,: Shunichi Kobayashi and Kui Jia.; A Theory of Boolean Valued Functions and Partitions.
BVFUNC_2,: Shunichi Kobayashi and Yatsuka Nakamura.; A Theory of Boolean Valued Functions and Quantifiers with Respect to Partitions.
BVFUNC_3,: Shunichi Kobayashi and Yatsuka Nakamura.; Predicate Calculus for Boolean Valued Functions. Part I.
BVFUNC_4,: Shunichi Kobayashi and Yatsuka Nakamura.; Predicate Calculus for Boolean Valued Functions. Part II.
BVFUNC_5,: Shunichi Kobayashi and Yatsuka Nakamura.; Propositional Calculus for Boolean Valued Functions. Part I.
BVFUNC_6,: Shunichi Kobayashi and Yatsuka Nakamura.; Propositional Calculus for Boolean Valued Functions. Part II.
BVFUNC_7,: Shunichi Kobayashi.; Propositional Calculus for Boolean Valued Functions. Part III.
BVFUNC_8,: Shunichi Kobayashi.; Propositional Calculus for Boolean Valued Functions. Part IV.
BVFUNC_9,: Shunichi Kobayashi.; Propositional Calculus for Boolean Valued Functions. Part V.

CANTOR_1,: Alexander Yu. Shibakov and Andrzej Trybulec.; The Cantor Set.
CARD_1,: Grzegorz Bancerek.; Cardinal Numbers.
CARD_2,: Grzegorz Bancerek.; Cardinal Arithmetics.
CARD_3,: Grzegorz Bancerek.; K\"onig's Theorem.
CARD_4,: Grzegorz Bancerek.; Countable Sets and Hessenberg's Theorem.
CARD_5,: Grzegorz Bancerek.; On Powers of Cardinals.
CARD_FIL,: Josef Urban.; Basic Facts about Inaccessible and Measurable Cardinals.
CARD_LAR,: Josef Urban.; Mahlo and Inaccessible Cardinals.
CAT_1,: Czeslaw Bylinski.; Introduction to Categories and Functors.
CAT_2,: Czeslaw Bylinski.; Subcategories and Products of Categories.
CAT_3,: Czeslaw Bylinski.; Products and Coproducts in Categories.
CAT_4,: Czeslaw Bylinski.; Cartesian Categories.
CAT_5,: Grzegorz Bancerek.; Categorial Categories and Slice Categories.
CATALG_1,: Grzegorz Bancerek.; Algebra of Morphisms.
CFCONT_1,: Takashi Mitsuishi, Katsumi Wasaki, and Yasunari Shidama.; Property of Complex Sequence and Continuity of Complex Function.
CFUNCT_1,: Takashi Mitsuishi, Katsumi Wasaki, and Yasunari Shidama.; Property of Complex Functions.
CHAIN_1,: Freek Wiedijk.; Chains on a Grating in Euclidean Space.
CIRCCMB2,: Grzegorz Bancerek, Shin'nosuke Yamaguchi, and Yasunari Shidama.; Combining of Multi Cell Circuits.
CIRCCMB3,: Grzegorz Bancerek and Adam Naumowicz.; Preliminaries to Automatic Generation of Mizar Documentation for Circuits.
CIRCCOMB,: Yatsuka Nakamura and Grzegorz Bancerek.; Combining of Circuits.
CIRCTRM1,: Grzegorz Bancerek.; Circuit Generated by Terms and Circuit Calculating Terms.
CIRCUIT1,: Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.; Introduction to Circuits, I.
CIRCUIT2,: Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.; Introduction to Circuits, II.
CLASSES1,: Grzegorz Bancerek.; Tarski's Classes and Ranks.
CLASSES2,: Bogdan Nowak and Grzegorz Bancerek.; Universal Classes.
CLOSURE1,: Artur Kornilowicz.; On the Many Sorted Closure Operator and the Many Sorted Closure System.
CLOSURE2,: Artur Kornilowicz.; On the Closure Operator and the Closure System of Many Sorted Sets.
CLOSURE3,: Agnieszka Julia Marasik.; Algebraic Operation on Subsets of Many Sorted Sets.
COH_SP,: Jaroslaw Kotowicz and Konrad Raczkowski.; Coherent Space.
COHSP_1,: Grzegorz Bancerek.; Continuous, Stable, and Linear Maps of Coherence Spaces.
COLLSP,: Wojciech Skaba.; The Collinearity Structure.
COMMACAT,: Grzegorz Bancerek and Agata Darmochwal.; Comma Category.
COMPLEX1,: Czeslaw Bylinski.; The Complex Numbers.
COMPLEX2,: Wenpai Chang, Yatsuka Nakamura, and Piotr Rudnicki.; Inner Products and Angles of Complex Numbers.
COMPLFLD,: Anna Justyna Milewska.; The Field of Complex Numbers.
COMPLSP1,: Czeslaw Bylinski and Andrzej Trybulec.; Complex Spaces.
COMPTRIG,: Robert Milewski.; Trigonometric Form of Complex Numbers.
COMPTS_1,: Agata Darmochwal.; Compact Spaces.
COMPUT_1,: Grzegorz Bancerek and Piotr Rudnicki.; The Set of Primitive Recursive Functions.
COMSEQ_1,: Agnieszka Banachowicz and Anna Winnicka.; Complex Sequences.
COMSEQ_2,: Adam Naumowicz.; Conjugate Sequences, Bounded Complex Sequences and Convergent Complex Sequences.
COMSEQ_3,: Yasunari Shidama and Artur Kornilowicz.; Convergence and the Limit of Complex Sequences. Series.
CONAFFM,: Jolanta Swierzynska and Bogdan Swierzynski.; Metric-Affine Configurations in Metric Affine Planes --- Part I.
CONLAT_1,: Christoph Schwarzweller.; Introduction to Concept Lattices.
CONLAT_2,: Christoph Schwarzweller.; A Characterization of Concept Lattices. Dual Concept Lattices.
CONMETR,: Jolanta Swierzynska and Bogdan Swierzynski.; Metric-Affine Configurations in Metric Affine Planes --- Part II.
CONMETR1,: Jolanta Swierzynska and Bogdan Swierzynski.; Shear Theorems and Their Role in Affine Geometry.
CONNSP_1,: Beata Padlewska.; Connected Spaces.
CONNSP_2,: Beata Padlewska.; Locally Connected Spaces.
CONNSP_3,: Yatsuka Nakamura and Andrzej Trybulec.; Components and Unions of Components.
CONVEX1,: Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama.; Convex Sets and Convex Combinations.
CONVEX2,: Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama.; Some Properties for Convex Combinations.
CONVEX3,: Noboru Endou and Yasunari Shidama.; Convex Hull, Set of Convex Combinations and Convex Cone.
CONVFUN1,: Grigory E. Ivanov.; Definition of Convex Function and Jensen's Inequality.
CQC_LANG,: Czeslaw Bylinski.; A Classical First Order Language.
CQC_SIM1,: Agata Darmochwal and Andrzej Trybulec.; Similarity of Formulae.
CQC_THE1,: Agata Darmochwal.; A First-Order Predicate Calculus.
CQC_THE2,: Agata Darmochwal.; Calculus of Quantifiers. Deduction Theorem.
CQC_THE3,: Oleg Okhotnikov.; Logical Equivalence of Formulae.

DECOMP_1,: Marian Przemski.; On the Decomposition of the Continuity.
DICKSON,: Gilbert Lee and Piotr Rudnicki.; Dickson's Lemma.
DIRAF,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; Ordered Affine Spaces Defined in Terms of Directed Parallelity --- Part I.
DIRORT,: Jaroslaw Zajkowski.; Oriented Metric-Affine Plane --- Part II.
DOMAIN_1,: Andrzej Trybulec.; Domains and Their Cartesian Products.
DTCONSTR,: Grzegorz Bancerek and Piotr Rudnicki.; On Defining Functions on Trees.
DYNKIN,: Franz Merkl.; Dynkin's Lemma in Measure Theory.

E_SIEC,: Waldemar Korczynski.; Definitions of Petri Net. Part II.
ENDALG,: Jaroslaw Gryko.; On the Monoid of Endomorphisms of Universal Algebra and Many Sorted Algebra.
ENS_1,: Czeslaw Bylinski.; Category Ens.
ENUMSET1,: Andrzej Trybulec.; Enumerated Sets.
EQREL_1,: Konrad Raczkowski and Pawel Sadowski.; Equivalence Relations and Classes of Abstraction.
EQUATION,: Artur Kornilowicz.; Equations in Many Sorted Algebras.
EUCLID,: Agata Darmochwal.; The Euclidean Space.
EUCLID_2,: Kanchun and Yatsuka Nakamura.; The Inner Product of Finite Sequences and of Points of $n$-dimensional Topological Space.
EUCLID_3,: Akihiro Kubo and Yatsuka Nakamura.; Angle and Triangle in Euclidian Topological Space.
EUCLID_4,: Akihiro Kubo.; Lines in $n$-Dimensional Euclidean Spaces.
EUCLID_5,: Kanchun, Hiroshi Yamazaki, and Yatsuka Nakamura.; Cross Products and Tripple Vector Products in 3-dimensional Euclidian Space.
EUCLMETR,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; Fundamental Types of Metric Affine Spaces.
EULER_1,: Yoshinori Fujisawa and Yasushi Fuwa.; The Euler's Function.
EULER_2,: Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu.; Euler's Theorem and Small Fermat's Theorem.
EXTENS_1,: Artur Kornilowicz.; Extensions of Mappings on Generator Set.
EXTREAL1,: Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.; Basic Properties of Extended Real Numbers.
EXTREAL2,: Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.; Some Properties of Extended Real Numbers Operations: abs, min and max.

FACIRC_1,: Grzegorz Bancerek and Yatsuka Nakamura.; Full Adder Circuit. Part I.
FACIRC_2,: Grzegorz Bancerek, Shin'nosuke Yamaguchi, and Katsumi Wasaki.; Full Adder Circuit. Part II.
FCONT_1,: Konrad Raczkowski and Pawel Sadowski.; Real Function Continuity.
FCONT_2,: Jaroslaw Kotowicz and Konrad Raczkowski.; Real Function Uniform Continuity.
FCONT_3,: Jaroslaw Kotowicz.; Monotonic and Continuous Real Function.
FDIFF_1,: Konrad Raczkowski and Pawel Sadowski.; Real Function Differentiability.
FDIFF_2,: Jaroslaw Kotowicz and Konrad Raczkowski.; Real Function Differentiability --- Part II.
FDIFF_3,: Ewa Burakowska and Beata Madras.; Real Function One-Side Differentiability.
FF_SIEC,: Waldemar Korczynski.; Definitions of Petri Net. Part I.
FIB_FUSC,: Grzegorz Bancerek and Piotr Rudnicki.; Two Programs for \bf SCM. Part II - Programs.
FIB_NUM,: Robert M. Solovay.; Fibonacci Numbers.
FILTER_0,: Grzegorz Bancerek.; Filters --- Part I.
FILTER_1,: Grzegorz Bancerek.; Filters - Part II. Quotient Lattices Modulo Filters and Direct Product of Two Lattices.
FILTER_2,: Grzegorz Bancerek.; Ideals.
FIN_TOPO,: Hiroshi Imura and Masayoshi Eguchi.; Finite Topological Spaces.
FINSEQ_1,: Grzegorz Bancerek and Krzysztof Hryniewiecki.; Segments of Natural Numbers and Finite Sequences.
FINSEQ_2,: Czeslaw Bylinski.; Finite Sequences and Tuples of Elements of a Non-empty Sets.
FINSEQ_3,: Wojciech A. Trybulec.; Non-contiguous Substrings and One-to-one Finite Sequences.
FINSEQ_4,: Wojciech A. Trybulec.; Pigeon Hole Principle.
FINSEQ_5,: Czeslaw Bylinski.; Some Properties of Restrictions of Finite Sequences.
FINSEQ_6,: Andrzej Trybulec.; On the Decomposition of Finite Sequences.
FINSEQ_7,: Hiroshi Yamazaki, Yoshinori Fujisawa, and Yatsuka Nakamura.; On Replace Function and Swap Function for Finite Sequences.
FINSEQOP,: Czeslaw Bylinski.; Binary Operations Applied to Finite Sequences.
FINSET_1,: Agata Darmochwal.; Finite Sets.
FINSOP_1,: Wojciech A. Trybulec.; Binary Operations on Finite Sequences.
FINSUB_1,: Andrzej Trybulec and Agata Darmochwal.; Boolean Domains.
FINTOPO2,: Gang Liu, Yasushi Fuwa, and Masayoshi Eguchi.; Formal Topological Spaces.
FRAENKEL,: Andrzej Trybulec.; Function Domains and Fr\aenkel Operator.
FRECHET,: Bartlomiej Skorulski.; First-countable, Sequential, and Frechet Spaces.
FRECHET2,: Bartlomiej Skorulski.; The Sequential Closure Operator in Sequential and Frechet Spaces.
FREEALG,: Beata Perkowska.; Free Universal Algebra Construction.
FSCIRC_1,: Katsumi Wasaki and Noboru Endou.; Full Subtracter Circuit. Part I.
FSCIRC_2,: Shin'nosuke Yamaguchi, Grzegorz Bancerek, and Katsumi Wasaki.; Full Subtracter Circuit. Part II.
FSM_1,: Miroslava Kaloper and Piotr Rudnicki.; Minimization of Finite State Machines.
FSM_2,: Hisayoshi Kunimune, Grzegorz Bancerek, and Yatsuka Nakamura.; On State Machines of Calculating Type.
FUNCOP_1,: Andrzej Trybulec.; Binary Operations Applied to Functions.
FUNCSDOM,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; Real Functions Spaces.
FUNCT_1,: Czeslaw Bylinski.; Functions and Their Basic Properties.
FUNCT_2,: Czeslaw Bylinski.; Functions from a Set to a Set.
FUNCT_3,: Czeslaw Bylinski.; Basic Functions and Operations on Functions.
FUNCT_4,: Czeslaw Bylinski.; The Modification of a Function by a Function and the Iteration of the Composition of a Function.
FUNCT_5,: Grzegorz Bancerek.; Curried and Uncurried Functions.
FUNCT_6,: Grzegorz Bancerek.; Cartesian Product of Functions.
FUNCT_7,: Grzegorz Bancerek and Andrzej Trybulec.; Miscellaneous Facts about Functions.
FUNCTOR0,: Andrzej Trybulec.; Functors for Alternative Categories.
FUNCTOR1,: Claus Zinn and Wolfgang Jaksch.; Basic Properties of Functor Structures.
FUNCTOR2,: Robert Nieszczerzewski.; Category of Functors between Alternative Categories.
FUNCTOR3,: Artur Kornilowicz.; The Composition of Functors and Transformations in Alternative Categories.
FUZZY_1,: Takashi Mitsuishi, Noboru Endou, and Yasunari Shidama.; The Concept of Fuzzy Set and Membership Function and Basic Properties of Fuzzy Set Operation.
FUZZY_2,: Takashi Mitsuishi, Katsumi Wasaki, and Yasunari Shidama.; Basic Properties of Fuzzy Set Operation and Membership Function.
FUZZY_3,: Takashi Mitsuishi, Katsumi Wasaki, and Yasunari Shidama.; The Concept of Fuzzy Relation and Basic Properties of its Operation.
FUZZY_4,: Noboru Endou, Takashi Mitsuishi, and Keiji Ohkubo.; Properties of Fuzzy Relation.
FVSUM_1,: Katarzyna Zawadzka.; Sum and Product of Finite Sequences of Elements of a Field.

GATE_1,: Yatsuka Nakamura.; Logic Gates and Logical Equivalence of Adders.
GATE_2,: Yuguang Yang, Katsumi Wasaki, Yasushi Fuwa, and Yatsuka Nakamura.; Correctness of Binary Counter Circuits.
GATE_3,: Yuguang Yang, Katsumi Wasaki, Yasushi Fuwa, and Yatsuka Nakamura.; Correctness of Johnson Counter Circuits.
GATE_4,: Yuguang Yang, Katsumi Wasaki, Yasushi Fuwa, and Yatsuka Nakamura.; Correctness of a Cyclic Redundancy Check Code Generator.
GATE_5,: Hiroshi Yamazaki and Katsumi Wasaki.; The Correctness of the High Speed Array Multiplier Circuits.
GCD_1,: Christoph Schwarzweller.; The Correctness of the Generic Algorithms of Brown and Henrici Concerning Addition and Multiplication in Fraction Fields.
GENEALG1,: Akihiko Uchibori and Noboru Endou.; Basic Properties of Genetic Algorithm.
GEOMTRAP,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; A Construction of Analytical Ordered Trapezium Spaces.
GOBOARD1,: Jaroslaw Kotowicz and Yatsuka Nakamura.; Introduction to Go-Board --- Part I.
GOBOARD2,: Jaroslaw Kotowicz and Yatsuka Nakamura.; Introduction to Go-Board --- Part II.
GOBOARD3,: Jaroslaw Kotowicz and Yatsuka Nakamura.; Properties of Go-Board --- Part III.
GOBOARD4,: Jaroslaw Kotowicz and Yatsuka Nakamura.; Go-Board Theorem.
GOBOARD5,: Yatsuka Nakamura and Andrzej Trybulec.; Decomposing a Go-Board into Cells.
GOBOARD6,: Andrzej Trybulec.; On the Geometry of a Go-Board.
GOBOARD7,: Andrzej Trybulec.; On the Go-Board of a Standard Special Circular Sequence.
GOBOARD8,: Andrzej Trybulec.; More on Segments on a Go-Board.
GOBOARD9,: Andrzej Trybulec.; Left and Right Component of the Complement of a Special Closed Curve.
GOBRD10,: Yatsuka Nakamura and Andrzej Trybulec.; Adjacency Concept for Pairs of Natural Numbers.
GOBRD11,: Yatsuka Nakamura and Andrzej Trybulec.; Some Topological Properties of Cells in $R^2$.
GOBRD12,: Yatsuka Nakamura and Andrzej Trybulec.; The First Part of Jordan's Theorem for Special Polygons.
GOBRD13,: Czeslaw Bylinski.; Some Properties of Cells on Go Board.
GOBRD14,: Artur Kornilowicz.; Properties of Left and Right Components.
GR_CY_1,: Dariusz Surowik.; Cyclic Groups and Some of Their Properties --- Part I.
GR_CY_2,: Dariusz Surowik.; Isomorphisms of Cyclic Groups. Some Properties of Cyclic Groups.
GRAPH_1,: Krzysztof Hryniewiecki.; Graphs.
GRAPH_2,: Yatsuka Nakamura and Piotr Rudnicki.; Vertex Sequences Induced by Chains.
GRAPH_3,: Yatsuka Nakamura and Piotr Rudnicki.; Euler Circuits and Paths.
GRAPH_4,: Yatsuka Nakamura and Piotr Rudnicki.; Oriented Chains.
GRAPH_5,: Jing-Chao Chen and Yatsuka Nakamura.; The Underlying Principle of Dijkstra's Shortest Path Algorithm.
GRAPHSP,: Jing-Chao Chen.; Dijkstra's Shortest Path Algorithm.
GRCAT_1,: Michal Muzalewski.; Categories of Groups.
GRFUNC_1,: Czeslaw Bylinski.; Graphs of Functions.
GROEB_1,: Christoph Schwarzweller.; Characterization and Existence of Gr\"obner Bases.
GROEB_2,: Christoph Schwarzweller.; Construction of Gr\"obner bases. S-Polynomials and Standard Representations.
GROUP_1,: Wojciech A. Trybulec.; Groups.
GROUP_2,: Wojciech A. Trybulec.; Subgroup and Cosets of Subgroups.
GROUP_3,: Wojciech A. Trybulec.; Classes of Conjugation. Normal Subgroups.
GROUP_4,: Wojciech A. Trybulec.; Lattice of Subgroups of a Group. Frattini Subgroup.
GROUP_5,: Wojciech A. Trybulec.; Commutator and Center of a Group.
GROUP_6,: Wojciech A. Trybulec and Michal J. Trybulec.; Homomorphisms and Isomorphisms of Groups. Quotient Group.
GROUP_7,: Artur Kornilowicz.; The Product of the Families of the Groups.
GRSOLV_1,: Katarzyna Zawadzka.; Solvable Groups.

HAHNBAN,: Bogdan Nowak and Andrzej Trybulec.; Hahn-Banach Theorem.
HAHNBAN1,: Anna Justyna Milewska.; The Hahn Banach Theorem in the Vector Space over the Field of Complex Numbers.
HAUSDORF,: Adam Grabowski.; On the Hausdorff Distance Between Compact Subsets.
HEINE,: Agata Darmochwal and Yatsuka Nakamura.; Heine--Borel's Covering Theorem.
HERMITAN,: Jaroslaw Kotowicz.; Hermitan Functionals. Canonical Construction of Scalar Product in Quotient Vector Space.
HESSENBE,: Eugeniusz Kusak and Wojciech Leonczuk.; Hessenberg Theorem.
HEYTING1,: Andrzej Trybulec.; Algebra of Normal Forms Is a Heyting Algebra.
HEYTING2,: Adam Grabowski.; Lattice of Substitutions is a Heyting Algebra.
HEYTING3,: Adam Grabowski.; The Incompleteness of the Lattice of Substitutions.
HIDDEN,: Library Committee.; Mizar Built-in Notions.
HILBASIS,: Jonathan Backer and Piotr Rudnicki.; Hilbert Basis Theorem.
HILBERT1,: Adam Grabowski.; Hilbert Positive Propositional Calculus.
HILBERT2,: Andrzej Trybulec.; Defining by Structural Induction in the Positive Propositional Language.
HILBERT3,: Andrzej Trybulec.; The Canonical Formulae.
HOMOTHET,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; Homotheties and Shears in Affine Planes.

IDEA_1,: Yasushi Fuwa and Yoshinori Fujisawa.; Algebraic Group on Fixed-length Bit Integer and its Adaptation to IDEA Cryptography.
IDEAL_1,: Jonathan Backer, Piotr Rudnicki, and Christoph Schwarzweller.; Ring Ideals.
INCPROJ,: Wojciech Leonczuk and Krzysztof Prazmowski.; Incidence Projective Spaces.
INCSP_1,: Wojciech A. Trybulec.; Axioms of Incidency.
INDEX_1,: Grzegorz Bancerek.; Indexed Category.
INSTALG1,: Grzegorz Bancerek.; Institution of Many Sorted Algebras. Part I: Signature Reduct of an Algebra.
INT_1,: Michal J. Trybulec.; Integers.
INT_2,: Rafal Kwiatek and Grzegorz Zwara.; The Divisibility of Integers and Integer Relatively Primes.
INT_3,: Christoph Schwarzweller.; The Ring of Integers, Euclidean Rings and Modulo Integers.
INTEGRA1,: Noboru Endou and Artur Kornilowicz.; The Definition of the Riemann Definite Integral and some Related Lemmas.
INTEGRA2,: Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.; Scalar Multiple of Riemann Definite Integral.
INTEGRA3,: Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.; Darboux's Theorem.
INTEGRA4,: Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.; Integrability of Bounded Total Functions.
INTEGRA5,: Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.; Definition of Integrability for Partial Functions from $\Bbb R$ to $\Bbb R$ and Integrability for Continuous Functions.
INTPRO_1,: Takao Inoue.; Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator. Part I.
IRRAT_1,: Freek Wiedijk.; Irrationality of $e$.
ISOCAT_1,: Andrzej Trybulec.; Isomorphisms of Categories.
ISOCAT_2,: Andrzej Trybulec.; Some Isomorphisms Between Functor Categories.

JCT_MISC,: Andrzej Trybulec.; Some Lemmas for the Jordan Curve Theorem.
JGRAPH_1,: Yatsuka Nakamura.; Graph Theoretical Properties of Arcs in the Plane and Fashoda Meet Theorem.
JGRAPH_2,: Yatsuka Nakamura.; On Outside Fashoda Meet Theorem.
JGRAPH_3,: Yatsuka Nakamura.; On the Simple Closed Curve Property of the Circle and the Fashoda Meet Theorem for It.
JGRAPH_4,: Yatsuka Nakamura.; Fan Homeomorphisms in the Plane.
JGRAPH_5,: Yatsuka Nakamura.; General Fashoda Meet Theorem for Unit Circle.
JGRAPH_6,: Yatsuka Nakamura.; General Fashoda Meet Theorem for Unit Circle and Square.
JORDAN1,: Yatsuka Nakamura and Jaroslaw Kotowicz.; The Jordan's Property for Certain Subsets of the Plane.
JORDAN10,: Artur Kornilowicz.; Properties of the External Approximation of Jordan's Curve.
JORDAN11,: Andrzej Trybulec.; Preparing the Internal Approximations of Simple Closed Curves.
JORDAN12,: Mariusz Giero.; On the General Position of Special Polygons.
JORDAN13,: Andrzej Trybulec.; Introducing Spans.
JORDAN14,: Robert Milewski.; Properties of the Internal Approximation of Jordan's Curve.
JORDAN15,: Robert Milewski.; Properties of the Upper and Lower Sequence on the Cage.
JORDAN16,: Andrzej Trybulec and Yatsuka Nakamura.; On the Decomposition of a Simple Closed Curve into Two Arcs.
JORDAN17,: Artur Kornilowicz.; The Ordering of Points on a Curve. Part III.
JORDAN18,: Artur Kornilowicz.; The Ordering of Points on a Curve. Part IV.
JORDAN19,: Robert Milewski.; On the Upper and Lower Approximations of the Curve.
JORDAN1A,: Artur Kornilowicz, Robert Milewski, Adam Naumowicz, and Andrzej Trybulec.; Gauges and Cages. Part I.
JORDAN1B,: Robert Milewski, Andrzej Trybulec, Artur Kornilowicz, and Adam Naumowicz.; Some Properties of Cells and Arcs.
JORDAN1C,: Adam Grabowski, Artur Kornilowicz, and Andrzej Trybulec.; Some Properties of Cells and Gauges.
JORDAN1D,: Artur Kornilowicz and Robert Milewski.; Gauges and Cages. Part II.
JORDAN1E,: Robert Milewski.; Upper and Lower Sequence of a Cage.
JORDAN1F,: Adam Naumowicz.; Some Remarks on Finite Sequences on Go-Boards.
JORDAN1G,: Robert Milewski.; Upper and Lower Sequence on the Cage. Part II.
JORDAN1H,: Andrzej Trybulec.; More on External Approximation of a Continuum.
JORDAN1I,: Adam Naumowicz and Robert Milewski.; Some Remarks on Clockwise Oriented Sequences on Go-boards.
JORDAN1J,: Robert Milewski.; Upper and Lower Sequence on the Cage, Upper and Lower Arcs.
JORDAN1K,: Andrzej Trybulec.; On the Minimal Distance Between Sets in Euclidean Space.
JORDAN2B,: Roman Matuszewski and Yatsuka Nakamura.; Projections in $n$-Dimensional Euclidean Space to Each Coordinates.
JORDAN2C,: Yatsuka Nakamura, Andrzej Trybulec, and Czeslaw Bylinski.; Bounded Domains and Unbounded Domains.
JORDAN3,: Yatsuka Nakamura and Roman Matuszewski.; Reconstructions of Special Sequences.
JORDAN4,: Yatsuka Nakamura, Roman Matuszewski, and Adam Grabowski.; Subsequences of Standard Special Circular Sequences in $\cal E^2_\rm T$.
JORDAN5A,: Adam Grabowski and Yatsuka Nakamura.; Some Properties of Real Maps.
JORDAN5B,: Adam Grabowski and Yatsuka Nakamura.; The Ordering of Points on a Curve. Part I.
JORDAN5C,: Adam Grabowski and Yatsuka Nakamura.; The Ordering of Points on a Curve. Part II.
JORDAN5D,: Yatsuka Nakamura and Adam Grabowski.; Bounding Boxes for Special Sequences in $\calE^2$.
JORDAN6,: Yatsuka Nakamura and Andrzej Trybulec.; A Decomposition of Simple Closed Curves and the Order of Their Points.
JORDAN7,: Yatsuka Nakamura.; On the Dividing Function of the Simple Closed Curve into Segments.
JORDAN8,: Czeslaw Bylinski.; Gauges.
JORDAN9,: Czeslaw Bylinski and Mariusz Zynel.; Cages - the External Approximation of Jordan's Curve.
JORDAN_A,: Andrzej Trybulec.; On the Segmentation of a Simple Closed Curve.

KNASTER,: Piotr Rudnicki and Andrzej Trybulec.; Fixpoints in Complete Lattices.
KURATO_1,: Lilla Krystyna Baginska and Adam Grabowski.; On the Kuratowski Closure-Complement Problem.
KURATO_2,: Adam Grabowski.; On the Kuratowski Limit Operators.

L_HOSPIT,: Malgorzata Korolkiewicz.; The de l'Hospital Theorem.
LANG1,: Patricia L. Carlson and Grzegorz Bancerek.; Context-Free Grammar --- Part I.
LATSUBGR,: Janusz Ganczarski.; On the Lattice of Subgroups of a Group.
LATTICE2,: Andrzej Trybulec.; Finite Join and Finite Meet, and Dual Lattices.
LATTICE3,: Grzegorz Bancerek.; Complete Lattices.
LATTICE4,: Jolanta Kamienska and Jaroslaw Stanislaw Walijewski.; Homomorphisms of Lattices, Finite Join and Finite Meet.
LATTICE5,: Jaroslaw Gryko.; The Jonsson Theorem.
LATTICE6,: Christoph Schwarzweller.; Noetherian Lattices.
LATTICE7,: Marek Dudzicz.; Representation Theorem for Finite Distributive Lattices.
LATTICE8,: Mariusz \Lapinski.; The Jonsson Theorem about the Representation of Modular Lattices.
LATTICES,: Stanislaw Zukowski.; Introduction to Lattice Theory.
LFUZZY_0,: Takashi Mitsuishi and Grzegorz Bancerek.; Lattice of Fuzzy Sets.
LFUZZY_1,: Takashi Mitsuishi and Grzegorz Bancerek.; Transitive Closure of Fuzzy Relations.
LIMFUNC1,: Jaroslaw Kotowicz.; The Limit of a Real Function at Infinity.
LIMFUNC2,: Jaroslaw Kotowicz.; The One-Side Limits of a Real Function at a Point.
LIMFUNC3,: Jaroslaw Kotowicz.; The Limit of a Real Function at a Point.
LIMFUNC4,: Jaroslaw Kotowicz.; The Limit of a Composition of Real Functions.
LMOD_5,: Michal Muzalewski and Wojciech Skaba.; Linear Independence in Left Module over Domain.
LMOD_6,: Michal Muzalewski.; Submodules.
LMOD_7,: Michal Muzalewski.; Domains of Submodules, Join and Meet of Finite Sequences of Submodules and Quotient Modules.
LOPBAN_1,: Yasunari Shidama.; Banach Space of Bounded Linear Operators.
LOPCLSET,: Jaroslaw Stanislaw Walijewski.; Representation Theorem for Boolean Algebras.
LUKASI_1,: Grzegorz Bancerek, Agata Darmochwal, and Andrzej Trybulec.; Propositional Calculus.

MARGREL1,: Edmund Woronowicz.; Many-Argument Relations.
MATRIX_1,: Katarzyna Jankowska.; Matrices. Abelian Group of Matrices.
MATRIX_2,: Katarzyna Jankowska.; Transpose Matrices and Groups of Permutations.
MATRIX_3,: Katarzyna Zawadzka.; The Product and the Determinant of Matrices with Entries in a Field.
MATRIX_4,: Yatsuka Nakamura and Hiroshi Yamazaki.; Calculation of Matrices of Field Elements. Part I.
MATRLIN,: Robert Milewski.; Associated Matrix of Linear Map.
MBOOLEAN,: Artur Kornilowicz.; Definitions and Basic Properties of Boolean and Union of Many Sorted Sets.
MCART_1,: Andrzej Trybulec.; Tuples, Projections and Cartesian Products.
MCART_2,: Michal Muzalewski and Wojciech Skaba.; $N$-Tuples and Cartesian Products for $n=5$.
MCART_3,: Michal Muzalewski and Wojciech Skaba.; $N$-Tuples and Cartesian Products for $n=6$.
MCART_4,: Michal Muzalewski and Wojciech Skaba.; $N$-Tuples and Cartesian Products for $n=7$.
MCART_5,: Michal Muzalewski and Wojciech Skaba.; $N$-Tuples and Cartesian Products for $n=8$.
MCART_6,: Michal Muzalewski and Wojciech Skaba.; $N$-Tuples and Cartesian Products for $n=9$.
MEASURE1,: Jozef Bialas.; The $\sigma$-additive Measure Theory.
MEASURE2,: Jozef Bialas.; Several Properties of the $\sigma$-additive Measure.
MEASURE3,: Jozef Bialas.; Completeness of the $\sigma$-Additive Measure. Measure Theory.
MEASURE4,: Jozef Bialas.; Properties of Caratheodor's Measure.
MEASURE5,: Jozef Bialas.; Properties of the Intervals of Real Numbers.
MEASURE6,: Jozef Bialas.; Some Properties of the Intervals.
MEASURE7,: Jozef Bialas.; The One-Dimensional Lebesgue Measure.
MEMBERED,: Andrzej Trybulec.; On the Sets Inhabited by Numbers.
MESFUNC1,: Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.; Definitions and Basic Properties of Measurable Functions.
MESFUNC2,: Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.; The Measurability of Extended Real Valued Functions.
METRIC_1,: Stanislawa Kanas, Adam Lecko, and Mariusz Startek.; Metric Spaces.
METRIC_2,: Adam Lecko and Mariusz Startek.; On Pseudometric Spaces.
METRIC_3,: Stanislawa Kanas and Jan Stankiewicz.; Metrics in Cartesian Product.
METRIC_4,: Stanislawa Kanas and Adam Lecko.; Metrics in the Cartesian Product --- Part II.
METRIC_6,: Stanislawa Kanas and Adam Lecko.; Sequences in Metric Spaces.
MIDSP_1,: Michal Muzalewski.; Midpoint algebras.
MIDSP_2,: Michal Muzalewski.; Atlas of Midpoint Algebra.
MIDSP_3,: Michal Muzalewski.; Reper Algebras.
MOD_1,: Michal Muzalewski and Wojciech Skaba.; Groups, Rings, Left- and Right-Modules.
MOD_2,: Michal Muzalewski.; Rings and Modules --- Part II.
MOD_3,: Michal Muzalewski.; Free Modules.
MOD_4,: Michal Muzalewski.; Opposite Rings, Modules and Their Morphisms.
MODAL_1,: Alicia de la Cruz.; Introduction to Modal Propositional Logic.
MODCAT_1,: Michal Muzalewski.; Category of Left Modules.
MONOID_0,: Grzegorz Bancerek.; Monoids.
MONOID_1,: Grzegorz Bancerek.; Monoid of Multisets and Subsets.
MSAFREE,: Beata Perkowska.; Free Many Sorted Universal Algebra.
MSAFREE1,: Andrzej Trybulec.; A Scheme for Extensions of Homomorphisms of Many Sorted Algebras.
MSAFREE2,: Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.; Preliminaries to Circuits, II.
MSAFREE3,: Grzegorz Bancerek and Artur Kornilowicz.; Yet Another Construction of Free Algebra.
MSALIMIT,: Adam Grabowski.; Inverse Limits of Many Sorted Algebras.
MSATERM,: Grzegorz Bancerek.; Terms Over Many Sorted Universal Algebra.
MSINST_1,: Adam Grabowski.; Examples of Category Structures.
MSSCYC_1,: Czeslaw Bylinski and Piotr Rudnicki.; The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. Part I.
MSSCYC_2,: Czeslaw Bylinski and Piotr Rudnicki.; The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. Part II.
MSSUBFAM,: Artur Kornilowicz.; Certain Facts about Families of Subsets of Many Sorted Sets.
MSSUBLAT,: Adam Naumowicz and Agnieszka Julia Marasik.; The Correspondence Between Lattices of Subalgebras of Universal Algebras and Many Sorted Algebras.
MSUALG_1,: Andrzej Trybulec.; Many Sorted Algebras.
MSUALG_2,: Ewa Burakowska.; Subalgebras of Many Sorted Algebra. Lattice of Subalgebras.
MSUALG_3,: Malgorzata Korolkiewicz.; Homomorphisms of Many Sorted Algebras.
MSUALG_4,: Malgorzata Korolkiewicz.; Many Sorted Quotient Algebra.
MSUALG_5,: Robert Milewski.; Lattice of Congruences in Many Sorted Algebra.
MSUALG_6,: Grzegorz Bancerek.; Translations, Endomorphisms, and Stable Equational Theories.
MSUALG_7,: Robert Milewski.; More on the Lattice of Many Sorted Equivalence Relations.
MSUALG_8,: Robert Milewski.; More on the Lattice of Congruences in Many Sorted Algebra.
MSUALG_9,: Artur Kornilowicz.; On the Trivial Many Sorted Algebras and Many Sorted Congruences.
MSUHOM_1,: Adam Grabowski.; The Correspondence Between Homomorphisms of Universal Algebra \& Many Sorted Algebra.
MULTOP_1,: Michal Muzalewski and Wojciech Skaba.; Three-Argument Operations and Four-Argument Operations.

NAT_1,: Grzegorz Bancerek.; The Fundamental Properties of Natural Numbers.
NAT_2,: Robert Milewski.; Natural Numbers.
NAT_LAT,: Marek Chmur.; The Lattice of Natural Numbers and The Sublattice of it. The Set of Prime Numbers..
NATTRA_1,: Andrzej Trybulec.; Natural transformations. Discrete categories.
NECKLA_2,: Krzysztof Retel.; The Class of Series-Parallel Graphs. Part II.
NECKLACE,: Krzysztof Retel.; The Class of Series -- Parallel Graphs. Part I.
NET_1,: Waldemar Korczynski.; Some Elementary Notions of the Theory of Petri Nets.
NEWTON,: Rafal Kwiatek.; Factorial and Newton Coefficients.
NORMFORM,: Andrzej Trybulec.; Algebra of Normal Forms.
NORMSP_1,: Jan Popiolek.; Real Normed Space.
NUMBERS,: Andrzej Trybulec.; Subsets of Complex Numbers.
NUMERALS,: Library Committee.; Numerals --- Requirements.

O_RING_1,: Michal Muzalewski and Leslaw W. Szczerba.; Ordered Rings - Part I.
O_RING_2,: Michal Muzalewski and Leslaw W. Szczerba.; Ordered Rings - Part II.
O_RING_3,: Michal Muzalewski and Leslaw W. Szczerba.; Ordered Rings - Part III.
OPENLATT,: Jolanta Kamienska.; Representation Theorem for Heyting Lattices.
OPOSET_1,: Markus Moschner.; Basic Notions and Properties of Orthoposets.
OPPCAT_1,: Czeslaw Bylinski.; Opposite Categories and Contravariant Functors.
ORDERS_1,: Wojciech A. Trybulec.; Partially Ordered Sets.
ORDERS_2,: Wojciech A. Trybulec and Grzegorz Bancerek.; Kuratowski - Zorn Lemma.
ORDERS_3,: Adam Grabowski.; On the Category of Posets.
ORDERS_4,: Marta Pruszynska and Marek Dudzicz.; On the Isomorphism between Finite Chains.
ORDINAL1,: Grzegorz Bancerek.; The Ordinal Numbers.
ORDINAL2,: Grzegorz Bancerek.; Sequences of Ordinal Numbers.
ORDINAL3,: Grzegorz Bancerek.; Ordinal Arithmetics.
ORDINAL4,: Grzegorz Bancerek.; Increasing and Continuous Ordinal Sequences.
ORTSP_1,: Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski.; Construction of a bilinear symmetric form in orthogonal vector space.
OSAFREE,: Josef Urban.; Free Order Sorted Universal Algebra.
OSALG_1,: Josef Urban.; Order Sorted Algebras.
OSALG_2,: Josef Urban.; Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras.
OSALG_3,: Josef Urban.; Homomorphisms of Order Sorted Algebras.
OSALG_4,: Josef Urban.; Order Sorted Quotient Algebra.

PAPDESAF,: Krzysztof Prazmowski.; Fanoian, Pappian and Desarguesian Affine Spaces.
PARDEPAP,: Krzysztof Prazmowski and Krzysztof Radziszewski.; Elementary Variants of Affine Configurational Theorems.
PARSP_1,: Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski.; Parallelity Spaces.
PARSP_2,: Eugeniusz Kusak and Wojciech Leonczuk.; Fano-Desargues Parallelity Spaces.
PARTFUN1,: Czeslaw Bylinski.; Partial Functions.
PARTFUN2,: Jaroslaw Kotowicz.; Partial Functions from a Domain to a Domain.
PARTIT1,: Shunichi Kobayashi and Kui Jia.; A Theory of Partitions. Part I.
PARTIT_2,: Andrzej Trybulec.; Classes of Independent Partitions.
PASCH,: Henryk Oryszczyszyn, Krzysztof Prazmowski, and Malgorzata Prazmowska.; Classical and Non-classical Pasch Configurations in Ordered Affine Planes.
PBOOLE,: Andrzej Trybulec.; Many-sorted Sets.
PCOMPS_1,: Leszek Borys.; Paracompact and Metrizable Spaces.
PCOMPS_2,: Leszek Borys.; On Paracompactness of Metrizable Spaces.
PENCIL_1,: Adam Naumowicz.; On Segre's Product of Partial Line Spaces.
PENCIL_2,: Adam Naumowicz.; On Cosets in Segre's Product of Partial Linear Spaces.
PEPIN,: Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu.; Public-Key Cryptography and Pepin's Test for the Primality of Fermat Numbers.
PETRI,: Pauline N. Kawamoto, Yasushi Fuwa, and Yatsuka Nakamura.; Basic Petri Net Concepts.
PNPROC_1,: Grzegorz Bancerek, Mitsuru Aoki, Akio Matsumoto, and Yasunari Shidama.; Processes in Petri nets.
POLYALG1,: Ewa Gradzka.; The Algebra of Polynomials.
POLYEQ_1,: Xiquan Liang.; Solving Roots of Polynomial Equations of Degree 2 and 3 with Real Coefficients.
POLYEQ_2,: Xiquan Liang.; Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients.
POLYNOM1,: Piotr Rudnicki and Andrzej Trybulec.; Multivariate Polynomials with Arbitrary Number of Variables.
POLYNOM2,: Christoph Schwarzweller and Andrzej Trybulec.; The Evaluation of Multivariate Polynomials.
POLYNOM3,: Robert Milewski.; The Ring of Polynomials.
POLYNOM4,: Robert Milewski.; The Evaluation of Polynomials.
POLYNOM5,: Robert Milewski.; Fundamental Theorem of Algebra.
POLYNOM6,: Barbara Dzienis.; On Polynomials with Coefficients in a Ring of Polynomials.
POLYNOM7,: Christoph Schwarzweller.; More on Multivariate Polynomials: Monomials and Constant Polynomials.
POLYRED,: Christoph Schwarzweller.; Polynomial Reduction.
POWER,: Konrad Raczkowski and Andrzej Nedzusiak.; Real Exponents and Logarithms.
PRALG_1,: Beata Madras.; Product of Family of Universal Algebras.
PRALG_2,: Beata Madras.; Products of Many Sorted Algebras.
PRALG_3,: Mariusz Giero.; More on Products of Many Sorted Algebras.
PRE_CIRC,: Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.; Preliminaries to Circuits, I.
PRE_FF,: Grzegorz Bancerek and Piotr Rudnicki.; Two Programs for \bf SCM. Part I - Preliminaries.
PRE_TOPC,: Beata Padlewska and Agata Darmochwal.; Topological Spaces and Continuous Functions.
PRELAMB,: Wojciech Zielonka.; Preliminaries to the Lambek Calculus.
PREPOWER,: Konrad Raczkowski.; Integer and Rational Exponents.
PRGCOR_1,: Yatsuka Nakamura.; Correctness of Non Overwriting Programs. Part I.
PROB_1,: Andrzej Nedzusiak.; $\sigma$-Fields and Probability.
PROB_2,: Andrzej Nedzusiak.; Probability.
PROCAL_1,: Jan Popiolek and Andrzej Trybulec.; Calculus of Propositions.
PROJDES1,: Eugeniusz Kusak.; Desargues Theorem In Projective 3-Space.
PROJPL_1,: Michal Muzalewski.; Projective Planes.
PROJRED1,: Eugeniusz Kusak and Wojciech Leonczuk.; Incidence Projective Space (a reduction theorem in a plane).
PROJRED2,: Eugeniusz Kusak, Wojciech Leonczuk, and Krzysztof Prazmowski.; On Projections in Projective Planes --- Part II.
PRVECT_1,: Anna Lango and Grzegorz Bancerek.; Product of Families of Groups and Vector Spaces.
PSCOMP_1,: Czeslaw Bylinski and Piotr Rudnicki.; Bounding Boxes for Compact Sets in $\calE^2$.
PUA2MSS1,: Grzegorz Bancerek.; Minimal Signature for Partial Algebra.
PYTHTRIP,: Freek Wiedijk.; Pythagorean Triples.
PZFMISC1,: Artur Kornilowicz.; Some Basic Properties of Many Sorted Sets.

QC_LANG1,: Piotr Rudnicki and Andrzej Trybulec.; A First Order Language.
QC_LANG2,: Grzegorz Bancerek.; Connectives and Subformulae of the First Order Language.
QC_LANG3,: Czeslaw Bylinski and Grzegorz Bancerek.; Variables in Formulae of the First Order Language.
QC_LANG4,: Oleg Okhotnikov.; The Subformula Tree of a Formula of the First Order Language.
QMAX_1,: Pawel Sadowski, Andrzej Trybulec, and Konrad Raczkowski.; The Fundamental Logic Structure in Quantum Mechanics.
QUANTAL1,: Grzegorz Bancerek.; Quantales.
QUIN_1,: Jan Popiolek.; Quadratic Inequalities.
QUOFIELD,: Christoph Schwarzweller.; The Field of Quotients Over an Integral Domain.

RADIX_1,: Yoshinori Fujisawa and Yasushi Fuwa.; Definitions of Radix-$2^k$ Signed-Digit Number and its Adder Algorithm.
RADIX_2,: Yasushi Fuwa and Yoshinori Fujisawa.; High-Speed Algorithms for RSA Cryptograms.
RADIX_3,: Masaaki Niimura and Yasushi Fuwa.; Improvement of Radix-$2^k$ Signed-Digit Number for High Speed Circuit.
RADIX_4,: Masaaki Niimura and Yasushi Fuwa.; High Speed Adder Algorithm with Radix-$2^k$ Sub Signed-Digit Number.
RADIX_5,: Masaaki Niimura and Yasushi Fuwa.; Magnitude Relation Properties of Radix-$2^k$ SD Number.
RADIX_6,: Masaaki Niimura and Yasushi Fuwa.; High Speed Modulo Calculation Algorithm with Radix-$2^k$ SD Number.
RAT_1,: Andrzej Kondracki.; Basic Properties of Rational Numbers.
RCOMP_1,: Konrad Raczkowski and Pawel Sadowski.; Topological Properties of Subsets in Real Numbers.
RCOMP_2,: Yatsuka Nakamura.; Half Open Intervals in Real Numbers.
REAL,: Library Committee.; Basic Properties of Real Numbers --- Requirements.
REAL_1,: Krzysztof Hryniewiecki.; Basic Properties of Real Numbers.
REAL_2,: Andrzej Kondracki.; Equalities and Inequalities in Real Numbers.
REAL_LAT,: Marek Chmur.; The Lattice of Real Numbers. The Lattice of Real Functions.
REALSET1,: Jozef Bialas.; Group and Field Definitions.
REALSET2,: Jozef Bialas.; Properties of Fields.
REALSET3,: Jozef Bialas.; Several Properties of Fields. Field Theory.
REARRAN1,: Yuji Sakai and Jaroslaw Kotowicz.; Introduction to Theory of Rearrangement.
RECDEF_1,: Krzysztof Hryniewiecki.; Recursive Definitions.
RELAT_1,: Edmund Woronowicz.; Relations and Their Basic Properties.
RELAT_2,: Edmund Woronowicz and Anna Zalewska.; Properties of Binary Relations.
RELOC,: Yasushi Tanaka.; Relocatability.
RELSET_1,: Edmund Woronowicz.; Relations Defined on Sets.
REVROT_1,: Andrzej Trybulec.; Rotating and Reversing.
REWRITE1,: Grzegorz Bancerek.; Reduction Relations.
RFINSEQ,: Jaroslaw Kotowicz.; Functions and Finite Sequences of Real Numbers.
RFINSEQ2,: Yatsuka Nakamura.; Sorting Operators for Finite Sequences.
RFUNCT_1,: Jaroslaw Kotowicz.; Partial Functions from a Domain to the Set of Real Numbers.
RFUNCT_2,: Jaroslaw Kotowicz.; Properties of Real Functions.
RFUNCT_3,: Jaroslaw Kotowicz and Yuji Sakai.; Properties of Partial Functions from a Domain to the Set of Real Numbers.
RFUNCT_4,: Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.; Introduction to Several Concepts of Convexity and Semicontinuity for Function from $\Bbb R$ to $\Bbb R$.
RINGCAT1,: Michal Muzalewski.; Category of Rings.
RLSUB_1,: Wojciech A. Trybulec.; Subspaces and Cosets of Subspaces in Real Linear Space.
RLSUB_2,: Wojciech A. Trybulec.; Operations on Subspaces in Real Linear Space.
RLVECT_1,: Wojciech A. Trybulec.; Vectors in Real Linear Space.
RLVECT_2,: Wojciech A. Trybulec.; Linear Combinations in Real Linear Space.
RLVECT_3,: Wojciech A. Trybulec.; Basis of Real Linear Space.
RLVECT_4,: Wojciech A. Trybulec.; Subspaces of Real Linear Space Generated by One, Two, or Three Vectors and Their Cosets.
RLVECT_5,: Jing-Chao Chen.; The Steinitz Theorem and the Dimension of a Real Linear Space.
RMOD_2,: Michal Muzalewski and Wojciech Skaba.; Submodules and Cosets of Submodules in Right Module over Associative Ring.
RMOD_3,: Michal Muzalewski and Wojciech Skaba.; Operations on Submodules in Right Module over Associative Ring.
RMOD_4,: Michal Muzalewski and Wojciech Skaba.; Linear Combinations in Right Module over Associative Ring.
RMOD_5,: Michal Muzalewski and Wojciech Skaba.; Linear Independence in Right Module over Domain.
ROBBINS1,: Adam Grabowski.; Robbins Algebras vs. Boolean Algebras.
ROBBINS2,: Wioletta Truszkowska and Adam Grabowski.; On the Two Short Axiomatizations of Ortholattices.
ROLLE,: Jaroslaw Kotowicz, Konrad Raczkowski, and Pawel Sadowski.; Average Value Theorems for Real Functions of One Variable.
ROUGHS_1,: Adam Grabowski.; Basic Properties of Rough Sets and Rough Membership Function.
RPR_1,: Jan Popiolek.; Introduction to Probability.
RSSPACE,: Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama.; Real Linear Space of Real Sequences.
RSSPACE2,: Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama.; Hilbert Space of Real Sequences.
RSSPACE3,: Yasumasa Suzuki, Noboru Endou, and Yasunari Shidama.; Banach Space of Absolute Summable Real Sequences.
RSSPACE4,: Yasumasa Suzuki.; Banach Space of Bounded Real Sequences.
RUSUB_1,: Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama.; Subspaces and Cosets of Subspace of Real Unitary Space.
RUSUB_2,: Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama.; Operations on Subspaces in Real Unitary Space.
RUSUB_3,: Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama.; Linear Combinations in Real Unitary Space.
RUSUB_4,: Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama.; Dimension of Real Unitary Space.
RUSUB_5,: Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama.; Topology of Real Unitary Space.
RVSUM_1,: Czeslaw Bylinski.; The Sum and Product of Finite Sequences of Real Numbers.

SCHEME1,: Jaroslaw Kotowicz.; Schemes of Existence of Some Types of Functions.
SCHEMS_1,: Stanislaw T. Czuba.; Schemes.
SCM_1,: Grzegorz Bancerek and Piotr Rudnicki.; Development of Terminology for \bf SCM.
SCM_COMP,: Grzegorz Bancerek and Piotr Rudnicki.; A Compiler of Arithmetic Expressions for SCM.
SCM_HALT,: Jing-Chao Chen and Yatsuka Nakamura.; Initialization Halting Concepts and Their Basic Properties of \SCMFSA.
SCMBSORT,: Jing-Chao Chen and Yatsuka Nakamura.; Bubble Sort on \SCMFSA.
SCMFSA10,: Artur Kornilowicz.; On the Instructions of \SCMFSA.
SCMFSA6A,: Andrzej Trybulec, Yatsuka Nakamura, and Noriko Asamoto.; On the Compositions of Macro Instructions. Part I.
SCMFSA6B,: Noriko Asamoto, Yatsuka Nakamura, Piotr Rudnicki, and Andrzej Trybulec.; On the Composition of Macro Instructions. Part II.
SCMFSA6C,: Noriko Asamoto, Yatsuka Nakamura, Piotr Rudnicki, and Andrzej Trybulec.; On the Composition of Macro Instructions. Part III.
SCMFSA7B,: Noriko Asamoto.; Constant Assignment Macro Instructions of \SCMFSA. Part II.
SCMFSA8A,: Noriko Asamoto.; Conditional Branch Macro Instructions of \SCMFSA. Part I.
SCMFSA8B,: Noriko Asamoto.; Conditional Branch Macro Instructions of \SCMFSA. Part II.
SCMFSA8C,: Noriko Asamoto.; The \tt loop and \tt Times Macroinstruction for \SCMFSA.
SCMFSA9A,: Piotr Rudnicki.; The \tt while Macro Instructions of \SCMFSA. Part II.
SCMFSA_1,: Andrzej Trybulec, Yatsuka Nakamura, and Piotr Rudnicki.; An Extension of \bf SCM.
SCMFSA_2,: Andrzej Trybulec, Yatsuka Nakamura, and Piotr Rudnicki.; The \SCMFSA Computer.
SCMFSA_3,: Andrzej Trybulec and Yatsuka Nakamura.; Computation in \SCMFSA.
SCMFSA_4,: Andrzej Trybulec and Yatsuka Nakamura.; Modifying Addresses of Instructions of \SCMFSA.
SCMFSA_5,: Andrzej Trybulec and Yatsuka Nakamura.; Relocability for \SCMFSA.
SCMFSA_7,: Noriko Asamoto.; Some Multi Instructions Defined by Sequence of Instructions of \SCMFSA.
SCMFSA_9,: Jing-Chao Chen.; While Macro Instructions of \SCMFSA.
SCMISORT,: Jing-Chao Chen.; Insert Sort on \SCMFSA.
SCMP_GCD,: Jing-Chao Chen.; Recursive Euclide Algorithm.
SCMPDS_1,: Jing-Chao Chen.; A Small Computer Model with Push-Down Stack.
SCMPDS_2,: Jing-Chao Chen.; The SCMPDS Computer and the Basic Semantics of its Instructions.
SCMPDS_3,: Jing-Chao Chen.; Computation and Program Shift in the SCMPDS Computer.
SCMPDS_4,: Jing-Chao Chen.; The Construction and Shiftability of Program Blocks for SCMPDS.
SCMPDS_5,: Jing-Chao Chen.; Computation of Two Consecutive Program Blocks for SCMPDS.
SCMPDS_6,: Jing-Chao Chen.; The Construction and Computation of Conditional Statements for SCMPDS.
SCMPDS_7,: Jing-Chao Chen and Piotr Rudnicki.; The Construction and Computation of for-loop Programs for SCMPDS.
SCMPDS_8,: Jing-Chao Chen.; The Construction and Computation of While-Loop Programs for SCMPDS.
SCMPDS_9,: Artur Kornilowicz and Yasunari Shidama.; SCMPDS Is Not Standard.
SCMRING1,: Artur Kornilowicz.; The Construction of \SCM over Ring.
SCMRING2,: Artur Kornilowicz.; The Basic Properties of \SCM over Ring.
SCMRING3,: Artur Kornilowicz.; The Properties of Instructions of SCM over Ring.
SCPINVAR,: Jing-Chao Chen.; Justifying the Correctness of the Fibonacci Sequence and the Euclide Algorithm by Loop-Invariant.
SCPISORT,: Jing-Chao Chen.; Insert Sort on SCMPDS.
SCPQSORT,: Jing-Chao Chen.; Quick Sort on SCMPDS.
SEMI_AF1,: Eugeniusz Kusak and Krzysztof Radziszewski.; Semi-Affine Space.
SEQ_1,: Jaroslaw Kotowicz.; Real Sequences and Basic Operations on Them.
SEQ_2,: Jaroslaw Kotowicz.; Convergent Sequences and the Limit of Sequences.
SEQ_4,: Jaroslaw Kotowicz.; Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers.
SEQFUNC,: Beata Perkowska.; Functional Sequence from a Domain to a Domain.
SEQM_3,: Jaroslaw Kotowicz.; Monotone Real Sequences. Subsequences.
SERIES_1,: Konrad Raczkowski and Andrzej Nedzusiak.; Series.
SETFAM_1,: Beata Padlewska.; Families of Sets.
SETWISEO,: Andrzej Trybulec.; Semilattice Operations on Finite Subsets.
SETWOP_2,: Czeslaw Bylinski.; Semigroup Operations on Finite Subsets.
SF_MASTR,: Piotr Rudnicki and Andrzej Trybulec.; Memory Handling for \SCMFSA.
SFMASTR1,: Piotr Rudnicki.; On the Composition of Non-parahalting Macro Instructions.
SFMASTR2,: Piotr Rudnicki.; Another \tt times Macro Instruction.
SFMASTR3,: Piotr Rudnicki.; The \tt for (going up) Macro Instruction.
SGRAPH1,: Yozo Toda.; The Formalization of Simple Graphs.
SIN_COS,: Yuguang Yang and Yasunari Shidama.; Trigonometric Functions and Existence of Circle Ratio.
SIN_COS2,: Takashi Mitsuishi and Yuguang Yang.; Properties of the Trigonometric Function.
SIN_COS3,: Takashi Mitsuishi, Noboru Endou, and Keiji Ohkubo.; Trigonometric Functions on Complex Space.
SPPOL_1,: Yatsuka Nakamura and Czeslaw Bylinski.; Extremal Properties of Vertices on Special Polygons, Part I.
SPPOL_2,: Czeslaw Bylinski and Yatsuka Nakamura.; Special Polygons.
SPRECT_1,: Andrzej Trybulec and Yatsuka Nakamura.; On the Rectangular Finite Sequences of the Points of the Plane.
SPRECT_2,: Andrzej Trybulec and Yatsuka Nakamura.; On the Order on a Special Polygon.
SPRECT_3,: Andrzej Trybulec and Yatsuka Nakamura.; Some Properties of Special Polygonal Curves.
SPRECT_4,: Andrzej Trybulec and Yatsuka Nakamura.; On the Components of the Complement of a Special Polygonal Curve.
SPRECT_5,: Andrzej Trybulec and Yatsuka Nakamura.; Again on the Order on a Special Polygon.
SQUARE_1,: Andrzej Trybulec and Czeslaw Bylinski.; Some Properties of Real Numbers Operations: min, max, square, and square root.
STRUCT_0,: Library Committee.; Preliminaries to Structures.
SUB_METR,: Adam Lecko and Mariusz Startek.; Submetric Spaces --- Part I.
SUBSET,: Library Committee.; Basic Properties of Subsets --- Requirements.
SUBSET_1,: Zinaida Trybulec.; Properties of Subsets.
SUBSTLAT,: Adam Grabowski.; Lattice of Substitutions.
SUPINF_1,: Jozef Bialas.; Infimum and Supremum of the Set of Real Numbers. Measure Theory.
SUPINF_2,: Jozef Bialas.; Series of Positive Real Numbers. Measure Theory.
SYMSP_1,: Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski.; Construction of a bilinear antisymmetric form in symplectic vector space.
SYSREL,: Waldemar Korczynski.; Some Properties of Binary Relations.

T_0TOPSP,: Mariusz Zynel and Adam Guzowski.; \Tzero\ Topological Spaces.
T_1TOPSP,: Adam Naumowicz and Mariusz \Lapinski.; On \Tone\ Reflex of Topological Space.
TARSKI,: Andrzej Trybulec.; Tarski Grothendieck Set Theory.
TAXONOM1,: Mariusz Giero and Roman Matuszewski.; Lower Tolerance. Preliminaries to Wroclaw Taxonomy.
TAXONOM2,: Mariusz Giero.; Hierarchies and Classifications of Sets.
TBSP_1,: Alicia de la Cruz.; Totally Bounded Metric Spaces.
TDGROUP,: Grzegorz Lewandowski and Krzysztof Prazmowski.; A Construction of an Abstract Space of Congruence of Vectors.
TDLAT_1,: Toshihiko Watanabe.; The Lattice of Domains of a Topological Space.
TDLAT_2,: Zbigniew Karno and Toshihiko Watanabe.; Completeness of the Lattices of Domains of a Topological Space.
TDLAT_3,: Zbigniew Karno.; The Lattice of Domains of an Extremally Disconnected Space.
TERMORD,: Christoph Schwarzweller.; Term Orders.
TEX_1,: Zbigniew Karno.; On Discrete and Almost Discrete Topological Spaces.
TEX_2,: Zbigniew Karno.; Maximal Discrete Subspaces of Almost Discrete Topological Spaces.
TEX_3,: Zbigniew Karno.; On Nowhere and Everywhere Dense Subspaces of Topological Spaces.
TEX_4,: Zbigniew Karno.; Maximal Anti-Discrete Subspaces of Topological Spaces.
TMAP_1,: Zbigniew Karno.; Continuity of Mappings over the Union of Subspaces.
TOLER_1,: Krzysztof Hryniewiecki.; Relations of Tolerance.
TOPGRP_1,: Artur Kornilowicz.; The Definition and Basic Properties of Topological Groups.
TOPMETR,: Agata Darmochwal and Yatsuka Nakamura.; Metric Spaces as Topological Spaces --- Fundamental Concepts.
TOPMETR2,: Yatsuka Nakamura and Agata Darmochwal.; Some Facts about Union of Two Functions and Continuity of Union of Functions.
TOPMETR3,: Yatsuka Nakamura and Andrzej Trybulec.; Sequences of Metric Spaces and an Abstract Intermediate Value Theorem.
TOPREAL1,: Agata Darmochwal and Yatsuka Nakamura.; The Topological Space $\calE^2_\rmT$. Arcs, Line Segments and Special Polygonal Arcs.
TOPREAL2,: Agata Darmochwal and Yatsuka Nakamura.; The Topological Space $\calE^2_\rmT$. Simple Closed Curves.
TOPREAL3,: Yatsuka Nakamura and Jaroslaw Kotowicz.; Basic Properties of Connecting Points with Line Segments in $\calE^2_\rmT$.
TOPREAL4,: Yatsuka Nakamura and Jaroslaw Kotowicz.; Connectedness Conditions Using Polygonal Arcs.
TOPREAL5,: Yatsuka Nakamura and Andrzej Trybulec.; Intermediate Value Theorem and Thickness of Simple Closed Curves.
TOPREAL6,: Artur Kornilowicz.; Compactness of the Bounded Closed Subsets of $\cal E^2_\rm T$.
TOPREAL7,: Artur Kornilowicz.; Homeomorphism between [:$\cal E^i_\rm T, \cal E^j_\rm T$:] and $\cal E^i+j_\rm T$.
TOPREAL8,: Andrzej Trybulec.; More on the Finite Sequences on the Plane.
TOPRNS_1,: Agnieszka Sakowicz, Jaroslaw Gryko, and Adam Grabowski.; Sequences in $\calE^N_\rmT$.
TOPS_1,: Miroslaw Wysocki and Agata Darmochwal.; Subsets of Topological Spaces.
TOPS_2,: Agata Darmochwal.; Families of Subsets, Subspaces and Mappings in Topological Spaces.
TOPS_3,: Zbigniew Karno.; Remarks on Special Subsets of Topological Spaces.
TRANSGEO,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; Transformations in Affine Spaces.
TRANSLAC,: Henryk Oryszczyszyn and Krzysztof Prazmowski.; Translations in Affine Planes.
TREAL_1,: Toshihiko Watanabe.; The Brouwer Fixed Point Theorem for Intervals.
TREES_1,: Grzegorz Bancerek.; Introduction to Trees.
TREES_2,: Grzegorz Bancerek.; K\"onig's Lemma.
TREES_3,: Grzegorz Bancerek.; Sets and Functions of Trees and Joining Operations of Trees.
TREES_4,: Grzegorz Bancerek.; Joining of Decorated Trees.
TREES_9,: Grzegorz Bancerek.; Subtrees.
TREES_A,: Oleg Okhotnikov.; Replacement of Subtrees in a Tree.
TRIANG_1,: Beata Madras.; On the Concept of the Triangulation.
TSEP_1,: Zbigniew Karno.; Separated and Weakly Separated Subspaces of Topological Spaces.
TSEP_2,: Zbigniew Karno.; On a Duality Between Weakly Separated Subspaces of Topological Spaces.
TSP_1,: Zbigniew Karno.; On Kolmogorov Topological Spaces.
TSP_2,: Zbigniew Karno.; Maximal Kolmogorov Subspaces of a Topological Space as Stone Retracts of the Ambient Space.
TURING_1,: Jing-Chao Chen and Yatsuka Nakamura.; Introduction to Turing Machines.
TWOSCOMP,: Katsumi Wasaki and Pauline N. Kawamoto.; 2's Complement Circuit.

UNIALG_1,: Jaroslaw Kotowicz, Beata Madras, and Malgorzata Korolkiewicz.; Basic Notation of Universal Algebra.
UNIALG_2,: Ewa Burakowska.; Subalgebras of the Universal Algebra. Lattices of Subalgebras.
UNIALG_3,: Miroslaw Jan Paszek.; On the Lattice of Subalgebras of a Universal Algebra.
UNIFORM1,: Yatsuka Nakamura and Andrzej Trybulec.; Lebesgue's Covering Lemma, Uniform Continuity and Segmentation of Arcs.
UNIROOTS,: Broderic Arneson and Piotr Rudnicki.; Primitive Roots of Unity and Cyclotomic Polynomials.
UPROOTS,: Piotr Rudnicki.; Little Bezout Theorem (Factor Theorem).
URYSOHN1,: Jozef Bialas and Yatsuka Nakamura.; Dyadic Numbers and T$_4$ Topological Spaces.
URYSOHN2,: Jozef Bialas and Yatsuka Nakamura.; Some Properties of Dyadic Numbers and Intervals.
URYSOHN3,: Jozef Bialas and Yatsuka Nakamura.; The Urysohn Lemma.

VALUAT_1,: Edmund Woronowicz.; Interpretation and Satisfiability in the First Order Logic.
VECTMETR,: Robert Milewski.; Real Linear-Metric Space and Isometric Functions.
VECTSP10,: Jaroslaw Kotowicz.; Quotient Vector Spaces and Functionals.
VECTSP_1,: Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski.; Abelian Groups, Fields and Vector Spaces.
VECTSP_2,: Michal Muzalewski.; Construction of Rings and Left-, Right-, and Bi-Modules over a Ring.
VECTSP_3,: Wojciech A. Trybulec.; Finite Sums of Vectors in Vector Space.
VECTSP_4,: Wojciech A. Trybulec.; Subspaces and Cosets of Subspaces in Vector Space.
VECTSP_5,: Wojciech A. Trybulec.; Operations on Subspaces in Vector Space.
VECTSP_6,: Wojciech A. Trybulec.; Linear Combinations in Vector Space.
VECTSP_7,: Wojciech A. Trybulec.; Basis of Vector Space.
VECTSP_8,: Andrzej Iwaniuk.; On the Lattice of Subspaces of a Vector Space.
VECTSP_9,: Mariusz Zynel.; The Steinitz Theorem and the Dimension of a Vector Space.
VFUNCT_1,: Hiroshi Yamazaki and Yasunari Shidama.; Algebra of Vector Functions.

WAYBEL10,: Grzegorz Bancerek.; Closure Operators and Subalgebras.
WAYBEL11,: Andrzej Trybulec.; Scott Topology.
WAYBEL12,: Artur Kornilowicz.; On the Baire Category Theorem.
WAYBEL13,: Robert Milewski.; Algebraic and Arithmetic Lattices. Part I.
WAYBEL14,: Czeslaw Bylinski and Piotr Rudnicki.; The Scott Topology. Part II.
WAYBEL15,: Robert Milewski.; Algebraic and Arithmetic Lattices. Part II.
WAYBEL16,: Robert Milewski.; Completely-Irreducible Elements.
WAYBEL17,: Adam Grabowski.; Scott-Continuous Functions.
WAYBEL18,: Jaroslaw Gryko.; Injective Spaces.
WAYBEL19,: Grzegorz Bancerek.; The Lawson Topology.
WAYBEL20,: Piotr Rudnicki.; Kernel Projections and Quotient Lattices.
WAYBEL21,: Grzegorz Bancerek.; Lawson Topology in Continuous Lattices.
WAYBEL22,: Piotr Rudnicki.; Representation Theorem for Free Continuous Lattices.
WAYBEL23,: Robert Milewski.; Bases of Continuous Lattices.
WAYBEL24,: Adam Grabowski.; Scott-Continuous Functions. Part II.
WAYBEL25,: Artur Kornilowicz and Jaroslaw Gryko.; Injective Spaces. Part II.
WAYBEL26,: Grzegorz Bancerek.; Continuous Lattices of Maps between T$_0$ Spaces.
WAYBEL27,: Grzegorz Bancerek and Adam Naumowicz.; Function Spaces in the Category of Directed Suprema Preserving Maps.
WAYBEL28,: Bartlomiej Skorulski.; Lim-Inf Convergence.
WAYBEL29,: Grzegorz Bancerek and Adam Naumowicz.; The Characterization of the Continuity of Topologies.
WAYBEL30,: Artur Kornilowicz.; Meet Continuous Lattices Revisited.
WAYBEL31,: Robert Milewski.; Weights of Continuous Lattices.
WAYBEL32,: Ewa Gradzka.; On the Order-consistent Topology of Complete and Uncomplete Lattices.
WAYBEL33,: Grzegorz Bancerek and Noboru Endou.; Compactness of Lim-inf Topology.
WAYBEL34,: Grzegorz Bancerek.; Duality Based on Galois Connection. Part I.
WAYBEL35,: Artur Kornilowicz.; Morphisms Into Chains. Part I.
WAYBEL_0,: Grzegorz Bancerek.; Directed Sets, Nets, Ideals, Filters, and Maps.
WAYBEL_1,: Czeslaw Bylinski.; Galois Connections.
WAYBEL_2,: Artur Kornilowicz.; Meet -- Continuous Lattices.
WAYBEL_3,: Grzegorz Bancerek.; The ``Way-Below'' Relation.
WAYBEL_4,: Adam Grabowski.; Auxiliary and Approximating Relations.
WAYBEL_5,: Mariusz Zynel.; The Equational Characterization of Continuous Lattices.
WAYBEL_6,: Beata Madras.; Irreducible and Prime Elements.
WAYBEL_7,: Grzegorz Bancerek.; Prime Ideals and Filters.
WAYBEL_8,: Robert Milewski.; Algebraic Lattices.
WAYBEL_9,: Artur Kornilowicz.; On the Topological Properties of Meet-Continuous Lattices.
WEDDWITT,: Broderic Arneson, Matthias Baaz, and Piotr Rudnicki.; Witt's Proof of the Wedderburn Theorem.
WEIERSTR,: Jozef Bialas and Yatsuka Nakamura.; The Theorem of Weierstrass.
WELLFND1,: Piotr Rudnicki and Andrzej Trybulec.; On Same Equivalents of Well-foundedness.
WELLORD1,: Grzegorz Bancerek.; The Well Ordering Relations.
WELLORD2,: Grzegorz Bancerek.; Zermelo Theorem and Axiom of Choice.
WELLSET1,: Bogdan Nowak and Slawomir Bialecki.; Zermelo's Theorem.
WSIERP_1,: Andrzej Kondracki.; The Chinese Remainder Theorem.

XBOOLE_0,: Library Committee.; Boolean Properties of Sets --- Definitions.
XBOOLE_1,: Library Committee.; Boolean Properties of Sets --- Theorems.
XCMPLX_0,: Library Committee.; Complex Numbers --- Basic Definitions.
XCMPLX_1,: Library Committee.; Complex Numbers --- Basic Theorems.
XREAL_0,: Library Committee.; Introduction to Arithmetic of Real Numbers.

YELLOW10,: Artur Kornilowicz.; The Properties of Product of Relational Structures.
YELLOW11,: Adam Naumowicz.; On the Characterization of Modular and Distributive Lattices.
YELLOW12,: Artur Kornilowicz.; On the Characterization of Hausdorff Spaces.
YELLOW13,: Artur Kornilowicz.; Introduction to Meet-Continuous Topological Lattices.
YELLOW14,: Jaroslaw Gryko and Artur Kornilowicz.; Some Properties of Isomorphism between Relational Structures. On the Product of Topological Spaces.
YELLOW15,: Robert Milewski.; Components and Basis of Topological Spaces.
YELLOW16,: Grzegorz Bancerek.; Retracts and Inheritance.
YELLOW17,: Bartlomiej Skorulski.; The Tichonov Theorem.
YELLOW18,: Grzegorz Bancerek.; Concrete Categories.
YELLOW19,: Grzegorz Bancerek, Noboru Endou, and Yuji Sakai.; On the Characterizations of Compactness.
YELLOW20,: Grzegorz Bancerek.; Miscellaneous Facts about Functors.
YELLOW21,: Grzegorz Bancerek.; Categorial Background for Duality Theory.
YELLOW_0,: Grzegorz Bancerek.; Bounds in Posets and Relational Substructures.
YELLOW_1,: Adam Grabowski and Robert Milewski.; Boolean Posets, Posets under Inclusion and Products of Relational Structures.
YELLOW_2,: Mariusz Zynel and Czeslaw Bylinski.; Properties of Relational Structures, Posets, Lattices and Maps.
YELLOW_3,: Artur Kornilowicz.; Cartesian Products of Relations and Relational Structures.
YELLOW_4,: Artur Kornilowicz.; Definitions and Properties of the Join and Meet of Subsets.
YELLOW_5,: Agnieszka Julia Marasik.; Miscellaneous Facts about Relation Structure.
YELLOW_6,: Andrzej Trybulec.; Moore-Smith Convergence.
YELLOW_7,: Grzegorz Bancerek.; Duality in Relation Structures.
YELLOW_8,: Andrzej Trybulec.; Baire Spaces, Sober Spaces.
YELLOW_9,: Grzegorz Bancerek.; Bases and Refinements of Topologies.
YONEDA_1,: Miroslaw Wojciechowski.; Yoneda Embedding.

ZF_COLLA,: Grzegorz Bancerek.; The Contraction Lemma.
ZF_FUND1,: Andrzej Kondracki.; Mostowski's Fundamental Operations --- Part I.
ZF_FUND2,: Grzegorz Bancerek and Andrzej Kondracki.; Mostowski's Fundamental Operations --- Part II.
ZF_LANG,: Grzegorz Bancerek.; A Model of ZF Set Theory Language.
ZF_LANG1,: Grzegorz Bancerek.; Replacing of Variables in Formulas of ZF Theory.
ZF_MODEL,: Grzegorz Bancerek.; Models and Satisfiability.
ZF_REFLE,: Grzegorz Bancerek.; The Reflection Theorem.
ZFMISC_1,: Czeslaw Bylinski.; Some Basic Properties of Sets.
ZFMODEL1,: Grzegorz Bancerek.; Properties of ZF Models.
ZFMODEL2,: Grzegorz Bancerek.; Definable Functions.
ZFREFLE1,: Grzegorz Bancerek.; Consequences of the Reflection Theorem.

[Journal of Formalized Mathematics, Mizar Home Page]