let G be Graph; for sc being simple Chain of G holds
( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )
let sc be simple Chain of G; ( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )
hereby ( ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) implies sc is Path of G )
end;
assume A4:
( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 )
; sc is Path of G
per cases
( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 )
by A4;
suppose A5:
sc . 1
<> sc . 2
;
sc is Path of Gnow for n, m being Nat st 1 <= n & n < m & m <= len sc holds
sc . n <> sc . mlet n,
m be
Nat;
( 1 <= n & n < m & m <= len sc implies sc . n <> sc . m )assume that A6:
1
<= n
and A7:
n < m
and A8:
m <= len sc
;
sc . n <> sc . mthus
sc . n <> sc . m
verumproof
consider vs being
FinSequence of the
carrier of
G such that A9:
vs is_vertex_seq_of sc
and A10:
for
n,
m being
Nat st 1
<= n &
n < m &
m <= len vs &
vs . n = vs . m holds
(
n = 1 &
m = len vs )
by Def9;
set vm1 =
vs /. (m + 1);
A11:
len vs = (len sc) + 1
by A9;
then A12:
m + 1
<= len vs
by A8, XREAL_1:6;
then A13:
vs /. (m + 1) = vs . (m + 1)
by FINSEQ_4:15, NAT_1:12;
set vn1 =
vs /. (n + 1);
set vn =
vs /. n;
A14:
n <= len sc
by A7, A8, XXREAL_0:2;
then A15:
sc . n joins vs /. n,
vs /. (n + 1)
by A6, A9;
n + 1
<= len vs
by A11, A14, XREAL_1:6;
then A16:
vs /. (n + 1) = vs . (n + 1)
by FINSEQ_4:15, NAT_1:12;
n <= len vs
by A11, A14, NAT_1:12;
then A17:
vs /. n = vs . n
by A6, FINSEQ_4:15;
set vm =
vs /. m;
A18:
1
<= m
by A6, A7, XXREAL_0:2;
then A19:
sc . m joins vs /. m,
vs /. (m + 1)
by A8, A9;
A20:
m <= len vs
by A8, A11, NAT_1:12;
then A21:
vs /. m = vs . m
by A18, FINSEQ_4:15;
assume A22:
not
sc . n <> sc . m
;
contradiction
per cases
( ( vs /. n = vs /. m & vs /. (n + 1) = vs /. (m + 1) ) or ( vs /. n = vs /. (m + 1) & vs /. (n + 1) = vs /. m ) )
by A22, A15, A19;
suppose A23:
(
vs /. n = vs /. m &
vs /. (n + 1) = vs /. (m + 1) )
;
contradictionA24:
n + 1
< m + 1
by A7, XREAL_1:6;
n = 1
by A6, A7, A10, A20, A17, A21, A23;
hence
contradiction
by A10, A12, A16, A13, A23, A24;
verum end; suppose A25:
(
vs /. n = vs /. (m + 1) &
vs /. (n + 1) = vs /. m )
;
contradictionthus
contradiction
verumproof
A26:
n + 1
<= m
by A7, NAT_1:13;
A27:
n + 0 < m + 1
by A7, XREAL_1:8;
per cases
( n + 1 = m or n + 1 < m )
by A26, XXREAL_0:1;
suppose A29:
n + 1
< m
;
contradiction
n = 1
by A6, A10, A12, A17, A13, A25, A27;
hence
contradiction
by A10, A20, A16, A21, A25, A29;
verum end; end;
end; end; end;
end; end; hence
sc is
Path of
G
by GRAPH_1:def 16;
verum end; end;