Formalized Mathematics    (ISSN 1426-2630)
Volume 5, Number 3 (1996): pdf, ps, dvi.
  1. Yatsuka Nakamura, Piotr Rudnicki. Vertex Sequences Induced by Chains, Formalized Mathematics 5(3), pages 297-304, 1996. MML Identifier: GRAPH_2
    Summary: In the three preliminary sections to the article we define two operations on finite sequences which seem to be of general interest. The first is the $cut$ operation that extracts a contiguous chunk of a finite sequence from a position to a position. The second operation is a glueing catenation that given two finite sequences catenates them with removal of the first element of the second sequence. The main topic of the article is to define an operation which for a given chain in a graph returns the sequence of vertices through which the chain passes. We define the exact conditions when such an operation is uniquely definable. This is done with the help of the so called two-valued alternating finite sequences. We also prove theorems about the existence of simple chains which are subchains of a given chain. In order to do this we define the notion of a finite subsequence of a typed finite sequence.
  2. Andrzej Iwaniuk. On the Lattice of Subspaces of a Vector Space, Formalized Mathematics 5(3), pages 305-308, 1996. MML Identifier: VECTSP_8
    Summary:
  3. Janusz Ganczarski. On the Lattice of Subgroups of a Group, Formalized Mathematics 5(3), pages 309-312, 1996. MML Identifier: LATSUBGR
    Summary:
  4. Miroslaw Jan Paszek. On the Lattice of Subalgebras of a Universal Algebra, Formalized Mathematics 5(3), pages 313-316, 1996. MML Identifier: UNIALG_3
    Summary:
  5. Andrzej Trybulec. On the Decomposition of Finite Sequences, Formalized Mathematics 5(3), pages 317-322, 1996. MML Identifier: FINSEQ_6
    Summary:
  6. Yatsuka Nakamura, Andrzej Trybulec. Decomposing a Go-Board into Cells, Formalized Mathematics 5(3), pages 323-328, 1996. MML Identifier: GOBOARD5
    Summary:
  7. Grzegorz Bancerek. Indexed Category, Formalized Mathematics 5(3), pages 329-337, 1996. MML Identifier: INDEX_1
    Summary: The concept of indexing of a category (a part of indexed category, see \cite{TarleckiBurstallGoguen}) is introduced as a pair formed by a many sorted category and a many sorted functor. The indexing of a category $C$ against to \cite{TarleckiBurstallGoguen} is not a functor but it can be treated as a functor from $C$ into some categorial category (see \cite{CAT_5.ABS}). The goal of the article is to work out the notation necessary to define institutions (see \cite{GoguenBurstall}).
  8. Robert Milewski. Associated Matrix of Linear Map, Formalized Mathematics 5(3), pages 339-345, 1996. MML Identifier: MATRLIN
    Summary:
  9. Andrzej Trybulec. On the Geometry of a Go-Board, Formalized Mathematics 5(3), pages 347-352, 1996. MML Identifier: GOBOARD6
    Summary:
  10. Jozef Bialas, Yatsuka Nakamura. The Theorem of Weierstrass, Formalized Mathematics 5(3), pages 353-359, 1996. MML Identifier: WEIERSTR
    Summary:
  11. Jozef Bialas, Yatsuka Nakamura. Dyadic Numbers and T$_4$ Topological Spaces, Formalized Mathematics 5(3), pages 361-366, 1996. MML Identifier: URYSOHN1
    Summary:
  12. Grzegorz Bancerek, Yatsuka Nakamura. Full Adder Circuit. Part I, Formalized Mathematics 5(3), pages 367-380, 1996. MML Identifier: FACIRC_1
    Summary: We continue the formalisation of circuits started by Piotr Rudnicki, Andrzej Trybulec, Pauline Kawamoto, and the second author in \cite{PRE_CIRC.ABS}, \cite{MSAFREE2.ABS}, \cite{CIRCUIT1.ABS}, \cite{CIRCUIT2.ABS}. The first step in proving properties of full $n$-bit adder circuit, i.e. 1-bit adder, is presented. We employ the notation of combining circuits introduced in \cite{CIRCCOMB.ABS}.
  13. Grzegorz Bancerek. Continuous, Stable, and Linear Maps of Coherence Spaces, Formalized Mathematics 5(3), pages 381-393, 1996. MML Identifier: COHSP_1
    Summary:
  14. Artur Kornilowicz. Some Basic Properties of Many Sorted Sets, Formalized Mathematics 5(3), pages 395-399, 1996. MML Identifier: PZFMISC1
    Summary:
  15. Oleg Okhotnikov. Replacement of Subtrees in a Tree, Formalized Mathematics 5(3), pages 401-403, 1996. MML Identifier: TREES_A
    Summary: This paper is based on previous works \cite{TREES_1.ABS}, \cite{TREES_2.ABS} in which the operation replacement of subtree in a tree has been defined. We extend this notion for arbitrary non empty antichain.
  16. Grzegorz Bancerek. Minimal Signature for Partial Algebra, Formalized Mathematics 5(3), pages 405-414, 1996. MML Identifier: PUA2MSS1
    Summary: The concept of characterizing of partial algebras by many sorted signature is introduced, i.e. we say that a signature $S$ characterizes a partial algebra $A$ if there is an $S$-algebra whose sorts form a partition of the carrier of algebra $A$ and operations are formed from operations of $A$ by the partition. The main result is that for any partial algebra there is the minimal many sorted signature which characterizes the algebra. The minimality means that there are signature endomorphisms from any signature which characterizes the algebra $A$ onto the minimal one.
  17. Oleg Okhotnikov. The Subformula Tree of a Formula of the First Order Language, Formalized Mathematics 5(3), pages 415-422, 1996. MML Identifier: QC_LANG4
    Summary: A continuation of \cite{QC_LANG3.ABS}. The notions of list of immediate constituents of a formula and subformula tree of a formula are introduced. The some propositions related to these notions are proved.
  18. Mariusz Zynel. The Steinitz Theorem and the Dimension of a Vector Space, Formalized Mathematics 5(3), pages 423-428, 1996. MML Identifier: VECTSP_9
    Summary: The main purpose of the paper is to define the dimension of an abstract vector space. The dimension of a finite-dimensional vector space is, by the most common definition, the number of vectors in a basis. Obviously, each basis contains the same number of vectors. We prove the Steinitz Theorem together with Exchange Lemma in the second section. The Steinitz Theorem says that each linearly-independent subset of a vector space has cardinality less than any subset that generates the space, moreover it can be extended to a basis. Further we review some of the standard facts involving the dimension of a vector space. Additionally, in the last section, we introduce two notions: the family of subspaces of a fixed dimension and the pencil of subspaces. Both of them can be applied in the algebraic representation of several geometries.
  19. Andrzej Trybulec. On the Go-Board of a Standard Special Circular Sequence, Formalized Mathematics 5(3), pages 429-438, 1996. MML Identifier: GOBOARD7
    Summary:
  20. Jaroslaw Gryko. On the Monoid of Endomorphisms of Universal Algebra and Many Sorted Algebra, Formalized Mathematics 5(3), pages 439-442, 1996. MML Identifier: ENDALG
    Summary:
  21. Andrzej Trybulec. More on Segments on a Go-Board, Formalized Mathematics 5(3), pages 443-450, 1996. MML Identifier: GOBOARD8
    Summary: We continue the preparatory work for the Jordan Curve Theorem.
  22. Artur Kornilowicz. Certain Facts about Families of Subsets of Many Sorted Sets, Formalized Mathematics 5(3), pages 451-456, 1996. MML Identifier: MSSUBFAM
    Summary:
  23. Beata Madras. On the Concept of the Triangulation, Formalized Mathematics 5(3), pages 457-462, 1996. MML Identifier: TRIANG_1
    Summary: