:: A Note on the Seven Bridges of K\"onigsberg Problem
::
:: Copyright (c) 2014-2021 Association of Mizar Users

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

:: deftheorem defines KVertices GRAPH_3A:def 1 :
KVertices = {0,1,2,3};

:: deftheorem defines KEdges GRAPH_3A:def 2 :
KEdges = {10,20,30,40,50,60,70};

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]};
correctness
coherence
{[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]} is Function of KEdges,KVertices
;
proof end;
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]};
correctness
coherence
{[10,1],[20,2],[30,3],[40,2],[50,2],[60,3],[70,3]} is Function of KEdges,KVertices
;
proof end;
end;

:: deftheorem defines KSource GRAPH_3A:def 3 :
KSource = {[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]};

:: deftheorem defines KTarget GRAPH_3A:def 4 :
KTarget = {[10,1],[20,2],[30,3],[40,2],[50,2],[60,3],[70,3]};

definition
correctness
coherence ;
;
end;

:: deftheorem defines KoenigsbergBridges GRAPH_3A:def 5 :

registration
correctness
coherence ;
proof end;
end;

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

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

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

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

:: Seven Bridges of Koenigsberg
theorem :: GRAPH_3A:5
for p being Path of KoenigsbergBridges holds
( not p is cyclic or not p is Eulerian )
proof end;

theorem :: GRAPH_3A:6
for p being Path of KoenigsbergBridges holds
( p is cyclic or not p is Eulerian )
proof end;