:: A Note on the Seven Bridges of K\"onigsberg Problem
::  by Adam Naumowicz
:: 
:: Received June 16, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, FINSEQ_1, ABIAN, RELAT_1, XXREAL_0, ARYTM_3,
      GRAPH_2, FUNCT_1, CARD_1, GRAPH_1, GLIB_000, STRUCT_0, TREES_2, ORDINAL4,
      NAT_1, PARTFUN1, TARSKI, RELAT_2, FINSET_1, ZFMISC_1, GRAPH_3, FUNCT_2,
      GRAPH_3A;
 notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, ORDINAL1, NUMBERS, RELSET_1,
      FUNCT_1, PARTFUN1, FUNCT_2, CARD_1, NAT_1, FINSEQ_1, FINSEQ_4, STRUCT_0,
      GRAPH_1, GRAPH_2, MSSCYC_1, ABIAN, XXREAL_0, GRAPH_3;
 constructors FINSEQ_4, ABIAN, MSSCYC_1, RELSET_1, PRE_POLY, GRAPH_3, ENUMSET1;
 registrations XBOOLE_0, FINSET_1, XREAL_0, NAT_1, CARD_1, MEMBERED, FINSEQ_1,
      STRUCT_0, RELSET_1, SUBSET_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

definition
  func KVertices -> set equals
:: GRAPH_3A:def 1
{0,1,2,3};
  func KEdges -> set equals
:: GRAPH_3A:def 2
{10,20,30,40,50,60,70};
end;

definition
  func KSource -> Function of KEdges,KVertices
  equals
:: GRAPH_3A:def 3
{[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]};
  func KTarget -> Function of KEdges,KVertices
  equals
:: GRAPH_3A:def 4
{[10,1],[20,2],[30,3],[40,2],[50,2],[60,3],[70,3]};
end;

definition
  func KoenigsbergBridges -> Graph equals
:: GRAPH_3A:def 5
  MultiGraphStruct(# KVertices,KEdges,KSource,KTarget#);
end;

registration
  cluster KoenigsbergBridges -> finite connected;
end;

theorem :: GRAPH_3A:1
  for v being Vertex of KoenigsbergBridges st v=0 holds Degree v = 3;

theorem :: GRAPH_3A:2
  for v being Vertex of KoenigsbergBridges st v=1 holds Degree v = 3;

theorem :: GRAPH_3A:3
  for v being Vertex of KoenigsbergBridges st v=2 holds Degree v = 5;

theorem :: GRAPH_3A:4
  for v being Vertex of KoenigsbergBridges st v=3 holds Degree v = 3;

::$N Seven Bridges of Koenigsberg
theorem :: GRAPH_3A:5
  not ex p being Path of KoenigsbergBridges st p is cyclic Eulerian;

theorem :: GRAPH_3A:6
  not ex p being Path of KoenigsbergBridges st p is non cyclic Eulerian;