let V be set ; for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds
( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} )
let G be Graph; for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds
( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} )
let v1, v2 be Element of G; for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds
( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} )
let p be oriented Chain of G; ( p is_orientedpath_of v1,v2,V implies ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} ) )
defpred S1[ Nat] means for p being oriented Chain of G
for v1, v2 being Element of G st len p <= $1 + 1 & p is_orientedpath_of v1,v2,V holds
AcyclicPaths p <> {} ;
set FS = the Source of G;
set FT = the Target of G;
assume A1:
p is_orientedpath_of v1,v2,V
; ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} )
then
p is_orientedpath_of v1,v2
;
then
p <> {}
;
then
len p >= 1
by FINSEQ_1:20;
then A2:
((len p) -' 1) + 1 = len p
by XREAL_1:235;
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
now for p being oriented Chain of G
for v1, v2 being Element of G st len p <= (k + 1) + 1 & p is_orientedpath_of v1,v2,V holds
AcyclicPaths p <> {} let p be
oriented Chain of
G;
for v1, v2 being Element of G st len p <= (k + 1) + 1 & p is_orientedpath_of v1,v2,V holds
AcyclicPaths b3 <> {} let v1,
v2 be
Element of
G;
( len p <= (k + 1) + 1 & p is_orientedpath_of v1,v2,V implies AcyclicPaths b1 <> {} )assume that A5:
len p <= (k + 1) + 1
and A6:
p is_orientedpath_of v1,
v2,
V
;
AcyclicPaths b1 <> {} consider vs being
FinSequence of the
carrier of
G such that A7:
vs is_oriented_vertex_seq_of p
by GRAPH_4:9;
A8:
(vertices p) \ {v2} c= V
by A6;
A9:
len vs = (len p) + 1
by A7, GRAPH_4:def 5;
then A10:
len vs >= 1
by NAT_1:12;
A11:
p is_orientedpath_of v1,
v2
by A6;
then A12:
p <> {}
;
then A13:
len p >= 1
by FINSEQ_1:20;
then
p . (len p) orientedly_joins vs /. (len p),
vs /. ((len p) + 1)
by A7, GRAPH_4:def 5;
then
the
Target of
G . (p . (len p)) = vs /. ((len p) + 1)
by GRAPH_4:def 1;
then A14:
the
Target of
G . (p . (len p)) = vs . (len vs)
by A9, A10, FINSEQ_4:15;
per cases
( for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) or ex n, m being Nat st
( 1 <= n & n < m & m <= len vs & vs . n = vs . m & not ( n = 1 & m = len vs ) ) )
;
suppose
ex
n,
m being
Nat st
( 1
<= n &
n < m &
m <= len vs &
vs . n = vs . m & not (
n = 1 &
m = len vs ) )
;
AcyclicPaths b1 <> {} then consider n,
m being
Nat such that A15:
1
<= n
and A16:
n < m
and A17:
m <= len vs
and A18:
vs . n = vs . m
and A19:
( not
n = 1 or not
m = len vs )
;
consider i being
Nat such that A20:
m = 1
+ i
by A15, A16, NAT_1:10, XXREAL_0:2;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
A21:
m >= 1
by A15, A16, XXREAL_0:2;
hereby verum
per cases
( n = 1 or n <> 1 )
;
suppose A22:
n = 1
;
AcyclicPaths p <> {} then
m < len vs
by A17, A19, XXREAL_0:1;
then A23:
m <= len p
by A9, NAT_1:13;
then consider j being
Nat such that A24:
len p = m + j
by NAT_1:10;
A25:
p . 1
orientedly_joins vs /. 1,
vs /. (1 + 1)
by A7, A13, GRAPH_4:def 5;
A26:
n <= len vs
by A16, A17, XXREAL_0:2;
p . m orientedly_joins vs /. m,
vs /. (m + 1)
by A7, A16, A22, A23, GRAPH_4:def 5;
then A27: the
Source of
G . (p . m) =
vs /. m
by GRAPH_4:def 1
.=
vs . m
by A16, A17, A22, FINSEQ_4:15
.=
vs /. n
by A15, A18, A26, FINSEQ_4:15
.=
the
Source of
G . (p . 1)
by A22, A25, GRAPH_4:def 1
.=
v1
by A11
;
reconsider j =
j as
Element of
NAT by ORDINAL1:def 12;
A28:
len p = i + (1 + j)
by A20, A24;
then consider p1,
p2 being
FinSequence such that A29:
len p1 = i
and A30:
len p2 = 1
+ j
and A31:
p = p1 ^ p2
by FINSEQ_2:22;
A32:
1
<= len p2
by A30, NAT_1:11;
then A33:
p2 . 1
= p . m
by A20, A29, A31, Lm2;
p2 . (len p2) = p . (len p)
by A28, A29, A30, A31, A32, Lm2;
then A34:
the
Target of
G . (p2 . (len p2)) = v2
by A11;
reconsider p1 =
p1,
p2 =
p2 as
oriented Chain of
G by A31, Th9;
(i + 1) + (- 1) > 1
+ (- 1)
by A16, A20, A22, XREAL_1:8;
then
len p2 < len p
by A28, A30, XREAL_1:29;
then
len p2 < (k + 1) + 1
by A5, XXREAL_0:2;
then A35:
len p2 <= k + 1
by NAT_1:13;
(vertices (p1 ^ p2)) \ {v2} c= V
by A6, A31;
then A36:
(vertices p2) \ {v2} c= V
by Th21;
p2 <> {}
by A30;
then
p2 is_orientedpath_of v1,
v2
by A27, A33, A34;
then
p2 is_orientedpath_of v1,
v2,
V
by A36;
then
AcyclicPaths p2 <> {}
by A4, A35;
then consider r being
object such that A37:
r in AcyclicPaths p2
by XBOOLE_0:def 1;
consider q being
oriented Simple Chain of
G such that
r = q
and A38:
q <> {}
and A39:
( the
Source of
G . (q . 1) = v1 & the
Target of
G . (q . (len q)) = v2 )
and A40:
rng q c= rng p2
by A27, A33, A34, A37;
rng p2 c= rng p
by A31, FINSEQ_1:30;
then A41:
rng q c= rng p
by A40;
( the
Source of
G . (q . 1) = the
Source of
G . (p . 1) & the
Target of
G . (q . (len q)) = the
Target of
G . (p . (len p)) )
by A11, A39;
then
q in { w where w is oriented Simple Chain of G : ( w <> {} & the Source of G . (w . 1) = the Source of G . (p . 1) & the Target of G . (w . (len w)) = the Target of G . (p . (len p)) & rng w c= rng p ) }
by A38, A41;
hence
AcyclicPaths p <> {}
;
verum end; suppose A42:
n <> 1
;
AcyclicPaths p <> {} consider n1 being
Nat such that A43:
n = 1
+ n1
by A15, NAT_1:10;
reconsider n1 =
n1 as
Element of
NAT by ORDINAL1:def 12;
A44:
n < len vs
by A16, A17, XXREAL_0:2;
then A45:
n1 < len p
by A9, A43, XREAL_1:7;
then consider j being
Nat such that A46:
len p = n1 + j
by NAT_1:10;
reconsider j =
j as
Element of
NAT by ORDINAL1:def 12;
consider p1,
p2 being
FinSequence such that A47:
len p1 = n1
and
len p2 = j
and A48:
p = p1 ^ p2
by A46, FINSEQ_2:22;
A49:
n > 1
by A15, A42, XXREAL_0:1;
then A50:
n1 >= 1
by A43, NAT_1:13;
then A51:
p1 . (len p1) = p . n1
by A47, A48, Lm1;
p1 . 1
= p . 1
by A47, A48, A50, Lm1;
then A52:
the
Source of
G . (p1 . 1) = v1
by A11;
A53:
rng p1 c= rng p
by A48, FINSEQ_1:29;
reconsider p1 =
p1,
p2 =
p2 as
oriented Chain of
G by A48, Th9;
p . n1 orientedly_joins vs /. n1,
vs /. (n1 + 1)
by A7, A45, A50, GRAPH_4:def 5;
then A54: the
Target of
G . (p . n1) =
vs /. n
by A43, GRAPH_4:def 1
.=
vs . n
by A15, A44, FINSEQ_4:15
;
hereby verum
per cases
( m = len vs or m <> len vs )
;
suppose
m = len vs
;
AcyclicPaths p <> {} then A55:
the
Target of
G . (p1 . (len p1)) = v2
by A11, A14, A18, A54, A51;
(vertices (p1 ^ p2)) \ {v2} c= V
by A6, A48;
then A56:
(vertices p1) \ {v2} c= V
by Th21;
n1 < (k + 1) + 1
by A5, A45, XXREAL_0:2;
then A57:
len p1 <= k + 1
by A47, NAT_1:13;
p1 <> {}
by A49, A43, A47;
then
p1 is_orientedpath_of v1,
v2
by A52, A55;
then
p1 is_orientedpath_of v1,
v2,
V
by A56;
then
AcyclicPaths p1 <> {}
by A4, A57;
then consider r being
object such that A58:
r in AcyclicPaths p1
by XBOOLE_0:def 1;
consider q being
oriented Simple Chain of
G such that
r = q
and A59:
q <> {}
and A60:
the
Source of
G . (q . 1) = v1
and A61:
the
Target of
G . (q . (len q)) = v2
and A62:
rng q c= rng p1
by A52, A55, A58;
A63:
the
Target of
G . (q . (len q)) = the
Target of
G . (p . (len p))
by A11, A61;
(
rng q c= rng p & the
Source of
G . (q . 1) = the
Source of
G . (p . 1) )
by A11, A53, A60, A62;
then
q in { w where w is oriented Simple Chain of G : ( w <> {} & the Source of G . (w . 1) = the Source of G . (p . 1) & the Target of G . (w . (len w)) = the Target of G . (p . (len p)) & rng w c= rng p ) }
by A59, A63;
hence
AcyclicPaths p <> {}
;
verum end; suppose
m <> len vs
;
AcyclicPaths p <> {} then
m < len vs
by A17, XXREAL_0:1;
then A64:
m <= len p
by A9, NAT_1:13;
then consider h being
Nat such that A65:
len p = m + h
by NAT_1:10;
p . m orientedly_joins vs /. m,
vs /. (m + 1)
by A7, A21, A64, GRAPH_4:def 5;
then A66: the
Source of
G . (p . m) =
vs /. m
by GRAPH_4:def 1
.=
the
Target of
G . (p1 . (len p1))
by A17, A18, A21, A54, A51, FINSEQ_4:15
;
reconsider h =
h as
Element of
NAT by ORDINAL1:def 12;
A67:
len p = i + (1 + h)
by A20, A65;
then consider q1,
q2 being
FinSequence such that A68:
len q1 = i
and A69:
len q2 = 1
+ h
and A70:
p = q1 ^ q2
by FINSEQ_2:22;
reconsider q2 =
q2 as
oriented Chain of
G by A70, Th9;
A71:
1
<= len q2
by A69, NAT_1:12;
then
q2 . 1
= p . m
by A20, A68, A70, Lm2;
then reconsider pq =
p1 ^ q2 as
oriented Chain of
G by A66, Th10;
pq . (len pq) =
pq . ((len p1) + (len q2))
by FINSEQ_1:22
.=
q2 . (len q2)
by A71, Lm2
.=
p . (len p)
by A67, A68, A69, A70, A71, Lm2
;
then A72:
the
Target of
G . (pq . (len pq)) = v2
by A11;
A73:
rng pq = (rng p1) \/ (rng q2)
by FINSEQ_1:31;
rng q2 c= rng p
by A70, FINSEQ_1:30;
then A74:
rng pq c= rng p
by A53, A73, XBOOLE_1:8;
then A75:
(vertices pq) \ {v2} c= V
by A8, Th20;
A76:
len pq = n1 + (1 + h)
by A47, A69, FINSEQ_1:22;
m + h > n + h
by A16, XREAL_1:8;
then
len pq < (k + 1) + 1
by A5, A43, A65, A76, XXREAL_0:2;
then A77:
len pq <= k + 1
by NAT_1:13;
A78:
the
Source of
G . (pq . 1) = v1
by A47, A50, A52, Lm1;
pq <> {}
by A76;
then
pq is_orientedpath_of v1,
v2
by A78, A72;
then
pq is_orientedpath_of v1,
v2,
V
by A75;
then
AcyclicPaths pq <> {}
by A4, A77;
then consider r being
object such that A79:
r in AcyclicPaths pq
by XBOOLE_0:def 1;
consider q being
oriented Simple Chain of
G such that
r = q
and A80:
q <> {}
and A81:
( the
Source of
G . (q . 1) = v1 & the
Target of
G . (q . (len q)) = v2 )
and A82:
rng q c= rng pq
by A78, A72, A79;
A83:
rng q c= rng p
by A74, A82;
( the
Source of
G . (q . 1) = the
Source of
G . (p . 1) & the
Target of
G . (q . (len q)) = the
Target of
G . (p . (len p)) )
by A11, A81;
then
q in { w where w is oriented Simple Chain of G : ( w <> {} & the Source of G . (w . 1) = the Source of G . (p . 1) & the Target of G . (w . (len w)) = the Target of G . (p . (len p)) & rng w c= rng p ) }
by A80, A83;
hence
AcyclicPaths p <> {}
;
verum end; end; end; end;
hence
S1[
k + 1]
;
verum
end;
A84:
S1[ 0 ]
proof
let p be
oriented Chain of
G;
for v1, v2 being Element of G st len p <= 0 + 1 & p is_orientedpath_of v1,v2,V holds
AcyclicPaths p <> {} let v1,
v2 be
Element of
G;
( len p <= 0 + 1 & p is_orientedpath_of v1,v2,V implies AcyclicPaths p <> {} )
assume that A85:
len p <= 0 + 1
and A86:
p is_orientedpath_of v1,
v2,
V
;
AcyclicPaths p <> {}
p is_orientedpath_of v1,
v2
by A86;
then A87:
p <> {}
;
then
len p >= 1
by FINSEQ_1:20;
then reconsider r =
p as
oriented Simple Chain of
G by A85, Th13, XXREAL_0:1;
r in { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) }
by A87;
hence
AcyclicPaths p <> {}
;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A84, A3);
hence
AcyclicPaths p <> {}
by A1, A2; AcyclicPaths (v1,v2,V) <> {}
then A88:
ex x being object st x in AcyclicPaths p
by XBOOLE_0:def 1;
AcyclicPaths p c= AcyclicPaths (v1,v2,V)
by A1, Th39;
hence
AcyclicPaths (v1,v2,V) <> {}
by A88; verum