:: A Note on the Seven Bridges of K\"onigsberg Problem
:: by Adam Naumowicz
::
:: Received June 16, 2014
:: Copyright (c) 2014-2026 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;
definitions TARSKI, FUNCT_1, GRAPH_2, XBOOLE_0;
equalities GRAPH_3, FINSEQ_1;
expansions GRAPH_1;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, NAT_1, PARTFUN1, CARD_1, CARD_2,
FINSEQ_1, FINSEQ_3, XBOOLE_0, XXREAL_0, XTUPLE_0, GRAPH_3, POLYFORM,
ENUMSET1;
begin
definition
func KVertices -> set equals {0,1,2,3};
correctness;
func KEdges -> set equals {10,20,30,40,50,60,70};
correctness;
end;
definition
func KSource -> Function of KEdges,KVertices
equals {[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]};
correctness
proof
set K={[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]};
K c= [:KEdges,KVertices:]
proof
let x be object;
assume x in K;
then x: x=[10,0] or x=[20,0] or x=[30,0] or x=[40,1]
or x=[50,1] or x=[60,2] or x=[70,2] by ENUMSET1:def 5;
10 in KEdges & 20 in KEdges & 30 in KEdges & 40 in KEdges &
50 in KEdges & 60 in KEdges & 70 in KEdges &
0 in KVertices & 1 in KVertices & 2 in KVertices & 3 in KVertices
by ENUMSET1:def 2,def 5;
hence x in [:KEdges,KVertices:] by x,ZFMISC_1:87;
end;
then reconsider K as Relation of KEdges,KVertices;
K is Function-like
proof
let x,y1,y2 be object;
assume [x,y1] in K & [x,y2] in K;
then ([x,y1]=[10,0] or [x,y1]=[20,0] or [x,y1]=[30,0] or [x,y1]=[40,1]
or [x,y1]=[50,1] or [x,y1]=[60,2] or [x,y1]=[70,2]) &
([x,y2]=[10,0] or [x,y2]=[20,0] or [x,y2]=[30,0] or [x,y2]=[40,1]
or [x,y2]=[50,1] or [x,y2]=[60,2] or [x,y2]=[70,2]) by ENUMSET1:def 5;
then (x=10 & y1=0 or x=20 & y1=0 or x=30 & y1=0 or x=40 & y1=1
or x=50 & y1=1 or x=60 & y1=2 or x=70 & y1=2) &
(x=10 & y2=0 or x=20 & y2=0 or x=30 & y2=0 or x=40 & y2=1
or x=50 & y2=1 or x=60 & y2=2 or x=70 & y2=2) by XTUPLE_0:1;
hence y1 = y2;
end;
then reconsider K as PartFunc of KEdges,KVertices;
dom K = KEdges
proof
thus dom K c= KEdges;
let o be object;
assume o in KEdges; then
o: o=10 or o=20 or o=30 or o=40 or o=50 or o=60 or o=70
by ENUMSET1:def 5;
[10,0] in K & [20,0] in K & [30,0] in K & [40,1] in K & [50,1] in K &
[60,2] in K & [70,2] in K by ENUMSET1:def 5;
hence o in dom K by o,XTUPLE_0:def 12;
end; then
K is quasi_total by FUNCT_2:def 1;
hence thesis;
end;
func KTarget -> Function of KEdges,KVertices
equals {[10,1],[20,2],[30,3],[40,2],[50,2],[60,3],[70,3]};
correctness
proof
set K={[10,1],[20,2],[30,3],[40,2],[50,2],[60,3],[70,3]};
K c= [:KEdges,KVertices:]
proof
let x be object;
assume x in K;
then x: x=[10,1] or x=[20,2] or x=[30,3] or x=[40,2]
or x=[50,2] or x=[60,3] or x=[70,3] by ENUMSET1:def 5;
10 in KEdges & 20 in KEdges & 30 in KEdges & 40 in KEdges &
50 in KEdges & 60 in KEdges & 70 in KEdges &
0 in KVertices & 1 in KVertices & 2 in KVertices & 3 in KVertices
by ENUMSET1:def 2,def 5;
hence x in [:KEdges,KVertices:] by x,ZFMISC_1:87;
end;
then reconsider K as Relation of KEdges,KVertices;
K is Function-like
proof
let x,y1,y2 be object;
assume [x,y1] in K & [x,y2] in K;
then ([x,y1]=[10,1] or [x,y1]=[20,2] or [x,y1]=[30,3] or [x,y1]=[40,2]
or [x,y1]=[50,2] or [x,y1]=[60,3] or [x,y1]=[70,3]) &
([x,y2]=[10,1] or [x,y2]=[20,2] or [x,y2]=[30,3] or [x,y2]=[40,2]
or [x,y2]=[50,2] or [x,y2]=[60,3] or [x,y2]=[70,3]) by ENUMSET1:def 5;
then (x=10 & y1=1 or x=20 & y1=2 or x=30 & y1=3 or x=40 & y1=2
or x=50 & y1=2 or x=60 & y1=3 or x=70 & y1=3) &
(x=10 & y2=1 or x=20 & y2=2 or x=30 & y2=3 or x=40 & y2=2
or x=50 & y2=2 or x=60 & y2=3 or x=70 & y2=3) by XTUPLE_0:1;
hence y1 = y2;
end;
then reconsider K as PartFunc of KEdges,KVertices;
dom K = KEdges
proof
thus dom K c= KEdges;
let o be object;
assume o in KEdges; then
o: o=10 or o=20 or o=30 or o=40 or o=50 or o=60 or o=70
by ENUMSET1:def 5;
[10,1] in K & [20,2] in K & [30,3] in K & [40,2] in K & [50,2]in K &
[60,3] in K & [70,3] in K by ENUMSET1:def 5;
hence o in dom K by o,XTUPLE_0:def 12;
end; then
K is quasi_total by FUNCT_2:def 1;
hence thesis;
end;
end;
definition
func KoenigsbergBridges -> Graph equals
MultiGraphStruct(# KVertices,KEdges,KSource,KTarget#);
correctness;
end;
registration
cluster KoenigsbergBridges -> finite connected;
correctness
proof
for g1, g2 being Vertex of KoenigsbergBridges st g1 <> g2
ex c being Chain of KoenigsbergBridges,
vs being FinSequence of the carrier of KoenigsbergBridges
st c is non empty & vs is_vertex_seq_of c & vs.1 = g1 & vs.len vs = g2
proof
let g1, g2 be Vertex of KoenigsbergBridges;
assume g: g1 <> g2;
per cases by ENUMSET1:def 2;
suppose g1=0 & g2=0;
hence thesis by g;
end;
suppose gg: g1=0 & g2=1;
10 in KEdges by ENUMSET1:def 5; then
reconsider c = <*10*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c;
reconsider vs=<*g1,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus c is non empty;
l: len c = 1 & c.1 = 10 by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c
proof
thus len vs = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=10;
dom vs = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs & 2 in dom vs by TARSKI:def 2;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g2;
[10,0] in KSource & [10,1] in KTarget by ENUMSET1:def 5; then
KSource.(c.n) = g1 & KTarget.(c.n) = g2 by cn,gg,FUNCT_1:1;
hence c.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose gg: g1=0 & g2=2;
20 in KEdges by ENUMSET1:def 5; then
reconsider c = <*20*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c;
reconsider vs=<*g1,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus c is non empty;
l: len c = 1 & c.1 = 20 by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c
proof
thus len vs = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=20;
dom vs = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs & 2 in dom vs by TARSKI:def 2;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g2;
[20,0] in KSource & [20,2] in KTarget by ENUMSET1:def 5; then
KSource.(c.n) = g1 & KTarget.(c.n) = g2 by cn,gg,FUNCT_1:1;
hence c.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose gg: g1=0 & g2=3;
30 in KEdges by ENUMSET1:def 5; then
reconsider c = <*30*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c;
reconsider vs=<*g1,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus c is non empty;
l: len c = 1 & c.1 = 30 by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c
proof
thus len vs = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=30;
dom vs = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs & 2 in dom vs by TARSKI:def 2;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g2;
[30,0] in KSource & [30,3] in KTarget by ENUMSET1:def 5; then
KSource.(c.n) = g1 & KTarget.(c.n) = g2 by cn,gg,FUNCT_1:1;
hence c.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose gg: g1=1 & g2=0;
10 in KEdges by ENUMSET1:def 5; then
reconsider c = <*10*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c;
reconsider vs=<*g1,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus c is non empty;
l: len c = 1 & c.1 = 10 by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c
proof
thus len vs = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=10;
dom vs = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs & 2 in dom vs by TARSKI:def 2;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g2;
[10,0] in KSource & [10,1] in KTarget by ENUMSET1:def 5; then
KSource.(c.n) = g2 & KTarget.(c.n) = g1 by cn,gg,FUNCT_1:1;
hence c.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose g1=1 & g2=1;
hence thesis by g;
end;
suppose gg: g1=1 & g2=2;
40 in KEdges by ENUMSET1:def 5; then
reconsider c = <*40*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c;
reconsider vs=<*g1,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus c is non empty;
l: len c = 1 & c.1 = 40 by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c
proof
thus len vs = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=40;
dom vs = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs & 2 in dom vs by TARSKI:def 2;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g2;
[40,1] in KSource & [40,2] in KTarget by ENUMSET1:def 5; then
KSource.(c.n) = g1 & KTarget.(c.n) = g2 by cn,gg,FUNCT_1:1;
hence c.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose gg: g1=1 & g2=3;
reconsider g3=2 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
40 in KEdges by ENUMSET1:def 5; then
reconsider c = <*40*> as Path of KoenigsbergBridges by GRAPH_3:4;
60 in KEdges by ENUMSET1:def 5; then
reconsider d = <*60*> as Path of KoenigsbergBridges by GRAPH_3:4;
reconsider vs1=<*g1,g3*> as FinSequence of the carrier of
KoenigsbergBridges;
l: len c = 1 & c.1 = 40 by FINSEQ_1:40;
lv1: len vs1 = 2 by FINSEQ_1:44;
vs1: vs1 is_vertex_seq_of c
proof
thus len vs1 = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=40;
dom vs1 = Seg 2 by lv1,FINSEQ_1:def 3; then
dom vs1 = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs1 & 2 in dom vs1 by TARSKI:def 2;
v1: vs1/.n = vs1.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs1/.(n+1) = vs1.2 by d,n,PARTFUN1:def 6 .= g3;
[40,1] in KSource & [40,2] in KTarget by ENUMSET1:def 5; then
KSource.(c.n) = g1 & KTarget.(c.n) = g3 by cn,gg,FUNCT_1:1;
hence c.n joins vs1/.n, vs1/.(n+1) by v1,v2;
end;
reconsider vs2=<*g3,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
l: len d = 1 & d.1 = 60 by FINSEQ_1:40;
lv: len vs2 = 2 by FINSEQ_1:44;
vs2: vs2 is_vertex_seq_of d
proof
thus len vs2 = len d +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len d;
then n: n=1 by l,XXREAL_0:1;
then cn: d.n=60;
dom vs2 = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs2 = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs2 & 2 in dom vs2 by TARSKI:def 2;
v1: vs2/.n = vs2.n by d,n,PARTFUN1:def 6 .= g3 by n;
v2: vs2/.(n+1) = vs2.2 by d,n,PARTFUN1:def 6 .= g2;
[60,2] in KSource & [60,3] in KTarget by ENUMSET1:def 5; then
KSource.(d.n) = g3 & KTarget.(d.n) = g2 by cn,gg,FUNCT_1:1;
hence d.n joins vs2/.n, vs2/.(n+1) by v1,v2;
end;
rng c = {40} & rng d = {60} by FINSEQ_1:38; then
r: rng c misses rng d by ZFMISC_1:11;
vs1.len vs1 = g3 by lv1 .= vs2.1;
then reconsider cd=c^d as Path of KoenigsbergBridges
by vs1,vs2,r,GRAPH_3:6;
take cd;
reconsider vs=<*g1,g3,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus cd is non empty;
cd=<*40,60*>; then
l: len cd = 2 & cd.1 = 40 & cd.2 = 60 by FINSEQ_1:44;
lv: len vs = 3 by FINSEQ_1:45;
thus vs is_vertex_seq_of cd
proof
thus len vs = len cd +1 by l,FINSEQ_1:45;
let n be Nat;
assume 1<=n & n<=len cd; then
1 <= n & n <= 1+1 by l;
then n=1+0 or ... or n=1+1 by NAT_1:62;
then n=1 or n=2;
then per cases;
suppose n: n=1;
then cn: cd.n=40 by l;
dom vs = Seg 3 by lv,FINSEQ_1:def 3; then
dom vs = {1,2,3} by FINSEQ_3:1; then
d: 1 in dom vs & 2 in dom vs by ENUMSET1:def 1;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g3;
[40,1] in KSource & [40,2] in KTarget by ENUMSET1:def 5; then
KSource.(cd.n) = g1 & KTarget.(cd.n) = g3 by cn,gg,FUNCT_1:1;
hence cd.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
suppose n: n=2;
then cn: cd.n=60 by l;
dom vs = Seg 3 by lv,FINSEQ_1:def 3; then
dom vs = {1,2,3} by FINSEQ_3:1; then
d: 2 in dom vs & 3 in dom vs by ENUMSET1:def 1;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g3 by n;
v2: vs/.(n+1) = vs.3 by d,n,PARTFUN1:def 6 .= g2;
[60,2] in KSource & [60,3] in KTarget by ENUMSET1:def 5; then
KSource.(cd.n) = g3 & KTarget.(cd.n) = g2 by cn,gg,FUNCT_1:1;
hence cd.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose gg: g1=2 & g2=0;
20 in KEdges by ENUMSET1:def 5; then
reconsider c = <*20*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c;
reconsider vs=<*g1,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus c is non empty;
l: len c = 1 & c.1 = 20 by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c
proof
thus len vs = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=20;
dom vs = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs & 2 in dom vs by TARSKI:def 2;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g2;
[20,0] in KSource & [20,2] in KTarget by ENUMSET1:def 5; then
KTarget.(c.n) = g1 & KSource.(c.n) = g2 by cn,gg,FUNCT_1:1;
hence c.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose gg: g1=2 & g2=1;
40 in KEdges by ENUMSET1:def 5; then
reconsider c = <*40*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c;
reconsider vs=<*g1,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus c is non empty;
l: len c = 1 & c.1 = 40 by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c
proof
thus len vs = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=40;
dom vs = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs & 2 in dom vs by TARSKI:def 2;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g2;
[40,1] in KSource & [40,2] in KTarget by ENUMSET1:def 5; then
KTarget.(c.n) = g1 & KSource.(c.n) = g2 by cn,gg,FUNCT_1:1;
hence c.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose g1=2 & g2=2;
hence thesis by g;
end;
suppose gg: g1=2 & g2=3;
60 in KEdges by ENUMSET1:def 5; then
reconsider c = <*60*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c;
reconsider vs=<*g1,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus c is non empty;
l: len c = 1 & c.1 = 60 by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c
proof
thus len vs = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=60;
dom vs = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs & 2 in dom vs by TARSKI:def 2;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g2;
[60,2] in KSource & [60,3] in KTarget by ENUMSET1:def 5; then
KSource.(c.n) = g1 & KTarget.(c.n) = g2 by cn,gg,FUNCT_1:1;
hence c.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose gg: g1=3 & g2=0;
30 in KEdges by ENUMSET1:def 5; then
reconsider c = <*30*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c;
reconsider vs=<*g1,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus c is non empty;
l: len c = 1 & c.1 = 30 by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c
proof
thus len vs = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=30;
dom vs = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs & 2 in dom vs by TARSKI:def 2;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g2;
[30,0] in KSource & [30,3] in KTarget by ENUMSET1:def 5; then
KTarget.(c.n) = g1 & KSource.(c.n) = g2 by cn,gg,FUNCT_1:1;
hence c.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose gg: g1=3 & g2=1;
reconsider g3=2 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
60 in KEdges by ENUMSET1:def 5; then
reconsider c = <*60*> as Path of KoenigsbergBridges by GRAPH_3:4;
40 in KEdges by ENUMSET1:def 5; then
reconsider d = <*40*> as Path of KoenigsbergBridges by GRAPH_3:4;
reconsider vs1=<*g1,g3*> as FinSequence of the carrier of
KoenigsbergBridges;
l: len c = 1 & c.1 = 60 by FINSEQ_1:40;
lv1: len vs1 = 2 by FINSEQ_1:44;
vs1: vs1 is_vertex_seq_of c
proof
thus len vs1 = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=60;
dom vs1 = Seg 2 by lv1,FINSEQ_1:def 3; then
dom vs1 = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs1 & 2 in dom vs1 by TARSKI:def 2;
v1: vs1/.n = vs1.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs1/.(n+1) = vs1.2 by d,n,PARTFUN1:def 6 .= g3;
[60,2] in KSource & [60,3] in KTarget by ENUMSET1:def 5; then
KTarget.(c.n) = g1 & KSource.(c.n) = g3 by cn,gg,FUNCT_1:1;
hence c.n joins vs1/.n, vs1/.(n+1) by v1,v2;
end;
reconsider vs2=<*g3,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
l: len d = 1 & d.1 = 40 by FINSEQ_1:40;
lv: len vs2 = 2 by FINSEQ_1:44;
vs2: vs2 is_vertex_seq_of d
proof
thus len vs2 = len d +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len d;
then n: n=1 by l,XXREAL_0:1;
then cn: d.n=40;
dom vs2 = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs2 = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs2 & 2 in dom vs2 by TARSKI:def 2;
v1: vs2/.n = vs2.n by d,n,PARTFUN1:def 6 .= g3 by n;
v2: vs2/.(n+1) = vs2.2 by d,n,PARTFUN1:def 6 .= g2;
[40,1] in KSource & [40,2] in KTarget by ENUMSET1:def 5; then
KTarget.(d.n) = g3 & KSource.(d.n) = g2 by cn,gg,FUNCT_1:1;
hence d.n joins vs2/.n, vs2/.(n+1) by v1,v2;
end;
rng c = {60} & rng d = {40} by FINSEQ_1:38; then
r: rng c misses rng d by ZFMISC_1:11;
vs1.len vs1 = g3 by lv1 .= vs2.1;
then reconsider cd=c^d as Path of KoenigsbergBridges
by vs1,vs2,r,GRAPH_3:6;
take cd;
reconsider vs=<*g1,g3,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus cd is non empty;
cd=<*60,40*>; then
l: len cd = 2 & cd.1 = 60 & cd.2 = 40 by FINSEQ_1:44;
lv: len vs = 3 by FINSEQ_1:45;
thus vs is_vertex_seq_of cd
proof
thus len vs = len cd +1 by l,FINSEQ_1:45;
let n be Nat;
assume 1<=n & n<=len cd; then
1 <= n & n <= 1+1 by l;
then n=1+0 or ... or n=1+1 by NAT_1:62;
then n=1 or n=2;
then per cases;
suppose n: n=1;
then cn: cd.n=60 by l;
dom vs = Seg 3 by lv,FINSEQ_1:def 3; then
dom vs = {1,2,3} by FINSEQ_3:1; then
d: 1 in dom vs & 2 in dom vs by ENUMSET1:def 1;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g3;
[60,2] in KSource & [60,3] in KTarget by ENUMSET1:def 5; then
KTarget.(cd.n) = g1 & KSource.(cd.n) = g3 by cn,gg,FUNCT_1:1;
hence cd.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
suppose n: n=2;
then cn: cd.n=40 by l;
dom vs = Seg 3 by lv,FINSEQ_1:def 3; then
dom vs = {1,2,3} by FINSEQ_3:1; then
d: 2 in dom vs & 3 in dom vs by ENUMSET1:def 1;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g3 by n;
v2: vs/.(n+1) = vs.3 by d,n,PARTFUN1:def 6 .= g2;
[40,1] in KSource & [40,2] in KTarget by ENUMSET1:def 5; then
KTarget.(cd.n) = g3 & KSource.(cd.n) = g2 by cn,gg,FUNCT_1:1;
hence cd.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose gg: g1=3 & g2=2;
60 in KEdges by ENUMSET1:def 5; then
reconsider c = <*60*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c;
reconsider vs=<*g1,g2*> as FinSequence of the carrier of
KoenigsbergBridges;
take vs;
thus c is non empty;
l: len c = 1 & c.1 = 60 by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c
proof
thus len vs = len c +1 by l,FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then n: n=1 by l,XXREAL_0:1;
then cn: c.n=60;
dom vs = Seg 2 by lv,FINSEQ_1:def 3; then
dom vs = {1,2} by FINSEQ_1:2; then
d: 1 in dom vs & 2 in dom vs by TARSKI:def 2;
v1: vs/.n = vs.n by d,n,PARTFUN1:def 6 .= g1 by n;
v2: vs/.(n+1) = vs.2 by d,n,PARTFUN1:def 6 .= g2;
[60,2] in KSource & [60,3] in KTarget by ENUMSET1:def 5; then
KTarget.(c.n) = g1 & KSource.(c.n) = g2 by cn,gg,FUNCT_1:1;
hence c.n joins vs/.n, vs/.(n+1) by v1,v2;
end;
thus vs.1 = g1 & vs.len vs = g2 by lv;
end;
suppose g1=3 & g2=3;
hence thesis by g;
end;
end;
hence KoenigsbergBridges is finite connected by GRAPH_3:18;
end;
end;
theorem d0:
for v being Vertex of KoenigsbergBridges st v=0 holds Degree v = 3
proof
let v be Vertex of KoenigsbergBridges such that
v: v=0;
now
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in Edges_In(v);
then s: s in KEdges & KTarget.s=v by GRAPH_3:def 1;
dom KTarget = KEdges by FUNCT_2:def 1; then
s in dom KTarget by s; then
[s,v] in KTarget by s,FUNCT_1:1; then
[s,v]=[10,1] or [s,v]=[20,2] or [s,v]=[30,3] or [s,v]=[40,2] or
[s,v]=[50,2] or [s,v]=[60,3] or [s,v]=[70,3] by ENUMSET1:def 5;
hence contradiction by v,XTUPLE_0:1;
end; then
c1: Edges_In(v)={} by XBOOLE_0:def 1;
c2: Edges_Out(v)={10,20,30}
proof
thus Edges_Out(v)c={10,20,30}
proof
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in Edges_Out(v);
then s: s in KEdges & KSource.s=v by GRAPH_3:def 2;
dom KSource = KEdges by FUNCT_2:def 1; then
s in dom KSource by s; then
[s,v] in KSource by s,FUNCT_1:1; then
[s,v]=[10,0] or [s,v]=[20,0] or [s,v]=[30,0] or [s,v]=[40,1] or
[s,v]=[50,1] or [s,v]=[60,2] or [s,v]=[70,2] by ENUMSET1:def 5;
then s=10 or s=20 or s=30 by v,XTUPLE_0:1;
hence a in {10,20,30} by ENUMSET1:def 1;
end;
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in {10,20,30}; then
a: a=10 or a=20 or a=30 by ENUMSET1:def 1; then
s: s in KEdges by ENUMSET1:def 5;
[s,v] in KSource by v,a,ENUMSET1:def 5; then
KSource.s=v by FUNCT_1:1;
hence a in Edges_Out(v) by s,GRAPH_3:def 2;
end;
Degree(v, the carrier' of KoenigsbergBridges) = 0+3 by c1,c2,CARD_2:58;
hence Degree v = 3 by GRAPH_3:24;
end;
theorem d1:
for v being Vertex of KoenigsbergBridges st v=1 holds Degree v = 3
proof
let v be Vertex of KoenigsbergBridges such that
v: v=1;
c1: Edges_In(v)={10}
proof
thus Edges_In(v)c={10}
proof
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in Edges_In(v);
then s: s in KEdges & KTarget.s=v by GRAPH_3:def 1;
dom KTarget = KEdges by FUNCT_2:def 1; then
s in dom KTarget by s; then
[s,v] in KTarget by s,FUNCT_1:1; then
[s,v]=[10,1] or [s,v]=[20,2] or [s,v]=[30,3] or [s,v]=[40,2] or
[s,v]=[50,2] or [s,v]=[60,3] or [s,v]=[70,3] by ENUMSET1:def 5;
then s=10 by v,XTUPLE_0:1;
hence a in {10} by TARSKI:def 1;
end;
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in {10}; then
a: a=10 by TARSKI:def 1; then
s: s in KEdges by ENUMSET1:def 5;
[s,v] in KTarget by v,a,ENUMSET1:def 5; then
KTarget.s=v by FUNCT_1:1;
hence a in Edges_In(v) by s,GRAPH_3:def 1;
end;
c2: Edges_Out(v)={40,50}
proof
thus Edges_Out(v)c={40,50}
proof
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in Edges_Out(v);
then s: s in KEdges & KSource.s=v by GRAPH_3:def 2;
dom KSource = KEdges by FUNCT_2:def 1; then
s in dom KSource by s; then
[s,v] in KSource by s,FUNCT_1:1; then
[s,v]=[10,0] or [s,v]=[20,0] or [s,v]=[30,0] or [s,v]=[40,1] or
[s,v]=[50,1] or [s,v]=[60,2] or [s,v]=[70,2] by ENUMSET1:def 5;
then s=40 or s=50 by v,XTUPLE_0:1;
hence a in {40,50} by TARSKI:def 2;
end;
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in {40,50}; then
a: a=40 or a=50 by TARSKI:def 2; then
s: s in KEdges by ENUMSET1:def 5;
[s,v] in KSource by v,a,ENUMSET1:def 5; then
KSource.s=v by FUNCT_1:1;
hence a in Edges_Out(v) by s,GRAPH_3:def 2;
end;
card Edges_In(v)=1 & card Edges_Out(v)=2 by c1,c2,CARD_1:30,CARD_2:57;
then Degree(v, the carrier' of KoenigsbergBridges) = 1+2;
hence Degree v = 3 by GRAPH_3:24;
end;
theorem
for v being Vertex of KoenigsbergBridges st v=2 holds Degree v = 5
proof
let v be Vertex of KoenigsbergBridges such that
v: v=2;
c1: Edges_In(v)={20,40,50}
proof
thus Edges_In(v)c={20,40,50}
proof
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in Edges_In(v);
then s: s in KEdges & KTarget.s=v by GRAPH_3:def 1;
dom KTarget = KEdges by FUNCT_2:def 1; then
s in dom KTarget by s; then
[s,v] in KTarget by s,FUNCT_1:1; then
[s,v]=[10,1] or [s,v]=[20,2] or [s,v]=[30,3] or [s,v]=[40,2] or
[s,v]=[50,2] or [s,v]=[60,3] or [s,v]=[70,3] by ENUMSET1:def 5;
then s=20 or s=40 or s=50 by v,XTUPLE_0:1;
hence a in {20,40,50} by ENUMSET1:def 1;
end;
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in {20,40,50}; then
a: a=20 or a=40 or a=50 by ENUMSET1:def 1; then
s: s in KEdges by ENUMSET1:def 5;
[s,v] in KTarget by v,a,ENUMSET1:def 5; then
KTarget.s=v by FUNCT_1:1;
hence a in Edges_In(v) by s,GRAPH_3:def 1;
end;
c2: Edges_Out(v)={60,70}
proof
thus Edges_Out(v)c={60,70}
proof
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in Edges_Out(v);
then s: s in KEdges & KSource.s=v by GRAPH_3:def 2;
dom KSource = KEdges by FUNCT_2:def 1; then
s in dom KSource by s; then
[s,v] in KSource by s,FUNCT_1:1; then
[s,v]=[10,0] or [s,v]=[20,0] or [s,v]=[30,0] or [s,v]=[40,1] or
[s,v]=[50,1] or [s,v]=[60,2] or [s,v]=[70,2] by ENUMSET1:def 5;
then s=60 or s=70 by v,XTUPLE_0:1;
hence a in {60,70} by TARSKI:def 2;
end;
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in {60,70}; then
a: a=60 or a=70 by TARSKI:def 2; then
s: s in KEdges by ENUMSET1:def 5;
[s,v] in KSource by v,a,ENUMSET1:def 5; then
KSource.s=v by FUNCT_1:1;
hence a in Edges_Out(v) by s,GRAPH_3:def 2;
end;
card Edges_In(v)=3 & card Edges_Out(v)=2 by c1,c2,CARD_2:57,58;
then Degree(v, the carrier' of KoenigsbergBridges) = 3+2;
hence Degree v = 5 by GRAPH_3:24;
end;
theorem d3:
for v being Vertex of KoenigsbergBridges st v=3 holds Degree v = 3
proof
let v be Vertex of KoenigsbergBridges such that
v: v=3;
c1: Edges_In(v)={30,60,70}
proof
thus Edges_In(v)c={30,60,70}
proof
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in Edges_In(v);
then s: s in KEdges & KTarget.s=v by GRAPH_3:def 1;
dom KTarget = KEdges by FUNCT_2:def 1; then
s in dom KTarget by s; then
[s,v] in KTarget by s,FUNCT_1:1; then
[s,v]=[10,1] or [s,v]=[20,2] or [s,v]=[30,3] or [s,v]=[40,2] or
[s,v]=[50,2] or [s,v]=[60,3] or [s,v]=[70,3] by ENUMSET1:def 5;
then s=30 or s=60 or s=70 by v,XTUPLE_0:1;
hence a in {30,60,70} by ENUMSET1:def 1;
end;
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in {30,60,70}; then
a: a=30 or a=60 or a=70 by ENUMSET1:def 1; then
s: s in KEdges by ENUMSET1:def 5;
[s,v] in KTarget by v,a,ENUMSET1:def 5; then
KTarget.s=v by FUNCT_1:1;
hence a in Edges_In(v) by s,GRAPH_3:def 1;
end;
c2: Edges_Out(v)={}
proof
thus Edges_Out(v)c={}
proof
let a be object;
reconsider s=a as set by TARSKI:1;
assume a in Edges_Out(v);
then s: s in KEdges & KSource.s=v by GRAPH_3:def 2;
dom KSource = KEdges by FUNCT_2:def 1; then
s in dom KSource by s; then
[s,v] in KSource by s,FUNCT_1:1; then
[s,v]=[10,0] or [s,v]=[20,0] or [s,v]=[30,0] or [s,v]=[40,1] or
[s,v]=[50,1] or [s,v]=[60,2] or [s,v]=[70,2] by ENUMSET1:def 5;
hence a in {} by v,XTUPLE_0:1;
end;
let a be object;
assume a in {};
hence a in Edges_Out(v);
end;
card Edges_In(v)=3 & card Edges_Out(v)=0 by c1,c2,CARD_2:58;
then Degree(v, the carrier' of KoenigsbergBridges) = 3+0;
hence Degree v = 3 by GRAPH_3:24;
end;
::$N Seven Bridges of Koenigsberg
::$L https://en.wikipedia.org/wiki/Seven_Bridges_of_Konigsberg Seven Bridges of Koenigsberg
theorem
not ex p being Path of KoenigsbergBridges st p is cyclic Eulerian
proof
reconsider v=0 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
Degree v = 3 by d0; then
Degree v is not even by POLYFORM:6;
hence thesis by GRAPH_3:59;
end;
theorem
not ex p being Path of KoenigsbergBridges st p is non cyclic Eulerian
proof
given p being Path of KoenigsbergBridges such that
p: p is non cyclic Eulerian;
consider v1,v2 being Vertex of KoenigsbergBridges such that
v: v1<>v2 & for v being Vertex of KoenigsbergBridges holds
Degree v is even iff v<>v1 & v<>v2 by p,GRAPH_3:60;
(v1=0 or v1=1 or v1=2 or v1=3) & (v2=0 or v2=1 or v2=2 or v2=3) & v1<>v2
by v,ENUMSET1:def 2;
then per cases;
suppose s: v1=0 & v2=1 or v1=0 & v2=2 or v1=1 & v2=0 or
v1=1 & v2=2 or v1=2 & v2=0 or v1=2 & v2=1;
reconsider v=3 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
Degree v = 3 by d3; then
Degree v is not even by POLYFORM:6;
hence contradiction by s,v;
end;
suppose s: v1=1 & v2=3 or v1=2 & v2=3 or v1=3 & v2=1 or v1=3 & v2=2;
reconsider v=0 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
Degree v = 3 by d0; then
Degree v is not even by POLYFORM:6;
hence contradiction by s,v;
end;
suppose s: v1=0 & v2=3 or v1=3 & v2=0;
reconsider v=1 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
Degree v = 3 by d1; then
Degree v is not even by POLYFORM:6;
hence contradiction by s,v;
end;
end;