let G1 be _Graph; :: thesis: for G2 being Subgraph of G1

for W1 being Walk of G1

for W2 being Walk of G2 st W1 = W2 holds

( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

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

for W2 being Walk of G2 st W1 = W2 holds

( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 holds

( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

let W2 be Walk of G2; :: thesis: ( W1 = W2 implies ( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) ) )

assume A1: W1 = W2 ; :: thesis: ( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

then A2: W1 .last() = W2 .last() ;

W1 .first() = W2 .first() by A1;

hence ( W1 is closed iff W2 is closed ) by A2; :: thesis: ( ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

( W1 is trivial iff len W2 = 1 ) by A1, Lm55;

hence ( W1 is trivial iff W2 is trivial ) by Lm55; :: thesis: ( ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

( W1 is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W2 holds

W2 . m <> W2 . n ) by A1, Lm57;

hence A6: ( W1 is Trail-like iff W2 is Trail-like ) by Lm57; :: thesis: ( ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

( W1 is Path-like iff ( W1 is Trail-like & ( for m, n being odd Element of NAT st m < n & n <= len W2 & W2 . m = W2 . n holds

( m = 1 & n = len W2 ) ) ) ) by A1;

hence ( W1 is Path-like iff W2 is Path-like ) by A6; :: thesis: ( W1 is vertex-distinct iff W2 is vertex-distinct )

( W1 is vertex-distinct iff for m, n being odd Element of NAT st m <= len W2 & n <= len W2 & W2 . m = W2 . n holds

m = n ) by A1;

hence ( W1 is vertex-distinct iff W2 is vertex-distinct ) ; :: thesis: verum

for W1 being Walk of G1

for W2 being Walk of G2 st W1 = W2 holds

( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

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

for W2 being Walk of G2 st W1 = W2 holds

( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 holds

( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

let W2 be Walk of G2; :: thesis: ( W1 = W2 implies ( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) ) )

assume A1: W1 = W2 ; :: thesis: ( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

then A2: W1 .last() = W2 .last() ;

W1 .first() = W2 .first() by A1;

hence ( W1 is closed iff W2 is closed ) by A2; :: thesis: ( ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

now :: thesis: ( ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed Walk of G1 ) )

hence W1 is directed Walk of G1 by A1, Th173; :: thesis: verum

end;

hence
( W1 is directed iff W2 is directed )
; :: thesis: ( ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )hereby :: thesis: ( W2 is directed implies W1 is directed Walk of G1 )

assume
W2 is directed
; :: thesis: W1 is directed Walk of G1assume A3:
W1 is directed
; :: thesis: W2 is directed

end;now :: thesis: for n being odd Element of NAT st n < len W2 holds

(the_Source_of G2) . (W2 . (n + 1)) = W2 . n

hence
W2 is directed
; :: thesis: verum(the_Source_of G2) . (W2 . (n + 1)) = W2 . n

let n be odd Element of NAT ; :: thesis: ( n < len W2 implies (the_Source_of G2) . (W2 . (n + 1)) = W2 . n )

A4: 1 <= n + 1 by NAT_1:12;

assume A5: n < len W2 ; :: thesis: (the_Source_of G2) . (W2 . (n + 1)) = W2 . n

then n + 1 <= len W2 by NAT_1:13;

then n + 1 in dom W2 by A4, FINSEQ_3:25;

then W2 . (n + 1) in the_Edges_of G2 by Th7;

then (the_Source_of G2) . (W2 . (n + 1)) = (the_Source_of G1) . (W2 . (n + 1)) by GLIB_000:def 32;

hence (the_Source_of G2) . (W2 . (n + 1)) = W2 . n by A1, A3, A5; :: thesis: verum

end;A4: 1 <= n + 1 by NAT_1:12;

assume A5: n < len W2 ; :: thesis: (the_Source_of G2) . (W2 . (n + 1)) = W2 . n

then n + 1 <= len W2 by NAT_1:13;

then n + 1 in dom W2 by A4, FINSEQ_3:25;

then W2 . (n + 1) in the_Edges_of G2 by Th7;

then (the_Source_of G2) . (W2 . (n + 1)) = (the_Source_of G1) . (W2 . (n + 1)) by GLIB_000:def 32;

hence (the_Source_of G2) . (W2 . (n + 1)) = W2 . n by A1, A3, A5; :: thesis: verum

hence W1 is directed Walk of G1 by A1, Th173; :: thesis: verum

( W1 is trivial iff len W2 = 1 ) by A1, Lm55;

hence ( W1 is trivial iff W2 is trivial ) by Lm55; :: thesis: ( ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

( W1 is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W2 holds

W2 . m <> W2 . n ) by A1, Lm57;

hence A6: ( W1 is Trail-like iff W2 is Trail-like ) by Lm57; :: thesis: ( ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )

( W1 is Path-like iff ( W1 is Trail-like & ( for m, n being odd Element of NAT st m < n & n <= len W2 & W2 . m = W2 . n holds

( m = 1 & n = len W2 ) ) ) ) by A1;

hence ( W1 is Path-like iff W2 is Path-like ) by A6; :: thesis: ( W1 is vertex-distinct iff W2 is vertex-distinct )

( W1 is vertex-distinct iff for m, n being odd Element of NAT st m <= len W2 & n <= len W2 & W2 . m = W2 . n holds

m = n ) by A1;

hence ( W1 is vertex-distinct iff W2 is vertex-distinct ) ; :: thesis: verum