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 )
proof
assume A4: W1 is Path-like ; :: thesis: W2 is Path-like
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;
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;
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;
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;
per cases ( n = m + 2 or m + 2 < n or n < m + 2 ) by XXREAL_0:1;
suppose m + 2 < n ; :: thesis: contradiction
then ( m + 2 < n & n <= len W1 ) by A1, A9, Th30;
hence contradiction by A4, A7, A14, A15, GLIB_001:def 28; :: thesis: verum
end;
suppose n < m + 2 ; :: thesis: contradiction
then ( n < m + 2 & m + 2 <= len W2 ) by A11, CHORD:4;
then ( n < m + 2 & m + 2 <= len W1 ) by A1, Th30;
then n = 1 by A4, A7, A14, GLIB_001:def 28;
hence contradiction by A8, A15; :: thesis: verum
end;
end;
end;
end;
end;
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 )
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;
hence W2 is Path-like by A5, GLIB_001:def 28; :: thesis: verum
end;
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;