for g1, g2 being Vertex of KoenigsbergBridges st g1 <> g2 holds
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
proof
let g1,
g2 be
Vertex of
KoenigsbergBridges;
( g1 <> g2 implies ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 ) )
assume g:
g1 <> g2
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
per cases
( ( g1 = 0 & g2 = 0 ) or ( g1 = 0 & g2 = 1 ) or ( g1 = 0 & g2 = 2 ) or ( g1 = 0 & g2 = 3 ) or ( g1 = 1 & g2 = 0 ) or ( g1 = 1 & g2 = 1 ) or ( g1 = 1 & g2 = 2 ) or ( g1 = 1 & g2 = 3 ) or ( g1 = 2 & g2 = 0 ) or ( g1 = 2 & g2 = 1 ) or ( g1 = 2 & g2 = 2 ) or ( g1 = 2 & g2 = 3 ) or ( g1 = 3 & g2 = 0 ) or ( g1 = 3 & g2 = 1 ) or ( g1 = 3 & g2 = 2 ) or ( g1 = 3 & g2 = 3 ) )
by ENUMSET1:def 2;
suppose gg:
(
g1 = 0 &
g2 = 1 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
10
in KEdges
by ENUMSET1:def 5;
then reconsider c =
<*10*> as
Path of
KoenigsbergBridges by GRAPH_3:4;
take
c
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
c is
empty
;
( vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len c) + 1
by l, FINSEQ_1:44;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs /. n,vs /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 10
by l;
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, FINSEQ_1:44
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:44;
verum suppose gg:
(
g1 = 0 &
g2 = 2 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
20
in KEdges
by ENUMSET1:def 5;
then reconsider c =
<*20*> as
Path of
KoenigsbergBridges by GRAPH_3:4;
take
c
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
c is
empty
;
( vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len c) + 1
by l, FINSEQ_1:44;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs /. n,vs /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 20
by l;
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, FINSEQ_1:44
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:44;
verum suppose gg:
(
g1 = 0 &
g2 = 3 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
30
in KEdges
by ENUMSET1:def 5;
then reconsider c =
<*30*> as
Path of
KoenigsbergBridges by GRAPH_3:4;
take
c
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
c is
empty
;
( vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len c) + 1
by l, FINSEQ_1:44;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs /. n,vs /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 30
by l;
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, FINSEQ_1:44
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:44;
verum suppose gg:
(
g1 = 1 &
g2 = 0 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
10
in KEdges
by ENUMSET1:def 5;
then reconsider c =
<*10*> as
Path of
KoenigsbergBridges by GRAPH_3:4;
take
c
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
c is
empty
;
( vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len c) + 1
by l, FINSEQ_1:44;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs /. n,vs /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 10
by l;
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, FINSEQ_1:44
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:44;
verum suppose gg:
(
g1 = 1 &
g2 = 2 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
40
in KEdges
by ENUMSET1:def 5;
then reconsider c =
<*40*> as
Path of
KoenigsbergBridges by GRAPH_3:4;
take
c
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
c is
empty
;
( vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len c) + 1
by l, FINSEQ_1:44;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs /. n,vs /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 40
by l;
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, FINSEQ_1:44
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:44;
verum suppose gg:
(
g1 = 1 &
g2 = 3 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs1 /. b1,vs1 /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs1 /. n,vs1 /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs1 /. n,vs1 /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 40
by l;
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, FINSEQ_1:44
;
v2:
vs1 /. (n + 1) =
vs1 . 2
by d, n, PARTFUN1:def 6
.=
g3
by FINSEQ_1:44
;
(
[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;
verum
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;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len d or d . b1 joins vs2 /. b1,vs2 /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len d or d . n joins vs2 /. n,vs2 /. (n + 1) )
assume
( 1
<= n &
n <= len d )
;
d . n joins vs2 /. n,vs2 /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
d . n = 60
by l;
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, FINSEQ_1:44
;
v2:
vs2 /. (n + 1) =
vs2 . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
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, FINSEQ_1:44
.=
vs2 . 1
by FINSEQ_1:44
;
then reconsider cd =
c ^ d as
Path of
KoenigsbergBridges by vs1, vs2, r, GRAPH_3:6;
take
cd
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not cd is empty & vs is_vertex_seq_of cd & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g3,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not cd is empty & vs is_vertex_seq_of cd & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
cd is
empty
;
( vs is_vertex_seq_of cd & vs . 1 = g1 & vs . (len vs) = g2 )
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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len cd) + 1
by l, FINSEQ_1:45;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len cd or cd . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len cd or cd . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len cd )
;
cd . n joins vs /. n,vs /. (n + 1)
then
( 1
<= n &
n <= 1
+ 1 )
by l;
then
not not
n = 1
+ 0 & ... & not
n = 1
+ 1
by NAT_1:62;
then
(
n = 1 or
n = 2 )
;
per cases then
( n = 1 or n = 2 )
;
suppose n:
n = 1
;
cd . n joins vs /. n,vs /. (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, FINSEQ_1:45
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g3
by FINSEQ_1:45
;
(
[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;
verum end; suppose n:
n = 2
;
cd . n joins vs /. n,vs /. (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:
( 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, FINSEQ_1:45
;
v2:
vs /. (n + 1) =
vs . 3
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:45
;
(
[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;
verum end;
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:45;
verum end; suppose gg:
(
g1 = 2 &
g2 = 0 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
20
in KEdges
by ENUMSET1:def 5;
then reconsider c =
<*20*> as
Path of
KoenigsbergBridges by GRAPH_3:4;
take
c
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
c is
empty
;
( vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len c) + 1
by l, FINSEQ_1:44;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs /. n,vs /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 20
by l;
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, FINSEQ_1:44
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:44;
verum suppose gg:
(
g1 = 2 &
g2 = 1 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
40
in KEdges
by ENUMSET1:def 5;
then reconsider c =
<*40*> as
Path of
KoenigsbergBridges by GRAPH_3:4;
take
c
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
c is
empty
;
( vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len c) + 1
by l, FINSEQ_1:44;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs /. n,vs /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 40
by l;
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, FINSEQ_1:44
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:44;
verum suppose gg:
(
g1 = 2 &
g2 = 3 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
60
in KEdges
by ENUMSET1:def 5;
then reconsider c =
<*60*> as
Path of
KoenigsbergBridges by GRAPH_3:4;
take
c
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
c is
empty
;
( vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len c) + 1
by l, FINSEQ_1:44;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs /. n,vs /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 60
by l;
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, FINSEQ_1:44
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:44;
verum suppose gg:
(
g1 = 3 &
g2 = 0 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
30
in KEdges
by ENUMSET1:def 5;
then reconsider c =
<*30*> as
Path of
KoenigsbergBridges by GRAPH_3:4;
take
c
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
c is
empty
;
( vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len c) + 1
by l, FINSEQ_1:44;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs /. n,vs /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 30
by l;
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, FINSEQ_1:44
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:44;
verum suppose gg:
(
g1 = 3 &
g2 = 1 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs1 /. b1,vs1 /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs1 /. n,vs1 /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs1 /. n,vs1 /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 60
by l;
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, FINSEQ_1:44
;
v2:
vs1 /. (n + 1) =
vs1 . 2
by d, n, PARTFUN1:def 6
.=
g3
by FINSEQ_1:44
;
(
[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;
verum
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;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len d or d . b1 joins vs2 /. b1,vs2 /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len d or d . n joins vs2 /. n,vs2 /. (n + 1) )
assume
( 1
<= n &
n <= len d )
;
d . n joins vs2 /. n,vs2 /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
d . n = 40
by l;
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, FINSEQ_1:44
;
v2:
vs2 /. (n + 1) =
vs2 . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
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, FINSEQ_1:44
.=
vs2 . 1
by FINSEQ_1:44
;
then reconsider cd =
c ^ d as
Path of
KoenigsbergBridges by vs1, vs2, r, GRAPH_3:6;
take
cd
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not cd is empty & vs is_vertex_seq_of cd & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g3,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not cd is empty & vs is_vertex_seq_of cd & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
cd is
empty
;
( vs is_vertex_seq_of cd & vs . 1 = g1 & vs . (len vs) = g2 )
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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len cd) + 1
by l, FINSEQ_1:45;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len cd or cd . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len cd or cd . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len cd )
;
cd . n joins vs /. n,vs /. (n + 1)
then
( 1
<= n &
n <= 1
+ 1 )
by l;
then
not not
n = 1
+ 0 & ... & not
n = 1
+ 1
by NAT_1:62;
then
(
n = 1 or
n = 2 )
;
per cases then
( n = 1 or n = 2 )
;
suppose n:
n = 1
;
cd . n joins vs /. n,vs /. (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, FINSEQ_1:45
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g3
by FINSEQ_1:45
;
(
[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;
verum end; suppose n:
n = 2
;
cd . n joins vs /. n,vs /. (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:
( 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, FINSEQ_1:45
;
v2:
vs /. (n + 1) =
vs . 3
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:45
;
(
[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;
verum end;
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:45;
verum end; suppose gg:
(
g1 = 3 &
g2 = 2 )
;
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )
60
in KEdges
by ENUMSET1:def 5;
then reconsider c =
<*60*> as
Path of
KoenigsbergBridges by GRAPH_3:4;
take
c
;
ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )reconsider vs =
<*g1,g2*> as
FinSequence of the
carrier of
KoenigsbergBridges ;
take
vs
;
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )thus
not
c is
empty
;
( vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )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
( vs . 1 = g1 & vs . (len vs) = g2 )proof
thus
len vs = (len c) + 1
by l, FINSEQ_1:44;
GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins vs /. b1,vs /. (b1 + 1) )
let n be
Nat;
( not 1 <= n or not n <= len c or c . n joins vs /. n,vs /. (n + 1) )
assume
( 1
<= n &
n <= len c )
;
c . n joins vs /. n,vs /. (n + 1)
then n:
n = 1
by l, XXREAL_0:1;
then cn:
c . n = 60
by l;
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, FINSEQ_1:44
;
v2:
vs /. (n + 1) =
vs . 2
by d, n, PARTFUN1:def 6
.=
g2
by FINSEQ_1:44
;
(
[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;
verum
end; thus
(
vs . 1
= g1 &
vs . (len vs) = g2 )
by lv, FINSEQ_1:44;
verum
end;
hence
( KoenigsbergBridges is finite & KoenigsbergBridges is connected )
by GRAPH_3:18; verum