http://hdl.handle.net/11320/3332 Sat, 26 Sep 2026 12:18:40 GMT 2026-09-26T12:18:40Z http://hdl.handle.net/11320/21097 Tytuł: Open Mapping Theorem Autorzy: Sakurai, Hideki; Kunimune, Hisayoshi; Shidama, Yasunari Abstrakt: In this article we formalize one of the most important the orems 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. Tue, 01 Jan 2008 00:00:00 GMT http://hdl.handle.net/11320/21097 2008-01-01T00:00:00Z http://hdl.handle.net/11320/21093 Tytuł: Several Differentiation Formulas of Special Functions. Part VII Autorzy: Ge, Fuguo; Xie, Bing Abstrakt: 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. Tue, 01 Jan 2008 00:00:00 GMT http://hdl.handle.net/11320/21093 2008-01-01T00:00:00Z http://hdl.handle.net/11320/21092 Tytuł: Stability of the 4-2 Binary Addition Circuit Cells. Part I Autorzy: Wasaki, Katsumi Abstrakt: 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. Tue, 01 Jan 2008 00:00:00 GMT http://hdl.handle.net/11320/21092 2008-01-01T00:00:00Z http://hdl.handle.net/11320/21090 Tytuł: BCI-homomorphisms Autorzy: Ding, Yuzhong; Ge, Fuguo; Wu, Chenglong Abstrakt: 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. Tue, 01 Jan 2008 00:00:00 GMT http://hdl.handle.net/11320/21090 2008-01-01T00:00:00Z