:: Vertex sequences induced by chains
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received May 13, 1995
:: Copyright (c) 1995-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, XBOOLE_0, SUBSET_1, NAT_1, ARYTM_3, XXREAL_0,
INT_1, ARYTM_1, RELAT_1, FUNCT_1, TARSKI, FINSET_1, CARD_1, ORDINAL1,
ORDINAL4, GRAPH_1, STRUCT_0, TREES_2, PARTFUN1, GLIB_000, FINSEQ_2,
ZFMISC_1, FINSEQ_4, FUNCT_4, GRAPH_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XXREAL_0, RELAT_1, RELSET_1, XXREAL_2, FINSEQ_1, FUNCT_1, PARTFUN1,
FUNCT_2, ZFMISC_1, FINSEQ_2, FINSEQ_4, FUNCT_7, FINSET_1, INT_1, NAT_1,
NAT_D, RECDEF_1, STRUCT_0, GRAPH_1;
constructors WELLORD2, RECDEF_1, FINSEQ_4, FINSEQ_6, GRAPH_1, FUNCT_7,
XXREAL_2, NAT_D, RELSET_1, FINSEQ_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1,
INT_1, CARD_1, FINSEQ_1, FINSEQ_6, GRAPH_1, NUMBERS, MEMBERED, VALUED_0,
XXREAL_2, STRUCT_0, RELSET_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, GRAPH_1, XBOOLE_0, FINSEQ_1;
equalities FINSEQ_2, FINSEQ_1;
expansions TARSKI, GRAPH_1, FINSEQ_1;
theorems TARSKI, ENUMSET1, NAT_1, FINSEQ_1, FINSEQ_2, GRAPH_1, RELAT_1,
FUNCT_1, GRFUNC_1, FUNCT_2, INT_1, CARD_1, CARD_2, FINSEQ_3, FINSEQ_4,
ZFMISC_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, ORDINAL1, XREAL_1, FINSEQ_5,
XXREAL_0, MEMBERED, FUNCT_7, PARTFUN1, XXREAL_2, XREAL_0, NAT_D,
XTUPLE_0;
schemes NAT_1, FINSEQ_1, FUNCT_1;
begin :: Preliminaries
reserve p, q for FinSequence,
X, Y, x, y for set,
D for non empty set,
i, j, k , l, m, n, r for Nat;
theorem Th1:
for m,k,n being Nat holds m+1<=k & k<=n iff
ex i being Nat st m<=i & i m+$1;
set rF = {kk where kk is Nat: m+1<=kk & kk<=m+n};
A1: rF c= Seg (m+n)
proof
let x be object;
assume x in rF;
then consider x9 being Nat such that
A2: x9=x and
A3: m+1<=x9 and
A4: x9<=m+n;
1<=m+1 by NAT_1:11;
then 1<=x9 by A3,XXREAL_0:2;
hence thesis by A2,A4;
end;
then reconsider rF as finite set;
assume ex l st P[l];
then
A5: ex l be Nat st P[l];
consider k be Nat such that
A6: P[k] and
A7: for nn being Nat st P[nn] holds k <= nn from NAT_1:sch 5 (A5);
reconsider k as Element of NAT by ORDINAL1:def 12;
A8: m+k<=m+n by A6,XREAL_1:7;
reconsider Fk = F.k as Element of NAT;
A9: card rF = n
proof
per cases;
suppose
A10: n = 0;
rF = {}
proof
assume rF <> {};
then consider x being object such that
A11: x in rF by XBOOLE_0:def 1;
ex x9 being Nat st x9=x & m+1<=x9 & x9<=m+n by A11;
then m+1<=m+0 by A10,XXREAL_0:2;
hence contradiction by XREAL_1:6;
end;
hence thesis by A10;
end;
suppose
0 x;
F.x <> m+x by A6,A27,XCMPLX_1:2;
hence contradiction by A7,A29,A30,A31;
end;
end;
begin :: The cut operation
definition
let p be FinSequence, m, n be Nat;
func (m, n)-cut p -> FinSequence means
:Def1:
len it +m = n+1 & for i being
Nat st i
proof
assume that
A1: 1<=m and
A2: m<=len p;
set mp = (m,m)-cut p;
A3: len mp + m = m + 1 by A1,A2,Def1;
then mp.(0+1) = p.(m+0) by A1,A2,Def1
.= p.m;
hence thesis by A3,FINSEQ_1:40;
end;
theorem Th7:
(1, len p)-cut p = p
proof
set cp = (1, len p)-cut p;
now
A1: 1<=len p +1 by NAT_1:11;
then
A2: len cp + 1 = len p + 1 by Lm2;
hence len cp = len p;
thus len p = len p;
let i be Nat;
assume
A3: i in dom cp;
A4: dom cp = Seg len p by A2,FINSEQ_1:def 3;
then
A5: i<=len p by A3,FINSEQ_1:1;
0+1<=i by A4,A3,FINSEQ_1:1;
then ex k being Nat st 0<=k & k FinSequence of D;
coherence
proof
A1: rng p c= D by FINSEQ_1:def 4;
rng (m,n)-cut p c= rng p by Th11;
then rng (m,n)-cut p c= D by A1;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem Th12:
1<=m & m<=n & n<=len p implies ((m,n)-cut p).1 = p.m & ((m,n)
-cut p).len ((m,n)-cut p)=p.n
proof
set c = ((m,n)-cut p);
assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len p;
A4: m<=n+1 by A2,NAT_1:12;
then
A5: len c +m = n+1 by A1,A3,Lm2;
A6: now
assume len c = 0;
then n+1<=n+0 by A2,A5;
hence contradiction by XREAL_1:6;
end;
then 0+1<=len c by NAT_1:13;
then consider i being Nat such that
0<=i and
A7: i FinSequence equals
p^(2, len q)-cut q;
correctness;
end;
theorem Th13:
q<>{} implies len (p^'q) +1 = len p + len q
proof
set r = (p^'q);
set qc = (2,len q)-cut q;
assume q<>{};
then 0+1<=len q by NAT_1:13;
then 1+1<=len q +1 by XREAL_1:7;
then
A1: len qc +(1+1) = len q + 1 by Lm2;
thus len r +1 = len p + len qc + 1 by FINSEQ_1:22
.= len p + len q by A1;
end;
theorem Th14:
1<=k & k<=len p implies (p^'q).k=p.k
proof
assume that
A1: 1<=k and
A2: k<=len p;
k in dom p by A1,A2,FINSEQ_3:25;
hence thesis by FINSEQ_1:def 7;
end;
theorem Th15:
1<=k & k{};
then 0+1<=len q by NAT_1:13;
then
A3: 1+1<=len q +1 by XREAL_1:7;
then len qc +(1+1) = len q + 1 by Lm2;
then len qc +1+1 = len q + 1;
then
A4: k<=len qc by A2,NAT_1:13;
0+1<=k by A1;
then consider i being Nat such that
0<=i and
A5: i{} by A1;
then len r +1-1=len p +len q -1 by Th13;
then
A3: len r = len p +(len q -1);
1+1<=len q +1 by A1,XREAL_1:7;
then len qc +(1+1) = len q + 1 by Lm2;
then
A4: len qc +1+1 = len q + 1;
then len qc < len q by NAT_1:13;
hence thesis by A3,A4,A2,Th15;
end;
theorem Th17:
rng (p^'q) c= rng p \/ rng q
proof
set r = p^'q;
set qc = (2,len q)-cut q;
let x be object;
assume x in rng r;
then x in rng p \/ rng qc by FINSEQ_1:31;
then
A1: x in rng p or x in rng qc by XBOOLE_0:def 3;
rng qc c= rng q by Th11;
hence thesis by A1,XBOOLE_0:def 3;
end;
definition
let D be set, p, q be FinSequence of D;
redefine func p^'q -> FinSequence of D;
coherence
proof
A1: rng (p^'q) c= rng p \/ rng q by Th17;
A2: rng q c= D by FINSEQ_1:def 4;
rng p c= D by FINSEQ_1:def 4;
then rng p \/ rng q c= D by A2,XBOOLE_1:8;
then rng (p^'q) c= D by A1;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem
p<>{} & q<>{} & p.len p = q.1 implies rng (p^'q) = rng p \/ rng q
proof
set r = p^'q;
set qc = (2,len q)-cut q;
assume that
A1: p<>{} and
A2: q<>{} and
A3: p.len p = q.1;
0+1<=len q by A2,NAT_1:13;
then
A4: 1+1<=len q +1 by XREAL_1:7;
then len qc +(1+1) = len q + 1 by Lm2;
then
A5: len qc +1+1 = len q + 1;
now
let x be object;
hereby
assume x in rng r;
then x in rng p \/ rng qc by FINSEQ_1:31;
then
A6: x in rng p or x in rng qc by XBOOLE_0:def 3;
rng qc c= rng q by Th11;
hence x in rng p \/ rng q by A6,XBOOLE_0:def 3;
end;
assume x in rng p \/ rng q;
then
A7: x in rng p or x in rng q by XBOOLE_0:def 3;
assume not x in rng r;
then
A8: not x in rng p \/ rng qc by FINSEQ_1:31;
then consider y being object such that
A9: y in dom q and
A10: x=q.y by A7,FUNCT_1:def 3,XBOOLE_0:def 3;
A11: not x in rng p by A8,XBOOLE_0:def 3;
reconsider y as Element of NAT by A9;
A12: 1<=y by A9,FINSEQ_3:25;
A13: y<=len q by A9,FINSEQ_3:25;
A14: not x in rng qc by A8,XBOOLE_0:def 3;
per cases by A12,XXREAL_0:1;
suppose
A15: y=1;
0+1<=len p by A1,NAT_1:13;
then len p in dom p by FINSEQ_3:25;
hence contradiction by A3,A11,A10,A15,FUNCT_1:def 3;
end;
suppose
1;
2 > 1;
hence len p > 1 by FINSEQ_1:44;
thus 1 <> 2;
thus rng p = rng<*1*>\/ rng<*2*> by FINSEQ_1:31
.= {1} \/ rng <*2*> by FINSEQ_1:38
.= {1} \/ {2} by FINSEQ_1:38
.= {1, 2} by ENUMSET1:1;
end;
theorem Th19:
p is TwoValued iff len p >1 & ex x,y being object st x<>y & rng p = {x, y}
proof
hereby
assume p is TwoValued;
then card rng p = 2;
then consider x,y being object such that
A1: x<>y and
A2: rng p={x,y} by CARD_2:60;
thus len p >1
proof
set l=len p;
assume
A3: len p<=1;
per cases by A3,NAT_1:25;
suppose
l=0;
then p={};
hence contradiction by A2;
end;
suppose
A4: l=1;
then 1 in dom p by FINSEQ_3:25;
then consider z being object such that
A5: [1,z] in p by XTUPLE_0:def 12;
z=p.1 by A5,FUNCT_1:1;
then p=<*z*> by A4,FINSEQ_1:40;
then
A6: rng p = {z} by FINSEQ_1:39;
then z=x by A2,ZFMISC_1:4;
hence contradiction by A1,A2,A6,ZFMISC_1:4;
end;
end;
thus ex x,y being object st x<>y & rng p ={x, y} by A1,A2;
end;
assume len p >1;
given x, y being object such that
A7: x<>y and
A8: rng p = {x, y};
card rng p = 2 by A7,A8,CARD_2:57;
hence thesis;
end;
then
Lm4: <*1, 2*> is TwoValued by Lm3;
Lm5: now
let i be Nat;
set p = <*1, 2*>;
assume that
A1: 1<=i and
A2: (i+1)<=len p;
i+1<=1+1 by A2,FINSEQ_1:44;
then i<=1 by XREAL_1:6;
then
A3: i = 1 by A1,XXREAL_0:1;
then p.i = 1 by FINSEQ_1:44;
hence p.i <> p.(i+1) by A3,FINSEQ_1:44;
end;
definition
let f be FinSequence;
attr f is Alternating means
:Def4:
for i being Nat st 1<=i & (i+1)<=len f holds f.i <> f.(i+1);
end;
Lm6: <*1, 2*> is Alternating by Lm5;
registration
cluster TwoValued Alternating for FinSequence;
existence by Lm4,Lm6;
end;
reserve a, a1, a2 for TwoValued Alternating FinSequence;
theorem Th20:
len a1 = len a2 & rng a1 = rng a2 & a1.1 = a2.1 implies a1 = a2
proof
assume that
A1: len a1 = len a2 and
A2: rng a1 = rng a2 and
A3: a1.1 = a2.1;
defpred P[Nat] means 1<=$1 & $1<=len a1 implies a1.$1=a2.$1;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume that
A5: 1<=k & k<=len a1 implies a1.k = a2.k;
A6: 0=k or 0 Y and
A12: rng a1 = { X, Y } by Th19;
a1.(k+1) in rng a1 by A9,FUNCT_1:def 3;
then
A13: a1.(k+1)=X or a1.(k+1)= Y by A12,TARSKI:def 2;
dom a1 = Seg len a1 by FINSEQ_1:def 3;
then a2.(k+1) in rng a2 by A1,A9,A11,FUNCT_1:def 3;
then
A14: a2.(k+1) = X or a2.(k+1) = Y by A2,A12,TARSKI:def 2;
k<=len a1 by A8,NAT_1:13;
then k in dom a1 by A10,FINSEQ_3:25;
then a1.k in rng a1 by FUNCT_1:def 3;
then a1.k=X or a1.k=Y by A12,TARSKI:def 2;
hence thesis by A1,A5,A8,A10,A13,A14,Def4,NAT_1:13;
end;
end;
A15: P[0];
for i being Nat holds P[i] from NAT_1:sch 2(A15, A4);
hence thesis by A1;
end;
theorem Th21:
a1<>a2 & len a1 = len a2 & rng a1 = rng a2 implies for i st 1<=i
& i<=len a1 holds a1.i<>a2.i
proof
assume that
A1: a1 <> a2 and
A2: len a1 = len a2 and
A3: rng a1 = rng a2;
defpred P[Nat] means 1<=$1 & $1<=len a1 implies a1.$1<>a2.$1;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume that
A5: 1<=k & k<=len a1 implies a1.k <> a2.k;
A6: 0=k or 0 Y and
A13: rng a1 = { X, Y } by Th19;
a1.(k+1) in rng a1 by A9,FUNCT_1:def 3;
then
A14: a1.(k+1)=X or a1.(k+1)= Y by A13,TARSKI:def 2;
dom a1 = Seg len a1 by FINSEQ_1:def 3;
then a2.k in rng a2 by A2,A11,A12,FUNCT_1:def 3;
then
A15: a2.k=X or a2.k=Y by A3,A13,TARSKI:def 2;
a1.k in rng a1 by A11,FUNCT_1:def 3;
then a1.k=X or a1.k=Y by A13,TARSKI:def 2;
hence thesis by A2,A5,A8,A10,A15,A14,Def4,NAT_1:13;
end;
end;
A16: P[0];
thus for i holds P[i] from NAT_1:sch 2 (A16, A4);
end;
theorem Th22:
a1<>a2 & len a1 = len a2 & rng a1 = rng a2 implies for a st len
a=len a1 & rng a=rng a1 holds a=a1 or a=a2
proof
assume that
A1: a1 <> a2 and
A2: len a1 = len a2 and
A3: rng a1 = rng a2;
let a;
assume that
A4: len a = len a1 and
A5: rng a = rng a1;
assume
A6: a <> a1;
now
let i be Nat;
assume that
A7: 1<=i and
A8: i<=len a;
consider X, Y being object such that
X <> Y and
A9: rng a = { X, Y } by Th19;
A10: i in dom a by A7,A8,FINSEQ_3:25;
then a.i in rng a by FUNCT_1:def 3;
then
A11: a.i=X or a.i=Y by A9,TARSKI:def 2;
A12: dom a=Seg len a by FINSEQ_1:def 3;
dom a1=Seg len a1 by FINSEQ_1:def 3;
then a1.i in rng a1 by A4,A10,A12,FUNCT_1:def 3;
then
A13: a1.i=X or a1.i=Y by A5,A9,TARSKI:def 2;
dom a2=Seg len a2 by FINSEQ_1:def 3;
then a2.i in rng a2 by A2,A4,A10,A12,FUNCT_1:def 3;
then a2.i=X or a2.i=Y by A3,A5,A9,TARSKI:def 2;
hence a.i = a2.i by A1,A2,A3,A4,A5,A6,A7,A8,A11,A13,Th21;
end;
hence thesis by A2,A4;
end;
theorem Th23:
X <> Y & n > 1 implies ex a1 st rng a1 = {X, Y} & len a1 = n & a1.1 = X
proof
deffunc F(Nat,Nat) = 3-'$2;
assume that
A1: X <> Y and
A2: n > 1;
set p = <*X, Y*>;
A3: p.1 = X by FINSEQ_1:44;
A4: 3-'2 =1+2-2 by XREAL_0:def 2
.=1;
A5: p.2 = Y by FINSEQ_1:44;
consider f1 being sequence of NAT such that
A6: f1.0=2 & for n being Nat holds f1.(n+1)=F(n,f1.n) from NAT_1:sch 12;
defpred P[Nat] means (f1.$1=1 or f1.$1=2) & f1.$1<>f1.($1+1);
A7: 3-'1=2+1-1 by XREAL_0:def 2
.=2;
A8: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A9: f1.i = 1 or f1.i = 2 and
f1.i <> f1.(i+1);
thus f1.(i+1)=1 or f1.(i+1) = 2 by A6,A4,A7,A9;
hence thesis by A6,A4,A7;
end;
A10: P[0] by A6,A4;
A11: for i being Nat holds P[i] from NAT_1:sch 2(A10, A8);
deffunc F(Nat) = p.(f1.$1);
consider p1 being FinSequence such that
A12: len p1 = n & for k be Nat st k in dom p1 holds p1.k= F(k) from
FINSEQ_1:sch 2;
A13: f1.(0+1) = 1 by A6,A4;
then
A14: f1.(1+1) = 2 by A6,A7;
A15: now
let y be object;
hereby
assume y in {X, Y};
then
A16: y = X or y = Y by TARSKI:def 2;
1 in dom p1 by A2,A12,FINSEQ_3:25;
then
A17: p1.1=X by A3,A13,A12;
A18: 1 in dom p1 by A2,A12,FINSEQ_3:25;
1+1<=n by A2,NAT_1:13;
then
A19: 2 in dom p1 by A12,FINSEQ_3:25;
then p1.2=Y by A5,A14,A12;
hence ex x being object st x in dom p1 & y = p1.x by A16,A19,A17,A18;
end;
given x being object such that
A20: x in dom p1 and
A21: y = p1.x;
x in Seg len p1 by A20,FINSEQ_1:def 3;
then consider x9 being Nat such that
A22: x9=x and
A23: 1<=x9 and
A24: x9<=len p1;
x9 in dom p1 by A23,A24,FINSEQ_3:25;
then
A25: p1.x9 = p.(f1.x9) by A12;
f1.x9 = 1 or f1.x9 = 2 by A11;
hence y in {X, Y} by A3,A5,A21,A22,A25,TARSKI:def 2;
end;
then rng p1 = {X, Y} by FUNCT_1:def 3;
then reconsider p1 as TwoValued FinSequence by A1,A2,A12,Th19;
now
let i be Nat;
assume that
A26: 1<=i and
A27: (i+1)<=len p1;
1<=(i+1) by A26,NAT_1:13;
then (i+1) in dom p1 by A27,FINSEQ_3:25;
then
A28: p1.(i+1)=p.(f1.(i+1)) by A12;
A29: f1.(i+1)=1 or f1.(i+1)=2 by A11;
i<=n by A12,A27,NAT_1:13;
then
i in dom p1 by A12,A26,FINSEQ_3:25;
then p1.i=p.(f1.i) by A12;
hence p1.i <> p1.(i+1) by A1,A3,A5,A11,A28,A29;
end;
then reconsider p1 as TwoValued Alternating FinSequence by Def4;
take p1;
thus rng p1 = {X, Y} by A15,FUNCT_1:def 3;
thus len p1 = n by A12;
1 in dom p1 by A2,A12,FINSEQ_3:25;
hence thesis by A3,A13,A12;
end;
begin :: Finite subsequences of finite sequences
registration
let X;
let fs be FinSequence of X;
cluster -> FinSubsequence-like for Subset of fs;
coherence
proof
let IT be Subset of fs;
take len fs;
dom IT c= dom fs by RELAT_1:11;
hence thesis by FINSEQ_1:def 3;
end;
end;
theorem Th24:
for f being FinSubsequence, g, h, fg, fh, fgh being FinSequence
st rng g c= dom f & rng h c= dom f & fg=f*g & fh=f*h & fgh=f*(g^h) holds fgh =
fg^fh
proof
let f be FinSubsequence, g, h, fg, fh, fgh be FinSequence;
assume that
A1: rng g c= dom f and
A2: rng h c= dom f and
A3: fg=f*g and
A4: fh=f*h and
A5: fgh=f*(g^h);
now
rng (g^h) = rng g \/ rng h by FINSEQ_1:31;
hence len fgh = len (g^h) by A1,A2,A5,FINSEQ_2:29,XBOOLE_1:8
.= len g + len h by FINSEQ_1:22;
then
A6: dom fgh = Seg (len g +len h) by FINSEQ_1:def 3;
A7: dom fh = dom h by A2,A4,RELAT_1:27;
A8: dom fg = dom g by A1,A3,RELAT_1:27;
A9: len fg = len g by A1,A3,FINSEQ_2:29;
len fh = len h by A2,A4,FINSEQ_2:29;
hence len (fg^fh) = len g + len h by A9,FINSEQ_1:22;
let j be Nat;
assume
A10: j in dom fgh;
then
A11: 1<=j by A6,FINSEQ_1:1;
A12: j<=len g + len h by A6,A10,FINSEQ_1:1;
per cases;
suppose
j<=len g;
then
A13: j in dom g by A11,FINSEQ_3:25;
thus fgh.j = f.((g^h).j) by A5,A10,FUNCT_1:12
.= f.(g.j) by A13,FINSEQ_1:def 7
.= fg.j by A3,A13,FUNCT_1:13
.= (fg^fh).j by A8,A13,FINSEQ_1:def 7;
end;
suppose
len g < j;
then len g +1 <=j by NAT_1:13;
then
A14: 1<=j-len g by XREAL_1:19;
then j-'len g = j-len g by XREAL_0:def 2;
then reconsider j9 = j-len g as Element of NAT;
A15: j = len g + j9;
then j9<=len h by A12,XREAL_1:6;
then
A16: j9 in dom h by A14,FINSEQ_3:25;
thus fgh.j = f.((g^h).j) by A5,A10,FUNCT_1:12
.= f.(h.j9) by A15,A16,FINSEQ_1:def 7
.= fh.j9 by A4,A16,FUNCT_1:13
.= (fg^fh).j by A9,A7,A15,A16,FINSEQ_1:def 7;
end;
end;
hence thesis by FINSEQ_2:9;
end;
reserve fs, fs1, fs2 for FinSequence of X,
fss, fss2 for Subset of fs;
theorem
dom fss c= dom fs & rng fss c= rng fs by RELAT_1:11;
theorem Th26:
fs is Subset of fs
proof
fs c= fs;
hence thesis;
end;
theorem Th27:
fss|Y is Subset of fs
proof
reconsider f = fss|Y as FinSubsequence;
f c= fss by RELAT_1:59;
hence thesis by XBOOLE_1:1;
end;
theorem Th28:
for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 &
fss2 = fss|rng((Sgm dom fss)|dom fss1) holds Seq fss2 = fs2
proof
let fss1 be Subset of fs1 such that
A1: Seq fss = fs1 and
A2: Seq fss1 = fs2 and
A3: fss2 = fss|rng((Sgm dom fss)|dom fss1);
consider k be Nat such that
A4: dom fs = Seg k by FINSEQ_1:def 2;
reconsider d2 = dom fss2 as finite set;
reconsider d1 = dom fss1 as finite set;
A5: ex l be Nat st dom fs1 = Seg l by FINSEQ_1:def 2;
then
A6: dom Sgm d1 = Seg card d1 by FINSEQ_3:40,RELAT_1:11;
reconsider k as Element of NAT by ORDINAL1:def 12;
A7: dom fss c= Seg k by A4,RELAT_1:11;
then rng Sgm dom fss c= dom fss by FINSEQ_1:def 13;
then
A8: dom fs1 = dom Sgm dom fss by A1,RELAT_1:27;
dom fss2 c= Seg k by A4,RELAT_1:11;
then
A9: rng Sgm dom fss2 = dom fss2 by FINSEQ_1:def 13;
A10: (Sgm dom fss)|dom fss1 c= Sgm dom fss by RELAT_1:59;
then
A11: dom ((Sgm dom fss)|dom fss1) c= dom (Sgm dom fss) by RELAT_1:11;
rng ((Sgm dom fss)|dom fss1) c= rng (Sgm dom fss) by A10,RELAT_1:11;
then
rng((Sgm dom fss)|dom fss1) c= dom fss by A7,FINSEQ_1:def 13;
then
A12: dom fss2 = rng((Sgm dom fss)|dom fss1) by A3,RELAT_1:62;
A13: dom fss1 c= dom fs1 by RELAT_1:11;
now
take Z = (Sgm dom fss)|dom fss1;
A14: dom Z = dom fss1 by A8,RELAT_1:11,62;
hereby
let x be object;
assume
A15: x in d1;
reconsider y = Z.x as object;
take y;
thus y in d2 by A12,A14,A15,FUNCT_1:def 3;
thus [x,y] in Z by A14,A15,FUNCT_1:1;
end;
hereby
let y be object;
assume y in d2;
then consider x being object such that
A16: x in dom Z and
A17: y = Z.x by A12,FUNCT_1:def 3;
reconsider x as object;
take x;
thus x in d1 & [x,y] in Z by A13,A8,A16,A17,FUNCT_1:1,RELAT_1:62;
end;
let x,y,z,u be object;
assume that
A18: [x,y] in Z and
A19: [z,u] in Z;
A20: z in dom Z by A19,FUNCT_1:1;
A21: u = Z.z by A19,FUNCT_1:1;
A22: u = (Sgm dom fss).z by A20,A21,FUNCT_1:47;
A23: y = Z.x by A18,FUNCT_1:1;
hence x=z implies y=u by A19,FUNCT_1:1;
A24: x in dom Z by A18,FUNCT_1:1;
then
A25: y = (Sgm dom fss).x by A23,FUNCT_1:47;
assume
A26: y=u;
assume
A27: x<>z;
reconsider x,z as Element of NAT by A24,A20;
A28: x<=len Sgm dom fss by A11,A24,FINSEQ_3:25;
A29: z<= len Sgm dom fss by A11,A20,FINSEQ_3:25;
A30: 1<=z by A11,A20,FINSEQ_3:25;
A31: 1<=x by A11,A24,FINSEQ_3:25;
per cases by A27,XXREAL_0:1;
suppose
x set equals
{ v: ex e being Element of the carrier' of G st
e in X & (v = (the Source of G).e or v = (the Target of G).e) };
correctness;
end;
definition
let G, vs;
let c be FinSequence;
pred vs is_vertex_seq_of c means
len vs = len c + 1 & for n being Nat st 1<=n &
n<=len c holds c.n joins vs/.n, vs/.(n+1);
end;
theorem Th31:
c <>{} & vs is_vertex_seq_of c implies G-VSet rng c = rng vs
proof
assume that
A1: c <>{} and
A2: vs is_vertex_seq_of c;
A3: len vs = len c + 1 by A2;
now
let y be object;
hereby
assume y in G-VSet rng c;
then consider v being Element of G such that
A4: v=y and
A5: ex e being Element of the carrier' of G st e in rng c & (v = (
the Source of G).e or v = (the Target of G).e);
consider e being Element of the carrier' of G such that
A6: e in rng c and
A7: v = (the Source of G).e or v = (the Target of G).e by A5;
consider x being object such that
A8: x in dom c and
A9: e = c.x by A6,FUNCT_1:def 3;
reconsider x as Element of NAT by A8;
A10: 1<=x+1 by NAT_1:12;
set v2 = vs/.(x+1);
set v1 = vs/.x;
A11: x<=len c by A8,FINSEQ_3:25;
then x+1<=len vs by A3,XREAL_1:7;
then
A12: x+1 in dom vs by A10,FINSEQ_3:25;
A13: 1<=x by A8,FINSEQ_3:25;
then c.x joins v1, v2 by A2,A11;
then
A14: v = v1 or v = v2 by A7,A9;
A15: x<=len vs by A3,A11,NAT_1:12;
then
A16: v1 = vs.x by A13,FINSEQ_4:15;
A17: x in dom vs by A13,A15,FINSEQ_3:25;
v2 = vs.(x+1) by A3,A11,A10,FINSEQ_4:15,XREAL_1:7;
hence y in rng vs by A4,A16,A14,A17,A12,FUNCT_1:def 3;
end;
assume y in rng vs;
then consider x being object such that
A18: x in dom vs and
A19: y = vs.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A18;
A20: 1<=x by A18,FINSEQ_3:25;
A21: x<=len vs by A18,FINSEQ_3:25;
per cases by A3,A21,NAT_1:8;
suppose
A22: x<=len c;
then x in dom c by A20,FINSEQ_3:25;
then
A23: c.x in rng c by FUNCT_1:def 3;
rng c c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e = c.x as Element of the carrier' of G by A23;
x in dom c by A20,A22,FINSEQ_3:25;
then
A24: e in rng c by FUNCT_1:def 3;
set v2 = vs/.(x+1);
set v1 = vs/.x;
c.x joins v1, v2 by A2,A20,A22;
then
A25: v1 = (the Source of G).e & v2 = (the Target of G).e or v2 = (the
Source of G).e & v1 = (the Target of G).e;
v1 = vs.x by A20,A21,FINSEQ_4:15;
hence y in G-VSet rng c by A19,A25,A24;
end;
suppose
A26: x=len c+1;
set l = len c;
A27: rng c c= the carrier' of G by FINSEQ_1:def 4;
0+1=1;
then
A28: 1<=l by A1,NAT_1:13;
then l in dom c by FINSEQ_3:25;
then c.l in rng c by FUNCT_1:def 3;
then reconsider e = c.l as Element of the carrier' of G by A27;
set v2 = vs/.(l+1);
set v1 = vs/.l;
l in dom c by A28,FINSEQ_3:25;
then
A29: e in rng c by FUNCT_1:def 3;
c.l joins v1, v2 by A2,A28;
then
A30: v1 = (the Source of G).e & v2 = (the Target of G).e or v2 = (the
Source of G).e & v1 = (the Target of G).e;
v2 = vs.(l+1) by A3,A20,A26,FINSEQ_4:15;
hence y in G-VSet rng c by A19,A26,A30,A29;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th32:
<*v*> is_vertex_seq_of {}
by FINSEQ_1:40;
theorem Th33:
ex vs st vs is_vertex_seq_of c
proof
consider p such that
A1: len p = len c + 1 and
A2: for n st 1<=n & n<=len p holds p.n in the carrier of G and
A3: for n st 1<=n & n<=len c ex v1,v2 st v1=p.n & v2=p.(n+1) & c.n joins
v1,v2 by GRAPH_1:def 14;
rng p c= the carrier of G
proof
let y be object;
assume y in rng p;
then consider x being object such that
A4: x in dom p and
A5: y = p.x by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A4;
A6: n<=len p by A4,FINSEQ_3:25;
1<=n by A4,FINSEQ_3:25;
hence thesis by A2,A5,A6;
end;
then reconsider p as FinSequence of the carrier of G by FINSEQ_1:def 4;
take p;
thus len p = len c + 1 by A1;
let n be Nat;
assume that
A7: 1<=n and
A8: n<=len c;
A9: n<=len p by A1,A8,NAT_1:12;
1<=n+1 by NAT_1:12;
then
A10: p/.(n+1)=p.(n+1) by A1,A8,FINSEQ_4:15,XREAL_1:7;
ex v1,v2 st v1=p.n & v2=p.(n+1) & c.n joins v1,v2 by A3,A7,A8;
hence thesis by A7,A9,A10,FINSEQ_4:15;
end;
theorem Th34:
c <>{} & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & vs1
<> vs2 implies vs1.1<>vs2.1 & for vs st vs is_vertex_seq_of c holds vs = vs1 or
vs = vs2
proof
assume that
A1: c <>{} and
A2: vs1 is_vertex_seq_of c and
A3: vs2 is_vertex_seq_of c;
A4: len vs1 = len c +1 by A2;
defpred P[Nat] means $1 in dom vs1 & vs1.$1<>vs2.$1;
set TG = the Target of G;
set SG = the Source of G;
A5: Seg len vs1 = dom vs1 by FINSEQ_1:def 3;
A6: Seg len vs2 = dom vs2 by FINSEQ_1:def 3;
A7: len vs2 = len c +1 by A3;
assume vs1 <> vs2;
then
A8: ex j being Nat st P[j] by A4,A7,FINSEQ_2:9;
consider k be Nat such that
A9: P[k] and
A10: for n be Nat st P[n] holds k<=n from NAT_1:sch 5 (A8);
A11: 1<=k by A9,FINSEQ_3:25;
per cases by A11,XXREAL_0:1;
suppose
A12: k=1;
hence vs1.1 <> vs2.1 by A9;
set v21 = vs2/.1;
set v12 = vs1/.(1+1);
set v11 = vs1/.1;
let vs;
set v1 = vs/.1;
set v2 = vs/.(1+1);
assume
A13: vs is_vertex_seq_of c;
then
A14: len vs = len c +1;
0+1=1;
then
A15: 1<=len c by A1,NAT_1:13;
then
A16: c.1 joins vs/.1, vs/.(1+1) by A13;
c.1 joins vs1/.1, vs1/.(1+1) by A2,A15;
then
A17: v1=v11 & v2=v12 or v1=v12 & v2=v11 by A16;
A18: 1<=len vs1 by A4,NAT_1:12;
then
A19: v11=vs1.1 by FINSEQ_4:15;
A20: v21=vs2.1 by A4,A7,A18,FINSEQ_4:15;
A21: c.1 joins vs2/.1, vs2/.(1+1) by A3,A15;
thus vs = vs1 or vs = vs2
proof
per cases by A9,A12,A19,A20,A16,A21,A17;
suppose
A22: v1 = v11;
now
defpred P[Nat] means $1 in dom vs implies vs.$1=vs1.$1;
thus len vs = len vs;
thus len vs1 = len vs by A4,A13;
A23: for i being Nat st P[i] holds P[i+1]
proof
A24: 0+1=1;
let i be Nat;
assume
A25: i in dom vs implies vs.i=vs1.i;
assume
A26: i+1 in dom vs;
reconsider i as Element of NAT by ORDINAL1:def 12;
A27: 1<=i+1 by A26,FINSEQ_3:25;
A28: i+1<=len vs by A26,FINSEQ_3:25;
per cases by A24,NAT_1:13;
suppose
i=0;
hence thesis by A4,A14,A18,A19,A22,FINSEQ_4:15;
end;
suppose
A29: 1<=i;
set v12 = vs1/.(i+1);
set v11 = vs1/.i;
set v2 = vs/.(i+1);
A30: v2=vs.(i+1) by A27,A28,FINSEQ_4:15;
set v1 = vs/.i;
A31: i<=len c by A14,A28,XREAL_1:6;
then
A32: c.i joins vs1/.i, vs1/.(i+1) by A2,A29;
A33: i<=len vs by A14,A31,NAT_1:12;
then
A34: v1 =vs.i by A29,FINSEQ_4:15;
c.i joins vs/.i, vs/.(i+1) by A13,A29,A31;
then
A35: v1=v11 & v2=v12 or v1=v12 & v2=v11 by A32;
v11=vs1.i by A4,A14,A29,A33,FINSEQ_4:15;
hence thesis by A4,A14,A25,A27,A28,A29,A33,A34,A30,A35,
FINSEQ_3:25,FINSEQ_4:15;
end;
end;
A36: P[0] by FINSEQ_3:25;
thus for i being Nat holds P[i] from NAT_1:sch 2(A36, A23);
end;
hence thesis by FINSEQ_2:9;
end;
suppose
A37: v1 = v21;
now
defpred P[Nat] means $1 in dom vs implies vs.$1=vs2.$1;
thus len vs = len vs;
thus len vs2 = len vs by A7,A13;
A38: for i being Nat st P[i] holds P[i+1]
proof
A39: 0+1=1;
let i be Nat;
assume
A40: i in dom vs implies vs.i=vs2.i;
assume
A41: i+1 in dom vs;
then
A42: 1<=i+1 by FINSEQ_3:25;
A43: i+1<=len vs by A41,FINSEQ_3:25;
reconsider i as Element of NAT by ORDINAL1:def 12;
per cases by A39,NAT_1:13;
suppose
i=0;
hence thesis by A4,A14,A18,A20,A37,FINSEQ_4:15;
end;
suppose
A44: 1<=i;
set v12 = vs2/.(i+1);
set v11 = vs2/.i;
set v2 = vs/.(i+1);
A45: v2=vs.(i+1) by A42,A43,FINSEQ_4:15;
set v1 = vs/.i;
A46: i<=len c by A14,A43,XREAL_1:6;
then
A47: c.i joins vs2/.i, vs2/.(i+1) by A3,A44;
A48: i<=len vs by A14,A46,NAT_1:12;
then
A49: v1 =vs.i by A44,FINSEQ_4:15;
c.i joins vs/.i, vs/.(i+1) by A13,A44,A46;
then
A50: v1=v11 & v2=v12 or v1=v12 & v2=v11 by A47;
v11=vs2.i by A7,A14,A44,A48,FINSEQ_4:15;
hence thesis by A7,A14,A40,A42,A43,A44,A48,A49,A45,A50,
FINSEQ_3:25,FINSEQ_4:15;
end;
end;
A51: P[0] by FINSEQ_3:25;
thus for i being Nat holds P[i] from NAT_1:sch 2(A51, A38);
end;
hence thesis by FINSEQ_2:9;
end;
end;
end;
suppose
1=1 & card (G-VSet rng c)
= 2 & for n st n in dom c holds (the Source of G).(c.n) <> (the Target of G).(c
.n);
end;
theorem Th35:
c alternates_vertices_in G & vs is_vertex_seq_of c implies for k
st k in dom c holds vs.k <> vs.(k+1)
proof
assume that
A1: c alternates_vertices_in G and
A2: vs is_vertex_seq_of c;
set TG = (the Target of G);
set SG = (the Source of G);
let k;
set px = vs/.k;
set px1 = vs/.(k+1);
assume
A3: k in dom c;
then
A4: k<=len c by FINSEQ_3:25;
A5: 1<=k by A3,FINSEQ_3:25;
then c.k joins px, px1 by A2,A4;
then
A6: TG.(c.k)=px1 & SG.(c.k)=px or TG.(c.k)=px & SG.(c.k)=px1;
A7: len vs = len c +1 by A2;
then k<=len vs by A4,NAT_1:12;
then
A8: px = vs.k by A5,FINSEQ_4:15;
1<=k+1 by NAT_1:12;
then px1 = vs.(k+1) by A4,A7,FINSEQ_4:15,XREAL_1:7;
hence thesis by A1,A3,A8,A6;
end;
theorem Th36:
c alternates_vertices_in G & vs is_vertex_seq_of c implies rng
vs = {(the Source of G).(c.1), (the Target of G).(c.1)}
proof
assume that
A1: c alternates_vertices_in G and
A2: vs is_vertex_seq_of c;
set px1 = vs/.(1+1);
set TG = (the Target of G);
set SG = (the Source of G);
set px = vs/.1;
A3: len vs = len c +1 by A2;
then
A4: 1<=len vs by NAT_1:12;
then
A5: px = vs.1 by FINSEQ_4:15;
c <>{} by A1;
then G-VSet rng c = rng vs by A2,Th31;
then card rng vs = 2 by A1;
then consider x, y being object such that
x<>y and
A6: rng vs={x,y} by CARD_2:60;
1 in dom vs by A4,FINSEQ_3:25;
then vs.1 in rng vs by FUNCT_1:def 3;
then
A7: vs.1 = x or vs.1 = y by A6,TARSKI:def 2;
A8: 1<=len c by A1;
then
A9: 1 in dom c by FINSEQ_3:25;
A10: px1 = vs.(1+1) by A8,A3,FINSEQ_4:15,XREAL_1:7;
c.1 joins px, px1 by A2,A8;
then
A11: TG.(c.1)=px1 & SG.(c.1)=px or TG.(c.1)=px & SG.(c.1)=px1;
1+1<=len vs by A8,A3,XREAL_1:7;
then 1+1 in dom vs by FINSEQ_3:25;
then vs.(1+1) in rng vs by FUNCT_1:def 3;
then vs.(1+1) = x or vs.(1+1) = y by A6,TARSKI:def 2;
hence thesis by A1,A6,A5,A10,A11,A7,A9;
end;
theorem Th37:
c alternates_vertices_in G & vs is_vertex_seq_of c implies vs is
TwoValued Alternating FinSequence
proof
assume that
A1: c alternates_vertices_in G and
A2: vs is_vertex_seq_of c;
A3: c <>{} by A1;
A4: len vs = len c + 1 by A2;
A5: now
let k be Nat;
assume that
A6: 1<=k and
A7: (k+1)<=len vs;
k<=len c by A4,A7,XREAL_1:6;
then k in dom c by A6,FINSEQ_3:25;
hence vs.k <> vs.(k+1) by A1,A2,Th35;
end;
card (G-VSet rng c) = 2 by A1;
then card rng vs = 2 by A2,A3,Th31;
hence thesis by A5,Def3,Def4;
end;
theorem Th38:
c alternates_vertices_in G implies ex vs1,vs2 st vs1<>vs2 & vs1
is_vertex_seq_of c & vs2 is_vertex_seq_of c & for vs st vs is_vertex_seq_of c
holds vs=vs1 or vs=vs2
proof
set X = (the Source of G).(c.1);
set Y = (the Target of G).(c.1);
consider p1 being FinSequence of the carrier of G such that
A1: p1 is_vertex_seq_of c by Th33;
assume
A2: c alternates_vertices_in G;
then
A3: 1<=len c;
then
A4: 1 in dom c by FINSEQ_3:25;
A5: 1+1=2;
then
A6: p1.1 <> p1.2 by A2,A1,A4,Th35;
A7: rng p1 = {X, Y} by A2,A1,Th36;
A8: len p1 = len c + 1 by A1;
then
A9: len p1 > 1 by A3,NAT_1:13;
then consider p2 being TwoValued Alternating FinSequence such that
A10: rng p2 = {p1.2, p1.1} and
A11: len p2 = len p1 and
A12: p2.1=p1.2 by A6,Th23;
A13: dom p1 = dom p2 by A11,FINSEQ_3:29;
1+1<=len p1 by A9,NAT_1:13;
then 2 in dom p1 by FINSEQ_3:25;
then p1.2 in rng p1 by FUNCT_1:def 3;
then
A14: p1.2 = X or p1.2 = Y by A7,TARSKI:def 2;
1 in dom p1 by A9,FINSEQ_3:25;
then p1.1 in rng p1 by FUNCT_1:def 3;
then
A15: p1.1 = X or p1.1 = Y by A7,TARSKI:def 2;
then reconsider p2 as FinSequence of the carrier of G by A2,A1,A7,A4,A5,A10
,A14,Th35,FINSEQ_1:def 4;
take p1, p2;
thus p1<>p2 by A2,A1,A4,A5,A12,Th35;
thus p1 is_vertex_seq_of c by A1;
A16: p1 is TwoValued Alternating FinSequence by A2,A1,Th37;
now
thus len p2 = len c + 1 by A1,A11;
let n be Nat such that
A17: 1<=n and
A18: n<=len c;
A19: n<=len p1 by A8,A18,NAT_1:12;
then
A20: p2/.n = p2.n by A11,A17,FINSEQ_4:15;
A21: n in dom p1 by A17,A19,FINSEQ_3:25;
then p2.n in {X, Y} by A2,A1,A4,A5,A10,A13,A15,A14,Th35,FUNCT_1:def 3;
then
A22: p2.n=X or p2.n=Y by TARSKI:def 2;
set x = p1/.n;
set y = p1/.(n+1);
A23: c.n joins x, y by A1,A17,A18;
A24: n+1<=len p1 by A8,A18,XREAL_1:6;
then
A25: p2/.(n+1) = p2.(n+1) by A11,FINSEQ_4:15,NAT_1:12;
A26: 1<=n+1 by NAT_1:12;
then
A27: n+1 in dom p1 by A24,FINSEQ_3:25;
then p2.(n+1) in {X, Y} by A2,A1,A4,A5,A10,A13,A15,A14,Th35,FUNCT_1:def 3;
then
A28: p2.(n+1)=X or p2.(n+1)=Y by TARSKI:def 2;
p1.n in {X, Y} by A7,A21,FUNCT_1:def 3;
then p1.n=X or p1.n=Y by TARSKI:def 2;
then
A29: x = p2.(n+1) by A7,A16,A6,A10,A11,A12,A15,A14,A17,A19,A24,A22,A28,Def4
,Th21,FINSEQ_4:15;
p1.(n+1) in {X, Y} by A7,A27,FUNCT_1:def 3;
then p1.(n+1)=X or p1.(n+1)=Y by TARSKI:def 2;
then y = p2.n by A7,A16,A6,A10,A11,A12,A15,A14,A17,A26,A24,A22,A28,Def4
,Th21,FINSEQ_4:15;
hence c.n joins p2/.n,p2/.(n+1) by A23,A29,A20,A25;
end;
hence p2 is_vertex_seq_of c;
let p be FinSequence of the carrier of G;
assume
A30: p is_vertex_seq_of c;
then reconsider p9 = p as TwoValued Alternating FinSequence by A2,Th37;
A31: len p = len c + 1 by A30;
rng p = {X, Y} by A2,A30,Th36;
then p9=p1 or p9=p2 by A8,A7,A16,A6,A10,A11,A12,A15,A14,A31,Th22;
hence thesis;
end;
Lm7: (for x, y st x in D & y in D holds x=y) implies card D = 1
proof
set x = the Element of D;
assume for x, y st x in D & y in D holds x=y;
then for y be object holds y in D iff y=x;
then D = {x} by TARSKI:def 1;
hence thesis by CARD_2:42;
end;
theorem Th39:
vs is_vertex_seq_of c implies (card the carrier of G = 1 or c <>
{} & not c alternates_vertices_in G iff for vs1 st vs1 is_vertex_seq_of c holds
vs1 = vs)
proof
assume
A1: vs is_vertex_seq_of c;
hereby
assume
A2: card the carrier of G = 1 or c <>{} & not c alternates_vertices_in G;
per cases by A2;
suppose
A3: card the carrier of G = 1;
then reconsider tVG = the carrier of G as finite set;
consider X being object such that
A4: tVG = {X} by A3,CARD_2:42;
A5: rng vs c= {X} by A4,FINSEQ_1:def 4;
A6: len vs = len c +1 by A1;
let vs1;
A7: Seg len vs = dom vs by FINSEQ_1:def 3;
assume vs1 is_vertex_seq_of c;
then
A8: len vs1 = len c +1;
assume vs1 <> vs;
then consider j being Nat such that
A9: j in dom vs and
A10: vs1.j <> vs.j by A8,A6,FINSEQ_2:9;
vs.j in rng vs by A9,FUNCT_1:def 3;
then
A11: vs.j = X by A5,TARSKI:def 1;
A12: rng vs1 c= {X} by A4,FINSEQ_1:def 4;
Seg len vs1 = dom vs1 by FINSEQ_1:def 3;
then vs1.j in rng vs1 by A8,A6,A7,A9,FUNCT_1:def 3;
hence contradiction by A10,A12,A11,TARSKI:def 1;
end;
suppose
A13: c <>{} & not c alternates_vertices_in G;
thus for vs1 st vs1 is_vertex_seq_of c holds vs1 = vs
proof
set TG = the Target of G;
set SG = the Source of G;
let vs1;
defpred P[Nat] means $1 in dom vs1 & vs1.$1<>vs.$1;
assume
A14: vs1 is_vertex_seq_of c;
then
A15: len vs1 = len c +1;
A16: len vs = len c +1 by A1;
then
A17: dom vs1 = dom vs by A15,FINSEQ_3:29;
assume vs1 <> vs;
then
A18: ex i being Nat st P[i] by A15,A16,FINSEQ_2:9;
consider k be Nat such that
A19: P[k] and
A20: for n be Nat st P[n] holds k<=n from NAT_1:sch 5 (A18);
A21: 0+1=1 & k=0 or 0+1<=k by NAT_1:13;
per cases by A21,XXREAL_0:1;
suppose
k=0;
hence contradiction by A19,FINSEQ_3:25;
end;
suppose
A22: k=1;
thus contradiction
proof
A23: 0+1=1;
per cases by A23,NAT_1:13;
suppose
len c = 0;
hence contradiction by A13;
end;
suppose
A24: 1<=len c;
defpred P[Nat] means
$1 in dom c implies vs1/.$1<>vs
/.$1 & vs1/.($1+1)<>vs/.($1+1) & (TG.(c.$1)=TG.(c.1) & SG.(c.$1)=SG.(c.1) or TG
.(c.$1)=SG.(c.1) & SG.(c.$1)=TG.(c.1));
A25: vs/.k=vs.k by A17,A19,PARTFUN1:def 6;
A26: vs1/.k=vs1.k by A19,PARTFUN1:def 6;
A27: now
let n be Nat;
assume
A28: P[n];
thus P[n+1]
proof
assume
A29: (n+1) in dom c;
then
A30: 1<=n+1 by FINSEQ_3:25;
A31: n+1<=len c by A29,FINSEQ_3:25;
thus vs1/.(n+1)<>vs/.(n+1) & vs1/.(n+1+1)<>vs/.(n+1+1) & (TG
.(c.(n+1))=TG.(c.1) & SG.(c.(n+1))=SG.(c.1) or TG.(c.(n+1))=SG.(c.1) & SG.(c.(n
+1))=TG.(c.1))
proof
per cases;
suppose
A32: n=0;
hence vs1/.(n+1)<>vs/.(n+1) by A17,A19,A22,A26,
PARTFUN1:def 6;
A33: 1<=len c by A30,A31,XXREAL_0:2;
then c.1 joins vs/.1,vs/.(1+1) by A1;
then
A34: SG.(c.1)=vs/.1 & TG.(c.1)=vs/.(1+1) or SG.(c.1)=vs
/.(1+1) & TG.(c.1)= vs/.1;
c.1 joins vs1/.1,vs1/.(1+1) by A14,A33;
then
SG.(c.1)=vs1/.1 & TG.(c.1)= vs1/.(1+1) or SG.(c.1)=
vs1/.(1+1) & TG.(c. 1)=vs1/.1;
hence vs1/.(n+1+1)<>vs/.(n+1+1) by A17,A19,A22,A26,A32
,A34,PARTFUN1:def 6;
thus thesis by A32;
end;
suppose
A35: 0 vs/.(n+1) by A28,A36,FINSEQ_3:25;
c.n joins vs1/.n, vs1/.(n+1) by A14,A37,A36;
then
A38: SG.(c.n)=vs1/.n & TG.(c.n)= vs1/.(n+1) or SG.(c.n)=
vs1/.(n+1) & TG.(c. n)=vs1/.n;
c.(n+1) joins vs/.(n+1), vs/.(n+1+1) by A1,A30,A31;
then
A39: SG.(c.(n+1))=vs/.(n+1) & TG.(c.(n+1))=vs/.(n+1+1)
or SG.(c.(n+1))=vs/. (n+1+1) & TG.(c.(n+1))=vs/.(n+1);
A40: c.(n+1) joins vs1/.(n+1), vs1/.(n+1+1) by A14,A30,A31;
then
SG.(c.(n+1))=vs1/.(n+1) & TG. (c.(n+1))=vs1/.(n+1+1
) or SG.(c.(n+1))= vs1/.(n+1+1) & TG.(c.(n+1))=vs1/.(n+1);
hence vs1/.(n+1+1)<>vs/.(n+1+1) by A28,A37,A36,A39,
FINSEQ_3:25;
c.n joins vs/.n, vs/.(n+1) by A1,A37,A36;
hence thesis by A28,A37,A36,A38,A40,A39,FINSEQ_3:25;
end;
end;
end;
end;
A41: P[0] by FINSEQ_3:25;
A42: for n being Nat holds P[n] from NAT_1:sch 2(A41,A27);
now
let x be object;
hereby
assume x in G-VSet rng c;
then consider v such that
A43: x=v and
A44: ex e being Element of the carrier' of G st e in rng
c & (v = (the Source of G).e or v = (the Target of G).e);
consider e such that
A45: e in rng c and
A46: v = SG.e or v = TG.e by A44;
consider d being object such that
A47: d in dom c and
A48: e=c.d by A45,FUNCT_1:def 3;
reconsider d as Element of NAT by A47;
TG.(c.d)=TG.(c.1) & SG.(c.d)=SG.(c.1) or TG.(c.d)=SG.(c
.1) & SG.(c.d)=TG.(c.1) by A42,A47;
hence x in {SG.(c.1), TG.(c.1)} by A43,A46,A48,TARSKI:def 2;
end;
0+1<=len c by A13,NAT_1:13;
then
A49: 1 in dom c by FINSEQ_3:25;
then
A50: c.1 in rng c by FUNCT_1:def 3;
A51: rng c c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e=c.1 as Element of the carrier' of G by A50;
reconsider t = TG.e as Element of G by A50,A51,FUNCT_2:5;
reconsider s = SG.e as Element of G by A50,A51,FUNCT_2:5;
assume x in {SG.(c.1), TG.(c.1)};
then
A52: x=s or x =t by TARSKI:def 2;
e in rng c by A49,FUNCT_1:def 3;
hence x in G-VSet rng c by A52;
end;
then
A53: G-VSet rng c = {SG.(c.1), TG.(c.1)} by TARSKI:2;
c.k joins vs1/.k, vs1/.(k+1) by A14,A22,A24;
then
A54: SG.(c.1)=vs1/.1 & TG.(c.1)=vs1/.(k+1) or SG.(c.1)=vs1/.(k+1
) & TG.(c.1 )=vs1/.1 by A22;
A55: c.k joins vs/.k, vs/.(k+1) by A1,A22,A24;
A56: now
let n;
n in dom c implies TG.(c.n)=TG.(c.1) & SG.(c.n)=SG.(c.1)
or TG.(c.n)=SG.(c.1) & SG.(c.n)=TG.(c.1) by A42;
hence n in dom c implies SG.(c.n) <> TG.(c.n) by A19,A22,A26
,A25,A55,A54;
end;
SG.(c.1)=vs/.1 & TG.(c.1)=vs/.(k+1) or SG.(c.1)=vs/.(k+1) &
TG.(c.1)= vs/.1 by A22,A55;
then card (G-VSet rng c) = 2 by A19,A22,A26,A25,A54,A53,CARD_2:57
;
hence contradiction by A13,A24,A56;
end;
end;
end;
suppose
1 1;
then consider x, y such that
A70: x in the carrier of G and
A71: y in the carrier of G and
A72: x<>y by Lm7;
reconsider y as Element of G by A71;
reconsider x as Element of G by A70;
assume
A73: c ={} or c alternates_vertices_in G;
thus contradiction
proof
per cases by A73;
suppose
A74: c ={};
then <*x*> = vs by A69,Th32;
then
A75: vs.1 = x by FINSEQ_1:40;
<*y*> = vs by A69,A74,Th32;
hence contradiction by A72,A75,FINSEQ_1:40;
end;
suppose
c alternates_vertices_in G;
then consider vs1,vs2 such that
A76: vs1<>vs2 and
A77: vs1 is_vertex_seq_of c and
A78: vs2 is_vertex_seq_of c and
for vs st vs is_vertex_seq_of c holds vs=vs1 or vs=vs2 by Th38;
vs1 = vs by A69,A77;
hence contradiction by A69,A76,A78;
end;
end;
end;
definition
let G, c;
assume
A1: card the carrier of G = 1 or c <>{} & not c alternates_vertices_in G;
func vertex-seq c -> FinSequence of the carrier of G means
it is_vertex_seq_of c;
existence by Th33;
uniqueness by A1,Th39;
end;
theorem Th40:
vs is_vertex_seq_of c & c1 = c|Seg n & vs1= vs|Seg (n+1) implies
vs1 is_vertex_seq_of c1
proof
assume
A1: vs is_vertex_seq_of c;
then
A2: len vs = len c + 1;
assume that
A3: c1 = c|Seg n and
A4: vs1= vs|Seg (n+1);
now
per cases;
suppose
A5: n<=len c;
then
A6: n+1<=len vs by A2,XREAL_1:6;
then
A7: len vs1 = n+1 by A4,FINSEQ_1:17;
A8: len c1 = n by A3,A5,FINSEQ_1:17;
hence len vs1 = len c1 + 1 by A4,A6,FINSEQ_1:17;
let k be Nat;
assume that
A9: 1<=k and
A10: k<=len c1;
A11: 1<=k+1 by NAT_1:12;
then
A12: vs1/.(k+1)=vs1.(k+1) by A8,A7,A10,FINSEQ_4:15,XREAL_1:7;
k+1<=len c1 +1 by A10,XREAL_1:7;
then k+1 in Seg (n+1) by A8,A11;
then
A13: vs1.(k+1)=vs.(k+1) by A4,FUNCT_1:49;
A14: k<=len c by A5,A8,A10,XXREAL_0:2;
then k<=len vs by A2,NAT_1:12;
then
A15: vs/.k=vs.k by A9,FINSEQ_4:15;
A16: k<=n+1 by A8,A10,NAT_1:12;
then
A17: vs1/.k=vs1.k by A7,A9,FINSEQ_4:15;
k in Seg n by A8,A9,A10;
then
A18: c1.k = c.k by A3,FUNCT_1:49;
k in Seg (n+1) by A9,A16;
then
A19: vs1.k=vs.k by A4,FUNCT_1:49;
vs/.(k+1)=vs.(k+1) by A2,A14,A11,FINSEQ_4:15,XREAL_1:7;
hence c1.k joins vs1/.k,vs1/.(k+1) by A1,A9,A14,A18,A19,A13,A15,A17,A12;
end;
suppose
A20: len c <=n;
then len vs<=n+1 by A2,XREAL_1:6;
then
A21: vs1 = vs by A4,FINSEQ_2:20;
c1 = c by A3,A20,FINSEQ_2:20;
hence len vs1 = len c1 + 1 & for k being Nat st 1<=k & k<=len
c1 holds c1.k joins vs1/.k,vs1/.(k+1) by A1,A21;
end;
end;
hence thesis;
end;
theorem Th41:
1<=m & m<=n & n<=len c & q = (m,n)-cut c implies q is Chain of G
proof
assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len c;
A4: m<=n+1 by A2,NAT_1:12;
consider vs such that
A5: vs is_vertex_seq_of c by Th33;
set p9 = (m,n+1)-cut vs;
A6: now
let k be Nat;
assume that
A7: 1<=k and
A8: k<=len p9;
k in dom p9 by A7,A8,FINSEQ_3:25;
then
A9: p9.k in rng p9 by FUNCT_1:def 3;
A10: rng vs c= the carrier of G by FINSEQ_1:def 4;
rng p9 c= rng vs by Th11;
then p9.k in rng vs by A9;
hence p9.k in the carrier of G by A10;
end;
assume
A11: q = (m,n)-cut c;
then
A12: len q +m-m=n+1-m by A1,A3,A4,Lm2;
A13: len vs = len c + 1 by A5;
then
A14: n+1<=len vs by A3,XREAL_1:6;
then
A15: len p9+m-m=(n+1)+1-m by A1,A4,Def1;
then
A16: len p9 = n-m+1+1;
A17: now
1-1<=m-1 by A1,XREAL_1:9;
then m-1 = m-'1 by XREAL_0:def 2;
then reconsider m1= m-1 as Element of NAT;
let k be Nat;
reconsider i = m1+k as Nat;
assume that
A18: 1<=k and
A19: k<=len q;
0+1<=k by A18;
then consider j such that
0<=j and
A20: j {};
then
A5: len p +1 = len vs1 +len vs2 by Th13;
A6: now
let n be Nat such that
A7: 1<=n and
A8: n<=len p;
per cases;
suppose
A9: n<=len vs1;
then
A10: n in dom vs1 by A7,FINSEQ_3:25;
p.n = vs1.n by A7,A9,Th14;
hence p.n in the carrier of G by A10,FINSEQ_2:11;
end;
suppose
A11: n > len vs1;
then consider m being Nat such that
A12: n = len vs1 + m by NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
m <> 0 by A11,A12;
then
A13: 0+1<=m by NAT_1:13;
len vs1 + m<=len vs1 + (len vs2 - 1) by A5,A8,A12;
then m<=len vs2 - 1 by XREAL_1:6;
then
A14: m+1<=len vs2 - 1+1 by XREAL_1:6;
1<=m+1 by NAT_1:12;
then
A15: m+1 in dom vs2 by A14,FINSEQ_3:25;
m {};
then len p +1 = len vs1 +len vs2 by Th13;
then
A8: len p = len c1 + len c2 + 1 by A6,A7
.= len q + 1 by FINSEQ_1:22;
reconsider p as FinSequence of the carrier of G;
now
let n be Nat;
assume that
A9: 1<=n and
A10: n<=len q;
A11: n in dom q by A9,A10,FINSEQ_3:25;
n<=len p by A8,A10,NAT_1:12;
then
A12: p/.n=p.n by A9,FINSEQ_4:15;
1<=n+1 by NAT_1:12;
then
A13: p/.(n+1)=p.(n+1) by A8,A10,FINSEQ_4:15,XREAL_1:7;
per cases by A11,FINSEQ_1:25;
suppose
A14: n in dom c1;
set v2=vs1/.(n+1);
set v1=vs1/.n;
A15: 1<=n by A14,FINSEQ_3:25;
A16: n<=len c1 by A14,FINSEQ_3:25;
then n+1<=len c1+1 by XREAL_1:6;
then
A17: n+1<=len vs1 by A1;
then
A18: vs1/.(n+1)=vs1.(n+1) by FINSEQ_4:15,NAT_1:12;
A19: n<=len vs1 by A6,A16,NAT_1:12;
then
A20: vs1/.n=vs1.n by A15,FINSEQ_4:15;
A21: p.(n+1) = vs1.(n+1) by A17,Th14,NAT_1:12;
A22: p.n = vs1.n by A15,A19,Th14;
c1.n joins v1, v2 by A1,A15,A16;
hence q.n joins p/.n, p/.(n+1) by A12,A13,A14,A20,A18,A22,A21,
FINSEQ_1:def 7;
end;
suppose
ex k being Nat st k in dom c2 & n=len c1 + k;
then consider k being Element of NAT such that
A23: k in dom c2 and
A24: n = len c1 + k;
A25: 0+1<=k by A23,FINSEQ_3:25;
set v2 = vs2/.(k+1);
set v1 = vs2/.k;
A26: k<=len c2 by A23,FINSEQ_3:25;
then
A27: k is_vertex_seq_of {}
by FINSEQ_1:39;
definition
let G;
let IT be Chain of G;
attr IT is simple means
:Def9:
ex vs st vs is_vertex_seq_of IT & for n,m st
1<=n & n as FinSequence of the carrier of G;
take p;
thus p is_vertex_seq_of q by Lm8;
let n,m;
assume that
A1: 1<=n and
A2: nvs2.$1;
set TG = the Target of G;
set SG = the Source of G;
A5: Seg len vs1 = dom vs1 by FINSEQ_1:def 3;
A6: Seg len vs2 = dom vs2 by FINSEQ_1:def 3;
A7: len vs2 = len sc +1 by A3;
assume
A8: vs1 <> vs2;
then
A9: ex j being Nat st P[j] by A4,A7,FINSEQ_2:9;
consider k be Nat such that
A10: P[k] and
A11: for n be Nat st P[n] holds k<=n from NAT_1:sch 5 (A9);
A12: 1<=k by A10,FINSEQ_3:25;
per cases by A12,XXREAL_0:1;
suppose
A13: k=1;
set v23=vs2/.(1+1+1);
set v22=vs2/.(1+1);
set v21=vs2/.1;
set v13=vs1/.(1+1+1);
set v12=vs1/.(1+1);
set v11=vs1/.1;
A14: 1+1+1<=len vs1 by A1,A4,XREAL_1:6;
then
A15: v13=vs1.(1+1+1) by FINSEQ_4:15;
A16: 1<=len vs1 by A14,XXREAL_0:2;
then
A17: v11=vs1.1 by FINSEQ_4:15;
A18: 1<=len sc by A1,XXREAL_0:2;
then
A19: sc.1 joins v21,v22 by A3;
sc.1 joins v11,v12 by A2,A18;
then
A20: v11=v21 & v12=v22 or v11=v22 & v12=v21 by A19;
A21: v21=vs2.1 by A4,A7,A16,FINSEQ_4:15;
consider vs such that
A22: vs is_vertex_seq_of sc and
A23: for n,m st 1<=n & n{} by A1;
then
A24: vs = vs1 or vs = vs2 by A2,A3,A8,A22,Th34;
A25: v23=vs2.(1+1+1) by A4,A7,A14,FINSEQ_4:15;
A26: sc.2 joins v22,v23 by A1,A3;
A27: sc.2 joins v12,v13 by A1,A2;
then
A28: v21=v23 by A10,A13,A17,A21,A26,A20;
v11=v13 by A10,A13,A17,A21,A27,A26,A20;
then 1+1+1 = len vs by A4,A7,A14,A17,A15,A21,A25,A28,A23,A24;
hence contradiction by A1,A4,A7,A24;
end;
suppose
1.
:: ^ |
:: | v
:: .--->.<---.--->.
:: | ^
:: v |
:: .--->.
:: is a case in point:
theorem Th48:
not c is simple Chain of G & vs is_vertex_seq_of c implies ex fc
being Subset of c, fvs being Subset of vs, c1, vs1 st len c1 < len c & vs1
is_vertex_seq_of c1 & len vs1 < len vs & vs.1 = vs1.1 & vs.len vs = vs1.len vs1
& Seq fc = c1 & Seq fvs = vs1
proof
assume that
A1: not c is simple Chain of G and
A2: vs is_vertex_seq_of c;
consider n, m being Nat such that
A3: 1<=n and
A4: n1 or m<>len vs by A1,A2,Def9;
A8: m-n>n-n by A4,XREAL_1:9;
A9: len vs = len c + 1 by A2;
reconsider n1 = n-'1 as Element of NAT;
A10: 1-1<=n-1 by A3,XREAL_1:9;
then
A11: n-1 = n-'1 by XREAL_0:def 2;
then
A12: n1+1 = n;
per cases by A7;
suppose
A13: n<>1 & m <> len vs;
set DR = {kk where kk is Nat: m<=kk & kk<= len c};
set DL = {kk where kk is Nat: 1<=kk & kk<=n1};
set domfvs = {k where k is Nat: 1<=k & k<=n or m+1<=k & k<= len vs};
reconsider p2 = (m,len c+1)-cut vs as FinSequence of the carrier of G;
reconsider pp = (1,n)-cut vs as FinSequence of the carrier of G;
set p29 = (m+1, len c +1)-cut vs;
A14: 1<=m+1 by NAT_1:12;
A15: 1<=m by A3,A4,XXREAL_0:2;
then 1-1<=m-1 by XREAL_1:9;
then m-'1 = m-1 by XREAL_0:def 2;
then reconsider m1 = m-1 as Element of NAT;
A16: m < len vs by A5,A13,XXREAL_0:1;
then
A17: m<=len c by A9,NAT_1:13;
then reconsider c2 = (m,len c)-cut c as Chain of G by A15,Th41;
A18: len c2 +m = len c +1 by A15,A17,Def1;
deffunc F(object) = c.$1;
set domfc = {k where k is Nat: 1<=k & k<=n1 or m<=k & k<= len c};
consider fc being Function such that
A19: dom fc = domfc and
A20: for x being object st x in domfc holds fc.x = F(x) from FUNCT_1:sch 3;
n < len vs by A4,A5,XXREAL_0:2;
then
A21: n-1 < len c +1-1 by A9,XREAL_1:9;
domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider kk being Nat such that
A22: x = kk and
A23: 1<=kk & kk<=n1 or m<=kk & kk<= len c;
A24: 1<=kk by A15,A23,XXREAL_0:2;
kk<=len c by A11,A21,A23,XXREAL_0:2;
hence thesis by A22,A24;
end;
then reconsider fc as FinSubsequence by A19,FINSEQ_1:def 12;
A25: fc c= c
proof
let p be object;
assume
A26: p in fc;
then consider x, y being object such that
A27: [x,y] = p by RELAT_1:def 1;
A28: x in dom fc by A26,A27,FUNCT_1:1;
then consider kk being Nat such that
A29: x = kk and
A30: 1<=kk & kk<=n1 or m<=kk & kk<= len c by A19;
A31: 1<=kk by A15,A30,XXREAL_0:2;
kk<=len c by A11,A21,A30,XXREAL_0:2;
then
A32: x in dom c by A29,A31,FINSEQ_3:25;
y = fc.x by A26,A27,FUNCT_1:1;
then y = c.kk by A19,A20,A28,A29;
hence thesis by A27,A29,A32,FUNCT_1:1;
end;
1 < n by A3,A13,XXREAL_0:1;
then 1 + 1<=n by NAT_1:13;
then
A33: 1+1-1<=n-1 by XREAL_1:9;
then reconsider c1 = (1,n1)-cut c as Chain of G by A11,A21,Th41;
reconsider fc as Subset of c by A25;
take fc;
A34: pp is_vertex_seq_of c1 by A2,A12,A33,A21,Th42;
then
A35: len pp = len c1 + 1;
now
let x be object;
hereby
assume x in domfc;
then ex k being Nat st x=k &( 1<=k & k<=n1 or m<=k & k<=
len c);
then x in DL or x in DR;
hence x in DL \/ DR by XBOOLE_0:def 3;
end;
assume
A36: x in DL \/ DR;
per cases by A36,XBOOLE_0:def 3;
suppose
x in DL;
then ex k being Nat st x=k & 1<=k & k<=n1;
hence x in domfc;
end;
suppose
x in DR;
then ex k being Nat st x=k & m<=k & k<=len c;
hence x in domfc;
end;
end;
then
A37: domfc = DL \/ DR by TARSKI:2;
A38: DL c= Seg len c & DR c= Seg len c
proof
hereby
let x be object;
assume x in DL;
then consider k being Nat such that
A39: x=k and
A40: 1<=k and
A41: k<=n1;
k<=len c by A11,A21,A41,XXREAL_0:2;
hence x in Seg len c by A39,A40;
end;
let x be object;
assume x in DR;
then consider k being Nat such that
A42: x=k and
A43: m<=k and
A44: k<=len c;
1<=k by A15,A43,XXREAL_0:2;
hence thesis by A42,A44;
end;
then reconsider DR as finite set;
rng Sgm DR = DR by A38,FINSEQ_1:def 13;
then
A45: rng Sgm DR c= dom fc by A19,A37,XBOOLE_1:7;
reconsider DL as finite set by A38;
set SL = Sgm DL;
A46: 1<=m by A3,A4,XXREAL_0:2;
set SR = Sgm DR;
A47: len Sgm DR = card DR by A38,FINSEQ_3:39;
A48: m<=len c by A9,A16,NAT_1:13;
then
A49: m-m<=len c -m by XREAL_1:9;
then len c2 -'1 = len c2 -1 by A18,XREAL_0:def 2;
then reconsider lc21 = len c2 -1 as Element of NAT;
-(-(m-n)) = m-n;
then
A50: -(m-n) < 0 by A8;
A51: m = m1 +1;
then m1<=m by NAT_1:12;
then
A52: p2 = (m1+1, m)-cut vs ^ (m+1, len c +1)-cut vs by A5,A9,Th8;
A53: p2 is_vertex_seq_of c2 by A2,A15,A17,Th42;
then
A54: len p2 = len c2 + 1;
then 1<=len p2 by NAT_1:12;
then 1-1<=len p2 -1 by XREAL_1:9;
then len p2 -'1 = len p2 -1 by XREAL_0:def 2;
then reconsider lp21 = len p2 -1 as Element of NAT;
0+1=1;
then
A55: 1<=len p2 by A54,NAT_1:13;
m-m<=len c -m by A48,XREAL_1:9;
then 0+1<=len c -m+1 by XREAL_1:6;
then
A56: 1 by A55,Th6
.= <*vs.(m+0)*> by A9,A15,A54,A147,Lm2
.= (m,m)-cut vs by A5,A15,Th6;
then
A209: p1 = pp^p29 by A135,A52,FINSEQ_1:33;
rng Sgm DL = DL by A136,FINSEQ_1:def 13;
then rng Sgm DL c= dom fvs by A88,A144,XBOOLE_1:7;
hence thesis by A88,A209,A144,A208,A145,A175,A202,Th24;
end;
suppose
A210: n=1 & m <> len vs;
set domfvs = {k where k is Nat: m<=k & k<= len vs};
deffunc F(object) = c.$1;
set domfc = {k where k is Nat: m<=k & k<= len c};
set p2 = (m,len c+1)-cut vs;
consider fc being Function such that
A211: dom fc = domfc and
A212: for x being object st x in domfc holds fc.x = F(x) from FUNCT_1:sch 3;
A213: 1 < m by A3,A4,XXREAL_0:2;
then 1-1 < m-1 by XREAL_1:9;
then 0 < -(-(m-1));
then
A214: -(m-1) < 0;
1-1<=m-1 by A213,XREAL_1:9;
then m-'1 = m-1 by XREAL_0:def 2;
then reconsider m1 = m-1 as Element of NAT;
A215: m = m1 +1;
domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider kk being Nat such that
A216: x = kk and
A217: m<=kk and
A218: kk<= len c;
1<=kk by A213,A217,XXREAL_0:2;
hence thesis by A216,A218;
end;
then reconsider fc as FinSubsequence by A211,FINSEQ_1:def 12;
fc c= c
proof
let p be object;
assume
A219: p in fc;
then consider x, y being object such that
A220: [x,y] = p by RELAT_1:def 1;
A221: x in dom fc by A219,A220,FUNCT_1:1;
then consider kk being Nat such that
A222: x = kk and
A223: m<=kk and
A224: kk<= len c by A211;
1<=kk by A213,A223,XXREAL_0:2;
then
A225: x in dom c by A222,A224,FINSEQ_3:25;
y = fc.x by A219,A220,FUNCT_1:1;
then y = c.kk by A211,A212,A221,A222;
hence thesis by A220,A222,A225,FUNCT_1:1;
end;
then reconsider fc as Subset of c;
take fc;
deffunc F(object) = vs.$1;
consider fvs being Function such that
A226: dom fvs = domfvs and
A227: for x being object st x in domfvs holds fvs.x = F(x) from FUNCT_1:sch 3;
domfvs c= Seg len vs
proof
let x be object;
assume x in domfvs;
then consider kk being Nat such that
A228: x = kk and
A229: m<=kk and
A230: kk<= len vs;
1<=kk by A213,A229,XXREAL_0:2;
hence thesis by A228,A230;
end;
then reconsider fvs as FinSubsequence by A226,FINSEQ_1:def 12;
A231: fvs c= vs
proof
let p be object;
assume
A232: p in fvs;
then consider x, y being object such that
A233: [x,y] = p by RELAT_1:def 1;
A234: x in dom fvs by A232,A233,FUNCT_1:1;
then consider kk being Nat such that
A235: x = kk and
A236: m<=kk and
A237: kk<= len vs by A226;
1<=kk by A213,A236,XXREAL_0:2;
then
A238: x in dom vs by A235,A237,FINSEQ_3:25;
y = fvs.x by A232,A233,FUNCT_1:1;
then y = vs.kk by A226,A227,A234,A235;
hence thesis by A233,A235,A238,FUNCT_1:1;
end;
A239: m < len vs by A5,A210,XXREAL_0:1;
then
A240: m<=len c by A9,NAT_1:13;
then reconsider c2 = (m,len c)-cut c as Chain of G by A213,Th41;
A241: m<=len c by A9,A239,NAT_1:13;
reconsider fvs as Subset of vs by A231;
take fvs;
take c1 = c2;
take p1 = p2;
A242: len c2 +m = len c +1 by A4,A5,A9,A210,Lm2;
then len c2 = len c +(-m+1);
hence
A243: len c1 < len c by A214,XREAL_1:30;
1<=m by A3,A4,XXREAL_0:2;
hence p1 is_vertex_seq_of c1 by A2,A241,Th42;
p2 is_vertex_seq_of c2 by A2,A240,A213,Th42;
then len p1 = len c1 + 1;
hence len p1 < len vs by A9,A243,XREAL_1:6;
thus vs.1 = p1.1 by A4,A5,A6,A9,A210,Th12;
thus vs.len vs = p1.len p1 by A4,A5,A9,A210,Th12;
A244: domfvs c= Seg len vs
proof
let x be object;
assume x in domfvs;
then consider k being Nat such that
A245: x=k and
A246: m<=k and
A247: k<=len vs;
1<=k by A213,A246,XXREAL_0:2;
hence thesis by A245,A247;
end;
A248: domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider k being Nat such that
A249: x=k and
A250: m<=k and
A251: k<=len c;
1<=k by A213,A250,XXREAL_0:2;
hence thesis by A249,A251;
end;
then reconsider domfc as finite set;
A252: len Sgm domfc = card domfc by A248,FINSEQ_3:39;
reconsider domfvs as finite set by A244;
A253: rng Sgm domfvs c= dom fvs by A226,A244,FINSEQ_1:def 13;
set SR = Sgm domfc;
A254: len c +1<=len vs by A2;
A255: m-m<=len c -m by A240,XREAL_1:9;
then len c2 -'1 = len c2 -1 by A242,XREAL_0:def 2;
then reconsider lc21 = len c2 -1 as Element of NAT;
A256: m+lc21 = m1+len c2;
len c2 -'1 = len c2 -1 by A242,A255,XREAL_0:def 2;
then reconsider lc21 = len c2 -1 as Element of NAT;
m+lc21 = len c by A242;
then
A257: card domfc = len c2 + -1 +1 by Th4
.= len c2;
A258: rng Sgm domfc c= dom fc by A211,A248,FINSEQ_1:def 13;
now
let p be object;
hereby
assume
A259: p in c2;
then consider x, y being object such that
A260: p=[x,y] by RELAT_1:def 1;
A261: y=c2.x by A259,A260,FUNCT_1:1;
A262: x in dom c2 by A259,A260,FUNCT_1:1;
then reconsider k = x as Element of NAT;
A263: k<=len c2 by A262,FINSEQ_3:25;
1<=k by A262,FINSEQ_3:25;
then
A264: m1+k=SR.k by A242,A215,A256,A263,Th5;
0+1<=k by A262,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A265: i1 & m = len vs;
set domfvs = {k where k is Nat: 1<=k & k<=n};
set pp = (1,n)-cut vs;
deffunc F(object) = c.$1;
reconsider domfc = {k where k is Nat: 1<=k & k<=n1} as set;
consider fc being Function such that
A309: dom fc = domfc and
A310: for x being object st x in domfc holds fc.x = F(x) from FUNCT_1:sch 3;
n < len vs by A4,A5,XXREAL_0:2;
then
A311: n-1 < len c +1-1 by A9,XREAL_1:9;
domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider kk being Nat such that
A312: x = kk and
A313: 1<=kk and
A314: kk<=n1;
kk<=len c by A11,A311,A314,XXREAL_0:2;
hence thesis by A312,A313;
end;
then reconsider fc as FinSubsequence by A309,FINSEQ_1:def 12;
1 < n by A3,A308,XXREAL_0:1;
then 1 + 1<=n by NAT_1:13;
then
A315: 1+1-1<=n-1 by XREAL_1:9;
then reconsider c1 = (1,n1)-cut c as Chain of G by A11,A311,Th41;
A316: 1<=n1+1 by NAT_1:12;
then
A317: len c1+1=n1+1 by A11,A311,Lm2;
then
A318: len c1 = n - 1 by A10,XREAL_0:def 2;
A319: fc c= c
proof
let p be object;
assume
A320: p in fc;
then consider x, y being object such that
A321: [x,y] = p by RELAT_1:def 1;
A322: x in dom fc by A320,A321,FUNCT_1:1;
then consider kk being Nat such that
A323: x = kk and
A324: 1<=kk and
A325: kk<=n1 by A309;
kk<=len c by A11,A311,A325,XXREAL_0:2;
then
A326: x in dom c by A323,A324,FINSEQ_3:25;
y = fc.x by A320,A321,FUNCT_1:1;
then y = c.kk by A309,A310,A322,A323;
hence thesis by A321,A323,A326,FUNCT_1:1;
end;
A327: domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider k being Nat such that
A328: x=k and
A329: 1<=k and
A330: k<=n1;
k<=len c by A11,A311,A330,XXREAL_0:2;
hence thesis by A328,A329;
end;
reconsider fc as Subset of c by A319;
take fc;
reconsider domfc as finite set by A327;
set SL = Sgm domfc;
deffunc F(object) = vs.$1;
consider fvs being Function such that
A331: dom fvs = domfvs and
A332: for x being object st x in domfvs holds fvs.x = F(x)
from FUNCT_1:sch 3;
A333: n<=len vs by A4,A5,XXREAL_0:2;
domfvs c= Seg len vs
proof
let x be object;
assume x in domfvs;
then consider kk being Nat such that
A334: x = kk and
A335: 1<=kk and
A336: kk<=n;
kk<=len vs by A333,A336,XXREAL_0:2;
hence thesis by A334,A335;
end;
then reconsider fvs as FinSubsequence by A331,FINSEQ_1:def 12;
fvs c= vs
proof
let p be object;
assume
A337: p in fvs;
then consider x, y being object such that
A338: [x,y] = p by RELAT_1:def 1;
A339: x in dom fvs by A337,A338,FUNCT_1:1;
then consider kk being Nat such that
A340: x = kk and
A341: 1<=kk and
A342: kk<=n by A331;
kk<=len vs by A333,A342,XXREAL_0:2;
then
A343: x in dom vs by A340,A341,FINSEQ_3:25;
y = fvs.x by A337,A338,FUNCT_1:1;
then y = vs.kk by A331,A332,A339,A340;
hence thesis by A338,A340,A343,FUNCT_1:1;
end;
then reconsider fvs as Subset of vs;
domfvs c= Seg len vs
proof
let x be object;
assume x in domfvs;
then consider k being Nat such that
A344: x=k and
A345: 1<=k and
A346: k<=n;
k<=len vs by A333,A346,XXREAL_0:2;
hence thesis by A344,A345;
end;
then reconsider domfvs as finite set;
take fvs;
take c9 = c1;
take p1 = pp;
A347: pp is_vertex_seq_of c1 by A2,A12,A315,A311,Th42;
then
A348: len pp = len c1 + 1;
thus len c9 < len c by A10,A311,A317,XREAL_0:def 2;
thus p1 is_vertex_seq_of c9 by A2,A12,A315,A311,Th42;
len p1 = len c1 + 1 by A347;
hence len p1 < len vs by A4,A5,A318,XXREAL_0:2;
thus vs.1 = p1.1 by A3,A333,Th12;
thus vs.len vs = p1.len p1 by A3,A4,A6,A308,Th12;
A349: Sgm domfc = idseq n1 by FINSEQ_3:48;
then
A350: dom Sgm domfc = Seg n1;
now
let p be object;
hereby
assume
A351: p in c1;
then consider x, y being object such that
A352: p=[x,y] by RELAT_1:def 1;
A353: y=c1.x by A351,A352,FUNCT_1:1;
A354: x in dom c1 by A351,A352,FUNCT_1:1;
then reconsider k = x as Element of NAT;
A355: k<=len c1 by A354,FINSEQ_3:25;
A356: 1<=k by A354,FINSEQ_3:25;
then x in dom SL by A317,A350,A355;
then
A357: k=SL.k by A349,FUNCT_1:18;
0+1<=k by A354,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A358: i one-to-one for Chain of G;
correctness;
end;
theorem
p is Path of G implies p|Seg(n) is Path of G
proof
reconsider q=p|(Seg n) as FinSequence;
assume
A1: p is Path of G;
now
let n1,m1 be Nat;
assume that
A2: 1<=n1 and
A3: n1 < m1 and
A4: m1<=len q;
1 q.m1 by A1,A2,A3,A5,A6,GRAPH_1:def 16;
end;
hence thesis by A1,GRAPH_1:4,def 16;
end;
registration
let G;
cluster simple for Path of G;
existence
proof
set x = the Element of G;
set q = the empty Chain of G;
reconsider q as one-to-one Chain of G;
take q;
reconsider p = <*x*> as FinSequence of the carrier of G;
take p;
thus p is_vertex_seq_of q by Lm8;
let n,m;
assume that
A1: 1<=n and
A2: nsc.2
proof
hereby
assume
A1: sc is Path of G;
assume
A2: not len sc = 0;
assume not len sc = 1;
then len sc >1 by A2,NAT_1:25;
then
A3: 1+1<=len sc by NAT_1:13;
assume sc.1 = sc.2;
hence contradiction by A1,A3,GRAPH_1:def 16;
end;
assume
A4: len sc = 0 or len sc = 1 or sc.1<>sc.2;
per cases by A4;
suppose
len sc = 0;
then for n, m st 1<=n & nsc.m;
hence thesis by GRAPH_1:def 16;
end;
suppose
len sc = 1;
then for n,m st 1<=n & nsc.m by XXREAL_0:2;
hence thesis by GRAPH_1:def 16;
end;
suppose
A5: sc.1<>sc.2;
now
let n, m;
assume that
A6: 1<=n and
A7: nsc.m
proof
consider vs such that
A9: vs is_vertex_seq_of sc and
A10: for n,m st 1<=n & n oriented for Chain of G;
correctness;
end;
definition
let G;
let oc be oriented Chain of G;
assume
A1: oc <> {};
func vertex-seq oc -> FinSequence of the carrier of G means
it is_vertex_seq_of oc & it.1 = (the Source of G).(oc.1);
existence
proof
set TG = the Target of G;
set SG = the Source of G;
deffunc F(Nat) = SG.(oc.$1);
consider z being FinSequence such that
A2: len z = len oc & for j be Nat st j in dom z holds z.j = F(j) from
FINSEQ_1:sch 2;
set vs = z^<*TG.(oc.len oc)*>;
A3: len vs = len oc + len <*TG.(oc.len oc)*> by A2,FINSEQ_1:22
.= len oc +1 by FINSEQ_1:39;
A4: Seg len z = dom z by FINSEQ_1:def 3;
A5: Seg len oc = dom oc by FINSEQ_1:def 3;
0+1=1;
then
A6: 1<=len oc by A1,NAT_1:13;
rng vs c= the carrier of G
proof
let y be object;
assume y in rng vs;
then consider x being object such that
A7: x in dom vs and
A8: y = vs.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A7;
A9: 1<=x by A7,FINSEQ_3:25;
A10: x<=len vs by A7,FINSEQ_3:25;
per cases by A3,A10,NAT_1:8;
suppose
A11: x<=len oc;
A12: rng oc c= the carrier' of G by FINSEQ_1:def 4;
A13: x in dom oc by A9,A11,FINSEQ_3:25;
then
A14: oc.x in rng oc by FUNCT_1:def 3;
then reconsider e=oc.x as Element of the carrier' of G by A12;
A15: SG.e in rng the Source of G by A14,A12,FUNCT_2:4;
A16: rng the Source of G c= the carrier of G by RELAT_1:def 19;
vs.x = z.x by A2,A5,A4,A13,FINSEQ_1:def 7
.= SG.e by A2,A5,A4,A13;
hence thesis by A8,A15,A16;
end;
suppose
A17: x=len oc +1;
len oc in dom oc by A6,FINSEQ_3:25;
then
A18: oc.len oc in rng oc by FUNCT_1:def 3;
A19: rng oc c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e=oc.len oc as Element of the carrier' of G by A18;
A20: rng the Target of G c= the carrier of G by RELAT_1:def 19;
TG.e in rng the Target of G by A18,A19,FUNCT_2:4;
then y is Element of G by A2,A8,A17,A20,FINSEQ_1:42;
hence thesis;
end;
end;
then reconsider vs as FinSequence of the carrier of G by FINSEQ_1:def 4;
take vs;
now
thus len vs = len oc + 1 by A3;
let n;
assume that
A21: 1<=n and
A22: n<=len oc;
A23: 1<=n+1 by NAT_1:12;
n+1<=len vs by A3,A22,XREAL_1:7;
then n+1 in dom vs by A23,FINSEQ_3:25;
then reconsider vsn1 = vs.(n+1) as Element of G by FINSEQ_2:11;
A24: vsn1 = vs/.(n+1) by A3,A22,A23,FINSEQ_4:15,XREAL_1:7;
A25: vsn1 = TG.(oc.n)
proof
per cases by A22,XXREAL_0:1;
suppose
A26: n = f
proof
let f be FinSequence;
len <*x*> = 1 by FINSEQ_1:39;
then (2, len <*x*>)-cut <*x*> = {} by Def1;
hence thesis by FINSEQ_1:34;
end;
theorem :: GRAPH_2:14
for f1, f2 being FinSequence of D holds 1<=n & n<=len f1 implies (f1^'
f2)/.n = f1/.n
proof
let f1, f2 be FinSequence of D;
assume that
A1: 1<=n and
A2: n<=len f1;
per cases;
suppose
f2 = {};
hence thesis by Th55;
end;
suppose
A3: f2 <> {};
then
A4: len f1 + 0 < len f1 + len f2 by XREAL_1:6;
len (f1^'f2) + 1 = len f1 + len f2 by A3,Th13;
then n < len (f1^'f2) + 1 by A2,A4,XXREAL_0:2;
then n <= len (f1^'f2) by NAT_1:13;
hence (f1^'f2)/.n = (f1^'f2).n by A1,FINSEQ_4:15
.= f1.n by A1,A2,Th14
.= f1/.n by A1,A2,FINSEQ_4:15;
end;
end;
theorem :: GRAPH_2:15
for f1, f2 being FinSequence of D holds 1<=n & n {};
A6: len f1 + n < len f1 + len f2 by A2,XREAL_1:6;
len (f1^'f2) + 1 = len f1 + len f2 by A5,Th13;
hence len f1+n <= len (f1^'f2) by A6,NAT_1:13;
end;
suppose
f2 = {};
hence len f1+n <= len (f1^'f2) by A2;
end;
end;
A7: 0+1 <= n+1 by XREAL_1:6;
0+1 <= len f1 + n by A1,XREAL_1:7;
hence (f1^'f2)/.(len f1 + n) = (f1^'f2).(len f1 + n) by A4,FINSEQ_4:15
.= f2.(n+1) by A1,A2,Th15
.= f2/.(n+1) by A7,A3,FINSEQ_4:15;
end;
:: from SFMATR3, 2007.07.26, A.T.
definition
let F be FinSequence of INT, m, n be Nat;
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len F;
func min_at(F, m, n) -> Nat means
:Def11:
ex X being finite non
empty Subset of INT st X = rng ((m,n)-cut F) & it+1 = (min X)..(m,n)-cut F +m;
existence
proof
set Cut = (m,n)-cut F;
set X = rng Cut;
m < n+1 by A2,NAT_1:13;
then
A4: m-m < n+1-m by XREAL_1:9;
len Cut +m = n+1 by A1,A2,A3,Def1;
then
A5: Cut is non empty by A4;
rng (Cut qua Relation of NAT, INT) is Subset of INT;
then reconsider X as finite non empty Subset of INT by A5;
set q = (min X)..Cut +m -1;
1-1 <= m-1 by A1,XREAL_1:9;
then 0+0 <= (min X)..Cut + (m-1);
then reconsider q as Element of NAT by INT_1:3;
take q, X;
thus X = rng Cut;
thus thesis;
end;
uniqueness;
end;
reserve F, F1 for FinSequence of INT,
k, m, n, ma for Nat;
theorem Th59:
1 <= m & m <= n & n <= len F implies (ma = min_at(F, m, n) iff m
<= ma & ma <= n & (for i being Nat st m <= i & i <= n holds F.ma <=
F.i) & for i being Nat st m <= i & i < ma holds F.ma < F.i)
proof
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len F;
set Cut = (m,n)-cut F;
A4: len Cut +m = n+1 by A1,A2,A3,Def1;
hereby
A5: n-m < n-m+1 by XREAL_1:29;
assume ma = min_at(F, m, n);
then consider X being finite non empty Subset of INT such that
A6: X = rng Cut and
A7: ma+1 = (min X)..Cut +m by A1,A2,A3,Def11;
A8: ma = (min X)..Cut-1 +m by A7;
A9: ma = (min X)..Cut +m-1 by A7;
A10: min X in X by XXREAL_2:def 7;
then
A11: 1 <= (min X)..Cut by A6,FINSEQ_4:21;
then 1-1 <= (min X)..Cut-1 by XREAL_1:9;
then reconsider i1 = (min X)..Cut-1 as Element of NAT by INT_1:3;
A12: (min X)..Cut <= len Cut by A6,A10,FINSEQ_4:21;
then i1 < len Cut by XREAL_1:146,XXREAL_0:2;
then
A13: F.ma = Cut.(i1+1) by A1,A2,A3,A8,Def1
.= Cut.(ma+1-m) by A7;
(min X)..Cut+m <= len Cut +m by A12,XREAL_1:6;
then
A14: ma <= len Cut +m-1 by A9,XREAL_1:9;
m+1 <= (min X)..Cut +m by A11,XREAL_1:6;
then m+1-1 <= ma by A9,XREAL_1:9;
hence m <= ma & ma <= n by A4,A14;
A15: Cut.((min X)..Cut) = min X by A6,A10,FINSEQ_4:19;
thus
A16: for i being Nat st m <= i & i <= n holds F.ma <= F.i
proof
let i be Nat;
assume that
A17: m <= i and
A18: i <= n;
m-m <= i-m by A17,XREAL_1:9;
then reconsider i1 = i-m as Element of NAT by INT_1:3;
A19: 0+1 <= i1+1 by XREAL_1:6;
A20: n-m < n-m+1 by XREAL_1:29;
i1 <= n-m by A18,XREAL_1:9;
then
A21: i1 < len Cut by A4,A20,XXREAL_0:2;
then i1+1 <= len Cut by NAT_1:13;
then
A22: i1+1 in dom Cut by A19,FINSEQ_3:25;
Cut.(i1+1) = F.(m+i1) by A1,A2,A3,A21,Def1;
then F.i in rng Cut by A22,FUNCT_1:def 3;
hence thesis by A6,A7,A13,A15,XXREAL_2:def 7;
end;
let i be Nat;
assume that
A23: m <= i and
A24: i < ma;
A25: i <= n by A4,A14,A24,XXREAL_0:2;
then
A26: F.ma <= F.i by A16,A23;
m-m <= i-m by A23,XREAL_1:9;
then reconsider i1 = i-m as Element of NAT by INT_1:3;
reconsider k = i1+1 as Element of NAT;
i <= len Cut -1 +m by A14,A24,XXREAL_0:2;
then i-m <= len Cut -1 by XREAL_1:20;
then
A27: k <= len Cut by XREAL_1:19;
i1 <= n-m by A25,XREAL_1:9;
then
A28: i1 < len Cut by A4,A5,XXREAL_0:2;
0+1 <= k by XREAL_1:6;
then
A29: k in dom Cut by A27,FINSEQ_3:25;
i-m < ma-m by A24,XREAL_1:9;
then
A30: k < ma-m+1 by XREAL_1:6;
F.i = F.(i1+m) .= Cut.k by A1,A2,A3,A28,Def1;
then F.i <> F.ma by A6,A7,A10,A13,A30,A29,FINSEQ_4:19,24;
hence F.ma < F.i by A26,XXREAL_0:1;
end;
set Cut = (m,n)-cut F;
A31: len Cut +m = n+1 by A1,A2,A3,Def1;
then
A32: len Cut = n+1-m;
set X = rng Cut;
A33: rng (Cut qua Relation of NAT, INT) is Subset of INT;
m < n+1 by A2,NAT_1:13;
then m-m < n+1-m by XREAL_1:9;
then Cut is non empty by A31;
then reconsider X as finite non empty Subset of INT by A33;
reconsider rX = X as finite non empty Subset of REAL by MEMBERED:3;
assume that
A34: m <= ma and
A35: ma <= n and
A36: for i being Nat st m <= i & i <= n holds F.ma <= F.i and
A37: for i being Nat st m <= i & i < ma holds F.ma < F.i;
m-m <= ma-m by A34,XREAL_1:9;
then reconsider qm = ma-m as Element of NAT by INT_1:3;
A38: qm+1 = ma+1-m;
then reconsider q1 = ma+1-m as Element of NAT;
ma+1 <= n+1 by A35,XREAL_1:6;
then
A39: q1 <= len Cut by A32,XREAL_1:9;
0+1 <= qm+1 by XREAL_1:6;
then
A40: q1 in dom Cut by A39,FINSEQ_3:25;
A41: ma = qm+m;
qm < len Cut by A38,A39,NAT_1:13;
then
A42: F.ma = Cut.(ma+1-m) by A1,A2,A3,A38,A41,Def1;
now
thus F.ma in X by A40,A42,FUNCT_1:def 3;
let k be ExtReal;
assume k in X;
then consider dk being object such that
A43: dk in dom Cut and
A44: Cut.dk = k by FUNCT_1:def 3;
reconsider dk as Element of NAT by A43;
1 <= dk by A43,FINSEQ_3:25;
then 1-1 <= dk-1 by XREAL_1:9;
then reconsider dk1 = dk-1 as Element of NAT by INT_1:3;
A45: dk <= len Cut by A43,FINSEQ_3:25;
then dk+m <= (len Cut)+m by XREAL_1:6;
then
A46: dk+m-1 <= n by A4,XREAL_1:20;
dk1 < len Cut by A45,XREAL_1:146,XXREAL_0:2;
then F.(dk1+m) = Cut.(dk1+1) by A1,A2,A3,Def1
.= Cut.dk;
hence F.ma <= k by A36,A44,A46,NAT_1:12;
end;
then
A47: F.ma = min rX by XXREAL_2:def 7;
set mX = min X;
set mXC = mX..Cut;
A48: mX in X by XXREAL_2:def 7;
then 1 <= mXC by FINSEQ_4:21;
then 1-1 <= mXC -1 by XREAL_1:9;
then reconsider mXC1 = mXC-1 as Element of NAT by INT_1:3;
set mXCm = mXC1+m;
mXC <= len Cut by A48,FINSEQ_4:21;
then
A49: mXC1 < len Cut by XREAL_1:146,XXREAL_0:2;
mXC = mXC1+1;
then
A50: F.mXCm = Cut.mXC by A1,A2,A3,A49,Def1;
A51: m <= mXCm by NAT_1:12;
A52: Cut.(mX..Cut) = mX by A48,FINSEQ_4:19;
now
assume
A53: q1 <> mXC;
per cases by A53,XXREAL_0:1;
suppose
q1 < mXC;
hence contradiction by A40,A42,A47,FINSEQ_4:24;
end;
suppose
q1 > mXC;
then mXC+m < ma+1 by XREAL_1:20;
then mXC+m-1 < ma by XREAL_1:19;
hence contradiction by A37,A52,A47,A51,A50;
end;
end;
then ma+1 = mX..Cut +m;
hence thesis by A1,A2,A3,Def11;
end;
theorem
1 <= m & m <= len F implies min_at(F, m, m) = m
proof
assume that
A1: 1 <= m and
A2: m <= len F;
A3: for i being Nat st m <= i & i < m holds F.m < F.i;
for i being Nat st m <= i & i <= m holds F.m <= F.i by XXREAL_0:1;
hence thesis by A1,A2,A3,Th59;
end;
definition
let F be FinSequence of INT, m, n be Nat;
pred F is_non_decreasing_on m, n means
for i, j being Nat st m <= i & i <= j & j <= n holds F.i <= F.j;
end;
definition
let F be FinSequence of INT, n be Nat;
pred F is_split_at n means
for i, j being Nat st 1 <= i &
i <= n & n < j & j <= len F holds F.i <= F.j;
end;
theorem
k+1 <= len F & ma = min_at(F, k+1, len F) & F is_split_at k & F
is_non_decreasing_on 1, k & F1 = F+*(k+1, F.ma)+*(ma, F.(k+1)) implies F1
is_non_decreasing_on 1, k+1
proof
assume that
A1: k+1 <= len F and
A2: ma = min_at(F, k+1, len F) and
A3: F is_split_at k and
A4: F is_non_decreasing_on 1, k and
A5: F1 = F+*(k+1, F.ma)+*(ma, F.(k+1));
A6: 1 <= k+1 by NAT_1:12;
set Fk = F+*(k+1, F.ma);
A7: dom F1 = dom Fk by A5,FUNCT_7:30;
A8: dom Fk = dom F by FUNCT_7:30;
then
A9: k+1 in dom F1 by A1,A7,A6,FINSEQ_3:25;
let i, j be Nat such that
A10: 1 <= i and
A11: i <= j and
A12: j <= k+1;
A13: j <= len F by A1,A12,XXREAL_0:2;
1 <= j by A10,A11,XXREAL_0:2;
then
A14: j in dom F1 by A7,A8,A13,FINSEQ_3:25;
per cases by A12,XXREAL_0:1;
suppose
A15: j < k+1;
then i < k+1 by A11,XXREAL_0:2;
then i <> ma by A1,A2,A6,Th59;
then
A16: F1.i = Fk.i by A5,FUNCT_7:32
.= F.i by A11,A15,FUNCT_7:32;
j <> ma by A1,A2,A6,A15,Th59;
then
A17: F1.j = Fk.j by A5,FUNCT_7:32
.= F.j by A15,FUNCT_7:32;
j <= k by A15,NAT_1:13;
hence thesis by A4,A10,A11,A16,A17;
end;
suppose
A18: j = k+1;
thus F1.i <= F1.j
proof
per cases by A11,XXREAL_0:1;
suppose
A19: i < j;
then i <> ma by A1,A2,A6,A18,Th59;
then
A20: F1.i = Fk.i by A5,FUNCT_7:32
.= F.i by A18,A19,FUNCT_7:32;
A21: i <= k by A18,A19,NAT_1:13;
A22: k < j by A18,NAT_1:13;
thus F1.i <= F1.j
proof
per cases;
suppose
k+1 = ma;
then F1.j = F.(k+1) by A5,A7,A9,A18,FUNCT_7:31;
hence thesis by A1,A3,A10,A18,A20,A21,A22;
end;
suppose
A23: k+1 <> ma;
A24: ma <= len F by A1,A2,A6,Th59;
k+1 <= ma by A1,A2,A6,Th59;
then
A25: k < ma by NAT_1:13;
F1.j = Fk.j by A5,A18,A23,FUNCT_7:32
.= F.ma by A7,A8,A14,A18,FUNCT_7:31;
hence thesis by A3,A10,A20,A21,A25,A24;
end;
end;
end;
suppose
i = j;
hence thesis;
end;
end;
end;
end;
theorem
k+1 <= len F & ma = min_at(F, k+1, len F) & F is_split_at k & F1 = F+*
(k+1, F.ma)+*(ma, F.(k+1)) implies F1 is_split_at k+1
proof
assume that
A1: k+1 <= len F and
A2: ma = min_at(F, k+1, len F) and
A3: F is_split_at k and
A4: F1 = F+*(k+1, F.ma)+*(ma, F.(k+1));
A5: dom F1 = dom (F+*(k+1, F.ma)) by A4,FUNCT_7:30;
A6: k < k+1 by NAT_1:13;
A7: 1 <= k+1 by NAT_1:12;
let i, j be Nat;
assume that
A8: 1 <= i and
A9: i <= k+1 and
A10: k+1 < j and
A11: j <= len F1;
A12: k < j by A10,NAT_1:13;
A13: dom (F+*(k+1, F.ma)) = dom F by FUNCT_7:30;
then
A14: len F1 = len F by A5,FINSEQ_3:29;
then
A15: k+1 <= len F by A10,A11,XXREAL_0:2;
i <= len F1 by A1,A14,A9,XXREAL_0:2;
then
A16: i in dom F1 by A8,FINSEQ_3:25;
1 <= j by A10,NAT_1:12;
then
A17: j in dom F1 by A11,FINSEQ_3:25;
per cases by A9,XXREAL_0:1;
suppose
A18: i < k+1;
then i <> ma by A1,A2,A7,Th59;
then
A19: F1.i = (F+*(k+1, F.ma)).i by A4,FUNCT_7:32
.= F.i by A18,FUNCT_7:32;
A20: i <= k by A18,NAT_1:13;
thus F1.i <= F1.j
proof
per cases;
suppose
j <> ma;
then F1.j = (F+*(k+1, F.ma)).j by A4,FUNCT_7:32
.= F.j by A10,FUNCT_7:32;
hence thesis by A3,A14,A8,A11,A12,A20,A19;
end;
suppose
j = ma;
then F1.j = F.(k+1) by A4,A5,A17,FUNCT_7:31;
hence thesis by A3,A6,A8,A15,A20,A19;
end;
end;
end;
suppose
A21: i = k+1;
A22: F1.i = F.ma
proof
per cases;
suppose
k+1 = ma;
hence thesis by A4,A5,A16,A21,FUNCT_7:31;
end;
suppose
k+1 <> ma;
hence F1.i = (F+*(k+1, F.ma)).i by A4,A21,FUNCT_7:32
.= F.ma by A5,A13,A16,A21,FUNCT_7:31;
end;
end;
thus thesis
proof
per cases;
suppose
j = ma;
then F1.j = F.(k+1) by A4,A5,A17,FUNCT_7:31;
hence thesis by A1,A2,A7,A22,Th59;
end;
suppose
j <> ma;
then F1.j = (F+*(k+1, F.ma)).j by A4,FUNCT_7:32
.= F.j by A10,FUNCT_7:32;
hence thesis by A1,A2,A14,A7,A10,A11,A22,Th59;
end;
end;
end;
end;
:: from SCPISORT, 2011.02.13
theorem
for f being FinSequence of INT,m,n be Nat st m >= n
holds f is_non_decreasing_on m,n
proof
let f be FinSequence of INT,m,n be Nat;
assume
A1: m>=n;
let i, j be Nat such that
A2: m <= i & i <= j and
A3: j <= n;
A4: m <= j by A2,XXREAL_0:2;
per cases by A1,XXREAL_0:1;
suppose m=n;
then j=m by A3,A4,XXREAL_0:1;
hence f.i <= f.j by A2,XXREAL_0:1;
end;
suppose m>n;
hence thesis by A3,A4,XXREAL_0:2;
end;
end;