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