@MISC{RELSET_3.MIZ,
  AUTHOR = {Koch, Sebastian},
  TITLE = {Some Number Relations},
  SECTION1 = {Preliminaries},
  SECTION2 = {Successor Relation},
  SECTION3 = {Additive Relation},
  SECTION4 = {Multiplicative Relation},
  SECTION5 = {Modulo Relation},
  DAY = {27},
  MONTH = {December},
  YEAR = {2024},
  ADDRESS1 = {Mainz, Germany\\\href{mailto:fly.high.android@gmail.com}{fly.high.android@gmail.com}},
  SUMMARY = {In this article some number relations are formalized in the Mizar system.},
  INTRODUCTION = {Binary relations are interesting for the study of simple (di)graphs
  and in their own right (cf. \cite{AGT}, \cite{GRELAT}, \cite{SIMPLE}).
  The relationship between binary relations and graphs has been formalized in \cite{GLUNIR00.ABS}.
  Here some simple binary relations are introduced to the MML (cf. \cite{BancerekJAR:2018}, \cite{FourDecades}):
  the successor relation, an additive and multiplicative relation and the modulo relation.
  These can be used in the future for e.g. canonical (directed) path or cycle graphs (where the vertices are just numbers) including
  the ray and double-ray graph. More complicated structures can be obtained by combining some of these binary relations,
  although that is out of scope for this article.}}

@Article{BancerekJAR:2018,
  author={Bancerek, Grzegorz and Byli{\'{n}}ski, Czes{\l}aw and Grabowski, Adam and Korni{\l}owicz, Artur and Matuszewski, Roman and Naumowicz, Adam and P{\k{a}}k, Karol},
  title={The Role of the {M}izar {M}athematical {L}ibrary for Interactive Proof Development in {M}izar},
  journal={Journal of Automated Reasoning},
  year={2018},
  volume={61},
  number={1},
  pages={9--32},
  doi={10.1007/s10817-017-9440-6},
  url={https://doi.org/10.1007/s10817-017-9440-6}
}
@Article{FourDecades,
  author={Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
  title={Four Decades of {M}izar},
  journal={Journal of Automated Reasoning},
  year={2015},
  volume={55},
  number={3},
  pages={191--198},
  issn={1573-0670},
  doi={10.1007/s10817-015-9345-1}
}
@book{DIESTEL,
  TITLE = {Graph theory},
  VOLUME = {Graduate texts in mathematics ; 173},
  AUTHOR = {Diestel, Reinhard [Verfasser]},
  ADDRESS = {Berlin},
  PUBLISHER = {Springer},
  YEAR = {[2017]},
  EDITION = {Fifth edition},
  ISBN = {978-3-662-53621-6},
  PAGES = {XVIII, 428 p.}
}
@book{GRELAT,
  title={Relations and graphs: discrete mathematics for computer scientists},
  author={Schmidt, Gunther and Str{\"o}hlein, Thomas},
  year={2012},
  publisher={Springer Science \& Business Media}
}
@book{AGT,
  title={Algebraic graph theory: morphisms, monoids and matrices},
  author={Knauer, Ulrich},
  volume={41},
  year={2011},
  publisher={Walter de Gruyter}
}
