@MISC{GROUP_21.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Yamazaki, Hiroshi and Okazaki, Hiroyuki and Shidama, Yasunari},
  TITLE = {Conservation Rules of Direct Sum Decomposition of Groups},
  SECTION1 = {Preliminaries},
  SECTION2 = {Conservation Rule of Direct Sum Decomposition for Substitution of Subscript Set},
  SECTION3 = {Conservation Rule of Direct Sum Decomposition for Flattening},
  SECTION4 = {Conservation Rule of Direct Sum Decomposition for Layering},
  DAY = {31},
  MONTH = {December},
  YEAR = {2015},
  ADDRESS1 = {Shinshu University, Nagano, JAPAN},
  ADDRESS2 = {Shinshu University, Nagano, JAPAN},
  ADDRESS3 = {Shinshu University, Nagano, JAPAN},
  ADDRESS4 = {Shinshu University, Nagano, JAPAN},
  SUMMARY = {In this article, conservation rules of the direct
    sum decomposition of groups are mainly discussed.
    In the first section, we prepare miscellaneous definitions and theorems
    for further formalization in Mizar \cite{Mizar:2015}.
    In the next three sections, we formalized the fact that
    the property of direct
    sum decomposition is preserved against the subsitutions of the subscript set,
    flattening of direct sum, and layering of direct sum, respectively.
    We referred to \cite{rotman1995introduction}, \cite{robinson2012course}
    \cite{BourbakiAlgI} and \cite{lang-algebra} in the formalization.}}

@book{rotman1995introduction,
  AUTHOR    = {Rotman, J.J.},
  TITLE     = {An Introduction to the Theory of Groups},
  PUBLISHER = {Springer},
  YEAR      = {1995}}

@book{robinson2012course,
  AUTHOR    = {Robinson, D.},
  TITLE     = {A Course in the Theory of Groups},
  PUBLISHER = {Springer New York},
  YEAR      = {2012}}

@BOOK{BourbakiAlgI,
  AUTHOR    = {Bourbaki, Nicolas},
  TITLE     = {Elements of Mathematics. {A}lgebra {I}. {C}hapters 1-3},
  PUBLISHER = {Springer-Verlag},
  YEAR      = {1989},
  ADDRESS   = {Berlin, Heidelberg, New York, London, Paris, Tokyo}}

@BOOK{lang-algebra,
  AUTHOR    = {Lang, Serge},
  TITLE     = {Algebra},
  PUBLISHER = {Springer},
  YEAR      = {2005},
  EDITION   = {3rd}}
