let p, q be FinSequence; :: thesis: for G being Graph st p ^ q is oriented Simple Chain of G holds
( p is oriented Simple Chain of G & q is oriented Simple Chain of G )
let G be Graph; :: thesis: ( p ^ q is oriented Simple Chain of G implies ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) )
assume A1:
p ^ q is oriented Simple Chain of G
; :: thesis: ( p is oriented Simple Chain of G & q is oriented Simple Chain of G )
set r = p ^ q;
per cases
( p = {} or q = {} or ( not p = {} & not q = {} ) )
;
suppose A3:
( not
p = {} & not
q = {} )
;
:: thesis: ( p is oriented Simple Chain of G & q is oriented Simple Chain of G )then
len q <> 0
;
then A4:
len q > 0
;
consider vs being
FinSequence of the
carrier of
G such that A5:
(
vs is_oriented_vertex_seq_of p ^ q & ( for
n,
m being
Element of
NAT st 1
<= n &
n < m &
m <= len vs &
vs . n = vs . m holds
(
n = 1 &
m = len vs ) ) )
by A1, GRAPH_4:def 7;
A6:
(
len vs = (len (p ^ q)) + 1 & ( for
n being
Element of
NAT st 1
<= n &
n <= len (p ^ q) holds
(p ^ q) . n orientedly_joins vs /. n,
vs /. (n + 1) ) )
by A5, GRAPH_4:def 5;
A7:
len (p ^ q) = (len p) + (len q)
by FINSEQ_1:35;
then A8:
len vs = (len p) + ((len q) + 1)
by A6;
A9:
len vs = ((len p) + 1) + (len q)
by A6, A7;
then consider f1,
f2 being
FinSequence such that A10:
(
len f1 = (len p) + 1 &
len f2 = len q &
vs = f1 ^ f2 )
by FINSEQ_2:25;
reconsider f1 =
f1 as
FinSequence of the
carrier of
G by A10, FINSEQ_1:50;
now let n be
Element of
NAT ;
:: thesis: ( 1 <= n & n <= len p implies p . n orientedly_joins f1 /. n,f1 /. (n + 1) )assume A11:
( 1
<= n &
n <= len p )
;
:: thesis: p . n orientedly_joins f1 /. n,f1 /. (n + 1)
len p <= len (p ^ q)
by A7, NAT_1:11;
then A12:
n <= len (p ^ q)
by A11, XXREAL_0:2;
then A13:
(p ^ q) . n orientedly_joins vs /. n,
vs /. (n + 1)
by A5, A11, GRAPH_4:def 5;
A14:
n + 0 <= len f1
by A10, A11, XREAL_1:9;
len p <= len vs
by A8, NAT_1:11;
then
n <= len vs
by A11, XXREAL_0:2;
then A15:
n in dom vs
by A11, FINSEQ_3:27;
n in dom f1
by A11, A14, FINSEQ_3:27;
then A16:
f1 /. n =
f1 . n
by PARTFUN1:def 8
.=
vs . n
by A10, A11, A14, Lm1
.=
vs /. n
by A15, PARTFUN1:def 8
;
A17:
1
<= n + 1
by NAT_1:11;
n + 1
<= len vs
by A6, A12, XREAL_1:9;
then A18:
n + 1
in dom vs
by A17, FINSEQ_3:27;
n + 1
<= len f1
by A10, A11, XREAL_1:9;
then
n + 1
in dom f1
by A17, FINSEQ_3:27;
then f1 /. (n + 1) =
f1 . (n + 1)
by PARTFUN1:def 8
.=
vs . (n + 1)
by A10, A11, A17, Lm1, XREAL_1:9
.=
vs /. (n + 1)
by A18, PARTFUN1:def 8
;
hence
p . n orientedly_joins f1 /. n,
f1 /. (n + 1)
by A11, A13, A16, Lm1;
:: thesis: verum end; then A19:
f1 is_oriented_vertex_seq_of p
by A10, GRAPH_4:def 5;
now let n,
m be
Element of
NAT ;
:: thesis: ( 1 <= n & n < m & m <= len f1 & f1 . n = f1 . m implies ( n = 1 & m = len f1 ) )assume A20:
( 1
<= n &
n < m &
m <= len f1 &
f1 . n = f1 . m )
;
:: thesis: ( n = 1 & m = len f1 )assume
( not
n = 1 or not
m = len f1 )
;
:: thesis: contradiction
n <= len f1
by A20, XXREAL_0:2;
then A21:
f1 . n = vs . n
by A10, A20, Lm1;
1
<= m
by A20, XXREAL_0:2;
then A22:
f1 . m = vs . m
by A10, A20, Lm1;
(len f1) + 0 < len vs
by A4, A9, A10, XREAL_1:10;
then
m < len vs
by A20, XXREAL_0:2;
hence
contradiction
by A5, A20, A21, A22;
:: thesis: verum end; hence
p is
oriented Simple Chain of
G
by A1, A19, Th14, GRAPH_4:def 7;
:: thesis: q is oriented Simple Chain of Gconsider h1,
h2 being
FinSequence such that A23:
(
len h1 = len p &
len h2 = (len q) + 1 &
vs = h1 ^ h2 )
by A8, FINSEQ_2:25;
reconsider h2 =
h2 as
FinSequence of the
carrier of
G by A23, FINSEQ_1:50;
now let n be
Element of
NAT ;
:: thesis: ( 1 <= n & n <= len q implies q . n orientedly_joins h2 /. n,h2 /. (n + 1) )assume A24:
( 1
<= n &
n <= len q )
;
:: thesis: q . n orientedly_joins h2 /. n,h2 /. (n + 1)set m =
(len p) + n;
A25:
(len p) + n <= len (p ^ q)
by A7, A24, XREAL_1:9;
n <= (len p) + n
by NAT_1:11;
then A26:
1
<= (len p) + n
by A24, XXREAL_0:2;
then A27:
(p ^ q) . ((len p) + n) orientedly_joins vs /. ((len p) + n),
vs /. (((len p) + n) + 1)
by A5, A25, GRAPH_4:def 5;
A28:
n + 0 <= len h2
by A23, A24, XREAL_1:9;
len (p ^ q) <= len vs
by A6, NAT_1:11;
then
(len p) + n <= len vs
by A25, XXREAL_0:2;
then A29:
(len p) + n in dom vs
by A26, FINSEQ_3:27;
n in dom h2
by A24, A28, FINSEQ_3:27;
then A30:
h2 /. n =
h2 . n
by PARTFUN1:def 8
.=
vs . ((len p) + n)
by A23, A24, A28, Lm2
.=
vs /. ((len p) + n)
by A29, PARTFUN1:def 8
;
A31:
1
<= n + 1
by NAT_1:11;
A32:
1
<= ((len p) + n) + 1
by NAT_1:11;
((len p) + n) + 1
<= len vs
by A6, A25, XREAL_1:9;
then A33:
((len p) + n) + 1
in dom vs
by A32, FINSEQ_3:27;
n + 1
<= len h2
by A23, A24, XREAL_1:9;
then
n + 1
in dom h2
by A31, FINSEQ_3:27;
then h2 /. (n + 1) =
h2 . (n + 1)
by PARTFUN1:def 8
.=
vs . ((len h1) + (n + 1))
by A23, A24, A31, Lm2, XREAL_1:9
.=
vs /. (((len p) + n) + 1)
by A23, A33, PARTFUN1:def 8
;
hence
q . n orientedly_joins h2 /. n,
h2 /. (n + 1)
by A24, A27, A30, Lm2;
:: thesis: verum end; then A34:
h2 is_oriented_vertex_seq_of q
by A23, GRAPH_4:def 5;
now let n,
m be
Element of
NAT ;
:: thesis: ( 1 <= n & n < m & m <= len h2 & h2 . n = h2 . m implies ( n = 1 & m = len h2 ) )assume A35:
( 1
<= n &
n < m &
m <= len h2 &
h2 . n = h2 . m )
;
:: thesis: ( n = 1 & m = len h2 )assume
( not
n = 1 or not
m = len h2 )
;
:: thesis: contradiction
n <= len h2
by A35, XXREAL_0:2;
then A36:
h2 . n = vs . ((len h1) + n)
by A23, A35, Lm2;
1
<= m
by A35, XXREAL_0:2;
then A37:
h2 . m = vs . ((len h1) + m)
by A23, A35, Lm2;
len p <> 0
by A3;
then
0 < len p
;
then A38:
0 + 1
< (len h1) + n
by A23, A35, XREAL_1:10;
A39:
(len h1) + n < (len h1) + m
by A35, XREAL_1:10;
(len h1) + m <= len vs
by A8, A23, A35, XREAL_1:9;
hence
contradiction
by A5, A35, A36, A37, A38, A39;
:: thesis: verum end; hence
q is
oriented Simple Chain of
G
by A1, A34, Th14, GRAPH_4:def 7;
:: thesis: verum end;