Volume 16 (2008): Issue 4 (December 2008)

The article presents well known facts about eigenvalues of linear transformation of a vector space (see [13]). I formalize main dependencies between eigenvalues and the diagram of the matrix of a linear transformation over a finite-dimensional vector space. Finally, I formalize the subspace called a generalized eigenspace for the eigenvalue λ and show its basic properties.

MML identifier: VECTSP11, version: 7.9.03 4.108.1028

In this paper I present the Jordan Matrix Decomposition Theorem which states that an arbitrary square matrix M over an algebraically closed field can be decomposed into the form

where S is an invertible matrix and J is a matrix in a Jordan canonical form, i.e. a special type of block diagonal matrix in which each block consists of Jordan blocks (see [13]).

MML identifier: MATRIXJ2, version: 7.9.01 4.101.1015

In this article we prove the Fatou's Lemma and Lebesgue's Convergence Theorem [10].

MML identifier: MESFUN10, version: 7.9.01 4.101.1015

In this article, we defined a variety of extended Riemann integrals and proved that such integration is linear. Furthermore, we defined the one-sided Laplace transform and proved the linearity of that operator.

MML identifier: INTEGR10, version: 7.9.01 4.101.1015

In this article, we formalized the notion of the integral of a complex-valued function considered as a sum of its real and imaginary parts. Then we defined the measurability and integrability in this context, and proved the linearity and several other basic properties of complex-valued measurable functions. The set of properties showed in this paper is based on [15], where the case of real-valued measurable functions is considered.

MML identifier: MESFUN6C, version: 7.9.01 4.101.1015

The paper includes elements of the theory of matroids [23]. The formalization is done according to [12].

MML identifier: MATROID0, version: 7.9.03 4.108.1028

In this article, we define two single-variable functions SVF1 and SVF2, then discuss partial differentiation of real binary functions by dint of one variable function SVF1 and SVF2. The main properties of partial differentiation are shown [7].

MML identifier: PDIFF 2, version: 7.9.03 4.104.1021

This text includes verification of the basic algorithm in Simple On-the-fly Automatic Verification of Linear Temporal Logic (LTL). LTL formula can be transformed to Buchi automaton, and this transforming algorithm is mainly used at Simple On-the-fly Automatic Verification. In this article, we verified the transforming algorithm itself. At first, we prepared some definitions and operations for transforming. And then, we defined the Buchi automaton and verified the transforming algorithm.

MML identifier: MODELC 3, version: 7.9.03 4.108.1028

This article introduces definitions of circulant matrices, line-and column-circulant matrices as well as anti-circular matrices and describes their main properties.

MML identifier: MATRIX16, version: 7.9.03 4.108.1028

This article contains some definitions and properties refering to function spaces formed by partial functions defined over a measurable space. We formalized a function space, the so-called L¹ space and proved that the space turns out to be a normed space. The formalization of a real function space was given in [16]. The set of all function forms additive group. Here addition is defined by point-wise addition of two functions. However it is not true for partial functions. The set of partial functions does not form an additive group due to lack of right zeroed condition. Therefore, firstly we introduced a kind of a quasi-linear space, then, we introduced the definition of an equivalent relation of two functions which are almost everywhere equal (=_a.e.), thirdly we formalized a linear space by taking the quotient of a quasi-linear space by the relation (=_a.e.).

MML identifier: LPSPACE1, version: 7.9.03 4.108.1028

In this article the notion of the power of an element of BCI-algebra and its period in the book [11], sections 1.4 to 1.5 are firstly given. Then the definition of BCI-homomorphism is defined and the fundamental theorem of homomorphism, the first isomorphism theorem and the second isomorphism theorem are proved following the book [9], section 1.6.

MML identifier: BCIALG 6, version: 7.9.03 4.108.1028

To evaluate our formal verification method on a real-size calculation circuit, in this article, we continue to formalize the concept of the 4-2 Binary Addition Cell primitives (FTAs) to define the structures of calculation units for a very fast multiplication algorithm for VLSI implementation [11]. We define the circuit structure of four-types FTAs, TYPE-0 to TYPE-3, using the series constructions of the Generalized Full Adder Circuits (GFAs) that generalized adder to have for each positive and negative weights to inputs and outputs [15]. We then successfully prove its circuit stability of the calculation outputs after four-steps. The motivation for this research is to establish a technique based on formalized mathematics and its applications for calculation circuits with high reliability.

MML identifier: FTACELL1, version: 7.9.03 4.108.1028

In this article, we prove a series of differentiation identities [2] involving the arctan and arccot functions and specific combinations of special functions including trigonometric and exponential functions.

MML identifier: FDIFF 11, version: 7.10.01 4.111.1036

In this article we formalize one of the most important theorems of linear operator theory the Open Mapping Theorem commonly used in a standard book such as [8] in chapter 2.4.2. It states that a surjective continuous linear operator between Banach spaces is an open map.

MML identifier: LOPBAN 6, version: 7.10.01 4.111.1036