Copyright (c) 2003 Association of Mizar Users
environ
vocabulary FUNCT_1, BOOLE, RELAT_1, FINSET_1, ORDERS_1, FINSEQ_1, CARD_1,
GRAPH_1, GRAPH_5, RLVECT_1, GRAPH_4, FINSEQ_4, FINSEQ_2, PROB_1, ARYTM_1,
MSAFREE2;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, RELAT_1, FUNCT_1,
FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, FINSET_1, REAL_1, NAT_1, GRAPH_1,
BINARITH, FUNCT_2, GRAPH_4, PROB_1, RVSUM_1, GOBOARD1, GRAPH_3;
constructors REAL_1, BINARITH, FINSEQ_4, GRAPH_4, PROB_1, GOBOARD1, SEQ_2,
MEMBERED;
clusters FINSEQ_1, GRAPH_1, GRAPH_2, RELSET_1, SUBSET_1, GRAPH_4, FINSET_1,
PRELAMB, NAT_1, XREAL_0, MEMBERED;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
definitions TARSKI, FUNCT_1;
theorems FUNCT_2, XBOOLE_1, GRAPH_1, FINSEQ_1, GRAPH_4, FUNCT_1, FINSEQ_3,
REAL_1, AXIOMS, FINSEQ_4, NAT_1, CARD_1, TARSKI, YELLOW15, CARD_4,
CARD_5, FINSEQ_2, FINSET_1, XBOOLE_0, CARD_2, RVSUM_1, AMISTD_2,
SUBSET_1, AMI_5, ZFMISC_1, SCMFSA_7, XCMPLX_1;
schemes FUNCT_1, NAT_1;
begin :: Preliminaries
reserve n,m,i,j,k for Nat,
x,y,e,y1,y2,X,V,U for set,
W,f,g for Function;
theorem Th1:
for f being finite Function holds card rng f <= card dom f
proof
let f be finite Function;
reconsider X=rng f, Y=dom f as set;
Card X <=` Card Y by CARD_1:28;
hence thesis by CARD_2:57;
end;
theorem Th2:
rng f c= rng g & x in dom f implies ex y st y in dom g & f.x = g.y
proof
assume A1: rng f c= rng g & x in dom f;
then f.x in rng f by FUNCT_1:12;
hence thesis by A1,FUNCT_1:def 5;
end;
scheme LambdaAB { A, B()->set, F(Element of B())->set } :
ex f being Function st dom f = A() & for x being Element of B() st
x in A() holds f.x = F(x)
proof
defpred P[set,set] means ($1 is Element of B() implies ex
x being Element of B() st x=$1 & $2=F(x))
& (not $1 is Element of B() implies $2=0);
A1: for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1 = y2;
A2: for x st x in A() ex y st P[x,y]
proof
let x;
assume x in A();
per cases;
suppose x is Element of B();
then reconsider z=x as Element of B();
take y=F(z);
thus P[x,y];
suppose A3: not x is Element of B();
take y=0;
thus P[x,y] by A3;
end;
ex f st dom f = A() & for x st x in A() holds P[x,f.x]
from FuncEx(A1,A2);
then consider f such that
A4: dom f = A() & for x st x in A() holds P[x,f.x];
take f;
now let x be Element of B();
assume x in A();
then P[x,f.x] by A4;
hence f.x=F(x);
end;
hence thesis by A4;
end;
theorem Th3:
for D being finite set, n being Nat, X being set st
X = {x where x is Element of D* : 1 <= len x & len x <= n } holds
X is finite
proof
let D be finite set,n be Nat, X be set;
assume A1: X = {x where x is Element of D* : 1 <= len x & len x <= n };
deffunc F(Nat) = $1-tuples_on D;
consider f being Function such that
A2: dom f = Seg n & for x being Nat st x in Seg n
holds f.x = F(x) from LambdaAB;
now let x;
assume A3:x in dom f;
then reconsider z=x as Nat by A2;
f.z = F(z) by A2,A3;
hence f.x is finite by YELLOW15:2;
end;
then A4: Union f is finite by A2,CARD_4:63;
X c= Union f
proof let x;
assume x in X;
then consider y being Element of D* such that
A5: x=y & 1 <= len y & len y <= n by A1;
consider m such that
A6: dom y = Seg m by FINSEQ_1:def 2;
A7: len y = m by A6,FINSEQ_1:def 3;
then A8: m in dom f by A2,A5,FINSEQ_1:3;
y in { s where s is Element of D*: len s = m } by A7;
then y in m-tuples_on D by FINSEQ_2:def 4;
then y in f.m by A2,A8;
hence x in Union f by A5,A8,CARD_5:10;
end;
hence thesis by A4,FINSET_1:13;
end;
theorem Th4:
for D being finite set, n being Nat, X being set
st X = {x where x is Element of D* : len x <= n } holds X is finite
proof
let D be finite set,n be Nat, X be set;
assume A1: X = {x where x is Element of D* : len x <= n };
set B = {x where x is Element of D* : 1 <= len x & len x <= n };
A2: X c= { {} } \/ B
proof
let y; assume y in X;
then consider x being Element of D* such that
A3: y=x & len x <= n by A1;
per cases;
suppose len x < 0+1;
then len x <= 0 by NAT_1:38;
then len x = 0 by NAT_1:18;
then x = {} by FINSEQ_1:25;
then x in { {} } by TARSKI:def 1;
hence y in { {} } \/ B by A3,XBOOLE_0:def 2;
suppose len x >= 0+1;
then x in B by A3;
hence y in { {} } \/ B by A3,XBOOLE_0:def 2;
end;
B is finite by Th3;
then { {} } \/ B is finite by FINSET_1:14;
hence thesis by A2,FINSET_1:13;
end;
theorem Th5:
for D being finite set holds card D <> 0 iff D <> {}
proof
let D be finite set;
thus card D <> 0 implies D <> {} by CARD_1:78;
assume D <> {};
then consider x being set such that
A1: x in D by XBOOLE_0:def 1;
set C = D \ {x};
{x} c= D by A1,ZFMISC_1:37;
then A2: D=C \/ {x} by XBOOLE_1:45;
x in {x} by TARSKI:def 1;
then not x in C by XBOOLE_0:def 4;
then card D = card C + 1 by A2,CARD_2:54;
hence card D <> 0;
end;
theorem Th6:
for D being finite set, k being Nat st card D = k+1 holds
ex x being Element of D,C being Subset of D st D = C \/ { x } & card C = k
proof
let D be finite set,k be Nat;
assume A1: card D = k+1;
then D <> {} by Th5;
then consider x being set such that
A2: x in D by XBOOLE_0:def 1;
reconsider C=D \ { x } as Subset of D by XBOOLE_1:36;
reconsider x as Element of D by A2;
take x,C;
A3: x in {x} by TARSKI:def 1;
{x} c= D by A2,ZFMISC_1:37; hence
A4: D=C \/ {x} by XBOOLE_1:45;
not x in C by A3,XBOOLE_0:def 4;
then card D = card C + 1 by A4,CARD_2:54;
hence thesis by A1,XCMPLX_1:2;
end;
theorem Th7:
for D being finite set st card D = 1 holds ex x being Element of D st D={x}
proof
let D be finite set;
assume card D = 1;
then card D = 0+1;
then consider x being Element of D,C being Subset of D such that
A1: D = C \/ { x } & card C = 0 by Th6;
take x;
C = {} by A1,Th5;
hence D = {x} by A1;
end;
scheme MinValue { D() -> non empty finite set, F(Element of D())-> Real}:
ex x being Element of D() st for y being Element of D() holds F(x) <= F(y)
proof
defpred P[Nat] means for A being Subset of D() st $1+1 = card A
holds ex x being Element of D() st x in A &
for y being Element of D() st y in A holds F(x) <= F(y);
A1: P[0]
proof
let A be Subset of D();
assume 0+1 = card A;
then consider x being Element of A such that
A2: A = {x} by Th7;
reconsider x as Element of D() by A2,ZFMISC_1:37;
take x;
thus x in A by A2;
thus for y be Element of D() st y in A holds
F(x) <= F(y) by A2,TARSKI:def 1;
end;
A3: for k st P[k] holds P[k+1]
proof
let k;
assume A4: P[k];
now
let A be Subset of D();
assume A5: k+1+1 = card A;
then consider x being Element of A,C being Subset of A such that
A6: A = C \/ { x } & card C = k+1 by Th6;
A7: A <> {} by A5,Th5;
then x in A;
then reconsider x as Element of D();
reconsider C as Subset of D() by XBOOLE_1:1;
consider z being Element of D() such that
A8: z in C & for y being Element of D()
st y in C holds F(z) <= F(y) by A4,A6;
per cases;
suppose A9: F(x) <= F(z);
take x;
thus x in A by A7;
hereby let y be Element of D();
assume A10: y in A;
per cases by A6,A10,XBOOLE_0:def 2;
suppose y in C;
then F(z) <= F(y) by A8;
hence F(x) <= F(y) by A9,AXIOMS:22;
suppose y in {x};
hence F(x) <= F(y) by TARSKI:def 1;
end;
suppose A11: F(x) > F(z);
take z;
thus z in A by A8;
hereby let y be Element of D();
assume A12: y in A;
per cases by A6,A12,XBOOLE_0:def 2;
suppose y in C;
hence F(z) <= F(y) by A8;
suppose y in {x};
hence F(z) <= F(y) by A11,TARSKI:def 1;
end;
end;
hence P[k+1];
end;
A13: for k holds P[k] from Ind(A1,A3);
A14: card D() -' 1 + 1= card D() -1 +1 by AMISTD_2:4
.=card D()+ 1 -1 by XCMPLX_1:29
.=card D() by XCMPLX_1:26;
D() c= D();
then consider x being Element of D() such that
A15: x in D() & for y being Element of D() st y in D() holds F(x) <= F(y)
by A13,A14;
take x;
let y be Element of D();
thus F(x) <= F(y) by A15;
end;
definition let D be set, X be non empty Subset of D*;
redefine mode Element of X -> FinSequence of D;
coherence
proof
let x be Element of X;
reconsider y=x as Element of D*;
y is FinSequence of D;
hence x is FinSequence of D;
end;
end;
begin :: Additional Properties of Finite Sequences
reserve p,q for FinSequence;
theorem Th8:
p <> {} iff len p >= 1
proof
hereby
assume p <> {};
then len p <> 0 by FINSEQ_1:25;
then len p > 0 by NAT_1:19;
then len p+1 > 0+1 by REAL_1:67;
hence len p >=1 by NAT_1:38;
end;
assume len p >= 1;
then len p > 0 by AXIOMS:22;
hence p <> {} by FINSEQ_1:25;
end;
Lm1:
1 <= n & n <= len p implies p.n = (p^q).n
proof
assume 1 <= n & n <= len p;
then n in dom p by FINSEQ_3:27;
hence p.n = (p^q).n by FINSEQ_1:def 7;
end;
Lm2:
1 <= n & n <= len q implies q.n = (p^q).(len p+n)
proof
assume 1 <= n & n <= len q;
then n in dom q by FINSEQ_3:27;
hence q.n = (p^q).(len p+n) by FINSEQ_1:def 7;
end;
theorem Th9:
(for n,m st 1<=n & n<m & m<=len p holds p.n <> p.m) iff p is one-to-one
proof
hereby
assume A1:for n,m st 1<=n & n<m & m<=len p holds p.n <> p.m;
thus p is one-to-one
proof
let x1,x2 be set;
assume A2: x1 in dom p & x2 in dom p & p.x1 = p.x2;
assume A3: x1 <> x2;
reconsider n=x1, m=x2 as Nat by A2;
A4: 1 <= n & n <= len p by A2,FINSEQ_3:27;
A5: 1 <= m & m <= len p by A2,FINSEQ_3:27;
per cases;
suppose m <= n;
then m < n by A3,REAL_1:def 5;
hence contradiction by A1,A2,A4,A5;
suppose m > n;
hence contradiction by A1,A2,A4,A5;
end;
end;
assume A6: p is one-to-one;
let n,m;
assume A7: 1<=n & n<m & m<=len p;
assume A8: p.n = p.m;
n <= len p by A7,AXIOMS:22;
then A9: n in dom p by A7,FINSEQ_3:27;
1 <= m by A7,AXIOMS:22;
then m in dom p by A7,FINSEQ_3:27;
hence contradiction by A6,A7,A8,A9,FUNCT_1:def 8;
end;
theorem Th10:
(for n,m st 1<=n & n<m & m<=len p holds p.n <> p.m) iff card rng p = len p
proof
p is one-to-one iff card rng p=len p by FINSEQ_4:77;
hence thesis by Th9;
end;
reserve G for Graph,
pe,qe for FinSequence of the Edges of G;
theorem Th11:
i in dom pe implies (the Source of G).(pe.i) in the Vertices of G
& (the Target of G).(pe.i) in the Vertices of G
proof
assume i in dom pe;
then pe.i in the Edges of G by FINSEQ_2:13;
hence thesis by FUNCT_2:7;
end;
theorem Th12:
q^<*x*> is one-to-one & rng (q^<*x*>) c= rng p implies
ex p1,p2 being FinSequence st p=p1^<*x*>^p2 & rng q c= rng (p1^p2)
proof
set r=q^<*x*>,
i=len q +1;
assume A1: r is one-to-one & rng r c= rng p;
A2: len r =i by FINSEQ_2:19;
1 <= i by NAT_1:29;
then A3: i in dom r by A2,FINSEQ_3:27;
then consider y being set such that
A4: y in dom p & r.i = p.y by A1,Th2;
reconsider j=y as Nat by A4;
j <= len p by A4,FINSEQ_3:27;
then consider k being Nat such that
A5: len p = j+k by NAT_1:28;
consider s, p2 being FinSequence such that
A6: len s = j & len p2 = k & p = s^p2 by A5,FINSEQ_2:25;
A7: 1 <= j by A4,FINSEQ_3:27;
then consider m such that
A8: j = 1 + m by NAT_1:28;
consider p1 being FinSequence, d being set such that
A9: s = p1^<*d*> by A6,A8,FINSEQ_2:21;
A10: j = len p1 +1 by A6,A9,FINSEQ_2:19;
A11: r.i=x by FINSEQ_1:59;
j in dom s by A6,A7,FINSEQ_3:27;
then A12: s.j=x by A4,A6,A11,FINSEQ_1:def 7;
then A13: s = p1^<*x*> by A9,A10,FINSEQ_1:59;
take p1,p2;
thus
p=p1^<*x*>^p2 by A6,A9,A10,A12,FINSEQ_1:59;
A14: now let y be set;
assume A15: y in rng q;
assume y = x;
then consider z being set such that
A16: z in dom q & x = q.z by A15,FUNCT_1:def 5;
reconsider n=z as Nat by A16;
n <= len q by A16,FINSEQ_3:27;
then A17: n <> i by REAL_1:69;
A18: n in dom r by A16,FINSEQ_2:18;
r.n=r.i by A11,A16,FINSEQ_1:def 7;
hence contradiction by A1,A3,A17,A18,FUNCT_1:def 8;
end;
let y be set;
assume A19: y in rng q;
rng q c= rng r by FINSEQ_1:42;
then A20: rng q c= rng p by A1,XBOOLE_1:1;
rng p = rng (p1^<*x*>) \/ rng p2 by A6,A13,FINSEQ_1:44
.= rng p1 \/ rng <*x*> \/ rng p2 by FINSEQ_1:44
.= rng p1 \/ rng p2 \/ rng <*x*> by XBOOLE_1:4
.= rng (p1^p2) \/ rng <*x*> by FINSEQ_1:44
.= rng (p1^p2) \/ {x} by FINSEQ_1:55;
then A21: y in rng (p1^p2) or y in {x} by A19,A20,XBOOLE_0:def 2;
y <> x by A14,A19;
hence y in rng (p1^p2) by A21,TARSKI:def 1;
end;
begin :: Additional Properties of Chains and Oriented Paths
theorem Th13:
p^q is Chain of G implies p is Chain of G & q is Chain of G
proof
assume A1: p^q is Chain of G;
set r=p^q,
D=the Edges of G,
V=the Vertices of G;
consider f being FinSequence such that
A2: len f = len r + 1 &
(for n st 1 <= n & n <= len f holds f.n in V) &
for n st 1 <= n & n <= len r
ex x, y being Element of V st
x = f.n & y = f.(n+1) & r.n joins x, y by A1,GRAPH_1:def 11;
A3: p is FinSequence of D & q is FinSequence of D by A1,FINSEQ_1:50;
A4: now let n;
assume 1 <= n & n <= len p;
then n in dom p by FINSEQ_3:27;
hence p.n in D by A3,FINSEQ_2:13;
end;
A5: len r = len p + len q by FINSEQ_1:35;
then A6: len f = len p + (len q + 1) by A2,XCMPLX_1:1;
A7: len f = len p + 1 +len q by A2,A5,XCMPLX_1:1;
then consider f1,f2 being FinSequence such that
A8: len f1 = len p+1 & len f2 = len q & f = f1^f2 by FINSEQ_2:25;
now
take f1;
thus len f1 = len p + 1 by A8;
hereby
let n;
assume A9: 1 <= n & n <= len f1;
len f1 <= len f by A7,A8,NAT_1:29;
then n <= len f by A9,AXIOMS:22;
then A10: f.n in V by A2,A9;
n in dom f1 by A9,FINSEQ_3:27;
hence f1.n in V by A8,A10,FINSEQ_1:def 7;
end;
hereby
let n;
assume A11: 1 <= n & n <= len p;
len p <= len r by A5,NAT_1:29;
then n <= len r by A11,AXIOMS:22;
then consider x, y being Element of V such that
A12: x = f.n & y = f.(n+1) & r.n joins x, y by A2,A11;
take x,y;
len p <= len f1 by A8,NAT_1:29;
then n <= len f1 by A11,AXIOMS:22;
hence x = f1.n by A8,A11,A12,Lm1;
A13: 1 <= n+1 by NAT_1:29;
n+1 <= len f1 by A8,A11,REAL_1:55;
then n+1 in dom f1 by A13,FINSEQ_3:27;
hence y = f1.(n+1) by A8,A12,FINSEQ_1:def 7;
thus p.n joins x, y by A11,A12,Lm1;
end;
end;
hence p is Chain of G by A4,GRAPH_1:def 11;
A14: now let n;
assume 1 <= n & n <= len q;
then n in dom q by FINSEQ_3:27;
hence q.n in D by A3,FINSEQ_2:13;
end;
consider h1,h2 being FinSequence such that
A15: len h1 = len p & len h2 = len q +1 & f = h1^h2 by A6,FINSEQ_2:25;
now
take h2;
thus len h2 = len q + 1 by A15;
hereby
let n;
assume A16: 1 <= n & n <= len h2;
then n in dom h2 by FINSEQ_3:27;
then A17: h2.n=f.(len h1+n) by A15,FINSEQ_1:def 7;
len h1+n <= len h1 + len h2 by A16,REAL_1:55;
then A18: len h1+n <= len f by A15,FINSEQ_1:35;
n <= len h1+n by NAT_1:29;
then 1 <= len h1 +n by A16,AXIOMS:22;
hence h2.n in V by A2,A17,A18;
end;
hereby
let n;
assume A19: 1 <= n & n <= len q;
set m=len p+n;
A20: m <= len r by A5,A19,REAL_1:55;
n <= m by NAT_1:29;
then 1 <= m by A19,AXIOMS:22;
then consider x, y being Element of V such that
A21: x = f.m & y = f.(m+1) & r.m joins x, y by A2,A20;
take x,y;
len q <= len h2 by A15,NAT_1:29;
then n <= len h2 by A19,AXIOMS:22;
hence x = h2.n by A15,A19,A21,Lm2;
A22: n+1 <= len h2 by A15,A19,REAL_1:55;
1 <= n+1 by NAT_1:29;
hence h2.(n+1)=f.(len h1+(n+1)) by A15,A22,Lm2
.=y by A15,A21,XCMPLX_1:1;
thus q.n joins x, y by A19,A21,Lm2;
end;
end;
hence thesis by A14,GRAPH_1:def 11;
end;
theorem Th14:
p^q is oriented Chain of G implies p is oriented Chain of G &
q is oriented Chain of G
proof
assume A1: p^q is oriented Chain of G;
set r=p^q;
A2: len r = len p + len q by FINSEQ_1:35;
A3: now
let n;
assume A4: 1 <= n & n < len p;
len p <= len r by A2,NAT_1:29;
then n < len r by A4,AXIOMS:22;
then A5: (the Source of G).(r.(n+1))=(the Target of G).(r.n) by A1,A4,
GRAPH_1:def 12;
A6: n+1 <= len p by A4,NAT_1:38;
1 <= n+1 by NAT_1:29;
then p.(n+1)=r.(n+1) by A6,Lm1;
hence (the Source of G).(p.(n+1))=(the Target of G).(p.n)
by A4,A5,Lm1;
end;
now
let n;
assume A7: 1 <= n & n < len q;
set m=len p + n;
A8: m < len r by A2,A7,REAL_1:67;
n <= m by NAT_1:29;
then 1 <= m by A7,AXIOMS:22;
then A9: (the Source of G).(r.(m+1))=(the Target of G).(r.m) by A1,A8,
GRAPH_1:def 12;
A10: n+1 <= len q by A7,NAT_1:38;
1 <= n+1 by NAT_1:29;
then q.(n+1)=r.(len p+(n+1)) by A10,Lm2
.=r.(m+1) by XCMPLX_1:1;
hence (the Source of G).(q.(n+1))=(the Target of G).(q.n)
by A7,A9,Lm2;
end;
hence thesis by A1,A3,Th13,GRAPH_1:def 12;
end;
theorem Th15:
for p,q being oriented Chain of G st (the Target of G).(p.len p)
=(the Source of G).(q.1) holds p^q is oriented Chain of G
proof
let p,q be oriented Chain of G;
assume A1: (the Target of G).(p.len p)=(the Source of G).(q.1);
per cases;
suppose A2: p={} or q={};
hereby
per cases by A2;
suppose p={};
hence thesis by FINSEQ_1:47;
suppose q={};
hence thesis by FINSEQ_1:47;
end;
suppose not (p={} or q={});
then A3: len p >= 1 & len q >= 1 by Th8;
consider vs1 being FinSequence of the Vertices of G such that
A4: vs1 is_oriented_vertex_seq_of p by GRAPH_4:10;
consider vs2 being FinSequence of the Vertices of G such that
A5: vs2 is_oriented_vertex_seq_of q by GRAPH_4:10;
A6: len vs1 = len p + 1 &
for n st 1<=n & n<=len p holds p.n orientedly_joins vs1/.n, vs1/.(n+1)
by A4,GRAPH_4:def 5;
then A7: len vs1 >= 1 by NAT_1:37;
p.(len p) orientedly_joins vs1/.(len p), vs1/.(len p+1) by A3,A4,GRAPH_4
:def 5;
then A8: (the Target of G).(p.(len p))=vs1/.(len vs1) by A6,GRAPH_4:def 1
.=vs1.len vs1 by A7,FINSEQ_4:24;
len vs2 = len q + 1 &
for n st 1<=n & n<=len q holds q.n orientedly_joins vs2/.n, vs2/.(n+1)
by A5,GRAPH_4:def 5;
then A9: len vs2 >= 1 by NAT_1:37;
q.1 orientedly_joins vs2/.1, vs2/.(1+1) by A3,A5,GRAPH_4:def 5;
then (the Source of G).(q.1)=vs2/.1 by GRAPH_4:def 1
.=vs2.1 by A9,FINSEQ_4:24;
hence thesis by A1,A4,A5,A8,GRAPH_4:15;
end;
begin :: Additional Properties of Acyclic Oriented Paths
theorem Th16:
{} is Simple (oriented Chain of G)
proof
consider v being Element of the Vertices of G;
set vs=<*v*>;
A1: vs is_oriented_vertex_seq_of {} by GRAPH_4:9;
now
let n,m;
assume A2: 1<=n & n<m & m<=len vs & vs.n=vs.m;
assume not (n=1 & m=len vs);
len vs =1 by FINSEQ_1:56;
hence contradiction by A2,AXIOMS:22;
end;
hence thesis by A1,GRAPH_1:14,GRAPH_4:def 7;
end;
theorem Th17:
p^q is Simple (oriented Chain of G) implies
p is Simple (oriented Chain of G) & q is Simple (oriented Chain of G)
proof
assume A1: p^q is Simple (oriented Chain of G);
set r=p^q;
per cases;
suppose A2: p={} or q={};
hereby
per cases by A2;
suppose p={};
hence thesis by A1,Th16,FINSEQ_1:47;
suppose q={};
hence thesis by A1,Th16,FINSEQ_1:47;
end;
suppose A3: not (p={} or q={});
then len q <> 0 by FINSEQ_1:25;
then A4: len q > 0 by NAT_1:19;
consider vs being FinSequence of the Vertices of G such that
A5: vs is_oriented_vertex_seq_of r &
(for n,m 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 r + 1 &
for n st 1<=n & n<=len r holds r.n orientedly_joins vs/.n, vs/.(n+1)
by A5,GRAPH_4:def 5;
A7: len r = len p + len q by FINSEQ_1:35;
then A8: len vs = len p + (len q + 1) by A6,XCMPLX_1:1;
A9: len vs = len p + 1 +len q by A6,A7,XCMPLX_1:1;
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 as FinSequence of the Vertices of G by A10,FINSEQ_1:50;
now
let n;
assume A11: 1<=n & n <=len p;
len p <= len r by A7,NAT_1:29;
then A12: n <= len r by A11,AXIOMS:22;
then A13: r.n orientedly_joins vs/.n, vs/.(n+1) by A5,A11,GRAPH_4:def 5;
A14: n+ 0 <= len f1 by A10,A11,REAL_1:55;
len p <= len vs by A8,NAT_1:29;
then n <= len vs by A11,AXIOMS:22;
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 FINSEQ_4:def 4
.=vs.n by A10,A11,A14,Lm1
.=vs/.n by A15,FINSEQ_4:def 4;
A17: 1 <= n+1 by NAT_1:29;
n+1 <= len vs by A6,A12,REAL_1:55;
then A18: n+1 in dom vs by A17,FINSEQ_3:27;
A19: n+1 <= len f1 by A10,A11,REAL_1:55;
then n+1 in dom f1 by A17,FINSEQ_3:27;
then f1/.(n+1)=f1.(n+1) by FINSEQ_4:def 4
.=vs.(n+1) by A10,A17,A19,Lm1
.=vs/.(n+1) by A18,FINSEQ_4:def 4;
hence p.n orientedly_joins f1/.n, f1/.(n+1) by A11,A13,A16,Lm1;
end;
then A20: f1 is_oriented_vertex_seq_of p by A10,GRAPH_4:def 5;
now
let n,m;
assume A21: 1<=n & n<m & m<=len f1 & f1.n=f1.m;
assume not (n=1 & m=len f1);
n <= len f1 by A21,AXIOMS:22;
then A22: f1.n=vs.n by A10,A21,Lm1;
1 <= m by A21,AXIOMS:22;
then A23: f1.m=vs.m by A10,A21,Lm1;
len f1 + 0 < len vs by A4,A9,A10,REAL_1:67;
then m < len vs by A21,AXIOMS:22;
hence contradiction by A5,A21,A22,A23;
end;
hence p is Simple (oriented Chain of G) by A1,A20,Th14,GRAPH_4:def 7;
consider h1,h2 being FinSequence such that
A24: len h1 = len p & len h2 = len q +1 & vs = h1^h2 by A8,FINSEQ_2:25;
reconsider h2 as FinSequence of the Vertices of G by A24,FINSEQ_1:50;
now
let n;
assume A25: 1<=n & n <=len q;
set m=len p+n;
A26: m <= len r by A7,A25,REAL_1:55;
n <= m by NAT_1:29;
then A27: 1 <= m by A25,AXIOMS:22;
then A28: r.m orientedly_joins vs/.m, vs/.(m+1) by A5,A26,GRAPH_4:def 5;
A29: n+ 0 <= len h2 by A24,A25,REAL_1:55;
len r <= len vs by A6,NAT_1:29;
then m <= len vs by A26,AXIOMS:22;
then A30: m in dom vs by A27,FINSEQ_3:27;
n in dom h2 by A25,A29,FINSEQ_3:27;
then A31: h2/.n=h2.n by FINSEQ_4:def 4
.=vs.m by A24,A25,A29,Lm2
.=vs/.m by A30,FINSEQ_4:def 4;
A32: 1 <= n+1 by NAT_1:29;
A33: 1 <= m+1 by NAT_1:29;
m+1 <= len vs by A6,A26,REAL_1:55;
then A34: m+1 in dom vs by A33,FINSEQ_3:27;
A35: n+1 <= len h2 by A24,A25,REAL_1:55;
then n+1 in dom h2 by A32,FINSEQ_3:27;
then h2/.(n+1)=h2.(n+1) by FINSEQ_4:def 4
.=vs.(len h1 +(n+1)) by A24,A32,A35,Lm2
.=vs.(m+1) by A24,XCMPLX_1:1
.=vs/.(m+1) by A34,FINSEQ_4:def 4;
hence q.n orientedly_joins h2/.n, h2/.(n+1) by A25,A28,A31,Lm2;
end;
then A36: h2 is_oriented_vertex_seq_of q by A24,GRAPH_4:def 5;
now
let n,m;
assume A37: 1<=n & n<m & m<=len h2 & h2.n=h2.m;
assume not (n=1 & m=len h2);
n <= len h2 by A37,AXIOMS:22;
then A38: h2.n=vs.(len h1+n) by A24,A37,Lm2;
1 <= m by A37,AXIOMS:22;
then A39: h2.m=vs.(len h1+m) by A24,A37,Lm2;
len p <> 0 by A3,FINSEQ_1:25;
then 0 < len p by NAT_1:19;
then A40: 0 +1 < len h1 + n by A24,A37,REAL_1:67;
A41: len h1+n < len h1+m by A37,REAL_1:67;
len h1+m <= len vs by A8,A24,A37,REAL_1:55;
hence contradiction by A5,A37,A38,A39,A40,A41;
end;
hence q is Simple (oriented Chain of G) by A1,A36,Th14,GRAPH_4:def 7;
end;
theorem Th18:
len pe = 1 implies pe is Simple (oriented Chain of G)
proof
set p=pe;
assume A1: len p = 1;
then A2: 1 in dom p by FINSEQ_3:27;
set v1=(the Source of G).(p.1),
v2=(the Target of G).(p.1);
reconsider v1, v2 as Element of the Vertices of G by A2,Th11;
set vs=<*v1,v2*>;
A3: len vs = 2 by FINSEQ_1:61;
A4: len vs = len p +1 by A1,FINSEQ_1:61;
now
let n;
assume 1<=n & n<=len p;
then A5: n=1 by A1,AXIOMS:21;
vs/.1= v1 & vs/.(1+1)= v2 by FINSEQ_4:26;
hence p.n orientedly_joins vs/.n, vs/.(n+1) by A5,GRAPH_4:def 1;
end;
then A6: vs is_oriented_vertex_seq_of p by A4,GRAPH_4:def 5;
A7: now let n,m;
assume A8:1<=n & n<m & m<=len vs & vs.n=vs.m;
then n < 1+1 by A3,AXIOMS:22;
then n <= 1 by NAT_1:38;
hence n=1 by A8,AXIOMS:21;
1 < m by A8,AXIOMS:22;
then 1 + 1 < m + 1 by REAL_1:67;
then 2 <= m by NAT_1:38;
hence m=len vs by A3,A8,AXIOMS:21;
end;
A9: now let n;
assume 1 <= n & n <= len p;
then n in dom p by FINSEQ_3:27;
hence p.n in the Edges of G by FINSEQ_2:13;
end;
A10: now let n;
assume A11: 1 <= n & n <= len vs;
per cases;
suppose n < 1+1;
then n <= 1 by NAT_1:38;
then n=1 by A11,AXIOMS:21;
then vs.n=v1 by FINSEQ_1:61;
hence vs.n in the Vertices of G;
suppose n >= 2;
then n=2 by A3,A11,AXIOMS:21;
then vs.n=v2 by FINSEQ_1:61;
hence vs.n in the Vertices of G;
end;
A12: now let n;
assume 1 <= n & n <= len p;
then A13: n=1 by A1,AXIOMS:21;
take v1,v2;
thus v1= vs.n & v2 = vs.(n+1) by A13,FINSEQ_1:61;
thus p.n joins v1, v2 by A13,GRAPH_1:def 9;
end;
for n st 1 <= n & n < len p &
(the Source of G).(p.(n+1)) <> (the Target of G).(p.n) holds
contradiction by A1;
hence thesis by A4,A6,A7,A9,A10,A12,GRAPH_1:def 11,def 12,GRAPH_4:def 7;
end;
theorem Th19:
for p being Simple (oriented Chain of G), q being FinSequence of
the Edges of G st len p >=1 & len q=1 &
(the Source of G).(q.1)=(the Target of G).(p.(len p)) &
(the Source of G).(p.1) <> (the Target of G).(p.(len p)) &
not ex k st 1<=k & k <= len p & (the Target of G).(p.k)
=(the Target of G).(q.1) holds p^q is Simple (oriented Chain of G)
proof
let p be Simple (oriented Chain of G), q be FinSequence of
the Edges of G;
set FS=the Source of G,
FT=the Target of G,
v1=FS.(q.1),
v2=FT.(q.1),
vp=(the Target of G).(p.len p),
E=the Edges of G,
V=the Vertices of G;
assume A1: len p >=1 & len q=1 & v1=vp & FS.(p.1) <> vp &
not ex k st 1<=k & k <= len p & FT.(p.k) = v2;
consider r being FinSequence of V such that
A2: r is_oriented_vertex_seq_of p &
(for n,m st 1<=n & n<m & m<=len r & r.n=r.m holds n=1 & m=len r)
by GRAPH_4:def 7;
A3: len r = len p + 1 &
for n st 1<=n & n<=len p holds p.n orientedly_joins r/.n, r/.(n+1)
by A2,GRAPH_4:def 5;
A4: now
let n;
assume 1<=n & n<=len p;
then p.n orientedly_joins r/.n, r/.(n+1) by A2,GRAPH_4:def 5;
hence p.n joins r/.n, r/.(n+1) by GRAPH_4:1;
end;
set pq=p^q;
A5: now
let n;
assume 1 <= n & n <= len pq;
then n in dom pq by FINSEQ_3:27;
then pq.n in rng pq by FUNCT_1:def 5;
then A6: pq.n in rng p \/ rng q by FINSEQ_1:44;
rng p c= E & rng q c= E by FINSEQ_1:def 4;
then rng p \/ rng q c= E by XBOOLE_1:8;
hence pq.n in E by A6;
end;
1 in dom q by A1,FINSEQ_3:27;
then reconsider v1, v2 as Element of V by Th11;
set rv=r^<*v2*>;
A7: len rv = len r + 1 by FINSEQ_2:19;
then A8: len rv = len pq +1 by A1,A3,FINSEQ_1:35;
A9: now
let n;
assume A10: 1 <= n & n <= len rv;
per cases;
suppose n=len rv;
then rv.n=v2 by A7,FINSEQ_1:59;
hence rv.n in V;
suppose n<>len rv;
then n < len rv by A10,REAL_1:def 5;
then A11: n <= len r by A7,NAT_1:38;
then n in dom r by A10,FINSEQ_3:27;
then r.n in V by FINSEQ_2:13;
hence rv.n in V by A10,A11,Lm1;
end;
A12: now
let n;
assume A13: 1 <= n & n <= len pq;
per cases;
suppose n=len pq;
then A14: n = len r by A1,A3,FINSEQ_1:35;
take v1,v2;
set m=len p;
A15: n in dom r by A13,A14,FINSEQ_3:27;
p.m orientedly_joins r/.m, r/.(m+1) by A1,A2,GRAPH_4:def 5;
then vp = r/.(m+1) by GRAPH_4:def 1;
hence v1 = r.n by A1,A3,A14,A15,FINSEQ_4:def 4
.=rv.n by A13,A14,Lm1;
thus v2 = rv.(n+1) by A14,FINSEQ_1:59;
q.1 joins v1, v2 by GRAPH_1:def 9;
hence pq.n joins v1, v2 by A1,A3,A14,Lm2;
suppose n<>len pq;
then n < len pq by A13,REAL_1:def 5;
then A16: n < len p +1 by A1,FINSEQ_1:35;
then A17: n <= len p by NAT_1:38;
then A18: p.n joins r/.n, r/.(n+1) by A4,A13;
take x=r/.n;
take y=r/.(n+1);
n in dom r by A3,A13,A16,FINSEQ_3:27;
hence x = r.n by FINSEQ_4:def 4
.= rv.n by A3,A13,A16,Lm1;
A19: 1 <= n+1 by NAT_1:37;
A20: n+1 <= len r by A3,A16,NAT_1:38;
then n+1 in dom r by A19,FINSEQ_3:27;
hence y = r.(n+1) by FINSEQ_4:def 4
.=rv.(n+1) by A19,A20,Lm1;
thus pq.n joins x, y by A13,A17,A18,Lm1;
end;
A21: now
let n;
assume A22: 1 <= n & n < len pq;
per cases;
suppose A23: n < len p;
then A24: FS.(p.(n+1)) = FT.(p.n) by A22,GRAPH_1:def 12;
A25: p.n = pq.n by A22,A23,Lm1;
A26: 1 <= n+1 by NAT_1:37;
n+1 <= len p by A23,NAT_1:38;
hence FS.(pq.(n+1)) = FT.(pq.n) by A24,A25,A26,Lm1;
suppose A27: n >= len p;
n < len p + 1 by A1,A22,FINSEQ_1:35;
then n <= len p by NAT_1:38;
then A28: n = len p by A27,AXIOMS:21;
then pq.n=p.(len p) by A1,Lm1;
hence FS.(pq.(n+1)) = FT.(pq.n) by A1,A28,Lm2;
end;
set lp=len p;
p.lp orientedly_joins r/.lp, r/.(lp+1) by A1,A2,GRAPH_4:def 5;
then A29: vp = r/.(lp+1) by GRAPH_4:def 1;
now
let n;
assume A30: 1<=n & n<=len pq;
A31: dom r c= dom rv by FINSEQ_1:39;
per cases;
suppose A32: n <= len p;
then A33: p.n orientedly_joins r/.n, r/.(n+1) by A2,A30,GRAPH_4:def 5;
A34: n <= len r by A3,A32,NAT_1:37;
then A35: n in dom r by A30,FINSEQ_3:27;
then A36: r/.n= r.n by FINSEQ_4:def 4
.=rv.n by A30,A34,Lm1
.=rv/.n by A31,A35,FINSEQ_4:def 4;
A37: n+1 <= len r by A3,A32,REAL_1:55;
A38: 1 <= n+1 by NAT_1:37;
then A39: n+1 in dom r by A37,FINSEQ_3:27;
then r/.(n+1)= r.(n+1) by FINSEQ_4:def 4
.=rv.(n+1) by A37,A38,Lm1
.=rv/.(n+1) by A31,A39,FINSEQ_4:def 4;
hence pq.n orientedly_joins rv/.n, rv/.(n+1) by A30,A32,A33,A36,Lm1;
suppose n > len p;
then A40: len p +1 <= n by NAT_1:38;
A41: len p+1 >= n by A1,A30,FINSEQ_1:35;
then A42: n = len r by A3,A40,AXIOMS:21;
A43: n in dom r by A3,A30,A41,FINSEQ_3:27;
1 <= n+1 by NAT_1:37;
then A44: n+1 in dom rv by A7,A42,FINSEQ_3:27;
A45: v1 = r.n by A1,A3,A29,A42,A43,FINSEQ_4:def 4
.=rv.n by A3,A30,A41,Lm1
.=rv/.n by A31,A43,FINSEQ_4:def 4;
A46: v2 = rv.(n+1) by A42,FINSEQ_1:59
.=rv/.(n+1) by A44,FINSEQ_4:def 4;
q.1 orientedly_joins v1, v2 by GRAPH_4:def 1;
hence pq.n orientedly_joins rv/.n, rv/.(n+1) by A1,A3,A42,A45,A46,Lm2;
end;
then A47: rv is_oriented_vertex_seq_of pq by A8,GRAPH_4:def 5;
now
let n,m;
assume A48: 1<=n & n<m & m<=len rv & rv.n=rv.m;
assume A49: not (n=1 & m=len rv);
per cases;
suppose m < len rv;
then A50: m <= len r by A7,NAT_1:38;
then A51: n < len r by A48,AXIOMS:22;
A52: 1 <= m by A48,AXIOMS:22;
A53: r.n=rv.n by A48,A51,Lm1
.=r.m by A48,A50,A52,Lm1;
then A54: n=1 & m=len r by A2,A48,A50;
then A55: 1 in dom r by A48,FINSEQ_3:27;
A56: m in dom r by A50,A52,FINSEQ_3:27;
p.1 orientedly_joins r/.1, r/.(1+1) by A1,A2,GRAPH_4:def 5;
then FS.(p.1) = r/.1 by GRAPH_4:def 1
.=r.m by A53,A54,A55,FINSEQ_4:def 4
.=vp by A3,A29,A54,A56,FINSEQ_4:def 4;
hence contradiction by A1;
suppose A57: m >= len rv;
then m=len rv by A48,AXIOMS:21;
then A58: v2 = rv.m by A7,FINSEQ_1:59;
A59: 1 < n by A48,A49,A57,AXIOMS:21;
0 < n by A48,AXIOMS:22;
then consider k such that
A60: n=k+1 by NAT_1:22;
A61: 1 <= k by A59,A60,NAT_1:38;
k+1 < len r+1 by A7,A48,A60,AXIOMS:22;
then A62: k+1 <= len r by NAT_1:38;
then A63: k <= len p by A3,REAL_1:53;
A64: k+1 in dom r by A48,A60,A62,FINSEQ_3:27;
p.k orientedly_joins r/.k, r/.(k+1) by A2,A61,A63,GRAPH_4:def 5;
then FT.(p.k) = r/.(k+1) by GRAPH_4:def 1
.=r.(k+1) by A64,FINSEQ_4:def 4
.=v2 by A48,A58,A60,A62,Lm1;
hence contradiction by A1,A61,A63;
end;
hence pq is Simple (oriented Chain of G) by A5,A8,A9,A12,A21,A47,GRAPH_1:
def 11,def 12,GRAPH_4:def 7;
end;
theorem Th20:
for p being Simple (oriented Chain of G) holds p is one-to-one
proof
let p be Simple (oriented Chain of G);
set VV=the Vertices of G;
consider vs being FinSequence of VV such that
A1: vs is_oriented_vertex_seq_of p &
(for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs)
by GRAPH_4:def 7;
A2: len vs = len p + 1 &
for n st 1<=n & n<=len p holds p.n orientedly_joins vs/.n, vs/.(n+1)
by A1,GRAPH_4:def 5;
now
let n,m;
assume A3: 1<=n & n<m & m<=len p;
assume A4: p.n = p.m;
A5: n <= len p by A3,AXIOMS:22;
A6: 1 <= m by A3,AXIOMS:22;
then A7: p.m orientedly_joins vs/.m, vs/.(m+1) by A1,A3,GRAPH_4:def 5;
p.n orientedly_joins vs/.n, vs/.(n+1) by A1,A3,A5,GRAPH_4:def 5;
then A8: vs/.n = (the Source of G).(p.m) by A4,GRAPH_4:def 1
.= vs/.m by A7,GRAPH_4:def 1;
A9: len p < len vs by A2,REAL_1:69;
then n <= len vs by A5,AXIOMS:22;
then n in dom vs by A3,FINSEQ_3:27;
then A10: vs.n=vs/.n by FINSEQ_4:def 4;
A11: m <= len vs by A3,A9,AXIOMS:22;
then m in dom vs by A6,FINSEQ_3:27;
then vs.m=vs.n by A8,A10,FINSEQ_4:def 4;
then m= len vs by A1,A3,A11;
hence contradiction by A2,A3,REAL_1:69;
end;
hence thesis by Th9;
end;
begin :: The Set of the Vertices On a Path or an Edge
definition let G be Graph, e be Element of the Edges of G;
func vertices e equals :Def1:
{(the Source of G).e, (the Target of G).e};
coherence;
end;
definition let G,pe;
func vertices pe -> Subset of the Vertices of G equals :Def2:
{v where v is Vertex of G : ex i st i in dom pe & v in vertices(pe/.i)};
coherence
proof
set VT={v where v is Vertex of G : ex i st i in dom pe &
v in vertices(pe/.i) };
VT c= the Vertices of G
proof
let x be set;
assume x in VT;
then consider v being Vertex of G such that
A1: x=v & ex i st i in dom pe & v in vertices(pe/.i);
thus x in the Vertices of G by A1;
end;
hence VT is Subset of the Vertices of G;
end;
end;
theorem Th21:
for p being Simple (oriented Chain of G) st p=pe^qe & len pe >= 1 &
len qe >= 1 & (the Source of G).(p.1) <> (the Target of G).(p.len p)
holds not (the Source of G).(p.1) in vertices qe &
not (the Target of G).(p.len p) in vertices pe
proof
let p be Simple (oriented Chain of G);
set FT=the Target of G,
FS=the Source of G;
assume A1: p=pe^qe & len pe >= 1 & len qe >= 1 &
FS.(p.1) <> FT.(p.len p);
consider vs being FinSequence of the Vertices of G such that
A2: vs is_oriented_vertex_seq_of p &
(for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs)
by GRAPH_4:def 7;
A3: len vs = len p + 1 &
for n st 1<=n & n<=len p holds p.n orientedly_joins vs/.n, vs/.(n+1)
by A2,GRAPH_4:def 5;
A4: len p = len pe + len qe by A1,FINSEQ_1:35;
then A5: len p >= 1 by A1,NAT_1:37;
A6: 1 <= len vs by A3,NAT_1:37;
p.1 orientedly_joins vs/.1, vs/.(1+1) by A2,A5,GRAPH_4:def 5;
then A7: FS.(p.1)=vs/.1 by GRAPH_4:def 1
.=vs.1 by A6,FINSEQ_4:24;
p.len p orientedly_joins vs/.len p, vs/.(len p+1) by A2,A5,GRAPH_4:def 5
;
then A8: FT.(p.len p)=vs/.(len p+1) by GRAPH_4:def 1
.=vs.len vs by A3,A6,FINSEQ_4:24;
hereby
assume FS.(p.1) in vertices(qe);
then FS.(p.1) in {v where v is Vertex of G : ex i st i in dom qe &
v in vertices(qe/.i)} by Def2;
then consider x being Vertex of G such that
A9: FS.(p.1)=x & ex i st i in dom qe & x in vertices(qe/.i);
consider i such that
A10: i in dom qe & x in vertices(qe/.i) by A9;
A11: x in {FS.(qe/.i),FT.(qe/.i)} by A10,Def1;
set k=len pe + i;
A12: 1 <= i & i <= len qe by A10,FINSEQ_3:27;
A13: qe/.i=qe.i by A10,FINSEQ_4:def 4
.=p.k by A1,A10,FINSEQ_1:def 7;
A14: k <= len p by A4,A12,REAL_1:55;
A15: 1+i <= k by A1,REAL_1:55;
1 < i+1 by A12,NAT_1:38;
then A16: 1 < k by A15,AXIOMS:22;
A17: k <= len vs by A3,A14,NAT_1:38;
A18: p.k orientedly_joins vs/.k, vs/.(k+1) by A2,A14,A16,GRAPH_4:def 5;
per cases by A11,A13,TARSKI:def 2;
suppose A19: x=FS.(p.k);
FS.(p.k)=vs/.k by A18,GRAPH_4:def 1
.=vs.k by A16,A17,FINSEQ_4:24;
hence contradiction by A1,A2,A7,A8,A9,A16,A17,A19;
suppose A20: x=FT.(p.k);
A21: 1 <= k+1 by NAT_1:37;
A22: k+1 <= len vs by A3,A14,REAL_1:55;
A23: 1 < k+1 by A16,NAT_1:38;
FT.(p.k)=vs/.(k+1) by A18,GRAPH_4:def 1
.=vs.(k+1) by A21,A22,FINSEQ_4:24;
hence contradiction by A1,A2,A7,A8,A9,A20,A22,A23;
end;
hereby
assume FT.(p.len p) in vertices(pe);
then FT.(p.len p) in {v where v is Vertex of G : ex i st i in dom pe
&
v in vertices(pe/.i)} by Def2;
then consider x being Vertex of G such that
A24: FT.(p.len p)=x & ex i st i in dom pe & x in vertices(pe/.i);
consider i such that
A25: i in dom pe & x in vertices(pe/.i) by A24;
A26: x in {FS.(pe/.i),FT.(pe/.i)} by A25,Def1;
A27: 1 <= i & i <= len pe by A25,FINSEQ_3:27;
A28: pe/.i=pe.i by A25,FINSEQ_4:def 4
.=p.i by A1,A25,FINSEQ_1:def 7;
A29: i <= len p by A4,A27,NAT_1:37;
then A30: p.i orientedly_joins vs/.i, vs/.(i+1) by A2,A27,GRAPH_4:def 5;
A31: i < len vs by A3,A29,NAT_1:38;
per cases by A26,A28,TARSKI:def 2;
suppose A32: x=FS.(p.i);
FS.(p.i)=vs/.i by A30,GRAPH_4:def 1
.=vs.i by A27,A31,FINSEQ_4:24;
hence contradiction by A1,A2,A8,A24,A27,A31,A32;
suppose A33: x=FT.(p.i);
A34: 1 <= i+1 by NAT_1:37;
A35: i+1 <= len vs by A3,A29,REAL_1:55;
A36: len pe+1 <= len pe + len qe by A1,REAL_1:55;
i+1 <= len pe+1 by A27,REAL_1:55;
then i+1 <= len p by A4,A36,AXIOMS:22;
then A37: i+1 < len vs by A3,NAT_1:38;
FT.(p.i)=vs/.(i+1) by A30,GRAPH_4:def 1
.=vs.(i+1) by A34,A35,FINSEQ_4:24;
hence contradiction by A1,A2,A7,A8,A24,A33,A34,A37;
end;
end;
theorem Th22:
vertices pe c= V iff for i st i in dom pe holds vertices(pe/.i) c= V
proof
set FS=the Source of G, FT=the Target of G;
hereby
assume A1: vertices pe c= V;
hereby
let i;
assume A2: i in dom pe;
then A3: 1<=i & i <= len pe by FINSEQ_3:27;
thus vertices(pe/.i) c= V
proof
let x be set;
assume A4: x in vertices(pe/.i);
then x in {FS.(pe/.i),FT.(pe/.i)} by Def1;
then x = FS.(pe/.i) or x=FT.(pe/.i) by TARSKI:def 2;
then x = FS.(pe.i) or x=FT.(pe.i) by A3,FINSEQ_4:24;
then reconsider y=x as Vertex of G by A2,Th11;
y in {v where v is Vertex of G :
ex i st i in dom pe & v in vertices(pe/.i)} by A2,A4;
then y in vertices(pe) by Def2;
hence x in V by A1;
end;
end;
end;
assume A5: for i st i in dom pe holds vertices(pe/.i) c= V;
let x be set;
assume x in vertices pe;
then x in {v where v is Vertex of G : ex i st i in dom pe &
v in vertices(pe/.i)} by Def2;
then consider y being Vertex of G such that
A6: y=x & ex i st i in dom pe & y in vertices(pe/.i);
consider i such that
A7: i in dom pe & y in vertices(pe/.i) by A6;
vertices(pe/.i) c= V by A5,A7;
hence x in V by A6,A7;
end;
theorem Th23:
not vertices pe c= V implies ex i being Nat, q,r being FinSequence
of the Edges of G st i+1 <= len pe & not vertices(pe/.(i+1)) c= V &
len q=i & pe=q^r & vertices q c= V
proof
defpred P[Nat] means $1 in dom pe & not vertices(pe/.$1) c= V;
assume not vertices pe c= V;
then
A1: ex i st P[i] by Th22;
consider k such that
A2: P[k] & for n st P[n] holds k <= n from Min(A1);
A3: 1 <= k & k <= len pe by A2,FINSEQ_3:27;
then consider i such that
A4: k=1+i by NAT_1:28;
consider j such that
A5: len pe=k+j by A3,NAT_1:28;
len pe=i+(1+j) by A4,A5,XCMPLX_1:1;
then consider q,r being FinSequence such that
A6: len q = i & len r = 1+j & pe = q^r by FINSEQ_2:25;
reconsider q,r as FinSequence of the Edges of G by A6,FINSEQ_1:50;
take i,q,r;
thus i+1 <= len pe & not vertices(pe/.(i+1)) c= V by A2,A4,FINSEQ_3:27;
thus len q=i & pe=q^r by A6;
now let m;
assume A7: m in dom q;
then A8: m <= len q by FINSEQ_3:27;
assume A9: not vertices(q/.m) c= V;
A10: dom q c= dom pe by A6,FINSEQ_1:39;
q/.m=q.m by A7,FINSEQ_4:def 4
.=pe.m by A6,A7,FINSEQ_1:def 7
.=pe/.m by A7,A10,FINSEQ_4:def 4;
then k <= m by A2,A7,A9,A10;
hence contradiction by A4,A6,A8,NAT_1:38;
end;
hence vertices(q) c= V by Th22;
end;
theorem Th24:
rng qe c= rng pe implies vertices qe c= vertices pe
proof
assume A1: rng qe c= rng pe;
let x be set;
assume x in vertices qe;
then x in {v where v is Vertex of G : ex i st i in dom qe &
v in vertices(qe/.i)} by Def2;
then consider v being Vertex of G such that
A2: x=v & ex i st i in dom qe & v in vertices(qe/.i);
consider i such that
A3: i in dom qe & v in vertices(qe/.i) by A2;
A4: qe/.i=qe.i by A3,FINSEQ_4:def 4;
qe.i in rng qe by A3,FUNCT_1:def 5;
then consider j being set such that
A5: j in dom pe & qe.i = pe.j by A1,FUNCT_1:def 5;
reconsider j as Nat by A5;
pe/.j=qe/.i by A4,A5,FINSEQ_4:def 4;
then x in {u where u is Vertex of G : ex k st k in dom pe &
u in vertices(pe/.k)} by A2,A3,A5;
hence x in vertices(pe) by Def2;
end;
theorem Th25:
rng qe c= rng pe & vertices(pe) \ X c= V implies vertices(qe) \ X c= V
proof
assume A1: rng qe c= rng pe & vertices(pe) \ X c= V;
then vertices qe c= vertices pe by Th24;
then vertices qe \ X c= vertices(pe) \ X by XBOOLE_1:35;
hence thesis by A1,XBOOLE_1:1;
end;
theorem Th26:
vertices(pe^qe) \ X c= V implies vertices(pe) \ X c= V &
vertices(qe) \ X c= V
proof
assume A1: vertices(pe^qe) \ X c= V;
A2: rng pe c= rng(pe^qe) by FINSEQ_1:42;
rng qe c= rng(pe^qe) by FINSEQ_1:43;
hence thesis by A1,A2,Th25;
end;
reserve v,v1,v2,v3 for Element of the Vertices of G;
theorem Th27:
for e being Element of the Edges of G st
v=(the Source of G).e or v=(the Target of G).e holds v in vertices(e)
proof
set FS=the Source of G, FT=the Target of G;
let e be Element of the Edges of G;
assume v=FS.e or v=FT.e;
then v in {FS.e,FT.e} by TARSKI:def 2;
hence v in vertices(e) by Def1;
end;
theorem Th28:
i in dom pe & (v=(the Source of G).(pe.i) or
v=(the Target of G).(pe.i)) implies v in vertices pe
proof
set FS=the Source of G, FT=the Target of G;
assume A1:i in dom pe & (v=FS.(pe.i) or v=FT.(pe.i));
then v=FS.(pe/.i) or v=FT.(pe/.i) by FINSEQ_4:def 4;
then v in vertices(pe/.i) by Th27;
then v in {v1 where v1 is Vertex of G :
ex i st i in dom pe & v1 in vertices(pe/.i)} by A1;
hence v in vertices pe by Def2;
end;
theorem Th29:
len pe = 1 implies vertices(pe) = vertices(pe/.1)
proof
assume A1: len pe = 1;
set FS=the Source of G, FT=the Target of G;
A2: 1 in dom pe by A1,FINSEQ_3:27;
now
let x be set;
hereby
assume x in vertices(pe);
then x in {v where v is Vertex of G : ex i st i in dom pe &
v in vertices(pe/.i)} by Def2;
then consider y being Vertex of G such that
A3: y=x & ex i st i in dom pe & y in vertices(pe/.i);
consider i such that
A4: i in dom pe & y in vertices(pe/.i) by A3;
1<=i & i <= len pe by A4,FINSEQ_3:27;
hence x in vertices(pe/.1) by A1,A3,A4,AXIOMS:21;
end;
assume A5: x in vertices(pe/.1);
then x in {FS.(pe/.1),FT.(pe/.1)} by Def1;
then x=FS.(pe/.1) or x=FT.(pe/.1) by TARSKI:def 2;
then x=FS.(pe.1) or x=FT.(pe.1) by A1,FINSEQ_4:24;
then reconsider y=x as Vertex of G by A2,Th11;
y in {v where v is Vertex of G :
ex i st i in dom pe & v in vertices(pe/.i)} by A2,A5;
hence x in vertices(pe) by Def2;
end;
hence thesis by TARSKI:2;
end;
theorem Th30:
vertices pe c= vertices(pe^qe) & vertices qe c= vertices(pe^qe)
proof
A1: rng pe c= rng (pe^qe) by FINSEQ_1:42;
rng qe c= rng (pe^qe) by FINSEQ_1:43;
hence thesis by A1,Th24;
end;
reserve p,q for oriented Chain of G;
theorem Th31:
p = q^pe & len q >= 1 & len pe = 1 implies vertices(p) = vertices(q) \/
{(the Target of G).(pe.1)}
proof
assume A1: p = q^pe & len q >= 1 & len pe = 1;
set FS=the Source of G,
FT=the Target of G,
V3={FT.(pe.1)};
A2: len p = len q + 1 by A1,FINSEQ_1:35;
now
let x be set;
hereby
assume x in vertices p;
then x in {v where v is Vertex of G : ex i st i in dom p &
v in vertices(p/.i)} by Def2;
then consider y being Vertex of G such that
A3: y=x & ex i st i in dom p & y in vertices(p/.i);
consider i such that
A4: i in dom p & y in vertices(p/.i) by A3;
A5: 1<=i & i <= len p by A4,FINSEQ_3:27;
per cases;
suppose A6: i <= len q;
then A7: i in dom q by A5,FINSEQ_3:27;
p/.i=p.i by A5,FINSEQ_4:24
.=q.i by A1,A5,A6,Lm1
.=q/.i by A5,A6,FINSEQ_4:24;
then y in {v where v is Vertex of G : ex j st j in dom q &
v in vertices(q/.j)} by A4,A7;
then y in vertices(q) by Def2;
hence x in vertices(q) \/ V3 by A3,XBOOLE_0:def 2;
suppose i > len q;
then i >= len q+1 by NAT_1:38;
then A8: i = len q+1 by A2,A5,AXIOMS:21;
y in {FS.(p/.i),FT.(p/.i)} by A4,Def1;
then A9: y=FS.(p/.i) or y=FT.(p/.i) by TARSKI:def 2;
reconsider z=y as Vertex of G;
hereby
per cases by A5,A9,FINSEQ_4:24;
suppose A10: z=FS.(p.i);
len q < len p by A2,NAT_1:38;
then z=FT.(p.(len q)) by A1,A8,A10,GRAPH_1:def 12
.=FT.(q.(len q)) by A1,Lm1
.=FT.(q/.(len q)) by A1,FINSEQ_4:24;
then A11: z in vertices(q/.(len q)) by Th27;
len q in dom q by A1,FINSEQ_3:27;
then z in {v where v is Vertex of G : ex j st j in dom q
&
v in vertices(q/.j)} by A11;
then z in vertices(q) by Def2;
hence x in vertices(q) \/ V3 by A3,XBOOLE_0:def 2;
suppose z=FT.(p.i);
then z=FT.(pe.1) by A1,A8,Lm2;
then z in V3 by TARSKI:def 1;
hence x in vertices(q) \/ V3 by A3,XBOOLE_0:def 2;
end;
end;
assume A12: x in vertices(q) \/ V3;
per cases by A12,XBOOLE_0:def 2;
suppose A13: x in vertices q;
vertices q c= vertices p by A1,Th30;
hence x in vertices p by A13;
suppose x in V3;
then A14: x = FT.(pe.1) by TARSKI:def 1;
1 in dom pe by A1,FINSEQ_3:27;
then reconsider y=FT.(pe.1) as Vertex of G by Th11;
A15: 1 <= len p by A2,NAT_1:37;
y=FT.(p.(len p)) by A1,A2,Lm2
.=FT.(p/.(len p)) by A15,FINSEQ_4:24;
then A16: y in vertices(p/.(len p)) by Th27;
len p in dom p by A15,FINSEQ_3:27;
then y in {v where v is Vertex of G : ex j st j in dom p &
v in vertices(p/.j)} by A16;
hence x in vertices(p) by A14,Def2;
end;
hence thesis by TARSKI:2;
end;
theorem Th32:
v <> (the Source of G).(p.1) & v in vertices(p) implies
ex i st 1<=i & i <= len p & v = (the Target of G).(p.i)
proof
set FT=the Target of G, FS=the Source of G;
assume A1: v <> FS.(p.1) & v in vertices p;
then v in {u where u is Vertex of G: ex i st i in dom p &
u in vertices(p/.i)} by Def2;
then consider u being Vertex of G such that
A2: v=u & ex i st i in dom p & u in vertices(p/.i);
consider i such that
A3: i in dom p & u in vertices(p/.i) by A2;
u in {FS.(p/.i),FT.(p/.i)} by A3,Def1;
then A4: u=FS.(p/.i) or u=FT.(p/.i) by TARSKI:def 2;
A5: 1<=i & i <= len p by A3,FINSEQ_3:27;
per cases by A2,A4,A5,FINSEQ_4:24;
suppose A6: v=FT.(p.i);
take i;
thus thesis by A3,A6,FINSEQ_3:27;
suppose A7: v=FS.(p.i);
then A8: i > 1 by A1,A5,REAL_1:def 5;
consider j such that
A9: i=1+j by A5,NAT_1:28;
A10: j >= 1 by A8,A9,NAT_1:38;
A11: j < len p by A5,A9,NAT_1:38;
take j;
thus thesis by A7,A9,A10,A11,GRAPH_1:def 12;
end;
begin :: Directed Paths between Two vertices
definition let G, p, v1,v2;
pred p is_orientedpath_of v1,v2 means :Def3:
p <> {} & (the Source of G).(p.1) = v1 &
(the Target of G).(p.(len p))= v2;
end;
definition let G, v1,v2, p,V;
pred p is_orientedpath_of v1,v2,V means :Def4:
p is_orientedpath_of v1,v2 & vertices(p) \ {v2} c= V;
end;
definition let G be Graph, v1,v2 be Element of the Vertices of G;
func OrientedPaths(v1,v2) -> Subset of ((the Edges of G)*) equals :Def5:
{p where p is oriented Chain of G : p is_orientedpath_of v1,v2};
coherence
proof
set PT={p where p is oriented Chain of G: p is_orientedpath_of v1,v2};
PT c= ((the Edges of G)*)
proof
let e be set;
assume e in PT;
then consider p being oriented Chain of G such that
A1: (e=p & p is_orientedpath_of v1,v2);
thus e in ((the Edges of G)*) by A1,FINSEQ_1:def 11;
end;
hence PT is Subset of ((the Edges of G)*);
end;
end;
theorem Th33:
p is_orientedpath_of v1,v2 implies v1 in vertices p & v2 in vertices p
proof
assume p is_orientedpath_of v1,v2;
then A1: p <> {} & (the Source of G).(p.1) = v1 &
(the Target of G).(p.(len p))= v2 by Def3;
then 1 <= len p by Th8;
then 1 in dom p & len p in dom p by FINSEQ_3:27;
hence thesis by A1,Th28;
end;
theorem
x in OrientedPaths(v1,v2) iff ex p st p=x & p is_orientedpath_of v1,v2
proof
hereby assume x in OrientedPaths(v1,v2);
then x in {q where q is oriented Chain of G: q is_orientedpath_of v1,v2}
by Def5;
then consider p such that
A1: x = p & p is_orientedpath_of v1,v2;
take p;
thus x=p & p is_orientedpath_of v1,v2 by A1;
end;
assume ex p st (x=p & p is_orientedpath_of v1,v2);
then x in {q where q is oriented Chain of G: q is_orientedpath_of v1,v2};
hence x in OrientedPaths(v1,v2) by Def5;
end;
theorem Th35:
p is_orientedpath_of v1,v2,V & v1 <> v2 implies v1 in V
proof
assume A1: p is_orientedpath_of v1,v2,V & v1 <> v2;
then A2: vertices(p) \ {v2} c= V by Def4;
A3: not v1 in {v2} by A1,TARSKI:def 1;
p is_orientedpath_of v1,v2 by A1,Def4;
then v1 in vertices p by Th33;
then v1 in vertices(p) \ {v2} by A3,XBOOLE_0:def 4;
hence thesis by A2;
end;
theorem Th36:
p is_orientedpath_of v1,v2,V & V c= U implies p is_orientedpath_of v1,v2,U
proof
assume A1: p is_orientedpath_of v1,v2,V & V c= U;
then A2: p is_orientedpath_of v1,v2 & vertices(p) \ {v2} c= V by Def4;
then vertices(p) \ {v2} c= U by A1,XBOOLE_1:1;
hence thesis by A2,Def4;
end;
theorem Th37:
len p >= 1 & p is_orientedpath_of v1,v2 & pe.1 orientedly_joins v2,v3 &
len pe=1 implies ex q st q=p^pe & q is_orientedpath_of v1,v3
proof
assume A1: len p >= 1 & p is_orientedpath_of v1,v2 &
pe.1 orientedly_joins v2,v3 & len pe=1;
set FT=the Target of G,
FS=the Source of G;
A2: FS.(p.1)=v1 & FT.(p.len p)=v2 by A1,Def3;
A3: FS.(pe.1)=v2 & FT.(pe.1)=v3 by A1,GRAPH_4:def 1;
pe is oriented Chain of G by A1,Th18;
then reconsider q=p^pe as oriented Chain of G by A2,A3,Th15;
take q;
A4: len q=len p +1 by A1,FINSEQ_1:35;
then len q >= 1 by NAT_1:37;
then A5: q <> {} by Th8;
A6: FS.(q.1)=v1 by A1,A2,Lm1;
FT.(q.(len q))=v3 by A1,A3,A4,Lm2;
hence thesis by A5,A6,Def3;
end;
theorem Th38:
q=p^pe & len p >= 1 & len pe=1 & p is_orientedpath_of v1,v2,V &
pe.1 orientedly_joins v2,v3 implies q is_orientedpath_of v1,v3,V \/{v2}
proof
assume A1: q=p^pe & len p >= 1 & len pe=1 & p is_orientedpath_of v1,v2,V
& pe.1 orientedly_joins v2,v3;
set FT=the Target of G;
FT.(pe.1) = v3 by A1,GRAPH_4:def 1;
then vertices(q) \ {v3} = vertices(p) \/ {v3} \ {v3} by A1,Th31
.=vertices(p) \ {v3} by XBOOLE_1:40;
then A2: vertices(q) \ {v3} c= vertices(p) by XBOOLE_1:36;
vertices(p) \ {v2} c= V by A1,Def4;
then vertices p c= V \/ {v2} by XBOOLE_1:44;
then A3: vertices(q) \ {v3} c= V \/ {v2} by A2,XBOOLE_1:1;
p is_orientedpath_of v1,v2 by A1,Def4;
then consider r being oriented Chain of G such that
A4: r=p^pe & r is_orientedpath_of v1,v3 by A1,Th37;
thus thesis by A1,A3,A4,Def4;
end;
begin :: Acyclic (or Simple) Paths
definition let G be Graph, p be oriented Chain of G,
v1,v2 be Element of the Vertices of G;
pred p is_acyclicpath_of v1,v2 means :Def6:
p is Simple & p is_orientedpath_of v1,v2;
end;
definition let G be Graph, p be oriented Chain of G, v1,v2 be Element of
the Vertices of G,V be set;
pred p is_acyclicpath_of v1,v2,V means :Def7:
p is Simple & p is_orientedpath_of v1,v2,V;
end;
definition let G be Graph, v1,v2 be Element of the Vertices of G;
func AcyclicPaths(v1,v2) -> Subset of ((the Edges of G)*) equals :Def8:
{p where p is Simple (oriented Chain of G): p is_acyclicpath_of v1,v2};
coherence
proof
set PT={p where p is Simple (oriented Chain of G):
p is_acyclicpath_of v1,v2};
PT c= (the Edges of G)*
proof
let e be set;
assume e in PT;
then consider p being Simple (oriented Chain of G) such that
A1: (e=p & p is_acyclicpath_of v1,v2);
thus e in (the Edges of G)* by A1,FINSEQ_1:def 11;
end;
hence PT is Subset of (the Edges of G)*;
end;
end;
definition let G be Graph, v1,v2 be Element of the Vertices of G,V be set;
func AcyclicPaths(v1,v2,V) -> Subset of ((the Edges of G)*) equals :Def9:
{p where p is Simple (oriented Chain of G) : p is_acyclicpath_of v1,v2,V};
coherence
proof
set PT={p where p is Simple (oriented Chain of G):
p is_acyclicpath_of v1,v2,V};
PT c= (the Edges of G)*
proof
let e be set;
assume e in PT;
then consider p being Simple (oriented Chain of G) such that
A1: (e=p & p is_acyclicpath_of v1,v2,V);
thus e in ((the Edges of G)*) by A1,FINSEQ_1:def 11;
end;
hence PT is Subset of (the Edges of G)*;
end;
end;
definition let G be Graph, p be oriented Chain of G;
func AcyclicPaths(p) -> Subset of ((the Edges of G)*) equals :Def10:
{q where q is Simple (oriented 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};
coherence
proof
set PT={q where q is Simple (oriented 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};
PT c= (the Edges of G)*
proof
let e be set;
assume e in PT;
then consider q being Simple (oriented Chain of G) such that
A1: e=q & 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;
thus e in ((the Edges of G)*) by A1,FINSEQ_1:def 11;
end;
hence PT is Subset of (the Edges of G)*;
end;
end;
definition let G be Graph;
func AcyclicPaths(G) -> Subset of (the Edges of G)* equals :Def11:
{q where q is Simple (oriented Chain of G) : not contradiction};
coherence
proof
set PT={q where q is Simple (oriented Chain of G): not contradiction};
PT c= (the Edges of G)*
proof
let e be set;
assume e in PT;
then consider q being Simple (oriented Chain of G) such that
A1: e=q;
thus e in ((the Edges of G)*) by A1,FINSEQ_1:def 11;
end;
hence PT is Subset of (the Edges of G)*;
end;
end;
theorem
p={} implies not p is_acyclicpath_of v1,v2
proof
assume p={};
then not p is_orientedpath_of v1,v2 by Def3;
hence thesis by Def6;
end;
theorem
p is_acyclicpath_of v1,v2 implies p is_orientedpath_of v1,v2 by Def6;
theorem
AcyclicPaths(v1,v2) c= OrientedPaths(v1,v2)
proof
let x;
assume x in AcyclicPaths(v1,v2);
then x in {p where p is Simple (oriented Chain of G) :
p is_acyclicpath_of v1,v2} by Def8;
then consider p being Simple (oriented Chain of G) such that
A1: x=p & (p is_acyclicpath_of v1,v2);
p is_orientedpath_of v1,v2 by A1,Def6;
then p in {q where q is oriented Chain of G : q is_orientedpath_of v1,v2};
hence x in OrientedPaths(v1,v2) by A1,Def5;
end;
theorem Th42:
AcyclicPaths(p) c= AcyclicPaths(G)
proof
let e be set;
assume e in AcyclicPaths(p);
then e in {q where q is Simple (oriented 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 Def10;
then consider q being Simple (oriented Chain of G) such that
A1: e=q & 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;
e in {r where r is Simple (oriented Chain of G): not contradiction} by A1
;
hence e in AcyclicPaths(G) by Def11;
end;
theorem Th43:
AcyclicPaths(v1,v2) c= AcyclicPaths(G)
proof
let e be set;
assume e in AcyclicPaths(v1,v2);
then e in {p where p is Simple (oriented Chain of G) :
p is_acyclicpath_of v1,v2} by Def8;
then consider q being Simple (oriented Chain of G) such that
A1: e=q & q is_acyclicpath_of v1,v2;
e in {r where r is Simple (oriented Chain of G):
not contradiction} by A1;
hence e in AcyclicPaths(G) by Def11;
end;
theorem Th44:
p is_orientedpath_of v1,v2 implies AcyclicPaths(p) c= AcyclicPaths(v1,v2)
proof
assume p is_orientedpath_of v1,v2;
then A1: (the Source of G).(p.1) = v1 &
(the Target of G).(p.(len p)) = v2 by Def3;
let x;
assume x in AcyclicPaths(p);
then x in {q where q is Simple (oriented 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 Def10;
then consider q being Simple (oriented Chain of G) such that
A2: x=q & 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;
q is_orientedpath_of v1,v2 by A1,A2,Def3;
then q is_acyclicpath_of v1,v2 by Def6;
then q in {r where r is Simple (oriented Chain of G) :
r is_acyclicpath_of v1,v2};
hence x in AcyclicPaths(v1,v2) by A2,Def8;
end;
theorem Th45:
p is_orientedpath_of v1,v2,V implies
AcyclicPaths(p) c= AcyclicPaths(v1,v2,V)
proof
assume A1: p is_orientedpath_of v1,v2,V;
then p is_orientedpath_of v1,v2 by Def4;
then A2: (the Source of G).(p.1) = v1 &
(the Target of G).(p.(len p)) = v2 by Def3;
let x;
assume x in AcyclicPaths(p);
then x in {q where q is Simple (oriented 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 Def10;
then consider q being Simple (oriented Chain of G) such that
A3: x=q & 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;
A4: q is_orientedpath_of v1,v2 by A2,A3,Def3;
vertices(p) \ {v2} c= V by A1,Def4;
then vertices(q) \ {v2} c= V by A3,Th25;
then q is_orientedpath_of v1,v2,V by A4,Def4;
then q is_acyclicpath_of v1,v2,V by Def7;
then q in {r where r is Simple (oriented Chain of G) :
r is_acyclicpath_of v1,v2,V};
hence x in AcyclicPaths(v1,v2,V) by A3,Def9;
end;
theorem
q in AcyclicPaths(p) implies len q <= len p
proof
assume q in AcyclicPaths(p);
then q in {x where x is Simple (oriented Chain of G) : x <> {} &
(the Source of G).(x.1) = (the Source of G).(p.1) &
(the Target of G).(x.(len x)) = (the Target of G).(p.(len p)) &
rng (x) c= rng p} by Def10;
then consider x being Simple (oriented Chain of G) such that
A1: q=x & x <> {} & (the Source of G).(x.1) = (the Source of G).(p.1) &
(the Target of G).(x.(len x)) = (the Target of G).(p.(len p)) &
rng (x) c= rng p;
x is one-to-one by Th20;
then A2: card(rng x)=len x by FINSEQ_4:77;
A3: card (rng x) <= card (rng p) by A1,CARD_1:80;
A4: card (rng p) <= card (dom p) by Th1;
card (dom p) = card (Seg len p) by FINSEQ_1:def 3
.= len p by FINSEQ_1:78;
hence thesis by A1,A2,A3,A4,AXIOMS:22;
end;
theorem Th47:
p is_orientedpath_of v1,v2 implies AcyclicPaths(p) <> {} &
AcyclicPaths(v1,v2) <> {}
proof
assume A1: p is_orientedpath_of v1,v2;
defpred P[Nat] means for p,v1,v2 st $1+1 = len p &
p is_orientedpath_of v1,v2 holds AcyclicPaths(p) <> {};
set FS=the Source of G,
FT=the Target of G;
A2: P[0]
proof
let p,v1,v2;
assume A3: 0+1 = len p & p is_orientedpath_of v1,v2;
then reconsider r=p as Simple (oriented Chain of G) by Th18;
r <> {} by A3,FINSEQ_1:25;
then r in {q where q is Simple (oriented Chain of G) : q <> {} &
FS.(q.1) = FS.(p.1) & FT.(q.(len q)) = FT.(p.(len p)) &
rng q c= rng p};
hence AcyclicPaths(p) <> {} by Def10;
end;
A4: for k st P[k] holds P[k+1]
proof
let k;
assume A5: P[k];
now
let p,v1,v2;
assume A6: k+1+1 = len p & p is_orientedpath_of v1,v2;
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 as oriented Chain of G by A7,Th14;
A8: 1 <= len p1 by A7,NAT_1:29;
then A9: 1 in dom p1 & len p1 in dom p1 by FINSEQ_3:27;
then reconsider x=FS.(p1.1) as Element of the Vertices of G by Th11;
A10: p1.1=p.1 by A7,A8,Lm1;
reconsider y=FT.(p1.(len p1)) as Element of the Vertices of G
by A9,Th11;
p1 <> {} by A7,FINSEQ_1:25;
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;
r in {q where q is Simple (oriented Chain of G) : q <> {} &
FS.(q.1) = x & FT.(q.(len q)) = y & rng q c= rng (p1)}
by A11,Def10;
then consider q being Simple (oriented Chain of G) such that
A12: r=q & q <> {} & FS.(q.1) = x & FT.(q.(len q)) = y &
rng q c= rng p1;
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:38;
then A15: FS.(p.(len p1+1)) = FT.(p.(len p1)) by A8,GRAPH_1:def 12
.=FT.(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: FS.(p2.1)=FT.(q.(len q)) by A7,A13,A15,FINSEQ_1:def 7;
per cases;
suppose ex k st 1<=k & k <= len q & FT.(q.k)=FT.(p2.1);
then consider k such that
A19: 1<=k & k <= len q & FT.(q.k)=FT.(p2.1);
consider i such that
A20: len q = k + i by A19,NAT_1:28;
consider q1,q2 being FinSequence such that
A21: len q1 = k & len q2 = i & q = q1^q2 by A20,FINSEQ_2:25;
reconsider q1 as Simple (oriented 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;
0 < k by A19,AXIOMS:22;
then A23: q1 <> {} by A21,FINSEQ_1:25;
A24: rng q1 c= rng p by A16,A22,XBOOLE_1:1;
A25: FS.(q1.1) = FS.(p.1) by A10,A12,A19,A21,Lm1;
FT.(q1.(len q1)) = FT.(p.(len p)) by A6,A7,A14,A19,A21,Lm1;
then q1 in {w where w is Simple (oriented Chain of G) : w <> {} &
FS.(w.1) = FS.(p.1) & FT.(w.(len w)) = FT.(p.(len p)) &
rng (w) c= rng p} by A23,A24,A25;
hence AcyclicPaths(p) <> {} by Def10;
suppose A26: not ex k st 1<=k & k <= len q & FT.(q.k)=FT.(p2.1);
reconsider p2 as oriented Chain of G by A7,Th14;
hereby
per cases;
suppose A27: FS.(q.1) <> FT.(q.(len q));
set qp=q^p2;
A28: len q >=1 by A12,Th8;
then A29: qp is Simple (oriented Chain of G) by A7,A14,A15,A26,
A27,Th19;
A30: len qp = len q + 1 by A7,FINSEQ_1:35;
then A31: qp <> {} by FINSEQ_1:25;
A32: FS.(qp.1) = FS.(p.1) by A10,A12,A28,Lm1;
A33: FT.(qp.(len qp)) = FT.(p.(len p)) by A6,A7,A14,A30,Lm2;
A34: rng qp = rng q \/ rng p2 by FINSEQ_1:44;
rng q c= rng p by A12,A16,XBOOLE_1:1;
then rng qp c= rng p \/ rng p by A17,A34,XBOOLE_1:13;
then qp in {w where w is Simple (oriented Chain of G) : w <>
{} &
FS.(w.1) = FS.(p.1) & FT.(w.(len w)) = FT.(p.(len p)) &
rng (w) c= rng p} by A29,A31,A32,A33;
hence AcyclicPaths(p) <> {} by Def10;
suppose A35: FS.(q.1) = FT.(q.(len q));
reconsider p2 as Simple (oriented Chain of G) by A7,Th18;
A36: p2 <> {} by A7,FINSEQ_1:25;
FT.(p2.(len p2)) =FT.(p.(len p)) by A6,A7,Lm2;
then p2 in {w where w is Simple (oriented Chain of G) : w <>
{} &
FS.(w.1) = FS.(p.1) & FT.(w.(len w)) = FT.(p.(len p)) &
rng (w) c= rng p} by A10,A12,A17,A18,A35,A36;
hence AcyclicPaths(p) <> {} by Def10;
end;
end;
hence P[k+1];
end;
A37: for k holds P[k] from Ind(A2,A4);
p <> {} by A1,Def3;
then len p >=1 by Th8;
then len p -' 1 + 1= len p by AMI_5:4;
hence AcyclicPaths(p) <> {} by A1,A37;
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;
end;
theorem Th48:
p is_orientedpath_of v1,v2,V implies AcyclicPaths(p) <> {} &
AcyclicPaths(v1,v2,V) <> {}
proof
assume A1: p is_orientedpath_of v1,v2,V;
defpred P[Nat] means for p,v1,v2 st len p <= $1+1 &
p is_orientedpath_of v1,v2,V holds AcyclicPaths(p) <> {};
set FS=the Source of G,
FT=the Target of G;
A2: P[0]
proof
let p,v1,v2;
assume A3: len p <= 0+1 & p is_orientedpath_of v1,v2,V;
then p is_orientedpath_of v1,v2 by Def4;
then A4: p <> {} by Def3;
then len p >= 1 by Th8;
then len p = 1 by A3,AXIOMS:21;
then reconsider r=p as Simple (oriented Chain of G) by Th18;
r in {q where q is Simple (oriented Chain of G) : q <> {} &
FS.(q.1) = FS.(p.1) & FT.(q.(len q)) = FT.(p.(len p)) &
rng q c= rng p} by A4;
hence AcyclicPaths(p) <> {} by Def10;
end;
A5: for k st P[k] holds P[k+1]
proof
let k;
assume A6: P[k];
now
let p,v1,v2;
assume A7: len p <= k+1+1 & p is_orientedpath_of v1,v2,V;
consider vs being FinSequence of the Vertices of G such that
A8: vs is_oriented_vertex_seq_of p by GRAPH_4:10;
A9: len vs = len p + 1 & for n st 1<=n & n<=len p holds
p.n orientedly_joins vs/.n, vs/.(n+1) by A8,GRAPH_4:def 5;
A10: p is_orientedpath_of v1,v2 by A7,Def4;
then A11: p <> {} by Def3;
then A12: len p >= 1 by Th8;
A13: vertices(p) \ {v2} c= V by A7,Def4;
A14: len vs >= 1 by A9,NAT_1:37;
p.(len p) orientedly_joins vs/.(len p), vs/.(len p+1) by A8,A12,
GRAPH_4:def 5;
then FT.(p.(len p)) = vs/.(len p+1) by GRAPH_4:def 1;
then A15: FT.(p.(len p)) = vs.(len vs) by A9,A14,FINSEQ_4:24;
per cases;
suppose for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m
holds n=1 & m=len vs;
then p is Simple by A8,GRAPH_4:def 7;
then p in {w where w is Simple (oriented Chain of G) : w <> {}
&
FS.(w.1) = FS.(p.1) & FT.(w.(len w)) = FT.(p.(len p)) &
rng (w) c= rng p} by A11;
hence AcyclicPaths(p) <> {} by Def10;
suppose not for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m
holds n=1 & m=len vs;
then consider n,m such that
A16: 1<=n & n<m & m<=len vs & vs.n=vs.m & not (n=1 & m=len vs);
A17: m >= 1 by A16,AXIOMS:22;
then consider i such that
A18: m=1+i by NAT_1:28;
hereby
per cases;
suppose A19:n=1;
then m < len vs by A16,REAL_1:def 5;
then A20: m <= len p by A9,NAT_1:38;
then consider j such that
A21: len p=m+j by NAT_1:28;
A22: len p=i+(1+j) by A18,A21,XCMPLX_1:1;
then consider p1,p2 being FinSequence such that
A23: len p1 = i & len p2 = 1+j & p = p1^p2 by FINSEQ_2:25;
A24: n <= len vs by A16,AXIOMS:22;
A25: p.1 orientedly_joins vs/.1, vs/.(1+1) by A8,A12,GRAPH_4:
def 5;
p.m orientedly_joins vs/.m, vs/.(m+1) by A8,A16,A19,A20,
GRAPH_4:def 5
;
then A26: FS.(p.m) = vs/.m by GRAPH_4:def 1
.=vs.m by A16,A19,FINSEQ_4:24
.=vs/.n by A16,A24,FINSEQ_4:24
.=FS.(p.1) by A19,A25,GRAPH_4:def 1
.=v1 by A10,Def3;
A27: 1 <= len p2 by A23,NAT_1:29;
then A28: p2.1=p.m by A18,A23,Lm2;
p2.(len p2)=p.(len p) by A22,A23,A27,Lm2;
then A29: FT.(p2.(len p2))=v2 by A10,Def3;
reconsider p1,p2 as oriented Chain of G by A23,Th14;
p2 <> {} by A27,Th8;
then A30: p2 is_orientedpath_of v1,v2 by A26,A28,A29,Def3;
vertices(p1^p2) \ {v2} c= V by A7,A23,Def4;
then vertices(p2) \ {v2} c= V by Th26;
then A31: p2 is_orientedpath_of v1,v2,V by A30,Def4;
i+1+-1 > 1+-1 by A16,A18,A19,REAL_1:67;
then i > 1+-1 by XCMPLX_1:137;
then len p2 < len p by A22,A23,REAL_1:69;
then len p2 < k+1+1 by A7,AXIOMS:22;
then len p2 <= k+1 by NAT_1:38;
then AcyclicPaths(p2) <> {} by A6,A31;
then consider r being set such that
A32: r in AcyclicPaths(p2) by XBOOLE_0:def 1;
r in {q where q is Simple (oriented Chain of G) :
q <> {} & FS.(q.1) = v1 & FT.(q.(len q)) = v2 &
rng q c= rng p2} by A26,A28,A29,A32,Def10;
then consider q being Simple (oriented Chain of G) such
that
A33: r=q & q <> {} & FS.(q.1) = v1 & FT.(q.(len q)) = v2 &
rng q c= rng p2;
rng p2 c= rng p by A23,FINSEQ_1:43;
then A34: rng q c= rng p by A33,XBOOLE_1:1;
FS.(q.1) = FS.(p.1) & FT.(q.(len q)) = FT.(p.(len p))
by A10,A33,Def3;
then q in {w where w is Simple (oriented Chain of G) :
w <> {} & FS.(w.1) = FS.(p.1) & FT.(w.(len w)) =
FT.(p.(len p)) & rng w c= rng p} by A33,A34;
hence AcyclicPaths(p) <> {} by Def10;
suppose n<>1;
then A35: n > 1 by A16,REAL_1:def 5;
consider n1 being Nat such that
A36: n = 1+n1 by A16,NAT_1:28;
A37: n < len vs by A16,AXIOMS:22;
then A38: n1 < len p by A9,A36,REAL_1:55;
then consider j such that
A39: len p=n1+j by NAT_1:28;
consider p1,p2 being FinSequence such that
A40: len p1 = n1 & len p2 = j & p = p1^p2 by A39,FINSEQ_2:25;
A41: n1 >= 1 by A35,A36,NAT_1:38;
A42: rng p1 c= rng p by A40,FINSEQ_1:42;
p1.1=p.1 by A40,A41,Lm1;
then A43: FS.(p1.1)=v1 by A10,Def3;
p.n1 orientedly_joins vs/.n1,vs/.(n1+1)by A8,A38,A41,
GRAPH_4:def 5;
then A44: FT.(p.n1) = vs/.n by A36,GRAPH_4:def 1
.=vs.n by A16,A37,FINSEQ_4:24;
A45: p1.(len p1)=p.n1 by A40,A41,Lm1;
reconsider p1,p2 as oriented Chain of G by A40,Th14;
hereby
per cases;
suppose m=len vs;
then A46: FT.(p1.(len p1))=v2 by A10,A15,A16,A44,A45,Def3;
p1 <> {} by A40,A41,Th8;
then A47: p1 is_orientedpath_of v1,v2 by A43,A46,Def3;
vertices(p1^p2) \ {v2} c= V by A7,A40,Def4;
then vertices(p1) \ {v2} c= V by Th26;
then A48: p1 is_orientedpath_of v1,v2,V by A47,Def4;
n1 < k+1+1 by A7,A38,AXIOMS:22;
then len p1 <= k+1 by A40,NAT_1:38;
then AcyclicPaths(p1) <> {} by A6,A48;
then consider r being set such that
A49: r in AcyclicPaths(p1) by XBOOLE_0:def 1;
r in {q where q is Simple (oriented Chain of G):
q <> {} & FS.(q.1) = v1 & FT.(q.(len q)) = v2 &
rng q c= rng p1} by A43,A46,A49,Def10;
then consider q being Simple (oriented Chain of G) such
that
A50: r=q & q <> {} & FS.(q.1) = v1 & FT.(q.(len q))= v2
&rng q c= rng p1;
A51: rng q c= rng p by A42,A50,XBOOLE_1:1;
FS.(q.1) = FS.(p.1) & FT.(q.(len q)) = FT.(p.(len p)
)
by A10,A50,Def3;
then q in {w where w is Simple (oriented Chain of G)
:
w <> {} & FS.(w.1) = FS.(p.1) & FT.(w.(len w))=
FT.(p.(len p)) & rng w c= rng p} by A50,A51;
hence AcyclicPaths(p) <> {} by Def10;
suppose m<>len vs;
then m < len vs by A16,REAL_1:def 5;
then A52: m <= len p by A9,NAT_1:38;
then consider h being Nat such that
A53: len p=m+h by NAT_1:28;
A54: len p=i+(1+h) by A18,A53,XCMPLX_1:1;
then consider q1,q2 being FinSequence such that
A55: len q1 = i & len q2 = 1+h & p = q1^q2
by FINSEQ_2:25;
reconsider q2 as oriented Chain of G by A55,Th14;
p.m orientedly_joins vs/.m,vs/.(m+1)by A8,A17,A52,
GRAPH_4:def 5
;
then A56: FS.(p.m) = vs/.m by GRAPH_4:def 1
.=FT.(p1.len p1) by A16,A17,A44,A45,FINSEQ_4:24;
A57: 1 <= len q2 by A55,NAT_1:37;
then q2.1=p.m by A18,A55,Lm2;
then reconsider pq=p1^q2 as oriented Chain of G
by A56,Th15;
A58: FS.(pq.1)=v1 by A40,A41,A43,Lm1;
pq.(len pq)=pq.(len p1+len q2) by FINSEQ_1:35
.=q2.(len q2) by A57,Lm2
.=p.(len p) by A54,A55,A57,Lm2;
then A59: FT.(pq.(len pq))=v2 by A10,Def3;
A60: len pq = n1 + (1+h) by A40,A55,FINSEQ_1:35;
1 <= 1+h & 1+h <= n1+(1+h) by NAT_1:37;
then 1<= len pq by A60,AXIOMS:22;
then pq <> {} by Th8;
then A61: pq is_orientedpath_of v1,v2 by A58,A59,Def3;
A62: rng q2 c= rng p by A55,FINSEQ_1:43;
rng pq = rng p1 \/ rng q2 by FINSEQ_1:44;
then A63: rng pq c= rng p by A42,A62,XBOOLE_1:8;
then vertices(pq) \ {v2} c= V by A13,Th25;
then A64: pq is_orientedpath_of v1,v2,V by A61,Def4;
m+h > n+h by A16,REAL_1:67;
then n1+j > n1+(1+h) by A36,A39,A53,XCMPLX_1:1;
then len pq < k+1+1 by A7,A39,A60,AXIOMS:22;
then len pq <= k+1 by NAT_1:38;
then AcyclicPaths(pq) <> {} by A6,A64;
then consider r being set such that
A65: r in AcyclicPaths(pq) by XBOOLE_0:def 1;
r in {q where q is Simple (oriented Chain of G):
q <> {} & FS.(q.1) = v1 & FT.(q.(len q)) = v2 &
rng q c= rng pq} by A58,A59,A65,Def10;
then consider q being Simple (oriented Chain of G) such
that
A66: r=q & q <> {} & FS.(q.1) = v1 & FT.(q.(len q))= v2
& rng q c= rng pq;
A67: rng q c= rng p by A63,A66,XBOOLE_1:1;
FS.(q.1) = FS.(p.1) & FT.(q.(len q)) = FT.(p.(len p)
)
by A10,A66,Def3;
then q in {w where w is Simple (oriented Chain of G)
:
w <> {} & FS.(w.1) = FS.(p.1) & FT.(w.(len w))=
FT.(p.(len p)) & rng w c= rng p} by A66,A67;
hence AcyclicPaths(p) <> {} by Def10;
end;
end;
end;
hence P[k+1];
end;
A68: for k holds P[k] from Ind(A2,A5);
p is_orientedpath_of v1,v2 by A1,Def4;
then p <> {} by Def3;
then len p >=1 by Th8;
then len p -' 1 + 1= len p by AMI_5:4;
hence AcyclicPaths(p) <> {} by A1,A68;
then consider x being set such that
A69: x in AcyclicPaths(p) by XBOOLE_0:def 1;
AcyclicPaths(p) c= AcyclicPaths(v1,v2,V) by A1,Th45;
hence AcyclicPaths(v1,v2,V) <> {} by A69;
end;
theorem Th49:
AcyclicPaths(v1,v2,V) c= AcyclicPaths(G)
proof
let e be set;
assume e in AcyclicPaths(v1,v2,V);
then e in {p where p is Simple (oriented Chain of G) :
p is_acyclicpath_of v1,v2,V} by Def9;
then consider q being Simple (oriented Chain of G) such that
A1: e=q & q is_acyclicpath_of v1,v2,V;
e in {r where r is Simple (oriented Chain of G):
not contradiction} by A1;
hence e in AcyclicPaths(G) by Def11;
end;
begin :: Weight Graphs and Their Basic Properties
definition
func Real>=0 -> Subset of REAL equals :Def12:
{ r where r is Real : r >=0 };
coherence
proof
set IT = {r where r is Real : r >=0 };
now let x be set;
assume x in IT;
then consider r being Real such that
A1: x=r & r >= 0;
thus x in REAL by A1;
end;
hence thesis by TARSKI:def 3;
end;
end;
definition
cluster Real>=0 -> non empty;
coherence
proof
1 in Real>=0 by Def12;
hence thesis;
end;
end;
definition let G be Graph, W be Function;
pred W is_weight>=0of G means :Def13:
W is Function of the Edges of G, Real>=0;
end;
definition let G be Graph, W be Function;
pred W is_weight_of G means :Def14:
W is Function of (the Edges of G), REAL;
end;
definition
let G be Graph, p be FinSequence of the Edges of G, W be Function;
assume A1: W is_weight_of G;
func RealSequence(p,W) -> FinSequence of REAL means :Def15:
dom p = dom it & for i be Nat st i in dom p holds it.i=W.(p.i);
existence
proof
deffunc F(set) = W.(p.$1);
consider f such that
A2: dom f = dom p & for x st x in dom p holds f.x = F(x) from Lambda;
dom f = Seg len p by A2,FINSEQ_1:def 3;
then A3: f is FinSequence by FINSEQ_1:def 2;
now let i;
assume A4: i in dom f;
then A5: f.i=W.(p.i) by A2;
A6: W is Function of (the Edges of G), REAL by A1,Def14;
p.i in (the Edges of G) by A2,A4,FINSEQ_2:13;
hence f.i in REAL by A5,A6,FUNCT_2:7;
end;
then reconsider g=f as FinSequence of REAL by A3,FINSEQ_2:14;
take g; thus dom p = dom g by A2;
let i; assume i in dom p;
hence g.i=W.(p.i) by A2;
end;
uniqueness
proof
let f1, f2 be FinSequence of REAL;
assume A7: dom p = dom f1 &
for i be Nat st i in dom p holds f1.i=W.(p.i);
assume A8: dom p = dom f2 &
for i be Nat st i in dom p holds f2.i=W.(p.i);
now let i;
assume A9: i in dom f1;
hence f1.i=W.(p.i) by A7
.= f2.i by A7,A8,A9;
end;
hence f1=f2 by A7,A8,FINSEQ_1:17;
end;
end;
definition
let G be Graph, p be FinSequence of the Edges of G,W be Function;
func cost(p,W) -> Real equals :Def16:
Sum RealSequence(p,W);
coherence;
end;
theorem Th50:
W is_weight>=0of G implies W is_weight_of G
proof
assume W is_weight>=0of G;
then W is Function of the Edges of G, Real>=0 by Def13;
then W is Function of the Edges of G, REAL by FUNCT_2:9;
hence thesis by Def14;
end;
theorem Th51:
for f being FinSequence of REAL st
W is_weight>=0of G & f = RealSequence(pe,W) holds
for i st i in dom f holds f.i >= 0
proof
let f be FinSequence of REAL;
assume A1: W is_weight>=0of G & f = RealSequence(pe,W);
then W is_weight_of G by Th50;
then A2: dom pe = dom f &
for i st i in dom pe holds f.i=W.(pe.i) by A1,Def15;
A3: W is Function of the Edges of G, Real>=0 by A1,Def13;
let i;
assume A4:i in dom f;
then A5: f.i=W.(pe.i) by A2;
pe.i in (the Edges of G) by A2,A4,FINSEQ_2:13;
then f.i in Real>=0 by A3,A5,FUNCT_2:7;
then consider r being Real such that
A6: f.i=r & r >= 0 by Def12;
thus f.i >= 0 by A6;
end;
theorem Th52:
rng qe c= rng pe & W is_weight_of G & i in dom qe implies
ex j st j in dom pe & RealSequence(pe,W).j = RealSequence(qe,W).i
proof
assume A1: rng qe c= rng pe & W is_weight_of G & i in dom qe;
set f=RealSequence(pe,W), g=RealSequence(qe,W);
A2: g.i=W.(qe.i) by A1,Def15;
consider y being set such that
A3: y in dom pe & qe.i = pe.y by A1,Th2;
reconsider j=y as Nat by A3;
take j;
thus j in dom pe by A3;
thus f.j=g.i by A1,A2,A3,Def15;
end;
Lm3:
for f being FinSequence of REAL holds
(for y being Real st y in rng f holds y >= 0) iff
(for i st i in dom f holds f.i >= 0)
proof
let f be FinSequence of REAL;
hereby
assume A1: for y being Real st y in rng f holds y >= 0;
hereby
let i; assume i in dom f;
then f.i in rng f by FUNCT_1:def 5;
hence f.i >= 0 by A1;
end;
end;
assume A2: for i st i in dom f holds f.i >= 0;
hereby
let x be Real; assume x in rng f;
then consider y being set such that
A3: y in dom f & x = f.y by FUNCT_1:def 5;
thus x >= 0 by A2,A3;
end;
end;
Lm4:
for p,q,r being FinSequence of REAL st r=p^q & (for x being Real st x in
rng r holds x >= 0) holds (for i st i in dom p holds p.i >= 0) &
(for i st i in dom q holds q.i >= 0)
proof
let p, q,r be FinSequence of REAL;
assume A1: r=p^q & for x being Real st x in rng r holds x >= 0;
then rng p c= rng r by FINSEQ_1:42;
then for y be Real st y in rng p holds y >= 0 by A1;
hence for i st i in dom p holds p.i >= 0 by Lm3;
rng q c= rng r by A1,FINSEQ_1:43;
then for y be Real st y in rng q holds y >= 0 by A1;
hence for i st i in dom q holds q.i >= 0 by Lm3;
end;
theorem
len qe = 1 & rng qe c= rng pe & W is_weight>=0of G implies
cost(qe,W) <= cost(pe,W)
proof
assume A1: len qe = 1 & rng qe c= rng pe & W is_weight>=0of G;
then A2: 1 in dom qe by FINSEQ_3:27;
set f = RealSequence(pe,W),
g = RealSequence(qe,W);
A3: W is_weight_of G by A1,Th50;
then consider j such that
A4: j in dom pe & f.j = g.1 by A1,A2,Th52;
A5: 1 <= j & j <= len pe by A4,FINSEQ_3:27;
dom pe = dom f by A3,Def15;
then len pe = len f by FINSEQ_3:31;
then consider m such that
A6: len f = j+m by A5,NAT_1:28;
consider f1,f2 being FinSequence of REAL such that
A7: len f1 = j & len f2 = m & f = f1^f2 by A6,FINSEQ_2:26;
for i st i in dom f holds f.i >= 0 by A1,Th51;
then for y being Real st y in rng f holds y >= 0 by Lm3;
then A8: (for i st i in dom f1 holds f1.i >= 0) &
(for i st i in dom f2 holds f2.i >= 0) by A7,Lm4;
consider n such that
A9: j=1+n by A5,NAT_1:28;
dom g = dom qe by A3,Def15;
then len g = len qe by FINSEQ_3:31;
then A10: g = <*g.1*> by A1,FINSEQ_1:57;
A11: cost(qe,W) = Sum g by Def16
.= g.1 by A10,RVSUM_1:103;
A12: cost(pe,W) = Sum f by Def16;
consider h being FinSequence of REAL,d being Real such that
A13: f1= h^<*d*> by A7,A9,FINSEQ_2:22;
A14: j = len h +1 by A7,A13,FINSEQ_2:19;
j in dom f1 by A5,A7,FINSEQ_3:27;
then f1.j = g.1 by A4,A7,FINSEQ_1:def 7;
then A15: d=g.1 by A13,A14,FINSEQ_1:59;
A16: Sum f2 >= 0 by A8,RVSUM_1:114;
A17: Sum f= Sum f1 + Sum f2 by A7,RVSUM_1:105;
for y being Real st y in rng f1 holds y >= 0 by A8,Lm3;
then for i st i in dom h holds h.i >= 0 by A13,Lm4;
then A18: Sum h >= 0 by RVSUM_1:114;
Sum f1 = Sum h + Sum <*d*> by A13,RVSUM_1:105
.=Sum h + g.1 by A15,RVSUM_1:103;
then Sum f1 >= 0 + g.1 by A18,REAL_1:55;
hence thesis by A11,A12,A16,A17,REAL_1:55;
end;
theorem Th54:
W is_weight>=0of G implies cost(pe,W) >= 0
proof
assume A1: W is_weight>=0of G;
set f = RealSequence(pe,W);
for i st i in dom f holds f.i >= 0 by A1,Th51;
then Sum f>= 0 by RVSUM_1:114;
hence cost(pe,W) >= 0 by Def16;
end;
theorem Th55:
pe = {} & W is_weight_of G implies cost(pe,W) = 0
proof
assume A1: pe = {} & W is_weight_of G;
set f=RealSequence(pe,W);
dom f = dom pe by A1,Def15;
then len f = len pe by FINSEQ_3:31 .= 0 by A1,FINSEQ_1:25;
hence 0= Sum f by FINSEQ_1:32,RVSUM_1:102
.=cost(pe,W) by Def16;
end;
theorem Th56:
for D being non empty finite Subset of (the Edges of G)* st
D = AcyclicPaths(v1,v2) ex pe st pe in D & for qe st qe in D
holds cost(pe,W) <= cost(qe,W)
proof
let D be non empty finite Subset of (the Edges of G)*;
assume A1: D = AcyclicPaths(v1,v2);
deffunc F(Element of D) = cost($1,W);
consider x being Element of D such that
A2: for y being Element of D holds F(x) <= F(y) from MinValue;
x in AcyclicPaths(v1,v2) by A1;
then x in {p where p is Simple (oriented Chain of G) :
p is_acyclicpath_of v1,v2} by Def8;
then consider p being Simple (oriented Chain of G) such that
A3: x=p & p is_acyclicpath_of v1,v2;
take p;
thus p in D by A3;
let pe be FinSequence of the Edges of G;
assume pe in D;
then reconsider y=pe as Element of D;
F(x) <= F(y) by A2;
hence thesis by A3;
end;
theorem Th57:
for D being non empty finite Subset of (the Edges of G)* st
D = AcyclicPaths(v1,v2,V) holds ex pe st pe in D & for qe st qe in D
holds cost(pe,W) <= cost(qe,W)
proof
let D be non empty finite Subset of ((the Edges of G)*);
assume A1: D = AcyclicPaths(v1,v2,V);
deffunc F(Element of D) = cost($1,W);
consider x being Element of D such that
A2: for y being Element of D holds F(x) <= F(y) from MinValue;
x in AcyclicPaths(v1,v2,V) by A1;
then x in {p where p is Simple (oriented Chain of G) :
p is_acyclicpath_of v1,v2,V} by Def9;
then consider p being Simple (oriented Chain of G) such that
A3: x=p & p is_acyclicpath_of v1,v2,V;
take p;
thus p in D by A3;
let pe;
assume pe in D;
then reconsider y=pe as Element of D;
F(x) <= F(y) by A2;
hence thesis by A3;
end;
theorem Th58:
W is_weight_of G implies cost(pe^qe,W) = cost(pe,W) + cost(qe,W)
proof
assume A1: W is_weight_of G;
set r=pe^qe,
f=RealSequence(pe^qe,W),
g=RealSequence(pe,W),
h=RealSequence(qe,W);
A2: dom r = dom f & for i be Nat st i in dom r holds f.i=W.(r.i)
by A1,Def15;
A3: dom pe = dom g & for i be Nat st i in dom pe holds g.i=W.(pe.i)
by A1,Def15;
A4: dom qe = dom h & for i be Nat st i in dom qe holds h.i=W.(qe.i)
by A1,Def15;
then A5: len f = len r & len pe = len g & len qe = len h
by A2,A3,FINSEQ_3:31;
then A6: len f =len g + len h by FINSEQ_1:35;
A7: now
let i;
assume A8:i in dom g;
then A9: 1 <= i & i <= len g by FINSEQ_3:27;
A10: g.i=W.(pe.i) by A3,A8;
A11: r.i = pe.i by A3,A8,FINSEQ_1:def 7;
i <= len f by A6,A9,NAT_1:37;
then i in dom f by A9,FINSEQ_3:27;
hence f.i = g.i by A2,A10,A11;
end;
now
let i;
assume A12:i in dom h;
then A13: 1 <= i & i <= len h by FINSEQ_3:27;
A14: h.i=W.(qe.i) by A4,A12;
A15: r.(len g +i) = qe.i by A4,A5,A12,FINSEQ_1:def 7;
A16: 1 <= len g +i by A13,NAT_1:37;
len g +i <= len f by A6,A13,REAL_1:55;
then len g + i in dom f by A16,FINSEQ_3:27;
hence f.(len g +i) = h.i by A2,A14,A15;
end;
then A17: f=g^h by A6,A7,FINSEQ_3:43;
thus cost(pe^qe,W) = Sum f by Def16
.=Sum g + Sum h by A17,RVSUM_1:105
.= cost(pe,W) + Sum h by Def16
.= cost(pe,W) + cost(qe,W) by Def16;
end;
theorem Th59:
qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G implies
cost(qe,W) <= cost(pe,W)
proof
set D=the Edges of G;
assume A1: qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G;
defpred P[Nat] means
for p, q being FinSequence of D st q is one-to-one &
rng q c= rng p & len q = $1 holds cost(q,W) <= cost(p,W);
A2: W is_weight_of G by A1,Th50;
A3: P[0]
proof
let p, q be FinSequence of D;
assume q is one-to-one & rng q c= rng p & len q = 0;
then q = {} by FINSEQ_1:25;
then cost(q,W) = 0 by A2,Th55;
hence cost(q,W) <= cost(p,W) by A1,Th54;
end;
A4: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume A5: P[k];
now
let p, q be FinSequence of D;
assume A6: q is one-to-one & rng q c= rng p & len q = k+1;
then consider q1 being FinSequence, x being set such that
A7: q = q1^<*x*> by FINSEQ_2:21;
consider p1,p2 being FinSequence such that
A8: p=p1^<*x*>^p2 & rng q1 c= rng (p1^p2) by A6,A7,Th12;
k+1= len q1 +1 by A6,A7,FINSEQ_2:19;
then A9: len q1 = k by XCMPLX_1:2;
A10: p1^<*x*> is FinSequence of D by A8,FINSEQ_1:50;
then reconsider p1 as FinSequence of D by FINSEQ_1:50;
reconsider y=<*x*> as FinSequence of D by A10,FINSEQ_1:50;
reconsider p2 as FinSequence of D by A8,FINSEQ_1:50;
reconsider q1 as FinSequence of D by A7,FINSEQ_1:50;
A11: cost(q,W)=cost(q1,W)+cost(y,W) by A2,A7,Th58;
A12: cost(p,W)=cost(p1^y,W)+cost(p2,W) by A2,A8,Th58
.=cost(p1,W)+cost(y,W)+cost(p2,W) by A2,Th58
.=cost(p1,W)+cost(p2,W)+cost(y,W) by XCMPLX_1:1
.=cost(p1^p2,W)+cost(y,W) by A2,Th58;
q1 is one-to-one by A6,A7,FINSEQ_3:98;
then cost(q1,W) <= cost(p1^p2,W) by A5,A8,A9;
hence cost(q,W) <= cost(p,W) by A11,A12,REAL_1:55;
end;
hence P[k+1];
end;
for k being Nat holds P[k] from Ind(A3,A4);
then P[len qe];
hence thesis by A1;
end;
theorem Th60:
pe in AcyclicPaths(p) & W is_weight>=0of G implies cost(pe,W) <= cost(p,W)
proof
assume A1: pe in AcyclicPaths(p) & W is_weight>=0of G;
then pe in {r where r is Simple (oriented Chain of G) : r <> {} &
(the Source of G).(r.1) = (the Source of G).(p.1) &
(the Target of G).(r.(len r)) = (the Target of G).(p.(len p)) &
rng r c= rng p} by Def10;
then consider r being Simple (oriented Chain of G) such that
A2: r=pe & r <> {} & (the Source of G).(r.1) = (the Source of G).(p.1) &
(the Target of G).(r.(len r)) = (the Target of G).(p.(len p)) &
rng r c= rng p;
pe is one-to-one by A2,Th20;
hence cost(pe,W) <= cost(p,W) by A1,A2,Th59;
end;
begin :: Shortest Paths and Their Basic Properties
definition
let G be Graph, v1,v2 be Vertex of G,
p be oriented Chain of G, W be Function;
pred p is_shortestpath_of v1,v2,W means :Def17:
p is_orientedpath_of v1,v2 & for q being oriented Chain of G st q
is_orientedpath_of v1,v2 holds cost(p,W) <= cost(q,W);
end;
definition
let G be Graph, v1,v2 be Vertex of G, p be oriented Chain of G,
V be set, W be Function;
pred p is_shortestpath_of v1,v2,V,W means :Def18:
p is_orientedpath_of v1,v2,V & for q being oriented Chain of G
st q is_orientedpath_of v1,v2,V holds cost(p,W) <= cost(q,W);
end;
begin :: Basic Properties of a Graph with Finite Vertices
reserve G for finite Graph,
ps for Simple (oriented Chain of G),
P,Q for oriented Chain of G,
v1,v2,v3 for Element of the Vertices of G,
pe,qe for FinSequence of the Edges of G;
theorem
len ps <= VerticesCount G
proof
set VV=the Vertices of G;
consider vs being FinSequence of VV such that
A1: vs is_oriented_vertex_seq_of ps &
(for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs)
by GRAPH_4:def 7;
A2: len vs = len ps + 1 by A1,GRAPH_4:def 5;
then vs <> {} by FINSEQ_1:25;
then consider q being FinSequence, x be set such that
A3: vs = q^<*x*> by FINSEQ_1:63;
A4: len ps + 1 = len q + len <*x*> by A2,A3,FINSEQ_1:35
.=len q + 1 by FINSEQ_1:56;
then A5: len ps = len q by XCMPLX_1:2;
now
let n,m;
assume A6: 1<=n & n<m & m<=len q;
assume A7: q.n = q.m;
len q < len vs by A2,A4,REAL_1:69;
then A8: m < len vs by A6,AXIOMS:22;
A9: n <= len q by A6,AXIOMS:22;
A10: 1 <= m by A6,AXIOMS:22;
n in dom q by A6,A9,FINSEQ_3:27;
then A11: vs.n=q.n by A3,FINSEQ_1:def 7;
m in dom q by A6,A10,FINSEQ_3:27;
then vs.m=vs.n by A3,A7,A11,FINSEQ_1:def 7;
hence contradiction by A1,A6,A8;
end;
then A12: card(rng q)=len q by Th10;
A13: rng vs c= VV by FINSEQ_1:def 4;
reconsider V =VV as finite set by GRAPH_1:def 8;
rng q c= rng vs by A3,FINSEQ_1:42;
then rng q c= VV by A13,XBOOLE_1:1;
then card(rng q) <= card V by CARD_1:80;
hence thesis by A5,A12,GRAPH_1:def 18;
end;
theorem Th62:
len ps <= EdgesCount G
proof
ps is one-to-one by Th20;
then A1: card rng ps=len ps by FINSEQ_4:77;
A2: rng ps c= the Edges of G by FINSEQ_1:def 4;
reconsider V=the Edges of G as finite set by GRAPH_1:def 8;
card rng ps <= card V by A2,CARD_1:80;
hence len ps <= EdgesCount G by A1,GRAPH_1:def 19;
end;
Lm5:
AcyclicPaths(G) is finite
proof
A1: AcyclicPaths(G)= {p where p is Simple (oriented Chain of G):
not contradiction} by Def11;
set n = EdgesCount G,
D = the Edges of G,
A = {x where x is Element of D* : len x <= n };
D is finite by GRAPH_1:def 8;
then A2: A is finite by Th4;
AcyclicPaths(G) c= A
proof
let x;
assume x in AcyclicPaths(G);
then consider p being Simple (oriented Chain of G) such that
A3: x=p by A1;
A4: p is Element of D* by FINSEQ_1:def 11;
len p <= n by Th62;
hence x in A by A3,A4;
end;
hence thesis by A2,FINSET_1:13;
end;
definition let G;
cluster AcyclicPaths G -> finite;
coherence by Lm5;
end;
Lm6:
AcyclicPaths(P) is finite
proof
AcyclicPaths(P) c= AcyclicPaths(G) by Th42;
hence thesis by FINSET_1:13;
end;
Lm7:
AcyclicPaths(v1,v2) is finite
proof
AcyclicPaths(v1,v2) c= AcyclicPaths(G) by Th43;
hence thesis by FINSET_1:13;
end;
Lm8:
AcyclicPaths(v1,v2,V) is finite
proof
AcyclicPaths(v1,v2,V) c= AcyclicPaths(G) by Th49;
hence thesis by FINSET_1:13;
end;
definition let G, P;
cluster AcyclicPaths P -> finite;
coherence by Lm6;
end;
definition let G, v1, v2;
cluster AcyclicPaths(v1,v2) -> finite;
coherence by Lm7;
end;
definition let G, v1, v2, V;
cluster AcyclicPaths(v1,v2,V) -> finite;
coherence by Lm8;
end;
theorem
AcyclicPaths(v1,v2) <> {} implies ex pe st pe in AcyclicPaths(v1,v2) &
for qe st qe in AcyclicPaths(v1,v2) holds cost(pe,W) <= cost(qe,W) by Th56;
theorem
AcyclicPaths(v1,v2,V) <> {} implies ex pe st pe in AcyclicPaths(v1,v2,V) &
for qe st qe in AcyclicPaths(v1,v2,V) holds cost(pe,W) <= cost(qe,W) by Th57;
theorem
P is_orientedpath_of v1,v2 & W is_weight>=0of G implies
ex q being Simple(oriented Chain of G) st q is_shortestpath_of v1,v2,W
proof
assume A1: P is_orientedpath_of v1,v2 & W is_weight>=0of G;
then AcyclicPaths(v1,v2) <> {} by Th47;
then consider r being FinSequence of the Edges of G such that
A2: r in AcyclicPaths(v1,v2) & for s being FinSequence of the Edges of G
st s in AcyclicPaths(v1,v2) holds cost(r,W) <= cost(s,W) by Th56;
r in {t where t is Simple (oriented Chain of G) :
t is_acyclicpath_of v1,v2} by A2,Def8;
then consider t being Simple (oriented Chain of G) such that
A3: r=t & t is_acyclicpath_of v1,v2;
take t;
thus t is_orientedpath_of v1,v2 by A3,Def6;
hereby
let s be oriented Chain of G;
assume A4:s is_orientedpath_of v1,v2;
then AcyclicPaths(s) <> {} by Th47;
then consider x being Element of ((the Edges of G)*) such that
A5: x in AcyclicPaths(s) by SUBSET_1:10;
A6: cost(x,W) <= cost(s,W) by A1,A5,Th60;
AcyclicPaths(s) c= AcyclicPaths(v1,v2) by A4,Th44;
then cost(r,W) <= cost(x,W) by A2,A5;
hence cost(t,W) <= cost(s,W) by A3,A6,AXIOMS:22;
end;
end;
theorem Th66:
P is_orientedpath_of v1,v2,V & W is_weight>=0of G implies
ex q being Simple (oriented Chain of G) st q is_shortestpath_of v1,v2,V,W
proof
assume A1: P is_orientedpath_of v1,v2,V & W is_weight>=0of G;
then AcyclicPaths(v1,v2,V) <> {} by Th48;
then consider r being FinSequence of the Edges of G such that
A2: r in AcyclicPaths(v1,v2,V) & for s being FinSequence of the Edges of G
st s in AcyclicPaths(v1,v2,V) holds cost(r,W) <= cost(s,W) by Th57;
r in {t where t is Simple (oriented Chain of G) :
t is_acyclicpath_of v1,v2,V} by A2,Def9;
then consider t being Simple (oriented Chain of G) such that
A3: r=t & t is_acyclicpath_of v1,v2,V;
take t;
thus t is_orientedpath_of v1,v2,V by A3,Def7;
hereby
let s be oriented Chain of G;
assume A4:s is_orientedpath_of v1,v2,V;
then AcyclicPaths(s) <> {} by Th48;
then consider x being Element of ((the Edges of G)*) such that
A5: x in AcyclicPaths(s) by SUBSET_1:10;
A6: cost(x,W) <= cost(s,W) by A1,A5,Th60;
AcyclicPaths(s) c= AcyclicPaths(v1,v2,V) by A4,Th45;
then cost(r,W) <= cost(x,W) by A2,A5;
hence cost(t,W) <= cost(s,W) by A3,A6,AXIOMS:22;
end;
end;
begin :: Three Basic Theorems for Dijkstra's Shortest Path Algorithm
theorem Th67:
W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 &
(for Q, v3 st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds
cost(P,W) <= cost(Q,W)) implies P is_shortestpath_of v1,v2,W
proof
assume A1: W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W &
v1 <> v2 & (for Q, v3 st not v3 in V &
Q is_shortestpath_of v1,v3,V,W holds cost(P,W) <= cost(Q,W));
then A2: P is_orientedpath_of v1,v2,V by Def18;
then A3: P is_orientedpath_of v1,v2 by Def4;
A4: W is_weight_of G by A1,Th50;
A5: v1 in V by A1,A2,Th35;
now
let r be oriented Chain of G;
assume A6: r is_orientedpath_of v1,v2;
per cases;
suppose not vertices r c= V;
then consider i being Nat, s,t being FinSequence of the
Edges of G such that
A7: i+1 <= len r & not vertices(r/.(i+1)) c= V & len s=i
& r=s^t & vertices(s) c= V by Th23;
i+1 <= len s+len t by A7,FINSEQ_1:35;
then A8: 1 <= len t by A7,REAL_1:53;
then consider j such that
A9: len t = 1+j by NAT_1:28;
reconsider s,t as oriented Chain of G by A7,Th14;
consider t1,t2 being FinSequence such that
A10: len t1 = 1 & len t2 = j & t = t1^t2 by A9,FINSEQ_2:25;
reconsider t1,t2 as oriented Chain of G by A10,Th14;
A11: r=s^t1^t2 by A7,A10,FINSEQ_1:45;
then A12: cost(r,W)=cost(s^t1,W)+cost(t2,W) by A4,Th58;
cost(t2,W) >= 0 by A1,Th54;
then A13: cost(r,W) >= cost(s^t1,W)+0 by A12,REAL_1:55;
set e = r/.(i+1);
A14: 1 <= i+1 by NAT_1:29;
then A15: e = r.(i+1) by A7,FINSEQ_4:24;
A16: r.(i+1)=t.1 by A7,A8,Lm2
.=t1.1 by A10,Lm1;
set FT=the Target of G, FS=the Source of G;
consider x being set such that
A17: x in vertices e & not x in V by A7,TARSKI:def 3;
x in {FS.e,FT.e} by A17,Def1;
then A18: x=FS.e or x=FT.e by TARSKI:def 2;
1 in dom t1 by A10,FINSEQ_3:27;
then reconsider v3=x as Vertex of G by A15,A16,A18,Th11;
A19: v1=FS.(r.1) by A6,Def3;
hereby
per cases;
suppose A20: i=0;
then A21: v1=FS.e by A6,A15,Def3;
A22: t1 <> {} by A10,Th8;
A23: FS.(t1.1) = v1 by A6,A16,A20,Def3;
A24: t1 is_orientedpath_of v1,v3 by A1,A2,A10,A15,A16,A17,A18,
A21,A22,Def3,Th35;
vertices(t1) \ {v3} c= V
proof
let x be set;
assume x in vertices(t1) \ {v3};
then A25: x in vertices(t1) & not x in {v3} by XBOOLE_0:
def 4;
then x in vertices(t1/.1) by A10,Th29;
then x in {FS.(t1/.1),FT.(t1/.1)} by Def1;
then A26: x=FS.(t1/.1) or x=FT.(t1/.1) by TARSKI:def 2;
FT.(t1/.1) = v3 by A1,A2,A10,A15,A16,A17,A18,A19,A20
,Th35,FINSEQ_4:24;
hence x in V by A5,A10,A23,A25,A26,FINSEQ_4:24,TARSKI:
def 1;
end;
then A27: t1 is_orientedpath_of v1,v3,V by A24,Def4;
then consider q being Simple (oriented Chain of G) such
that
A28: q is_shortestpath_of v1,v3,V,W by A1,Th66;
A29: cost(P,W) <= cost(q,W) by A1,A17,A28;
cost(q,W) <= cost(t1,W) by A27,A28,Def18;
then A30: cost(P,W) <= cost(t1,W) by A29,AXIOMS:22;
s = {} by A7,A20,FINSEQ_1:25;
then s^t1 = t1 by FINSEQ_1:47;
hence cost(P,W) <= cost(r,W) by A13,A30,AXIOMS:22;
suppose i<>0;
then i > 0 by NAT_1:19;
then i+1 > 0+1 by REAL_1:67;
then A31: i >= 1 by NAT_1:38;
then A32: i in dom s by A7,FINSEQ_3:27;
A33: i < len r by A7,NAT_1:38;
A34: now
assume FS.(r.(i+1))=v3;
then A35: v3=FT.(r.i) by A31,A33,GRAPH_1:def 12;
r.i=s.i by A7,A31,Lm1;
then v3 in vertices s by A32,A35,Th28;
hence contradiction by A7,A17;
end;
reconsider u=s^t1 as oriented Chain of G by A11,Th14;
A36: len u = len s + len t1 by FINSEQ_1:35;
then len u >= 1 by A10,NAT_1:37;
then A37: u <> {} by Th8;
u.1 =s.1 by A7,A31,Lm1
.=r.1 by A7,A31,Lm1;
then A38: FS.(u.1) = v1 by A6,Def3;
u.len u =t1.1 by A10,A36,Lm2;
then A39: u is_orientedpath_of v1,v3 by A15,A16,A18,A34,A37,A38
,Def3;
vertices(u) \ {v3} c= V
proof
let x be set;
assume x in vertices(u) \ {v3};
then A40: x in vertices(u) & not x in {v3} by XBOOLE_0:def
4;
set V3={FT.(t1.1)};
vertices(u) = vertices(s) \/ V3 by A7,A10,A31,Th31;
then x in vertices(s) or x in V3 by A40,XBOOLE_0:def 2
;
hence x in V by A7,A14,A16,A18,A34,A40,FINSEQ_4:24;
end;
then A41: u is_orientedpath_of v1,v3,V by A39,Def4;
then consider q being Simple (oriented Chain of G) such
that
A42: q is_shortestpath_of v1,v3,V,W by A1,Th66;
A43: cost(P,W) <= cost(q,W) by A1,A17,A42;
cost(q,W) <= cost(u,W) by A41,A42,Def18;
then cost(P,W) <= cost(u,W) by A43,AXIOMS:22;
hence cost(P,W) <= cost(r,W) by A13,AXIOMS:22;
end;
suppose vertices r c= V;
then A44: vertices(r) \ {v2} c= V \ {v2} by XBOOLE_1:33;
V \ {v2} c= V by XBOOLE_1:36;
then vertices(r) \ {v2} c= V by A44,XBOOLE_1:1;
then r is_orientedpath_of v1,v2,V by A6,Def4;
hence cost(P,W) <= cost(r,W) by A1,Def18;
end;
hence P is_shortestpath_of v1,v2,W by A3,Def17;
end;
theorem
W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & V c= U &
(for Q, v3 st not v3 in V & Q is_shortestpath_of v1,v3,V,W
holds cost(P,W) <= cost(Q,W)) implies P is_shortestpath_of v1,v2,U,W
proof
assume A1: W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W &
v1 <> v2 & V c= U & (for Q, v3 st not v3 in V &
Q is_shortestpath_of v1,v3,V,W holds cost(P,W) <= cost(Q,W));
then P is_orientedpath_of v1,v2,V by Def18;
then A2: P is_orientedpath_of v1,v2,U by A1,Th36;
A3: P is_shortestpath_of v1,v2,W by A1,Th67;
now
let q be oriented Chain of G;
assume q is_orientedpath_of v1,v2,U;
then q is_orientedpath_of v1,v2 by Def4;
hence cost(P,W) <= cost(q,W) by A3,Def17;
end;
hence thesis by A2,Def18;
end;
definition let G be Graph, pe be FinSequence of the Edges of G,
V be set, v1 be Vertex of G, W be Function;
pred pe islongestInShortestpath V,v1,W means :Def19:
for v being Vertex of G st v in V & v <> v1 ex q being oriented Chain of G
st q is_shortestpath_of v1,v,V,W & cost(q,W) <= cost(pe,W);
end;
theorem
for G being finite oriented Graph,
P,Q,R being oriented Chain of G,
v1,v2,v3 being Element of the Vertices of G st
e in the Edges of G & W is_weight>=0of G & len P >= 1 &
P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & R=P^<*e*> &
Q is_shortestpath_of v1,v3,V,W & e orientedly_joins v2,v3 &
P islongestInShortestpath V,v1,W holds
(cost(Q,W) <= cost(R,W) implies Q is_shortestpath_of v1,v3,V \/{v2},W) &
(cost(Q,W) >= cost(R,W) implies R is_shortestpath_of v1,v3,V \/{v2},W)
proof
let G be finite oriented Graph,
P,Q,R be oriented Chain of G,
v1,v2,v3 be Element of the Vertices of G;
assume A1: e in the Edges of G & W is_weight>=0of G & len P >= 1 &
P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 &
R=P^<*e*> & Q is_shortestpath_of v1,v3,V,W &
e orientedly_joins v2,v3 & P islongestInShortestpath V,v1,W;
set V'=V \/ {v2};
A2: P is_orientedpath_of v1,v2,V by A1,Def18;
set Eg=the Edges of G;
reconsider pe=<*e*> as FinSequence of Eg by A1,SCMFSA_7:22;
len pe = 1 & pe.1=e by FINSEQ_1:57;
then A3: R is_orientedpath_of v1,v3,V' by A1,A2,Th38;
then consider s being Simple (oriented Chain of G) such that
A4: s is_shortestpath_of v1,v3,V',W by A1,Th66;
A5: s is_orientedpath_of v1,v3,V' by A4,Def18;
then A6: s is_orientedpath_of v1,v3 by Def4;
then s <> {} by Def3;
then A7: len s >= 1 by Th8;
A8: v1 in V by A1,A2,Th35;
A9: V c= V' by XBOOLE_1:7;
Q is_orientedpath_of v1,v3,V by A1,Def18;
then A10: Q is_orientedpath_of v1,v3,V' by A9,Th36;
A11: now
assume A12: cost(Q,W) <= cost(s,W);
hereby
assume cost(Q,W)<= cost(R,W);
now
let u be oriented Chain of G;
assume u is_orientedpath_of v1,v3,V';
then cost(s,W) <= cost(u,W) by A4,Def18;
hence cost(Q,W) <= cost (u,W) by A12,AXIOMS:22;
end;
hence Q is_shortestpath_of v1,v3,V',W by A10,Def18;
end;
hereby
assume A13: cost(Q,W)>= cost(R,W);
now
let u be oriented Chain of G;
assume u is_orientedpath_of v1,v3,V';
then cost(s,W) <= cost(u,W) by A4,Def18;
then cost(Q,W) <= cost (u,W) by A12,AXIOMS:22;
hence cost(R,W) <= cost (u,W) by A13,AXIOMS:22;
end;
hence R is_shortestpath_of v1,v3,V',W by A3,Def18;
end;
end;
set FT=the Target of G, FS=the Source of G;
A14: FT.(s.len s)=v3 by A6,Def3;
A15: FS.e=v2 & FT.e=v3 by A1,GRAPH_4:def 1;
A16: W is_weight_of G by A1,Th50;
per cases;
suppose len s >= 2;
then consider k such that
A17: len s = 1+1 + k by NAT_1:28;
A18: len s = 1 + (1+k) by A17,XCMPLX_1:1;
then consider s1,s2 being FinSequence such that
A19: len s1 = 1+k & len s2 = 1 & s = s1^s2 by FINSEQ_2:25;
reconsider s1,s2 as Simple (oriented Chain of G) by A19,Th17;
A20: s2.1 = s.len s by A18,A19,Lm2;
A21: len s1 >= 1 by A19,NAT_1:37;
A22: FS.(s.1)=v1 by A6,Def3;
then A23: FS.(s1.1)=v1 by A19,A21,Lm1;
A24: s1.len s1=s.len s1 by A19,A21,Lm1;
len s2 = 1 by A19;
then A25: not v3 in vertices(s1) & not v1 in vertices(s2) by A1,A14,A19,A21,
A22,Th21;
A26: len s1 < len s by A18,A19,NAT_1:38;
then A27: FS.(s.(len s1+1))=FT.(s.(len s1)) by A21,GRAPH_1:def 12;
A28: FS.(s2.1)=FT.(s1.(len s1)) by A18,A19,A20,A21,A24,A26,GRAPH_1:def 12;
A29: vertices(s) \ {v3} = vertices(s1) \/ {v3} \ {v3} by A14,A19,A20,A21,
Th31
.=vertices(s1) \ {v3} by XBOOLE_1:40
.=vertices(s1) by A25,ZFMISC_1:65;
A30: cost(s,W) = cost(s1,W)+cost(s2,W) by A16,A19,Th58;
vertices(s1) c= V' by A5,A29,Def4;
then A31: vertices(s1) \ {v2} c= V' \ {v2} by XBOOLE_1:33;
A32: V' \ {v2} = V \ {v2} by XBOOLE_1:40;
V \ {v2} c= V by XBOOLE_1:36;
then A33: vertices(s1) \ {v2} c= V by A31,A32,XBOOLE_1:1;
hereby
per cases;
suppose v2 in vertices(s1);
then consider i such that
A34: 1<=i & i <= len s1 & v2 = FT.(s1.i) by A1,A23,Th32;
s2/.1 in Eg by A1;
then A35: s2.1 in Eg by A19,FINSEQ_4:24;
hereby
per cases;
suppose A36: FS.(s2.1)=v2;
then s2.1=e by A1,A14,A15,A20,A35,GRAPH_1:def 4;
then A37: s2=pe by A19,FINSEQ_1:57;
s1 <> {} by A21,Th8;
then s1 is_orientedpath_of v1,v2 by A23,A28,A36,Def3;
then s1 is_orientedpath_of v1,v2,V by A33,Def4;
then A38: cost(P,W) <= cost(s1,W) by A1,Def18;
cost(R,W) = cost(P,W)+cost(s2,W) by A1,A16,A37,Th58;
then A39: cost(R,W) <= cost(s,W) by A30,A38,REAL_1:55;
hereby
assume cost(Q,W) <= cost(R,W);
then A40: cost(Q,W) <= cost(s,W) by A39,AXIOMS:22;
now
let u be oriented Chain of G;
assume u is_orientedpath_of v1,v3,V';
then cost(s,W) <= cost(u,W) by A4,Def18;
hence cost(Q,W) <= cost (u,W) by A40,AXIOMS:22;
end;
hence Q is_shortestpath_of v1,v3,V',W by A10,Def18;
end;
hereby
assume cost(Q,W)>= cost(R,W);
now
let u be oriented Chain of G;
assume u is_orientedpath_of v1,v3,V';
then cost(s,W) <= cost(u,W) by A4,Def18;
hence cost(R,W) <= cost (u,W) by A39,AXIOMS:22;
end;
hence R is_shortestpath_of v1,v3,V',W by A3,Def18;
end;
suppose A41: FS.(s2.1)<>v2;
len s1 in dom s1 by A21,FINSEQ_3:27;
then reconsider vx=FT.(s1.len s1) as Vertex of G by Th11;
1 in dom s2 by A19,FINSEQ_3:27;
then A42: vx <> v1 by A18,A19,A20,A24,A25,A27,Th28;
len s1 in dom s1 by A21,FINSEQ_3:27;
then A43: vx in vertices s1 by Th28;
A44: not vx in {v2} by A28,A41,TARSKI:def 1;
vertices s1 c= V' by A5,A29,Def4;
then A45: vx in V by A43,A44,XBOOLE_0:def 2;
then consider q' being oriented Chain of G such that
A46: q' is_shortestpath_of v1,vx,V,W & cost(q',W) <= cost(P,W)
by A1,A42,Def19;
A47: q' is_orientedpath_of v1,vx,V by A46,Def18;
then q' is_orientedpath_of v1,vx by Def4;
then A48: FS.(q'.1)=v1 & FT.(q'.len q')=vx & q'<>{} by Def3;
then reconsider qx=q'^s2 as oriented Chain of G by A18,A19,A20
,A24,A27,Th15;
A49: len qx = len q' + 1 by A19,FINSEQ_1:35;
then A50: qx <> {} by FINSEQ_1:25;
A51: len q' >= 1 by A48,Th8;
then A52: FS.(qx.1)=v1 by A48,Lm1;
FT.(qx.len qx)=v3 by A14,A19,A20,A49,Lm2;
then A53: qx is_orientedpath_of v1,v3 by A50,A52,Def3;
vertices(qx)= vertices(q') \/ {v3} by A14,A19,A20,A51,Th31;
then A54: vertices(qx) \ {v3} = vertices(q') \ {v3} by XBOOLE_1:40
;
vertices(q') \ {vx} c= V by A47,Def4;
then A55: vertices(q') c= V \/ {vx} by XBOOLE_1:44;
{vx} c= V
proof
let x be set;
assume x in {vx};
hence x in V by A45,TARSKI:def 1;
end;
then V \/ {vx} c= V by XBOOLE_1:8;
then vertices(q') c= V by A55,XBOOLE_1:1;
then A56: vertices(q') \ {v3} c= V \ {v3} by XBOOLE_1:33;
V \ {v3} c= V by XBOOLE_1:36;
then vertices(qx) \ {v3} c= V by A54,A56,XBOOLE_1:1;
then qx is_orientedpath_of v1,v3,V by A53,Def4;
then A57: cost(Q,W) <= cost(qx,W) by A1,Def18;
consider j such that
A58: len s1=i+j by A34,NAT_1:28;
consider t1,t2 being FinSequence such that
A59: len t1 = i & len t2 = j & s1 = t1^t2 by A58,FINSEQ_2:25;
reconsider t1,t2 as Simple (oriented Chain of G) by A59,Th17;
A60: t1 <> {} by A34,A59,Th8;
A61: FS.(t1.1)=v1 by A23,A34,A59,Lm1;
FT.(t1.len t1)=v2 by A34,A59,Lm1;
then A62: t1 is_orientedpath_of v1,v2 by A60,A61,Def3;
vertices(t1) c= vertices(t1^t2) by Th30;
then vertices(t1) \ {v2} c= vertices(s1) \ {v2}
by A59,XBOOLE_1:33;
then vertices(t1) \ {v2} c= V by A33,XBOOLE_1:1;
then t1 is_orientedpath_of v1,v2,V by A62,Def4;
then A63: cost(P,W) <= cost(t1,W) by A1,Def18;
A64: cost(s1,W)=cost(t1,W)+cost(t2,W) by A16,A59,Th58;
cost(t2,W) >= 0 by A1,Th54;
then cost(t1,W) + 0 <= cost(s1,W) by A64,REAL_1:55;
then cost(P,W) <= cost(s1,W) by A63,AXIOMS:22;
then A65: cost(q',W) <= cost(s1,W) by A46,AXIOMS:22;
cost(qx,W) = cost(q',W)+cost(s2,W) by A16,Th58;
then cost(qx,W) <= cost(s,W) by A30,A65,REAL_1:55;
then A66: cost(Q,W) <= cost(s,W) by A57,AXIOMS:22;
hereby
assume cost(Q,W) <= cost(R,W);
now
let u be oriented Chain of G;
assume u is_orientedpath_of v1,v3,V';
then cost(s,W) <= cost(u,W) by A4,Def18;
hence cost(Q,W) <= cost (u,W) by A66,AXIOMS:22;
end;
hence Q is_shortestpath_of v1,v3,V',W by A10,Def18;
end;
hereby
assume cost(Q,W)>= cost(R,W);
then A67: cost(R,W) <= cost(s,W) by A66,AXIOMS:22;
now
let u be oriented Chain of G;
assume u is_orientedpath_of v1,v3,V';
then cost(s,W) <= cost(u,W) by A4,Def18;
hence cost(R,W) <= cost (u,W) by A67,AXIOMS:22;
end;
hence R is_shortestpath_of v1,v3,V',W by A3,Def18;
end;
end;
suppose not v2 in vertices(s1);
then A68: vertices(s1) \ {v2} = vertices(s1) by ZFMISC_1:65;
then vertices(s1) \ {v2} c= V' by A5,A29,Def4;
then vertices(s) \ {v3} c= V by A29,A68,XBOOLE_1:43;
then s is_orientedpath_of v1,v3,V by A6,Def4;
hence thesis by A1,A11,Def18;
end;
suppose len s < 1+1;
then len s <= 1 by NAT_1:38;
then A69: len s=1 by A7,AXIOMS:21;
then A70: vertices s=vertices(s/.1) by Th29;
vertices(s) \ {v3} c= V
proof
let x be set;
assume x in vertices(s) \ {v3};
then A71: x in vertices(s/.1) & not x in {v3} by A70,XBOOLE_0:def 4;
then x in {FS.(s/.1),FT.(s/.1)} by Def1;
then A72: x=FS.(s/.1) or x=FT.(s/.1) by TARSKI:def 2;
A73: s/.1=s.1 by A7,FINSEQ_4:24;
v3=FT.(s.len s) by A6,Def3
.=FT.(s/.1) by A69,FINSEQ_4:24;
hence x in V by A6,A8,A71,A72,A73,Def3,TARSKI:def 1;
end;
then s is_orientedpath_of v1,v3,V by A6,Def4;
hence thesis by A1,A11,Def18;
end;