A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Yatsuka Nakamura, Artur Korni{\l}owicz, Nagato Oya, Yasunari Shidama.
The Real Vector Spaces of
Finite Sequences are Finite Dimensional,
Formalized Mathematics 17(1),
pages 1-9, 2009. MML Identifier:
EUCLID_7 Summary:
In this paper we show the finite dimensionality of real linear spaces with their
carriers equal ${\cal R}^n$. We also give the standard basis of such spaces. For
the set ${\cal R}^n$ we introduce the concepts of linear manifold subsets and orthogonal subsets.
The cardinality of orthonormal basis of discussed spaces is proved to equal $n$.
Bo Li, Yanping Zhuang, Bing Xie, Pan Wang.
Several Integrability Formulas
of Some Functions, Orthogonal Polynomials and Norm Functions,
Formalized Mathematics 17(1),
pages 11-21, 2009. MML Identifier:
INTEGRA9 Summary:
In this article, we give several integrability formulas of some functions including
the trigonometric function and the index function
\cite{Chen:1978}.
We also give the definitions of the orthogonal polynomial and norm function,
and some of their important properties
\cite{Renhong:1999}.
Bo Li, Yanping Zhuang, Yanhong Men, Xiquan Liang.
Several Integrability
Formulas of Special Functions. {P}art {II},
Formalized Mathematics 17(1),
pages 23-35, 2009. MML Identifier:
INTEGR11 Summary:
In this article, we give several differentiation and integrability formulas
of special and composite functions including the trigonometric function,
the hyperbolic function and the polynomial function
\cite{Chen:1978}.
Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama, Yatsuka Nakamura.
Cell {P}etri Net Concepts,
Formalized Mathematics 17(1),
pages 37-42, 2009. MML Identifier:
PETRI_2 Summary:
Based on the Petri net definitions and theorems already formalized in
\cite{PETRI.ABS},
with this article, we developed the concept
of ``Cell Petri Nets". It is based on
\cite{Kawamoto-Nakamura:1996}.
In a cell Petri net we introduce the notions of colors and colored states
of a Petri net, connecting mappings for linking two Petri nets, firing rules
for transitions, and the synthesis of two or more Petri nets.
Artur Korni{\l}owicz.
Arithmetic Operations on Functions
from Sets into Functional Sets,
Formalized Mathematics 17(1),
pages 43-60, 2009. MML Identifier:
VALUED_2 Summary:
In this paper we introduce sets containing number-valued functions. Different arithmetic
operations on maps between any set and such functional sets are later defined.