let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & len W1 <> 5 holds

( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) )

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & len W1 <> 5 holds

( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) )

let W2 be Walk of G2; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() & len W1 <> 5 implies ( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) ) )

assume A1: W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: ( not len W1 <> 5 or ( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) ) )

assume A2: len W1 <> 5 ; :: thesis: ( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) )

thus A3: ( W1 is Path-like implies W2 is Path-like ) :: thesis: ( W1 is Cycle-like implies W2 is Cycle-like )

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & len W1 <> 5 holds

( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) )

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & len W1 <> 5 holds

( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) )

let W2 be Walk of G2; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() & len W1 <> 5 implies ( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) ) )

assume A1: W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: ( not len W1 <> 5 or ( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) ) )

assume A2: len W1 <> 5 ; :: thesis: ( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) )

thus A3: ( W1 is Path-like implies W2 is Path-like ) :: thesis: ( W1 is Cycle-like implies W2 is Cycle-like )

proof

assume A4:
W1 is Path-like
; :: thesis: W2 is Path-like

A5: W2 is Trail-like

end;A5: W2 is Trail-like

proof

assume
not W2 is Trail-like
; :: thesis: contradiction

then consider m1, n1 being even Element of NAT such that

A6: ( 1 <= m1 & m1 < n1 & n1 <= len W2 & W2 . m1 = W2 . n1 ) by GLIB_001:138;

( not m1 is zero & not n1 is zero ) by A6;

then ( m1 - 1 is Nat & n1 - 1 is Nat ) by CHORD:1;

then reconsider m = m1 - 1, n = n1 - 1 as odd Element of NAT by ORDINAL1:def 12;

A7: ( W1 . n = W2 . n & W1 . m = W2 . m & W1 . (n + 2) = W2 . (n + 2) & W1 . (m + 2) = W2 . (m + 2) ) by A1, Th29;

A8: m < n by A6, XREAL_1:9;

A9: n < (len W2) - 0 by A6, XREAL_1:15;

then A10: W2 . (n + 1) Joins W2 . n,W2 . (n + 2),G2 by GLIB_001:def 3;

A11: m < len W2 by A8, A9, XXREAL_0:2;

then A12: W2 . (m + 1) Joins W2 . m,W2 . (m + 2),G2 by GLIB_001:def 3;

n + 2 <= len W2 by A9, CHORD:4;

then A13: n + 2 <= (len W1) + 0 by A1, Th30;

end;then consider m1, n1 being even Element of NAT such that

A6: ( 1 <= m1 & m1 < n1 & n1 <= len W2 & W2 . m1 = W2 . n1 ) by GLIB_001:138;

( not m1 is zero & not n1 is zero ) by A6;

then ( m1 - 1 is Nat & n1 - 1 is Nat ) by CHORD:1;

then reconsider m = m1 - 1, n = n1 - 1 as odd Element of NAT by ORDINAL1:def 12;

A7: ( W1 . n = W2 . n & W1 . m = W2 . m & W1 . (n + 2) = W2 . (n + 2) & W1 . (m + 2) = W2 . (m + 2) ) by A1, Th29;

A8: m < n by A6, XREAL_1:9;

A9: n < (len W2) - 0 by A6, XREAL_1:15;

then A10: W2 . (n + 1) Joins W2 . n,W2 . (n + 2),G2 by GLIB_001:def 3;

A11: m < len W2 by A8, A9, XXREAL_0:2;

then A12: W2 . (m + 1) Joins W2 . m,W2 . (m + 2),G2 by GLIB_001:def 3;

n + 2 <= len W2 by A9, CHORD:4;

then A13: n + 2 <= (len W1) + 0 by A1, Th30;

per cases
( ( W2 . n = W2 . m & W2 . (n + 2) = W2 . (m + 2) ) or ( W2 . n = W2 . (m + 2) & W2 . (n + 2) = W2 . m ) )
by A6, A10, A12, GLIB_000:15;

end;

suppose
( W2 . n = W2 . m & W2 . (n + 2) = W2 . (m + 2) )
; :: thesis: contradiction

then
( W1 . n = W1 . m & n <= len W1 )
by A1, A7, A9, Th30;

then n = len W1 by A4, A8, GLIB_001:def 28;

hence contradiction by A13, XREAL_1:6; :: thesis: verum

end;then n = len W1 by A4, A8, GLIB_001:def 28;

hence contradiction by A13, XREAL_1:6; :: thesis: verum

suppose A14:
( W2 . n = W2 . (m + 2) & W2 . (n + 2) = W2 . m )
; :: thesis: contradiction

then
( W1 . m = W1 . (n + 2) & m + 0 < n + 2 )
by A7, A8, XREAL_1:8;

then A15: ( m = 1 & n + 2 = len W1 ) by A4, A13, GLIB_001:def 28;

end;then A15: ( m = 1 & n + 2 = len W1 ) by A4, A13, GLIB_001:def 28;

now :: thesis: for m, n being odd Element of NAT st m < n & n <= len W2 & W2 . m = W2 . n holds

( m = 1 & n = len W2 )

hence
W2 is Path-like
by A5, GLIB_001:def 28; :: thesis: verum( m = 1 & n = len W2 )

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len W2 & W2 . m = W2 . n implies ( m = 1 & n = len W2 ) )

assume A16: ( m < n & n <= len W2 & W2 . m = W2 . n ) ; :: thesis: ( m = 1 & n = len W2 )

( W1 . m = W2 . m & W1 . n = W2 . n & len W1 = len W2 ) by A1, Th30, Th29;

hence ( m = 1 & n = len W2 ) by A4, A16, GLIB_001:def 28; :: thesis: verum

end;assume A16: ( m < n & n <= len W2 & W2 . m = W2 . n ) ; :: thesis: ( m = 1 & n = len W2 )

( W1 . m = W2 . m & W1 . n = W2 . n & len W1 = len W2 ) by A1, Th30, Th29;

hence ( m = 1 & n = len W2 ) by A4, A16, GLIB_001:def 28; :: thesis: verum

hereby :: thesis: verum

assume
W1 is Cycle-like
; :: thesis: W2 is Cycle-like

then ( W2 is closed & W2 is Path-like & W2 is V5() ) by A1, A3, Th31;

hence W2 is Cycle-like ; :: thesis: verum

end;then ( W2 is closed & W2 is Path-like & W2 is V5() ) by A1, A3, Th31;

hence W2 is Cycle-like ; :: thesis: verum