@MISC{GLIB_016.MIZ,
  AUTHOR = {Koch, Sebastian},
  TITLE = {About Regular Graphs},
  SECTION1 = {Directed-complete Graphs},
  SECTION2 = {Regular Graphs},
  SECTION3 = {Directed-regular Graphs},
  SECTION4 = {Counting the Edges},
  SECTION5 = {The Degree Map and Degree Sequence},
  DAY = {30},
  MONTH = {June},
  YEAR = {2023},
  ADDRESS1 = {Germany\\\href{mailto:fly.high.android@gmail.com}{fly.high.android@gmail.com}},
  SUMMARY = {In this article regular graphs, both directed and undirected,
  are formalized in the Mizar system \cite{FourDecades}, based on the formalization of graphs
  in \cite{GLIB_000.ABS}. The handshaking lemma is also proven.},
  INTRODUCTION = {Regular graphs, especially cubic graphs, are a cornerstone of graph theory
  (cf. \cite{MULTI}, \cite{SIMPLE}, cite{DIESTEL}).
  In this article the concept of regular graphs is formalized, along with some adjacent concepts.
  In the first section, the directed analogue of \texttt{complete} from \cite{CHORD.ABS} is introduced.
  Sections 2 and 3 deal with the undirected and directed-regular graphs respectively.
  Section 4 is rather technical in nature; at its end $2m=\mathfrak{a}n is proven, where $m$ and $n$
  denote the size and order of an $\mathfrak{a}-regular graph, where $\mathfrak{a}$ can be any cardinal.
  Finally Section 5 introduces tools needed to formalize the combinatorial proof of the rather
  simple Handshaking Lemma.}}


@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{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 p.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?10670775_toc.pdf},
}

@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{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 p.},
  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}
}
