http://hdl.handle.net/11320/3663 2026-06-01T16:03:30Z http://hdl.handle.net/11320/3694 Tytuł: Isometric Differentiable Functions on Real Normed Space Autorzy: Futa, Yuichi; Endou, Noboru; Shidama, Yasunari Abstrakt: In this article, we formalize isometric differentiable functions on real normed space [17], and their properties. 2013-01-01T00:00:00Z http://hdl.handle.net/11320/3696 Tytuł: Submodule of free Z-module Autorzy: Futa, Yuichi; Okazaki, Hiroyuki; Shidama, Yasunari Abstrakt: In this article, we formalize a free Z-module and its property. In particular, we formalize the vector space of rational field corresponding to a free Z-module and prove formally that submodules of a free Z-module are free. Z-module is necassary for lattice problems - LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm and cryptographic systems with lattice [20]. Some theorems in this article are described by translating theorems in [11] into theorems of Z-module, however their proofs are different. 2013-01-01T00:00:00Z http://hdl.handle.net/11320/3695 Tytuł: Differential Equations on Functions from R into Real Banach Space Autorzy: Narita, Keiko; Endou, Noboru; Shidama, Yasunari Abstrakt: In this article, we describe the differential equations on functions from R into real Banach space. The descriptions are based on the article [20]. As preliminary to the proof of these theorems, we proved some properties of differentiable functions on real normed space. For the proof we referred to descriptions and theorems in the article [21] and the article [32]. And applying the theorems of Riemann integral introduced in the article [22], we proved the ordinary differential equations on real Banach space. We referred to the methods of proof in [30]. 2013-01-01T00:00:00Z http://hdl.handle.net/11320/3693 Tytuł: Formulation of Cell Petri Nets Autorzy: Jitsukawa, Mitsuru; Kawamoto, Pauline N.; Shidama, Yasunari Abstrakt: Based on the Petri net definitions and theorems already formalized in the Mizar article [13], in this article we were able to formalize the definition of cell Petri nets. It is based on [12]. Colored Petri net has already been defined in [11]. In addition, the conditions of the firing rule and the colored set to this definition, that defines the cell Petri nets are further extended to CPNT.i further. The synthesis of two Petri nets was introduced in [11] and in this work the definition is extended to produce the synthesis of a family of colored Petri nets. Specifically, the extension to a CPNT family is performed by specifying how to link the outbound transitions of each colored Petri net to the place elements of other nets to form a neighborhood relationship. Finally, the activation of colored Petri nets was formalized. 2013-01-01T00:00:00Z