Copyright (c) 1995 Association of Mizar Users
environ
vocabulary FINSEQ_1, FINSET_1, FUNCT_1, ARYTM_1, RELAT_1, INT_1, CARD_1,
BOOLE, FINSEQ_2, TARSKI, GRAPH_1, ORDERS_1, GRAPH_2, FINSEQ_4;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1,
FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, FINSET_1, NAT_1,
INT_1, GRAPH_1, BINARITH;
constructors WELLORD2, INT_1, GRAPH_1, BINARITH, FINSEQ_4, PARTFUN1, MEMBERED;
clusters INT_1, FUNCT_1, FINSEQ_1, FINSET_1, CARD_1, GRAPH_1, RELSET_1, NAT_1,
XREAL_0, MEMBERED, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, REAL_1, GRAPH_1, XBOOLE_0;
theorems TARSKI, AXIOMS, ENUMSET1, NAT_1, REAL_1, FINSEQ_1, FINSEQ_2, GRAPH_1,
RELAT_1, FUNCT_1, GRFUNC_1, FUNCT_2, BINARITH, REAL_2, INT_1, FINSET_1,
CARD_1, CARD_2, CARD_4, FINSEQ_3, FINSEQ_4, CQC_THE1, ZFMISC_1, RELSET_1,
GROUP_3, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes NAT_1, RECDEF_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, k1, k2, n, r for Nat;
scheme FinSegRng{m, n() -> Nat, F(set)->set, P[Nat]}:
{F(i): m()<=i & i<=n() & P[i]} is finite
proof
set F = {F(i): m()<=i & i<=n() & P[i]};
deffunc G(Nat) = F($1-1);
consider f being FinSequence such that
A1: len f = n()+1 and
A2: for k st k in Seg (n()+1) holds f.k = G(k) from SeqLambda;
F c= rng f proof let x be set;assume x in F; then consider j such that
A3: x=F(j) & m()<=j & j<=n() and P[j];
1<=j+1 & j+1<=n()+1 by A3,AXIOMS:24,NAT_1:29;
then A4: j+1 in Seg (n()+1) by FINSEQ_1:3;
then A5: j+1 in dom f by A1,FINSEQ_1:def 3;
f.(j+1) = F(j+1-1) by A2,A4 .= F(j) by XCMPLX_1:26;
hence x in rng f by A3,A5,FUNCT_1:def 5;
end;
hence thesis by FINSET_1:13;
end;
theorem Th1: m+1<=k & k<=n iff ex i being Nat st m<=i & i<n & k=i+1 proof
hereby assume that
A1: m+1<=k and
A2: k<=n;
reconsider k'=k as Integer; reconsider 1'=1 as Integer;
1<=m+1 by NAT_1:29; then 1'<=k' by A1,AXIOMS:22;
then reconsider i=k'-1' as Nat by INT_1:18;
take i; m+1-1<=k-1 by A1,REAL_1:49;
hence m<=i by XCMPLX_1:26;
k<k+1 by NAT_1:38; then k-1<k+1-1 by REAL_1:54; then k-1<k by XCMPLX_1:26
;
hence i<n by A2,AXIOMS:22; thus k=i+1 by XCMPLX_1:27;
end; given i being Nat such that A3: m<=i & i<n & k=i+1;
thus m+1<=k & k<=n by A3,NAT_1:38,REAL_1:55;
end;
theorem Th2: q = p|Seg n implies
len q<=len p & for i st 1<=i & i<=len q
holds p.i = q.i
proof assume
A1: q = p|Seg n;
per cases;
suppose A2: n<=len p; then A3: len q = n by A1,FINSEQ_1:21;
thus len q<=len p by A1,A2,FINSEQ_1:21; let i be Nat;
assume that
A4: 1<=i and
A5: i<=len q;
i in Seg n by A3,A4,A5,FINSEQ_1:3;
hence p.i = q.i by A1,FUNCT_1:72;
suppose
A6: len p<=n;
hence len q<=len p by A1,FINSEQ_2:23; let i be Nat;
assume 1<=i & i<=len q;
thus p.i = q.i by A1,A6,FINSEQ_2:23;
end;
theorem Th3:
X c= Seg k & Y c= dom Sgm X
implies (Sgm X)*(Sgm Y) = Sgm rng ((Sgm X)|Y) proof
assume that
A1: X c= Seg k and
A2: Y c= dom Sgm X;
A3: Y c= Seg len Sgm X by A2,FINSEQ_1:def 3;
set M = (Sgm X)*(Sgm Y);
reconsider Y' = Y as finite set by A3,FINSET_1:13;
A4: dom Sgm Y' = Seg card Y' by A3,FINSEQ_3:45;
A5: rng Sgm Y = Y by A3,FINSEQ_1:def 13;
then dom M = Seg card Y' by A2,A4,RELAT_1:46;
then reconsider M as FinSequence by FINSEQ_1:def 2;
A6: rng Sgm X c= Seg k & Seg k c= NAT by A1,FINSEQ_1:def 13;
then A7: rng Sgm X c= NAT by XBOOLE_1:1;
rng M c= rng Sgm X by RELAT_1:45;
then rng M c= NAT by A7,XBOOLE_1:1;
then reconsider L = (Sgm X)*(Sgm Y) as FinSequence of NAT by FINSEQ_1:def 4;
set R = rng ((Sgm X)|Y);
R c= rng Sgm X by RELAT_1:99;
then A8: R c= Seg k by A6,XBOOLE_1:1;
now let y be set;
hereby assume y in rng L; then consider x such that
A9: x in dom L & y = L.x by FUNCT_1:def 5;
A10: y = (Sgm X).((Sgm Y).x) by A9,FUNCT_1:22;
x in dom Sgm Y by A9,FUNCT_1:21;
then (Sgm Y).x in Y by A5,FUNCT_1:def 5; hence y in R by A2,A10,FUNCT_1:73
;
end;
assume y in R; then consider x such that
A11: x in dom ((Sgm X)|Y) & y = ((Sgm X)|Y).x by FUNCT_1:def 5;
x in (dom Sgm X)/\Y by A11,RELAT_1:90;
then A12: x in dom Sgm X & x in Y by XBOOLE_0:def 3;
then A13: y = (Sgm X).x by A11,FUNCT_1:72;
consider z being set such that
A14: z in dom Sgm Y & x = (Sgm Y).z by A5,A12,FUNCT_1:def 5;
A15: z in dom((Sgm X)*(Sgm Y)) by A12,A14,FUNCT_1:21;
then L.z = y by A13,A14,FUNCT_1:22;
hence y in rng L by A15,FUNCT_1:def 5;
end;
then A16: rng L = R by TARSKI:2;
now let l,m,k1,k2;
assume that
A17: 1 <= l and
A18: l < m and
A19: m <= len L and
A20: k1=L.l and
A21: k2=L.m;
l <= len L & 1<=m by A17,A18,A19,AXIOMS:22;
then A22: l in dom L & m in dom L by A17,A19,FINSEQ_3:27;
then A23: L.l = (Sgm X).((Sgm Y).l) & L.m = (Sgm X).((Sgm Y).m) by FUNCT_1:22
;
A24: l in dom Sgm Y & (Sgm Y).l in dom Sgm X &
m in dom Sgm Y & (Sgm Y).m in dom Sgm X by A22,FUNCT_1:21;
then A25: 1<=l & l<=len Sgm Y & 1<=m & m<=len Sgm Y by FINSEQ_3:27;
reconsider K1 = (Sgm Y).l as Nat by A24;
reconsider K2 = (Sgm Y).m as Nat by A24;
A26: K1 < K2 by A3,A18,A25,FINSEQ_1:def 13;
1<=K1 & K1<=len Sgm X & 1<=K2 & K2<=len Sgm X by A24,FINSEQ_3:27;
hence k1 < k2 by A1,A20,A21,A23,A26,FINSEQ_1:def 13;
end;
hence (Sgm X)*(Sgm Y) = Sgm rng ((Sgm X)|Y) by A8,A16,FINSEQ_1:def 13;
end;
Lm1: for m, n being Nat, F being finite set
st F = {k: m<=k & k<=m+n} holds card F = n+1 proof
let m be Nat;
defpred P[Nat] means for F being finite set
st F = {k: m<=k & k<=m+$1} holds card F = $1+1;
A1: P[0] proof let F be finite set; assume
A2: F = {k: m<=k & k<=m+0};
now let x be set;
hereby assume x in F; then consider k being Nat such that
A3: x = k & m<=k & k<=m+0 by A2;
thus x = m by A3,AXIOMS:21;
end; assume x = m; hence x in F by A2;
end; then F = {m} & 0+1 = 1 by TARSKI:def 1;
hence card F = 0+1 by CARD_1:79;
end;
A4: now let n be Nat; assume
A5: P[n];
thus P[n+1]
proof
let F be finite set; assume
A6: F = {k: m<=k & k<=m+(n+1)};
set F1 = {k: m<=k & k<=m+n};
reconsider F2 = {k: k<=m+n} as finite set by CQC_THE1:12;
F1 c= F2 proof let x be set; assume
x in F1; then consider k being Nat such that
A7: x=k & m<=k & k<=m+n;
thus x in F2 by A7;
end; then reconsider F1 as finite set by FINSET_1:13;
now let x be set;
hereby assume x in F; then consider k such that
A8: x=k & m<=k & k<=m+(n+1) by A6;
k<=m+n+1 by A8,XCMPLX_1:1;
then k<=m+n or k=m+n+1 by NAT_1:26;
then k<=m+n or k=m+(n+1) by XCMPLX_1:1;
then k in F1 or k in {m+(n+1)} by A8,TARSKI:def 1;
hence x in F1 \/ {m+(n+1)} by A8,XBOOLE_0:def 2;
end;
assume
A9: x in F1 \/ {m+(n+1)};
per cases by A9,XBOOLE_0:def 2;
suppose x in F1; then consider k such that
A10: x=k & m<=k & k<=m+n;
k<=m+n+1 by A10,NAT_1:37; then k<=m+(n+1) by XCMPLX_1:1;
hence x in F by A6,A10;
suppose A11: x in {m+(n+1)};
then A12: x=m+(n+1) by TARSKI:def 1;
reconsider k = x as Nat by A11,TARSKI:def 1;
m<=k & k<=m+(n+1) by A12,NAT_1:29;
hence x in F by A6;
end;
then A13: F = {k: m<=k & k<=m+n} \/ {m+(n+1)} by TARSKI:2;
A14: not m+(n+1) in {k: m<=k & k<=m+n} proof assume
not thesis; then consider k such that
A15: m+(n+1) = k & m<=k & k<=m+n;
m+n+1<=m+n+0 by A15,XCMPLX_1:1; hence contradiction by REAL_1:53;
end;
card F1 = n+1 by A5;
hence card F = n+1+1 by A13,A14,CARD_2:54;
end;
end;
for n be Nat holds P[n] from Ind (A1, A4);
hence thesis;
end;
theorem Th4: for m, n being Nat holds Card {k: m<=k & k<=m+n} = n+1 proof
let m, n be Nat;
defpred P[Nat] means not contradiction;
deffunc F(Nat) = $1;
set F = {F(k): m<=k & k<=m+n & P[k]};
F is finite from FinSegRng;
then reconsider F as finite set;
F = {F(k): m<=k & k<=m+n}
proof
thus F c= {F(k): m<=k & k<=m+n}
proof
let x be set;
assume x in F; then
consider k1 being Nat such that
A1: x = F(k1) & m <= k1 & k1 <= m+n;
thus thesis by A1;
end;
let x be set;
assume x in {F(k): m<=k & k<=m+n}; then
consider k1 being Nat such that
A2:x = F(k1) & m <= k1 & k1 <= m+n;
thus thesis by A2;
end; then
reconsider G = {F(k): m<=k & k<=m+n} as finite set;
card G = n+1 by Lm1;
hence thesis;
end;
theorem Th5: for l st 1<=l & l<=n holds
Sgm {kk where kk is Nat: m+1<=kk & kk<=m+n}.l = m+l
proof
set F= Sgm {kk where kk is Nat: m+1<=kk & kk<=m+n};
defpred P[Nat] means 1<=$1 & $1<=n & F.$1 <> m+$1;
assume
A1: ex l st P[l];
consider k such that
A2: P[k] and
A3: for nn being Nat st P[nn] holds k <= nn from Min (A1);
set rF = {kk where kk is Nat: m+1<=kk & kk<=m+n};
A4: rF c= Seg (m+n) proof let x be set; assume x in rF;
then consider x' being Nat such that
A5: x'=x & m+1<=x' & x'<=m+n;
1<=m+1 by NAT_1:29; then 1<=x' by A5,AXIOMS:22;
hence x in Seg (m+n) by A5,FINSEQ_1:3;
end;
then reconsider rF as finite set by FINSET_1:13;
A6: card rF = n proof
per cases by NAT_1:19;
suppose
A7: n = 0;
rF = {} proof assume rF <> {}; then consider x being set such that
A8: x in rF by XBOOLE_0:def 1; consider x' being Nat such that
A9: x'=x & m+1<=x' & x'<=m+n by A8;
m+1<=m+0 by A7,A9,AXIOMS:22; hence contradiction by REAL_1:53;
end;
hence thesis by A7,CARD_1:78;
suppose 0<n; then 0+1<=n by NAT_1:38;
then 1-1<=n-1 by REAL_1:49;
then n-'1 = n-1 by BINARITH:def 3;
then reconsider n1 = n-1 as Nat;
(m+1)+n1 = m+(1+(n-1)) by XCMPLX_1:1 .= m+n by XCMPLX_1:27;
then card rF = n1+1 by Th4;
hence thesis by XCMPLX_1:27;
end;
m+1<=m+k & m+k<=m+n by A2,REAL_1:55;
then A10: m+k in rF;
A11: dom Sgm rF = Seg n by A4,A6,FINSEQ_3:45;
A12: len Sgm rF = n by A4,A6,FINSEQ_3:44;
A13: rng F c= NAT by FINSEQ_1:def 4;
A14: rng F = rF by A4,FINSEQ_1:def 13;
m+k in rng Sgm rF by A4,A10,FINSEQ_1:def 13; then consider x such that
A15: x in dom Sgm rF & m+k = (Sgm rF).x by FUNCT_1:def 5;
reconsider x as Nat by A15;
k in dom F by A2,A12,FINSEQ_3:27; then F.k in rng F by FUNCT_1:def 5;
then reconsider Fk = F.k as Nat by A13;
now
defpred P[Nat] means for Fk be Nat st 1<=$1 & $1<=n & Fk = F.$1
holds m+$1<=Fk;
A16: P[0];
A17: for k st P[k] holds P[k+1]
proof let k be Nat; assume
A18: P[k];
let Fk1 be Nat;
assume that
A19: 1<=k+1 and
A20: k+1<=n and
A21: Fk1 = F.(k+1);
A22: k<k+1 by NAT_1:38;
per cases by A19,REAL_1:def 5;
suppose 1<k+1;
then A23: 1<=k & k<=n by A20,NAT_1:38;
then k in dom F by A12,FINSEQ_3:27;
then F.k in rng F by FUNCT_1:def 5;
then reconsider Fk = F.k as Nat by A13;
A24: m+k<=Fk by A18,A23;
Fk < Fk1 by A4,A12,A20,A21,A22,A23,FINSEQ_1:def 13;
then m+k<Fk1 by A24,AXIOMS:22; then m+k+1<=Fk1 by NAT_1:38;
hence m+(k+1)<=Fk1 by XCMPLX_1:1;
suppose
A25: 1=k+1;
then 1 in dom F by A12,A20,FINSEQ_3:27;
then F.1 in rng F by FUNCT_1:def 5; then consider F1 being Nat such
that
A26: F1 = F.1 & m+1<=F1 & F1<=m+n by A14;
thus m+(k+1)<=Fk1 by A21,A25,A26;
end;
thus for k holds P[k] from Ind(A16,A17);
end;
then A27: m+k<=Fk by A2;
A28: 1<=x & x<=n by A11,A15,FINSEQ_1:3;
per cases by A2,A15,REAL_1:def 5;
suppose k < x;
hence contradiction by A2,A4,A12,A15,A27,A28,FINSEQ_1:def 13;
suppose
A29: k > x; F.x <> m+x by A2,A15,XCMPLX_1:2;
hence contradiction by A3,A28,A29;
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<len it holds it.(i+1)=p.(m+i)
if 1<=m & m<=n+1 & n<=len p
otherwise it ={};
consistency;
existence proof
hereby
assume that 1<=m and
A1: m<=n+1 and n<=len p;
deffunc F(Nat) = p.(m+($1-1));
consider s being FinSequence such that
A2: len s = n+1-'m & for k being Nat st k in Seg (n+1-'m) holds s.k=F(k)
from SeqLambda;
take s; m-m<=n+1-m by A1,REAL_1:49; then 0<=n+1-m by XCMPLX_1:14;
then len s +m = (n+1)-m+m by A2,BINARITH:def 3;
hence len s +m = n+1 by XCMPLX_1:27; let k be Nat; assume
A3: k<len s; 0<=k by NAT_1:18; then 0+1<=k+1 by REAL_1:55;
then 1<=k+1 & k+1<=len s by A3,NAT_1:38;
then k+1 in Seg (n+1-'m) by A2,FINSEQ_1:3;
hence s.(k+1) = p.(m+(k+1-1)) by A2 .= p.(m+k) by XCMPLX_1:26;
end;
thus thesis;
end;
uniqueness proof let s1, s2 be FinSequence;
hereby
assume 1<=m & m<=n+1 & n<=len p;
assume that
A4: len s1 +m = n+1 and
A5: for i being Nat st i<len s1 holds s1.(i+1) = p.(m+i);
assume that
A6: len s2 +m = n+1 and
A7: for i being Nat st i<len s2 holds s2.(i+1) = p.(m+i);
now thus len s1 = len s1; thus
A8: len s2 = len s1 by A4,A6,XCMPLX_1:2;
let i be Nat;assume i in Seg len s1; then 0+1<=i&i<=len s1 by FINSEQ_1:3;
then consider k such that
A9: 0<=k & k<len s1 & i=k+1 by Th1;
thus s1.i = p.(m+k) by A5,A9 .= s2.i by A7,A8,A9;
end; hence s1 = s2 by FINSEQ_2:10;
end;
thus thesis;
end;
end;
theorem Th6:
1<=m & m<=len p implies (m,m)-cut p = <*p.m*> proof
assume that
A1: 1<=m and
A2: m<=len p; set mp = (m,m)-cut p;
A3: m<=m+1 by NAT_1:37; then len mp + m = m + 1 by A1,A2,Def1;
then A4: len mp = 1 by XCMPLX_1:2;
then mp.(0+1) = p.(m+0) by A1,A2,A3,Def1 .= p.m;
hence (m,m)-cut p = <*p.m*> by A4,FINSEQ_1:57;
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:29; then len cp + 1 = len p + 1 by Def1; hence
A2: len cp = len p by XCMPLX_1:2; thus len p = len p;
let i; assume i in Seg len p; then 0+1<=i & i<=len p by FINSEQ_1:3;
then consider k being Nat such that A3: 0<=k & k<len cp & i=k+1 by A2,Th1;
thus cp.i = p.i by A1,A3,Def1;
end; hence thesis by FINSEQ_2:10;
end;
theorem Th8: m<=n & n<=r & r<=len p implies
(m+1, n)-cut p ^ (n+1, r)-cut p = (m+1, r)-cut p proof
assume that
A1: m<=n and
A2: n<=r and
A3: r<=len p;
set p1 = (m+1, n)-cut p; set p2 = (n+1, r)-cut p; set p3 = (m+1, r)-cut p;
set p12 = p1^p2;
now
A4: 1<=m+1 & m+1<=n+1 & n<=len p by A1,A2,A3,AXIOMS:22,24,NAT_1:29;
then len p1 +(m+1) = n+1 by Def1; then len p1+m+1 = n+1 by XCMPLX_1:1;
then len p1 +m-m = n-m by XCMPLX_1:2;
then A5: len p1 = n-m by XCMPLX_1:26;
A6: 1<=n+1 & n+1<=r+1 by A2,AXIOMS:24,NAT_1:29;
then len p2 +(n+1) = r+1 by A3,Def1;
then len p2 +n+1 = r+1 by XCMPLX_1:1;
then len p2 +n-n = r-n by XCMPLX_1:2;
then A7: len p2 = r-n by XCMPLX_1:26; m<=r by A1,A2,AXIOMS:22;
then A8: m+1<=r+1 by AXIOMS:24;
thus len p12 = len p12;
A9: len p12=len p1 +len p2 by FINSEQ_1:35 .= n-m+(r+ -n) by A5,A7,XCMPLX_0:def
8
.= (n-m)+ -n +r by XCMPLX_1:1 .= n-m-n+r by XCMPLX_0:def 8
.= n+ -m-n+r by XCMPLX_0:def 8 .= r+ -m by XCMPLX_1:26
.= r-m by XCMPLX_0:def 8;
m+1<=r+1 by A4,A6,AXIOMS:22; then len p3 +(m+1)=r+1 by A3,A4,Def1;
then len p3 +m+1 = r+1 by XCMPLX_1:1; then len p3 +m-m = r-m by XCMPLX_1:2;
hence
A10: len p3 = len p12 by A9,XCMPLX_1:26;
let i; assume i in Seg len p12;
then A11: 1<=i & i<=len p12 by FINSEQ_1:3;
reconsider m'=m as Integer;reconsider n'=n as Integer;
reconsider nm=n'-m' as Nat by A1,INT_1:18;
per cases by NAT_1:38;
suppose
A12: i<=nm; 0+1=1; then consider k being Nat such that
A13: 0<=k & k<nm & i=k+1 by A11,A12,Th1; nm<=r-m by A2,REAL_1:49
;
then A14: k<len p3 by A9,A10,A13,AXIOMS:22;
i in dom p1 by A5,A11,A12,FINSEQ_3:27;
hence p12.i = p1.i by FINSEQ_1:def 7 .= p.((m+1)+k) by A4,A5,A13,Def1
.= p3.i by A3,A4,A8,A13,A14,Def1;
suppose nm+1<=i; then consider k such that
A15: nm<=k & k<len p12 & i=k+1 by A11,Th1;
reconsider k''=k as Integer;
reconsider k'=k''-nm as Nat by A15,INT_1:18; k'+nm=k by XCMPLX_1:27;
then A16: i = nm+(k'+1) by A15,XCMPLX_1:1;
len p12 = len p2 + len p1 by FINSEQ_1:35;
then len p2 = len p12 - len p1 by XCMPLX_1:26;
then A17: k'<len p2 by A5,A15,REAL_1:54;
then 1<=k'+1 & k'+1<=len p2 by NAT_1:29,38;
then A18: k'+1 in dom p2 by FINSEQ_3:27;
A19: n+1+k' = n+(1+(k-(n-m))) by XCMPLX_1:1 .= 1+(k-n+m)+n by XCMPLX_1:37
.= 1+(k+ -n+m)+n by XCMPLX_0:def 8 .= 1+(k+m+-n)+n by XCMPLX_1:1
.= (1+(k+m))+-n+n by XCMPLX_1:1
.= (1+(k+m))-n+n by XCMPLX_0:def 8 .= 1+(k+m) by XCMPLX_1:27
.= m+1+k by XCMPLX_1:1;
thus p12.i = p2.(k'+1) by A5,A16,A18,FINSEQ_1:def 7
.= p.(n+1+k') by A3,A6,A17,Def1
.= p3.i by A3,A4,A8,A10,A15,A19,Def1;
end;
hence (m+1, n)-cut p ^ (n+1, r)-cut p = (m+1, r)-cut p by FINSEQ_2:10;
end;
theorem
m<=len p implies (1, m)-cut p ^ (m+1, len p)-cut p = p
proof
assume that
A1: m<=len p; A2: 0<=m by NAT_1:18;
set cp1 = (1, m)-cut p; set cpm = (m+1, len p)-cut p;
0+1=1; hence cp1 ^ cpm = (1, len p)-cut p by A1,A2,Th8 .= p by Th7;
end;
theorem
m<=n & n<=len p implies
(1, m)-cut p ^ (m+1, n)-cut p ^ (n+1, len p)-cut p = p proof
assume that
A1: m<=n and
A2: n<=len p; A3: 0<=m & 0<=n by NAT_1:18;
set cp1 = (1, m)-cut p; set cp2 = (m+1, n)-cut p; set cp3 = (n+1, len p)-cut p;
A4: 0+1=1;
hence cp1^cp2^cp3 = (1, n)-cut p ^cp3 by A1,A2,A3,Th8
.= (1, len p)-cut p by A2,A3,A4,Th8 .= p by Th7;
end;
theorem Th11: rng ((m,n)-cut p) c= rng p proof set c = ((m,n)-cut p);
A1: now assume that
A2: 1<=m and
A3: m<=n+1 and
A4: n<=len p;
thus thesis proof let x be set; assume x in rng c;
then consider z being set such that
A5: z in dom c & x = c.z by FUNCT_1:def 5;
reconsider z as Nat by A5;
0+1<=z & z<=len c by A5,FINSEQ_3:27; then consider i such that
A6: 0<=i & i<len c & z=i+1 by Th1;
A7: c.z = p.(m+i) by A2,A3,A4,A6,Def1;
m+i<len c +m by A6,REAL_1:53; then m+i<n+1 by A2,A3,A4,Def1;
then m+i<=n by NAT_1:38; then 1<=m+i & m+i<=len p
by A2,A4,AXIOMS:22,NAT_1:37;
then m+i in dom p by FINSEQ_3:27;
hence x in rng p by A5,A7,FUNCT_1:def 5;
end;
end;
now assume not (1<=m & m<=n+1 & n<=len p);
then c = {} by Def1; then rng c = {} by FINSEQ_1:27;
hence thesis by XBOOLE_1:2;
end;
hence thesis by A1;
end;
definition let D be set, p be FinSequence of D, m, n be Nat;
redefine func (m, n)-cut p -> 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,XBOOLE_1:1; 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:37;
then A5: len c +m = n+1 by A1,A3,Def1;
A6: now assume len c = 0;
then n+1<=n+0 by A2,A5; hence contradiction by REAL_1:53
;
end; A7: 0<=len c by NAT_1:18;
0<len c & 0+1=1 by A6,NAT_1:18;
hence c.1 = p.(m+0) by A1,A3,A4,Def1 .= p.m;
0+1<=len c by A6,A7,NAT_1:38; then consider i being Nat such that
A8: 0<=i & i<len c & len c =i+1 by Th1;
m+i = m+(len c -1) by A8,XCMPLX_1:26 .= n+1-1 by A5,XCMPLX_1:29 .= n by
XCMPLX_1:26;
hence c.(len c) = p.n by A1,A3,A4,A8,Def1;
end;
begin :: The glueing catenation
definition let p, q be FinSequence;
func p ^' q -> FinSequence equals
:Def2: 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;
A1: r = p^qc by Def2; assume
q<>{};
then len q <> 0 by FINSEQ_1:25; then 0<len q by NAT_1:19;
then 0+1<=len q by NAT_1:38; then 1+1<=len q +1 by REAL_1:55;
then len qc +(1+1) = len q + 1 by Def1;
then len qc +1+1 = len q + 1 by XCMPLX_1:1;
then A2: len qc +1 = len q by XCMPLX_1:2;
thus len r +1 = len p + len qc + 1 by A1,FINSEQ_1:35
.= len p + len q by A2,XCMPLX_1:1;
end;
theorem Th14:
1<=k & k<=len p implies (p^'q).k=p.k
proof
A1: p^'q = p^((2,len q)-cut q) by Def2;
assume that
A2: 1<=k and
A3: k<=len p; k in dom p by A2,A3,FINSEQ_3:27;
hence (p^'q).k=p.k by A1,FINSEQ_1:def 7;
end;
theorem Th15:
1<=k & k<len q implies (p^'q).(len p +k) = q.(k+1)
proof set qc = (2,len q)-cut q;
A1: p^'q = p^qc by Def2;
assume that
A2: 1<=k and
A3: k<len q;
per cases;
suppose q={}; then len q = 0 by FINSEQ_1:25;
hence thesis by A2,A3,AXIOMS:22;
suppose
q<>{}; then len q <> 0 by FINSEQ_1:25; then 0<len q by NAT_1:19;
then 0+1<=len q by NAT_1:38;
then A4: 1+1<=len q +1 by REAL_1:55;
then len qc +(1+1) = len q + 1 by Def1;
then len qc +1+1 = len q + 1 by XCMPLX_1:1;
then len qc +1 = len q by XCMPLX_1:2; then A5: k<=len qc by A3,NAT_1:38;
then A6: k in dom qc by A2,FINSEQ_3:27;
0+1<=k by A2; then consider i being Nat such that
A7: 0<=i & i<len qc & k=i+1 by A5,Th1;
thus (p^'q).(len p +k) = qc.k by A1,A6,FINSEQ_1:def 7
.= q.(1+1+i) by A4,A7,Def1
.= q.(k+1) by A7,XCMPLX_1:1;
end;
theorem Th16:
1<len q implies (p^'q).len (p^'q) = q.len q
proof set r = p^'q; set qc = (2,len q)-cut q; assume
A1: 1<len q; then len q <>0; then q<>{} by FINSEQ_1:25;
then len r +1-1=len p +len q -1 by Th13;
then A2: len r = len p + len q -1 by XCMPLX_1:26 .= len p +(len q -1) by
XCMPLX_1:29;
1+1<=len q +1 by A1,REAL_1:55; then len qc +(1+1) = len q + 1 by Def1
;
then len qc +1+1 = len q + 1 by XCMPLX_1:1;
then A3: len qc +1 = len q by XCMPLX_1:2;
then A4: len qc = len q -1 by XCMPLX_1:26;
1+1<=len q by A1,NAT_1:38;
then A5: 1+1-1<=len q -1 by REAL_1:49;
len qc < len q by A3,NAT_1:38;
hence r.len r = q.len q by A2,A3,A4,A5,Th15;
end;
theorem Th17: rng (p^'q) c= rng p \/ rng q
proof set r = p^'q; set qc = (2,len q)-cut q;
A1: r=p^qc by Def2;
let x be set; assume x in rng r;
then A2: x in rng p \/ rng qc by A1,FINSEQ_1:44;
A3: rng qc c= rng q by Th11;
x in rng p or x in rng qc by A2,XBOOLE_0:def 2;
hence x in rng p \/ rng q by A3,XBOOLE_0:def 2;
end;
definition let D be set, p, q be FinSequence of D;
redefine func p^'q -> FinSequence of D;
coherence proof
rng p c= D & rng q c= D by FINSEQ_1:def 4;
then A1: rng p \/ rng q c= D by XBOOLE_1:8
; rng (p^'q) c= rng p \/ rng q by Th17;
then rng (p^'q) c= D by A1,XBOOLE_1:1;
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;
A1: r=p^qc by Def2;
assume that
A2: p<>{} and
A3: q<>{} and
A4: p.len p = q.1;
len q <> 0 by A3,FINSEQ_1:25; then 0<len q by NAT_1:19;
then 0+1<=len q by NAT_1:38;
then A5: 1+1<=len q +1 by REAL_1:55;
then len qc +(1+1) = len q + 1 by Def1;
then len qc +1+1 = len q + 1 by XCMPLX_1:1;
then A6: len qc +1 = len q by XCMPLX_1:2;
now let x be set;
hereby assume x in rng r;
then A7: x in rng p \/ rng qc by A1,FINSEQ_1:44;
A8: rng qc c= rng q by Th11;
x in rng p or x in rng qc by A7,XBOOLE_0:def 2;
hence x in rng p \/ rng q by A8,XBOOLE_0:def 2;
end;
assume x in rng p \/ rng q;
then A9: x in rng p or x in rng q by XBOOLE_0:def 2;
assume
not x in rng r; then A10: not x in rng p \/ rng qc by A1,FINSEQ_1:44;
then A11: not x in rng p & not x in rng qc by XBOOLE_0:def 2;
consider y being set such that
A12: y in dom q & x=q.y by A9,A10,FUNCT_1:def 5,XBOOLE_0:def 2;
reconsider y as Nat by A12;
A13: 1<=y & y<=len q by A12,FINSEQ_3:27;
per cases by A13,REAL_1:def 5;
suppose A14: y=1; len p <>0 by A2,FINSEQ_1:25;
then 0<len p by NAT_1:19
;
then 0+1<=len p by NAT_1:38; then len p in dom p by FINSEQ_3:27;
hence contradiction by A4,A11,A12,A14,FUNCT_1:def 5;
suppose 1<y; then 1+1<=y by NAT_1:38; then consider i such that
A15: 1<=i & i<len q & y=i+1 by A13,Th1;
A16: 0+1<=i & i<=len qc by A6,A15,NAT_1:38
; then consider j such that
A17: 0<=j & j<len qc & i=j+1 by Th1;
A18: qc.(j+1) = q.(1+1+j) by A5,A17,Def1
.= q.y by A15,A17,XCMPLX_1:1;
i in dom qc by A16,FINSEQ_3:27; hence contradiction by A11,A12,A17,A18,
FUNCT_1:def 5;
end;
hence rng (p^'q) = rng p \/ rng q by TARSKI:2;
end;
begin :: Two valued alternating finsequences
definition let f be FinSequence;
attr f is TwoValued means
:Def3: card rng f = 2;
end;
Lm2: now set p = <*1, 2*>; 2 > 1;
hence len p > 1 by FINSEQ_1:61; thus 1 <> 2;
thus rng p = rng (<*1*>^<*2*>) by FINSEQ_1:def 9
.= rng<*1*>\/ rng<*2*> by FINSEQ_1:44 .= {1} \/ rng <*2*> by FINSEQ_1:55
.= {1} \/ {2} by FINSEQ_1:55 .= {1, 2} by ENUMSET1:41;
end;
theorem Th19:
p is TwoValued iff len p >1 & ex x,y being set st x<>y & rng p ={x, y} proof
hereby assume p is TwoValued; then card rng p = 2 by Def3;
then consider x,y being set such that
A1: x<>y & rng p={x,y} by GROUP_3:166;
thus len p >1 proof set l=len p; assume A2: len p<=1;
per cases by A2,CQC_THE1:2;
suppose l=0; then p={} by FINSEQ_1:25; hence contradiction by A1,FINSEQ_1:27
;
suppose A3: l=1; then 1 in dom p by FINSEQ_3:27;
then consider z being set such that
A4: [1,z] in p by RELAT_1:def 4;
z=p.1 by A4,FUNCT_1:8; then p=<*z*> by A3,FINSEQ_1:57;
then rng p = {z} by FINSEQ_1:56; then z=x & z=y by A1,ZFMISC_1:8;
hence contradiction by A1;
end;
thus ex x,y being set st x<>y & rng p ={x, y} by A1;
end;
assume len p >1;
given x, y being set such that
A5: x<>y & rng p = {x, y}; card rng p = 2 by A5,CARD_2:76;
hence p is TwoValued by Def3;
end;
then Lm3: <*1, 2*> is TwoValued by Lm2;
Lm4: now set p = <*1, 2*>;
let i be Nat;
assume that
A1: 1<=i and
A2: (i+1)<=len p;
i+1<=1+1 by A2,FINSEQ_1:61;
then i<=1 by REAL_1:53; then i = 1 by A1,AXIOMS:21;
then p.i = 1 & p.(i+1) = 2 by FINSEQ_1:61;
hence p.i <> p.(i+1);
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;
Lm5: <*1, 2*> is Alternating by Def4,Lm4;
definition
cluster TwoValued Alternating FinSequence;
existence by Lm3,Lm5;
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: P[0];
A5: for k being Nat st P[k] holds P[k+1]
proof let k be Nat;
assume
A6: 1<=k & k<=len a1 implies a1.k = a2.k;
assume that
A7: 1<=k+1 and
A8: k+1<=len a1;
A9: k+1 in dom a1 by A7,A8,FINSEQ_3:27;
A10: 0=k or 0<k & 0+1=1
by NAT_1:19;
per cases by A10,NAT_1:38;
suppose 0 = k; hence a1.(k+1) = a2.(k+1) by A3;
suppose
A11: 1<=k;
k<=len a1 by A8,NAT_1:38;
then A12: k in dom a1 by A11,FINSEQ_3:27;
A13: dom a1 = Seg len a1 & dom a2 = Seg len a2 by FINSEQ_1:def 3;
consider X, Y being set such that
A14: X <> Y & rng a1 = { X, Y } by Th19;
a1.k in rng a1 & a2.k in rng a2 &
a1.(k+1) in rng a1 & a2.(k+1) in rng a2
by A1,A9,A12,A13,FUNCT_1:def 5;
then (a1.k=X or a1.k=Y) & (a2.k=X or a2.k=Y) & (a1.(k+1)=X or a1.(k+1)=
Y) &
(a2.(k+1) = X or a2.(k+1) = Y) by A2,A14,TARSKI:def 2;
hence a1.(k+1) = a2.(k+1) by A1,A6,A8,A11,Def4,NAT_1:38;
end;
for i being Nat holds P[i] from Ind (A4, A5);
hence a1 = a2 by A1,FINSEQ_1:18;
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: P[0];
A5: for k being Nat st P[k] holds P[k+1]
proof let k be Nat; assume
A6: 1<=k & k<=len a1 implies a1.k <> a2.k;
assume that
A7: 1<=k+1 and
A8: k+1<=len a1;
A9: k+1 in dom a1 by A7,A8,FINSEQ_3:27;
A10: 0=k or 0<k & 0+1=1 by NAT_1:19;
per cases by A10,NAT_1:38;
suppose 0 = k; hence a1.(k+1) <> a2.(k+1) by A1,A2,A3,Th20;
suppose
A11: 1<=k;
k<=len a1 by A8,NAT_1:38;
then A12: k in dom a1 by A11,FINSEQ_3:27;
A13: dom a1 = Seg len a1 & dom a2 = Seg len a2 by FINSEQ_1:def 3;
consider X, Y being set such that
A14: X <> Y & rng a1 = { X, Y } by Th19;
a1.k in rng a1 & a2.k in rng a2 &
a1.(k+1) in rng a1 & a2.(k+1) in rng a2
by A2,A9,A12,A13,FUNCT_1:def 5;
then (a1.k=X or a1.k=Y) & (a2.k=X or a2.k=Y) & (a1.(k+1)=X or a1.(k+1)=
Y) &
(a2.(k+1) = X or a2.(k+1) = Y) by A3,A14,TARSKI:def 2;
hence a1.(k+1) <> a2.(k+1) by A2,A6,A8,A11,Def4,NAT_1:38;
end;
thus for i holds P[i] from Ind (A4, A5);
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;
A9: i in dom a by A7,A8,FINSEQ_3:27;
A10: dom a=Seg len a & dom a1=Seg len a1 & dom a2=Seg len a2 by FINSEQ_1:def 3;
consider X, Y being set such that
A11: X <> Y & rng a = { X, Y } by Th19;
a.i in rng a & a1.i in rng a1 & a2.i in rng a2
by A2,A4,A9,A10,FUNCT_1:def 5;
then (a.i=X or a.i=Y)&(a1.i=X or a1.i=Y)&(a2.i=X or a2.i=Y)
by A3,A5,A11,TARSKI:def 2;
hence a.i = a2.i by A1,A2,A3,A4,A5,A6,A7,A8,Th21;
end; hence a = a2 by A2,A4,FINSEQ_1:18;
end;
theorem Th23:
X <> Y & n > 1 implies ex a1 st rng a1 = {X, Y} & len a1 = n & a1.1 = X
proof assume that
A1: X <> Y and
A2: n > 1; set p = <*X, Y*>;
A3: p.1 = X & p.2 = Y by FINSEQ_1:61;
deffunc F(Nat,Nat) = 3-'$2;
consider f1 being Function of NAT, NAT such that
A4: f1.0=2 & for n holds f1.(n+1)=F(n,f1.n) from LambdaRecExD;
defpred P[Nat] means (f1.$1=1 or f1.$1=2) & f1.$1<>f1.($1+1);
A5: now
thus A6: 3-'2 =1+2-2 by BINARITH:def 3.=1;
thus A7: 3-'1=2+1-1 by BINARITH:def 3.=2;
thus f1.(0+1) = 1 by A4,A6;
hence f1.(1+1) = 2 by A4,A7;
end;
then A8: P[0] by A4;
A9: for i being Nat st P[i] holds P[i+1]
proof let i be Nat such that
A10: (f1.i = 1 or f1.i = 2) & f1.i <> f1.(i+1);
thus (f1.(i+1)=1 or f1.(i+1) = 2) by A4,A5,A10;
hence f1.(i+1) <> f1.((i+1)+1) by A4,A5;
end;
A11: for i holds P[i] from Ind (A8, A9);
deffunc F(Nat) = p.(f1.$1);
consider p1 being FinSequence such that
A12: len p1 = n & for k st k in Seg n holds p1.k= F(k) from SeqLambda;
A13: now let y be set;
hereby assume y in {X, Y}; then A14: y = X or y = Y by TARSKI:def 2;
1+1<=n by A2,NAT_1:38;
then 1<=1&1<=len p1&1<=2&2<=len p1 by A12,AXIOMS:22;
then A15: 1 in Seg len p1&2 in Seg len p1 by FINSEQ_1:3;
then A16: p1.1=X & p1.2=Y by A3,A5,A12;
1 in dom p1 & 2 in dom p1 by A15,FINSEQ_1:def 3;
hence ex x being set st x in dom p1 & y = p1.x by A14,A16;
end;
given x being set such that
A17: x in dom p1 & y = p1.x; x in Seg len p1 by A17,FINSEQ_1:def 3;
then x in { k : 1<=k & k<=len p1} by FINSEQ_1:def 1;
then consider x' being Nat such that
A18: x'=x & 1<=x' & x'<=len p1; x' in Seg n by A12,A18,FINSEQ_1:3;
then p1.x' = p.(f1.x') & (f1.x' = 1 or f1.x' = 2) by A11,A12;
hence y in {X, Y} by A3,A17,A18,TARSKI:def 2;
end;
then rng p1 = {X, Y} by FUNCT_1:def 5;
then reconsider p1 as TwoValued FinSequence by A1,A2,A12,Th19;
now let i be Nat;
assume that
A19: 1<=i and
A20: (i+1)<=len p1;
1<=i & i<=n & 1<=(i+1) & (i+1)<=n by A12,A19,A20,NAT_1:38;
then i in Seg n & (i+1) in Seg n by FINSEQ_1:3;
then p1.i=p.(f1.i)&p1.(i+1)=p.(f1.(i+1)) & (f1.i=1 or f1.i=2) &
(f1.(i+1)=1 or f1.(i+1)=2) & f1.i<>f1.(i+1) by A11,A12;
hence p1.i <> p1.(i+1) by A1,A3;
end;
then reconsider p1 as TwoValued Alternating FinSequence by Def4;
take p1; thus rng p1 = {X, Y} by A13,FUNCT_1:def 5; thus len p1 = n by A12;
1 in Seg n by A2,FINSEQ_1:3;
hence p1.1 = X by A3,A5,A12;
end;
begin :: Finite subsequences of finite sequences
definition let X; let fs be FinSequence of X;
mode FinSubsequence of fs -> FinSubsequence means
:Def5: it c= fs;
existence proof reconsider IT = fs as FinSubsequence by FINSEQ_1:68;
take IT; thus thesis;
end;
end;
reserve ss for FinSubsequence;
theorem Th24: ss is FinSequence implies Seq ss = ss proof assume
ss is FinSequence;
then reconsider ss'=ss as FinSequence; consider k such that
A1: dom ss' = Seg k by FINSEQ_1:def 2;
A2: len ss' <= k by A1,FINSEQ_1:def 3;
Seq ss = ss* Sgm Seg k by A1,FINSEQ_1:def 14
.= ss* idseq k by FINSEQ_3:54 .= ss by A2,FINSEQ_2:64;
hence thesis;
end;
canceled;
theorem Th26:
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:44;
then rng (g^h) c= dom f by A1,A2,XBOOLE_1:8;
hence
A6: len fgh = len (g^h) by A5,FINSEQ_2:33
.= len g + len h by FINSEQ_1:35;
A7: len fg = len g by A1,A3,FINSEQ_2:33;
A8: len fh = len h by A2,A4,FINSEQ_2:33;
A9: dom fgh = Seg (len g +len h) by A6,FINSEQ_1:def 3;
A10: dom fg = dom g by A1,A3,RELAT_1:46;
A11: dom fh = dom h by A2,A4,RELAT_1:46;
thus len (fg^fh) = len g + len h by A7,A8,FINSEQ_1:35;
let j; assume
A12: j in Seg (len g + len h);
then A13: 1<=j & j<=len g + len h by FINSEQ_1:3;
per cases;
suppose j<=len g;
then A14: j in dom g by A13,FINSEQ_3:27;
thus fgh.j = f.((g^h).j) by A5,A9,A12,FUNCT_1:22
.= f.(g.j) by A14,FINSEQ_1:def 7
.= fg.j by A3,A14,FUNCT_1:23
.= (fg^fh).j by A10,A14,FINSEQ_1:def 7;
suppose len g < j; then len g +1 <=j by NAT_1:38;
then A15: 1<=j-len g by REAL_1:84; then 0<=j-len g by AXIOMS:22;
then j-'len g = j-len g by BINARITH:def 3;
then reconsider j' = j-len g as Nat;
A16: j = len g + j' by XCMPLX_1:27;
then j'<=len h by A13,REAL_1:53;
then A17: j' in dom h by A15,FINSEQ_3:27;
thus fgh.j = f.((g^h).j) by A5,A9,A12,FUNCT_1:22
.= f.(h.j') by A16,A17,FINSEQ_1:def 7
.= fh.j' by A4,A17,FUNCT_1:23
.= (fg^fh).j by A7,A11,A16,A17,FINSEQ_1:def 7;
end;
hence fgh = fg^fh by FINSEQ_2:10;
end;
reserve fs, fs1, fs2 for FinSequence of X,
fss, fss2 for FinSubsequence of fs;
theorem Th27: dom fss c= dom fs & rng fss c= rng fs
proof fss c= fs by Def5; hence thesis by RELAT_1:25; end;
theorem Th28: fs is FinSubsequence of fs
proof reconsider fs'=fs as FinSubsequence by FINSEQ_1:68; fs' c= fs;
hence thesis by Def5;
end;
theorem Th29: fss|Y is FinSubsequence of fs proof
consider k such that
A1: dom fss c= Seg k by FINSEQ_1:def 12;
dom (fss|Y) c= dom fss by RELAT_1:89;
then dom (fss|Y) c= Seg k by A1,XBOOLE_1:1;
then reconsider f = fss|Y as FinSubsequence by FINSEQ_1:def 12;
f c= fss & fss c= fs by Def5,RELAT_1:88; then f c= fs by XBOOLE_1:1;
hence thesis by Def5;
end;
theorem Th30:
for fss1 being FinSubsequence 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 FinSubsequence of fs1 such that
A1: Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss|rng((Sgm dom fss)|dom fss1);
consider k such that
A2: dom fs = Seg k by FINSEQ_1:def 2;
A3: dom fss c= Seg k by A2,Th27;
A4: dom fss2 c= Seg k by A2,Th27;
A5: dom fss1 c= dom fs1 by Th27; consider l such that
A6: dom fs1 = Seg l by FINSEQ_1:def 2;
(Sgm dom fss)|dom fss1 c= Sgm dom fss by RELAT_1:88;
then A7: dom ((Sgm dom fss)|dom fss1) c= dom (Sgm dom fss) &
rng ((Sgm dom fss)|dom fss1) c= rng (Sgm dom fss) by RELAT_1:25;
then A8: rng((Sgm dom fss)|dom fss1) c= dom fss by A3,FINSEQ_1:def 13;
then A9: dom fss2 = rng((Sgm dom fss)|dom fss1) by A1,RELAT_1:91;
A10: rng Sgm dom fss c= dom fss by A3,FINSEQ_1:def 13;
A11: dom fs1 = dom (fss*Sgm dom fss) by A1,FINSEQ_1:def 14
.= dom Sgm dom fss by A10,RELAT_1:46;
A12: rng Sgm dom fss2 = dom fss2 by A4,FINSEQ_1:def 13;
A13: rng Sgm dom fss1 = dom fss1 by A5,A6,FINSEQ_1:def 13;
reconsider d1 = dom fss1 as finite set by A5,A6,FINSET_1:13;
reconsider d2 = dom fss2 as finite set by A4,FINSET_1:13;
now take Z = (Sgm dom fss)|dom fss1;
A14: dom Z = dom fss1 by A5,A11,RELAT_1:91;
hereby let x be set; assume
A15: x in d1;
take y = Z.x;
thus y in d2 by A9,A14,A15,FUNCT_1:def 5;
thus [x,y] in Z by A14,A15,FUNCT_1:8;
end;
hereby let y be set; assume y in d2;
then consider x such that
A16: x in dom Z & y = Z.x by A9,FUNCT_1:def 5;
take x;
thus x in d1 & [x,y] in Z by A5,A11,A16,FUNCT_1:8,RELAT_1:91;
end;
let x,y,z,u be set;
assume that
A17: [x,y] in Z and
A18: [z,u] in Z;
A19: x in dom Z & y = Z.x & z in dom Z & u = Z.z by A17,A18,FUNCT_1:8;
then A20: x in Seg l & z in Seg l by A5,A6,A14;
A21: y = (Sgm dom fss).x & u = (Sgm dom fss).z by A19,FUNCT_1:70;
y in rng Z & u in rng Z by A19,FUNCT_1:def 5;
then y in dom fss & u in dom fss by A8;
then A22: y in Seg k & u in Seg k by A3;
thus x=z implies y=u by A19;
assume
A23: y=u;
assume
A24: x<>z;
reconsider x,z as Nat by A20;
reconsider y,u as Nat by A22;
A25: 1<=x & x<=len Sgm dom fss & 1<=z & z<=
len Sgm dom fss by A7,A19,FINSEQ_3:27;
per cases by A24,REAL_1:def 5;
suppose x<z; then y < u by A3,A21,A25,FINSEQ_1:def 13;
hence contradiction by A23;
suppose z<x; then u < y by A3,A21,A25,FINSEQ_1:def 13;
hence contradiction by A23;
end; then d1,d2 are_equipotent by TARSKI:def 6;
then card d1 = card d2 by CARD_1:81;
then A26: dom Sgm d1 = Seg card d1 &
dom Sgm d2 = Seg card d1 by A4,A5,A6,FINSEQ_3:45;
now
now let x be set;
hereby assume x in dom fs2;
then x in dom (fss1*Sgm dom fss1) by A1,FINSEQ_1:def 14;
then A27: x in dom Sgm dom fss2 by A26,FUNCT_1:21;
then (Sgm dom fss2).x in dom fss2 by A12,FUNCT_1:def 5;
then x in dom (fss2*Sgm dom fss2) by A27,FUNCT_1:21;
hence x in dom Seq fss2 by FINSEQ_1:def 14;
end;
assume x in dom Seq fss2;
then x in dom (fss2*Sgm dom fss2) by FINSEQ_1:def 14;
then A28: x in dom Sgm dom fss1 by A26,FUNCT_1:21;
then (Sgm dom fss1).x in dom fss1 by A13,FUNCT_1:def 5;
then x in dom (fss1*Sgm dom fss1) by A28,FUNCT_1:21;
hence x in dom fs2 by A1,FINSEQ_1:def 14;
end;
hence
A29: dom fs2 = dom Seq fss2 by TARSKI:2;
thus dom fs2 = dom fs2;
let k; assume
A30: k in dom fs2;
then A31: k in dom (fss1*Sgm dom fss1) by A1,FINSEQ_1:def 14;
A32: k in dom (fss2*Sgm dom fss2) by A29,A30,FINSEQ_1:def 14;
A33: k in dom Sgm dom fss1 by A31,FUNCT_1:21;
A34: (Sgm dom fss1).k in dom fss1 by A31,FUNCT_1:21;
dom fss1 c= dom Seq fss by A1,Th27;
then dom fss1 c= dom (fss*Sgm dom fss) by FINSEQ_1:def 14;
then A35: (Sgm dom fss1).k in dom Sgm dom fss by A34,FUNCT_1:21;
fss1 c= Seq fss by A1,Def5;
then A36: fss1.((Sgm dom fss1).k) = (Seq fss).((Sgm dom fss1).k) by A34,
GRFUNC_1:8;
(Sgm dom fss1).k in dom fss1 by A31,FUNCT_1:21;
then A37: k in dom ((Sgm dom fss)*(Sgm dom fss1)) by A5,A11,A33,FUNCT_1:21;
(Sgm dom fss2).k = ((Sgm dom fss)*(Sgm dom fss1)).k by A3,A5,A9,A11,Th3;
then A38: (Sgm dom fss2).k = (Sgm dom fss).((Sgm dom fss1).k) by A37,
FUNCT_1:22;
A39: fss2 c= fss by A1,RELAT_1:88;
A40: (Sgm dom fss2).k in dom fss2 by A32,FUNCT_1:21;
thus (Seq fss2).k = (fss2*Sgm dom fss2).k by FINSEQ_1:def 14
.= fss2.((Sgm dom fss2).k) by A32,FUNCT_1:22
.= fss.((Sgm dom fss).((Sgm dom fss1).k)) by A38,A39,A40,GRFUNC_1:8
.= (fss*Sgm dom fss).((Sgm dom fss1).k) by A35,FUNCT_1:23
.= fss1.((Sgm dom fss1).k) by A36,FINSEQ_1:def 14.= (fss1*Sgm dom fss1).k
by A31,FUNCT_1:22
.= fs2.k by A1,FINSEQ_1:def 14;
end;
hence Seq fss2 = fs2 by FINSEQ_1:17;
end;
begin :: Vertex sequences induced by chains
reserve G for Graph;
definition let G;
cluster the Vertices of G -> non empty;
coherence by GRAPH_1:def 1;
end;
reserve v, v1, v2, v3, v4 for Element of the Vertices of G,
e for set;
theorem Th31: e joins v1,v2 implies e joins v2,v1
proof assume e joins v1,v2;
then ((the Source of G).e = v1 & (the Target of G).e = v2) or
((the Source of G).e = v2 & (the Target of G).e = v1) by GRAPH_1:def 9;
hence e joins v2,v1 by GRAPH_1:def 9;
end;
theorem Th32:
e joins v1,v2 & e joins v3,v4 implies v1=v3 & v2=v4 or v1=v4 & v2=v3 proof
assume that
A1: e joins v1,v2 and
A2: e joins v3,v4;
(((the Source of G).e = v1 & (the Target of G).e = v2) or
((the Source of G).e = v2 & (the Target of G).e = v1)) &
(((the Source of G).e = v3 & (the Target of G).e = v4) or
((the Source of G).e = v4 & (the Target of G).e = v3))
by A1,A2,GRAPH_1:def 9;
hence v1=v3 & v2=v4 or v1=v4 & v2=v3;
end;
reserve vs, vs1, vs2 for FinSequence of the Vertices of G,
c, c1, c2 for Chain of G;
definition let G;
cluster empty Chain of G;
existence proof {} is Chain of G by GRAPH_1:14; hence thesis; end;
end;
definition let G, X;
func G-VSet X -> set equals
:Def6: { v: ex e being Element of the Edges 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
:Def7:
len vs = len c + 1 &
for n st 1<=n & n<=len c holds c.n joins vs/.n, vs/.(n+1);
end;
canceled;
theorem Th34:
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,Def7;
A4: G-VSet rng c = { v: ex e being Element of the Edges of G st e in rng c &
(v = (the Source of G).e or v = (the Target of G).e) } by Def6;
now let y be set;
hereby assume
y in G-VSet rng c;
then consider v being Element of the Vertices of G such that
A5: v=y & ex e being Element of the Edges of G st e in rng c &
(v = (the Source of G).e or v = (the Target of G).e) by A4;
consider e being Element of the Edges of G such that
A6: e in rng c & (v = (the Source of G).e or v = (the Target of G).e) by A5;
consider x being set such that
A7: x in dom c & e = c.x by A6,FUNCT_1:def 5;
reconsider x as Nat by A7;
A8: 1<=x & x<=len c by A7,FINSEQ_3:27;
then A9: 1<=x+1 & x+1<=len vs & x<=len vs by A3,NAT_1:37,REAL_1:55;
set v1 = vs/.x; set v2 = vs/.(x+1);
A10: v1 = vs.x & v2 = vs.(x+1) by A8,A9,FINSEQ_4:24;
c.x joins v1, v2 by A2,A8,Def7;
then A11: v = v1 or v = v2 by A6,A7,GRAPH_1:def 9;
x in dom vs & x+1 in dom vs by A8,A9,FINSEQ_3:27;
hence y in rng vs by A5,A10,A11,FUNCT_1:def 5;
end; assume y in rng vs; then consider x being set such that
A12: x in dom vs & y = vs.x by FUNCT_1:def 5;
reconsider x as Nat by A12;
A13: 1<=x & x<=len vs by A12,FINSEQ_3:27;
per cases by A3,A13,NAT_1:26;
suppose
A14: x<=len c;
then A15: 1<=x+1 & x+1<=len vs & x<=len vs by A3,NAT_1:37,REAL_1:55;
x in dom c by A13,A14,FINSEQ_3:27;
then c.x in rng c & rng c c= the Edges of G by FINSEQ_1:def 4,FUNCT_1:def 5
;
then reconsider e = c.x as Element of the Edges of G;
set v1 = vs/.x; set v2 = vs/.(x+1);
A16: v1 = vs.x & v2 = vs.(x+1) by A13,A15,FINSEQ_4:24;
c.x joins v1, v2 by A2,A13,A14,Def7;
then A17: 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 by GRAPH_1:def 9;
x in dom c by A13,A14,FINSEQ_3:27;
then e in rng c by FUNCT_1:def 5;
hence y in G-VSet rng c by A4,A12,A16,A17;
suppose
A18: x=len c+1; set l = len c;
l <> 0 by A1,FINSEQ_1:25; then 0<l & 0+1=1 by NAT_1:19;
then A19: 1<=l & l<=l+1 by NAT_1:38;
then l in dom c by FINSEQ_3:27;
then c.l in rng c & rng c c= the Edges of G by FINSEQ_1:def 4,FUNCT_1:def 5
;
then reconsider e = c.l as Element of the Edges of G;
set v1 = vs/.l; set v2 = vs/.(l+1);
A20: v1 = vs.l & v2 = vs.(l+1) by A3,A13,A18,A19,FINSEQ_4:24;
c.l joins v1, v2 by A2,A19,Def7;
then A21: 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 by GRAPH_1:def 9;
l in dom c by A19,FINSEQ_3:27;
then e in rng c by FUNCT_1:def 5;
hence y in G-VSet rng c by A4,A12,A18,A20,A21;
end;
hence G-VSet rng c = rng vs by TARSKI:2;
end;
theorem Th35: <*v*> is_vertex_seq_of {} proof
A1: len {} = 0 by FINSEQ_1:25;
hence len <*v*> = len {} +1 by FINSEQ_1:57;
thus thesis by A1,AXIOMS:22;
end;
theorem Th36: ex vs st vs is_vertex_seq_of c proof consider p such that
A1: len p = len c + 1 &
(for n st 1<=n & n<=len p holds p.n in the Vertices of G) &
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 11;
rng p c= the Vertices of G proof let y be set; assume y in rng p;
then consider x being set such that
A2: x in dom p & y = p.x by FUNCT_1:def 5;
reconsider n=x as Nat by A2;
1<=n & n<=len p by A2,FINSEQ_3:27; hence y in the Vertices of G by A1,A2
;
end;
then reconsider p as FinSequence of the Vertices of G by FINSEQ_1:def 4;
take p;
thus len p = len c + 1 by A1;
let n; assume that
A3: 1<=n and
A4: n<=len c; consider v1,v2 such that
A5: v1=p.n & v2=p.(n+1) & c.n joins v1,v2 by A1,A3,A4;
A6: 1<=n+1 & len c <=len c +1 & n+1<=len c +1 by A4,NAT_1:37,REAL_1:55;
n<=len p by A1,A4,NAT_1:37;
then p/.n=p.n & p/.(n+1)=p.(n+1) by A1,A3,A6,FINSEQ_4:24;
hence c.n joins p/.n, p/.(n+1) by A5;
end;
theorem Th37:
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; assume
A4: vs1 <> vs2;
set SG = the Source of G; set TG = the Target of G;
A5: len vs1 = len c +1 & len vs2 = len c +1 by A2,A3,Def7;
defpred P[Nat] means $1 in dom vs1 & vs1.$1<>vs2.$1;
A6: Seg len vs1 = dom vs1 & Seg len vs2 = dom vs2 by FINSEQ_1:def 3;
then A7: ex j st P[j] by A4,A5,FINSEQ_2:10;
consider k such that
A8: P[k] and
A9: for n st P[n] holds k<=n from Min (A7);
A10: 1<=k & k<=len c +1 by A5,A8,FINSEQ_3:27;
per cases by A10,REAL_1:def 5;
suppose
A11: k=1;
hence vs1.1 <> vs2.1 by A8; let vs; assume
A12: vs is_vertex_seq_of c;
then A13: len vs = len c +1 by Def7;
len c <>0 by A1,FINSEQ_1:25; then 0+1=1 & 0<len c by NAT_1:19;
then A14: 1<=len c by NAT_1:38;
A15: 1<=len vs1 by A5,NAT_1:37;
A16: Seg len vs = dom vs by FINSEQ_1:def 3;
set v1 = vs/.1; set v2 = vs/.(1+1);
set v11 = vs1/.1; set v12 = vs1/.(1+1);
set v21 = vs2/.1;
A17: v1=vs.1 & v11=vs1.1 & v21=vs2.1 by A5,A13,A15,FINSEQ_4:24;
A18: c.1 joins vs/.1, vs/.(1+1) by A12,A14,Def7;
A19: c.1 joins vs1/.1, vs1/.(1+1) by A2,A14,Def7;
A20: c.1 joins vs2/.1, vs2/.(1+1) by A3,A14,Def7;
A21: v1=v11 & v2=v12 or v1=v12 & v2=v11 by A18,A19,Th32;
thus vs = vs1 or vs = vs2 proof
per cases by A8,A11,A17,A18,A20,A21,Th32;
suppose
A22: v1 = v11;
now thus len vs = len vs; thus len vs1 = len vs by A5,A12,Def7;
defpred P[Nat] means $1 in dom vs implies vs.$1=vs1.$1;
A23: P[0] by FINSEQ_3:27;
A24: for i st P[i] holds P[i+1]
proof let i; assume
A25: i in dom vs implies vs.i=vs1.i; assume i+1 in dom vs;
then A26: 1<=i+1 & i+1<=len vs by FINSEQ_3:27;
A27: (0=i or 0<i) & 0+1=1 by NAT_1:19;
per cases by A27,NAT_1:38;
suppose i=0;
hence vs.(i+1) = vs1.(i+1) by A17,A22;
suppose
A28: 1<=i;
A29: i<=len c by A13,A26,REAL_1:53;
then A30: i<=len vs by A13,NAT_1:37;
set v1 = vs/.i; set v2 = vs/.(i+1);
set v11 = vs1/.i; set v12 = vs1/.(i+1);
A31: v1=vs.i & v11=vs1.i & v2=vs.(i+1) & v12=vs1.(i+1) by A5,A13,A26,A28,A30,
FINSEQ_4:24;
A32: c.i joins vs/.i, vs/.(i+1) by A12,A28,A29,Def7;
c.i joins vs1/.i, vs1/.(i+1) by A2,A28,A29,Def7;
then v1=v11 & v2=v12 or v1=v12 & v2=v11 by A32,Th32;
hence vs.(i+1) = vs1.(i+1) by A25,A28,A30,A31,FINSEQ_3:27;
end;
thus for i holds P[i] from Ind (A23, A24);
end;
hence thesis by A16,FINSEQ_2:10;
suppose
A33: v1 = v21;
now thus len vs = len vs; thus len vs2 = len vs by A5,A12,Def7;
defpred P[Nat] means $1 in dom vs implies vs.$1=vs2.$1;
A34: P[0] by FINSEQ_3:27;
A35: for i st P[i] holds P[i+1]
proof let i; assume
A36: i in dom vs implies vs.i=vs2.i; assume i+1 in dom vs;
then A37: 1<=i+1 & i+1<=len vs by FINSEQ_3:27;
A38: (0=i or 0<i) & 0+1=1 by NAT_1:19;
per cases by A38,NAT_1:38;
suppose i=0;
hence vs.(i+1) = vs2.(i+1) by A17,A33;
suppose
A39: 1<=i;
A40: i<=len c by A13,A37,REAL_1:53;
then A41: i<=len vs by A13,NAT_1:37;
set v1 = vs/.i; set v2 = vs/.(i+1);
set v11 = vs2/.i; set v12 = vs2/.(i+1);
A42: v1=vs.i & v11=vs2.i & v2=vs.(i+1) & v12=vs2.(i+1) by A5,A13,A37,A39,A41,
FINSEQ_4:24;
A43: c.i joins vs/.i, vs/.(i+1) by A12,A39,A40,Def7;
c.i joins vs2/.i, vs2/.(i+1) by A3,A39,A40,Def7;
then v1=v11 & v2=v12 or v1=v12 & v2=v11 by A43,Th32;
hence vs.(i+1) = vs2.(i+1) by A36,A39,A41,A42,FINSEQ_3:27;
end;
thus for i holds P[i] from Ind (A34, A35);
end;
hence thesis by A16,FINSEQ_2:10;
end;
suppose 1<k;
then 1+1<=k by NAT_1:38; then consider k1 being Nat such that
A44: 1<=k1 & k1<k & k=k1+1 by Th1;
A45: k<=len vs1 by A8,FINSEQ_3:27;
then A46: k1<=len c by A5,A44,REAL_1:53;
A47: k1<=len vs1 by A44,A45,AXIOMS:22;
then A48: k1 in dom vs1 by A44,FINSEQ_3:27;
A49: vs1/.k1=vs1.k1 & vs1/.k=vs1.k &
vs2/.k1=vs2.k1 & vs2/.k=vs2.k
by A5,A6,A8,A44,A47,FINSEQ_4:24,def 4;
A50: c.k1 joins vs1/.k1, vs1/.(k1+1) by A2,A44,A46,Def7;
c.k1 joins vs2/.k1, vs2/.(k1+1) by A3,A44,A46,Def7;
then (SG.(c.k1)=vs1/.k1 & TG.(c.k1)=vs1/.k or
SG.(c.k1)=vs1/.k & TG.(c.k1)=vs1/.k1) &
(SG.(c.k1)=vs2/.k1 & TG.(c.k1)=vs2/.k or
SG.(c.k1)=vs2/.k & TG.(c.k1)=vs2/.k1) by A44,A50,GRAPH_1:def 9;
hence thesis by A8,A9,A44,A48,A49;
end;
definition let G; let c be FinSequence;
pred c alternates_vertices_in G means
:Def8: len c>=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 Th38: 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;
let k; assume
A3: k in dom c;
then A4: 1<=k & k<=len c by FINSEQ_3:27;
set SG = (the Source of G); set TG = (the Target of G);
set px = vs/.k; set px1 = vs/.(k+1);
len vs = len c +1 by A2,Def7;
then k<=len vs & 1<=k+1 & k+1<=len vs by A4,NAT_1:37,REAL_1:55;
then A5: px = vs.k & px1 = vs.(k+1) by A4,FINSEQ_4:24;
c.k joins px, px1 by A2,A4,Def7;
then TG.(c.k)=px1 & SG.(c.k)=px or TG.(c.k)=px & SG.(c.k)=px1 by GRAPH_1:def
9;
hence vs.k <> vs.(k+1) by A1,A3,A5,Def8;
end;
theorem Th39: 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;
c <>{} proof assume not thesis; then len c = 0 by FINSEQ_1:25;
hence contradiction by A1,Def8; end;
then G-VSet rng c = rng vs by A2,Th34;
then card rng vs = 2 by A1,Def8;
then consider x, y being set such that
A3: x<>y & rng vs={x,y} by GROUP_3:166;
set SG = (the Source of G); set TG = (the Target of G);
set px = vs/.1; set px1 = vs/.(1+1);
A4: 1<=len c by A1,Def8;
len vs = len c +1 by A2,Def7;
then A5: 1<=len vs & 1<=1+1 & 1+1<=len vs by A4,NAT_1:37,REAL_1:55;
then A6: px = vs.1 & px1 = vs.(1+1) by FINSEQ_4:24;
c.1 joins px, px1 by A2,A4,Def7;
then A7: TG.(c.1)=px1 & SG.(c.1)=px or TG.(c.1)=px & SG.(c.1)=px1 by GRAPH_1:
def 9;
1 in dom vs & 1+1 in dom vs by A5,FINSEQ_3:27;
then vs.1 in rng vs & vs.(1+1) in rng vs by FUNCT_1:def 5;
then A8: (vs.1 = x or vs.1 = y) & (vs.(1+1) = x or vs.(1+1) = y) by A3,TARSKI:
def 2
;
1 in dom c by A4,FINSEQ_3:27;
hence rng vs = {(the Source of G).(c.1), (the Target of G).(c.1)}
by A1,A3,A6,A7,A8,Def8;
end;
theorem Th40: 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;
set SG = (the Source of G); set TG = (the Target of G);
A3: 1<=len c & Card (G-VSet rng c) = 2 &
for n st n in dom c holds SG.(c.n) <> TG.(c.n) by A1,Def8;
c <>{} proof assume not thesis; then len c = 0 by FINSEQ_1:25;
hence contradiction by A1,Def8; end;
then A4: card rng vs = 2 by A2,A3,Th34;
A5: len vs = len c + 1 &
for n st 1<=n & n<=len c holds c.n joins vs/.n,vs/.(n+1)
by A2,Def7;
now let k be Nat; assume that
A6: 1<=k and
A7: (k+1)<=len vs;
k<=len c by A5,A7,REAL_1:53; then k in dom c by A6,FINSEQ_3:27;
hence vs.k <> vs.(k+1) by A1,A2,Th38;
end; hence vs is TwoValued Alternating FinSequence
by A4,Def3,Def4;
end;
theorem Th41: 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 assume
A1: c alternates_vertices_in G;
then A2: 1<=len c by Def8;
consider p1 being FinSequence of the Vertices of G such that
A3: p1 is_vertex_seq_of c by Th36;
A4: len p1 = len c + 1 by A3,Def7;
then A5: len p1 > 1 by A2,NAT_1:38;
set X = (the Source of G).(c.1); set Y = (the Target of G).(c.1);
A6: rng p1 = {X, Y} by A1,A3,Th39;
A7: p1 is TwoValued Alternating FinSequence by A1,A3,Th40;
A8: 1 in dom c & 1+1=2 by A2,FINSEQ_3:27;
then A9: p1.1 <> p1.2 by A1,A3,Th38;
then consider p2 being TwoValued Alternating FinSequence such that
A10: rng p2 = {p1.2, p1.1} & len p2 = len p1 & p2.1=p1.2 by A5,Th23;
A11: dom p1 = dom p2 by A10,FINSEQ_3:31;
1+1<=len p1 by A5,NAT_1:38;
then 1<=len p1 & 2<=len p1 by NAT_1:38;
then 1 in dom p1 & 2 in dom p1 by FINSEQ_3:27;
then p1.1 in rng p1 & p1.2 in rng p1 by FUNCT_1:def 5;
then A12: (p1.1 = X or p1.1 = Y) & (p1.2 = X or p1.2 = Y) & {X, Y} = {Y, X}
by A6,TARSKI:def 2;
then rng p2 c= the Vertices of G by A1,A3,A6,A8,A10,Th38,FINSEQ_1:def 4;
then reconsider p2 as FinSequence of the Vertices of G by FINSEQ_1:def 4;
take p1, p2; thus
p1<>p2 by A1,A3,A8,A10,Th38;
thus p1 is_vertex_seq_of c by A3;
now thus len p2 = len c + 1 by A3,A10,Def7;
let n be Nat such that
A13: 1<=n & n<=len c;
set x = p1/.n; set y = p1/.(n+1);
A14: c.n joins x, y by A3,A13,Def7;
A15: 1<=n & n<=len p1 & 1<=n+1 & n+1<=len p1
by A4,A13,AXIOMS:24,NAT_1:37;
then n in dom p1 & n+1 in dom p1 by FINSEQ_3:27;
then p1.n in {X, Y} & p1.(n+1) in {X, Y} &
p2.n in {X, Y} & p2.(n+1) in {X, Y} by A1,A3,A6,A8,A10,A11,A12,Th38,
FUNCT_1:def 5;
then (p1.n=X or p1.n=Y) & (p2.n=X or p2.n=Y) &
(p1.(n+1)=X or p1.(n+1)=Y) & (p2.(n+1)=X or p2.(n+1)=Y) by TARSKI:def 2;
then A16: y = p2.n & x = p2.(n+1) by A6,A7,A9,A10,A12,A15,Def4,Th21,FINSEQ_4:
24;
p2/.n = p2.n & p2/.(n+1) = p2.(n+1) by A10,A15,FINSEQ_4:24;
hence c.n joins p2/.n,p2/.(n+1) by A14,A16,Th31;
end;
hence p2 is_vertex_seq_of c by Def7;
let p be FinSequence of the Vertices of G; assume
A17: p is_vertex_seq_of c;
then reconsider p' = p as TwoValued Alternating FinSequence by A1,Th40;
A18: len p = len c + 1 by A17,Def7;
rng p = {X, Y} by A1,A17,Th39;
then p'=p1 or p'=p2 by A4,A6,A7,A9,A10,A12,A18,Th22;
hence thesis;
end;
Lm6:
(for x, y st x in D & y in D holds x=y) implies Card D = 1 proof assume
A1: for x, y st x in D & y in D holds x=y;
consider x being Element of D; for y holds y in D iff y=x by A1;
then D = {x} by TARSKI:def 1; hence Card D = 1 by CARD_2:60;
end;
theorem Th42:
vs is_vertex_seq_of c implies
(Card the Vertices 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 Vertices of G = 1 or c <>{} & not c alternates_vertices_in G;
per cases by A2;
suppose
A3: Card the Vertices of G = 1;
then reconsider tVG = the Vertices of G as finite set by CARD_4:1;
consider X being set such that
A4: tVG = {X} by A3,CARD_2:60;
let vs1; assume
A5: vs1 is_vertex_seq_of c; assume
A6: vs1 <> vs;
A7: len vs1 = len c +1 & len vs = len c +1 by A1,A5,Def7;
A8: Seg len vs1 = dom vs1 & Seg len vs = dom vs by FINSEQ_1:def 3;
then consider j such that
A9: j in dom vs & vs1.j <> vs.j by A6,A7,FINSEQ_2:10;
A10: vs1.j in rng vs1 & vs.j in rng vs by A7,A8,A9,FUNCT_1:def 5;
rng vs1 c= {X} & rng vs c= {X} by A4,FINSEQ_1:def 4;
then vs.j = X & vs1.j = X by A10,TARSKI:def 1;
hence contradiction by A9;
suppose
A11: c <>{} & not c alternates_vertices_in G;
thus for vs1 st vs1 is_vertex_seq_of c holds vs1 = vs proof let vs1; assume
A12: vs1 is_vertex_seq_of c; assume
A13: vs1 <> vs;
set SG = the Source of G; set TG = the Target of G;
A14: len vs1 = len c +1 & len vs = len c +1 by A1,A12,Def7;
then A15: dom vs1 = dom vs by FINSEQ_3:31;
defpred P[Nat] means $1 in dom vs1 & vs1.$1<>vs.$1;
Seg len vs1 = dom vs1 & Seg len vs = dom vs by FINSEQ_1:def 3;
then A16: ex i st P[i] by A13,A14,FINSEQ_2:10;
consider k such that
A17: P[k] and
A18: for n st P[n] holds k<=n from Min (A16);
0<=k by NAT_1:18; then A19: 0+1=1 & k=0 or 0+1<=k by NAT_1:38;
per cases by A19,REAL_1:def 5;
suppose k=0; hence contradiction by A17,FINSEQ_3:27;
suppose
A20: k=1; thus contradiction proof A21: 0+1=1 &(len c =0 or 0<len c) by NAT_1:
18;
per cases by A21,NAT_1:38;
suppose len c = 0; hence contradiction by A11,FINSEQ_1:25;
suppose
A22: 1<=len c;
then 1<=k+1 & k+1<=len vs1 by A14,A20,AXIOMS:24;
then A23: vs1/.k=vs1.k & vs1/.(k+1)=vs1.(k+1) &
vs/.k=vs.k & vs/.(k+1)=vs.(k+1) by A14,A15,A17,FINSEQ_4:24,def 4;
A24: c.k joins vs1/.k, vs1/.(k+1) by A12,A20,A22,Def7;
c.k joins vs/.k, vs/.(k+1) by A1,A20,A22,Def7;
then A25: (SG.(c.1)=vs1/.1 & TG.(c.1)=vs1/.(k+1) or
SG.(c.1)=vs1/.(k+1) & TG.(c.1)=vs1/.1) &
(SG.(c.1)=vs/.1 & TG.(c.1)=vs/.(k+1) or
SG.(c.1)=vs/.(k+1) & TG.(c.1)=vs/.1) by A20,A24,GRAPH_1:def 9;
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));
A26: P[0] by FINSEQ_3:27;
A27: now let n be Nat; assume
A28: P[n];
thus P[n+1]
proof
assume (n+1) in dom c;
then
A29: 1<=n+1 & n+1<=len c by FINSEQ_3:27;
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 by NAT_1:19;
suppose
A30: n=0; 1<=len c by A29,AXIOMS:22;
then c.1 joins vs1/.1,vs1/.(1+1) & c.1 joins vs/.1,vs/.(1+1)
by A1,A12,Def7;
then A31: (SG.(c.1)=vs1/.1 & TG.(c.1)=vs1/.(1+1) or
SG.(c.1)=vs1/.(1+1) & TG.(c.1)=vs1/.1) &
(SG.(c.1)=vs/.1 & TG.(c.1)=vs/.(1+1) or
SG.(c.1)=vs/.(1+1) & TG.(c.1)=vs/.1) by GRAPH_1:def 9;
thus vs1/.(n+1)<>vs/.(n+1) by A17,A20,A23,A30;
thus vs1/.(n+1+1)<>vs/.(n+1+1) by A17,A20,A23,A30,A31;
thus thesis by A30;
suppose 0<n; then 0+1<=n & n<=n+1 by NAT_1:38;
then A32: 1<=n & n<=len c by A29,AXIOMS:22;
then A33: c.n joins vs1/.n, vs1/.(n+1) by A12,Def7;
c.n joins vs/.n, vs/.(n+1) by A1,A32,Def7;
then A34: (SG.(c.n)=vs1/.n & TG.(c.n)=vs1/.(n+1) or
SG.(c.n)=vs1/.(n+1) & TG.(c.n)=vs1/.n) &
(SG.(c.n)=vs/.n & TG.(c.n)=vs/.(n+1) or
SG.(c.n)=vs/.(n+1) & TG.(c.n)=vs/.n) by A33,GRAPH_1:def 9;
A35: c.(n+1) joins vs1/.(n+1), vs1/.(n+1+1) by A12,A29,Def7;
c.(n+1) joins vs/.(n+1), vs/.(n+1+1) by A1,A29,Def7;
then A36: (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)) &
(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)) by A35,GRAPH_1:def 9;
thus vs1/.(n+1)<> vs/.(n+1) by A28,A32,FINSEQ_3:27;
thus vs1/.(n+1+1)<>vs/.(n+1+1) by A28,A32,A36,FINSEQ_3:27;
thus thesis by A28,A32,A34,A36,FINSEQ_3:27;
end;
end;
end;
A37: for n holds P[n] from Ind(A26,A27);
A38: 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 A37;
hence n in dom c implies SG.(c.n) <> TG.(c.n) by A17,A20,A23,A25;
end;
now let x be set;
A39: G-VSet rng c = { v: ex e being Element of the Edges of G st e in rng c &
(v = (the Source of G).e or v = (the Target of G).e)} by Def6;
hereby assume x in G-VSet rng c; then consider v such that
A40: x=v & ex e being Element of the Edges of G st e in rng c &
(v = (the Source of G).e or v = (the Target of G).e) by A39;
consider e such that
A41: e in rng c & (v = SG.e or v = TG.e) by A40;
consider d being set such that
A42: d in dom c & e=c.d by A41,FUNCT_1:def 5;
reconsider d as Nat by A42;
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 A37,A42;
hence x in {SG.(c.1), TG.(c.1)} by A40,A41,A42,TARSKI:def 2;
end; assume A43: x in {SG.(c.1), TG.(c.1)};
len c <> 0 by A11,FINSEQ_1:25; then 0< len c by NAT_1:19;
then 0+1<=len c by NAT_1:38;
then A44: 1 in dom c & 1 in dom c by FINSEQ_3:27;
then A45: c.1 in rng c & rng c c= the Edges of G
by FINSEQ_1:def 4,FUNCT_1:def 5;
then reconsider e=c.1 as Element of the Edges of G;
reconsider s = SG.e as Element of the Vertices of G by A45,FUNCT_2:7;
reconsider t = TG.e as Element of the Vertices of G by A45,FUNCT_2:7;
A46: e in rng c by A44,FUNCT_1:def 5;
x=s or x =t by A43,TARSKI:def 2; hence x in G-VSet rng c by A39,A46;
end;
then G-VSet rng c = {SG.(c.1), TG.(c.1)} by TARSKI:2;
then Card (G-VSet rng c) = 2 by A17,A20,A23,A25,CARD_2:76;
hence contradiction by A11,A22,A38,Def8;
end;
suppose 1<k; then 1+1<=k by NAT_1:38; then consider k1 being Nat such that
A47: 1<=k1 & k1<k & k=k1+1 by Th1;
A48: k<=len vs1 by A17,FINSEQ_3:27;
then A49: k1<=len c by A14,A47,REAL_1:53;
A50: k1<=len vs1 by A47,A48,AXIOMS:22;
then A51: k1 in dom vs1 by A47,FINSEQ_3:27;
A52: vs1/.k1=vs1.k1 & vs1/.k=vs1.k &
vs/.k1=vs.k1 & vs/.k=vs.k
by A14,A15,A17,A47,A50,FINSEQ_4:24,def 4;
A53: c.k1 joins vs1/.k1, vs1/.(k1+1) by A12,A47,A49,Def7;
c.k1 joins vs/.k1, vs/.(k1+1) by A1,A47,A49,Def7;
then (SG.(c.k1)=vs1/.k1 & TG.(c.k1)=vs1/.k or
SG.(c.k1)=vs1/.k & TG.(c.k1)=vs1/.k1) &
(SG.(c.k1)=vs/.k1 & TG.(c.k1)=vs/.k or
SG.(c.k1)=vs/.k & TG.(c.k1)=vs/.k1) by A47,A53,GRAPH_1:def 9;
hence contradiction by A17,A18,A47,A51,A52;
end;
end; assume
A54: for vs1 st vs1 is_vertex_seq_of c holds vs1 = vs; assume
A55: Card the Vertices of G <> 1; assume
A56: c ={} or c alternates_vertices_in G;
consider x, y such that
A57: x in the Vertices of G & y in the Vertices of G & x<>y by A55,Lm6;
reconsider x as Element of the Vertices of G by A57;
reconsider y as Element of the Vertices of G by A57;
thus contradiction proof per cases by A56;
suppose c ={};
then <*x*> is_vertex_seq_of c & <*y*> is_vertex_seq_of c by Th35;
then <*x*> = vs & <*y*> = vs by A54;
then vs.1 = x & vs.1 = y by FINSEQ_1:57;
hence contradiction by A57;
suppose c alternates_vertices_in G; then consider vs1,vs2 such that
A58: 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 by Th41;
vs1 = vs & vs2 = vs by A54,A58;
hence contradiction by A58;
end;
end;
definition let G, c; assume
A1: Card the Vertices of G = 1 or c <>{} & not c alternates_vertices_in G;
func vertex-seq c -> FinSequence of the Vertices of G means
it is_vertex_seq_of c;
existence by Th36;
uniqueness by A1,Th42;
end;
theorem Th43: 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 &
for n st 1<=n & n<=len c holds c.n joins vs/.n,vs/.(n+1)
by Def7;
assume that
A3: c1 = c|Seg n and
A4: vs1= vs|Seg (n+1);
now
per cases;
suppose
A5: n<=len c; then n+1<=len vs by A2,AXIOMS:24;
then A6: len c1 = n & len vs1 = n+1 by A3,A4,A5,FINSEQ_1:21;
hence len vs1 = len c1 + 1;
let k be Nat;
assume that
A7: 1<=k and
A8: k<=len c1;
A9: k<=len c by A5,A6,A8,AXIOMS:22;
then k in dom c & k in Seg n by A6,A7,A8,FINSEQ_1:3,FINSEQ_3:27;
then A10: c1.k = c.k by A3,FUNCT_1:72; A11: k<=len vs by A2,A9,NAT_1:37;
A12: k<=n+1 by A6,A8,NAT_1:37;
then A13: k in dom vs & k in Seg (n+1) by A7,A11,FINSEQ_1:3,FINSEQ_3:27;
A14: k+1<=len vs by A2,A9,REAL_1:55;
A15: 1<=k+1 & k+1<=len c1 +1 by A8,NAT_1:37,REAL_1:55;
then k+1 in dom vs & k+1 in Seg (n+1) by A6,A14,FINSEQ_1:3,FINSEQ_3:27;
then A16: vs1.k=vs.k & vs1.(k+1)=vs.(k+1) by A4,A13,FUNCT_1:72;
A17: vs/.k=vs.k & vs/.(k+1)=vs.(k+1) by A7,A11,A14,A15,FINSEQ_4:24;
vs1/.k=vs1.k & vs1/.(k+1)=vs1.(k+1) by A6,A7,A12,A15,FINSEQ_4:24;
hence c1.k joins vs1/.k,vs1/.(k+1) by A1,A7,A9,A10,A16,A17,Def7;
suppose
A18: len c <=n; then len vs<=n+1 by A2,AXIOMS:24;
then c1 = c & vs1 = vs by A3,A4,A18,FINSEQ_2:23;
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,Def7;
end; hence vs1 is_vertex_seq_of c1 by Def7;
end;
theorem Th44:
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; assume
A4: q = (m,n)-cut c; consider vs such that
A5: vs is_vertex_seq_of c by Th36; set p' = (m,n+1)-cut vs;
A6: len vs = len c + 1 by A5,Def7;
then A7: m<=n+1 & n+1<=len vs by A2,A3,AXIOMS:24,NAT_1:37;
then A8: m<=n+1+1 by NAT_1:37;
len q +m-m=n+1-m by A1,A3,A4,A7,Def1;
then A9: len q = n+1-m by XCMPLX_1:26
.= n+1+ -m by XCMPLX_0:def 8 .= n+ -m+1 by XCMPLX_1:1
.= n-m+1 by XCMPLX_0:def 8;
len p'+m-m=(n+1)+1-m by A1,A7,A8,Def1;
then A10: len p' = (n+1)+1-m by XCMPLX_1:26 .= (n+1)+1+ -m by XCMPLX_0:def 8
.= n+(1+1)+-m by XCMPLX_1:1 .= n+-m+(1+1) by XCMPLX_1:1
.= n-m+(1+1) by XCMPLX_0:def 8 .= n-m+1+1 by XCMPLX_1:1;
A11: now let k be Nat;
assume that
A12: 1<=k and
A13: k<=len p';
k in dom p' by A12,A13,FINSEQ_3:27;
then A14: p'.k in rng p' by FUNCT_1:def 5;
rng p' c= rng vs by Th11;
then A15: p'.k in rng vs by A14;
rng vs c= the Vertices of G by FINSEQ_1:def 4;
hence p'.k in the Vertices of G by A15;
end;
A16: now let k be Nat; 1-1<=m-1 by A1,REAL_1:49;
then m-1 = m-'1 by BINARITH:def 3;
then reconsider m1= m-1 as Nat; reconsider i = m1+k as Nat;
assume that
A17: 1<=k and
A18: k<=len q; 0+1<=k by A17; then consider j such that
A19: 0<=j & j<len q & k=j+1 by A18,Th1;
A20: i= m-1+1+j by A19,XCMPLX_1:1 .= m+j by XCMPLX_1:27;
set v1 = vs/.i; set v2 = vs/.(i+1);
1-1<=m-1 by A1,REAL_1:49;
then A21: 0+1<=m-1+k by A17,REAL_1:55; k<=n-(m-1) by A9,A18,XCMPLX_1:37;
then i<=(m-1)+(n-(m-1)) by AXIOMS:24;
then i<=n by XCMPLX_1:27;
then A22: 1<=i & i<=len c by A3,A21,AXIOMS:22;
then A23: c.i joins v1, v2 by A5,Def7;
A24: i<=len vs & 1<=i+1 & i+1<=len vs by A6,A22,NAT_1:37,REAL_1:55;
A25: i+1 = m+(j+1) by A20,XCMPLX_1:1;
j<len p' & j+1<len p' by A9,A10,A19,NAT_1:38,REAL_1:53;
then A26: p'.k = vs.i & p'.(k+1) = vs.(i+1) by A1,A7,A8,A19,A20,A25,Def1;
take v1, v2;
thus v1 = p'.k & v2 = p'.(k+1) & q.k joins v1, v2 by A1,A3,A4,A7,A19,A20,
A21,A23,A24,A26,Def1,FINSEQ_4:24;
end;
thus q is Chain of G proof
hereby let k be Nat;
assume that
A27: 1<=k and
A28: k<=len q;
k in dom q by A27,A28,FINSEQ_3:27;
then A29: q.k in rng q by FUNCT_1:def 5; rng q c= rng c by A4,Th11;
then A30: q.k in rng c by A29; rng c c= the Edges of G by FINSEQ_1:def 4;
hence q.k in the Edges of G by A30;
end;
take p'; thus len p' = len q + 1 by A9,A10;
thus (for n st 1<=n & n<=len p' holds p'.n in the Vertices of G) by A11;
thus thesis by A16;
end;
end;
theorem Th45:
1<=m & m<=n & n<=len c & c1 = (m,n)-cut c &
vs is_vertex_seq_of c & vs1 = (m,n+1)-cut vs
implies vs1 is_vertex_seq_of c1 proof
assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len c; assume
A4: c1 = (m,n)-cut c;
assume that
A5: vs is_vertex_seq_of c and
A6: vs1 = (m,n+1)-cut vs;
A7: len vs = len c + 1 by A5,Def7;
then A8: m<=n+1 & n+1<=len vs by A2,A3,AXIOMS:24,NAT_1:37;
then A9: m<=n+1+1 by NAT_1:37;
A10: len c1 +m= n+1 by A1,A3,A4,A8,Def1;
len vs1 +m = n+1+1 by A1,A6,A8,A9,Def1;
hence A11: len vs1 = n+1+1-m by XCMPLX_1:26 .= n+1+1+-m by XCMPLX_0:def 8
.= n+1+-m+1 by XCMPLX_1:1
.= n+1-m+1 by XCMPLX_0:def 8 .= len c1 + 1 by A10,XCMPLX_1:26;
let k be Nat;
assume that
A12: 1<=k and
A13: k<=len c1; 0+1<=k by A12; then consider j such that
A14: 0<=j & j<len c1 & k=j+1 by A13,Th1;
set i = m+j; set v1 = vs/.i; set v2 = vs/.(i+1);
m+k<=len c1 +m by A13,REAL_1:55;
then m+j+1<=len c1+m by A14,XCMPLX_1:1;
then m+j+1-1<=len c1 +m-1 by REAL_1:49;
then i<=len c1 +m-1 by XCMPLX_1:26; then i<=n by A10,XCMPLX_1:26;
then A15: 1<=i & i<=len c by A1,A3,AXIOMS:22,NAT_1:37;
then A16: c.i joins v1, v2 by A5,Def7;
j<len vs1 by A11,A14,NAT_1:38;
then A17: vs1.k = vs.i by A1,A6,A8,A9,A14,Def1;
A18: j+1<len vs1 by A11,A14,REAL_1:53;
m+j+1 = m+(j+1) by XCMPLX_1:1;
then A19: vs1.(k+1) = vs.(i+1) by A1,A6,A8,A9,A14,A18,Def1;
i<=len vs & 1<=i+1 & i+1<=len vs by A7,A15,NAT_1:37,REAL_1:55;
then A20: vs/.i=vs.i & vs/.(i+1)=vs.(i+1) by A15,FINSEQ_4:24;
0+1=1;
then A21: 1<=k & k<=len c1 by A14,NAT_1:38,REAL_1:55;
then k<=len vs1 & 1<=k+1 & k+1<=len vs1 by A11,NAT_1:37,REAL_1:55;
then vs1/.k=vs1.k & vs1/.(k+1)=vs1.(k+1) by A21,FINSEQ_4:24;
hence c1.k joins vs1/.k, vs1/.(k+1) by A1,A3,A4,A8,A14,A16,A17,A19,A20,Def1
;
end;
theorem Th46:
vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1.len vs1 = vs2.1
implies c1^c2 is Chain of G proof
assume that
A1: vs1 is_vertex_seq_of c1 and
A2: vs2 is_vertex_seq_of c2 & vs1.len vs1 = vs2.1;
A3: len vs1 = len c1 + 1 & len vs2 = len c2 + 1 by A1,A2,Def7;
then A4: vs1 <> {} & vs2 <> {} by FINSEQ_1:25;
set q=c1^c2; set p=vs1^'vs2; len p +1 = len vs1 +len vs2 by A4,Th13;
then A5: len p = len vs1 + len vs2 - 1 by XCMPLX_1:26;
then A6: len p = (len c1 +1)+((len c2 +1)-1)by A3,XCMPLX_1:29
.= len c1 + 1 + len c2 by XCMPLX_1:26
.= len c1 + len c2 + 1 by XCMPLX_1:1
.= len q + 1 by FINSEQ_1:35;
A7: now let n be Nat such that
A8: 1<=n & n<=len p;
per cases;
suppose
A9: n<=len vs1;
then A10: p.n = vs1.n by A8,Th14; n in dom vs1 by A8,A9,FINSEQ_3:27;
hence p.n in the Vertices of G by A10,FINSEQ_2:13;
suppose
A11: n > len vs1; then consider m being Nat such that
A12: n = len vs1 + m by NAT_1:28;
m <> 0 by A11,A12;
then 0 < m by NAT_1:19; then A13: 0+1<=m by NAT_1:38;
A14: 1<=m+1 by NAT_1:37;
len vs1 + m<=len vs1 + (len vs2 - 1) by A5,A8,A12,XCMPLX_1:29;
then m<=len vs2 - 1 by REAL_1:53;
then m+1<=len vs2 - 1+1 by AXIOMS:24;
then A15: m+1<=len vs2 by XCMPLX_1:27; then m<len vs2 by NAT_1:38;
then A16: p.(len vs1 + m) = vs2.(m+1) by A13,Th15;
m+1 in dom vs2 by A14,A15,FINSEQ_3:27;
hence p.n in the Vertices of G by A12,A16,FINSEQ_2:13;
end;
A17: now let n be Nat; assume
1<=n & n<=len q;
then A18: n in dom q by FINSEQ_3:27;
per cases by A18,FINSEQ_1:38;
suppose
A19: n in dom c1;
then A20: q.n = c1.n by FINSEQ_1:def 7;
set v1=vs1/.n; set v2=vs1/.(n+1);
A21: 1<=n & n<=len c1 by A19,FINSEQ_3:27;
then A22: c1.n joins v1, v2 by A1,Def7;
A23: n<=len vs1 by A3,A21,NAT_1:37;
1<=n+1 & n+1<=len c1+1 by A21,AXIOMS:24,NAT_1:37;
then A24: 1<=n+1 & n+1<=len vs1 by A1,Def7;
then A25: vs1/.n=vs1.n & vs1/.(n+1)=vs1.(n+1) by A21,A23,FINSEQ_4:24;
p.n = vs1.n & p.(n+1) = vs1.(n+1) by A21,A23,A24,Th14;
hence ex v1, v2 being Element of the Vertices of G st
v1 = p.n & v2 = p.(n+1) & q.n joins v1, v2 by A20,A22,A25;
suppose ex k being Nat st k in dom c2 & n=len c1 + k;
then consider k being Nat such that
A26: k in dom c2 & n = len c1 + k;
A27: q.n = c2.k by A26,FINSEQ_1:def 7;
A28: 1<=k & k<=len c2 by A26,FINSEQ_3:27;
then A29: 1<=k+1 & k<=len vs2 & k+1<=len vs2 by A3,NAT_1:37,REAL_1:55;
set v1 = vs2/.k; set v2 = vs2/.(k+1);
A30: vs2/.k=vs2.k & vs2/.(k+1)=vs2.(k+1) by A28,A29,FINSEQ_4:24;
A31: c2.k joins v1, v2 by A2,A28,Def7;
A32: k<=len vs2 by A3,A28,NAT_1:37;
0+1<=k by A26,FINSEQ_3:27; then consider j such that
A33: 0<=j & j<len vs2 & k=j+1 by A32,Th1;
A34: p.n = vs2.k
proof per cases by A28,REAL_1:def 5;
suppose A35: 1=k; 0<len vs1 by A3,NAT_1:19;
then 0+1<=len vs1 by NAT_1:38;
hence p.n = vs2.k by A2,A3,A26,A35,Th14;
suppose 1<k; then A36:1<=j by A33,NAT_1:38;
thus p.n = p.(len vs1 +j) by A3,A26,A33,XCMPLX_1:1
.= vs2.k by A33,A36,Th15;
end;
A37: k<len vs2 by A3,A28,NAT_1:38;
p.(n+1) = p.(len c1 +1+k) by A26,XCMPLX_1:1
.= vs2.(k+1) by A3,A28,A37,Th15;
hence ex v1, v2 being Element of the Vertices of G st
v1 = p.n & v2 = p.(n+1) & q.n joins v1, v2 by A27,A30,A31,A34;
end;
thus c1^c2 is Chain of G proof
hereby let n be Nat; assume
1<=n & n<=len q;
then A38: n in dom q by FINSEQ_3:27;
per cases by A38,FINSEQ_1:38;
suppose
A39: n in dom c1;
then A40: 1<=n & n<=len c1 by FINSEQ_3:27;
q.n = c1.n by A39,FINSEQ_1:def 7;
hence (c1^c2).n in the Edges of G by A40,GRAPH_1:def 11;
suppose ex k being Nat st k in dom c2 & n=len c1 + k;
then consider k being Nat such that
A41: k in dom c2 & n = len c1 + k;
A42: q.n = c2.k by A41,FINSEQ_1:def 7;
1<=k & k<=
len c2 by A41,FINSEQ_3:27; hence (c1^c2).n in the Edges of G by A42,GRAPH_1:def
11;
end; thus thesis by A6,A7,A17;
end;
end;
theorem Th47:
vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1.len vs1 = vs2.1 &
c = c1^c2 & vs = vs1^'vs2
implies vs is_vertex_seq_of c proof
assume that
A1: vs1 is_vertex_seq_of c1 and
A2: vs2 is_vertex_seq_of c2 & vs1.len vs1 = vs2.1;
assume that
A3: c = c1^c2 and
A4: vs = vs1^'vs2;
A5: len vs1 = len c1 + 1 & len vs2 = len c2 + 1 by A1,A2,Def7;
then A6: vs1 <> {} & vs2 <> {} by FINSEQ_1:25;
set q=c1^c2; set p=vs1^'vs2;
len p +1 = len vs1 +len vs2 by A6,Th13;
then len p = len vs1 + len vs2 - 1 by XCMPLX_1:26;
then A7: len p = (len c1 +1)+((len c2 +1)-1)by A5,XCMPLX_1:29
.= len c1 + 1 + len c2 by XCMPLX_1:26
.= len c1 + len c2 + 1 by XCMPLX_1:1
.= len q + 1 by FINSEQ_1:35;
reconsider p as FinSequence of the Vertices of G;
now let n be Nat;
assume that
A8: 1<=n and
A9: n<=len q;
n<=len p & 1<=n+1 & n+1<=len p by A7,A9,NAT_1:37,REAL_1:55;
then A10: p/.n=p.n & p/.(n+1)=p.(n+1) by A8,FINSEQ_4:24;
A11: n in dom q by A8,A9,FINSEQ_3:27;
per cases by A11,FINSEQ_1:38;
suppose
A12: n in dom c1;
set v1=vs1/.n; set v2=vs1/.(n+1);
A13: 1<=n & n<=len c1 by A12,FINSEQ_3:27;
then A14: c1.n joins v1, v2 by A1,Def7;
A15: n<=len vs1 by A5,A13,NAT_1:37;
1<=n+1 & n+1<=len c1+1 by A13,AXIOMS:24,NAT_1:37;
then A16: 1<=n+1 & n+1<=len vs1 by A1,Def7;
then A17: vs1/.n=vs1.n & vs1/.(n+1)=vs1.(n+1) by A13,A15,FINSEQ_4:24;
p.n = vs1.n & p.(n+1) = vs1.(n+1) by A13,A15,A16,Th14;
hence q.n joins p/.n, p/.(n+1) by A10,A12,A14,A17,FINSEQ_1:def 7;
suppose ex k being Nat st k in dom c2 & n=len c1 + k;
then consider k being Nat such that
A18: k in dom c2 & n = len c1 + k;
A19: 1<=k & k<=len c2 by A18,FINSEQ_3:27;
then A20: 1<=k+1 & k<=len vs2 & k+1<=len vs2 by A5,NAT_1:37,REAL_1:55;
set v1 = vs2/.k; set v2 = vs2/.(k+1);
A21: vs2/.k=vs2.k & vs2/.(k+1)=vs2.(k+1) by A19,A20,FINSEQ_4:24;
A22: c2.k joins v1, v2 by A2,A19,Def7;
A23: k<=len vs2 by A5,A19,NAT_1:37;
0+1<=k by A18,FINSEQ_3:27; then consider j such that
A24: 0<=j & j<len vs2 & k=j+1 by A23,Th1;
A25: p.n = vs2.k proof per cases by A19,REAL_1:def 5;
suppose A26: 1=k; 0<len vs1 by A5,NAT_1:19;
then 0+1<=len vs1 by NAT_1:38;
hence p.n = vs2.k by A2,A5,A18,A26,Th14;
suppose 1<k; then A27:1<=j by A24,NAT_1:38;
thus p.n = p.(len vs1 +j) by A5,A18,A24,XCMPLX_1:1
.= vs2.k by A24,A27,Th15;
end;
A28: k<len vs2 by A5,A19,NAT_1:38;
p.(n+1) = p.(len c1 +1+k) by A18,XCMPLX_1:1
.= vs2.(k+1) by A5,A19,A28,Th15;
hence q.n joins p/.n,p/.(n+1) by A10,A18,A21,A22,A25,FINSEQ_1:def 7;
end;
hence vs is_vertex_seq_of c by A3,A4,A7,Def7;
end;
begin :: Simple chains, paths and oriented chains
Lm7: <*v*> is_vertex_seq_of {} proof
set p = <*v*>, ec = {};
A1: len p = 0 + 1 by FINSEQ_1:56 .= len ec + 1 by FINSEQ_1:25;
now let n;
assume that
A2: 1<=n and
A3: n<=len ec;
1<=len ec by A2,A3,AXIOMS:22; then 1<=0 by FINSEQ_1:25;
hence ec.n joins p/.n,p/.(n+1);
end;
hence p is_vertex_seq_of ec by A1,Def7;
end;
definition let G;
let IT be Chain of G;
attr IT is simple means
:Def10: ex vs st vs is_vertex_seq_of IT &
(for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs);
end;
definition let G;
cluster simple Chain of G;
existence proof consider q being empty Chain of G;
take q; consider x being Element of the Vertices of G;
reconsider p =<*x*> as FinSequence of the Vertices of G;
take p;
thus p is_vertex_seq_of q by Lm7;
let n,m; assume 1<=n & n<m & m<=len p & p.n = p.m;
then 1<m & m<=1 by AXIOMS:22,FINSEQ_1:56;
hence n =1 & m = len p;
end;
end;
reserve sc for simple Chain of G;
canceled;
theorem sc|(Seg n) is simple Chain of G proof consider vs such that
A1: vs is_vertex_seq_of sc &
(for n, m st 1<=n & n < m & m<=len vs & vs.n = vs.m holds
n=1 & m=len vs) by Def10;
reconsider q' = sc|Seg n as Chain of G by GRAPH_1:4;
reconsider p' = vs|Seg(n+1) as FinSequence of the Vertices of G by FINSEQ_1:23;
now
take p'; thus p' is_vertex_seq_of q' by A1,Th43;
let k, m;
assume that
A2: 1<=k and
A3: k < m and
A4: m<=len p' and
A5: p'.k = p'.m;
k<=len p' & 1<=m by A2,A3,A4,AXIOMS:22;
then A6: p'.k = vs.k & p'.m = vs.m by A2,A4,Th2;
A7: len p'<=len vs by Th2;
then A8: m<=len vs by A4,AXIOMS:22;
hence k=1 by A1,A2,A3,A5,A6;
len p' = len vs or len p' < len vs by A7,REAL_1:def 5;
hence m = len p' by A1,A2,A3,A4,A5,A6,A8;
end; hence thesis by Def10;
end;
theorem Th50:
2<len sc & vs1 is_vertex_seq_of sc & vs2 is_vertex_seq_of sc
implies vs1=vs2 proof
assume that
A1: 2<len sc and
A2: vs1 is_vertex_seq_of sc and
A3: vs2 is_vertex_seq_of sc; assume
A4: vs1 <> vs2;
set SG = the Source of G; set TG = the Target of G;
A5: len vs1 = len sc +1 & len vs2 = len sc +1 by A2,A3,Def7;
defpred P[Nat] means $1 in dom vs1 & vs1.$1<>vs2.$1;
A6: Seg len vs1 = dom vs1 & Seg len vs2 = dom vs2 by FINSEQ_1:def 3;
then A7: ex j st P[j] by A4,A5,FINSEQ_2:10;
consider k such that
A8: P[k] and
A9: for n st P[n] holds k<=n from Min (A7);
A10: 1<=k & k<=len sc +1 by A5,A8,FINSEQ_3:27;
per cases by A10,REAL_1:def 5;
suppose
A11: k=1;
A12: 1+1+1<=len vs1 by A1,A5,AXIOMS:24;
then A13: 1<=len vs1 & 1+1<=len vs1 by AXIOMS:22;
set v11=vs1/.1; set v12=vs1/.(1+1); set v13=vs1/.(1+1+1);
set v21=vs2/.1; set v22=vs2/.(1+1); set v23=vs2/.(1+1+1);
A14: v11=vs1.1 & v12=vs1.(1+1) & v13=vs1.(1+1+1) &
v21=vs2.1 & v22=vs2.(1+1) & v23=vs2.(1+1+1) by A5,A12,A13,FINSEQ_4:24;
1+1<=len sc & 1<=len sc by A1,AXIOMS:22;
then A15: sc.1 joins v11,v12 & sc.1 joins v21,v22 &
sc.2 joins v12,v13 & sc.2 joins v22,v23 by A2,A3,Def7;
then v11=v21 & v12=v22 or v11=v22 & v12=v21 by Th32;
then A16: v11=v13 & v21=v23 by A8,A11,A14,A15,Th32;
consider vs such that
A17: vs is_vertex_seq_of sc &
for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs
by Def10;
sc <>{} proof assume not thesis; then len sc =0 by FINSEQ_1:25;
hence contradiction by A1; end;
then A18: vs = vs1 or vs = vs2 by A2,A3,A4,A17,Th37;
then A19: 1+1+1 = len vs by A5,A12,A14,A16,A17;
1+1+1<=
len sc by A1,NAT_1:38; hence contradiction by A5,A18,A19,NAT_1:38;
suppose 1<k; then 1+1<=k by NAT_1:38; then consider k1 being Nat such that
A20: 1<=k1 & k1<k & k=k1+1 by Th1;
A21: k<=len vs1 by A8,FINSEQ_3:27;
then A22: k1<=len sc by A5,A20,REAL_1:53;
A23: k1<=len vs1 by A20,A21,AXIOMS:22;
then A24: k1 in dom vs1 by A20,FINSEQ_3:27;
A25: vs1/.k1=vs1.k1 & vs1/.k=vs1.k &
vs2/.k1=vs2.k1 & vs2/.k=vs2.k
by A5,A6,A8,A20,A23,FINSEQ_4:24,def 4;
A26: sc.k1 joins vs1/.k1, vs1/.(k1+1) by A2,A20,A22,Def7;
sc.k1 joins vs2/.k1, vs2/.(k1+1) by A3,A20,A22,Def7;
then (SG.(sc.k1)=vs1/.k1 & TG.(sc.k1)=vs1/.k or
SG.(sc.k1)=vs1/.k & TG.(sc.k1)=vs1/.k1) &
(SG.(sc.k1)=vs2/.k1 & TG.(sc.k1)=vs2/.k or
SG.(sc.k1)=vs2/.k & TG.(sc.k1)=vs2/.k1)
by A20,A26,GRAPH_1:def 9;
hence contradiction by A8,A9,A20,A24,A25;
end;
theorem vs is_vertex_seq_of sc implies
for n, m st 1<=n & n<m & m<=len vs & vs.n = vs.m holds n=1 & m=len vs
proof assume
A1: vs is_vertex_seq_of sc;
consider vs1 such that
A2: vs1 is_vertex_seq_of sc &
(for n,m st 1<=n & n<m & m<=len vs1 & vs1.n=vs1.m holds n=1 & m=len vs1)
by Def10;
per cases;
suppose A3: len sc <= 2;
thus thesis proof
per cases by A3,CQC_THE1:3;
suppose len sc = 0;
then A4: len vs = 0+1 by A1,Def7;
let n,m;
thus thesis by A4,AXIOMS:22;
suppose
len sc = 1;
then A5: len vs = 1+1 & len vs1 = 1+1 by A1,A2,Def7;
let n,m; assume that
A6: 1<=n and
A7: n<m and
A8: m<=len vs and
vs.n=vs.m;
A9: n+1<=m by A7,NAT_1:38;
then n+1<=1+1 by A5,A8,AXIOMS:22; then n<=1 by REAL_1:53;
then n=1 by A6,AXIOMS:21;
hence thesis by A5,A8,A9,AXIOMS:21;
suppose
A10: len sc = 2;
then A11: len vs = 1+1+1 & len vs1 = 1+1+1 by A1,A2,Def7;
set v1=vs/.1; set v2=vs/.(1+1); set v3=vs/.(1+1+1);
set v11=vs1/.1; set v12=vs1/.(1+1); set v13=vs1/.(1+1+1);
A12: v1=vs.1 & v2=vs.(1+1) & v3=vs.(1+1+1) &
v11=vs1.1 & v12=vs1.(1+1) & v13=vs1.(1+1+1) by A11,FINSEQ_4:24;
A13: sc.1 joins v1, v2 & sc.1 joins v11,v12 &
sc.2 joins v2, v3 & sc.2 joins v12,v13 by A1,A2,A10,Def7;
then A14: v1=v11 & v2=v12 or v1=v12 & v2=v11 by Th32;
A15: v2=v12 & v3=v13 or v2=v13 & v3=v12 by A13,Th32;
let n,m;
assume that
A16: 1<=n and
A17: n<m and
A18: m<=len vs and
A19: vs.n=vs.m; n+1<=m by A17,NAT_1:38;
then n+1<=1+1+1 by A11,A18,AXIOMS:22;
then A20: n<=1+1 by REAL_1:53;
thus thesis proof
per cases by A16,A20,NAT_1:27;
suppose
A21: n=1; 1<m by A16,A17,AXIOMS:22;
then A22: 1+1<=m by NAT_1:38;
thus thesis proof
per cases by A11,A18,A22,NAT_1:27;
suppose m=1+1; hence thesis by A2,A11,A12,A14,A19,A21;
suppose m=1+1+1; hence thesis by A1,A10,A21,Def7;
end;
suppose
A23: n=1+1; then 1+1+1<=m by A17,NAT_1:38;
then m=1+1+1 by A11,A18,AXIOMS:21;
hence thesis by A2,A11,A12,A15,A19,A23;
end;
end;
suppose 2<len sc; then vs=vs1 by A1,A2,Th50;
hence thesis by A2;
end;
:: A chain may have more than one simple chain spanning its endpoints.
:: The following chain:
:: .--->.
:: ^ |
:: | v
:: .--->.<---.--->.
:: | ^
:: v |
:: .--->.
:: is a case in point:
theorem Th52:
not c is simple Chain of G & vs is_vertex_seq_of c implies
ex fc being FinSubsequence of c, fvs being FinSubsequence 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 & n<m & m<=len vs & vs.n=vs.m & (n<>1 or m<>len vs) by A1,A2,Def10;
A4: len vs = len c + 1 by A2,Def7; m-n>n-n by A3,REAL_1:54;
then A5: m-n>0 by XCMPLX_1:14;
reconsider n1 = n-'1 as Nat; 1-1<=n-1 by A3,REAL_1:49;
then A6: n-1 = n-'1 by BINARITH:def 3;
then A7: n1+1 = n by XCMPLX_1:27;
per cases by A3;
suppose
A8: n<>1 & m <> len vs;
then 1 < n by A3,REAL_1:def 5;
then 1 + 1<=n by NAT_1:38; then A9: 1+1-1<=n-1 by REAL_1:49;
n < len vs by A3,AXIOMS:22; then n-1 < len c +1-1 by A4,REAL_1:54;
then A10: 1<=1 & 1<=n1 & n1<=len c by A6,A9,XCMPLX_1:26;
A11: 1<=n1+1 by NAT_1:37; A12: m < len vs by A3,A8,REAL_1:def 5;
then A13: m<=len c by A4,NAT_1:38;
A14: 1<=m & m<=len c & len c <=len c by A3,A4,A12,AXIOMS:22,NAT_1:38;
reconsider c1 = (1,n1)-cut c as Chain of G by A10,Th44;
reconsider c2 = (m,len c)-cut c as Chain of G by A14,Th44;
set p2' = (m+1, len c +1)-cut vs;
reconsider pp = (1,n)-cut vs as FinSequence of the Vertices of G;
reconsider p2 = (m,len c+1)-cut vs as FinSequence of the Vertices of G;
A15: 1<=n & n<=len vs by A3,AXIOMS:22;
A16: 1<=n+1 by NAT_1:37;
A17: 1<=m & m<=len c + 1 & len c + 1<=len vs by A2,A3,Def7,AXIOMS:22;
A18: pp is_vertex_seq_of c1 by A2,A7,A10,Th45;
A19: p2 is_vertex_seq_of c2 by A2,A14,Th45;
A20: len pp = len c1 + 1 by A18,Def7;
A21: len p2 = len c2 + 1 by A19,Def7;
1-1<=m-1 by A14,REAL_1:49;
then m-'1 = m-1 by BINARITH:def 3;
then reconsider m1 = m-1 as Nat;
A22: m = m1 +1 by XCMPLX_1:27; len c2 +m = len c +1 by A3,A4,A14,Def1;
then A23: len c2 = len c +1-m by XCMPLX_1:26 .=len c - m + 1 by XCMPLX_1:29;
m-m<=len c -m by A13,REAL_1:49; then 0<=len c -m by XCMPLX_1:14
;
then A24: 0+1<=len c -m +1 by AXIOMS:24;
then 1-1<=len c2 -1 by A23,REAL_1:49;
then len c2 -'1 = len c2 -1 by BINARITH:def 3;
then reconsider lc21 = len c2 -1 as Nat;
A25: m+lc21 = m1+(len c2 -1+1) by A22,XCMPLX_1:1 .= m1+len c2 by XCMPLX_1:27;
A26: 0+1=1 & 0<len p2 by A21,NAT_1:19;
then A27: 0+1=1 & 0<=1 & 1<=len p2 by NAT_1:38;
A28: p2 = (0+1, len p2)-cut p2 by Th7
.= (0+1, 1)-cut p2 ^ (1+1, len p2)-cut p2 by A27,Th8;
m1<=m by A22,NAT_1:37;
then A29: p2 = (m1+1, m)-cut vs ^ (m+1, len c +1)-cut vs by A3,A4,A22,Th8;
A30: m<=len c +1+1 by A3,A4,NAT_1:37;
(1,1)-cut p2 = <*p2.(0+1)*> by A27,Th6
.= <*vs.(m+0)*> by A4,A14,A26,A30,Def1
.= (m,m)-cut vs by A3,A14,Th6;
then A31: p2' = (2, len p2)-cut p2 by A22,A28,A29,FINSEQ_1:46;
set domfc = {k: 1<=k & k<=n1 or m<=k & k<= len c};
deffunc F(set) = c.$1;
consider fc being Function such that
A32: dom fc = domfc and
A33: for x st x in domfc holds fc.x = F(x) from Lambda;
domfc c= Seg len c proof let x be set; assume x in domfc;
then consider kk being Nat such that
A34: x = kk & (1<=kk & kk<=n1 or m<=kk & kk<= len c);
1<=kk & kk<=len c by A10,A14,A34,AXIOMS:22;
hence x in Seg len c by A34,FINSEQ_1:3;
end;
then reconsider fc as FinSubsequence by A32,FINSEQ_1:def 12;
A35: fc c= c proof let p be set; assume
A36: p in fc; then consider x, y such that
A37: [x,y] = p by RELAT_1:def 1;
A38: x in dom fc & y = fc.x by A36,A37,FUNCT_1:8;
then consider kk being Nat such that
A39: x = kk & (1<=kk & kk<=n1 or m<=kk & kk<= len c) by A32;
1<=kk & kk<=len c by A10,A14,A39,AXIOMS:22;
then A40: x in dom c by A39,FINSEQ_3:27; y = c.kk by A32,A33,A38,A39;
hence p in c by A37,A39,A40,FUNCT_1:8;
end;
then reconsider fc as FinSubsequence of c by Def5;
take fc;
set domfvs = {k: 1<=k & k<=n or m+1<=k & k<= len vs};
deffunc F(set) = vs.$1;
consider fvs being Function such that
A41: dom fvs = domfvs and
A42: for x st x in domfvs holds fvs.x = F(x) from Lambda;
domfvs c= Seg len vs proof let x be set; assume x in domfvs;
then consider kk being Nat such that
A43: x = kk & (1<=kk & kk<=n or m+1<=kk & kk<= len vs);
1<=m+1 by NAT_1:37; then 1<=kk & kk<=len vs by A15,A43,AXIOMS:22;
hence x in Seg len vs by A43,FINSEQ_1:3;
end;
then reconsider fvs as FinSubsequence by A41,FINSEQ_1:def 12;
A44: fvs c= vs proof let p be set; assume
A45: p in fvs; then consider x, y such that
A46: [x,y] = p by RELAT_1:def 1;
A47: x in dom fvs & y = fvs.x by A45,A46,FUNCT_1:8;
then consider kk being Nat such that
A48: x = kk & (1<=kk & kk<=n or m+1<=kk & kk<= len vs) by A41;
1<=m+1 by NAT_1:37;
then 1<=kk & kk<=len vs by A15,A48,AXIOMS:22;
then A49: x in dom vs by A48,FINSEQ_3:27; y = vs.kk by A41,A42,A47,A48;
hence p in vs by A46,A48,A49,FUNCT_1:8;
end;
then reconsider fvs as FinSubsequence of vs by Def5;
take fvs;
A50: p2.1 = vs.m & pp.len pp = vs.n by A15,A17,Th12;
then reconsider c' = c1^c2 as Chain of G by A3,A18,A19,Th46;
take c';
take p1=pp^'p2;
A51: p1 = pp^p2' by A31,Def2;
A52: len c1 +1 = n1+1 by A10,A11,Def1;
then A53: len c1 = n - 1 by A6,XCMPLX_1:2;
-(-(m-n)) = m-n; then -(m-n) < 0 by A5,REAL_1:66;
then A54: n+ -m < 0 by XCMPLX_1:162;
len c' = (n-1)+(len c -m+1) by A23,A53,FINSEQ_1:35
.= (n+ -1)+(len c -m+1) by XCMPLX_0:def 8 .= (n+ -1)+(len c + -m +1) by
XCMPLX_0:def 8
.= (n+-1)+(len c +(-m +1)) by XCMPLX_1:1 .= len c + ((n+ -1) + (-m +1)) by
XCMPLX_1:1
.= len c +(n+(-1+(-m+1))) by XCMPLX_1:1 .= len c + (n+ (-m + -1 +1)) by
XCMPLX_1:1 .= len c + (n+ (-m -1 +1)) by XCMPLX_0:def 8
.= len c + (n+ -m ) by XCMPLX_1:27;
hence
A55: len c' < len c by A54,REAL_2:173;
thus p1 is_vertex_seq_of c' by A3,A18,A19,A50,Th47;
then len p1 = len c' + 1 by Def7;
hence len p1 < len vs by A4,A55,REAL_1:53;
1<=1 + len c1 by NAT_1:37; then 1<=len pp by A18,Def7;
then p1.1 = pp.1 by Th14;
hence vs.1 = p1.1 by A15,Th12;
A56: p2.len p2 = vs.(len c + 1) by A17,Th12;
m-m<=len c -m by A13,REAL_1:49; then 0<=len c -m by XCMPLX_1:14;
then 0+1<=len c -m+1 by AXIOMS:24; then 1<len p2 by A21,A23,NAT_1:38;
hence vs.len vs = p1.len p1 by A4,A56,Th16;
set DL = {kk where kk is Nat: 1<=kk & kk<=n1};
set DR = {kk where kk is Nat: m<=kk & kk<= len c};
now let x be set;
hereby assume x in domfc; then consider k being Nat such that
A57: x=k & (1<=k & k<=n1 or m<=k & k<= len c);
x in DL or x in DR by A57;
hence x in DL \/ DR by XBOOLE_0:def 2;
end; assume A58: x in DL \/ DR;
per cases by A58,XBOOLE_0:def 2;
suppose x in DL; then consider k being Nat such that
A59: x=k & 1<=k & k<=n1;
thus x in domfc by A59;
suppose x in DR; then consider k being Nat such that
A60: x=k & m<=k & k<=len c;
thus x in domfc by A60;
end;
then A61: domfc = DL \/ DR by TARSKI:2;
A62: DL c= Seg len c & DR c= Seg len c proof
hereby let x be set; assume x in DL; then consider k being Nat such that
A63: x=k & 1<=k & k<=n1; k<=len c by A10,A63,AXIOMS:22;
hence x in Seg len c by A63,FINSEQ_1:3;
end; let x be set; assume x in DR; then consider k being Nat such that
A64: x=k & m<=k & k<=len c; 1<=k by A14,A64,AXIOMS:22;
hence x in Seg len c by A64,FINSEQ_1:3;
end;
then reconsider DL as finite set by FINSET_1:13;
reconsider DR as finite set by A62,FINSET_1:13;
now let i,j; assume i in DL; then consider k being Nat such that
A65: k=i & 1<=k & k<=n1;
assume j in DR; then consider l being Nat such that
A66: l=j & m<=l & l<=len c;
n1<m by A3,A7,NAT_1:38; then k<m by A65,AXIOMS:22;
hence i < j by A65,A66,AXIOMS:22;
end;
then A67: Sgm (DL \/ DR) = (Sgm DL)^(Sgm DR) by A62,FINSEQ_3:48;
A68: m+lc21 = len c -m + m by A23,XCMPLX_1:26 .= len c by XCMPLX_1:27;
then A69: card DR = lc21 + 1 by Th4 .= len c2 + -1 +1 by XCMPLX_0:def 8
.= len c2 +(-1+1) by XCMPLX_1:1 .= len c2;
A70: len Sgm DL = card DL & len Sgm DR = card DR by A62,FINSEQ_3:44; DL
=
Seg n1 by FINSEQ_1:def 1;
then A71: Sgm DL = idseq n1 by FINSEQ_3:54;
then A72: dom Sgm DL = Seg n1 by FINSEQ_2:54;
rng Sgm DL = DL by A62,FINSEQ_1:def 13;
then A73: rng Sgm DL c= dom fc by A32,A61,XBOOLE_1:7;
rng Sgm DR = DR by A62,FINSEQ_1:def 13;
then A74: rng Sgm DR c= dom fc by A32,A61,XBOOLE_1:7;
set SL = Sgm DL; set SR = Sgm DR;
now let p be set;
hereby assume
A75: p in c1; then consider x, y being set such that
A76: p=[x,y] by RELAT_1:def 1;
A77: x in dom c1 & y=c1.x by A75,A76,FUNCT_1:8;
then reconsider k = x as Nat;
A78: 1<=k & k<=len c1 by A77,FINSEQ_3:27;
then A79: x in dom SL by A6,A53,A72,FINSEQ_1:3;
then A80: k=SL.k by A71,A72,FINSEQ_2:56;
A81: k in domfc by A6,A53,A78;
then A82: x in dom (fc*SL) by A32,A79,A80,FUNCT_1:21; 0+1<=k by A77,FINSEQ_3:
27;
then consider i being Nat such that
A83: 0<=i & i<n1 & k=i+1 by A6,A53,A78,Th1;
(fc*SL).x = fc.k by A80,A82,FUNCT_1:22 .= c.(1+i) by A32,A35,A81,A83,
GRFUNC_1:8
.= y by A6,A10,A11,A53,A77,A83,Def1;
hence p in fc*(Sgm DL) by A76,A82,FUNCT_1:8;
end; assume
A84: p in fc*(Sgm DL); then consider x,y being set such that
A85: p=[x,y] by RELAT_1:def 1;
A86: x in dom (fc*SL) & y = (fc*SL).x by A84,A85,FUNCT_1:8;
then A87: (fc*SL).x = fc.(SL.x) by FUNCT_1:22;
A88: x in dom SL & SL.x in dom fc by A86,FUNCT_1:21;
then x in {kk where kk is Nat: 1<=kk & kk<=n1} by A72,FINSEQ_1:def 1;
then consider k such that
A89: k=x & 1<=k & k<=n1;
A90: k in dom fc by A32,A89;
A91: k=SL.k by A71,A72,A88,A89,FINSEQ_2:56;
A92: k in dom c1 by A6,A53,A89,FINSEQ_3:27; 0+1<=k by A89;
then consider i being Nat such that
A93: 0<=i & i<n1 & k=i+1 by A89,Th1;
c1.k = c.k by A6,A10,A11,A53,A93,Def1
.= y by A35,A86,A87,A89,A90,A91,GRFUNC_1:8;
hence p in c1 by A85,A89,A92,FUNCT_1:8;
end;
then A94: c1 = fc*(Sgm DL) by TARSKI:2;
now let p be set;
hereby assume
A95: p in c2; then consider x, y being set such that
A96: p=[x,y] by RELAT_1:def 1;
A97: x in dom c2 & y=c2.x by A95,A96,FUNCT_1:8;
then reconsider k = x as Nat;
A98: 1<=k & k<=len c2 by A97,FINSEQ_3:27;
A99: x in dom SR by A69,A70,A97,FINSEQ_3:31;
A100: m1+k=SR.k by A22,A25,A68,A98,Th5;
A101: SR.k in rng SR by A99,FUNCT_1:def 5;
then A102: x in dom (fc*SR) by A74,A99,FUNCT_1:21; 0+1<=k by A97,FINSEQ_3:27
;
then consider i being Nat such that
A103: 0<=i & i<len c2 & k=i+1 by A98,Th1;
(fc*SR).x = fc.(m1+k) by A100,A102,FUNCT_1:22 .= c.(m1+k) by A35,A74,
A100,A101,GRFUNC_1:8
.= c.(m1+1+i) by A103,XCMPLX_1:1 .= c.(m+i) by XCMPLX_1:27
.= y by A3,A4,A14,A97,A103,Def1;
hence p in fc*(Sgm DR) by A96,A102,FUNCT_1:8;
end; assume
A104: p in fc*(Sgm DR); then consider x,y being set such that
A105: p=[x,y] by RELAT_1:def 1;
A106: x in dom (fc*SR) & y = (fc*SR).x by A104,A105,FUNCT_1:8;
then A107: x in dom SR & SR.x in dom fc by FUNCT_1:21;
then reconsider k=x as Nat;
A108: k in dom c2 by A69,A70,A107,FINSEQ_3:31;
A109: 1<=k & k<=len c2 by A69,A70,A107,FINSEQ_3:27;
then A110: m1+k=SR.k by A22,A25,A68,Th5; 0+1<=k by A107,FINSEQ_3:27;
then consider i being Nat such that
A111: 0<=i & i<len c2 & k=i+1 by A109,Th1;
c2.k = c.(m+i) by A3,A4,A14,A111,Def1 .= c.(m1+1+i) by XCMPLX_1:27
.= c.(m1+k) by A111,XCMPLX_1:1 .= fc.(SR.k) by A35,A107,A110,GRFUNC_1:
8 .= y by A106,A107,FUNCT_1:23;
hence p in c2 by A105,A108,FUNCT_1:8;
end;
then A112: c2 = fc*(Sgm DR) by TARSKI:2;
Seq fc= fc*((Sgm DL)^(Sgm DR))by A32,A61,A67,FINSEQ_1:def 14;
hence Seq fc = c' by A73,A74,A94,A112,Th26;
set DL = {kk where kk is Nat: 1<=kk & kk<=n};
set DR = {kk where kk is Nat: m+1<=kk & kk<= len vs};
now let x be set;
hereby assume x in domfvs; then consider k being Nat such that
A113: x=k & (1<=k & k<=n or m+1<=k & k<= len vs);
x in DL or x in DR by A113;
hence x in DL \/ DR by XBOOLE_0:def 2;
end; assume A114: x in DL \/ DR;
per cases by A114,XBOOLE_0:def 2;
suppose x in DL; then consider k being Nat such that
A115: x=k & 1<=k & k<=n;
thus x in domfvs by A115;
suppose x in DR; then consider k being Nat such that
A116: x=k & m+1<=k & k<=len vs;
thus x in domfvs by A116;
end;
then A117: domfvs = DL \/ DR by TARSKI:2;
A118: DL c= Seg len vs & DR c= Seg len vs proof
hereby let x be set; assume x in DL; then consider k being Nat such that
A119: x=k & 1<=k & k<=n; k<=len vs by A15,A119,AXIOMS:22;
hence x in Seg len vs by A119,FINSEQ_1:3;
end; let x be set; assume x in DR; then consider k being Nat such that
A120: x=k & m+1<=k & k<=len vs;
1<=m+1 by NAT_1:37; then 1<=k by A120,AXIOMS:22;
hence x in Seg len vs by A120,FINSEQ_1:3;
end;
then reconsider DL as finite set by FINSET_1:13;
reconsider DR as finite set by A118,FINSET_1:13;
now let i,j; assume i in DL; then consider k being Nat such that
A121: k=i & 1<=k & k<=n;
assume j in DR; then consider l being Nat such that
A122: l=j & m+1<=l & l<=len vs; m<=m+1 by NAT_1:37;
then A123: m<=l by A122,AXIOMS:22; k<m by A3,A121,AXIOMS:22;
hence i < j by A121,A122,A123,AXIOMS:22;
end;
then A124: Sgm (DL \/ DR) = (Sgm DL)^(Sgm DR) by A118,FINSEQ_3:48;
1<=len p2 by A21,NAT_1:37;
then 1-1<=len p2 -1 by REAL_1:49;
then len p2 -'1 = len p2 -1 by BINARITH:def 3;
then reconsider lp21 = len p2 -1 as Nat;
1<=lp21 by A21,A23,A24,XCMPLX_1:26;
then 1-1<=lp21 -1 by REAL_1:49;
then lp21 -'1 = lp21 -1 by BINARITH:def 3;
then reconsider lp22 = lp21 -1 as Nat;
A125: m+1+lp22 = m+((lp21 -1)+1) by XCMPLX_1:1
.= m+(len c -m +1 +1 -1) by A21,A23,XCMPLX_1:27
.= m+(len c -m +1) by XCMPLX_1:26 .= (len c -m + m)+1 by XCMPLX_1:1
.= len c +1 by XCMPLX_1:27;
then A126: card DR = lp21 -1+1 by A4,Th4 .= lp21 by XCMPLX_1:27;
A127: 1<=m+1 & m+1<=len c +1+1 by A3,A4,AXIOMS:24,NAT_1:37;
len p2 +m = len c +1+1 by A4,A14,A30,Def1
.= len p2' +(m+1) by A4,A127,Def1 .= (len p2'+1)+m by XCMPLX_1:1;
then len p2 -1 = len p2'+1-1 by XCMPLX_1:2;
then A128: len p2' = lp21 by XCMPLX_1:26;
A129: len Sgm DL = card DL & len Sgm DR = card DR by A118,FINSEQ_3:44;
A130: len pp = n by A6,A20,A52,XCMPLX_1:27; DL = Seg n by FINSEQ_1:def 1;
then A131: Sgm DL = idseq n by FINSEQ_3:54;
then A132: dom Sgm DL = Seg n by FINSEQ_2:54;
rng Sgm DL = DL by A118,FINSEQ_1:def 13;
then A133: rng Sgm DL c= dom fvs by A41,A117,XBOOLE_1:7;
rng Sgm DR = DR by A118,FINSEQ_1:def 13;
then A134: rng Sgm DR c= dom fvs by A41,A117,XBOOLE_1:7;
set SL = Sgm DL; set SR = Sgm DR;
now let p be set;
hereby assume
A135: p in pp; then consider x, y being set such that
A136: p=[x,y] by RELAT_1:def 1;
A137: x in dom pp & y=pp.x by A135,A136,FUNCT_1:8;
then reconsider k = x as Nat;
A138: 1<=k & k<=len pp by A137,FINSEQ_3:27;
then A139: x in dom SL by A130,A132,FINSEQ_1:3;
then A140: k=SL.k by A131,A132,FINSEQ_2:56;
A141: k in domfvs by A130,A138;
then A142: x in dom (fvs*SL) by A41,A139,A140,FUNCT_1:21; 0+1<=k by A137,
FINSEQ_3:27;
then consider i being Nat such that
A143: 0<=i & i<n & k=i+1 by A130,A138,Th1;
(fvs*SL).x = fvs.k by A140,A142,FUNCT_1:22 .= vs.(1+i) by A41,A44,A141,
A143,GRFUNC_1:8 .= y by A15,A16,A130,A137,A143,Def1;
hence p in fvs*(Sgm DL) by A136,A142,FUNCT_1:8;
end; assume
A144: p in fvs*(Sgm DL); then consider x,y being set such that
A145: p=[x,y] by RELAT_1:def 1;
A146: x in dom (fvs*SL) & y = (fvs*SL).x by A144,A145,FUNCT_1:8;
then A147: (fvs*SL).x = fvs.(SL.x) by FUNCT_1:22;
A148: x in dom SL & SL.x in dom fvs by A146,FUNCT_1:21;
then x in {kk where kk is Nat: 1<=kk & kk<=n} by A132,FINSEQ_1:def 1;
then consider k such that
A149: k=x & 1<=k & k<=n;
A150: k in dom fvs by A41,A149;
A151: k=SL.k by A131,A132,A148,A149,FINSEQ_2:56;
A152: k in dom pp by A130,A149,FINSEQ_3:27; 0+1<=k by A149;
then consider i being Nat such that
A153: 0<=i & i<n & k=i+1 by A149,Th1;
pp.k = vs.k by A15,A16,A130,A153,Def1
.= y by A44,A146,A147,A149,A150,A151,GRFUNC_1:8;
hence p in pp by A145,A149,A152,FUNCT_1:8;
end;
then A154: pp = fvs*(Sgm DL) by TARSKI:2;
A155: m+1+lp22 =m+((lp21 -1)+1) by XCMPLX_1:1
.= m+lp21 by XCMPLX_1:27;
A156: 1<=m+1 & m+1<=len c +1+1 by A3,A4,NAT_1:37,REAL_1:55;
now let p be set;
hereby assume
A157: p in p2'; then consider x, y being set such that
A158: p=[x,y] by RELAT_1:def 1;
A159: x in dom p2' & y=p2'.x by A157,A158,FUNCT_1:8;
then reconsider k = x as Nat;
A160: 1<=k & k<=len p2' by A159,FINSEQ_3:27;
A161: x in dom SR by A126,A128,A129,A159,FINSEQ_3:31;
A162: m+k=SR.k by A4,A125,A128,A155,A160,Th5;
A163: SR.k in rng SR by A161,FUNCT_1:def 5;
then A164: x in dom (fvs*SR) by A134,A161,FUNCT_1:21; 0+1<=k by A159,FINSEQ_3
:27;
then consider i being Nat such that
A165: 0<=i & i<len p2' & k=i+1 by A160,Th1;
(fvs*SR).x = fvs.(m+k) by A162,A164,FUNCT_1:22 .= vs.(m+k) by A44,A134,
A162,A163,GRFUNC_1:8
.= vs.(m+1+i) by A165,XCMPLX_1:1 .= y by A4,A156,A159,A165,Def1;
hence p in fvs*(Sgm DR) by A158,A164,FUNCT_1:8;
end; assume
A166: p in fvs*(Sgm DR); then consider x,y being set such that
A167: p=[x,y] by RELAT_1:def 1;
A168: x in dom (fvs*SR) & y = (fvs*SR).x by A166,A167,FUNCT_1:8;
then A169: x in dom SR & SR.x in dom fvs by FUNCT_1:21;
then reconsider k=x as Nat;
A170: k in dom p2' by A126,A128,A129,A169,FINSEQ_3:31;
A171: 1<=k & k<=len p2' by A126,A128,A129,A169,FINSEQ_3:27;
then A172: m+k=SR.k by A4,A125,A128,A155,Th5; 0+1<=k by A169,FINSEQ_3:27;
then consider i being Nat such that
A173: 0<=i & i<len p2' & k=i+1 by A171,Th1;
p2'.k = vs.(m+1+i) by A4,A156,A173,Def1
.= vs.(m+k) by A173,XCMPLX_1:1 .= fvs.(SR.k) by A44,A169,A172,GRFUNC_1
:8 .= y by A168,A169,FUNCT_1:23;
hence p in p2' by A167,A170,FUNCT_1:8;
end;
then A174: p2' = fvs*(Sgm DR) by TARSKI:2;
Seq fvs = fvs*((Sgm DL)^(Sgm DR)) by A41,A117,A124,FINSEQ_1:def 14;
hence Seq fvs = p1 by A51,A133,A134,A154,A174,Th26;
suppose
A175: n=1 & m <> len vs;
then A176: m < len vs by A3,REAL_1:def 5;
then A177: m<=len c by A4,NAT_1:38;
A178: 1 < m by A3,AXIOMS:22;
A179: 1<=m & m<=len c & len c <=len c by A3,A4,A176,AXIOMS:22,NAT_1:38;
reconsider c2 = (m,len c)-cut c as Chain of G by A177,A178,Th44;
set p2 = (m,len c+1)-cut vs;
A180: p2 is_vertex_seq_of c2 by A2,A177,A178,Th45;
set domfc = {k: m<=k & k<= len c};
deffunc F(set) = c.$1;
consider fc being Function such that
A181: dom fc = domfc and
A182: for x st x in domfc holds fc.x = F(x) from Lambda;
domfc c= Seg len c proof let x be set; assume x in domfc;
then consider kk being Nat such that
A183: x = kk & m<=kk & kk<= len c;
1<=kk & kk<=len c by A178,A183,AXIOMS:22;
hence x in Seg len c by A183,FINSEQ_1:3;
end;
then reconsider fc as FinSubsequence by A181,FINSEQ_1:def 12;
A184: fc c= c proof let p be set; assume
A185: p in fc; then consider x, y such that
A186: [x,y] = p by RELAT_1:def 1;
A187: x in dom fc & y = fc.x by A185,A186,FUNCT_1:8;
then consider kk being Nat such that
A188: x = kk & m<=kk & kk<= len c by A181;
1<=kk & kk<=len c by A178,A188,AXIOMS:22;
then A189: x in dom c by A188,FINSEQ_3:27;
y = c.kk by A181,A182,A187,A188;
hence p in c by A186,A188,A189,FUNCT_1:8;
end;
then reconsider fc as FinSubsequence of c by Def5;
take fc;
set domfvs = {k: m<=k & k<= len vs};
deffunc F(set) = vs.$1;
consider fvs being Function such that
A190: dom fvs = domfvs and
A191: for x st x in domfvs holds fvs.x = F(x) from Lambda;
domfvs c= Seg len vs proof let x be set; assume x in domfvs;
then consider kk being Nat such that
A192: x = kk & m<=kk & kk<= len vs;
1<=kk & kk<=len vs by A178,A192,AXIOMS:22;
hence x in Seg len vs by A192,FINSEQ_1:3;
end;
then reconsider fvs as FinSubsequence by A190,FINSEQ_1:def 12;
A193: fvs c= vs proof let p be set; assume
A194: p in fvs; then consider x, y such that
A195: [x,y] = p by RELAT_1:def 1;
A196: x in dom fvs & y = fvs.x by A194,A195,FUNCT_1:8;
then consider kk being Nat such that
A197: x = kk & m<=kk & kk<= len vs by A190;
1<=kk & kk<=len vs by A178,A197,AXIOMS:22;
then A198: x in dom vs by A197,FINSEQ_3:27;
y = vs.kk by A190,A191,A196,A197;
hence p in vs by A195,A197,A198,FUNCT_1:8;
end;
then reconsider fvs as FinSubsequence of vs by Def5;
take fvs; take c1 = c2; take p1 = p2;
len c2 +m = len c +1 by A3,A4,A175,Def1;
then A199: len c2 = len c +1-m by XCMPLX_1:26 .=len c - m + 1 by XCMPLX_1:29;
m-m<=len c -m by A177,REAL_1:49; then 0<=len c -m by XCMPLX_1:14;
then A200: 0+1<=len c -m +1 by AXIOMS:24;
1-1<=m-1 by A178,REAL_1:49;
then m-'1 = m-1 by BINARITH:def 3; then reconsider m1 = m-1 as Nat;
A201: m = m1 +1 by XCMPLX_1:27;
1-1<=len c2 -1 by A199,A200,REAL_1:49;
then len c2 -'1 = len c2 -1 by BINARITH:def 3;
then reconsider lc21 = len c2 -1 as Nat;
A202: m+lc21 = m1+(len c2 -1+1) by A201,XCMPLX_1:1
.= m1+len c2 by XCMPLX_1:27;
A203: 1<=m & m<=len c +1+1 & len c +1<=len vs by A3,A4,A175,NAT_1:37;
then len p2 +m = len c +1 +1 by Def1;
then A204: len p2 = len c +1 +1 -m by XCMPLX_1:26 .= len c +1 -m +1 by XCMPLX_1
:29
.= len c -m +1+1 by XCMPLX_1:29;
then A205: 1<=len p2 by A199,NAT_1:37;
A206: len c2 = len c +-m+1 by A199,XCMPLX_0:def 8.= len c +(-m+1) by XCMPLX_1:1
;
1-1 < m-1 by A178,REAL_1:54;
then 0 < -(-(m-1)); then -(m-1) < 0 by REAL_1:66;
then -m + 1 < 0 by XCMPLX_1:162;
hence
A207: len c1 < len c by A206,REAL_2:173;
thus p1 is_vertex_seq_of c1 by A2,A179,Th45; len p1 = len c1 + 1 by A180,Def7
;
hence len p1 < len vs by A4,A207,REAL_1:53;
thus vs.1 = p1.1 by A3,A4,A175,Th12;
thus vs.len vs = p1.len p1 by A3,A4,A175,Th12;
A208: domfc c= Seg len c proof
let x be set; assume x in domfc; then consider k being Nat such that
A209: x=k & m<=k & k<=len c; 1<=k by A178,A209,AXIOMS:22;
hence x in Seg len c by A209,FINSEQ_1:3;
end;
then reconsider domfc as finite set by FINSET_1:13;
1-1<=len c2 -1 by A199,A200,REAL_1:49;
then len c2 -'1 = len c2 -1 by BINARITH:def 3;
then reconsider lc21 = len c2 -1 as Nat;
A210: m+lc21 = len c -m + m by A199,XCMPLX_1:26 .= len c by XCMPLX_1:27;
then A211: card domfc = lc21 + 1 by Th4 .= len c2 + -1 +1 by XCMPLX_0:def 8
.= len c2 +(-1+1) by XCMPLX_1:1 .= len c2;
A212: len Sgm domfc = card domfc by A208,FINSEQ_3:44;
A213: rng Sgm domfc c= dom fc by A181,A208,FINSEQ_1:def 13;
set SR = Sgm domfc;
now let p be set;
hereby assume
A214: p in c2; then consider x, y being set such that
A215: p=[x,y] by RELAT_1:def 1;
A216: x in dom c2 & y=c2.x by A214,A215,FUNCT_1:8;
then reconsider k = x as Nat;
A217: 1<=k & k<=len c2 by A216,FINSEQ_3:27;
A218: x in dom SR by A211,A212,A216,FINSEQ_3:31;
A219: m1+k=SR.k by A201,A202,A210,A217,Th5;
A220: SR.k in rng SR by A218,FUNCT_1:def 5;
then A221: x in dom (fc*SR) by A213,A218,FUNCT_1:21; 0+1<=k by A216,FINSEQ_3:
27;
then consider i being Nat such that
A222: 0<=i & i<len c2 & k=i+1 by A217,Th1;
(fc*SR).x = fc.(m1+k) by A219,A221,FUNCT_1:22 .= c.(m1+k) by A184,A213,
A219,A220,GRFUNC_1:8
.= c.(m1+1+i) by A222,XCMPLX_1:1 .= c.(m+i) by XCMPLX_1:27
.= y by A3,A4,A175,A216,A222,Def1;
hence p in fc*(Sgm domfc) by A215,A221,FUNCT_1:8;
end; assume
A223: p in fc*(Sgm domfc); then consider x,y being set such that
A224: p=[x,y] by RELAT_1:def 1;
A225: x in dom (fc*SR) & y = (fc*SR).x by A223,A224,FUNCT_1:8;
then A226: x in dom SR & SR.x in dom fc by FUNCT_1:21;
then reconsider k=x as Nat;
A227: k in dom c2 by A211,A212,A226,FINSEQ_3:31;
A228: 1<=k & k<=len c2 by A211,A212,A226,FINSEQ_3:27;
then A229: m1+k=SR.k by A201,A202,A210,Th5; 0+1<=k by A226,FINSEQ_3:27;
then consider i being Nat such that
A230: 0<=i & i<len c2 & k=i+1 by A228,Th1;
c2.k = c.(m+i) by A3,A4,A175,A230,Def1 .= c.(m1+1+i) by XCMPLX_1:27
.= c.(m1+k) by A230,XCMPLX_1:1 .= fc.(SR.k) by A184,A226,A229,GRFUNC_1
:8 .= y by A225,A226,FUNCT_1:23;
hence p in c2 by A224,A227,FUNCT_1:8;
end;
then c2 = fc*(Sgm domfc) by TARSKI:2;
hence Seq fc = c1 by A181,FINSEQ_1:def 14;
A231: domfvs c= Seg len vs proof
let x be set; assume x in domfvs; then consider k being Nat such that
A232: x=k & m<=k & k<=len vs; 1<=k by A178,A232,AXIOMS:22;
hence x in Seg len vs by A232,FINSEQ_1:3;
end;
then reconsider domfvs as finite set by FINSET_1:13;
1-1<=len p2 -1 by A205,REAL_1:49;
then len p2 -'1 = len p2 -1 by BINARITH:def 3;
then reconsider lp21 = len p2 -1 as Nat;
A233: m+lp21 =len c -m+1+m by A204,XCMPLX_1:26 .= len c -m + m +1 by XCMPLX_1:1
.= len c+1 by XCMPLX_1:27;
A234: m+lp21 = m1+(len p2 -1+1) by A201,XCMPLX_1:1
.= m1+len p2 by XCMPLX_1:27;
A235: card domfvs = lp21 + 1 by A4,A233,Th4 .= len p2 + -1 +1 by XCMPLX_0:def
8
.= len p2 +(-1+1) by XCMPLX_1:1 .= len p2;
A236: len Sgm domfvs = card domfvs by A231,FINSEQ_3:44;
A237: rng Sgm domfvs c= dom fvs by A190,A231,FINSEQ_1:def 13;
set SR = Sgm domfvs;
now let p be set;
hereby assume
A238: p in p2; then consider x, y being set such that
A239: p=[x,y] by RELAT_1:def 1;
A240: x in dom p2 & y=p2.x by A238,A239,FUNCT_1:8;
then reconsider k = x as Nat;
A241: 1<=k & k<=len p2 by A240,FINSEQ_3:27;
A242: x in dom SR by A235,A236,A240,FINSEQ_3:31;
A243: m1+k=SR.k by A4,A201,A233,A234,A241,Th5; A244: SR.k in rng SR by A242,
FUNCT_1:def 5
;
then A245: x in dom (fvs*SR) by A237,A242,FUNCT_1:21; 0+1<=k by A240,FINSEQ_3
:27;
then consider i being Nat such that
A246: 0<=i & i<len p2 & k=i+1 by A241,Th1;
(fvs*SR).x = fvs.(m1+k) by A243,A245,FUNCT_1:22 .= vs.(m1+k) by A193,
A237,A243,A244,GRFUNC_1:8
.= vs.(m1+1+i) by A246,XCMPLX_1:1 .= vs.(m+i) by XCMPLX_1:27
.= y by A203,A240,A246,Def1;
hence p in fvs*(Sgm domfvs) by A239,A245,FUNCT_1:8;
end; assume
A247: p in fvs*(Sgm domfvs); then consider x,y being set such that
A248: p=[x,y] by RELAT_1:def 1;
A249: x in dom (fvs*SR) & y = (fvs*SR).x by A247,A248,FUNCT_1:8;
then A250: x in dom SR & SR.x in dom fvs by FUNCT_1:21;
then reconsider k=x as Nat;
A251: k in dom p2 by A235,A236,A250,FINSEQ_3:31;
A252: 1<=k & k<=len p2 by A235,A236,A250,FINSEQ_3:27;
then A253: m1+k=SR.k by A4,A201,A233,A234,Th5; 0+1<=k by A250,FINSEQ_3:27;
then consider i being Nat such that
A254: 0<=i & i<len p2 & k=i+1 by A252,Th1;
p2.k = vs.(m+i) by A203,A254,Def1 .= vs.(m1+1+i) by XCMPLX_1:27
.= vs.(m1+k) by A254,XCMPLX_1:1 .= fvs.(SR.k) by A193,A250,A253,
GRFUNC_1:8 .= y by A249,A250,FUNCT_1:23
;
hence p in p2 by A248,A251,FUNCT_1:8;
end;
then p2 = fvs*(Sgm domfvs) by TARSKI:2;
hence Seq fvs = p1 by A190,FINSEQ_1:def 14;
suppose
A255: n<>1 & m = len vs;
then 1 < n by A3,REAL_1:def 5;
then 1 + 1<=n by NAT_1:38; then A256: 1+1-1<=n-1 by REAL_1:49;
n < len vs by A3,AXIOMS:22; then A257: n-1 < len c +1-1 by A4,REAL_1:54;
then A258: n-1 < len c by XCMPLX_1:26;
A259: 1<=1 & 1<=n1 & n1<=len c by A6,A256,A257,XCMPLX_1:26;
A260: 1<=n1+1 by NAT_1:37;
reconsider c1 = (1,n1)-cut c as Chain of G by A6,A256,A258,Th44;
set pp = (1,n)-cut vs; A261: 1<=n & n<=len vs by A3,AXIOMS:22;
A262: 1<=n+1 by NAT_1:37;
A263: pp is_vertex_seq_of c1 by A2,A6,A7,A256,A258,Th45;
then A264: len pp = len c1 + 1 by Def7;
reconsider domfc = {k: 1<=k & k<=n1} as set;
deffunc F(set) = c.$1;
consider fc being Function such that
A265: dom fc = domfc and
A266: for x st x in domfc holds fc.x = F(x) from Lambda;
domfc c= Seg len c proof let x be set; assume x in domfc;
then consider kk being Nat such that
A267: x = kk & 1<=kk & kk<=n1; 1<=kk & kk<=len c by A6,A258,A267,AXIOMS:22
;
hence x in Seg len c by A267,FINSEQ_1:3;
end;
then reconsider fc as FinSubsequence by A265,FINSEQ_1:def 12;
A268: fc c= c proof let p be set; assume
A269: p in fc; then consider x, y such that
A270: [x,y] = p by RELAT_1:def 1;
A271: x in dom fc & y = fc.x by A269,A270,FUNCT_1:8;
then consider kk being Nat such that
A272: x = kk & 1<=kk & kk<=n1 by A265;
1<=kk & kk<=len c by A6,A258,A272,AXIOMS:22;
then A273: x in dom c by A272,FINSEQ_3:27; y = c.kk by A265,A266,A271,A272;
hence p in c by A270,A272,A273,FUNCT_1:8;
end;
then reconsider fc as FinSubsequence of c by Def5;
take fc;
set domfvs = {k: 1<=k & k<=n};
deffunc F(set) = vs.$1;
consider fvs being Function such that
A274: dom fvs = domfvs and
A275: for x st x in domfvs holds fvs.x = F(x) from Lambda;
domfvs c= Seg len vs proof let x be set; assume x in domfvs;
then consider kk being Nat such that
A276: x = kk & 1<=kk & kk<=n; 1<=kk & kk<=len vs by A261,A276,AXIOMS:22;
hence x in Seg len vs by A276,FINSEQ_1:3;
end;
then reconsider fvs as FinSubsequence by A274,FINSEQ_1:def 12;
A277: fvs c= vs proof let p be set; assume
A278: p in fvs; then consider x, y such that
A279: [x,y] = p by RELAT_1:def 1;
A280: x in dom fvs & y = fvs.x by A278,A279,FUNCT_1:8;
then consider kk being Nat such that
A281: x = kk & 1<=kk & kk<=n by A274;
1<=kk & kk<=len vs by A261,A281,AXIOMS:22;
then A282: x in dom vs by A281,FINSEQ_3:27; y = vs.kk by A274,A275,A280,A281
;
hence p in vs by A279,A281,A282,FUNCT_1:8;
end;
then reconsider fvs as FinSubsequence of vs by Def5;
take fvs; take c' = c1; take p1 = pp;
len c1+1=n1+1 by A6,A258,A260,Def1;
then A283: len c1 = n1+1-1 by XCMPLX_1:26 .= n - 1 by A6,XCMPLX_1:26;
hence
len c' < len c by A257,XCMPLX_1:26;
thus p1 is_vertex_seq_of c' by A2,A7,A259,Th45; len p1 = len c1 + 1 by A263,
Def7;
hence len p1 < len vs by A4,A258,A283,REAL_1:53;
thus vs.1 = p1.1 by A261,Th12;
thus vs.len vs = p1.len p1 by A3,A255,Th12;
domfc c= Seg len c proof
let x be set; assume x in domfc; then consider k being Nat such that
A284: x=k & 1<=k & k<=n1; k<=len c by A6,A258,A284,AXIOMS:22;
hence x in Seg len c by A284,FINSEQ_1:3;
end;
then reconsider domfc as finite set by FINSET_1:13; domfc = Seg n1
by FINSEQ_1:def 1;
then A285: Sgm domfc = idseq n1 by FINSEQ_3:54;
then A286: dom Sgm domfc = Seg n1 by FINSEQ_2:54;
set SL = Sgm domfc;
now let p be set;
hereby assume
A287: p in c1; then consider x, y being set such that
A288: p=[x,y] by RELAT_1:def 1;
A289: x in dom c1 & y=c1.x by A287,A288,FUNCT_1:8;
then reconsider k = x as Nat;
A290: 1<=k & k<=len c1 by A289,FINSEQ_3:27;
then A291: x in dom SL by A6,A283,A286,FINSEQ_1:3;
then A292: k=SL.k by A285,A286,FINSEQ_2:56;
A293: k in domfc by A6,A283,A290;
then A294: x in dom (fc*SL) by A265,A291,A292,FUNCT_1:21; 0+1<=k by A289,
FINSEQ_3:27;
then consider i being Nat such that
A295: 0<=i & i<n1 & k=i+1 by A6,A283,A290,Th1;
(fc*SL).x = fc.k by A292,A294,FUNCT_1:22 .= c.(1+i) by A265,A268,A293,
A295,GRFUNC_1:8
.= y by A6,A258,A260,A283,A289,A295,Def1;
hence p in fc*(Sgm domfc) by A288,A294,FUNCT_1:8;
end; assume
A296: p in fc*(Sgm domfc); then consider x,y being set such that
A297: p=[x,y] by RELAT_1:def 1;
A298: x in dom (fc*SL) & y = (fc*SL).x by A296,A297,FUNCT_1:8;
then A299: (fc*SL).x = fc.(SL.x) by FUNCT_1:22;
A300: x in dom SL & SL.x in dom fc by A298,FUNCT_1:21;
then x in {kk where kk is Nat: 1<=kk & kk<=n1} by A286,FINSEQ_1:def 1;
then consider k such that
A301: k=x & 1<=k & k<=n1;
A302: k in dom fc by A265,A301;
A303: k=SL.k by A285,A286,A300,A301,FINSEQ_2:56;
A304: k in dom c1 by A6,A283,A301,FINSEQ_3:27; 0+1<=k by A301;
then consider i being Nat such that
A305: 0<=i & i<n1 & k=i+1 by A301,Th1;
c1.k = c.k by A6,A258,A260,A283,A305,Def1
.= y by A268,A298,A299,A301,A302,A303,GRFUNC_1:8;
hence p in c1 by A297,A301,A304,FUNCT_1:8;
end; then c1 = fc*(Sgm domfc) by TARSKI:2;
hence Seq fc = c' by A265,FINSEQ_1:def 14;
domfvs c= Seg len vs proof
let x be set; assume x in domfvs; then consider k being Nat such that
A306: x=k & 1<=k & k<=n; k<=len vs by A261,A306,AXIOMS:22;
hence x in Seg len vs by A306,FINSEQ_1:3;
end; then reconsider domfvs as finite set by FINSET_1:13;
A307: len pp = n by A264,A283,XCMPLX_1:27;
domfvs = Seg n by FINSEQ_1:def 1;
then A308: Sgm domfvs = idseq n by FINSEQ_3:54;
then A309: dom Sgm domfvs = Seg n by FINSEQ_2:54;
set SL = Sgm domfvs;
now let p be set;
hereby assume
A310: p in pp; then consider x, y being set such that
A311: p=[x,y] by RELAT_1:def 1;
A312: x in dom pp & y=pp.x by A310,A311,FUNCT_1:8;
then reconsider k = x as Nat;
A313: 1<=k & k<=len pp by A312,FINSEQ_3:27;
then A314: x in dom SL by A307,A309,FINSEQ_1:3;
then A315: k=SL.k by A308,A309,FINSEQ_2:56;
A316: k in domfvs by A307,A313;
then A317: x in dom (fvs*SL) by A274,A314,A315,FUNCT_1:21; 0+1<=k by A312,
FINSEQ_3:27;
then consider i being Nat such that
A318: 0<=i & i<n & k=i+1 by A307,A313,Th1;
(fvs*SL).x = fvs.k by A315,A317,FUNCT_1:22 .= vs.(1+i) by A274,A277,
A316,A318,GRFUNC_1:8
.= y by A261,A262,A307,A312,A318,Def1;
hence p in fvs*(Sgm domfvs) by A311,A317,FUNCT_1:8;
end; assume
A319: p in fvs*(Sgm domfvs); then consider x,y being set such that
A320: p=[x,y] by RELAT_1:def 1;
A321: x in dom (fvs*SL) & y = (fvs*SL).x by A319,A320,FUNCT_1:8;
then A322: (fvs*SL).x = fvs.(SL.x) by FUNCT_1:22;
A323: x in dom SL & SL.x in dom fvs by A321,FUNCT_1:21;
then x in {kk where kk is Nat: 1<=kk & kk<=n} by A309,FINSEQ_1:def 1;
then consider k such that
A324: k=x & 1<=k & k<=n;
A325: k in dom fvs by A274,A324;
A326: k=SL.k by A308,A309,A323,A324,FINSEQ_2:56;
A327: k in dom pp by A307,A324,FINSEQ_3:27; 0+1<=k by A324;
then consider i being Nat such that
A328: 0<=i & i<n & k=i+1 by A324,Th1;
pp.k = vs.k by A261,A262,A307,A328,Def1
.= y by A277,A321,A322,A324,A325,A326,GRFUNC_1:8;
hence p in pp by A320,A324,A327,FUNCT_1:8;
end;
then pp = fvs*(Sgm domfvs) by TARSKI:2;
hence Seq fvs = p1 by A274,FINSEQ_1:def 14;
end;
theorem vs is_vertex_seq_of c implies
ex fc being FinSubsequence of c, fvs being FinSubsequence of vs, sc, vs1
st Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc &
vs.1 = vs1.1 & vs.len vs = vs1.len vs1 proof assume
A1: vs is_vertex_seq_of c;
per cases;
suppose A2: c is simple Chain of G;
reconsider fc = c as FinSubsequence of c by Th28;
reconsider fvs = vs as FinSubsequence of vs by Th28;
reconsider sc = c as simple Chain of G by A2;
take fc, fvs, sc, vs;
thus Seq fc = sc & Seq fvs = vs by Th24;
thus vs is_vertex_seq_of sc by A1;
thus vs.1 = vs.1 & vs.len vs = vs.len vs;
suppose A3: not c is simple Chain of G;
defpred P[Nat] means
ex fc being FinSubsequence of c, fvs being FinSubsequence of vs, c1, vs1
st Seq fc = c1 & Seq fvs = vs1 & vs1 is_vertex_seq_of c1 &
vs.1 = vs1.1 & vs.len vs = vs1.len vs1 &
len c1 = $1 & not c1 is simple Chain of G;
P[len c] proof
reconsider fc = c as FinSubsequence of c by Th28;
reconsider fvs = vs as FinSubsequence of vs by Th28;
take fc, fvs, c,vs;
thus Seq fc = c & Seq fvs = vs by Th24;
thus vs is_vertex_seq_of c by A1;
thus vs.1 = vs.1 & vs.len vs = vs.len vs;
thus len c = len c & not c is simple Chain of G by A3;
end;
then A4: ex k st P[k]; consider k such that
A5: P[k] & for n being Nat st P[n] holds k<=n from Min(A4);
consider fc being FinSubsequence of c, fvs being FinSubsequence of vs,
c1, vs1 such that
A6: Seq fc = c1 & Seq fvs = vs1 & vs1 is_vertex_seq_of c1 &
vs.1 = vs1.1 & vs.len vs = vs1.len vs1 &
len c1 = k & not c1 is simple Chain of G by A5;
consider fc1 being FinSubsequence of c1, fvs1 being FinSubsequence of vs1,
c2, vs2 such that
A7: len c2 < len c1 & vs2 is_vertex_seq_of c2 & len vs2 < len vs1 &
vs1.1 = vs2.1 & vs1.len vs1 = vs2.len vs2 &
Seq fc1 = c2 & Seq fvs1 = vs2 by A6,Th52;
reconsider fc'=fc|rng((Sgm dom fc)|dom fc1) as FinSubsequence of c by Th29;
A8: Seq fc' = c2 by A6,A7,Th30;
reconsider fvs'=fvs|rng((Sgm dom fvs)|dom fvs1) as FinSubsequence of vs
by Th29;
A9: Seq fvs' = vs2 by A6,A7,Th30;
then c2 is simple Chain of G implies thesis by A6,A7,A8;
hence thesis by A5,A6,A7,A8,A9;
end;
definition let G;
cluster empty -> one-to-one Chain of G;
correctness;
end;
theorem p is Path of G implies p|Seg(n) is Path of G proof assume
A1: p is Path of G;
reconsider q=p|(Seg n) as FinSequence by FINSEQ_1:19;
now let n1,m1 be Nat; assume that
A2: 1<=n1 and
A3: n1 < m1 and
A4: m1<=len q; 1<m1 by A2,A3,AXIOMS:22;
then m1 in dom q by A4,FINSEQ_3:27;
then A5: q.m1=p.m1 by FUNCT_1:68; n1 < len q by A3,A4,AXIOMS:22;
then n1 in dom q by A2,FINSEQ_3:27;
then A6: q.n1=p.n1 by FUNCT_1:68;
dom q c= dom p by FUNCT_1:76; then dom q c= Seg len p by FINSEQ_1:def 3;
then Seg len q c= Seg len p by FINSEQ_1:def 3;
then len q<=len p by FINSEQ_1:7;
then m1<=len p by A4,AXIOMS:22;
hence q.n1 <> q.m1 by A1,A2,A3,A5,A6,GRAPH_1:def 13;
end; hence thesis by A1,GRAPH_1:4,def 13;
end;
definition let G;
cluster simple Path of G;
existence proof consider q being empty Chain of G;
reconsider q as one-to-one Chain of G;
take q; consider x being Element of the Vertices of G;
reconsider p = <*x*> as FinSequence of the Vertices of G;
take p;
thus p is_vertex_seq_of q by Lm7;
let n,m; assume 1<=n & n<m & m<=len p & p.n = p.m;
then 1<m & m<=1 by AXIOMS:22,FINSEQ_1:56;
hence n =1 & m = len p;
end;
end;
theorem
2<len sc implies sc is Path of G
proof assume
A1: 2 < len sc; assume not sc is Path of G; then consider m, n such that
A2: 1<=m & m<n & n<=len sc & sc.m = sc.n by GRAPH_1:def 13;
consider vs such that
A3: vs is_vertex_seq_of sc &
(for n, m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs)
by Def10;
A4: len vs = len sc + 1 by A3,Def7; A5: m<=len sc by A2,AXIOMS:22;
A6: 1<=n by A2,AXIOMS:22;
A7: 1<=m & m<n & n<=len vs by A2,A4,NAT_1:37;
A8: 1<=m+1 & m+1<n+1 & n+1<=len vs by A2,A4,AXIOMS:24,NAT_1:37,REAL_1:53;
then A9: 1<=m & m<n+1 & n+1<=len vs by A2,NAT_1:37;
set v1 = vs/.m; set v2 = vs/.(m+1);
A10: sc.m joins v1, v2 by A2,A3,A5,Def7;
set v1' = vs/.n; set v2' = vs/.(n+1);
A11: sc.n joins v1', v2' by A2,A3,A6,Def7;
m<=len vs & m+1<=len vs & 1<=n+1 by A8,A9,AXIOMS:22;
then A12: v1=vs.m & v2=vs.(m+1) & v1'=vs.n & v2'=vs.(n+1)
by A6,A7,A8,FINSEQ_4:24;
per cases by A2,A10,A11,Th32;
suppose A13: v1=v1' & v2=v2'; then m=1 & n=len vs by A3,A7,A12;
hence contradiction by A3,A8,A12,A13;
suppose
A14: v1=v2' & v2=v1';
then A15: m=1 & n+1=len vs by A3,A9,A12; m+1<=n by A2,NAT_1:38;
then m+1 < n or m+1=n by REAL_1:def 5;
hence contradiction by A1,A3,A4,A7,A12,A14,A15,REAL_1:53;
end;
theorem sc is Path of G iff len sc = 0 or len sc = 1 or sc.1<>sc.2 proof
hereby assume
A1: sc is Path of G; assume
A2: not len sc = 0; assume
A3: not len sc = 1; assume
A4: sc.1 = sc.2;
len sc >1 by A2,A3,CQC_THE1:2;
then 1+1<=len sc by NAT_1:38; hence contradiction by A1,A4,GRAPH_1:def 13;
end; assume
A5: len sc = 0 or len sc = 1 or sc.1<>sc.2;
per cases by A5;
suppose len sc = 0;
then for n, m st 1<=n & n<m & m<=len sc holds sc.n<>sc.m by AXIOMS:22;
hence sc is Path of G by GRAPH_1:def 13;
suppose len sc = 1;
then for n,m st 1<=n & n<m & m<=len sc holds sc.n<>sc.m by AXIOMS:22;
hence sc is Path of G by GRAPH_1:def 13;
suppose
A6: sc.1<>sc.2;
now let n, m; assume that
A7: 1<=n and
A8: n<m and
A9: m<=len sc;
thus sc.n<>sc.m proof assume
A10: not thesis;
consider vs such that
A11: vs is_vertex_seq_of sc &
for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs
by Def10;
A12: len vs = len sc +1 by A11,Def7;
A13: n<=len sc & 1<=m by A7,A8,A9,AXIOMS:22;
then A14: n<=len vs & m<=len vs by A9,A12,NAT_1:37;
A15: 1<=n+1 & n+1<=len vs & 1<=m+1 & m+1<=len vs
by A9,A12,A13,AXIOMS:24,NAT_1:37;
set vn = vs/.n; set vn1 = vs/.(n+1);
set vm = vs/.m; set vm1 = vs/.(m+1);
A16: vn=vs.n & vn1=vs.(n+1) & vm=vs.m & vm1=vs.(m+1)
by A7,A13,A14,A15,FINSEQ_4:24;
A17: sc.n joins vn, vn1 & sc.m joins vm, vm1 by A7,A9,A11,A13,Def7;
per cases by A10,A17,Th32;
suppose
A18: vn=vm & vn1=vm1; n+1<m+1 by A8,REAL_1:53;
then n=1 & m=len vs & n+1=1 & m+1=len vs by A7,A8,A11,A14,A15,A16,A18;
hence contradiction;
suppose
A19: vn=vm1 & vn1=vm;
thus contradiction proof A20: n+0<m+1 by A8,REAL_1:67;
A21: n+1<=m by A8,NAT_1:38;
per cases by A21,REAL_1:def 5;
suppose
A22: n+1=m; n=1 & m+1=len vs by A7,A11,A15,A16,A19,A20;
hence contradiction by A6,A10,A22;
suppose
n+1<m; then n=1 & m+1=len vs & n+1=1 & m=len vs
by A7,A11,A14,A15,A16,A19,A20
;
hence contradiction;
end;
end; end;
hence sc is Path of G by GRAPH_1:def 13;
end;
definition let G;
cluster empty -> oriented Chain of G;
correctness proof let p be Chain of G; assume A1: p is empty;
for n st 1<=n & n < len p holds
(the Source of G).(p.(n+1)) = (the Target of G).(p.n) proof
let n; assume 1<=n & n<=len p;
then 1<=len p by AXIOMS:22; then 1<=0 by A1,FINSEQ_1:25;
hence thesis;
end;
hence thesis by GRAPH_1:def 12;
end;
end;
definition let G; let oc be oriented Chain of G; assume
A1: oc <> {};
func vertex-seq oc -> FinSequence of the Vertices of G means
it is_vertex_seq_of oc & it.1 = (the Source of G).(oc.1);
existence proof
set SG = the Source of G; set TG = the Target of G;
deffunc F(Nat) = SG.(oc.$1);
consider z being FinSequence such that
A2: len z = len oc &
for j st j in Seg len oc holds z.j = F(j) from SeqLambda;
A3: Seg len oc = dom oc & Seg len z = dom z by FINSEQ_1:def 3;
len oc <> 0 by A1,FINSEQ_1:25; then 0<len oc & 0+1=1 by NAT_1:19;
then A4: 1<=len oc by NAT_1:38;
then A5: 1 in dom z by A2,FINSEQ_3:27;
set vs = z^<*TG.(oc.len oc)*>;
A6: len vs = len oc + len <*TG.(oc.len oc)*> by A2,FINSEQ_1:35
.= len oc +1 by FINSEQ_1:56;
rng vs c= the Vertices of G proof let y be set; assume
y in rng vs; then consider x being set such that
A7: x in dom vs & y = vs.x by FUNCT_1:def 5;
reconsider x as Nat by A7;
A8: 1<=x & x<=len vs by A7,FINSEQ_3:27;
per cases by A6,A8,NAT_1:26;
suppose
x<=len oc;
then A9: x in dom oc by A8,FINSEQ_3:27;
then A10: oc.x in rng oc & rng oc c= the Edges of G by FINSEQ_1:def 4,
FUNCT_1:def 5;
then reconsider e=oc.x as Element of the Edges of G;
A11: SG.e in rng the Source of G by A10,FUNCT_2:6;
A12: rng the Source of G c= the Vertices of G by RELSET_1:12;
vs.x = z.x by A2,A3,A9,FINSEQ_1:def 7 .= SG.e by A2,A3,A9;
hence y in the Vertices of G by A7,A11,A12;
suppose A13:
x=len oc +1; len oc in dom oc by A4,FINSEQ_3:27;
then A14: oc.len oc in rng oc & rng oc c= the Edges of G
by FINSEQ_1:def 4,FUNCT_1:def 5;
then reconsider e=oc.len oc as Element of the Edges of G;
A15: TG.e in rng the Target of G by A14,FUNCT_2:6;
rng the Target of G c= the Vertices of G by RELSET_1:12;
then y is Element of the Vertices of G by A2,A7,A13,A15,FINSEQ_1:59;
hence y in the Vertices of G;
end;
then reconsider vs as FinSequence of the Vertices of G by FINSEQ_1:def 4;
take vs;
now thus len vs = len oc + 1 by A6;
let n; assume that
A16: 1<=n and
A17: n<=len oc;
A18: n<=len vs & 1<=n+1 & n+1<=len vs by A6,A17,NAT_1:37,REAL_1:55;
then A19: n in dom vs & n+1 in dom vs by A16,FINSEQ_3:27;
A20: n in dom oc by A16,A17,FINSEQ_3:27;
reconsider vsn = vs.n as Element of the Vertices of G by A19,FINSEQ_2:13;
reconsider vsn1 = vs.(n+1) as Element of the Vertices of G by A19,FINSEQ_2:13;
A21: vsn = z.n by A2,A3,A20,FINSEQ_1:def 7 .= SG.(oc.n) by A2,A3,A20;
A22: vsn1 = TG.(oc.n) proof
per cases by A17,REAL_1:def 5;
suppose A23: n<len oc; then n+1<=len oc by NAT_1:38;
then A24: n+1 in dom oc by A18,FINSEQ_3:27;
hence vsn1 = z.(n+1) by A2,A3,FINSEQ_1:def 7 .= SG.(oc.(n+1)) by A2,A3,A24
.= TG.(oc.n) by A16,A23,GRAPH_1:def 12;
suppose n=len oc;
hence thesis by A2,FINSEQ_1:59;
end;
vsn = vs/.n & vsn1 = vs/.(n+1) by A16,A18,FINSEQ_4:24;
hence oc.n joins vs/.n, vs/.(n+1) by A21,A22,GRAPH_1:def 9;
end;
hence vs is_vertex_seq_of oc by Def7;
z.1 = SG.(oc.1) by A2,A3,A5;
hence vs.1 = SG.(oc.1) by A5,FINSEQ_1:def 7;
end;
uniqueness by A1,Th37;
end;