let G be _Graph; :: thesis: for p being FinSequence of the_Vertices_of G
for q being FinSequence of the_Edges_of G st len p = 1 + (len q) & ( for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G ) holds
ex W being Walk of G st
( W .vertexSeq() = p & W .edgeSeq() = q )

let p be FinSequence of the_Vertices_of G; :: thesis: for q being FinSequence of the_Edges_of G st len p = 1 + (len q) & ( for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G ) holds
ex W being Walk of G st
( W .vertexSeq() = p & W .edgeSeq() = q )

let q be FinSequence of the_Edges_of G; :: thesis: ( len p = 1 + (len q) & ( for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G ) implies ex W being Walk of G st
( W .vertexSeq() = p & W .edgeSeq() = q ) )

assume that
A1: len p = 1 + (len q) and
A2: for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G ; :: thesis: ex W being Walk of G st
( W .vertexSeq() = p & W .edgeSeq() = q )

defpred S1[ object , object ] means ex m being Nat st
( m = \$1 & ( m is odd implies \$2 = p . ((m + 1) div 2) ) & ( m is even implies \$2 = q . (m div 2) ) );
A3: for k being Nat st k in Seg ((len p) + (len q)) holds
ex x being Element of () \/ () st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg ((len p) + (len q)) implies ex x being Element of () \/ () st S1[k,x] )
assume k in Seg ((len p) + (len q)) ; :: thesis: ex x being Element of () \/ () st S1[k,x]
then A4: ( 1 <= k & k <= (len p) + (len q) ) by FINSEQ_1:1;
per cases ( k is odd or k is even ) ;
suppose A5: k is odd ; :: thesis: ex x being Element of () \/ () st S1[k,x]
k + 0 <= ((len p) + (len q)) + 1 by ;
then A6: k <= 2 * (len p) by A1;
1 + 1 <= k + 1 by ;
then 1 <= (k + 1) div 2 by NAT_2:13;
then (k + 1) div 2 in dom p by ;
then p . ((k + 1) div 2) in rng p by FUNCT_1:3;
then reconsider x = p . ((k + 1) div 2) as Element of () \/ () by XBOOLE_0:def 3;
take x ; :: thesis: S1[k,x]
take k ; :: thesis: ( k = k & ( k is odd implies x = p . ((k + 1) div 2) ) & ( k is even implies x = q . (k div 2) ) )
thus k = k ; :: thesis: ( ( k is odd implies x = p . ((k + 1) div 2) ) & ( k is even implies x = q . (k div 2) ) )
thus ( k is odd implies x = p . ((k + 1) div 2) ) ; :: thesis: ( k is even implies x = q . (k div 2) )
thus ( k is even implies x = q . (k div 2) ) by A5; :: thesis: verum
end;
suppose A7: k is even ; :: thesis: ex x being Element of () \/ () st S1[k,x]
A8: k - 1 = k -' 1 by ;
reconsider r = k - 1 as Nat by A8;
r <= (1 + (2 * (len q))) - 1 by ;
then A9: (r + 1) div 2 <= len q by NAT_2:25;
2 <= k
proof
assume A10: k < 2 ; :: thesis: contradiction
consider s being Nat such that
A11: k = 2 * s by ;
(2 * s) / 2 < (1 * 2) / 2 by ;
then s = 0 by NAT_1:14;
hence contradiction by A4, A11; :: thesis: verum
end;
then 1 <= k div 2 by NAT_2:13;
then k div 2 in dom q by ;
then q . (k div 2) in rng q by FUNCT_1:3;
then reconsider x = q . (k div 2) as Element of () \/ () by XBOOLE_0:def 3;
take x ; :: thesis: S1[k,x]
take k ; :: thesis: ( k = k & ( k is odd implies x = p . ((k + 1) div 2) ) & ( k is even implies x = q . (k div 2) ) )
thus k = k ; :: thesis: ( ( k is odd implies x = p . ((k + 1) div 2) ) & ( k is even implies x = q . (k div 2) ) )
thus ( k is odd implies x = p . ((k + 1) div 2) ) by A7; :: thesis: ( k is even implies x = q . (k div 2) )
thus ( k is even implies x = q . (k div 2) ) ; :: thesis: verum
end;
end;
end;
consider W being FinSequence of () \/ () such that
A12: dom W = Seg ((len p) + (len q)) and
A13: for k being Nat st k in Seg ((len p) + (len q)) holds
S1[k,W . k] from A14: len W = (2 * (len q)) + 1 by ;
A15: W . 1 in the_Vertices_of G
proof
1 + 0 <= 1 + ((len q) + (len q)) by XREAL_1:7;
then consider m being Nat such that
A16: m = 1 and
A17: ( m is odd implies W . 1 = p . ((m + 1) div 2) ) and
( m is even implies W . 1 = q . (m div 2) ) by ;
A18: W . 1 = p . ((m + 1) div 2) by
.= p . 1 by ;
1 + 0 <= 1 + (len q) by XREAL_1:7;
then 1 in dom p by ;
then p . 1 in rng p by FUNCT_1:3;
hence W . 1 in the_Vertices_of G by A18; :: thesis: verum
end;
for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),G
proof
let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) Joins W . n,W . (n + 2),G )
assume A19: n < len W ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G
set m = (n + 1) div 2;
1 + 1 <= n + 1 by ;
then A20: 1 <= (n + 1) div 2 by NAT_2:13;
reconsider m = (n + 1) div 2 as Nat ;
A21: ( 1 + 0 <= n + 1 & 1 + 0 <= n + 2 ) by XREAL_1:7;
A22: n + 2 <= len W by ;
( n + 0 <= n + 2 & n + 1 <= n + 2 ) by XREAL_1:7;
then ( n <= len W & n + 1 <= len W ) by ;
then A23: ( n in dom W & n + 1 in dom W & n + 2 in dom W ) by ;
A24: ((n + 2) + 1) div 2 = ((n + 1) + 2) div 2
.= m + 1 by NAT_2:14 ;
consider n0 being Nat such that
A25: n0 = n and
A26: ( n0 is odd implies W . n = p . ((n0 + 1) div 2) ) and
( n0 is even implies W . n = q . (n0 div 2) ) by ;
consider n1 being Nat such that
A27: n1 = n + 1 and
( n1 is odd implies W . (n + 1) = p . ((n1 + 1) div 2) ) and
A28: ( n1 is even implies W . (n + 1) = q . (n1 div 2) ) by ;
consider n2 being Nat such that
A29: n2 = n + 2 and
A30: ( n2 is odd implies W . (n + 2) = p . ((n2 + 1) div 2) ) and
( n2 is even implies W . (n + 2) = q . (n2 div 2) ) by ;
A31: W . n = p . m by ;
A32: W . (n + 1) = q . m by ;
A33: W . (n + 2) = p . (m + 1) by ;
A34: n + 2 <= ((len p) - 1) + (len p) by ;
(2 * (len p)) - 1 <= (2 * (len p)) - 0 by XREAL_1:13;
then n + 2 <= 2 * (len p) by ;
then ((n + 2) + 1) div 2 <= len p by NAT_2:25;
then ((n + 1) + 2) div 2 <= len p ;
then m + 1 <= len p by NAT_2:14;
hence W . (n + 1) Joins W . n,W . (n + 2),G by A2, A20, A31, A32, A33; :: thesis: verum
end;
then reconsider W = W as Walk of G by ;
take W ; :: thesis: ( W .vertexSeq() = p & W .edgeSeq() = q )
A35: 2 * (len ()) = (len W) + 1 by GLIB_001:def 14
.= ((len p) + (len q)) + 1 by
.= 2 * (len p) by A1 ;
for k being Nat st 1 <= k & k <= len p holds
p . k = () . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len p implies p . k = () . k )
assume A36: ( 1 <= k & k <= len p ) ; :: thesis: p . k = () . k
2 * k <= 2 * (len p) by ;
then A37: (2 * k) - 1 <= (((len p) + 1) + (len q)) - 1 by ;
2 * 1 <= 2 * k by ;
then A38: (1 + 1) - 1 <= (2 * k) - 1 by XREAL_1:9;
then (2 * k) - 1 in NAT by INT_1:3;
then consider m being Nat such that
A39: m = (2 * k) - 1 and
A40: ( m is odd implies W . ((2 * k) - 1) = p . ((m + 1) div 2) ) and
( m is even implies W . ((2 * k) - 1) = q . (m div 2) ) by ;
W . ((2 * k) - 1) = p . k by ;
hence p . k = () . k by ; :: thesis: verum
end;
hence W .vertexSeq() = p by ; :: thesis:
A41: (2 * (len ())) + 1 = (2 * (len q)) + 1 by ;
for k being Nat st 1 <= k & k <= len q holds
q . k = () . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len q implies q . k = () . k )
assume A42: ( 1 <= k & k <= len q ) ; :: thesis: q . k = () . k
then A43: (W .edgeSeq()) . k = W . (2 * k) by ;
2 * k <= 2 * (len q) by ;
then A44: (2 * k) + 0 <= ((len q) + (len q)) + 1 by XREAL_1:7;
1 * 1 <= 2 * k by ;
then consider m being Nat such that
A45: m = 2 * k and
( m is odd implies W . (2 * k) = p . ((m + 1) div 2) ) and
A46: ( m is even implies W . (2 * k) = q . (m div 2) ) by ;
thus q . k = () . k by ; :: thesis: verum
end;
hence W .edgeSeq() = q by ; :: thesis: verum