### The Mizar article:

### The Underlying Principle of Dijkstra's Shortest Path Algorithm

**by****Jing-Chao Chen, and****Yatsuka Nakamura**

- Received January 7, 2003
Copyright (c) 2003 Association of Mizar Users

- MML identifier: GRAPH_5
- [ MML identifier index ]

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;

Back to top