let G be Graph; :: thesis: 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; :: thesis: ( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )

( 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; :: thesis: ( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )

hereby :: thesis: ( ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) implies sc is Path of G )

assume A4:
( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 )
; :: thesis: sc is Path of Gassume A1:
sc is Path of G
; :: thesis: ( not len sc = 0 & not len sc = 1 implies not sc . 1 = sc . 2 )

assume A2: not len sc = 0 ; :: thesis: ( not len sc = 1 implies not sc . 1 = sc . 2 )

assume not len sc = 1 ; :: thesis: not sc . 1 = sc . 2

then len sc > 1 by A2, NAT_1:25;

then A3: 1 + 1 <= len sc by NAT_1:13;

assume sc . 1 = sc . 2 ; :: thesis: contradiction

hence contradiction by A1, A3, GRAPH_1:def 16; :: thesis: verum

end;assume A2: not len sc = 0 ; :: thesis: ( not len sc = 1 implies not sc . 1 = sc . 2 )

assume not len sc = 1 ; :: thesis: not sc . 1 = sc . 2

then len sc > 1 by A2, NAT_1:25;

then A3: 1 + 1 <= len sc by NAT_1:13;

assume sc . 1 = sc . 2 ; :: thesis: contradiction

hence contradiction by A1, A3, GRAPH_1:def 16; :: thesis: verum

per cases
( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 )
by A4;

end;

suppose
len sc = 0
; :: thesis: sc is Path of G

then
for n, m being Nat st 1 <= n & n < m & m <= len sc holds

sc . n <> sc . m ;

hence sc is Path of G by GRAPH_1:def 16; :: thesis: verum

end;sc . n <> sc . m ;

hence sc is Path of G by GRAPH_1:def 16; :: thesis: verum

suppose
len sc = 1
; :: thesis: sc is Path of G

then
for n, m being Nat st 1 <= n & n < m & m <= len sc holds

sc . n <> sc . m by XXREAL_0:2;

hence sc is Path of G by GRAPH_1:def 16; :: thesis: verum

end;sc . n <> sc . m by XXREAL_0:2;

hence sc is Path of G by GRAPH_1:def 16; :: thesis: verum

suppose A5:
sc . 1 <> sc . 2
; :: thesis: sc is Path of G

end;

now :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len sc holds

sc . n <> sc . m

hence
sc is Path of G
by GRAPH_1:def 16; :: thesis: verumsc . n <> sc . m

let n, m be Nat; :: thesis: ( 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 ; :: thesis: sc . n <> sc . m

thus sc . n <> sc . m :: thesis: verum

end;assume that

A6: 1 <= n and

A7: n < m and

A8: m <= len sc ; :: thesis: sc . n <> sc . m

thus sc . n <> sc . m :: thesis: verum

proof

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 ; :: thesis: contradiction

end;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 ; :: thesis: 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;

end;

suppose A23:
( vs /. n = vs /. m & vs /. (n + 1) = vs /. (m + 1) )
; :: thesis: contradiction

A24:
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; :: thesis: verum

end;n = 1 by A6, A7, A10, A20, A17, A21, A23;

hence contradiction by A10, A12, A16, A13, A23, A24; :: thesis: verum

suppose A25:
( vs /. n = vs /. (m + 1) & vs /. (n + 1) = vs /. m )
; :: thesis: contradiction

thus
contradiction
:: thesis: verum

end;