@MISC{SGRAPH1.MIZ,
  AUTHOR = {Toda, Yozo},
  TITLE = {The Formalization of Simple Graphs},
  SECTION1 = {Preliminaries},
  SECTION2 = {Simple Graphs},
  SECTION3 = {Equality Relation on Simple Graphs},
  SECTION4 = {Properties of Simple Graphs},
  SECTION5 = {Subgraphs},
  SECTION6 = {Degree of Vertices},
  SECTION7 = {Path and Cycle},
  SECTION8 = {Some Famous Graphs},
  DAY = {08},
  MONTH = {September},
  YEAR = {1994},
  ADDRESS1 = {Information Processing Center\\Chiba University},
  SUMMARY = {A graph is simple when
 \begin{itemize}
  \parskip -1mm
  \item it is non-directed,
  \item there is at most one edge between two vertices,
  \item there is no loop of length one.
 \end{itemize}
A formalization of simple graphs is given from scratch.
There is already an article \cite{GRAPH_1.ABS}, dealing with the similar
subject.
It is not used as a starting-point, because
 \cite{GRAPH_1.ABS} formalizes directed non-empty graphs.
Given a set of vertices, edge is defined as an (unordered) pair of 
different two vertices and graph as a pair of a set of vertices and 
a set of edges.\par
The following concepts are introduced:
 \begin{itemize}
   \parskip -1mm
  \item simple graph structure,
  \item the set of all simple graphs,
  \item equality relation on graphs.
  \item the notion of degrees of vertices;
      the number of edges connected to, or the number of adjacent vertices,
  \item the notion of subgraphs,
  \item path, cycle,
  \item complete and bipartite complete graphs,
 \end{itemize}\par
Theorems proved in this articles include:
 \begin{itemize}
  \parskip -1mm
 \item the set of simple graphs satisfies a certain minimality condition,
  \item equivalence between two notions of degrees.
 \end{itemize}}}

