@MISC{GLIBPRE1.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {Miscellaneous Graph Preliminaries, {I}},
  SECTION1 = {Preliminaries not directly related to graphs},
  SECTION2 = {Into GLIB_000},
  SECTION3 = {Into GLIB_001},
  SECTION4 = {Into GLIB_002},
  SECTION5 = {Into CHORD},
  SECTION6 = {Into GLIB_006},
  SECTION7 = {Into GLIB_007},
  SECTION8 = {Into GLIB_008},
  SECTION9 = {Into GLIB_009},
  SECTION10 = {Into GLIB_010},
  SECTION11 = {Into GLIB_014},
  SECTION12 = {Into GLUNIR00},
  DAY = {30},
  MONTH = {March},
  YEAR = {2021},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {This article contains many auxiliary theorems 
  which were missing in the Mizar Mathematical Library 
  to the best of the author's knowledge. Most of them regard 
  graph theory as formalized in the \texttt{GLIB} series and 
  are needed in upcoming articles.},
  INTRODUCTION = {A generalized approach to graph theory 
  as it was done in \cite{MULTI,AGT} in contrast to 
  \cite{SIMPLE,HOMO} is rather uncommon. To avoid duplication 
  of the same theorems in different formalization frameworks 
  in the Mizar Mathematical Library \cite{BancerekJAR:2018}, 
  a generalized approach to formalization is preferable 
  (cf. \cite{GLIB_000.ABS,GLIB_010.ABS}). However, due to 
  the sheer amount of ``obvious facts'' such an approach 
  brings with it, it is only natural some of them not 
  immediately needed slip the initial formalization 
  process. This article, like its precedessor \cite{GLIBPRE0.ABS}, 
  aims to fill some of the gaps that emerged.\par
  Many theorems in this article regard the property of a 
  walk in a graph to be the shortest one, which have been 
  rather neglected in the author's work on graphs in 
  Mizar until now. Another good portion is concered with 
  theorems about graph mappings which are missing from 
  \cite{GLIB_010.ABS}. Further worthy of note is the theorem 
  that combines adding an edge or adjacent vertex with the 
  reversal of the edge to be added and the two theorems noting 
  that a connected graph is unicyclic if and only iff the 
  connected subgraph it can be constructed from by adding an 
  edge is a tree.}}

@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{AGT,
  title={Algebraic graph theory: morphisms, monoids and matrices},
  author={Knauer, Ulrich},
  volume={41},
  year={2011},
  publisher={Walter de Gruyter}
}
@book{SIMPLE,
  TITLE = {Introduction to graph theory},
  AUTHOR = {Wilson, Robin James},
  ADDRESS = {Edinburgh},
  PUBLISHER = {Oliver & Boyd},
  YEAR = {1972},
  ISBN = {0-05-002534-1},
  PAGES = {VIII, 168 S.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?10670775_toc.pdf},
}
@book{MULTI,
  TITLE = {Graph theory},
  SERIES = {Graduate texts in mathematics ; 244},
  AUTHOR = {Bondy, John Adrian ; Murty, U. S. R.},
  ADDRESS = {New York, NY},
  PUBLISHER = {Springer},
  YEAR = {2008},
  ISBN = {978-1-84628-969-9},
  PAGES = {XII, 652 S.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?19542627_toc.pdf ; http://scans.hebis.de/HEBCGI/show.pl?19542627_kap-2.pdf ; http://scans.hebis.de/HEBCGI/show.pl?19542627_ein-1.pdf}
}
@book{HOMO,
  title = {Graphs and homomorphisms},
  series = {Oxford lecture series in mathematics and its applications ; 28},
  author = {Hell, Pavol ; Nesetril, Jaroslav},
  address = {Oxford},
  publisher = {Oxford Univ. Press},
  year = {2004},
  ISBN = {0-19-852817-5},
  pages = {IX, 244 S.},
  url = {http://scans.hebis.de/HEBCGI/show.pl?12385357_toc.pdf}
}