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 S_{1}[ 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 (the_Vertices_of G) \/ (the_Edges_of G) st S_{1}[k,x]

A12: dom W = Seg ((len p) + (len q)) and

A13: for k being Nat st k in Seg ((len p) + (len q)) holds

S_{1}[k,W . k]
from FINSEQ_1:sch 5(A3);

A14: len W = (2 * (len q)) + 1 by A1, A12, FINSEQ_1:def 3;

A15: W . 1 in the_Vertices_of G

W . (n + 1) Joins W . n,W . (n + 2),G

take W ; :: thesis: ( W .vertexSeq() = p & W .edgeSeq() = q )

A35: 2 * (len (W .vertexSeq())) = (len W) + 1 by GLIB_001:def 14

.= ((len p) + (len q)) + 1 by A12, FINSEQ_1:def 3

.= 2 * (len p) by A1 ;

for k being Nat st 1 <= k & k <= len p holds

p . k = (W .vertexSeq()) . k

A41: (2 * (len (W .edgeSeq()))) + 1 = (2 * (len q)) + 1 by A14, GLIB_001:def 15;

for k being Nat st 1 <= k & k <= len q holds

q . k = (W .edgeSeq()) . k

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 S

( 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 (the_Vertices_of G) \/ (the_Edges_of G) st S

proof

consider W being FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) such that
let k be Nat; :: thesis: ( k in Seg ((len p) + (len q)) implies ex x being Element of (the_Vertices_of G) \/ (the_Edges_of G) st S_{1}[k,x] )

assume k in Seg ((len p) + (len q)) ; :: thesis: ex x being Element of (the_Vertices_of G) \/ (the_Edges_of G) st S_{1}[k,x]

then A4: ( 1 <= k & k <= (len p) + (len q) ) by FINSEQ_1:1;

end;assume k in Seg ((len p) + (len q)) ; :: thesis: ex x being Element of (the_Vertices_of G) \/ (the_Edges_of G) st S

then A4: ( 1 <= k & k <= (len p) + (len q) ) by FINSEQ_1:1;

per cases
( k is odd or k is even )
;

end;

suppose A5:
k is odd
; :: thesis: ex x being Element of (the_Vertices_of G) \/ (the_Edges_of G) st S_{1}[k,x]

k + 0 <= ((len p) + (len q)) + 1
by A4, XREAL_1:7;

then A6: k <= 2 * (len p) by A1;

1 + 1 <= k + 1 by A5, ABIAN:12, XREAL_1:6;

then 1 <= (k + 1) div 2 by NAT_2:13;

then (k + 1) div 2 in dom p by A6, FINSEQ_3:25, NAT_2:25;

then p . ((k + 1) div 2) in rng p by FUNCT_1:3;

then reconsider x = p . ((k + 1) div 2) as Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

take x ; :: thesis: S_{1}[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;then A6: k <= 2 * (len p) by A1;

1 + 1 <= k + 1 by A5, ABIAN:12, XREAL_1:6;

then 1 <= (k + 1) div 2 by NAT_2:13;

then (k + 1) div 2 in dom p by A6, FINSEQ_3:25, NAT_2:25;

then p . ((k + 1) div 2) in rng p by FUNCT_1:3;

then reconsider x = p . ((k + 1) div 2) as Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

take x ; :: thesis: S

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

suppose A7:
k is even
; :: thesis: ex x being Element of (the_Vertices_of G) \/ (the_Edges_of G) st S_{1}[k,x]

A8:
k - 1 = k -' 1
by A4, XREAL_1:233;

reconsider r = k - 1 as Nat by A8;

r <= (1 + (2 * (len q))) - 1 by A1, A4, XREAL_1:9;

then A9: (r + 1) div 2 <= len q by NAT_2:25;

2 <= k

then k div 2 in dom q by A9, FINSEQ_3:25;

then q . (k div 2) in rng q by FUNCT_1:3;

then reconsider x = q . (k div 2) as Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

take x ; :: thesis: S_{1}[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;reconsider r = k - 1 as Nat by A8;

r <= (1 + (2 * (len q))) - 1 by A1, A4, XREAL_1:9;

then A9: (r + 1) div 2 <= len q by NAT_2:25;

2 <= k

proof

then
1 <= k div 2
by NAT_2:13;
assume A10:
k < 2
; :: thesis: contradiction

consider s being Nat such that

A11: k = 2 * s by A7, ABIAN:def 2;

(2 * s) / 2 < (1 * 2) / 2 by A10, A11, XREAL_1:81;

then s = 0 by NAT_1:14;

hence contradiction by A4, A11; :: thesis: verum

end;consider s being Nat such that

A11: k = 2 * s by A7, ABIAN:def 2;

(2 * s) / 2 < (1 * 2) / 2 by A10, A11, XREAL_1:81;

then s = 0 by NAT_1:14;

hence contradiction by A4, A11; :: thesis: verum

then k div 2 in dom q by A9, FINSEQ_3:25;

then q . (k div 2) in rng q by FUNCT_1:3;

then reconsider x = q . (k div 2) as Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

take x ; :: thesis: S

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

A12: dom W = Seg ((len p) + (len q)) and

A13: for k being Nat st k in Seg ((len p) + (len q)) holds

S

A14: len W = (2 * (len q)) + 1 by A1, A12, FINSEQ_1:def 3;

A15: W . 1 in the_Vertices_of G

proof

for n being odd Element of NAT st n < len W holds
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 A1, A13, FINSEQ_1:1;

A18: W . 1 = p . ((m + 1) div 2) by A16, A17

.= p . 1 by A16, NAT_2:3 ;

1 + 0 <= 1 + (len q) by XREAL_1:7;

then 1 in dom p by A1, FINSEQ_3:25;

then p . 1 in rng p by FUNCT_1:3;

hence W . 1 in the_Vertices_of G by A18; :: thesis: verum

end;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 A1, A13, FINSEQ_1:1;

A18: W . 1 = p . ((m + 1) div 2) by A16, A17

.= p . 1 by A16, NAT_2:3 ;

1 + 0 <= 1 + (len q) by XREAL_1:7;

then 1 in dom p by A1, FINSEQ_3:25;

then p . 1 in rng p by FUNCT_1:3;

hence W . 1 in the_Vertices_of G by A18; :: thesis: verum

W . (n + 1) Joins W . n,W . (n + 2),G

proof

then reconsider W = W as Walk of G by A14, A15, GLIB_001:def 3;
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 ABIAN:12, XREAL_1:6;

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 A14, A19, GLIB_001:1;

( n + 0 <= n + 2 & n + 1 <= n + 2 ) by XREAL_1:7;

then ( n <= len W & n + 1 <= len W ) by A22, XXREAL_0:2;

then A23: ( n in dom W & n + 1 in dom W & n + 2 in dom W ) by A21, A22, ABIAN:12, FINSEQ_3:25;

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 A12, A13, A23;

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 A12, A13, A23;

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 A12, A13, A23;

A31: W . n = p . m by A25, A26;

A32: W . (n + 1) = q . m by A27, A28;

A33: W . (n + 2) = p . (m + 1) by A24, A29, A30;

A34: n + 2 <= ((len p) - 1) + (len p) by A1, A12, A22, FINSEQ_1:def 3;

(2 * (len p)) - 1 <= (2 * (len p)) - 0 by XREAL_1:13;

then n + 2 <= 2 * (len p) by A34, XXREAL_0:2;

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;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 ABIAN:12, XREAL_1:6;

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 A14, A19, GLIB_001:1;

( n + 0 <= n + 2 & n + 1 <= n + 2 ) by XREAL_1:7;

then ( n <= len W & n + 1 <= len W ) by A22, XXREAL_0:2;

then A23: ( n in dom W & n + 1 in dom W & n + 2 in dom W ) by A21, A22, ABIAN:12, FINSEQ_3:25;

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 A12, A13, A23;

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 A12, A13, A23;

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 A12, A13, A23;

A31: W . n = p . m by A25, A26;

A32: W . (n + 1) = q . m by A27, A28;

A33: W . (n + 2) = p . (m + 1) by A24, A29, A30;

A34: n + 2 <= ((len p) - 1) + (len p) by A1, A12, A22, FINSEQ_1:def 3;

(2 * (len p)) - 1 <= (2 * (len p)) - 0 by XREAL_1:13;

then n + 2 <= 2 * (len p) by A34, XXREAL_0:2;

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

take W ; :: thesis: ( W .vertexSeq() = p & W .edgeSeq() = q )

A35: 2 * (len (W .vertexSeq())) = (len W) + 1 by GLIB_001:def 14

.= ((len p) + (len q)) + 1 by A12, FINSEQ_1:def 3

.= 2 * (len p) by A1 ;

for k being Nat st 1 <= k & k <= len p holds

p . k = (W .vertexSeq()) . k

proof

hence
W .vertexSeq() = p
by A35, FINSEQ_1:def 17; :: thesis: W .edgeSeq() = q
let k be Nat; :: thesis: ( 1 <= k & k <= len p implies p . k = (W .vertexSeq()) . k )

assume A36: ( 1 <= k & k <= len p ) ; :: thesis: p . k = (W .vertexSeq()) . k

2 * k <= 2 * (len p) by A36, XREAL_1:64;

then A37: (2 * k) - 1 <= (((len p) + 1) + (len q)) - 1 by A1, XREAL_1:9;

2 * 1 <= 2 * k by A36, XREAL_1:64;

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 A13, A37, A38, FINSEQ_1:1;

W . ((2 * k) - 1) = p . k by A39, A40, NAT_D:18;

hence p . k = (W .vertexSeq()) . k by A35, A36, GLIB_001:def 14; :: thesis: verum

end;assume A36: ( 1 <= k & k <= len p ) ; :: thesis: p . k = (W .vertexSeq()) . k

2 * k <= 2 * (len p) by A36, XREAL_1:64;

then A37: (2 * k) - 1 <= (((len p) + 1) + (len q)) - 1 by A1, XREAL_1:9;

2 * 1 <= 2 * k by A36, XREAL_1:64;

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 A13, A37, A38, FINSEQ_1:1;

W . ((2 * k) - 1) = p . k by A39, A40, NAT_D:18;

hence p . k = (W .vertexSeq()) . k by A35, A36, GLIB_001:def 14; :: thesis: verum

A41: (2 * (len (W .edgeSeq()))) + 1 = (2 * (len q)) + 1 by A14, GLIB_001:def 15;

for k being Nat st 1 <= k & k <= len q holds

q . k = (W .edgeSeq()) . k

proof

hence
W .edgeSeq() = q
by A41, FINSEQ_1:def 17; :: thesis: verum
let k be Nat; :: thesis: ( 1 <= k & k <= len q implies q . k = (W .edgeSeq()) . k )

assume A42: ( 1 <= k & k <= len q ) ; :: thesis: q . k = (W .edgeSeq()) . k

then A43: (W .edgeSeq()) . k = W . (2 * k) by A41, GLIB_001:def 15;

2 * k <= 2 * (len q) by A42, XREAL_1:64;

then A44: (2 * k) + 0 <= ((len q) + (len q)) + 1 by XREAL_1:7;

1 * 1 <= 2 * k by A42, XREAL_1:66;

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 A1, A13, A44, FINSEQ_1:1;

thus q . k = (W .edgeSeq()) . k by A43, A45, A46, NAT_D:18; :: thesis: verum

end;assume A42: ( 1 <= k & k <= len q ) ; :: thesis: q . k = (W .edgeSeq()) . k

then A43: (W .edgeSeq()) . k = W . (2 * k) by A41, GLIB_001:def 15;

2 * k <= 2 * (len q) by A42, XREAL_1:64;

then A44: (2 * k) + 0 <= ((len q) + (len q)) + 1 by XREAL_1:7;

1 * 1 <= 2 * k by A42, XREAL_1:66;

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 A1, A13, A44, FINSEQ_1:1;

thus q . k = (W .edgeSeq()) . k by A43, A45, A46, NAT_D:18; :: thesis: verum