let G be Graph; :: thesis: for v1, v2 being Element of the carrier of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds
( AcyclicPaths p <> {} & AcyclicPaths v1,v2 <> {} )
let v1, v2 be Element of the carrier of G; :: thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds
( AcyclicPaths p <> {} & AcyclicPaths v1,v2 <> {} )
let p be oriented Chain of G; :: thesis: ( p is_orientedpath_of v1,v2 implies ( AcyclicPaths p <> {} & AcyclicPaths v1,v2 <> {} ) )
assume A1:
p is_orientedpath_of v1,v2
; :: thesis: ( AcyclicPaths p <> {} & AcyclicPaths v1,v2 <> {} )
defpred S1[ Element of NAT ] means for p being oriented Chain of G
for v1, v2 being Element of the carrier of G st $1 + 1 = len p & p is_orientedpath_of v1,v2 holds
AcyclicPaths p <> {} ;
set FS = the Source of G;
set FT = the Target of G;
A2:
S1[ 0 ]
A4:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
:: thesis: S1[k + 1]
now let p be
oriented Chain of
G;
:: thesis: for v1, v2 being Element of the carrier of G st (k + 1) + 1 = len p & p is_orientedpath_of v1,v2 holds
AcyclicPaths b3 <> {} let v1,
v2 be
Element of the
carrier of
G;
:: thesis: ( (k + 1) + 1 = len p & p is_orientedpath_of v1,v2 implies AcyclicPaths b1 <> {} )assume A6:
(
(k + 1) + 1
= len p &
p is_orientedpath_of v1,
v2 )
;
:: thesis: AcyclicPaths b1 <> {} then consider p1,
p2 being
FinSequence such that A7:
(
len p1 = k + 1 &
len p2 = 1 &
p = p1 ^ p2 )
by FINSEQ_2:25;
reconsider p1 =
p1 as
oriented Chain of
G by A7, Th14;
A8:
1
<= len p1
by A7, NAT_1:11;
then A9:
( 1
in dom p1 &
len p1 in dom p1 )
by FINSEQ_3:27;
then reconsider x = the
Source of
G . (p1 . 1) as
Element of the
carrier of
G by FINSEQ_2:13, FUNCT_2:7;
A10:
p1 . 1
= p . 1
by A7, A8, Lm1;
reconsider y = the
Target of
G . (p1 . (len p1)) as
Element of the
carrier of
G by A9, FINSEQ_2:13, FUNCT_2:7;
p1 <> {}
by A7;
then
p1 is_orientedpath_of x,
y
by Def3;
then
AcyclicPaths p1 <> {}
by A5, A7;
then consider r being
set such that A11:
r in AcyclicPaths p1
by XBOOLE_0:def 1;
consider q being
oriented Simple Chain of
G such that A12:
(
r = q &
q <> {} & the
Source of
G . (q . 1) = x & the
Target of
G . (q . (len q)) = y &
rng q c= rng p1 )
by A11;
A13:
1
in dom p2
by A7, FINSEQ_3:27;
then A14:
p . ((len p1) + 1) = p2 . 1
by A7, FINSEQ_1:def 7;
len p1 < len p
by A6, A7, NAT_1:13;
then A15: the
Source of
G . (p . ((len p1) + 1)) =
the
Target of
G . (p . (len p1))
by A8, GRAPH_1:def 13
.=
the
Target of
G . (q . (len q))
by A7, A8, A12, Lm1
;
A16:
rng p1 c= rng p
by A7, FINSEQ_1:42;
A17:
rng p2 c= rng p
by A7, FINSEQ_1:43;
A18:
the
Source of
G . (p2 . 1) = the
Target of
G . (q . (len q))
by A7, A13, A15, FINSEQ_1:def 7;
per cases
( ex k being Element of NAT st
( 1 <= k & k <= len q & the Target of G . (q . k) = the Target of G . (p2 . 1) ) or for k being Element of NAT holds
( not 1 <= k or not k <= len q or not the Target of G . (q . k) = the Target of G . (p2 . 1) ) )
;
suppose
ex
k being
Element of
NAT st
( 1
<= k &
k <= len q & the
Target of
G . (q . k) = the
Target of
G . (p2 . 1) )
;
:: thesis: AcyclicPaths b1 <> {} then consider k being
Element of
NAT such that A19:
( 1
<= k &
k <= len q & the
Target of
G . (q . k) = the
Target of
G . (p2 . 1) )
;
consider i being
Nat such that A20:
len q = k + i
by A19, NAT_1:10;
consider q1,
q2 being
FinSequence such that A21:
(
len q1 = k &
len q2 = i &
q = q1 ^ q2 )
by A20, FINSEQ_2:25;
reconsider q1 =
q1 as
oriented Simple Chain of
G by A21, Th17;
rng q1 c= rng q
by A21, FINSEQ_1:42;
then A22:
rng q1 c= rng p1
by A12, XBOOLE_1:1;
A23:
q1 <> {}
by A19, A21;
A24:
rng q1 c= rng p
by A16, A22, XBOOLE_1:1;
A25:
the
Source of
G . (q1 . 1) = the
Source of
G . (p . 1)
by A10, A12, A19, A21, Lm1;
the
Target of
G . (q1 . (len q1)) = the
Target of
G . (p . (len p))
by A6, A7, A14, A19, A21, Lm1;
then
q1 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 A23, A24, A25;
hence
AcyclicPaths p <> {}
;
:: thesis: verum end; suppose A26:
for
k being
Element of
NAT holds
( not 1
<= k or not
k <= len q or not the
Target of
G . (q . k) = the
Target of
G . (p2 . 1) )
;
:: thesis: AcyclicPaths b1 <> {} reconsider p2 =
p2 as
oriented Chain of
G by A7, Th14;
hereby :: thesis: verum
per cases
( the Source of G . (q . 1) <> the Target of G . (q . (len q)) or the Source of G . (q . 1) = the Target of G . (q . (len q)) )
;
suppose A27:
the
Source of
G . (q . 1) <> the
Target of
G . (q . (len q))
;
:: thesis: AcyclicPaths p <> {} set qp =
q ^ p2;
A28:
len q >= 1
by A12, FINSEQ_1:28;
then A29:
q ^ p2 is
oriented Simple Chain of
G
by A7, A14, A15, A26, A27, Th19;
A30:
len (q ^ p2) = (len q) + 1
by A7, FINSEQ_1:35;
then A31:
q ^ p2 <> {}
;
A32:
the
Source of
G . ((q ^ p2) . 1) = the
Source of
G . (p . 1)
by A10, A12, A28, Lm1;
A33:
the
Target of
G . ((q ^ p2) . (len (q ^ p2))) = the
Target of
G . (p . (len p))
by A6, A7, A14, A30, Lm2;
A34:
rng (q ^ p2) = (rng q) \/ (rng p2)
by FINSEQ_1:44;
rng q c= rng p
by A12, A16, XBOOLE_1:1;
then
rng (q ^ p2) c= (rng p) \/ (rng p)
by A17, A34, XBOOLE_1:13;
then
q ^ p2 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 A29, A31, A32, A33;
hence
AcyclicPaths p <> {}
;
:: thesis: verum end; end; end;
hence
S1[
k + 1]
;
:: thesis: verum
end;
A37:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A2, A4);
p <> {}
by A1, Def3;
then
len p >= 1
by FINSEQ_1:28;
then
((len p) -' 1) + 1 = len p
by XREAL_1:237;
hence
AcyclicPaths p <> {}
by A1, A37; :: thesis: AcyclicPaths v1,v2 <> {}
then consider x being set such that
A38:
x in AcyclicPaths p
by XBOOLE_0:def 1;
AcyclicPaths p c= AcyclicPaths v1,v2
by A1, Th44;
hence
AcyclicPaths v1,v2 <> {}
by A38; :: thesis: verum