let q be FinSequence; :: thesis: for m, n being Element of NAT
for G being Graph
for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = m,n -cut c holds
q is oriented Chain of G
let m, n be Element of NAT ; :: thesis: for G being Graph
for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = m,n -cut c holds
q is oriented Chain of G
let G be Graph; :: thesis: for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = m,n -cut c holds
q is oriented Chain of G
let c be oriented Chain of G; :: thesis: ( 1 <= m & m <= n & n <= len c & q = m,n -cut c implies q is oriented Chain of G )
assume A1:
( 1 <= m & m <= n & n <= len c & q = m,n -cut c )
; :: thesis: q is oriented Chain of G
consider vs being FinSequence of the carrier of G such that
A2:
vs is_oriented_vertex_seq_of c
by Th10;
A3:
((len q) + m) - m = (n + 1) - m
by A1, GRAPH_2:def 1;
reconsider qq = q as Chain of G by A1, GRAPH_2:44;
for n being Element of NAT st 1 <= n & n < len q holds
the Source of G . (q . (n + 1)) = the Target of G . (q . n)
proof
let k be
Element of
NAT ;
:: thesis: ( 1 <= k & k < len q implies the Source of G . (q . (k + 1)) = the Target of G . (q . k) )
assume A4:
( 1
<= k &
k < len q )
;
:: thesis: the Source of G . (q . (k + 1)) = the Target of G . (q . k)
1
- 1
<= m - 1
by A1, XREAL_1:11;
then
m - 1
= m -' 1
by XREAL_0:def 2;
then reconsider m1 =
m - 1 as
Element of
NAT ;
reconsider i =
m1 + k as
Element of
NAT ;
set v1 =
vs /. i;
set v2 =
vs /. (i + 1);
0 + 1
<= k
by A4;
then consider j being
Element of
NAT such that A5:
(
0 <= j &
j < len q &
k = j + 1 )
by A4, GRAPH_2:1;
A6:
i = m + j
by A5;
i + 1
= m + (j + 1)
by A5;
then A7:
(
c . (i + 1) = q . (k + 1) &
c . i = q . k )
by A1, A4, A5, A6, GRAPH_2:def 1;
1
- 1
<= m - 1
by A1, XREAL_1:11;
then A8:
0 + 1
<= (m - 1) + k
by A4, XREAL_1:9;
i <= (m - 1) + (n - (m - 1))
by A3, A4, XREAL_1:8;
then
( 1
<= i &
i <= len c )
by A1, A8, XXREAL_0:2;
then
c . i orientedly_joins vs /. i,
vs /. (i + 1)
by A2, Def5;
then A9:
( the
Source of
G . (c . i) = vs /. i & the
Target of
G . (c . i) = vs /. (i + 1) )
by Def1;
A10:
1
< i + 1
by A8, NAT_1:13;
k + m < n + 1
by A3, A4, XREAL_1:8;
then
k + m <= n
by NAT_1:13;
then
m + k <= len c
by A1, XXREAL_0:2;
then
c . (i + 1) orientedly_joins vs /. (i + 1),
vs /. ((i + 1) + 1)
by A2, A10, Def5;
hence
the
Source of
G . (q . (k + 1)) = the
Target of
G . (q . k)
by A7, A9, Def1;
:: thesis: verum
end;
then
qq is oriented
by GRAPH_1:def 13;
hence
q is oriented Chain of G
; :: thesis: verum