:: Subsequences of Standard Special Circular Sequences in $ { \cal E
:: } ^2_ { \rm T } $
:: by Yatsuka Nakamura , Roman Matuszewski and Adam Grabowski
::
:: Received May 12, 1997
:: Copyright (c) 1997-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, NAT_1, ARYTM_3, INT_1, CARD_1,
ARYTM_1, XXREAL_0, RELAT_1, XBOOLE_0, FINSEQ_1, FINSEQ_6, FUNCT_1,
PARTFUN1, RFINSEQ, EUCLID, TOPREAL1, JORDAN3, FINSEQ_5, RLTOPSP1,
GOBOARD5, ORDINAL4, TARSKI, PRE_TOPC, SUPINF_2, TOPREAL4, TOPREAL2,
MCART_1, JORDAN4;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, NAT_D, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_5,
STRUCT_0, TOPREAL1, TOPREAL2, TOPREAL4, GOBOARD5, PRE_TOPC, RLVECT_1,
RLTOPSP1, EUCLID, FINSEQ_6, RFINSEQ, XXREAL_0;
constructors REAL_1, NAT_D, RFINSEQ, BINARITH, FINSEQ_5, TOPREAL2, TOPREAL4,
GOBOARD5, RELSET_1;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, STRUCT_0, EUCLID,
SPPOL_2, GOBOARD5, NAT_1, CARD_1, ORDINAL1, FINSEQ_5;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities RLTOPSP1, RLVECT_1, FINSEQ_1;
theorems TARSKI, JORDAN3, TOPREAL4, TOPREAL1, TOPREAL2, FUNCT_1, SPPOL_1,
GOBOARD5, FINSEQ_1, GOBOARD7, NAT_1, SPPOL_2, FINSEQ_3, FINSEQ_2,
FINSEQ_4, FINSEQ_5, RFINSEQ, FINSEQ_6, ENUMSET1, ZFMISC_1, TOPREAL3,
XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, NAT_D, CARD_1,
XREAL_0, RLTOPSP1, RLVECT_4, RLVECT_1, PARTFUN1, RELAT_1;
begin :: Preliminaries
reserve i, i1, i2, j, k for Nat,
r, s for Real;
theorem Th1:
for i, j being Nat holds j<i & i<j+j implies i mod j<>0
proof
let i, j be Nat;
assume that
A1: j<i and
A2: i<j+j;
A3: i-j<j+j-j by A2,XREAL_1:9;
i-j=i-'j by A1,XREAL_1:233;
then
A4: (i-'j) mod j=i-'j by A3,NAT_D:24;
assume
A5: i mod j=0;
i=i-j+j;
then i mod j=(i-'j+j) mod j by A1,XREAL_1:233
.=((i-'j)+ (j mod j)) mod j by NAT_D:23
.=(i-'j+0)mod j by NAT_D:25
.=(i-'j)mod j;
hence contradiction by A1,A5,A4,NAT_D:36;
end;
theorem Th2:
for i,j being Nat holds j<=i & i<j+j implies i mod j=i-j & i mod j=i-'j
proof
let i,j be Nat;
assume that
A1: j<=i and
A2: i<j+j;
A3: i-j<j+j-j by A2,XREAL_1:9;
i=i-j+j;
then
A4: i mod j=(i-'j+j) mod j by A1,XREAL_1:233
.=((i-'j)+(j mod j))mod j by NAT_D:23
.=((i-'j)+0)mod j by NAT_D:25
.=(i-'j)mod j;
i-j=i-'j by A1,XREAL_1:233;
hence thesis by A4,A3,NAT_D:24;
end;
theorem Th3:
for i,j being Nat holds (j+j) mod j=0
proof
let i, j be Nat;
thus (j+j)mod j= (2*j) mod j .= 0 by NAT_D:13;
end;
theorem Th4:
for j,k being Nat holds 0<k & k<=j & k mod j=0 implies k=j
proof
let j,k be Nat;
assume that
A1: 0<k and
A2: k<=j and
A3: k mod j=0;
k >= j by A1,A3,NAT_D:24;
hence thesis by A2,XXREAL_0:1;
end;
begin :: Some facts about cutting of finite sequences
reserve D for non empty set,
f1 for FinSequence of D;
::$CT 2
theorem Th7:
for g being FinSequence of TOP-REAL 2,i st g is being_S-Seq &
i+1<len g holds g/^i is being_S-Seq
proof
let g be FinSequence of TOP-REAL 2,i;
assume that
A1: g is being_S-Seq and
A2: i+1<len g;
A3: mid(g,i+1,len g)=g/^(i+1-'1) by A2,FINSEQ_6:117
.=g/^i by NAT_D:34;
A4: 1<=i+1 by NAT_1:11;
then 1<len g by A2,XXREAL_0:2;
hence thesis by A1,A2,A4,A3,JORDAN3:6;
end;
::$CT 9
registration
cluster empty for FinSequence;
existence
proof
take <*>the set;
thus thesis;
end;
end;
registration let f be empty FinSequence;
let k be Nat;
cluster f|k -> empty;
coherence by RELAT_1:82;
end;
::$CT 2
theorem Th19:
for f being FinSequence of TOP-REAL 2,i1,i2,i st 1<=i1 & i1<i2 &
i2<=len f & 1<=i & i<i2-'i1+1 holds LSeg(mid(f,i1,i2),i)=LSeg(f,i+i1-'1)
proof
let f be FinSequence of TOP-REAL 2,i1,i2,i;
assume that
A1: 1<=i1 and
A2: i1<i2 and
A3: i2<=len f and
A4: 1<=i and
A5: i<i2-'i1+1;
A6: i+i1-'1+1=i+i1-1+1 by A1,NAT_D:37
.=i+1+i1-1
.=i+1+i1-'1 by A1,NAT_D:37;
i2-i1+1=i2-'i1+1 by A2,XREAL_1:233;
then i+i1<i2-i1+1+i1 by A5,XREAL_1:6;
then i+i1+1-1<=i2+1-1 by NAT_1:13;
then
A7: i+i1-1+1<=len f by A3,XXREAL_0:2;
then
A8: i+i1-'1+1<=len f by A1,NAT_D:37;
then
A9: i+i1-'1<len f by NAT_1:13;
1+1<=i+i1 by A1,A4,XREAL_1:7;
then 1+1-1<=i+i1-1 by XREAL_1:9;
then
A10: 1<=i+i1-'1 by A1,NAT_D:37;
then
A11: 1<i+i1-'1+1 by NAT_1:13;
A12: LSeg(f,i+i1-'1)=LSeg(f/.(i+i1-'1),f/.(i+i1-'1+1)) by A10,A8,TOPREAL1:def 3
;
A13: i+1<=i2-'i1+1 by A5,NAT_1:13;
A14: i+i1-'1+1<=len f by A1,A7,NAT_D:37;
A15: 1<=1+i by NAT_1:11;
A16: i<len mid(f,i1,i2) by A1,A2,A3,A5,FINSEQ_6:186;
then
A17: mid(f,i1,i2)/.i=mid(f,i1,i2).i by A4,FINSEQ_4:15
.=f.(i+i1-'1) by A1,A2,A3,A4,A5,FINSEQ_6:122
.=f/.(i+i1-'1) by A10,A9,FINSEQ_4:15;
A18: i+1<=len mid(f,i1,i2) by A16,NAT_1:13;
i+1<=len mid(f,i1,i2) by A16,NAT_1:13;
then mid(f,i1,i2)/.(i+1)=mid(f,i1,i2).(i+1) by FINSEQ_4:15,NAT_1:11
.=f.(i+1+i1-'1) by A1,A2,A3,A13,A15,FINSEQ_6:122
.=f/.(i+1+i1-'1) by A11,A14,A6,FINSEQ_4:15;
hence thesis by A4,A18,A12,A6,A17,TOPREAL1:def 3;
end;
theorem Th20:
for f being FinSequence of TOP-REAL 2,i1,i2,i st 1<=i1 & i1<i2 &
i2<=len f & 1<=i & i<i2-'i1+1 holds LSeg(mid(f,i2,i1),i)=LSeg(f,i2-'i)
proof
let f be FinSequence of TOP-REAL 2,i1,i2,i;
assume that
A1: 1<=i1 and
A2: i1<i2 and
A3: i2<=len f and
A4: 1<=i and
A5: i<i2-'i1+1;
A6: len mid(f,i2,i1)=i2-'i1+1 by A1,A2,A3,FINSEQ_6:187;
i<len mid(f,i2,i1) by A1,A2,A3,A5,FINSEQ_6:187;
then i+1<=len mid(f,i2,i1) by NAT_1:13;
then
A7: i+1-i<=len mid(f,i2,i1)-i by XREAL_1:9;
then
A8: 1<=len mid(f,i2,i1)-'i by NAT_D:39;
i2<=i2+(i1-'1) by NAT_1:11;
then i2<=i2+(i1-1) by A1,XREAL_1:233;
then i2-(i1-1)<=i2+(i1-1)-(i1-1) by XREAL_1:9;
then i2-i1+1<=i2;
then
A9: i2-'i1+1<=i2 by A2,XREAL_1:233;
A10: i2-'i1+1-'i+i1-'1 =i2-'i1+1-'i+i1-1 by A1,NAT_D:37
.=i2-'i1+1-i+i1-1 by A5,XREAL_1:233
.=i2-'i1-i+i1
.=i2-i1-i+i1 by A2,XREAL_1:233
.=i2-i
.=i2-'i by A5,A9,XREAL_1:233,XXREAL_0:2;
len mid(f,i2,i1)+1<=len mid(f,i2,i1)+i by A4,XREAL_1:6;
then len mid(f,i2,i1)<len mid(f,i2,i1)+i by NAT_1:13;
then len mid(f,i2,i1)-i<len mid(f,i2,i1)+i-i by XREAL_1:9;
then
A11: len mid(f,i2,i1)-'i<i2-'i1+1 by A6,A7,NAT_D:39;
i+(len mid(f,i2,i1)-'i) =len mid(f,i2,i1) by A5,A6,XREAL_1:235;
hence LSeg(mid(f,i2,i1),i) =LSeg(Rev mid(f,i2,i1),len mid(f,i2,i1)-'i) by
SPPOL_2:2
.=LSeg(mid(f,i1,i2),len mid(f,i2,i1)-'i) by FINSEQ_6:196
.=LSeg(f,len mid(f,i2,i1)-'i+i1-'1) by A1,A2,A3,A8,A11,Th19
.=LSeg(f,i2-'i) by A1,A2,A3,A10,FINSEQ_6:187;
end;
begin :: Dividing of special circular sequences into parts
definition
let n be Nat, f be FinSequence;
func S_Drop(n,f) -> Nat equals :Def1:
(n mod (len f -'1)) if n
mod (len f -'1)<>0 otherwise len f -'1;
correctness;
end;
theorem Th21:
for f being FinSequence holds S_Drop(len f-'1,f)=len f-'1
proof
let f be FinSequence;
(len f-'1) mod (len f-'1)=0 by NAT_D:25;
hence thesis by Def1;
end;
theorem Th22:
for n being Nat, f being FinSequence st
1<=n & n<=len f-'1 holds S_Drop(n,f)=n
proof
let n be Nat,f be FinSequence;
assume that
A1: 1<=n and
A2: n<=len f-'1;
per cases by A2,XXREAL_0:1;
suppose
n<len f-'1;
then n mod (len f-'1)=n by NAT_D:24;
hence thesis by A1,Def1;
end;
suppose
n=len f-'1;
hence thesis by Th21;
end;
end;
theorem Th23:
for n being Nat,f being FinSequence holds
S_Drop(n,f)=S_Drop(n+(len f-'1),f) &
S_Drop(n,f)=S_Drop(len f-'1+n,f)
proof
let n be Nat,f be FinSequence;
A1: (n+(len f-'1))mod (len f-'1) = (n+(len f-'1)*1)mod (len f-'1)
.=n mod (len f-'1) by NAT_D:21;
per cases;
suppose
A2: n mod (len f-'1)<>0;
then S_Drop(n,f)=n mod (len f-'1) by Def1;
hence thesis by A1,A2,Def1;
end;
suppose
A3: n mod (len f-'1)=0;
then S_Drop(n,f)=len f-'1 by Def1;
hence thesis by A1,A3,Def1;
end;
end;
definition
let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
pred g is_a_part>_of f,i1,i2 means
1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f &
g.len g=f.i2 & 1<=len g & len g<len f &
for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f);
end;
definition
let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
pred g is_a_part<_of f,i1,i2 means
1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f & g.len g=f.i2 &
1<=len g & len g<len f & for i being Nat st 1<=i & i<=len g holds
g.i=f.S_Drop(len f +i1-'i,f);
end;
definition
let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
pred g is_a_part_of f,i1,i2 means
g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2;
end;
theorem
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part_of f,i1,i2 holds
1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g &
len g<len f & ((for i being Nat st 1<=i & i<=len g holds
g.i=f.S_Drop((i1+i)-'1,f)) or
for i being Nat st 1<=i & i<=len g holds
g.i=f.S_Drop (len f +i1-'i,f) )
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume
A1: g is_a_part_of f,i1,i2;
now
per cases by A1;
case
g is_a_part>_of f,i1,i2;
hence thesis;
end;
case
g is_a_part<_of f,i1,i2;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th25:
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part>_of f,i1,i2 & i1<=i2 holds
len g=i2-'i1+1 & g=mid(f,i1,i2)
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part>_of f,i1,i2 and
A2: i1<=i2;
A3: 1<=len g by A1;
A4: 1<=i1 by A1;
A5: i1+1<=len f by A1;
then
A6: i1+1-1<=len f-1 by XREAL_1:9;
then
A7: 1<=len f-1 by A4,XXREAL_0:2;
then
A8: len f-1=len f-'1 by NAT_D:39;
A9: now
per cases;
case
A10: (i1+len g)-'1 mod (len f -'1)<>0;
A11: i1<=len f -'1 by A5,NAT_D:49;
then
A12: ((i1+len g)-'1 mod (len f -'1)) <len f-'1 by A4,NAT_D:1;
1<=len f -'1 by A4,A11,XXREAL_0:2;
then
A13: len f -'1<len f by NAT_D:51;
S_Drop((i1+len g)-'1,f)=((i1+len g)-'1 mod (len f -'1)) by A10,Def1;
hence S_Drop((i1+len g)-'1,f)< len f by A12,A13,XXREAL_0:2;
end;
case
A14: (i1+len g)-'1 mod (len f -'1)=0;
i1<=len f -'1 by A5,NAT_D:49;
then
A15: 1<=len f -'1 by A4,XXREAL_0:2;
S_Drop((i1+len g)-'1,f)=len f -'1 by A14,Def1;
hence S_Drop((i1+len g)-'1,f)< len f by A15,NAT_D:51;
end;
end;
A16: f.i2=f.S_Drop((i1+len g)-'1,f) by A1;
A17: i2+1<=len f by A1;
A18: now
per cases;
case
(i1+len g)-'1 mod (len f -'1)<>0;
then 0+1<=(i1+len g)-'1 mod (len f -'1) by NAT_1:13;
hence 1<=S_Drop((i1+len g)-'1,f) by Def1;
end;
case
A19: (i1+len g)-'1 mod (len f -'1)=0;
A20: i1<=len f -'1 by A5,NAT_D:49;
S_Drop((i1+len g)-'1,f)=len f -'1 by A19,Def1;
hence 1<=S_Drop((i1+len g)-'1,f) by A4,A20,XXREAL_0:2;
end;
end;
i1<=i1+1 by NAT_1:11;
then
A21: i1<=len f by A5,XXREAL_0:2;
A22: 0<>len f-'1 by A7,NAT_D:39;
A23: len g<len f by A1;
A24: 1<=i2 by A1;
i2<=i2+1 by NAT_1:11;
then
A25: i2<=len f by A17,XXREAL_0:2;
A26: i2<=len f -'1 by A17,NAT_D:49;
then 1<=len f -'1 by A24,XXREAL_0:2;
then len f -'1<len f by NAT_D:51;
then
A27: i2<len f by A26,XXREAL_0:2;
now
per cases by XXREAL_0:1;
case
A28: i2<S_Drop((i1+len g)-'1,f);
i2<=len f by A17,NAT_D:46;
then
A29: f/.i2=f.i2 by A24,FINSEQ_4:15;
A30: 1<=S_Drop((i1+len g)-'1,f) by A24,A28,XXREAL_0:2;
f/.i2<>f/.(S_Drop((i1+len g)-'1,f)) by A24,A9,A28,GOBOARD7:36;
hence contradiction by A16,A9,A29,A30,FINSEQ_4:15;
end;
case
A31: i2>S_Drop((i1+len g)-'1,f);
i2<=len f by A17,NAT_D:46;
then
A32: f/.i2=f.i2 by A24,FINSEQ_4:15;
f/.i2<>f/.(S_Drop((i1+len g)-'1,f)) by A18,A27,A31,GOBOARD7:36;
hence contradiction by A16,A18,A9,A32,FINSEQ_4:15;
end;
case
A33: i2=S_Drop((i1+len g)-'1,f);
now
per cases;
case
A34: (i1+len g)-'1 mod (len f -'1)<>0;
ex n being Nat st i1+len g -'1 =(len f-'1)*n+((i1+len g-'1) mod
(len f -'1)) & ((i1+len g-'1) mod (len f -'1))<len f -'1 by A22,NAT_D:def 2;
then consider n being Nat such that
A35: i1+len g -'1 =(len f-'1)*n+((i1+len g)-'1 mod (len f -'1));
A36: i1+len g -'1=(len f-'1)*n+i2 by A33,A34,A35,Def1;
now
per cases;
case
A37: n=0;
A38: dom g = Seg len g by FINSEQ_1:def 3;
A39: i1+len g-'1=i1+len g-1 by A4,NAT_1:12,XREAL_1:233;
A40: i2=i1+len g -'1 by A33,A34,A35,A37,Def1;
then
A41: i2+1-i1 = len g by A39;
A42: for j be Nat st j in dom g holds g.j = mid(f,i1,i2).j
proof
let j be Nat;
assume
A43: j in dom g;
then
A44: 1<=j by A38,FINSEQ_1:1;
then
A45: i1+j-'1=i1+j-1 by NAT_D:37;
i1+j>=1+1 by A4,A44,XREAL_1:7;
then
A46: i1+j-'1<>0 by A45;
A47: j<=len g by A38,A43,FINSEQ_1:1;
then j+i1<=i2-i1+1+i1 by A40,A39,XREAL_1:6;
then
A48: i1+j<=len f by A17,XXREAL_0:2;
A49: now
per cases;
case
A50: i1+j=len f;
then (i1+j-'1) mod (len f-'1)=0 by NAT_D:25;
hence S_Drop(i1+j-'1,f)=i1+j-'1 by A50,Def1;
end;
case
i1+j<>len f;
then i1+j<len f by A48,XXREAL_0:1;
then i1+j-1<len f-1 by XREAL_1:9;
then i1+j-'1<len f-'1 by A4,A8,NAT_D:37;
then (i1+j-'1)mod (len f-'1)=i1+j-'1 by NAT_D:24;
hence S_Drop((i1+j)-'1,f)=i1+j-'1 by A46,Def1;
end;
end;
g.j=f.S_Drop((i1+j)-'1,f) by A1,A44,A47;
hence thesis by A2,A4,A25,A41,A44,A47,A49,FINSEQ_6:122;
end;
A51: i2-i1+1=len g by A40,A39;
then len g=i2-'i1+1 by A2,XREAL_1:233;
then len mid(f,i1,i2) = len g by A2,A4,A24,A21,A25,FINSEQ_6:118;
hence thesis by A2,A51,A42,FINSEQ_2:9,XREAL_1:233;
end;
case
n<>0;
then 0+1<=n by NAT_1:13;
then
A52: (len f-'1)*n>=(len f-'1)*1 by XREAL_1:64;
len g+1<=len f by A23,NAT_1:13;
then len g+1-1<=len f-1 by XREAL_1:9;
then len g<=len f-'1 by XREAL_0:def 2;
then len g+i1<=len f-'1+i2 by A2,XREAL_1:7;
then i1+len g<len f-'1+i2+1 by NAT_1:13;
then
A53: i1+len g-1<len f-'1+i2+1-1 by XREAL_1:14;
i1<=i1+len g by NAT_1:11;
then i1+len g-1=i1+len g-'1 by A4,XREAL_1:233,XXREAL_0:2;
then i1+len g-'1-i2<len f-'1+i2-i2 by A53,XREAL_1:14;
hence contradiction by A36,A52;
end;
end;
hence thesis;
end;
case
A54: (i1+len g)-'1 mod (len f -'1)=0;
ex n being Nat st i1+len g -'1 =(len f-'1)*n+((i1+len g-'1) mod
(len f -'1)) & ((i1+len g-'1) mod (len f -'1))<len f -'1 by A22,NAT_D:def 2;
then consider n being Nat such that
A55: i1+len g -'1 =(len f-'1)*n+((i1+len g-'1) mod (len f -'1));
A56: now
assume n>1;
then n>=1+1 by NAT_1:13;
then
A57: i1+len g -'1>=(len f-'1)*(1+1) by A54,A55,NAT_1:4;
len g -1<len f-1 by A23,XREAL_1:9;
then i1+(len g -1)<len f-'1+(len f-'1) by A6,A8,XREAL_1:8;
then i1+len g -1<len f-'1+(len f-'1);
hence contradiction by A4,A57,NAT_1:12,XREAL_1:233;
end;
now
assume n=0;
then
A58: i1+len g<=1 by A54,A55,NAT_D:36;
i1+len g>=1+1 by A4,A3,XREAL_1:7;
hence contradiction by A58,XXREAL_0:2;
end;
then n>=0+1 by NAT_1:13;
then
A59: n=1 by A56,XXREAL_0:1;
i1+len g -'1=i2*n by A33,A54,A55,Def1;
then
A60: i1+len g-1=i2 by A24,A59,NAT_D:39;
A61: i2-i1=i2-'i1 by A2,XREAL_1:233;
then
A62: len g=i2-'i1+1 by A60;
A63: dom g = Seg len g by FINSEQ_1:def 3;
A64: for j be Nat st j in dom g holds g.j = mid(f,i1,i2).j
proof
let j be Nat;
assume
A65: j in dom g;
then
A66: 1<=j by A63,FINSEQ_1:1;
then
A67: i1+j-'1=i1+j-1 by NAT_D:37;
A68: j<=len g by A63,A65,FINSEQ_1:1;
then j+i1<=i2-i1+1+i1 by A60,XREAL_1:6;
then
A69: i1+j<=len f by A17,XXREAL_0:2;
i1+j>=1+1 by A4,A66,XREAL_1:7;
then
A70: i1+j-'1<>0 by A67;
A71: now
per cases;
case
A72: i1+j=len f;
then (i1+j-'1) mod (len f-'1)=0 by NAT_D:25;
hence S_Drop(i1+j-'1,f)=i1+j-'1 by A72,Def1;
end;
case
i1+j<>len f;
then i1+j<len f by A69,XXREAL_0:1;
then i1+j-1<len f-1 by XREAL_1:9;
then
A73: i1+j-'1<len f-'1 by A4,A8,NAT_D:37;
then (i1+j-'1) mod (len f-'1)<>0 by A70,NAT_D:24;
then S_Drop((i1+j)-'1,f)=(i1+j-'1) mod (len f-'1) by Def1;
hence S_Drop((i1+j)-'1,f)=i1+j-'1 by A73,NAT_D:24;
end;
end;
g.j=f.S_Drop((i1+j)-'1,f) by A1,A66,A68;
hence thesis by A2,A4,A25,A62,A66,A68,A71,FINSEQ_6:122;
end;
len mid(f,i1,i2) = len g by A2,A4,A24,A21,A25,A62,FINSEQ_6:118;
hence thesis by A60,A61,A64,FINSEQ_2:9;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th26:
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part>_of f,i1,i2 & i1>i2 holds
len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2) &
g=mid(f,i1,len f-'1)^mid(f,1,i2)
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part>_of f,i1,i2 and
A2: i1>i2;
A3: 1<=len g by A1;
A4: f.i2=f.S_Drop((i1+len g)-'1,f) by A1;
A5: i2<=i2+1 by NAT_1:11;
A6: i1<=i1+1 by NAT_1:12;
A7: 1<=i1 by A1;
A8: i1+1<=len f by A1;
then
A9: i1+1-1<=len f-1 by XREAL_1:9;
then
A10: 1<=len f-1 by A7,XXREAL_0:2;
then
A11: len f-1=len f-'1 by NAT_D:39;
A12: now
per cases;
case
A13: (i1+len g)-'1 mod (len f -'1)<>0;
A14: i1<=len f -'1 by A8,NAT_D:49;
then
A15: ((i1+len g)-'1 mod (len f -'1)) <len f-'1 by A7,NAT_D:1;
1<=len f -'1 by A7,A14,XXREAL_0:2;
then
A16: len f -'1<len f by NAT_D:51;
S_Drop((i1+len g)-'1,f)=((i1+len g)-'1 mod (len f -'1)) by A13,Def1;
hence S_Drop((i1+len g)-'1,f)< len f by A15,A16,XXREAL_0:2;
end;
case
A17: (i1+len g)-'1 mod (len f -'1)=0;
i1<=len f -'1 by A8,NAT_D:49;
then
A18: 1<=len f -'1 by A7,XXREAL_0:2;
S_Drop((i1+len g)-'1,f)=len f -'1 by A17,Def1;
hence S_Drop((i1+len g)-'1,f)< len f by A18,NAT_D:51;
end;
end;
i1<=len f -'1 by A8,NAT_D:49;
then 1<=len f -'1 by A7,XXREAL_0:2;
then
A19: len f -'1<len f by NAT_D:51;
A20: now
per cases;
case
(i1+len g)-'1 mod (len f -'1)<>0;
then 0+1<=(i1+len g)-'1 mod (len f -'1) by NAT_1:13;
hence 1<=S_Drop((i1+len g)-'1,f) by Def1;
end;
case
A21: (i1+len g)-'1 mod (len f -'1)=0;
A22: i1<=len f -'1 by A8,NAT_D:49;
S_Drop((i1+len g)-'1,f)=len f -'1 by A21,Def1;
hence 1<=S_Drop((i1+len g)-'1,f) by A7,A22,XXREAL_0:2;
end;
end;
A23: 1<=i2 by A1;
A24: i2+1<=len f by A1;
then
A25: i2<=len f -'1 by NAT_D:49;
then
A26: 1<=len f -'1 by A23,XXREAL_0:2;
then len f -'1<len f by NAT_D:51;
then
A27: i2<len f by A25,XXREAL_0:2;
A28: len g<len f by A1;
A29: 0<>len f-'1 by A10,NAT_D:39;
now
per cases by XXREAL_0:1;
case
A30: i2<S_Drop((i1+len g)-'1,f);
i2<=len f by A24,NAT_D:46;
then
A31: f/.i2=f.i2 by A23,FINSEQ_4:15;
A32: 1<=S_Drop((i1+len g)-'1,f) by A23,A30,XXREAL_0:2;
f/.i2<>f/.(S_Drop((i1+len g)-'1,f)) by A23,A12,A30,GOBOARD7:36;
hence contradiction by A4,A12,A31,A32,FINSEQ_4:15;
end;
case
A33: i2>S_Drop((i1+len g)-'1,f);
i2<=len f by A24,NAT_D:46;
then
A34: f/.i2=f.i2 by A23,FINSEQ_4:15;
f/.i2<>f/.(S_Drop((i1+len g)-'1,f)) by A20,A27,A33,GOBOARD7:36;
hence contradiction by A4,A20,A12,A34,FINSEQ_4:15;
end;
case
A35: i2=S_Drop((i1+len g)-'1,f);
now
per cases;
case
A36: (i1+len g)-'1 mod (len f -'1)<>0;
(ex n being Nat st i1+len g -'1 =(len f-'1)*n+((i1+len g-'1)
mod (len f -'1)) & ((i1+len g-'1) mod (len f -'1))<len f -'1)or ((i1+len g-'1)
mod (len f -'1))=0 & len f-'1=0 by NAT_D:def 2;
then consider n being Nat such that
A37: i1+len g -'1 =(len f-'1)*n+((i1+len g)-'1 mod (len f -'1))
by A10,NAT_D:39;
A38: i1+len g -'1=(len f-'1)*n+i2 by A35,A36,A37,Def1;
now
per cases;
case
n=0;
then i2=i1+len g -'1 by A35,A36,A37,Def1;
then i2+1=i1+len g -1+1 by A23,NAT_D:39
.=i1+len g;
hence contradiction by A2,A3,XREAL_1:8;
end;
case
n<>0;
then
A39: 0+1<=n by NAT_1:13;
now
per cases by A39,XXREAL_0:1;
case
A40: 1=n;
len f-'1=len f-1 by A26,NAT_D:39;
then
A41: i1+len g-1=len f-1+i2 by A7,A38,A40,NAT_D:37;
then
A42: len g=len f+i2-i1;
A43: len f-'1<=len f by NAT_D:50;
A44: dom g = Seg len g by FINSEQ_1:def 3;
A45: i1<=len f by A8,A6,XXREAL_0:2;
A46: 1<=len f-'1 by A10,NAT_D:39;
A47: i1<=len f-'1 by A9,A10,NAT_D:39;
then
A48: len (mid(f,i1,len f-'1))=len f-'1-'i1+ 1 by A7,A45,A46,A43,
FINSEQ_6:118;
A49: len f-'1-'i1+1 =len f-1-i1+1 by A9,A11,XREAL_1:233
.=len f-i1;
len (mid(f,i1,len f-'1)^(f|i2)) = len (mid(f,i1,len f-'
1))+ len(f|i2) by FINSEQ_1:22;
then len (mid(f,i1,len f-'1)^(f|i2))=len f-i1+i2 by A24,A5
,A48,A49,FINSEQ_1:59,XXREAL_0:2
.=len f+i2-i1
.=len f+i2-'i1 by A8,A6,NAT_D:37,XXREAL_0:2;
then
A50: len (mid(f,i1,len f-'1 )^(f|i2))=len g by A8,A6,A42,NAT_D:37
,XXREAL_0:2;
A51: len f-'1-'i1=len f-'1-i1 by A9,A11,XREAL_1:233;
for j be Nat st j in dom g holds g.j =(mid(f,i1,len f-'
1)^(f|i2)).j
proof
let j be Nat;
assume
A52: j in dom g;
then
A53: 1<=j by A44,FINSEQ_1:1;
then
A54: i1+j-'1=i1+j-1 by NAT_D:37;
i1+j>=1+1 by A7,A53,XREAL_1:7;
then
A55: i1+j-'1<>0 by A54;
A56: j<=len g by A44,A52,FINSEQ_1:1;
then
A57: g.j=f.S_Drop((i1+j)-'1,f) by A1,A53;
now
per cases;
case
A58: j<=len mid(f,i1,len f-'1);
then
A59: j+i1<=len f-'1-i1+1+i1 by A48,A51,XREAL_1:6;
A60: now
per cases;
case
A61: i1+j=len f;
then (i1+j-'1) mod (len f-'1)=0 by NAT_D:25;
hence S_Drop(i1+j-'1,f)=i1+j-'1 by A61,Def1;
end;
case
i1+j<>len f;
then i1+j<len f by A11,A59,XXREAL_0:1;
then i1+j-1<len f-1 by XREAL_1:9;
then
A62: i1+j-'1<len f-'1 by A7,A11,NAT_D:37;
then (i1+j-'1) mod (len f-'1)<>0 by A55,NAT_D:24;
then S_Drop((i1+j)-'1,f)=(i1+j-'1) mod (len f-'1)
by Def1;
hence S_Drop((i1+j)-'1,f)=i1+j-'1 by A62,NAT_D:24;
end;
end;
A63: len f-'1<=len f by NAT_D:50;
j in dom mid(f,i1,len f-'1) by A53,A58,FINSEQ_3:25;
then
A64: (mid(f,i1,len f-'1)^(f|i2) ).j =mid(f,i1,len f-'1
).j by FINSEQ_1:def 7;
A65: 1<=j by A44,A52,FINSEQ_1:1;
i1<=len f-'1 by A9,A10,NAT_D:39;
hence thesis by A7,A45,A46,A57,A58,A64,A63,A65,A60,
FINSEQ_6:118;
end;
case
A66: j>len mid(f,i1,len f-'1);
j<=len f+i2-i1 by A41,A44,A52,FINSEQ_1:1;
then j+i1<=len f+i2-i1+i1 by XREAL_1:6;
then
A67: j+i1-len f<=len f+i2-len f by XREAL_1:9;
j<len f by A28,A56,XXREAL_0:2;
then
A68: j<=len f-1 by SPPOL_1:1;
i1+1-1<=len f-1 by A8,XREAL_1:9;
then
A69: i1+j<=(len f-'1)+(len f-'1 ) by A11,A68,XREAL_1:7;
A70: (mid(f,i1,len f-'1)^(f|i2)).j =(f|i2).(j-len mid
(f,i1,len f-'1)) by A50,A56,A66,FINSEQ_6:108;
A71: i1+j-1=i1+j-'1 by A7,NAT_D:37;
len mid(f,i1,len f-'1)+1<=j by A66,NAT_1:13;
then len mid(f,i1,len f-'1)+1- len mid(f,i1,len f-'1)
<=j -len mid(f,i1,len f-'1) by XREAL_1:9;
then 1+len f<=i1+j-len f+len f by A48,A49,XREAL_1:6;
then 1+len f -1<=i1+j-1 by XREAL_1:9;
then
A72: len f-'1<i1+j-'1 by A19,A71,XXREAL_0:2;
j+i1>len f-i1+i1 by A48,A49,A66,XREAL_1:6;
then
A73: i1+j-len f>len f-len f by XREAL_1:9;
then
A74: i1+j-'len f=i1+j-len f by XREAL_0:def 2;
j -len mid(f,i1,len f-'1)=j-(len f-i1) by A7,A45,A46
,A43,A47,A49,FINSEQ_6:118
.=j+i1-len f;
then
A75: (f|i2).(j-len mid(f,i1,len f-'1)) =f.(i1+j-'len
f) by A74,A67,FINSEQ_3:112;
i1+j<i1+j+1 by NAT_1:13;
then i1+j-1<i1+j+1-1 by XREAL_1:9;
then
A76: i1+j-'1<(len f-'1)+(len f -'1) by A71,A69,XXREAL_0:2;
now
per cases;
case
(i1+j-'1) mod (len f -'1)=0;
hence contradiction by A72,A76,Th1;
end;
case
A77: (i1+j-'1) mod (len f -'1)<>0;
i1+j-'len f+(len f-'1)=i1+j-'len f+(len f-1)
by A10,NAT_D:39
.=i1+j-len f+(len f-1) by A73,XREAL_0:def 2
.=i1+j-1
.=i1+j-'1 by A53,NAT_D:37;
then
A78: (i1+j-'1) mod (len f-'1) =(i1+j-'len f+((len
f-'1)mod (len f-'1))) mod (len f-'1) by NAT_D:23
.=(i1+j-'len f+0) mod (len f-'1) by NAT_D:25
.=(i1+j-'len f) mod (len f-'1);
i1+j-(len f-'1)<=(len f-'1)+(len f-'1)-(len
f-'1) by A69,XREAL_1:9;
then i1+j-(len f-1)<=(len f-'1) by A10,NAT_D:39;
then i1+j-'len f+1<=(len f-'1) by A74;
then
A79: i1+j-'len f<(len f-'1) by NAT_1:13;
S_Drop (i1+j-'1,f)= (i1+j-'1) mod (len f -'1
) by A77,Def1;
hence thesis by A57,A70,A75,A78,A79,NAT_D:24;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence
len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2) by A8,A6,A42
,A50,FINSEQ_2:9,NAT_D:37,XXREAL_0:2;
end;
case
1<n;
then 1+1<=n by NAT_1:13;
then (len f-'1)*n>=(len f-'1)*(1+1) by XREAL_1:64;
then
A80: i1+len g-'1>=(len f-'1)*(1+1)+i2 by A38,XREAL_1:6;
A81: (len f-'1)*(1+1)<=(len f-'1)*(1+1)+i2 by NAT_1:11;
A82: i1+1-1<=len f-1 by A8,XREAL_1:9;
len g-1<len f-'1 by A28,A11,XREAL_1:9;
then
A83: i1+(len g-1)<len f-'1+(len f-'1) by A11,A82,XREAL_1:8;
i1+len g-1=i1+len g-'1 by A7,NAT_D:37;
hence contradiction by A80,A83,A81,XXREAL_0:2;
end;
end;
hence len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2);
end;
end;
hence len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2);
end;
case
A84: (i1+len g)-'1 mod (len f -'1)=0;
ex n being Nat st i1+len g -'1 =(len f-'1)*n+((i1+len g-'1)
mod (len f -'1)) & ((i1+len g-'1) mod (len f -'1))<len f -'1 by A29,NAT_D:def 2
;
then consider n being Nat such that
A85: i1+len g -'1 =(len f-'1)*n+((i1+len g-'1) mod (len f -'1));
A86: now
assume n>1;
then n>=1+1 by NAT_1:13;
then
A87: i1+len g -'1>=(len f-'1)*(1+1) by A84,A85,NAT_1:4;
len g -1<len f-1 by A28,XREAL_1:9;
then i1+(len g -1)<len f-'1+(len f-'1) by A9,A11,XREAL_1:8;
then i1+len g -1<len f-'1+(len f-'1);
hence contradiction by A7,A87,NAT_1:12,XREAL_1:233;
end;
now
assume n=0;
then
A88: i1+len g<=1 by A84,A85,NAT_D:36;
i1+len g>=1+1 by A7,A3,XREAL_1:7;
hence contradiction by A88,XXREAL_0:2;
end;
then n>=0+1 by NAT_1:13;
then n=1 by A86,XXREAL_0:1;
then i1+len g-'1=i2 by A35,A84,A85,Def1;
then
A89: i1+len g-1=i2 by A23,NAT_D:39;
i2-i2<i1-i2 by A2,XREAL_1:9;
then
A90: -0>-(i1-i2) by XREAL_1:24;
1-1<=len g-1 by A3,XREAL_1:9;
hence contradiction by A89,A90;
end;
end;
hence len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2);
end;
end;
hence thesis by A23,FINSEQ_6:116;
end;
theorem Th27:
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part<_of f,i1,i2 & i1>=i2 holds
len g=i1-'i2+1 & g=mid(f,i1,i2)
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part<_of f,i1,i2 and
A2: i1>=i2;
A3: 1<=len g by A1;
A4: f.i2=f.S_Drop((len f+i1-'len g),f) by A1;
A5: i1+1<=len f by A1;
i1<=i1+1 by NAT_1:11;
then
A6: i1<=len f by A5,XXREAL_0:2;
A7: 1<=i2 by A1;
A8: i2+1<=len f by A1;
then i2+1-1<=len f-1 by XREAL_1:9;
then
A9: 1<=len f-1 by A7,XXREAL_0:2;
then
A10: len f-1=len f-'1 by NAT_D:39;
A11: now
per cases;
case
A12: (len f+i1-'len g) mod (len f -'1)<>0;
A13: i2<=len f -'1 by A8,NAT_D:49;
then
A14: ((len f+i1-'len g) mod (len f -'1)) <len f-'1 by A7,NAT_D:1;
1<=len f -'1 by A7,A13,XXREAL_0:2;
then
A15: len f -'1<len f by NAT_D:51;
S_Drop((len f+i1-'len g),f) =((len f+i1-'len g) mod (len f -'1)) by A12
,Def1;
hence S_Drop((len f+i1-'len g),f)< len f by A14,A15,XXREAL_0:2;
end;
case
A16: (len f+i1-'len g) mod (len f -'1)=0;
i2<=len f -'1 by A8,NAT_D:49;
then
A17: 1<=len f -'1 by A7,XXREAL_0:2;
S_Drop((len f+i1-'len g),f)=len f -'1 by A16,Def1;
hence S_Drop((len f+i1-'len g),f)< len f by A17,NAT_D:51;
end;
end;
A18: i2<=len f -'1 by A8,NAT_D:49;
then 1<=len f -'1 by A7,XXREAL_0:2;
then len f -'1<len f by NAT_D:51;
then
A19: i2<len f by A18,XXREAL_0:2;
A20: 0<>len f-'1 by A9,NAT_D:39;
A21: now
per cases;
case
(len f+i1-'len g) mod (len f -'1)<>0;
then 0+1<=(len f+i1-'len g) mod (len f -'1) by NAT_1:13;
hence 1<=S_Drop((len f+i1-'len g),f) by Def1;
end;
case
A22: (len f+i1-'len g) mod (len f -'1)=0;
A23: i2<=len f -'1 by A8,NAT_D:49;
S_Drop((len f+i1-'len g),f)=len f -'1 by A22,Def1;
hence 1<=S_Drop((len f+i1-'len g),f) by A7,A23,XXREAL_0:2;
end;
end;
A24: len g<len f by A1;
A25: 0<len f-'1 by A9,NAT_D:39;
now
per cases by XXREAL_0:1;
case
A26: i2<S_Drop((len f+i1-'len g),f);
i2<=len f by A8,NAT_1:13;
then
A27: f/.i2=f.i2 by A7,FINSEQ_4:15;
A28: 1<=S_Drop((len f+i1-'len g),f) by A7,A26,XXREAL_0:2;
f/.i2<>f/.(S_Drop((len f+i1-'len g),f)) by A7,A11,A26,GOBOARD7:36;
hence contradiction by A4,A11,A27,A28,FINSEQ_4:15;
end;
case
A29: i2>S_Drop((len f+i1-'len g),f);
i2<=len f by A8,NAT_1:13;
then
A30: f/.i2=f.i2 by A7,FINSEQ_4:15;
f/.i2<>f/.(S_Drop((len f+i1-'len g),f)) by A21,A19,A29,GOBOARD7:36;
hence contradiction by A4,A21,A11,A30,FINSEQ_4:15;
end;
case
A31: i2=S_Drop((len f+i1-'len g),f);
now
per cases;
case
A32: (len f+i1-'len g) mod (len f -'1)<>0;
ex n being Nat st len f+i1-'len g =(len f-'1)*n+((len f+i1-'len
g) mod (len f -'1)) & ((len f+i1-'len g) mod (len f -'1))<len f -'1 by A20,
NAT_D:def 2;
then consider n being Nat such that
A33: len f+i1-'len g =(len f-'1)*n+((len f+i1-'len g) mod (len f -'1));
A34: n=0 or n>=0+1 by NAT_1:13;
A35: len f+i1-'len g=(len f-'1)*n+i2 by A31,A32,A33,Def1;
now
per cases by A34,XXREAL_0:1;
case
n=0;
then i2=len f+i1-'len g by A31,A32,A33,Def1;
then i2=len f+i1-len g by A24,NAT_D:37;
then i2+len g=i1+len f;
hence contradiction by A2,A24,XREAL_1:8;
end;
case
A36: n=1;
A37: len f+i1-'len g=len f+i1-len g by A24,NAT_D:37;
A38: len f-1+i2=len f+i1-'len g by A10,A31,A32,A33,A36,Def1;
then
A39: len g=i1-i2+1 by A37;
then
A40: len g=i1-'i2+1 by A2,XREAL_1:233;
A41: dom g = Seg len g by FINSEQ_1:def 3;
A42: for j be Nat st j in dom g holds g.j =mid(f,i1,i2).j
proof
let j be Nat;
assume
A43: j in dom g;
then
A44: 1<=j by A41,FINSEQ_1:1;
A45: j<=len g by A41,A43,FINSEQ_1:1;
1-1<=i2-1 by A7,XREAL_1:9;
then
A46: i1-0>=i1-(i2-1) by XREAL_1:10;
then
A47: i1-'j+1=i1-j+1 by A38,A37,A45,XREAL_1:233,XXREAL_0:2;
A48: j<=i1 by A38,A37,A45,A46,XXREAL_0:2;
A49: now
per cases;
case
len f+i1-'j=len f-'1;
then len f+i1-j=len f-'1 by A24,A45,NAT_D:37,XXREAL_0:2
.=len f-1 by A9,NAT_D:39;
then i1-j=-1;
hence contradiction by A48,XREAL_1:48;
end;
case
len f+i1-'j<>len f-'1;
i1+1+0<len f+j by A5,A44,XREAL_1:8;
then i1+1-j<len f+j-j by XREAL_1:9;
then i1+1-j-1<len f-1 by XREAL_1:9;
then i1-j<len f-1;
then i1-'j<len f-'1 by A10,A38,A37,A45,A46,XREAL_1:233
,XXREAL_0:2;
then
A50: i1-'j+1<=len f-'1 by NAT_1:13;
A51: len f+i1-'j=len f+i1-j by A24,A45,NAT_D:37,XXREAL_0:2;
now
per cases by A50,XXREAL_0:1;
case
A52: i1-'j+1=len f-'1;
len f+i1-'j=len f-1+1+i1-j by A24,A45,NAT_D:37
,XXREAL_0:2
.=len f-'1+(i1-j+1) by A10
.=len f-'1+(len f-'1) by A38,A37,A45,A46,A52,
XREAL_1:233,XXREAL_0:2;
then (len f+i1-'j)mod (len f-'1)=0 by Th3;
hence S_Drop(len f+i1-'j,f)=i1-'j+1 by A52,Def1;
end;
case
A53: i1-'j+1<len f-'1;
A54: len f=len f-1+1 .=len f-'1+1 by A9,NAT_D:39;
len f-'1+1+i1-'j=len f-'1+1+i1-j by A38,A37,A45,A46,
NAT_D:37,XXREAL_0:2
.=len f-'1+(1+(i1-j))
.=len f-'1+(1+(i1-'j)) by A38,A37,A45,A46,XREAL_1:233
,XXREAL_0:2;
then
(len f+i1-'j)mod (len f-'1) =(((len f-'1)mod (len
f-'1))+(1+(i1-'j)))mod (len f-'1) by A54,NAT_D:22
.=(0+(1+(i1-'j)))mod (len f-'1) by NAT_D:25
.=(i1-'j+1) by A53,NAT_D:24;
then
A55: S_Drop(len f+i1-'j,f)= (len f+i1-'j)mod (len f-'1
) by Def1;
len f-1+1+i1-j=(len f-1)+(i1-j+1);
then
A56: len f+i1-'j=i1-'j+1+( len f-'1) by A9,A47,A51,NAT_D:39;
(len f-'1)mod(len f-'1)=0 by NAT_D:25;
then S_Drop(len f+i1-'j,f)=(i1-'j+1+0)mod (len f-'1)
by A55,A56,NAT_D:22
.=(i1-'j+1)mod (len f-'1);
hence S_Drop(len f+i1-'j,f)=i1-'j+1 by A53,NAT_D:24;
end;
end;
hence S_Drop(len f+i1-'j,f)=i1-'j+1;
end;
end;
g.j=f.S_Drop(len f+i1-'j,f) by A1,A44,A45;
hence thesis by A2,A7,A6,A40,A44,A45,A49,FINSEQ_6:190;
end;
len mid(f,i1,i2) = len g by A2,A7,A6,A40,FINSEQ_6:187;
hence thesis by A2,A39,A42,FINSEQ_2:9,XREAL_1:233;
end;
case
n>1;
then 1+1<=n by NAT_1:13;
then
A57: len f+i1-'len g-i2>=(len f-'1)*(1+1) by A35,XREAL_1:64;
A58: len f-i2<=len f-1 by A7,XREAL_1:10;
i1+1+0<i1+1+len g by A3,XREAL_1:8;
then i1+1-len g<i1+1+len g-len g by XREAL_1:14;
then i1-len g+1-i2<i1+1-i2 by XREAL_1:14;
then
A59: len f-1+(i1-len g-i2+1)<len f-1+(i1+1-i2) by XREAL_1:8;
i1+1-i2<=len f-i2 by A5,XREAL_1:9;
then i1+1-i2<=len f-1 by A58,XXREAL_0:2;
then len f-1+(i1+1-i2)<=len f-1+(len f-1) by XREAL_1:7;
then len f+i1-len g-i2<len f-1+(len f-1) by A59,XXREAL_0:2;
hence contradiction by A24,A10,A57,NAT_D:37;
end;
end;
hence thesis;
end;
case
A60: (len f+i1-'len g) mod (len f -'1)=0;
(ex n being Nat st len f+i1-'len g =(len f-'1)*n+((len f+i1-'
len g) mod (len f -'1)) & ((len f+i1-'len g) mod (len f -'1))<len f -'1)or ((
len f+i1-'len g) mod (len f -'1))=0 & len f-'1=0 by NAT_D:def 2;
then consider n being Nat such that
A61: len f+i1-'len g =(len f-'1)*n+((len f+i1-'len g) mod (len
f -'1)) by A9,NAT_D:39;
A62: len f+i1-'len g=i2*n by A31,A60,A61,Def1;
now
assume n=0;
then
A63: len g>=len f+i1 by A60,A61,NAT_D:36;
len f<=len f +i1 by NAT_1:11;
hence contradiction by A24,A63,XXREAL_0:2;
end;
then
A64: n>=0+1 by NAT_1:13;
A65: now
per cases by A64,XXREAL_0:1;
case
A66: n>1;
A67: len f-'1+(len f-'1)=(len f-'1)*(1+1);
i1+1+1<=len f+len g by A5,A3,XREAL_1:7;
then 1+(i1+1)-len g<=len f+len g-len g by XREAL_1:9;
then 1+((i1+1)-len g)-1<=len f-1 by XREAL_1:9;
then len f-1+((i1+1)-len g)<=len f-1+(len f-1) by XREAL_1:6;
then len f+i1-len g<=len f-1+(len f-1);
then
A68: len f+i1-'len g<=len f-'1+(len f-'1) by A24,A10,NAT_D:37;
A69: n>=1+1 by A66,NAT_1:13;
now
per cases by A69,XXREAL_0:1;
case
n>1+1;
hence contradiction by A25,A60,A61,A68,A67,XREAL_1:68;
end;
case
A70: n=1+1;
then
A71: len f-1+(1+i1)-len g=len f-'1+(len f-' 1) by A24,A60,A61,
NAT_D:37;
then 1+(len f-'1)<=(1+i1)-(len f-'1)+(len f-'1) by A3,A10,
XREAL_1:6;
then 1+(len f-1)<=(1+i1) by A9,NAT_D:39;
then
A72: len f=i1+1 by A5,XXREAL_0:1;
then i2=i1 by A60,A61,A62,A70,NAT_D:34;
then i1-'i2=0 by XREAL_1:232;
hence len g=i1-'i2+1 by A10,A71,A72;
end;
end;
hence len g=i1-'i2+1;
end;
case
A73: n=1;
len f+i1-'len g=len f+i1-len g by A24,NAT_D:37;
then len f+i1=i2+len g by A62,A73;
hence contradiction by A2,A24,XREAL_1:8;
end;
end;
A74: dom g = Seg len g by FINSEQ_1:def 3;
A75: for j be Nat st j in dom g holds g.j =mid(f,i1,i2).j
proof
let j be Nat;
assume
A76: j in dom g;
then
A77: 1<=j by A74,FINSEQ_1:1;
A78: j<=len g by A74,A76,FINSEQ_1:1;
1-1<=i2-1 by A7,XREAL_1:9;
then
A79: i1-0>=i1-(i2-1) by XREAL_1:10;
A80: i1-'i2+1=i1-i2+1 by A2,XREAL_1:233
.=i1-(i2-1);
then
A81: i1-'j+1=i1-j+1 by A65,A78,A79,XREAL_1:233,XXREAL_0:2;
A82: j<=i1 by A65,A78,A80,A79,XXREAL_0:2;
A83: now
per cases;
case
len f+i1-'j=len f-'1;
then len f+i1-j=len f-'1 by A65,A78,A80,A79,NAT_D:37,XXREAL_0:2
.=len f-1 by A9,NAT_D:39;
then i1-j=-1;
hence contradiction by A82,XREAL_1:48;
end;
case
len f+i1-'j<>len f-'1;
i1+1+0<len f+j by A5,A77,XREAL_1:8;
then i1+1-j<len f+j-j by XREAL_1:9;
then i1+1-j-1<len f-1 by XREAL_1:9;
then i1-j<len f-1;
then i1-'j<len f-'1 by A10,A65,A78,A80,A79,XREAL_1:233
,XXREAL_0:2;
then
A84: i1-'j+1<=len f-'1 by NAT_1:13;
A85: len f+i1-'j=len f+i1-j by A65,A78,A80,A79,NAT_D:37,XXREAL_0:2;
now
per cases by A84,XXREAL_0:1;
case
A86: i1-'j+1=len f-'1;
len f+i1-'j=len f-1+1+i1-j by A65,A78,A80,A79,NAT_D:37
,XXREAL_0:2
.=len f-'1+(i1-j+1) by A10
.=len f-'1+(len f-'1) by A65,A78,A80,A79,A86,XREAL_1:233
,XXREAL_0:2;
then (len f+i1-'j)mod (len f-'1)=0 by Th3;
hence S_Drop(len f+i1-'j,f)=i1-'j+1 by A86,Def1;
end;
case
A87: i1-'j+1<len f-'1;
A88: len f=len f-1+1 .=len f-'1+1 by A9,NAT_D:39;
len f-'1+1+i1-'j=len f-'1+1+i1-j by A65,A78,A80,A79,
NAT_D:37,XXREAL_0:2
.=len f-'1+(1+(i1-j))
.=len f-'1+(1+(i1-'j)) by A65,A78,A80,A79,XREAL_1:233
,XXREAL_0:2;
then (len f+i1-'j)mod (len f-'1) =(((len f-'1)mod (len f
-'1))+(1+(i1-'j)))mod (len f-'1) by A88,NAT_D:22
.=(0+(1+(i1-'j)))mod (len f-'1) by NAT_D:25
.=(i1-'j+1) by A87,NAT_D:24;
then
A89: S_Drop(len f+i1-'j,f)=(len f+ i1-'j)mod (len f-'1) by Def1;
len f-1+1+i1-j=(len f-1)+(i1-j+1);
then
A90: len f+i1-'j=i1-'j+1+(len f-'1) by A9,A81,A85,NAT_D:39;
(len f-'1)mod(len f-'1)=0 by NAT_D:25;
then S_Drop(len f+i1-'j,f)=(i1-'j+1+0)mod (len f-'1) by A89
,A90,NAT_D:22
.=(i1-'j+1)mod (len f-'1);
hence S_Drop(len f+i1-'j,f)=i1-'j+1 by A87,NAT_D:24;
end;
end;
hence S_Drop(len f+i1-'j,f)=i1-'j+1;
end;
end;
g.j=f.S_Drop(len f+i1-'j,f) by A1,A77,A78;
hence thesis by A2,A7,A6,A65,A77,A78,A83,FINSEQ_6:190;
end;
len mid(f,i1,i2) = len g by A2,A7,A6,A65,FINSEQ_6:187;
hence thesis by A65,A75,FINSEQ_2:9;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th28:
for f being non constant standard special_circular_sequence, g
being FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part<_of f
,i1,i2 & i1<i2 holds len g=len f+i1-'i2 & g=mid(f,i1,1)^mid(f,len f-'1,i2)
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part<_of f,i1,i2 and
A2: i1<i2;
A3: 1<=len g by A1;
A4: 1<=i1 by A1;
A5: f.i2=f.S_Drop(len f+i1-'len g,f) by A1;
A6: i2<=i2+1 by NAT_1:11;
A7: i2+1<=len f by A1;
then
A8: i2+1-1<=len f-1 by XREAL_1:9;
A9: i1+1<=len f by A1;
then i1+1-1<=len f-1 by XREAL_1:9;
then
A10: 1<=len f-1 by A4,XXREAL_0:2;
then
A11: len f-1=len f-'1 by NAT_D:39;
A12: now
per cases;
case
A13: len f+i1-'len g mod (len f -'1)<>0;
A14: i1<=len f -'1 by A9,NAT_D:49;
then
A15: (len f+i1-'len g mod (len f -'1)) <len f-'1 by A4,NAT_D:1;
1<=len f -'1 by A4,A14,XXREAL_0:2;
then
A16: len f -'1<len f by NAT_D:51;
S_Drop(len f+i1-'len g,f) =(len f+i1-'len g mod (len f -'1)) by A13,Def1;
hence S_Drop(len f+i1-'len g,f)< len f by A15,A16,XXREAL_0:2;
end;
case
A17: len f+i1-'len g mod (len f -'1)=0;
i1<=len f -'1 by A9,NAT_D:49;
then
A18: 1<=len f -'1 by A4,XXREAL_0:2;
S_Drop(len f+i1-'len g,f)=len f -'1 by A17,Def1;
hence S_Drop(len f+i1-'len g,f)< len f by A18,NAT_D:51;
end;
end;
A19: 1<=i2 by A1;
A20: now
per cases;
case
len f+i1-'len g mod (len f -'1)<>0;
then 0+1<=len f+i1-'len g mod (len f -'1) by NAT_1:13;
hence 1<=S_Drop(len f+i1-'len g,f) by Def1;
end;
case
A21: len f+i1-'len g mod (len f -'1)=0;
A22: i1<=len f -'1 by A9,NAT_D:49;
S_Drop(len f+i1-'len g,f)=len f -'1 by A21,Def1;
hence 1<=S_Drop(len f+i1-'len g,f) by A4,A22,XXREAL_0:2;
end;
end;
i1<=i1+1 by NAT_1:11;
then
A23: i1<=len f by A9,XXREAL_0:2;
i1<=i1+1 by NAT_1:12;
then
A24: i1<=len f by A9,XXREAL_0:2;
A25: 0<>len f-'1 by A10,NAT_D:39;
i1<=len f -'1 by A9,NAT_D:49;
then 1<=len f -'1 by A4,XXREAL_0:2;
then
A26: len f -'1<len f by NAT_D:51;
A27: len g<len f by A1;
A28: i2<=len f -'1 by A7,NAT_D:49;
then 1<=len f -'1 by A19,XXREAL_0:2;
then len f -'1<len f by NAT_D:51;
then
A29: i2<len f by A28,XXREAL_0:2;
now
per cases by XXREAL_0:1;
case
A30: i2<S_Drop(len f+i1-'len g,f);
i2<=len f by A7,NAT_1:13;
then
A31: f/.i2=f.i2 by A19,FINSEQ_4:15;
A32: 1<=S_Drop(len f+i1-'len g,f) by A19,A30,XXREAL_0:2;
f/.i2<>f/.(S_Drop(len f+i1-'len g,f)) by A19,A12,A30,GOBOARD7:36;
hence contradiction by A5,A12,A31,A32,FINSEQ_4:15;
end;
case
A33: i2>S_Drop(len f+i1-'len g,f);
i2<=len f by A7,NAT_1:13;
then
A34: f/.i2=f.i2 by A19,FINSEQ_4:15;
f/.i2<>f/.(S_Drop(len f+i1-'len g,f)) by A20,A29,A33,GOBOARD7:36;
hence contradiction by A5,A20,A12,A34,FINSEQ_4:15;
end;
case
A35: i2=S_Drop(len f+i1-'len g,f);
now
per cases;
case
A36: len f+i1-'len g mod (len f -'1)<>0;
ex n being Nat st len f+i1-'len g =(len f-'1)*n+((len f+i1-'len
g) mod (len f -'1)) & ((len f+i1-'len g) mod (len f -'1))<len f -'1 by A25,
NAT_D:def 2;
then consider n being Nat such that
A37: len f+i1-'len g =(len f-'1)*n+(len f+i1-'len g mod (len f -'1));
A38: len f+i1-'len g=(len f-'1)*n+i2 by A35,A36,A37,Def1;
now
per cases;
case
n=0;
then
A39: i2=len f+i1-'len g by A35,A36,A37,Def1
.=len f+i1-len g by A27,NAT_D:37
.=len f-len g+i1;
then
A40: len g=len f+i1-i2;
A41: len (mid(f,i1,1))=i1-'1+1 by A4,A24,FINSEQ_6:187
.=i1 by A4,XREAL_1:235;
len (mid(f,len f-'1,i2))=len f-'1-'i2+1 by A19,A11,A8,A26,
FINSEQ_6:187;
then
A42: len (mid(f,len f-'1,i2))=len f-'1-i2+1 by A11,A8,XREAL_1:233;
A43: dom g = Seg len g by FINSEQ_1:def 3;
len (mid(f,i1,1)^mid(f,len f-'1,i2)) = len (mid(f,i1,1))+
len(mid(f,len f-'1,i2)) by FINSEQ_1:22;
then
len (mid(f,i1,1)^mid(f,len f-'1,i2))=i1+len f-i2 by A11,A41,A42
.=len f+i1-'i2 by A7,A6,NAT_D:37,XXREAL_0:2;
then
A44: len (mid(f,i1,1)^mid(f,len f-'1,i2))=len g by A7,A6,A40,NAT_D:37
,XXREAL_0:2;
for j be Nat st j in dom g holds g.j = (mid(f,i1,1)^mid(f,
len f-'1,i2)).j
proof
let j be Nat;
assume
A45: j in dom g;
then
A46: 1<=j by A43,FINSEQ_1:1;
A47: j<=len g by A43,A45,FINSEQ_1:1;
then
A48: g.j=f.S_Drop(len f+i1-'j,f) by A1,A46;
A49: len f+i1-'j=len f+i1-j by A27,A47,NAT_D:37,XXREAL_0:2;
now
per cases;
case
A50: j<=len mid(f,i1,1);
len f-'1<=len f by NAT_D:50;
then len f-1+j<=len f+i1 by A11,A41,A50,XREAL_1:7;
then
A51: len f-1+j-j<=len f+i1-j by XREAL_1:9;
j in dom mid(f,i1,1) by A46,A50,FINSEQ_3:25;
then
A52: (mid(f,i1,1)^mid(f,len f-'1,i2)).j =mid(f,i1,1).j by
FINSEQ_1:def 7;
A53: len mid(f,i1,1)=i1-'1+1 by A4,A23,FINSEQ_6:187;
now
per cases;
case
len f+i1-'j=len f-'1;
then len f+i1-j=len f-1 by A11,A41,A50,NAT_D:37;
then i1+1=j;
hence thesis by A41,A50,NAT_1:13;
end;
case
A54: len f+i1-'j<>len f-'1;
A55: j-1>=0 by A46,XREAL_1:48;
then j-1=j-'1 by XREAL_0:def 2;
then
A56: len f<=len f+(j-1) by NAT_1:11;
A57: len f+i1-'j>len f-'1 by A11,A49,A51,A54,XXREAL_0:1;
now
per cases;
case
A58: i1+1=len f & j-1=0;
then len f+i1-'j=len f-1+len f-1 by A4,NAT_D:37
.=len f-'1+(len f-'1) by A11;
then (len f+i1-'j)mod (len f-'1)=0 by Th3;
then S_Drop(len f+i1-'j,f) =j+i1-'1 by A58,Def1;
then
A59: S_Drop(len f+i1-'j,f) =1+i1-1 by A58,NAT_D:37
.=i1-j+1 by A58;
A60: 1<=i1-'j+1 by NAT_1:11;
i1<=i1+(j-'1) by NAT_1:11;
then
A61: i1-(j-'1)<=i1 by XREAL_1:20;
A62: i1-j+1=i1-'j+1 by A41,A50,XREAL_1:233;
A63: j-1=j-'1 by A46,XREAL_1:233;
mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1) by A4,A23
,A46,A50,A53,FINSEQ_6:191
.=f.(i1-'j+1) by A23,A62,A60,A63,A61,FINSEQ_6:123
;
hence thesis by A41,A48,A50,A52,A59,XREAL_1:233;
end;
case
A64: i1+1<>len f or j-1<>0;
now
per cases by A64;
case
i1+1<>len f;
then i1+1<len f by A9,XXREAL_0:1;
hence i1+1<len f+(j-1) by A56,XXREAL_0:2;
end;
case
j-1<>0;
then len f<len f+(j-1) by A55,XREAL_1:29;
hence i1+1<len f+(j-1) by A9,XXREAL_0:2;
end;
end;
then i1+1-j<len f-1+j-j by XREAL_1:9;
then
A65: len f-1+(i1+1-j)< len f-1+(len f-1) by XREAL_1:8;
then (len f+i1-'j) mod (len f-'1)<>0 by A11,A49,A57
,Th1;
then
A66: S_Drop(len f+i1-'j,f) =(len f+i1-'j) mod (
len f-'1) by Def1
.=len f+i1-j-(len f-1) by A11,A49,A51,A65,Th2
.=(i1-j)+1;
A67: 1<=i1-'j+1 by NAT_1:11;
i1<=i1+(j-'1) by NAT_1:11;
then
A68: i1-(j-'1)<=i1 by XREAL_1:20;
A69: i1-j+1=i1-'j+1 by A41,A50,XREAL_1:233;
A70: j-1=j-'1 by A46,XREAL_1:233;
mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1) by A4,A23
,A46,A50,A53,FINSEQ_6:191
.=f.(i1-'j+1) by A23,A69,A67,A70,A68,FINSEQ_6:123
;
hence thesis by A41,A48,A50,A52,A66,XREAL_1:233;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
A71: j>len mid(f,i1,1);
i2+1-1<=len f-1 by A7,XREAL_1:9;
then
A72: i2-i2<=len f-1-i2 by XREAL_1:9;
A73: len f-i2=len f-1-i2+1
.=len f-'1-'i2+1 by A11,A72,XREAL_0:def 2;
A74: len f+0<len f+i1 by A4,XREAL_1:8;
A75: (mid(f,i1,1)^(mid(f,len f-'1,i2))).j =(mid(f,len f-'
1,i2)).(j-len mid(f,i1,1)) by A44,A47,A71,FINSEQ_6:108;
A76: j-i1<=len f+i1-i2-i1 by A39,A47,XREAL_1:9;
i1+1<=j by A41,A71,NAT_1:13;
then
A77: i1+1-i1<=j-i1 by XREAL_1:9;
then
A78: j-i1 =j-'len mid(f,i1,1) by A41,XREAL_0:def 2;
i2-i1>=0 by A2,XREAL_1:48;
then len f+0<=len f+(i2-i1) by XREAL_1:7;
then
A79: len f-(i2-i1)<=len f+(i2-i1)-(i2- i1) by XREAL_1:9;
A80: j<=len f+i1-i2 by A39,A43,A45,FINSEQ_1:1;
then j<=len f by A79,XXREAL_0:2;
then j<len f+i1 by A74,XXREAL_0:2;
then j-j<len f+i1-j by XREAL_1:9;
then
A81: 0<len f+i1-'j by A80,A79,NAT_D:37,XXREAL_0:2;
len f-i2<=len f-1 by A19,XREAL_1:13;
then j-i1<=len f-'1 by A11,A76,XXREAL_0:2;
then j-'i1<=len f-'1 by A41,A71,XREAL_1:233;
then len f-'1-'(j-'i1)+1=len f-'1-(j-'i1)+1 by XREAL_1:233
.=len f-1-(j-i1)+1 by A11,A41,A71,XREAL_1:233
.=len f+i1-j
.=len f+i1-'j by A80,A79,NAT_D:37,XXREAL_0:2;
then
A82: (mid(f,i1,1)^(mid(f,len f-'1,i2))) .j =f.(len f+i1-'
j) by A19,A11,A8,A26,A41,A75,A77,A76,A73,A78,FINSEQ_6:190;
A83: i1+1<=j by A41,A71,NAT_1:13;
A84: len f+i1-j=len f+i1-'j by A27,A47,NAT_D:37,XXREAL_0:2;
i1+1<=j by A41,A71,NAT_1:13;
then len f+(i1+1)<=len f+j by XREAL_1:6;
then len f+i1+1-1<=len f+j-1 by XREAL_1:9;
then len f+i1-j<=len f+j-1-j by XREAL_1:9;
then
A85: len f-'1>=len f+i1-'j by A11,A80,A79,NAT_D:37,XXREAL_0:2;
now
per cases;
case
A86: (len f+i1-'j) mod (len f -'1)=0;
then len f+i1-'j=len f-'1 by A81,A85,Th4;
hence thesis by A48,A82,A86,Def1;
end;
case
A87: (len f+i1-'j) mod (len f -'1)<>0;
len f+(i1+1)<=len f+j by A83,XREAL_1:7;
then len f+i1+1-j<=len f+j-j by XREAL_1:9;
then
A88: len f+i1+1-j-1<=len f-1 by XREAL_1:9;
A89: S_Drop(len f+i1-'j,f) = (len f+i1-'j) mod (len f
-'1) by A87,Def1;
len f+i1-j=len f-'1 implies contradiction by A84,A87,
NAT_D:25;
then len f+i1-'j<(len f-'1) by A11,A84,A88,XXREAL_0:1;
hence thesis by A48,A82,A89,NAT_D:24;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by A7,A6,A40,A44,FINSEQ_2:9,NAT_D:37,XXREAL_0:2;
end;
case
n<>0;
then
A90: 0+1<=n by NAT_1:13;
now
per cases by A90,XXREAL_0:1;
case
A91: 1=n;
A92: len f+i1-'len g=len f+i1-len g by A27,NAT_D:37;
i1+1+0<i2+len g by A2,A3,XREAL_1:8;
hence contradiction by A11,A38,A91,A92;
end;
case
1<n;
then 1+1<=n by NAT_1:13;
then (len f-'1)*n>=(len f-'1)*(1+1) by XREAL_1:64;
then
A93: len f+i1-'len g>=(len f-'1)*(1+1)+i2 by A38,XREAL_1:6;
A94: (len f-'1)*(1+1)<(len f-'1)*(1+1)+i2 by A2,XREAL_1:29;
i1+1-1<=len f-1 by A9,XREAL_1:9;
then 1+i1<=len g+(len f-'1) by A3,A11,XREAL_1:7;
then len f-1+(1+i1)<=len f-1+(len g+(len f-'1)) by XREAL_1:6;
then
A95: len f+i1-len g<=len f-1+len g+(len f-' 1)-len g by XREAL_1:9;
len f+i1-len g=len f+i1-'len g by A27,NAT_D:37;
hence contradiction by A11,A93,A95,A94,XXREAL_0:2;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
case
A96: len f+i1-'len g mod (len f -'1)=0;
ex n being Nat st len f+i1-'len g =(len f-'1)*n+((len f+i1-'
len g) mod (len f -'1)) & ((len f+i1-'len g) mod (len f -'1))<len f -'1 by A25,
NAT_D:def 2;
then consider n being Nat such that
A97: len f+i1-'len g =(len f-'1)*n+((len f+i1-'len g) mod (len f -'1));
A98: now
assume n>1;
then n>=1+1 by NAT_1:13;
then
A99: len f+i1-'len g>=(len f-'1)*(1+1) by A96,A97,NAT_1:4;
now
assume i1+1<len f;
then i1+1+1<len f+len g by A3,XREAL_1:8;
then i1+1+1-1<len f+len g-1 by XREAL_1:9;
then i1+1-len g<len f+len g-1-len g by XREAL_1:9;
then len f-1+(i1+1-len g)<len f-1+(len f-1) by XREAL_1:6;
then len f+i1-len g<len f-1+(len f-1);
hence contradiction by A27,A11,A99,NAT_D:37;
end;
then i1+1=len f by A9,XXREAL_0:1;
then i2+1>len f-1+1 by A2,XREAL_1:6;
hence contradiction by A1;
end;
now
assume n=0;
then
A100: len f+i1<=len g by A96,A97,NAT_D:36;
len f<=len f+i1 by NAT_1:11;
hence contradiction by A27,A100,XXREAL_0:2;
end;
then n>=0+1 by NAT_1:13;
then
A101: n=1 by A98,XXREAL_0:1;
len f+i1-'len g=i2*n by A35,A96,A97,Def1;
then
A102: len f+i1-len g=i2 by A27,A101,NAT_D:37;
then
A103: len f+i1-i2=len g;
A104: dom g = Seg len g by FINSEQ_1:def 3;
A105: len (mid(f,i1,1))=i1-'1+1 by A4,A24,FINSEQ_6:187
.=i1 by A4,XREAL_1:235;
len (mid(f,len f-'1,i2))=len f-'1-'i2+1 by A19,A11,A8,A26,
FINSEQ_6:187;
then len (mid(f,len f-'1,i2))=len f-1-i2+1 by A11,A8,XREAL_1:233;
then len (mid(f,i1,1)^mid(f,len f-'1,i2))=i1+(len f-i2) by A105,
FINSEQ_1:22
.=i1+len f-i2
.=len f+i1-'i2 by A7,A6,NAT_D:37,XXREAL_0:2;
then
A106: len (mid(f,i1,1)^mid(f,len f-'1,i2))=len g by A7,A6,A103,NAT_D:37
,XXREAL_0:2;
for j be Nat st j in dom g holds g.j = (mid(f,i1,1)^mid(f,len
f-'1,i2)).j
proof
let j be Nat;
assume
A107: j in dom g;
then
A108: 1<=j by A104,FINSEQ_1:1;
A109: j<=len g by A104,A107,FINSEQ_1:1;
then
A110: g.j=f.S_Drop(len f+i1-'j,f) by A1,A108;
A111: len f+i1-'j=len f+i1-j by A27,A109,NAT_D:37,XXREAL_0:2;
now
per cases;
case
A112: j<=len mid(f,i1,1);
len f-'1<=len f by NAT_D:50;
then len f-1+j<=len f+i1 by A11,A105,A112,XREAL_1:7;
then
A113: len f-1+j-j<=len f+i1-j by XREAL_1:9;
j in dom mid(f,i1,1) by A108,A112,FINSEQ_3:25;
then
A114: (mid(f,i1,1)^mid(f,len f-'1,i2)).j =mid(f, i1,1).j by
FINSEQ_1:def 7;
A115: len mid(f,i1,1)=i1-'1+1 by A4,A23,FINSEQ_6:187;
now
per cases;
case
len f+i1-'j=len f-'1;
then len f+i1-j=len f-1 by A11,A105,A112,NAT_D:37;
then i1+1=j;
hence thesis by A105,A112,NAT_1:13;
end;
case
A116: len f+i1-'j<>len f-'1;
A117: j-1>=0 by A108,XREAL_1:48;
then j-1=j-'1 by XREAL_0:def 2;
then
A118: len f<=len f+(j-1) by NAT_1:11;
A119: len f+i1-'j>len f-'1 by A11,A111,A113,A116,XXREAL_0:1;
now
per cases;
case
A120: i1+1=len f & j-1=0;
then len f+i1-'j=len f-1+len f-1 by A4,NAT_D:37
.=len f-'1+(len f-'1) by A11;
then (len f+i1-'j)mod (len f-'1)=0 by Th3;
then S_Drop(len f+i1-'j,f) =j+i1-'1 by A120,Def1;
then S_Drop(len f+i1-'j,f) =i1+ 1-1 by A120,NAT_D:37
.=i1-j+1 by A120;
then
A121: f.S_Drop(len f+i1-'j,f)=f.(i1-'j+1) by A105,A112,
XREAL_1:233;
A122: 1<=i1-'j+1 by NAT_1:11;
i1<=i1+(j-'1) by NAT_1:11;
then
A123: i1-(j-'1)<=i1 by XREAL_1:20;
A124: i1-j+1=i1-'j+1 by A105,A112,XREAL_1:233;
A125: j-1=j-'1 by A108,XREAL_1:233;
mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1) by A4,A23,A108
,A112,A115,FINSEQ_6:191
.=f.(i1-'j+1) by A23,A124,A122,A125,A123,FINSEQ_6:123
;
hence thesis by A1,A108,A109,A114,A121;
end;
case
A126: i1+1<>len f or j-1<>0;
now
per cases by A126;
case
i1+1<>len f;
then i1+1<len f by A9,XXREAL_0:1;
hence i1+1<len f+(j-1) by A118,XXREAL_0:2;
end;
case
j-1<>0;
then len f<len f+(j-1) by A117,XREAL_1:29;
hence i1+1<len f+(j-1) by A9,XXREAL_0:2;
end;
end;
then i1+1-j<len f-1+j-j by XREAL_1:9;
then
A127: len f-1+(i1+1-j)<len f-1+( len f-1) by XREAL_1:8;
then (len f+i1-'j) mod (len f-'1)<>0 by A11,A111,A119
,Th1;
then
A128: S_Drop(len f+i1-'j,f) =(len f+i1-'j) mod (len f
-'1) by Def1
.=len f+(i1-j)-(len f-1) by A11,A111,A113,A127,Th2
.=(i1-j)+1;
A129: 1<=i1-'j+1 by NAT_1:11;
i1<=i1+(j-'1) by NAT_1:11;
then
A130: i1-(j-'1)<=i1 by XREAL_1:20;
A131: i1-j+1=i1-'j+1 by A105,A112,XREAL_1:233;
A132: j-1=j-'1 by A108,XREAL_1:233;
mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1) by A4,A23,A108
,A112,A115,FINSEQ_6:191
.=f.(i1-'j+1) by A23,A131,A129,A132,A130,FINSEQ_6:123
;
hence thesis by A105,A110,A112,A114,A128,XREAL_1:233;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
A133: j>len mid(f,i1,1);
i2+1-1<=len f-1 by A7,XREAL_1:9;
then
A134: i2-i2<=len f-1-i2 by XREAL_1:9;
A135: len f-i2=len f-1-i2+1
.=len f-'1-'i2+1 by A11,A134,XREAL_0:def 2;
A136: len f+0<len f+i1 by A4,XREAL_1:8;
A137: (mid(f,i1,1)^(mid(f,len f-'1,i2))).j =(mid(f,len f-'1,i2
)).(j-len mid(f,i1,1)) by A106,A109,A133,FINSEQ_6:108;
A138: j-i1<=len f+i1-i2-i1 by A102,A109,XREAL_1:9;
i1+1<=j by A105,A133,NAT_1:13;
then
A139: i1+1-i1<=j-i1 by XREAL_1:9;
then
A140: j-i1 =j-'len mid(f,i1,1) by A105,XREAL_0:def 2;
i2-i1>=0 by A2,XREAL_1:48;
then len f+0<=len f+(i2-i1) by XREAL_1:7;
then
A141: len f-(i2-i1)<=len f+(i2-i1)-(i2-i1) by XREAL_1:9;
A142: j<=len f+i1-i2 by A102,A104,A107,FINSEQ_1:1;
then j<=len f by A141,XXREAL_0:2;
then j<len f+i1 by A136,XXREAL_0:2;
then j-j<len f+i1-j by XREAL_1:9;
then
A143: 0<len f+i1-'j by A142,A141,NAT_D:37,XXREAL_0:2;
len f-i2<=len f-1 by A19,XREAL_1:13;
then j-i1<=len f-'1 by A11,A138,XXREAL_0:2;
then j-'i1<=len f-'1 by A105,A133,XREAL_1:233;
then len f-'1-'(j-'i1)+1=len f-'1-(j-'i1)+1 by XREAL_1:233
.=len f-1-(j-i1)+1 by A11,A105,A133,XREAL_1:233
.=len f+i1-j
.=len f+i1-'j by A142,A141,NAT_D:37,XXREAL_0:2;
then
A144: (mid(f,i1,1)^(mid(f,len f-'1,i2))).j =f.(len f+i1-'j) by A19
,A11,A8,A26,A105,A137,A139,A138,A135,A140,FINSEQ_6:190;
A145: i1+1<=j by A105,A133,NAT_1:13;
A146: len f+i1-j=len f+i1-'j by A27,A109,NAT_D:37,XXREAL_0:2;
i1+1<=j by A105,A133,NAT_1:13;
then len f+(i1+1)<=len f+j by XREAL_1:6;
then len f+i1+1-1<=len f+j-1 by XREAL_1:9;
then len f+i1-j<=len f+j-1-j by XREAL_1:9;
then
A147: len f-'1>=len f+i1-'j by A11,A142,A141,NAT_D:37,XXREAL_0:2;
now
per cases;
case
A148: (len f+i1-'j) mod (len f -'1)=0;
then len f+i1-'j=len f-'1 by A143,A147,Th4;
hence thesis by A110,A144,A148,Def1;
end;
case
A149: (len f+i1-'j) mod (len f -'1)<>0;
len f+(i1+1)<=len f+j by A145,XREAL_1:7;
then len f+i1+1-j<=len f+j-j by XREAL_1:9;
then
A150: len f+i1+1-j-1<=len f-1 by XREAL_1:9;
A151: S_Drop(len f+i1-'j,f) = (len f+i1-'j) mod (len f -'1
) by A149,Def1;
len f+i1-j=len f-'1 implies contradiction by A146,A149,
NAT_D:25;
then len f+i1-'j<(len f-'1) by A11,A146,A150,XXREAL_0:1;
hence thesis by A110,A144,A151,NAT_D:24;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by A7,A6,A103,A106,FINSEQ_2:9,NAT_D:37,XXREAL_0:2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th29:
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part>_of f,i1,i2 holds Rev g is_a_part<_of f,i2,i1
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
A1: len g=len (Rev g) by FINSEQ_5:def 3;
assume
A2: g is_a_part>_of f,i1,i2;
then
A3: 1<=len g;
A4: len g<len f by A2;
A5: i1+1<=len f by A2;
then i1+1-1<=len f-1 by XREAL_1:9;
then
A6: i1<=len f-'1 by A3,A4,XREAL_1:233,XXREAL_0:2;
A7: i1<len f by A5,NAT_1:13;
A8: for i being Nat st 1<=i & i<=len (Rev g) holds (Rev g).i=f.S_Drop(len f
+i2-'i,f)
proof
let i be Nat;
assume that
A9: 1<=i and
A10: i<=len (Rev g);
len g<=len g+(i-'1) by NAT_1:11;
then len g<=len g+(i-1) by A9,XREAL_1:233;
then len g-(i-1)<=len g+(i-1)-(i-1) by XREAL_1:9;
then len g-i+1<=len g;
then
A11: len g-'i+1<=len g by A1,A10,XREAL_1:233;
A12: 1<=len g-'i+1 by NAT_1:11;
A13: (Rev g).i=g.(len g-i+1) by A1,A9,A10,FINSEQ_6:115
.=g.(len g-'i+1) by A1,A10,XREAL_1:233
.=f.S_Drop((i1+(len g-'i+1)-'1),f) by A2,A12,A11;
now
per cases;
case
A14: i1<=i2;
then len f-1+len g=len f-1+(i2-'i1+1) by A2,Th25;
then len f-1+len g=len f+(i2-'i1);
then len f-1+len g=len f+(i2-i1) by A14,XREAL_1:233;
then len f+i2-i=len f-1+(i1+len g)-i;
then len f+i2-'i=len f-1+(i1+(len g-i)) by A4,A1,A10,NAT_D:37
,XXREAL_0:2;
then len f+i2-'i=len f-1+(i1+(len g-'i)+1-1) by A1,A10,XREAL_1:233;
then len f+i2-'i=len f-1+(i1+(len g-'i+1)-'1) by NAT_D:37;
then len f+i2-'i=(i1+(len g-'i+1)-'1)+(len f-'1) by A3,A4,XREAL_1:233
,XXREAL_0:2;
hence thesis by A13,Th23;
end;
case
i1>i2;
then len g=len f+i2-'i1 by A2,Th26;
then len g+i1=len f+i2-i1+i1 by A7,NAT_D:37;
then len f+i2-'i=i1+len g-i by A1,A10,NAT_D:37;
then len f+i2-'i=i1+(len g-i);
then len f+i2-'i=i1+(len g-'i)+1-1 by A1,A10,XREAL_1:233;
hence thesis by A13,NAT_D:37;
end;
end;
hence thesis;
end;
A15: i2+1<=len f by A2;
A16: 1<=i1 by A2;
A17: (Rev g).len (Rev g)=(Rev g).len g by FINSEQ_5:def 3
.=g.(len g-len g+1) by A3,FINSEQ_6:115
.=f.S_Drop((i1+1-'1),f) by A2
.=f.S_Drop(i1,f) by NAT_D:34;
A18: now
per cases;
case
A19: i1 mod (len f-'1)<>0;
then i1 <> len f-'1 by NAT_D:25;
then
A20: i1<len f-'1 by A6,XXREAL_0:1;
S_Drop(i1,f)=i1 mod (len f-'1) by A19,Def1;
hence (Rev g).len (Rev g)=f.i1 by A17,A20,NAT_D:24;
end;
case
A21: i1 mod (len f-'1)=0;
then S_Drop(i1,f)=len f-'1 by Def1;
hence (Rev g).len (Rev g)=f.i1 by A16,A17,A6,A21,Th4;
end;
end;
1<=i2 by A2;
hence thesis by A16,A5,A15,A3,A4,A1,A18,A8;
end;
theorem Th30:
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part<_of f,i1,i2 holds Rev g is_a_part>_of f,i2,i1
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
A1: len g=len (Rev g) by FINSEQ_5:def 3;
assume
A2: g is_a_part<_of f,i1,i2;
then
A3: 1<=len g;
A4: 1<=i2 by A2;
A5: len g<len f by A2;
A6: i2+1<=len f by A2;
then
A7: i2<len f by NAT_1:13;
A8: for i being Nat st 1<=i & i<=len (Rev g) holds (Rev g).i=f.S_Drop((i2+i
)-'1,f)
proof
let i be Nat;
assume that
A9: 1<=i and
A10: i<=len (Rev g);
A11: 1<=len g-'i+1 by NAT_1:11;
len g<=len g+(i-'1) by NAT_1:11;
then len g<=len g+(i-1) by A9,XREAL_1:233;
then len g-(i-1)<=len g+(i-1)-(i-1) by XREAL_1:9;
then len g-i+1<=len g;
then
A12: len g-'i+1<=len g by A1,A10,XREAL_1:233;
A13: (Rev g).i=g.(len g-i+1) by A1,A9,A10,FINSEQ_6:115
.=g.(len g-'i+1) by A1,A10,XREAL_1:233
.=f.S_Drop(len f+i1-'(len g-'i+1),f) by A2,A11,A12;
len g+1<=len g+1+i by NAT_1:11;
then len g+1-i<=len g+1+i-i by XREAL_1:9;
then len g-i+1<=len g+1;
then
A14: len g-'i+1<=len g+1 by A1,A10,XREAL_1:233;
A15: len g+1<=len f by A5,NAT_1:13;
now
per cases;
case
A16: i1<i2;
len f=len f-'1+1 by A3,A5,XREAL_1:235,XXREAL_0:2;
then
A17: -len f+i2+i=i2+i-1-(len f-'1);
len g=len f+i1-'i2 by A2,A16,Th28;
then len g=len f+i1-i2 by A7,NAT_D:37;
then i1-(len g-i)=i2+i-'1-(len f-'1) by A4,A17,NAT_D:37;
then i1-(len g-'i)=i2+i-'1-(len f-'1) by A1,A10,XREAL_1:233;
then len f-'1+1+i1-(len g-'i+1)=len f-'1+(i2+i-'1)-(len f-'1);
then len f+i1-(len g-'i+1)=len f-'1+(i2+i-'1)-(len f-'1) by A3,A5,
XREAL_1:235,XXREAL_0:2;
hence thesis by A13,A15,A14,NAT_D:37,XXREAL_0:2;
end;
case
A18: i1>=i2;
then len g=i1-'i2+1 by A2,Th27;
then len g=i1-i2+1 by A18,XREAL_1:233;
then i1-(len g-i)=(i2+i)-1;
then i1-(len g-i)=(i2+i)-'1 by A9,NAT_D:37;
then i1-(len g-'i)=(i2+i)-'1 by A1,A10,XREAL_1:233;
then len f-1+(i1-(len g-'i))=(i2+i)-'1+(len f-'1) by A3,A5,XREAL_1:233
,XXREAL_0:2;
then len f+i1-(len g-'i+1)=(i2+i)-'1+(len f-'1);
then (Rev g).i=f.S_Drop((i2+i)-'1+(len f-'1),f) by A13,A15,A14,NAT_D:37
,XXREAL_0:2
.=f.S_Drop((i2+i)-'1,f) by Th23;
hence thesis;
end;
end;
hence thesis;
end;
A19: S_Drop(len f-'1+i1,f)=S_Drop(i1,f) by Th23;
A20: i1+1<=len f by A2;
then i1+1-1<=len f-1 by XREAL_1:9;
then
A21: i1<=len f-'1 by A3,A5,XREAL_1:233,XXREAL_0:2;
A22: 1<=i1 by A2;
A23: (Rev g).len (Rev g)=(Rev g).len g by FINSEQ_5:def 3
.=g.(len g-len g+1) by A3,FINSEQ_6:115
.=f.S_Drop(len f+i1-'1,f) by A2
.=f.S_Drop(len f-'1+i1,f) by A3,A5,NAT_D:38,XXREAL_0:2;
now
per cases;
case
A24: i1 mod (len f-'1)<>0;
then i1 <> len f-'1 by NAT_D:25;
then
A25: i1<len f-'1 by A21,XXREAL_0:1;
S_Drop(i1,f)=i1 mod (len f-'1) by A24,Def1;
hence (Rev g).len (Rev g)=f.i1 by A23,A19,A25,NAT_D:24;
end;
case
A26: i1 mod (len f-'1)=0;
then S_Drop(i1,f)=len f-'1 by Def1;
hence (Rev g).len (Rev g)=f.i1 by A22,A23,A21,A19,A26,Th4;
end;
end;
hence thesis by A22,A20,A4,A6,A3,A5,A1,A8;
end;
theorem Th31:
for f being non constant standard special_circular_sequence, i1,
i2 being Nat st 1<=i1 & i1<=i2 & i2<len f holds mid(f,i1,i2)
is_a_part>_of f,i1,i2
proof
let f be non constant standard special_circular_sequence, i1,i2 be Nat;
assume that
A1: 1<=i1 and
A2: i1<=i2 and
A3: i2<len f;
A4: 1<=i2 by A1,A2,XXREAL_0:2;
A5: i1<len f by A2,A3,XXREAL_0:2;
then
A6: len mid(f,i1,i2)=i2-'i1+1 by A1,A2,A3,A4,FINSEQ_6:118;
then
A7: 1<=len mid(f,i1,i2) by NAT_1:11;
A8: i2+1<=len f by A3,NAT_1:13;
A9: i2-'i1+1=i2-i1+1 by A2,XREAL_1:233;
A10: for i being Nat st 1<=i & i<=len mid(f,i1,i2) holds mid(f,i1,i2).i=f.
S_Drop((i1+i)-'1,f)
proof
let i be Nat;
assume that
A11: 1<=i and
A12: i<=len mid(f,i1,i2);
i+i1<=i2-i1+1+i1 by A6,A9,A12,XREAL_1:6;
then i1+i<=len f by A8,XXREAL_0:2;
then i1+i-1<=len f-1 by XREAL_1:9;
then i1+i-1<=len f-'1 by A3,A4,XREAL_1:233,XXREAL_0:2;
then
A13: i1+i-'1<=len f-'1 by A1,NAT_D:37;
1+1<=i1+i by A1,A11,XREAL_1:7;
then 1+1-1<=i1+i-1 by XREAL_1:9;
then 1<=i1+i-'1 by A1,NAT_D:37;
then S_Drop((i1+i)-'1,f)=(i1+i)-'1 by A13,Th22;
hence thesis by A1,A2,A3,A4,A5,A11,A12,FINSEQ_6:118;
end;
A14: mid(f,i1,i2).len mid(f,i1,i2)=f.i2 by A1,A2,A3,FINSEQ_6:188;
A15: i1+1<=len f by A5,NAT_1:13;
i2+1<i2+1+i1 by A1,XREAL_1:29;
then i2+1-i1<i2+1+i1-i1 by XREAL_1:9;
then len mid(f,i1,i2)<len f by A8,A6,A9,XXREAL_0:2;
hence thesis by A1,A4,A15,A8,A14,A7,A10;
end;
theorem Th32:
for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i1 & i1<=i2 & i2<len f holds
mid(f,i2,i1) is_a_part<_of f,i2,i1
proof
let f be non constant standard special_circular_sequence, i1,i2 be Nat;
assume that
A1: 1<=i1 and
A2: i1<=i2 and
A3: i2<len f;
Rev mid(f,i1,i2) is_a_part<_of f,i2,i1 by A1,A2,A3,Th29,Th31;
hence thesis by FINSEQ_6:196;
end;
theorem Th33:
for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i2 & i1>i2 & i1<len f holds
mid(f,i1,len f-'1)^mid(f,1,i2) is_a_part>_of f,i1,i2
proof
let f be non constant standard special_circular_sequence, i1,i2 be Nat;
assume that
A1: 1<=i2 and
A2: i1>i2 and
A3: i1<len f;
A4: len mid(f,1,i2)=len (f|i2) by A1,FINSEQ_6:116
.=i2 by A2,A3,FINSEQ_1:59,XXREAL_0:2;
A5: 1<=i1 by A1,A2,XXREAL_0:2;
len f<len f+1 by NAT_1:13;
then len f-1<len f+1-1 by XREAL_1:9;
then
A6: len f-'1<len f by A3,A5,XREAL_1:233,XXREAL_0:2;
A7: i1+1<=len f by A3,NAT_1:13;
then i1+1-1<=len f-1 by XREAL_1:9;
then
A8: i1<=len f-'1 by A3,A5,XREAL_1:233,XXREAL_0:2;
then
A9: 1<=len f-'1 by A5,XXREAL_0:2;
then len mid(f,i1,len f-'1)=len f-'1-'i1+1 by A3,A5,A8,A6,FINSEQ_6:118
.=len f-'1-i1+1 by A8,XREAL_1:233
.=len f-1-i1+1 by A3,A5,XREAL_1:233,XXREAL_0:2
.=len f-i1;
then
A10: len (mid(f,i1,len f-'1)^mid(f,1,i2))=len f-i1 +i2 by A4,FINSEQ_1:22
.=len f-(i1-i2);
A11: i2<len f by A2,A3,XXREAL_0:2;
then
A12: i2+1<=len f by NAT_1:13;
then i2+1-1<=len f-1 by XREAL_1:9;
then
A13: i2<=len f-'1 by A3,A5,XREAL_1:233,XXREAL_0:2;
A14: for i being Nat st 1<=i & i<=len (mid(f,i1,len f-'1)^mid(f,1,i2)) holds
(mid(f,i1,len f-'1)^mid(f,1,i2)).i =f.S_Drop((i1+i)-'1,f)
proof
let i be Nat;
assume that
A15: 1<=i and
A16: i<=len (mid(f,i1,len f-'1)^mid(f,1,i2));
A17: i1+i-'1=i1+i-1 by A15,NAT_D:37;
A18: len f-i1=len f-'i1 by A3,XREAL_1:233;
A19: len f-'1-'i1+1=len f-'1-i1+1 by A8,XREAL_1:233
.=len f-1-i1+1 by A3,A5,XREAL_1:233,XXREAL_0:2
.=len f-i1;
A20: len mid(f,i1,len f-'1)=len f-'1-'i1+1 by A3,A5,A8,A9,A6,FINSEQ_6:118;
now
per cases;
case
A21: i<=len mid(f,i1,len f-'1);
then i1+i<=i1+(len f-'1-'i1+1) by A20,XREAL_1:6;
then i1+i<=(len f-'1-i1+1)+i1 by A8,XREAL_1:233;
then i1+i<=len f-'1+1;
then i1+i<=len f by A3,A5,XREAL_1:235,XXREAL_0:2;
then i1+i-'1<=len f-1 by A17,XREAL_1:9;
then
A22: i1+i-'1<=len f-'1 by A3,A5,XREAL_1:233,XXREAL_0:2;
0<=i-1 by A15,XREAL_1:48;
then
A23: 1+0<=i1+(i-1) by A5,XREAL_1:7;
i in dom mid(f,i1,len f-'1) by A15,A21,FINSEQ_3:25;
then
A24: (mid(f,i1,len f-'1)^mid(f,1,i2)).i=mid(f,i1,len f-'1).i by
FINSEQ_1:def 7;
mid(f,i1,len f-'1).i=f.(i1+i-'1) by A3,A5,A8,A9,A6,A15,A21,
FINSEQ_6:118;
hence thesis by A17,A24,A23,A22,Th22;
end;
case
A25: i>len mid(f,i1,len f-'1);
then i>=len f-'i1+1 by A20,A19,A18,NAT_1:13;
then
A26: i-(len f-'i1)>=len f-'i1+1-(len f-'i1) by XREAL_1:9;
then
A27: 1<=i-'(len f-'i1) by NAT_D:39;
A28: len f-i1=len f-'i1 by A3,XREAL_1:233;
i-(len f-i1)<=len f-i1+i2-(len f-i1) by A10,A16,XREAL_1:9;
then
A29: i-'(len f-'i1)<=i2 by A28,A26,NAT_D:39;
then
A30: i-'(len f-'i1)<=len f-'1 by A13,XXREAL_0:2;
len f-'1+(i-'(len f-'i1))=len f-'1+(i-(len f-'i1)) by A20,A19,A18,A25,
XREAL_1:233
.=len f-'1+i-(len f-'i1)
.=len f-1+i-(len f-'i1) by A3,A5,XREAL_1:233,XXREAL_0:2
.=len f-1+i-(len f-i1) by A3,XREAL_1:233
.=(i+i1)-1
.=i1+i-'1 by A15,NAT_D:37;
then
A31: S_Drop((i1+i)-'1,f) =S_Drop(i-'(len f-'i1),f) by Th23
.=i-'(len f-'i1) by A27,A30,Th22;
(mid(f,i1,len f-'1)^mid(f,1,i2)).i =mid(f,1,i2).(i-len mid(f,i1,
len f-'1)) by A16,A25,FINSEQ_6:108
.=mid(f,1,i2).(i-'(len f-'i1)) by A20,A19,A18,A25,XREAL_1:233
.=f.(i-'(len f-'i1)) by A11,A27,A29,FINSEQ_6:123;
hence thesis by A31;
end;
end;
hence thesis;
end;
i1-i2>0 by A2,XREAL_1:50;
then len f<len f+(i1-i2) by XREAL_1:29;
then
A32: len f-(i1-i2)<len f+(i1-i2)-(i1-i2) by XREAL_1:9;
A33: len (mid(f,i1,len f-'1)^mid(f,1,i2)) =len mid(f,i1,len f-'1)+ len mid(f
,1,i2) by FINSEQ_1:22;
then len mid(f,1,i2)<=len (mid(f,i1,len f-'1)^mid(f,1,i2)) by NAT_1:11;
then
A34: 1<=len (mid(f,i1,len f-'1)^mid(f,1,i2)) by A1,A4,XXREAL_0:2;
len mid(f,i1,len f-'1)< len mid(f,i1,len f-'1)+ len mid(f,1,i2) by A1,A4,
XREAL_1:29;
then
(mid(f,i1,len f-'1)^mid(f,1,i2)).len (mid(f,i1,len f-'1)^mid(f,1,i2 ) )
=mid(f,1,i2).(len mid(f,i1,len f-'1)+ len mid(f,1,i2) -len mid(f,i1,len f-'1))
by A33,FINSEQ_6:108
.=f.i2 by A1,A11,FINSEQ_6:188;
hence thesis by A1,A5,A12,A7,A34,A10,A32,A14;
end;
theorem Th34:
for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i1 & i1<i2 & i2<len f holds
mid(f,i1,1)^mid(f,len f-'1,i2) is_a_part<_of f,i1,i2
proof
let f be non constant standard special_circular_sequence, i1,i2 be Nat;
assume that
A1: 1<=i1 and
A2: i1<i2 and
A3: i2<len f;
Rev (mid(f,i2,len f-'1)^mid(f,1,i1)) =Rev(mid(f,1,i1))^Rev(mid(f,i2,len
f-'1)) by FINSEQ_5:64
.=mid(f,i1,1)^Rev(mid(f,i2,len f-'1)) by FINSEQ_6:196
.=mid(f,i1,1)^mid(f,len f-'1,i2) by FINSEQ_6:196;
hence thesis by A1,A2,A3,Th29,Th33;
end;
theorem Th35:
for h being FinSequence of TOP-REAL 2,i1,i2 st 1<=i1 & i1<=len h
& 1<=i2 & i2<=len h holds L~mid(h,i1,i2) c= L~h
proof
let h be FinSequence of TOP-REAL 2,i1,i2;
assume that
A1: 1<=i1 and
A2: i1<=len h and
A3: 1<=i2 and
A4: i2<=len h;
thus L~mid(h,i1,i2) c= L~h
proof
let x be object;
assume
A5: x in L~mid(h,i1,i2);
now
per cases;
case
A6: i1<=i2;
x in union { LSeg(mid(h,i1,i2),i) : 1 <= i & i+1 <= len mid(h,i1,
i2) } by A5,TOPREAL1:def 4;
then consider Y being set such that
A7: x in Y & Y in { LSeg(mid(h,i1,i2),i) : 1 <= i & i+1 <= len mid
(h,i1,i2) } by TARSKI:def 4;
consider i such that
A8: Y=LSeg(mid(h,i1,i2),i) and
A9: 1 <= i and
A10: i+1 <= len mid(h,i1,i2) by A7;
A11: LSeg(mid(h,i1,i2),i)=LSeg(mid(h,i1,i2)/.i,mid(h,i1,i2)/.(i+1)) by A9
,A10,TOPREAL1:def 3;
i<=i+1 by NAT_1:11;
then
A12: i<=len mid(h,i1,i2) by A10,XXREAL_0:2;
then
A13: mid(h,i1,i2).i=h.(i+i1-'1) by A1,A2,A3,A4,A6,A9,FINSEQ_6:118;
A14: mid(h,i1,i2)/.i=mid(h,i1,i2).i by A9,A12,FINSEQ_4:15;
A15: mid(h,i1,i2)/.(i+1)=mid(h,i1,i2).(i+1) by A10,FINSEQ_4:15,NAT_1:11;
1+1<=i+i1 by A1,A9,XREAL_1:7;
then
A16: 1+1-1<=i+i1-1 by XREAL_1:9;
then
A17: 1<=i+i1-'1 by A1,NAT_D:37;
i+i1-'1<=i+i1-'1+1 by NAT_1:11;
then i+i1-'1<=i+i1-1+1 by A1,NAT_D:37;
then
A18: 1<=i+i1 by A17,XXREAL_0:2;
1<=i+1 by NAT_1:11;
then
A19: mid(h,i1,i2).(i+1)=h.(i+1+i1-'1) by A1,A2,A3,A4,A6,A10,FINSEQ_6:118;
A20: i+1+i1-'1=i+1+i1-1 by A1,NAT_D:37
.=i+i1;
then
A21: i+1+i1-'1=i+i1-1+1 .=i+i1-'1+1 by A1,NAT_D:37;
len mid(h,i1,i2)=i2-'i1+1 by A1,A2,A3,A4,A6,FINSEQ_6:118;
then i+1-1<=i2-'i1+1-1 by A10,XREAL_1:9;
then i<=i2-i1 by A6,XREAL_1:233;
then
A22: i+i1<=i2-i1+i1 by XREAL_1:6;
then
A23: i+i1<=len h by A4,XXREAL_0:2;
A24: i+i1<=len h by A4,A22,XXREAL_0:2;
then h/.(i+i1-'1)=h.(i+i1-'1) by A17,FINSEQ_4:15,NAT_D:44;
then
LSeg(mid(h,i1,i2),i)=LSeg(h/.(i+i1-'1),h/.(i+1+i1-'1)) by A11,A13,A19
,A14,A15,A20,A18,A23,FINSEQ_4:15
.=LSeg(h,i+i1-'1) by A16,A24,A20,A21,TOPREAL1:def 3;
then LSeg(mid(h,i1,i2),i) in { LSeg(h,j) : 1 <= j & j+1 <= len h} by
A16,A20,A21,A23;
then x in union { LSeg(h,j) : 1 <= j & j+1 <= len h} by A7,A8,
TARSKI:def 4;
hence thesis by TOPREAL1:def 4;
end;
case
A25: i1>i2;
mid(h,i1,i2)=Rev mid(h,i2,i1) by FINSEQ_6:196;
then x in L~mid(h,i2,i1) by A5,SPPOL_2:22;
then
x in union { LSeg(mid(h,i2,i1),i) : 1 <= i & i+1 <= len mid(h,i2,
i1) } by TOPREAL1:def 4;
then consider Y being set such that
A26: x in Y & Y in { LSeg(mid(h,i2,i1),i) : 1 <= i & i+1 <= len
mid(h,i2,i1) } by TARSKI:def 4;
consider i such that
A27: Y=LSeg(mid(h,i2,i1),i) and
A28: 1 <= i and
A29: i+1 <= len mid(h,i2,i1) by A26;
A30: LSeg(mid(h,i2,i1),i)=LSeg(mid(h,i2,i1)/.i,mid(h,i2,i1)/.(i+1)) by A28
,A29,TOPREAL1:def 3;
i<=i+1 by NAT_1:11;
then
A31: i<=len mid(h,i2,i1) by A29,XXREAL_0:2;
then
A32: mid(h,i2,i1).i=h.(i+i2-'1) by A1,A2,A3,A4,A25,A28,FINSEQ_6:118;
A33: mid(h,i2,i1)/.i=mid(h,i2,i1).i by A28,A31,FINSEQ_4:15;
A34: mid(h,i2,i1)/.(i+1)=mid(h,i2,i1).(i+1) by A29,FINSEQ_4:15,NAT_1:11;
1+1<=i+i2 by A3,A28,XREAL_1:7;
then
A35: 1+1-1<=i+i2-1 by XREAL_1:9;
then
A36: 1<=i+i2-'1 by A3,NAT_D:37;
i+i2-'1<=i+i2-'1+1 by NAT_1:11;
then i+i2-'1<=i+i2-1+1 by A3,NAT_D:37;
then
A37: 1<=i+i2 by A36,XXREAL_0:2;
1<=i+1 by NAT_1:11;
then
A38: mid(h,i2,i1).(i+1)=h.(i+1+i2-'1) by A1,A2,A3,A4,A25,A29,FINSEQ_6:118;
A39: i+1+i2-'1=i+1+i2-1 by A3,NAT_D:37
.=i+i2;
then
A40: i+1+i2-'1=i+i2-1+1 .=i+i2-'1+1 by A3,NAT_D:37;
len mid(h,i2,i1)=i1-'i2+1 by A1,A2,A3,A4,A25,FINSEQ_6:118;
then i+1-1<=i1-'i2+1-1 by A29,XREAL_1:9;
then i<=i1-i2 by A25,XREAL_1:233;
then
A41: i+i2<=i1-i2+i2 by XREAL_1:6;
then
A42: i+i2<=len h by A2,XXREAL_0:2;
A43: i+i2<=len h by A2,A41,XXREAL_0:2;
then h/.(i+i2-'1)=h.(i+i2-'1) by A36,FINSEQ_4:15,NAT_D:44;
then
LSeg(mid(h,i2,i1),i)=LSeg(h/.(i+i2-'1),h/.(i+1+i2-'1)) by A30,A32,A38
,A33,A34,A39,A37,A42,FINSEQ_4:15
.=LSeg(h,i+i2-'1) by A35,A43,A39,A40,TOPREAL1:def 3;
then LSeg(mid(h,i2,i1),i) in { LSeg(h,j) : 1 <= j & j+1 <= len h} by
A35,A39,A40,A42;
then x in union { LSeg(h,j) : 1 <= j & j+1 <= len h} by A26,A27,
TARSKI:def 4;
hence thesis by TOPREAL1:def 4;
end;
end;
hence thesis;
end;
end;
theorem Th36:
for g being FinSequence of D holds g is one-to-one iff for i1,i2
st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g & (g.i1=g.i2 or g/.i1=g/.i2) holds
i1 = i2
proof
let g be FinSequence of D;
A1: (for i1,i2 st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g & (g.i1=g.i2 or g/.
i1=g/.i2) holds i1=i2) implies g is one-to-one
proof
assume
A2: for i1,i2 st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g & (g.i1=g.i2
or g/.i1=g/.i2) holds i1=i2;
for x1,x2 being object st x1 in dom g & x2 in dom g & g.x1=g.x2
holds x1 = x2
proof
let x1,x2 be object;
assume that
A3: x1 in dom g and
A4: x2 in dom g and
A5: g.x1=g.x2;
reconsider n2=x2 as Nat by A4;
A6: 1<=n2 by A4,FINSEQ_3:25;
reconsider n1=x1 as Nat by A3;
A7: n1<=len g by A3,FINSEQ_3:25;
A8: n2<=len g by A4,FINSEQ_3:25;
1<=n1 by A3,FINSEQ_3:25;
hence thesis by A2,A5,A7,A6,A8;
end;
hence thesis by FUNCT_1:def 4;
end;
g is one-to-one implies for i1,i2 st 1<=i1<=len g & 1<=i2<=len
g & (g.i1=g.i2 or g/.i1=g/.i2) holds i1=i2
proof
assume
A9: g is one-to-one;
thus for i1,i2 st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g & (g.i1=g.i2 or g
/.i1=g/.i2) holds i1=i2
proof
let i1,i2;
assume that
A10: 1<=i1 and
A11: i1<=len g and
A12: 1<=i2 and
A13: i2<=len g and
A14: g.i1=g.i2 or g/.i1=g/.i2;
A15: i2 in dom g by A12,A13,FINSEQ_3:25;
A16: g/.i2=g.i2 by A12,A13,FINSEQ_4:15;
A17: g/.i1=g.i1 by A10,A11,FINSEQ_4:15;
i1 in dom g by A10,A11,FINSEQ_3:25;
hence thesis by A9,A14,A15,A17,A16,FUNCT_1:def 4;
end;
end;
hence thesis by A1;
end;
theorem Th37:
for f being non constant standard special_circular_sequence,
i2 st 1<i2 & i2+1<=len f holds f|i2 is being_S-Seq
proof
let f be non constant standard special_circular_sequence,i2;
assume that
A1: 1<i2 and
A2: i2+1<=len f;
i2<=len f by A2,NAT_1:13;
then
A3: len (f|i2)=i2 by FINSEQ_1:59;
for n1,n2 being Nat st 1<=n1 & n1<=len (f|i2) & 1<=n2 & n2<=
len (f|i2) &((f|i2).n1=(f|i2).n2 or (f|i2)/.n1=(f|i2)/.n2) holds n1=n2
proof
let n1,n2 be Nat;
assume that
A4: 1<=n1 and
A5: n1<=len (f|i2) and
A6: 1<=n2 and
A7: n2<= len (f|i2) and
A8: (f|i2).n1=(f|i2).n2 or (f|i2)/.n1=(f|i2)/.n2;
A9: n2 in dom (f|i2) by A6,A7,FINSEQ_3:25;
A10: n1 in dom (f|i2) by A4,A5,FINSEQ_3:25;
now
per cases by XXREAL_0:1;
case
A11: n1<n2;
n2+1<=i2+1 by A3,A7,XREAL_1:6;
then n2+1<=len f by A2,XXREAL_0:2;
then
A12: n2<len f by NAT_1:13;
len f>4 by GOBOARD7:34;
then
A13: f/.n1<>f/.n2 by A4,A11,A12,GOBOARD7:35;
A14: (f|i2)/.n1=f/.n1 by A10,FINSEQ_4:70;
A15: (f|i2)/.n2=f/.n2 by A9,FINSEQ_4:70;
(f|i2)/.n1=(f|i2).n1 by A4,A5,FINSEQ_4:15;
hence contradiction by A6,A7,A8,A13,A14,A15,FINSEQ_4:15;
end;
case
n1=n2;
hence thesis;
end;
case
A16: n2<n1;
n1+1<=i2+1 by A3,A5,XREAL_1:6;
then n1+1<=len f by A2,XXREAL_0:2;
then
A17: n1<len f by NAT_1:13;
len f>4 by GOBOARD7:34;
then
A18: f/.n2<>f/.n1 by A6,A16,A17,GOBOARD7:35;
A19: (f|i2)/.n2=f/.n2 by A9,FINSEQ_4:70;
A20: (f|i2)/.n1=f/.n1 by A10,FINSEQ_4:70;
(f|i2)/.n2=(f|i2).n2 by A6,A7,FINSEQ_4:15;
hence contradiction by A4,A5,A8,A18,A19,A20,FINSEQ_4:15;
end;
end;
hence thesis;
end;
then
A21: f|i2 is one-to-one by Th36;
for i,j be Nat st i+1 < j holds LSeg(f|i2,i) misses LSeg(f|i2,j)
proof
let i,j be Nat;
assume
A22: i+1 < j;
now
per cases;
case
A23: 1<=i & j+1<=len (f|i2);
i2<=len f by A2,NAT_1:13;
then len (f|i2)=i2 by FINSEQ_1:59;
then j+1<i2+1 by A23,NAT_1:13;
then j+1<len f by A2,XXREAL_0:2;
then
A24: LSeg(f,i) misses LSeg(f,j) by A22,GOBOARD5:def 4;
A25: j<=len (f|i2) by A23,NAT_1:13;
LSeg(f|i2,j)=LSeg(f,j) by A23,SPPOL_2:3;
then LSeg(f|i2,i) /\ LSeg(f|i2,j) = LSeg(f,i) /\ LSeg(f,j) by A22,A25,
SPPOL_2:3,XXREAL_0:2;
then LSeg(f|i2,i) /\ LSeg(f|i2,j) = {} by A24,XBOOLE_0:def 7;
hence thesis by XBOOLE_0:def 7;
end;
case
A26: 1>i or j+1>len (f|i2);
now
per cases by A26;
case
1>i;
then LSeg(f|i2,i)={} by TOPREAL1:def 3;
then LSeg(f|i2,i) /\ LSeg(f|i2,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
case
j+1>len (f|i2);
then LSeg(f|i2,j)={} by TOPREAL1:def 3;
then LSeg(f|i2,i) /\ LSeg(f|i2,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A27: f|i2 is s.n.c. by TOPREAL1:def 7;
1+1<=len (f|i2) by A1,A3,NAT_1:13;
hence thesis by A27,A21,TOPREAL1:def 8;
end;
theorem Th38:
for f being non constant standard special_circular_sequence,
i2 st 1<=i2 & i2+1<len f holds f/^i2 is being_S-Seq
proof
let f be non constant standard special_circular_sequence,i2;
assume that
A1: 1<=i2 and
A2: i2+1<len f;
A3: i2<len f by A2,NAT_1:13;
for i,j be Nat st i+1 < j holds LSeg(f/^i2,i) misses LSeg(f/^i2,j)
proof
let i,j be Nat;
assume
A4: i+1 < j;
then
A5: i<j by NAT_1:13;
now
per cases;
case
A6: 1<=i & j<len (f/^i2);
then 1<j by A5,XXREAL_0:2;
then LSeg(f/^i2,j)=LSeg(f,i2+j) by A3,SPPOL_2:4;
then
A7: LSeg(f/^i2,i) /\ LSeg(f/^i2,j) = LSeg(f,i2+i) /\ LSeg(f,i2+j) by A3,A6,
SPPOL_2:4;
i2+(i+1)<i2+j by A4,XREAL_1:6;
then
A8: i2+i+1<i2+j;
1+1<=i2+i by A1,A6,XREAL_1:7;
then
A9: 1<i2+i by XXREAL_0:2;
j<len f-i2 by A3,A6,RFINSEQ:def 1;
then j+i2<len f-i2+i2 by XREAL_1:6;
then LSeg(f,i2+i) misses LSeg(f,i2+j) by A8,A9,GOBOARD5:def 4;
then LSeg(f,i2+i) /\ LSeg(f,i2+j) = {} by XBOOLE_0:def 7;
hence thesis by A7,XBOOLE_0:def 7;
end;
case
A10: 1>i or j>=len (f/^i2);
now
per cases by A10;
case
1>i;
then LSeg(f/^i2,i)={} by TOPREAL1:def 3;
then LSeg(f/^i2,i) /\ LSeg(f/^i2,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
case
j>=len (f/^i2);
then j+1>len (f/^i2) by NAT_1:13;
then LSeg(f/^i2,j)={} by TOPREAL1:def 3;
then LSeg(f/^i2,i) /\ LSeg(f/^i2,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A11: f/^i2 is s.n.c. by TOPREAL1:def 7;
A12: len (f/^i2)=len f-i2 by A3,RFINSEQ:def 1;
for n1,n2 being Nat st 1<=n1 & n1<=len (f/^i2) & 1<=n2 & n2
<=len (f/^i2) &((f/^i2).n1=(f/^i2).n2 or (f/^i2)/.n1=(f/^i2)/.n2) holds n1=n2
proof
let n1,n2 be Nat;
assume that
A13: 1<=n1 and
A14: n1<=len (f/^i2) and
A15: 1<=n2 and
A16: n2<=len (f/^i2) and
A17: (f/^i2).n1=(f/^i2).n2 or (f/^i2)/.n1=(f/^i2)/.n2;
A18: n2 in dom (f/^i2) by A15,A16,FINSEQ_3:25;
A19: n1 in dom (f/^i2) by A13,A14,FINSEQ_3:25;
now
per cases by XXREAL_0:1;
case
n1<n2;
then
A20: i2+n1<i2+n2 by XREAL_1:6;
A21: 1<i2+1 by A1,NAT_1:13;
i2+1<=i2+n1 by A13,XREAL_1:6;
then
A22: 1<i2+n1 by A21,XXREAL_0:2;
n2+i2<=len f-i2+i2 by A12,A16,XREAL_1:6;
then
A23: f/.(i2+n1)<>f/.(i2+n2) by A22,A20,GOBOARD7:37;
A24: (f/^i2)/.n1=f/.(i2+n1) by A19,FINSEQ_5:27;
A25: (f/^i2)/.n2=f/.(i2+n2) by A18,FINSEQ_5:27;
(f/^i2)/.n1=(f/^i2).(n1) by A13,A14,FINSEQ_4:15;
hence contradiction by A15,A16,A17,A23,A24,A25,FINSEQ_4:15;
end;
case
n1=n2;
hence thesis;
end;
case
n2<n1;
then
A26: i2+n2<i2+n1 by XREAL_1:6;
A27: 1<i2+1 by A1,NAT_1:13;
i2+1<=i2+n2 by A15,XREAL_1:6;
then
A28: 1<i2+n2 by A27,XXREAL_0:2;
n1+i2<=len f-i2+i2 by A12,A14,XREAL_1:6;
then
A29: f/.(i2+n2)<>f/.(i2+n1) by A28,A26,GOBOARD7:37;
n2 in dom (f/^i2) by A15,A16,FINSEQ_3:25;
then
A30: (f/^i2)/.n2=f/.(i2+n2) by FINSEQ_5:27;
n1 in dom (f/^i2) by A13,A14,FINSEQ_3:25;
then
A31: (f/^i2)/.n1=f/.(i2+n1) by FINSEQ_5:27;
(f/^i2)/.n2=(f/^i2).n2 by A15,A16,FINSEQ_4:15;
hence contradiction by A13,A14,A17,A29,A30,A31,FINSEQ_4:15;
end;
end;
hence thesis;
end;
then
A32: f/^i2 is one-to-one by Th36;
i2+1-i2<len f-i2 by A2,XREAL_1:9;
then 1+1<=len (f/^i2) by A12,NAT_1:13;
hence thesis by A11,A32,TOPREAL1:def 8;
end;
theorem Th39:
for f being non constant standard special_circular_sequence,
i1,i2 st 1<=i1 & i1<i2 & i2+1<=len f holds
mid(f,i1,i2) is being_S-Seq
proof
let f be non constant standard special_circular_sequence, i1,i2;
assume that
A1: 1<=i1 and
A2: i1<i2 and
A3: i2+1<=len f;
A4: mid(f,i1,i2)=(f/^(i1-'1))|(i2-'i1+1) by A2,FINSEQ_6:def 3;
i1<i1+1 by NAT_1:13;
then i1-1<i1+1-1 by XREAL_1:9;
then i1-1<i2 by A2,XXREAL_0:2;
then
A5: i1-'1<i2 by A1,XREAL_1:233;
i2-'i1+1=i2-i1+1 by A2,XREAL_1:233
.=i2-(i1-1)
.=i2-(i1-'1) by A1,XREAL_1:233
.=i2-'(i1-'1) by A5,XREAL_1:233;
then
A6: mid(f,i1,i2)=(f|i2)/^(i1-'1) by A4,FINSEQ_5:80;
i2<len f by A3,NAT_1:13;
then i1-1+1<len (f|i2) by A2,FINSEQ_1:59;
then
A7: i1-'1+1<len (f|i2) by A1,XREAL_1:233;
1<i2 by A1,A2,XXREAL_0:2;
hence thesis by A3,A6,A7,Th7,Th37;
end;
theorem Th40:
for f being non constant standard special_circular_sequence,
i1,i2 st 1<i1 & i1<i2 & i2<=len f holds
mid(f,i1,i2) is being_S-Seq
proof
let f be non constant standard special_circular_sequence, i1,i2;
assume that
A1: 1<i1 and
A2: i1<i2 and
A3: i2<=len f;
A4: i2-(i1-'1)<=len f-(i1-'1) by A3,XREAL_1:9;
1+1<=i1 by A1,NAT_1:13;
then 1+1-1<=i1-1 by XREAL_1:9;
then
A5: 1<=i1-'1 by NAT_D:39;
A6: mid(f,i1,i2)=(f/^(i1-'1))|(i2-'i1+1) by A2,FINSEQ_6:def 3;
A7: i2-i1>0 by A2,XREAL_1:50;
then
A8: 1<>i2-'i1+1 by XREAL_0:def 2;
i2-'i1>0 by A7,XREAL_0:def 2;
then
A9: i2-'i1>=0+1 by NAT_1:13;
then
A10: 1<=i2-'i1+1 by NAT_1:13;
i1<i1+1 by NAT_1:13;
then i1-1<i1+1-1 by XREAL_1:9;
then i1-1<i2 by A2,XXREAL_0:2;
then i1-'1<i2 by A1,XREAL_1:233;
then
A11: i1-'1<len f by A3,XXREAL_0:2;
then len (f/^(i1-'1))=len f-(i1-'1) by RFINSEQ:def 1;
then i2-(i1-1)<=len (f/^(i1-'1)) by A1,A4,XREAL_1:233;
then i2-i1+1<=len (f/^(i1-'1));
then
A12: i2-'i1+1<=len (f/^(i1-'1)) by A9,NAT_D:39;
A13: i1<len f by A2,A3,XXREAL_0:2;
then i1-'1+1<len f by A1,XREAL_1:235;
then i1-'1+1-(i1-'1)<len f-(i1-'1) by XREAL_1:9;
then
A14: 1<=len (f/^(i1-'1)) by A11,RFINSEQ:def 1;
i1-'1+1<len f by A1,A13,XREAL_1:235;
then mid(f/^(i1-'1),1,i2-'i1+1) is being_S-Seq by A5,A14,A10,A12,A8,Th38,
JORDAN3:6;
hence thesis by A6,A10,FINSEQ_6:116;
end;
theorem Th41:
for p0,p,q1,q2 being Point of TOP-REAL 2 st p0 in LSeg(p,q1) &
p0 in LSeg(p,q2) & p<>p0 holds q1 in LSeg(p,q2) or q2 in LSeg(p,q1)
proof
let p0,p,q1,q2 be Point of TOP-REAL 2;
assume that
A1: p0 in LSeg(p,q1) and
A2: p0 in LSeg(p,q2) and
A3: p<>p0;
consider r such that
A4: p0=(1-r)*p + r*q1 and
A5: 0 <= r and
A6: r <= 1 by A1;
A7: 1-r>=0 by A6,XREAL_1:48;
A8: p0-r*q1=(1-r)*p by A4,RLVECT_4:1;
consider s such that
A9: p0=(1-s)*p + s*q2 and
A10: 0 <= s and
A11: s <= 1 by A2;
A12: 1-s>=0 by A11,XREAL_1:48;
A13: p0-s*q2=(1-s)*p by A9,RLVECT_4:1;
A14: p0-(1-s)*p=s*q2 by A9,RLVECT_4:1;
A15: p0-(1-r)*p=r*q1 by A4,RLVECT_4:1;
A16: now
assume
A17: r<>s;
now
per cases by A17,XXREAL_0:1;
case
A18: r<s;
(1-r)*p0-(1-r)*((1-s)*p)=(1-r)*(s*q2) by A14,RLVECT_1:34;
then (1-r)*p0-((1-r)*(1-s))*p=(1-r)*(s*q2) by RLVECT_1:def 7;
then (1-r)*p0-((1-r)*(1-s))*p=((1-r)*s)*q2 by RLVECT_1:def 7;
then (1-r)*p0-(1-s)*((1-r)*p)=((1-r)*s)*q2 by RLVECT_1:def 7;
then (1-r)*p0-((1-s)*p0-(1-s)*(r*q1))=((1-r)*s)*q2 by A8,RLVECT_1:34;
then (1-r)*p0-(1-s)*p0+(1-s)*(r*q1)=((1-r)*s)*q2 by RLVECT_1:29;
then
A19: ((1-r)-(1-s))*p0+(1-s)*(r*q1)=((1-r)*s)*q2 by RLVECT_1:35;
A20: now
assume (1-r)*s=0;
then
A21: 1-r+r=0+r or s=0 by XCMPLX_1:6;
now
per cases by A21;
case
r=1;
hence contradiction by A11,A18;
end;
case
s=0;
hence contradiction by A5,A18;
end;
end;
hence contradiction;
end;
then 1=((1-r)*s)/((1-r)*s) by XCMPLX_1:60;
then 1=((1-r)*s)*((1-r)*s)" by XCMPLX_0:def 9;
then (((1-r)*s)*((1-r)*s)")*((s-r)*p0+(1-s)*(r*q1))=((1-r)*s)*q2 by A19
,RLVECT_1:def 8;
then ((1-r)*s)*(((1-r)*s)"*((s-r)*p0+(1-s)*(r*q1)))=((1-r)*s)*q2 by
RLVECT_1:def 7;
then q2=((1-r)*s)"*((s-r)*p0+(1-s)*(r*q1)) by A20,RLVECT_1:36;
then q2=((1-r)*s)"*((s-r)*p0+((1-s)*r)*q1) by RLVECT_1:def 7;
then q2=((1-r)*s)"*((s-r)*p0)+((1-r)*s)"*(((1-s)*r)*q1) by
RLVECT_1:def 5;
then q2=(((1-r)*s)"*(s-r))*p0+((1-r)*s)"*(((1-s)*r)*q1) by
RLVECT_1:def 7;
then
A22: q2=(((1-r)*s)"*(s-r))*p0+(((1-r)*s)"*((1-s)*r))*q1 by RLVECT_1:def 7;
set s1=(((1-r)*s)"*((1-s)*r));
q1 in LSeg(p,q1) by RLTOPSP1:68;
then
A23: LSeg(p0,q1) c= LSeg(p,q1) by A1,TOPREAL1:6;
r-s*r+s*r<=s-s*r+s*r by A18;
then 1*r-s*r<=(1-r)*s by XREAL_1:6;
then ((1-s)*r)/((1-r)*s)*((1-r)*s)<=1*((1-r)*s) by A20,XCMPLX_1:87;
then ((1-s)*r)/((1-r)*s)<=1 by A10,A7,A20,XREAL_1:68;
then
A24: s1<=1 by XCMPLX_0:def 9;
(((1-r)*s)"*(s-r))=(((1-r)*s)-((1-r)*s-(s-r)))/((1-r)*s) by
XCMPLX_0:def 9
.= ((1-r)*s)/((1-r)*s)-((1-r)*s-(s-r))/((1-r)*s) by XCMPLX_1:120
.= 1-(r+(s-r*s)-s)/((1-r)*s) by A20,XCMPLX_1:60
.=1-s1 by XCMPLX_0:def 9;
then q2 in LSeg(p0,q1) by A5,A10,A7,A12,A22,A24;
hence thesis by A23;
end;
case
A25: s<r;
(1-s)*p0-(1-s)*((1-r)*p)=(1-s)*(r*q1) by A15,RLVECT_1:34;
then (1-s)*p0-((1-s)*(1-r))*p=(1-s)*(r*q1) by RLVECT_1:def 7;
then (1-s)*p0-((1-s)*(1-r))*p=((1-s)*r)*q1 by RLVECT_1:def 7;
then (1-s)*p0-(1-r)*((1-s)*p)=((1-s)*r)*q1 by RLVECT_1:def 7;
then (1-s)*p0-((1-r)*p0-(1-r)*(s*q2))=((1-s)*r)*q1 by A13,RLVECT_1:34;
then (1-s)*p0-(1-r)*p0+(1-r)*(s*q2)=((1-s)*r)*q1 by RLVECT_1:29;
then
A26: ((1-s)-(1-r))*p0+(1-r)*(s*q2)=((1-s)*r)*q1 by RLVECT_1:35;
A27: now
assume (1-s)*r=0;
then
A28: 1-s+s=0+s or r=0 by XCMPLX_1:6;
now
per cases by A28;
case
s=1;
hence contradiction by A6,A25;
end;
case
r=0;
hence contradiction by A10,A25;
end;
end;
hence contradiction;
end;
then 1=((1-s)*r)/((1-s)*r) by XCMPLX_1:60;
then 1=((1-s)*r)*((1-s)*r)" by XCMPLX_0:def 9;
then (((1-s)*r)*((1-s)*r)")*((r-s)*p0+(1-r)*(s*q2))=((1-s)*r)*q1 by A26
,RLVECT_1:def 8;
then ((1-s)*r)*(((1-s)*r)"*((r-s)*p0+(1-r)*(s*q2)))=((1-s)*r)*q1 by
RLVECT_1:def 7;
then q1=((1-s)*r)"*((r-s)*p0+(1-r)*(s*q2)) by A27,RLVECT_1:36;
then q1=((1-s)*r)"*((r-s)*p0+((1-r)*s)*q2) by RLVECT_1:def 7;
then q1=((1-s)*r)"*((r-s)*p0)+((1-s)*r)"*(((1-r)*s)*q2) by
RLVECT_1:def 5;
then q1=(((1-s)*r)"*(r-s))*p0+((1-s)*r)"*(((1-r)*s)*q2) by
RLVECT_1:def 7;
then
A29: q1=(((1-s)*r)"*(r-s))*p0+(((1-s)*r)"*((1-r)*s))*q2 by RLVECT_1:def 7;
set s1=(((1-s)*r)"*((1-r)*s));
q2 in LSeg(p,q2) by RLTOPSP1:68;
then
A30: LSeg(p0,q2) c= LSeg(p,q2) by A2,TOPREAL1:6;
s-r*s+r*s<=r-r*s+r*s by A25;
then 1*s-r*s<=(1-s)*r by XREAL_1:6;
then ((1-r)*s)/((1-s)*r)*((1-s)*r)<=1*((1-s)*r) by A27,XCMPLX_1:87;
then ((1-r)*s)/((1-s)*r)<=1 by A5,A12,A27,XREAL_1:68;
then
A31: s1<=1 by XCMPLX_0:def 9;
(((1-s)*r)"*(r-s))=(((1-s)*r)-((1-s)*r-(r-s)))/((1-s)*r) by
XCMPLX_0:def 9
.= ((1-s)*r)/((1-s)*r)-((1-s)*r-(r-s))/((1-s)*r) by XCMPLX_1:120
.= 1-(s+(r-s*r)-r)/((1-s)*r) by A27,XCMPLX_1:60
.=1-s1 by XCMPLX_0:def 9;
then q1 in LSeg(p0,q2) by A5,A10,A7,A12,A29,A31;
hence thesis by A30;
end;
end;
hence thesis;
end;
now
assume r=s;
then r*q1+((1-r)*p-(1-r)*p) =r*q2+(1-r)*p-(1-r)*p by A4,A9,RLVECT_1:def 3;
then r*q1+0.TOP-REAL 2 =r*q2+(1-r)*p-(1-r)*p by RLVECT_1:5;
then r*q1+0.TOP-REAL 2 =r*q2 by RLVECT_4:1;
then
A32: r*q1=r*q2 by RLVECT_1:4;
A33: q1 in LSeg(p,q1) by RLTOPSP1:68;
now
per cases;
case
r<>0;
hence thesis by A32,A33,RLVECT_1:36;
end;
case
r=0;
then p0=(1-0)*p+0.TOP-REAL 2 by A4,RLVECT_1:10;
then p0=(1-0)*p by RLVECT_1:4;
hence contradiction by A3,RLVECT_1:def 8;
end;
end;
hence thesis;
end;
hence thesis by A16;
end;
theorem Th42:
for f being non constant standard special_circular_sequence
holds LSeg(f,1)/\ LSeg(f,len f-'1)={f.1}
proof
let f be non constant standard special_circular_sequence;
A1: 3<len f by GOBOARD7:34,XXREAL_0:2;
A2: len f>4 by GOBOARD7:34;
then
A3: len f-1=len f-'1 by XREAL_1:233,XXREAL_0:2;
A4: 2<len f by GOBOARD7:34,XXREAL_0:2;
then
A5: 1+1-1<=len f-1 by XREAL_1:9;
len f-1+1=len f;
then
A6: f/.len f in LSeg(f,len f-'1) by A3,A5,TOPREAL1:21;
A7: f/.1=f/.len f by FINSEQ_6:def 1;
A8: 1<len f by GOBOARD7:34,XXREAL_0:2;
A9: 3+1-1<len f-1 by A2,XREAL_1:9;
A10: LSeg(f,1)/\ LSeg(f,len f-'1) c={f.1}
proof
let x be object;
A11: 1+1<=len f by GOBOARD7:34,XXREAL_0:2;
assume
A12: x in LSeg(f,1)/\ LSeg(f,len f-'1);
then reconsider p=x as Point of TOP-REAL 2;
x in LSeg(f,1) by A12,XBOOLE_0:def 4;
then
A13: p in LSeg(f/.1,f/.(1+1)) by A11,TOPREAL1:def 3;
2+1-1<=len f-1 by A1,XREAL_1:9;
then
A14: 1+1-1<=len f-'1 -1 by A3,XREAL_1:9;
A15: LSeg(f/.1,f/.(1+1))=LSeg(f,1) by A4,TOPREAL1:def 3;
len f-'1+1=len f-1+1 by A2,XREAL_1:233,XXREAL_0:2
.=len f;
then
A16: f/.(len f-'1+1)=f/.1 by FINSEQ_6:def 1;
A17: LSeg(f/.(1+1),f/.(1+1+1))=LSeg(f,1+1) by A1,TOPREAL1:def 3;
x in LSeg(f,len f-'1) by A12,XBOOLE_0:def 4;
then
A18: p in LSeg(f/.1,f/.(len f-'1)) by A3,A5,A16,TOPREAL1:def 3;
len f<len f+1 by NAT_1:13;
then
A19: len f-1<len f+1-1 by XREAL_1:9;
len f-'1-'1+1=len f-'1-1+1 by A3,A5,XREAL_1:233
.=len f-'1;
then
A20: LSeg(f/.(len f-'1-'1),f/.(len f-'1))=LSeg(f,len f-'1-'1) by A3,A14,A19,
TOPREAL1:def 3;
A21: LSeg(f/.(len f-'1),f/.(len f-'1+1))=LSeg(f,len f-'1) by A3,A5,
TOPREAL1:def 3;
now
per cases;
case
A22: p<>f/.1;
now
per cases by A13,A18,A22,Th41;
case
A23: f/.(1+1) in LSeg(f/.1,f/.(len f-'1));
len f-'1+1=len f-1+1 by A2,XREAL_1:233,XXREAL_0:2
.=len f;
then
A24: f/.(len f-'1+1)=f/.1 by FINSEQ_6:def 1;
f/.(1+1) in LSeg(f/.(1+1),f/.(1+1+1)) by RLTOPSP1:68;
then
LSeg(f/.(1+1),f/.(1+1+1))/\ LSeg(f/.(len f-'1),f/.(len f-'1+1
)) <>{} by A23,A24,XBOOLE_0:def 4;
then LSeg(f/.(1+1),f/.(1+1+1)) meets LSeg(f/.(len f-'1),f/.(len f
-'1+1)) by XBOOLE_0:def 7;
hence contradiction by A9,A3,A17,A19,A21,GOBOARD5:def 4;
end;
case
A25: f/.(len f-'1) in LSeg(f/.1,f/.(1+1));
f/.(len f-'1) in LSeg(f/.(len f-'1-'1),f/.(len f-'1)) by
RLTOPSP1:68;
then LSeg(f,1)/\ LSeg(f,len f-'1-'1)<>{} by A15,A20,A25,
XBOOLE_0:def 4;
then
A26: LSeg(f,1) meets LSeg(f,len f-'1-'1) by XBOOLE_0:def 7;
3+1-1<len f-1 by A2,XREAL_1:9;
then 2+1-1<len f-1-1 by XREAL_1:9;
then
A27: 1+1<len f-'1-'1 by A3,A5,XREAL_1:233;
len f-1-1+1<len f by A19;
then len f-'1-'1+1<len f by A3,A5,XREAL_1:233;
hence contradiction by A26,A27,GOBOARD5:def 4;
end;
end;
hence contradiction;
end;
case
p=f/.1;
then x in {f/.1} by TARSKI:def 1;
hence thesis by A8,FINSEQ_4:15;
end;
end;
hence thesis;
end;
1+1<=len f by GOBOARD7:34,XXREAL_0:2;
then
A28: f/.1 in LSeg(f,1) by TOPREAL1:21;
f.1=f/.1 by A8,FINSEQ_4:15;
then f.1 in LSeg(f,1)/\ LSeg(f,len f-'1) by A28,A6,A7,XBOOLE_0:def 4;
then {f.1} c= LSeg(f,1)/\ LSeg(f,len f-'1) by ZFMISC_1:31;
hence thesis by A10,XBOOLE_0:def 10;
end;
theorem Th43:
for f being non constant standard special_circular_sequence,
i1,i2 being Nat,g1,g2 being FinSequence of TOP-REAL 2 st
1<=i1 & i1<i2 & i2<len f & g1=mid(f,i1,i2) &
g2=mid(f,i1,1)^mid(f,len f-'1,i2) holds
(L~g1)/\(L~g2)={f.i1,f.i2} & (L~g1) \/ (L~g2)=L~f
proof
let f be non constant standard special_circular_sequence, i1,i2 be Nat,
g1,g2 be FinSequence of TOP-REAL 2;
assume that
A1: 1<=i1 and
A2: i1<i2 and
A3: i2<len f and
A4: g1=mid(f,i1,i2) and
A5: g2=mid(f,i1,1)^mid(f,len f-'1,i2);
A6: i1<len f by A2,A3,XXREAL_0:2;
then
A7: 1<len f by A1,XXREAL_0:2;
then
A8: L~mid(f,i1,1) c= L~f by A1,A6,Th35;
A9: 1<i2 by A1,A2,XXREAL_0:2;
then
A10: len mid(f,i1,i2)=i2-'i1+1 by A1,A2,A3,A6,FINSEQ_6:118;
A11: i2+1<=len f by A3,NAT_1:13;
then
A12: i2+1-1<=len f-1 by XREAL_1:9;
then
A13: i2<=len f-'1 by A1,A6,XREAL_1:233,XXREAL_0:2;
then
A14: len f-'1-'i2+1=len f-'1-i2+1 by XREAL_1:233
.=len f-1-i2+1 by A1,A6,XREAL_1:233,XXREAL_0:2
.=len f-i2;
A15: 0<i2-i1 by A2,XREAL_1:50;
then 0<i2-'i1 by A2,XREAL_1:233;
then 0+1<=i2-'i1 by NAT_1:13;
then 1<len g1 by A4,A10,NAT_1:13;
then
A16: 1+1<=len g1 by NAT_1:13;
A17: {f.i1} c= L~g1
proof
let x be object;
assume x in {f.i1};
then
A18: x=f.i1 by TARSKI:def 1;
g1.1 =f.i1 by A1,A3,A4,A9,A6,FINSEQ_6:118;
hence thesis by A16,A18,JORDAN3:1;
end;
A19: 0+1<=len f-'1-'i2+1 by NAT_1:13;
A20: len mid(f,i1,1)=i1-'1+1 by A1,A6,FINSEQ_6:187;
then
A21: 0+1<=len mid(f,i1,1) by NAT_1:13;
A22: len f-'1<len f-'1+1 by NAT_1:13;
then
A23: len f-'1<len f by A1,A6,XREAL_1:235,XXREAL_0:2;
then
A24: len mid(f,len f-'1,i2)=len f-'1-'i2+1 by A9,A13,FINSEQ_6:187;
then
A25: 1<=len mid(f,len f-'1,i2) by NAT_1:11;
A26: 1<len f-'1 by A9,A13,XXREAL_0:2;
then
A27: f/.(len f-'1) =f.(len f-'1) by A23,FINSEQ_4:15
.=mid(f,len f-'1,i2).1 by A3,A9,A26,A23,FINSEQ_6:118
.=mid(f,len f-'1,i2)/.1 by A25,FINSEQ_4:15;
len f-'1+1=len f by A1,A6,XREAL_1:235,XXREAL_0:2;
then
A28: LSeg(f,len f-'1) =LSeg(f/.(len f-'1+1),f/.(len f-'1)) by A26,
TOPREAL1:def 3;
A29: f/.(len f-'1+1) =f/.len f by A1,A6,XREAL_1:235,XXREAL_0:2
.=f/.1 by FINSEQ_6:def 1
.=f.1 by A7,FINSEQ_4:15
.=mid(f,i1,1).len mid(f,i1,1) by A1,A6,A7,FINSEQ_6:189
.=mid(f,i1,1)/.len mid(f,i1,1) by A21,FINSEQ_4:15;
then LSeg(mid(f,i1,1)/.len mid(f,i1,1),mid(f,len f-'1,i2)/.1) c= L~f by A28
,A27,TOPREAL3:19;
then
A30: L~mid(f,i1,1) \/ LSeg(mid(f,i1,1)/.len mid(f,i1,1),mid(f,len f-'1,i2)
/.1) c= L~f by A8,XBOOLE_1:8;
A31: mid(f,i1,1)<><*>(TOP-REAL 2) by A20;
mid(f,len f-'1,i2)<><*>(TOP-REAL 2) by A24;
then
A32: L~(mid(f,i1,1)^mid(f,len f-'1,i2)) = L~mid(f,i1,1) \/ LSeg(mid(f,i1,1)
/.len mid(f,i1,1),mid(f,len f-'1,i2)/.1) \/ L~mid(f,len f-'1,i2) by A31,
SPPOL_2:23;
A33: L~f c= (L~g1) \/ (L~g2)
proof
let x be object;
assume
A34: x in L~f;
then reconsider p=x as Point of TOP-REAL 2;
consider i such that
A35: 1 <= i and
A36: i+1 <= len f and
A37: p in LSeg(f,i) by A34,SPPOL_2:13;
now
per cases;
case
A38: i1<=i & i<i2;
then i-i1<i2-i1 by XREAL_1:9;
then i-i1+1<i2-i1+1 by XREAL_1:6;
then i-'i1+1<i2-i1+1 by A38,XREAL_1:233;
then
A39: i-'i1+1<i2-'i1+1 by A2,XREAL_1:233;
0<=i-i1 by A38,XREAL_1:48;
then 0+1<=i-i1+1 by XREAL_1:6;
then
A40: 1<=i-'i1+1 by A38,XREAL_1:233;
i-'i1+1+i1-'1=i-'i1+1+i1-1 by A1,NAT_D:37
.=i-'i1+i1
.=i by A38,XREAL_1:235;
then x in LSeg(mid(f,i1,i2),i-'i1+1) by A1,A2,A3,A37,A40,A39,Th19;
then x in L~mid(f,i1,i2) by SPPOL_2:17;
hence thesis by A4,XBOOLE_0:def 3;
end;
case
A41: i<i1;
i1+1<=i1+i by A35,XREAL_1:6;
then i1<i1+i by NAT_1:13;
then i1-i<i1+i-i by XREAL_1:9;
then i1-'i<i1-1+1 by A41,XREAL_1:233;
then
A42: i1-'i<i1-'1+1 by A1,XREAL_1:233;
i1<=i1+i by NAT_1:11;
then i1-i<=i1+i-i by XREAL_1:9;
then i1-'i <= i1 by A41,XREAL_1:233;
then
A43: i1-'(i1-'i)=i1-(i1-'i) by XREAL_1:233
.=i1-(i1-i) by A41,XREAL_1:233
.=i;
i+1<=i1 by A41,NAT_1:13;
then i+1-i<=i1-i by XREAL_1:9;
then
A44: 1<=i1-'i by NAT_D:39;
1<i1 by A35,A41,XXREAL_0:2;
then x in LSeg(mid(f,i1,1),i1-'i) by A6,A37,A42,A44,A43,Th20;
then x in L~mid(f,i1,1) by SPPOL_2:17;
then x in L~mid(f,i1,1) \/ LSeg(mid(f,i1,1)/.len mid(f,i1,1),mid(f,
len f-'1,i2)/.1) by XBOOLE_0:def 3;
then x in L~(mid(f,i1,1)^mid(f,len f-'1,i2)) by A32,XBOOLE_0:def 3;
hence thesis by A5,XBOOLE_0:def 3;
end;
case
A45: i2<=i;
now
per cases by A36,XXREAL_0:1;
case
i+1=len f;
then i=len f-1;
then i=len f-'1 by A1,A6,XREAL_1:233,XXREAL_0:2;
hence
x in LSeg(mid(f,i1,1)/.len mid(f,i1,1), mid(f,len f-'1,i2)/.1
) \/ L~mid(f,len f-'1,i2) by A28,A29,A27,A37,XBOOLE_0:def 3;
end;
case
i+1<len f;
then i+1+1<=len f by NAT_1:13;
then i+1+1-1<=len f-1 by XREAL_1:9;
then
A46: i+1<=len f-'1 by A1,A6,XREAL_1:233,XXREAL_0:2;
then
A47: i<len f-'1 by NAT_1:13;
then len f-'1-(len f-'1-'i) =len f-'1-(len f-'1-i) by XREAL_1:233
.=i;
then
A48: len f-'1-'(len f-'1-'i)=i by XREAL_0:def 2;
i2<i+1 by A45,NAT_1:13;
then len f-'1+i2<len f-'1+(i+1) by XREAL_1:6;
then len f-'1+i2-i2<len f-'1+(i+1)-i2 by XREAL_1:9;
then len f-'1-i<len f-'1+1+i-i2-i by XREAL_1:9;
then len f-'1-i<len f-'1-i2+1;
then len f-'1-i<len f-'1-'i2+1 by A45,A47,XREAL_1:233,XXREAL_0:2;
then
A49: len f-'1-'i<len f-'1-'i2+1 by A47,XREAL_1:233;
i+1-i<=len f-'1-i by A46,XREAL_1:9;
then
A50: 1<=len f-'1-'i by NAT_D:39;
i2<len f-'1 by A45,A47,XXREAL_0:2;
then x in LSeg(mid(f,len f-'1,i2),len f-'1-'i) by A9,A23,A37,A50
,A49,A48,Th20;
then x in L~mid(f,len f-'1,i2) by SPPOL_2:17;
hence
x in LSeg(mid(f,i1,1)/.len mid(f,i1,1), mid(f,len f-'1,i2)/.1
) \/ L~mid(f,len f-'1,i2) by XBOOLE_0:def 3;
end;
end;
then x in L~mid(f,i1,1) \/ (LSeg(mid(f,i1,1)/.len mid(f,i1,1),mid(f,
len f-'1,i2)/.1) \/ L~mid(f,len f-'1,i2)) by XBOOLE_0:def 3;
then x in L~(mid(f,i1,1)^mid(f,len f-'1,i2)) by A32,XBOOLE_1:4;
hence thesis by A5,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
A51: i1+1<=len f by A6,NAT_1:13;
i2+1-i2<=len f-i2 by A11,XREAL_1:9;
then
A52: 1<=len f-'i2 by NAT_D:39;
A53: len g2 =len mid(f,i1,1) + len mid(f,len f-'1,i2) by A5,FINSEQ_1:22
.=i1-'1+1+(len f-'1-'i2+1) by A1,A6,A24,FINSEQ_6:187
.=i1+(len f-'1-'i2+1) by A1,XREAL_1:235;
then
A54: 1+1<=len g2 by A1,A19,XREAL_1:7;
A55: {f.i1} c= L~g2
proof
let x be object;
assume x in {f.i1};
then
A56: x=f.i1 by TARSKI:def 1;
g2.1 =mid(f,i1,1).1 by A5,A21,FINSEQ_1:64
.=f.i1 by A1,A6,A7,FINSEQ_6:118;
hence thesis by A54,A56,JORDAN3:1;
end;
A57: len f-'1+1=len f by A1,A6,XREAL_1:235,XXREAL_0:2;
A58: (L~g1)/\(L~g2) c= {f.i1,f.i2}
proof
let x be object;
assume
A59: x in (L~g1)/\(L~g2);
then reconsider p=x as Point of TOP-REAL 2;
x in L~g1 by A59,XBOOLE_0:def 4;
then consider i such that
A60: 1 <= i and
A61: i+1 <= len mid(f,i1,i2) and
A62: p in LSeg(mid(f,i1,i2),i) by A4,SPPOL_2:13;
A63: i<i2-'i1+1 by A10,A61,NAT_1:13;
then
A64: LSeg(mid(f,i1,i2),i)=LSeg(f,i+i1-'1) by A1,A2,A3,A60,Th19;
i+1<=i2-'i1+1 by A1,A2,A3,A9,A6,A61,FINSEQ_6:118;
then
A65: i+1-1<=i2-'i1+1-1 by XREAL_1:9;
x in L~(mid(f,i1,1)^mid(f,len f-'1,i2)) by A5,A59,XBOOLE_0:def 4;
then
A66: x in L~mid(f,i1,1) \/ LSeg(mid(f,i1,1)/.len mid(f,i1,1),mid(f,len f-'
1,i2)/.1) or x in L~mid(f,len f-'1,i2) by A32,XBOOLE_0:def 3;
now
per cases by A66,XBOOLE_0:def 3;
case
x in L~mid(f,i1,1);
then consider k such that
A67: 1 <= k and
A68: k+1 <= len mid(f,i1,1) and
A69: p in LSeg(mid(f,i1,1),k) by SPPOL_2:13;
now
per cases;
case
i1<>1;
then
A70: 1<i1 by A1,XXREAL_0:1;
then 1+1<=i1 by NAT_1:13;
then
A71: 1+1-1<=i1-1 by XREAL_1:9;
set k3=i1-'k,i3=i+i1-'1;
A72: i+i1-'1=i+i1-1 by A1,NAT_D:37;
A73: k<i1-'1+1 by A20,A68,NAT_1:13;
i1-'1+1=i1 by A1,XREAL_1:235;
then
A74: i1-'k=i1-k by A73,XREAL_1:233;
i1<=len f by A2,A3,XXREAL_0:2;
then
A75: LSeg(mid(f,i1,1),k)=LSeg(f,i1-'k) by A67,A70,A73,Th20;
then
A76: x in LSeg(f,k3)/\ LSeg(f,i3) by A62,A64,A69,XBOOLE_0:def 4;
A77: LSeg(f,k3) meets LSeg(f,i3) by A62,A64,A69,A75,XBOOLE_0:3;
1+1<=i+k by A60,A67,XREAL_1:7;
then 1<i+k by XXREAL_0:2;
then 1-k<i+k-k by XREAL_1:9;
then 1-k-1<i-1 by XREAL_1:9;
then i1+(1-k-1)<i1+(i-1) by XREAL_1:6;
then
A78: k3+1<=i3 by A74,A72,NAT_1:13;
A79: now
i<i2-i1+1 by A2,A63,XREAL_1:233;
then
A80: i+i1<i2-i1+1+i1 by XREAL_1:6;
assume k3+1<>i3;
then
A81: k3+1<i3 by A78,XXREAL_0:1;
i2+1<=len f by A3,NAT_1:13;
then i+i1-1+1<len f by A80,XXREAL_0:2;
hence contradiction by A72,A77,A81,GOBOARD5:def 4;
end;
then
A82: 1+1=i+k-1+1 by A74,A72;
A83: now
assume
A84: not(i=1 & k=1);
now
per cases by A84;
case
i<>1;
then 1<i by A60,XXREAL_0:1;
hence contradiction by A67,A82,XREAL_1:8;
end;
case
k<>1;
then 1<k by A67,XXREAL_0:1;
hence contradiction by A60,A82,XREAL_1:8;
end;
end;
hence contradiction;
end;
then
A85: i3=i1 by NAT_D:34;
k3+2=i1-'1+1+1 by A83
.=i1+1 by A1,XREAL_1:235;
then x in {f/.(k3+1)} by A51,A76,A79,A71,TOPREAL1:def 6;
then
A86: x=f/.i1 by A79,A85,TARSKI:def 1;
f/.i1=f.i1 by A1,A6,FINSEQ_4:15;
hence thesis by A86,TARSKI:def 2;
end;
case
A87: i1=1;
A88: 1+1<=k+1 by A67,XREAL_1:6;
1 <= len f by A6,A87; then
1 in dom f by FINSEQ_3:25; then
len mid(f,1,1)=1 by FINSEQ_6:193;
hence contradiction by A68,A87,A88,XXREAL_0:2;
end;
end;
hence thesis;
end;
case
A89: x in LSeg(mid(f,i1,1)/.len mid(f,i1,1),mid(f,len f-'1,i2)/.1);
i2+1-i2<=len f-i2 by A11,XREAL_1:9;
then
A90: mid(f,len f-'1,i2)/.1=mid(f,len f-'1,i2).1 by A24,A14,FINSEQ_4:15
.=f.(len f-'1) by A3,A9,A26,A23,FINSEQ_6:118
.=f/.(len f-'1) by A26,A23,FINSEQ_4:15;
mid(f,i1,1)/.len mid(f,i1,1) =mid(f,i1,1).len mid(f,i1,1) by A21,
FINSEQ_4:15
.=f.1 by A1,A6,A7,FINSEQ_6:189
.=f/.1 by A7,FINSEQ_4:15
.=f/.len f by FINSEQ_6:def 1;
then x in LSeg(f,len f-'1) by A26,A57,A89,A90,TOPREAL1:def 3;
then
A91: x in LSeg(f,i+i1-'1)/\ LSeg(f,len f-'1) by A62,A64,XBOOLE_0:def 4;
then
A92: LSeg(f,i+i1-'1) meets LSeg(f,len f-'1) by XBOOLE_0:4;
now
per cases;
case
A93: 1<i1 or 1<i;
A94: now
1+1<i+i1 by A1,A60,A93,XREAL_1:8;
then 1+1<i+i1-'1+1 by XREAL_1:235,XXREAL_0:2;
then
A95: 1+1-1<i+i1-'1+1-1 by XREAL_1:9;
assume
A96: i+i1-'1+1<len f-'1;
len f-'1<len f by A1,A6,A22,XREAL_1:235,XXREAL_0:2;
hence contradiction by A92,A96,A95,GOBOARD5:def 4;
end;
set i3=i+i1-'1;
len f-1+1<=len f;
then
A97: len f-'1+1<=len f by A1,A6,XREAL_1:233,XXREAL_0:2;
1+1<=i+i1 by A1,A60,XREAL_1:7;
then 1+1-1<=i+i1-1 by XREAL_1:9;
then
A98: 1<=i3 by A1,NAT_D:37;
i<=i2-i1 by A2,A65,XREAL_1:233;
then i+i1<=i2-i1+i1 by XREAL_1:6;
then i+i1<len f by A3,XXREAL_0:2;
then i+i1-1<len f-1 by XREAL_1:9;
then i+i1-'1<len f-1 by A1,NAT_D:37;
then i+i1-'1<len f-'1 by A1,A6,XREAL_1:233,XXREAL_0:2;
then
A99: i+i1-'1+1<=len f-'1 by NAT_1:13;
then
A100: i3+1=len f-'1 by A94,XXREAL_0:1;
A101: i+i1-'1=i+i1-1 by A1,NAT_D:37;
now
i+i1<=i2-'i1+i1 by A65,XREAL_1:6;
then
A102: i+i1<=i2-i1+i1 by A15,XREAL_0:def 2;
assume i2<len f-'1;
hence contradiction by A99,A94,A101,A102,XXREAL_0:1;
end;
then
A103: i3+1=i2 by A13,A100,XXREAL_0:1;
i+i1-'1+1=len f-'1 by A99,A94,XXREAL_0:1;
then i3+2<=len f by A97;
then x in {f/.(i3+1)} by A91,A98,A100,TOPREAL1:def 6;
then
A104: x=f/.i2 by A103,TARSKI:def 1;
f/.i2=f.i2 by A3,A9,FINSEQ_4:15;
hence thesis by A104,TARSKI:def 2;
end;
case
A105: not(1<i1 or 1<i);
then i=1 by A60,XXREAL_0:1;
then
A106: i+i1-'1=1+1-'1 by A1,A105,XXREAL_0:1
.=1 by NAT_D:34;
A107: i1=1 by A1,A105,XXREAL_0:1;
LSeg(f,1)/\ LSeg(f,len f-'1)={f.1} by Th42;
then x=f.1 by A91,A106,TARSKI:def 1;
hence thesis by A107,TARSKI:def 2;
end;
end;
hence thesis;
end;
case
x in L~mid(f,len f-'1,i2);
then consider k such that
A108: 1 <= k and
A109: k+1 <= len mid(f,len f-'1,i2) and
A110: p in LSeg(mid(f,len f-'1,i2),k) by SPPOL_2:13;
A111: k<len f-'1-'i2+1 by A24,A109,NAT_1:13;
then
A112: k<=len f-'1-'i2 by NAT_1:13;
k<len f-'i2 by A3,A14,A111,XREAL_1:233;
then k+1<=len f-'i2 by NAT_1:13;
then k+1-1<=len f-'i2-1 by XREAL_1:9;
then
A113: k<=len f-'i2-'1 by A52,XREAL_1:233;
A114: len f-'i2-'1=len f-'i2-1 by A52,XREAL_1:233
.=len f-i2-1 by A3,XREAL_1:233
.=len f-1-i2
.=len f-'1-i2 by A1,A6,XREAL_1:233,XXREAL_0:2
.=len f-'1-'i2 by A13,XREAL_1:233;
A115: k<len f-i2 by A24,A14,A109,NAT_1:13;
then k+i2<len f-i2+i2 by XREAL_1:6;
then
A116: k+i2-k<len f-k by XREAL_1:9;
then
A117: 1<len f-k by A9,XXREAL_0:2;
then 1+k<len f-k+k by XREAL_1:6;
then 1+k-1<len f-1 by XREAL_1:9;
then
A118: k<len f-'1 by A1,A6,XREAL_1:233,XXREAL_0:2;
1<len f-'k by A117,XREAL_0:def 2;
then
A119: len f-'k-'1=len f-'k-1 by XREAL_1:233
.=len f-k-1 by A116,XREAL_0:def 2
.=len f-1-k
.=len f-'1-k by A1,A6,XREAL_1:233,XXREAL_0:2
.=len f-'1-'k by A118,XREAL_1:233;
now
per cases;
case
i2<>len f-'1;
then
A120: i2<len f-'1 by A13,XXREAL_0:1;
A121: k<len f-'1-'i2+1 by A24,A109,NAT_1:13;
k+(i2-1)<len f-i2+(i2-1) by A115,XREAL_1:6;
then
A122: k+(i2-'1)<len f-1 by A1,A2,XREAL_1:233,XXREAL_0:2;
k<=k+(i2-'1) by NAT_1:11;
then
A123: k<len f-1 by A122,XXREAL_0:2;
then k+1<len f-1+1 by XREAL_1:6;
then k+1-k<len f-k by XREAL_1:9;
then
A124: 1<len f-'k by NAT_D:39;
i2+(len f-'1-i2)<len f by A1,A6,A22,XREAL_1:235,XXREAL_0:2;
then i2-i1+i1+(len f-'1-'i2)<len f by A13,XREAL_1:233;
then
A125: (i2-'i1)+i1+(len f-'1-'i2)<len f by A2,XREAL_1:233;
set k3=len f-'1-'k,i3=i+i1-'1;
A126: 1<=i2 by A1,A2,XXREAL_0:2;
i+i1<=(i2-'i1)+i1 by A65,XREAL_1:6;
then
A127: i+i1+k<=(i2-'i1)+i1+k by XREAL_1:6;
(i2-'i1)+i1+k<=(i2-'i1)+i1+(len f-'1-'i2) by A112,XREAL_1:6;
then i+i1+k<=(i2-'i1)+i1+(len f-'1-'i2) by A127,XXREAL_0:2;
then i+i1+k<len f by A125,XXREAL_0:2;
then
A128: i+i1+k-k<len f-k by XREAL_1:9;
k<len f-'1 by A1,A6,A123,XREAL_1:233,XXREAL_0:2;
then
A129: len f-'1-'k=len f-'1-k by XREAL_1:233;
len f<len f+1 by NAT_1:13;
then len f-1<len f+1-1 by XREAL_1:9;
then len f-'k=len f-k by A123,XREAL_1:233,XXREAL_0:2;
then i+i1-1<len f-'k-1 by A128,XREAL_1:9;
then i+i1-1<len f-'k-'1 by A124,XREAL_1:233;
then i+i1-'1<len f-'1-'k by A60,A119,NAT_D:37;
then
A130: i3+1<=k3 by NAT_1:13;
len f-'1<=len f by A1,A6,A22,XREAL_1:235,XXREAL_0:2;
then
A131: LSeg(mid(f,len f-'1,i2),k)=LSeg(f,len f-'1-'k) by A108,A126,A120
,A121,Th20;
then
A132: LSeg(f,i3) meets LSeg(f,k3) by A62,A64,A110,XBOOLE_0:3;
A133: now
len f-'1+1<=len f-'1+k by A108,XREAL_1:6;
then len f-'1+1-k<=len f-'1+k-k by XREAL_1:9;
then
A134: k3+1<len f by A23,A129,XXREAL_0:2;
assume not i3+1=k3;
then i3+1<k3 by A130,XXREAL_0:1;
hence contradiction by A132,A134,GOBOARD5:def 4;
end;
i+i1-'1=i+i1-1 by A1,NAT_D:37;
then
A135: len f-1-k=i1+i-1+1 by A1,A6,A129,A133,XREAL_1:233,XXREAL_0:2;
A136: now
assume
A137: not(i=i2-'i1 & k=len f-'1-'i2);
now
per cases by A137;
case
i<>i2-'i1;
then i<i2-'i1 by A65,XXREAL_0:1;
then i+k<i2-'i1+(len f-'i2-'1) by A113,XREAL_1:8;
then i+k<i2-i1+(len f-'i2-'1) by A2,XREAL_1:233;
then i+k<i2-i1+(len f-'i2-1) by A52,XREAL_1:233;
then i+k<i2-i1+(len f-i2-1) by A3,XREAL_1:233;
hence contradiction by A135;
end;
case
k<>len f-'1-'i2;
then k<len f-'1-'i2 by A112,XXREAL_0:1;
then i+k<i2-'i1+(len f-'i2-'1) by A65,A114,XREAL_1:8;
then i+k<i2-i1+(len f-'i2-'1) by A2,XREAL_1:233;
then i+k<i2-i1+(len f-'i2-1) by A52,XREAL_1:233;
then i+k<i2-i1+(len f-i2-1) by A3,XREAL_1:233;
hence contradiction by A135;
end;
end;
hence contradiction;
end;
then i3 =i2-'i1+i1-1 by A1,NAT_D:37
.=i2-i1+i1-1 by A2,XREAL_1:233
.=i2-1;
then
A138: i3+2=i2+1;
1+1<=i2 by A9,NAT_1:13;
then
A139: 1+1-1<=i2-1 by XREAL_1:9;
A140: len f-'1=len f-1 by A1,A6,XREAL_1:233,XXREAL_0:2;
len f<=len f+i2 by NAT_1:11;
then len f-'1+1<=len f+i2 by A1,A6,XREAL_1:235,XXREAL_0:2;
then len f-'1+1-i2<=len f+i2-i2 by XREAL_1:9;
then len f-'1+1-i2-1<=len f-1 by XREAL_1:9;
then len f-'1-i2<=len f-1;
then len f-'1-'i2<=len f-'1 by A12,A140,XREAL_1:233;
then
A141: k3 =len f-'1-(len f-'1-'i2) by A136,XREAL_1:233
.=len f-1-(len f-1-i2) by A12,A140,XREAL_1:233
.=i2;
x in LSeg(f,i3)/\ LSeg(f,k3) by A62,A64,A110,A131,XBOOLE_0:def 4;
then x in {f/.(i3+1)} by A11,A133,A138,A139,TOPREAL1:def 6;
then x=f/.i2 by A133,A141,TARSKI:def 1;
then x=f.i2 by A3,A9,FINSEQ_4:15;
hence thesis by TARSKI:def 2;
end;
case
A142: i2=len f-'1;
A143: 1+1<=k+1 by A108,XREAL_1:6;
1 <= i2 by A26,A142; then
i2 in dom f by A3,FINSEQ_3:25; then
len mid(f,len f-'1,len f-'1)=1 by A142,FINSEQ_6:193;
hence contradiction by A109,A142,A143,XXREAL_0:2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A144: len mid(f,i1,1)=i1 by A1,A20,XREAL_1:235;
{f.i2} c= L~g2
proof
let x be object;
assume x in {f.i2};
then
A145: x=f.i2 by TARSKI:def 1;
g2.len g2 =mid(f,len f-'1,i2).(len f-'1-'i2+1) by A5,A144,A24,A19,A53,
FINSEQ_1:65
.=f.i2 by A3,A9,A26,A23,A24,FINSEQ_6:189;
hence thesis by A54,A145,JORDAN3:1;
end;
then {f.i1} \/ {f.i2} c= L~g2 by A55,XBOOLE_1:8;
then
A146: {f.i1,f.i2} c= L~g2 by ENUMSET1:1;
{f.i2} c= L~g1
proof
let x be object;
assume x in {f.i2};
then
A147: x=f.i2 by TARSKI:def 1;
g1.len g1=f.i2 by A1,A3,A4,A9,A6,FINSEQ_6:189;
hence thesis by A16,A147,JORDAN3:1;
end;
then {f.i1} \/ {f.i2} c= L~g1 by A17,XBOOLE_1:8;
then {f.i1,f.i2} c= L~g1 by ENUMSET1:1;
then
A148: {f.i1,f.i2} c= (L~g1)/\(L~g2) by A146,XBOOLE_1:19;
L~mid(f,len f-'1,i2) c= L~f by A3,A9,A26,A23,Th35;
then
A149: L~g2 c= L~f by A5,A32,A30,XBOOLE_1:8;
L~g1 c= L~f by A1,A3,A4,A9,A6,Th35;
then (L~g1) \/ (L~g2) c= L~f by A149,XBOOLE_1:8;
hence thesis by A58,A148,A33,XBOOLE_0:def 10;
end;
theorem Th44:
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part>_of f,i1,i2 & i1<i2 holds
L~g is_S-P_arc_joining f/.i1,f/.i2
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part>_of f,i1,i2 and
A2: i1<i2;
A3: 1<=i1 by A1;
i1+1<=len f by A1;
then
A4: i1<len f by NAT_1:13;
then
A5: f/.i1=f.i1 by A3,FINSEQ_4:15;
A6: i2+1<=len f by A1;
then
A7: i2<len f by NAT_1:13;
A8: 1<=len g by A1;
then
A9: g/.len g=g.len g by FINSEQ_4:15;
A10: 1<=i2 by A1;
A11: g=mid(f,i1,i2) by A1,A2,Th25;
then g.1=f.i1 by A3,A10,A4,A7,FINSEQ_6:118;
then
A12: f/.i1=g/.1 by A8,A5,FINSEQ_4:15;
g.len g=f.i2 by A1;
then
A13: f/.i2=g/.len g by A10,A7,A9,FINSEQ_4:15;
g is being_S-Seq by A2,A11,A3,A6,Th39;
hence thesis by A12,A13,TOPREAL4:def 1;
end;
Lm1: for f being non constant standard special_circular_sequence, g being
FinSequence of TOP-REAL 2,i1,i2 being Nat st g is_a_part>_of f,i1,i2
& i1>i2 holds L~g is_S-P_arc_joining f/.i1,f/.i2
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part>_of f,i1,i2 and
A2: i1>i2;
A3: g=mid(f,i1,len f-'1)^(f|i2) by A1,A2,Th26;
set f1=mid(f,i1,len f);
A4: 1<=i1 by A1;
then
A5: i1-1=i1-'1 by XREAL_1:233;
A6: 1<=len g by A1;
then
A7: g/.len g=g.len g by FINSEQ_4:15;
A8: len g<len f by A1;
then
A9: 1<len f by A6,XXREAL_0:2;
then
A10: f.(len f)=f/.len f by FINSEQ_4:15;
A11: i1+1<=len f by A1;
then
A12: i1<len f by NAT_1:13;
then
A13: f1.len f1=f.(len f) by A4,FINSEQ_6:188;
A14: 1<=i2 by A1;
then 1<i1 by A2,XXREAL_0:2;
then
A15: f1 is being_S-Seq by A12,Th40;
A16: i2+1<=len f by A1;
then
A17: i2<len f by NAT_1:13;
then
A18: mid(f,1,i2).1=f.1 by A14,A9,FINSEQ_6:118;
Z1: f.1=f/.1 by A9,FINSEQ_4:15;
then
A19: f1.len f1=mid(f,1,i2).1 by A13,A18,A10,FINSEQ_6:def 1;
A20: len f1=len f-'i1+1 by A4,A9,A12,FINSEQ_6:118;
g.len g=f.i2 by A1;
then
A21: f/.i2=g/.len g by A14,A17,A7,FINSEQ_4:15;
len f1<len f1+1 by NAT_1:13;
then len f1-1<len f1+1-1 by XREAL_1:9;
then
A22: len f1-'1<=len f1 by A20,NAT_D:34;
i1+1-i1<=len f-i1 by A11,XREAL_1:9;
then 1<=len f-'i1 by NAT_D:39;
then
A23: 1<=len f1-'1 by A20,NAT_D:34;
i1<len f by A11,NAT_1:13;
then
A24: f/.i1=f.i1 by A4,FINSEQ_4:15;
i1+1-i1<=len f-i1 by A11,XREAL_1:9;
then 1<=len f-'i1 by NAT_D:39;
then
A25: len f-'i1-'1+1=len f-'i1-1+1 by XREAL_1:233
.=len f-i1 by A12,XREAL_1:233;
A26: L~(f|i2)= union { LSeg((f|i2),i) : 1 <= i & i+1 <= len (f|i2) } by
TOPREAL1:def 4;
A27: len f-'1<len f-'1+1 by NAT_1:13;
A28: len f-'1=len f-1 by A6,A8,XREAL_1:233,XXREAL_0:2;
then
A29: len f-'1+1=len f;
A30: i1+1-1<=len f-1 by A11,XREAL_1:9;
then
A31: 1<=len f-'1 by A4,A28,XXREAL_0:2;
then
A32: len mid(f,i1,len f-'1)=len f-'1-'i1+1 by A4,A28,A12,A30,A27,FINSEQ_6:118
.=len f-1-i1+1 by A28,A30,XREAL_1:233
.=len f-i1;
len mid(f,i1,len f-'1)=len f-'1-'i1+1 by A4,A28,A12,A30,A31,A27,FINSEQ_6:118;
then 1<=len mid(f,i1,len f-'1) by NAT_1:11;
then 1 in Seg len mid(f,i1,len f-'1);
then 1 in dom mid(f,i1,len f-'1) by FINSEQ_1:def 3;
then g.1=mid(f,i1,len f-'1).1 by A3,FINSEQ_1:def 7;
then g.1=f.i1 by A4,A28,A12,A31,A27,FINSEQ_6:118;
then
A33: f/.i1=g/.1 by A6,A24,FINSEQ_4:15;
A34: L~(f/^(i1-'1)) = union { LSeg((f/^(i1-'1)),i) : 1 <= i & i+1 <= len (f
/^(i1-'1)) } by TOPREAL1:def 4;
A35: f/.1=f/.len f by FINSEQ_6:def 1;
A36: 1+1<=len f by A9,NAT_1:13;
A38: now
per cases by A14,XXREAL_0:1;
case
A39: i2>1;
union { LSeg((f/^(i1-'1)),i) : 1 <= i & i+1 <= len (f/^(i1-'1)) }
/\ union { LSeg((f|i2),j) : 1 <= j & j+1 <= len (f|i2) } ={f.1}
proof
A40: (f|2).(1+1)=f.(1+1) by FINSEQ_3:112;
A41: (f|2).1=f.1 by FINSEQ_3:112;
A42: len (f|2)=2 by A36,FINSEQ_1:59;
then
A43: (f|2)/.1=(f|2).1 by FINSEQ_4:15;
len (f|2)-'1=2-1 by A42,NAT_D:39
.=1;
then
A44: LSeg((f|2),len (f|2)-'1) = LSeg((f|2)/.(len (f|2)-'1) ,(f|2)/.(
len (f|2)-'1+1)) by A42,TOPREAL1:def 3;
A45: len (f|i2)=i2 by A17,FINSEQ_1:59;
then
A46: 1+1<=len (f|i2) by A39,NAT_1:13;
then
A47: LSeg(f|i2,1)=LSeg((f|i2)/.1,(f|i2)/.(1+1)) by TOPREAL1:def 3;
(f|i2).1=f.1 by A14,FINSEQ_3:112;
then
A48: (f|2)/.1=(f|i2)/.1 by A14,A43,A41,A45,FINSEQ_4:15;
A49: f.1=f/.1 by A9,FINSEQ_4:15;
A50: len (f|2)-'1=1+1-'1 by A36,FINSEQ_1:59
.=1 by NAT_D:34;
then (f|2)/.(len (f|2)-'1)=f/.1 by A49,A43,FINSEQ_3:112;
then
A51: f.1 in LSeg((f|2),len (f|2)-'1) by A49,A44,RLTOPSP1:68;
A52: (f|2)/.(1+1)=(f|2).(1+1) by A42,FINSEQ_4:15;
A53: f/.len f in LSeg((f/^(i1-'1))/.(len (f/^(i1-'1))-'1), f/.len f)
by RLTOPSP1:68;
(f|i2).(1+1)=f.(1+1) by A45,A46,FINSEQ_3:112;
then
A54: (f|2)/.(1+1)=(f|i2)/.(1+1) by A46,A40,A52,FINSEQ_4:15;
A55: len (f/^(i1-'1))=len f-'(i1-'1) by RFINSEQ:29;
i1-i1<len f-i1 by A12,XREAL_1:9;
then i1-i1+1<len f-i1+1 by XREAL_1:6;
then 1<len f-(i1-1);
then 1<len f-(i1-'1) by A4,XREAL_1:233;
then
A56: 1<len (f/^(i1-'1)) by A55,NAT_D:39;
then
A57: len (f/^(i1-'1))-'1+1=len (f/^(i1-'1))-1+1 by XREAL_1:233
.=len (f/^(i1-'1));
1+1<=len (f/^(i1-'1)) by A56,NAT_1:13;
then
A58: 1+1-1<=len (f/^(i1-'1))-1 by XREAL_1:9;
then
A59: LSeg((f/^(i1-'1)),len (f/^(i1-'1))-'1) =LSeg((f/^(i1-'1))/.(len (
f/^(i1-'1))-'1) ,(f/^(i1-'1))/.(len (f/^(i1-'1))-'1+1)) by A57,TOPREAL1:def 3;
A60: LSeg((f/^(i1-'1)),len (f/^(i1-'1))-'1) in { LSeg((f/^(i1-'1)),i):
1<=i & i+1 <= len (f/^(i1-'1))} by A58,A57;
A61: i1-1<len f-1 by A12,XREAL_1:9;
then i1-1<len f by A28,A27,XXREAL_0:2;
then
A62: i1-'1<len f by A4,XREAL_1:233;
then (f/^(i1-'1))/.(len (f/^(i1-'1))-'1+1)=f/.len f by A57,
FINSEQ_6:185;
then f.1 in LSeg((f/^(i1-'1)),len (f/^(i1-'1))-'1) by A59,A53,A49,
FINSEQ_6:def 1;
then
A63: f.1 in union { LSeg((f/^(i1-'1)),i):1<=i & i+1 <= len (f/^ (i1-'
1))} by A60,TARSKI:def 4;
i1-'1<=len f-1 by A4,A61,XREAL_1:233;
then
A64: i1-'1<=len f-'1 by A6,A8,XREAL_1:233,XXREAL_0:2;
A65: union { LSeg((f/^(i1-'1)),i) : 1 <= i & i+1 <= len (f/^(i1-'1))
} /\ union { LSeg((f|i2),j) : 1 <= j & j+1 <= len (f|i2) } c= {f.1}
proof
let x be object;
assume
A66: x in union { LSeg((f/^(i1-'1)),i) : 1 <= i & i+1 <= len (f
/^(i1-'1)) } /\ union { LSeg((f|i2),j) : 1 <= j & j+1 <= len (f|i2) };
then x in union { LSeg((f/^(i1-'1)),i) : 1 <= i & i+1 <= len (f/^(
i1-'1)) } by XBOOLE_0:def 4;
then consider Y1 being set such that
A67: x in Y1 & Y1 in { LSeg(f/^(i1-'1),i):1<=i & i+1 <= len (f
/^(i1-'1))} by TARSKI:def 4;
consider j1 be Nat such that
A68: Y1=LSeg((f/^(i1-'1)),j1) and
A69: 1<=j1 and
A70: j1+1 <= len (f/^(i1-'1)) by A67;
A71: 0+1<=(i1-'1)+j1 by A69,XREAL_1:7;
j1+1<=len f-'(i1-'1) by A70,RFINSEQ:29;
then j1+1+(i1-'1)<=len f-'(i1-'1)+(i1-'1) by XREAL_1:6;
then j1+1+(i1-'1)<=len f by A62,XREAL_1:235;
then
A72: (f/^(i1-'1)).(j1+1)=f.((i1-'1)+j1+1) by FINSEQ_6:114,NAT_1:11;
j1 <= len (f/^(i1-'1)) by A70,NAT_1:13;
then
A73: (f/^(i1-'1))/.j1=(f/^(i1-'1)).j1 by A69,FINSEQ_4:15;
j1+1+(i1-'1)<=len f-'(i1-'1)+(i1-'1) by A55,A70,XREAL_1:6;
then
A74: j1+1+(i1-'1)<=len f by A62,XREAL_1:235;
A75: LSeg(f/^(i1-'1),j1)=LSeg((f/^(i1-'1))/.j1,(f/^(i1-'1))/.(j1+1)
) by A69,A70,TOPREAL1:def 3;
A76: (f/^(i1-'1))/.(j1+1)=(f/^(i1-'1)).(j1+1) by A70,FINSEQ_4:15,NAT_1:11;
(i1-'1)+j1<=(i1-'1)+j1+1 by NAT_1:11;
then
A77: j1+(i1-'1)<=len f by A74,XXREAL_0:2;
then (f/^(i1-'1)).j1=f.((i1-'1)+j1) by A69,FINSEQ_6:114;
then
A78: (f/^(i1-'1))/.j1=f/.((i1-'1)+j1) by A71,A73,A77,FINSEQ_4:15;
LSeg(f,(i1-'1)+j1)=LSeg(f/.((i1-'1)+j1),f/.((i1-'1)+j1 +1)) by A71
,A74,TOPREAL1:def 3;
then
A79: LSeg(f/^(i1-'1),j1)=LSeg(f,(i1-'1)+j1) by A75,A74,A78,A72,A76,
FINSEQ_4:15,NAT_1:11;
x in union { LSeg((f|i2),j) : 1 <= j & j+1 <= len (f|i2) } by A66,
XBOOLE_0:def 4;
then consider Y2 being set such that
A80: x in Y2 & Y2 in { LSeg(f|i2,i):1<=i & i+1 <= len (f|i2)}
by TARSKI:def 4;
consider j2 be Nat such that
A81: Y2=LSeg((f|i2),j2) and
A82: 1<=j2 and
A83: j2+1 <= len (f|i2) by A80;
A84: len (f|i2)<=len f by FINSEQ_5:16;
then
A85: j2+1<=len f by A83,XXREAL_0:2;
A86: j2+1<=len f by A83,A84,XXREAL_0:2;
A87: (f|i2)/.(j2+1)=(f|i2).(j2+1) by A83,FINSEQ_4:15,NAT_1:11
.=f.(j2+1) by A45,A83,FINSEQ_3:112
.=f/.(j2+1) by A86,FINSEQ_4:15,NAT_1:11;
A88: LSeg(f|i2,j2)=LSeg((f|i2)/.j2, (f|i2)/.(j2+1)) by A82,A83,
TOPREAL1:def 3;
A89: j2<len (f|i2) by A83,NAT_1:13;
then
A90: j2<len f by A84,XXREAL_0:2;
(f|i2)/.j2=(f|i2).j2 by A82,A89,FINSEQ_4:15
.= f.j2 by A45,A89,FINSEQ_3:112
.= f/.j2 by A82,A90,FINSEQ_4:15;
then
A91: LSeg(f|i2,j2)=LSeg(f,j2) by A82,A87,A88,A85,TOPREAL1:def 3;
A92: now
len (f/^(i1-'1))=len f-(i1-'1) by A12,A55,NAT_D:44,XREAL_1:233;
then
A93: j1+1+(i1-'1) <= len f-(i1-'1)+(i1-'1) by A70,XREAL_1:6;
then (i1-'1)+j1+1 <= len f;
then
A94: (i1-'1)+j1<len f by NAT_1:13;
A95: i2+1<=i1 by A2,NAT_1:13;
assume
A96: not (j2=1 & i1-'1+j1=len f-'1);
A97: i1-'1+1<=i1-'1+j1 by A69,XREAL_1:6;
A98: i1-'1+1=i1 by A4,XREAL_1:235;
j2+1<i2+1 by A45,A83,NAT_1:13;
then j2+1<i1-'1+1 by A95,A98,XXREAL_0:2;
then
A99: j2+1<(i1-'1)+j1 by A97,XXREAL_0:2;
A100: (i1-'1)+j1+1-1 <= len f-1 by A93,XREAL_1:9;
now
per cases by A28,A82,A96,A100,XXREAL_0:1;
case
j2>1;
then LSeg(f,(i1-'1)+j1) misses LSeg(f,j2) by A99,A94,
GOBOARD5:def 4;
hence LSeg(f,(i1-'1)+j1) /\ LSeg(f,j2)={} by XBOOLE_0:def 7;
end;
case
(i1-'1)+j1 < len f-'1;
then (i1-'1)+j1+1 < len f-'1+1 by XREAL_1:6;
then LSeg(f,(i1-'1)+j1) misses LSeg(f,j2) by A28,A99,
GOBOARD5:def 4;
hence LSeg(f,(i1-'1)+j1) /\ LSeg(f,j2)={} by XBOOLE_0:def 7;
end;
end;
hence contradiction by A67,A68,A80,A81,A79,A91,XBOOLE_0:def 4;
end;
then
A101: LSeg((f|i2),j2) = LSeg(f,1) by A46,SPPOL_2:3;
len f-'1-(i1-'1)+(i1-'1)<=len f by A28,A27;
then
A102: len f-'1-'(i1-'1)+(i1-'1)<=len f by A64,XREAL_1:233;
A103: len f-'1-'(i1-'1)+1+(i1-'1)= len f-'1-(i1-'1)+1+(i1-'1) by A64,
XREAL_1:233
.=len f-'1+1
.=len f-1+1 by A6,A8,XREAL_1:233,XXREAL_0:2
.=len f;
A104: len (f/^(i1-'1))=len f-(i1-'1) by A12,A55,NAT_D:44,XREAL_1:233;
len f-'1-(i1-'1)<len f-(i1-'1) by A28,A27,XREAL_1:9;
then
A105: len f-'1-'(i1-'1)<len (f/^(i1-'1)) by A64,A104,XREAL_1:233;
then
A106: len f-'1-'(i1-'1)+1<=len (f/^(i1-'1)) by NAT_1:13;
i1+1-1<=len f-1 by A11,XREAL_1:9;
then
A107: i1-(i1-1)<=len f-1-(i1-1) by XREAL_1:9;
then
A108: 1<=len f-'1-'(i1-'1) by A28,A5,NAT_D:39;
then
A109: (f/^(i1-'1))/.(len f-'1-'(i1-'1))=(f/^(i1-'1)).(len f -'1-'(i1
-'1)) by A105,FINSEQ_4:15
.=f.(len f-'1-'(i1-'1)+(i1-'1)) by A102,A108,FINSEQ_6:114
.=f.(len f-'1-(i1-'1)+(i1-'1)) by A64,XREAL_1:233
.=f/.(len f-'1) by A28,A31,A27,FINSEQ_4:15;
A110: 1<len f-'1-'(i1-'1)+1 by A108,NAT_1:13;
then
A111: (f/^(i1-'1))/.(len f-'1-'(i1-'1)+1) =(f/^(i1-'1)).(len f-'1-'(
i1-'1)+1) by A106,FINSEQ_4:15
.=f.(1+((len f-'1-'(i1-'1))+(i1-'1))) by A103,A110,FINSEQ_6:114
.=f.(len f-'1-(i1-'1)+(i1-'1)+1) by A64,XREAL_1:233
.=f.len f by A6,A8,XREAL_1:235,XXREAL_0:2
.=f/.len f by A9,FINSEQ_4:15;
A112: 1<=len f-'1-'(i1-'1) by A28,A5,A107,NAT_D:39;
j1=len f-'1-(i1-'1) by A92
.=len f-'1-'(i1-'1) by A64,XREAL_1:233;
then LSeg(f/^(i1-'1),j1) =LSeg((f/^(i1-'1))/.(len f-'1-'(i1-'1)), (
f/^(i1-'1))/.(len f-'1-'(i1-'1)+1)) by A112,A106,TOPREAL1:def 3
.=LSeg(f,len f-'1) by A29,A31,A109,A111,TOPREAL1:def 3;
then LSeg((f/^(i1-'1)),j1) /\ LSeg((f|i2),j2) ={f.1} by A101,Th42;
hence thesis by A67,A68,A80,A81,XBOOLE_0:def 4;
end;
1+1<=len (f|i2) by A39,A45,NAT_1:13;
then LSeg((f|2),len (f|2)-'1) in { LSeg((f|i2),i) : 1<=i & i+1 <= len
(f|i2) } by A44,A50,A48,A54,A47;
then
f.1 in union { LSeg(f|i2,j) : 1 <= j & j+1 <= len (f|i2) } by A51,
TARSKI:def 4;
then
f.1 in union { LSeg((f/^(i1-'1)),i):1<=i & i+1 <= len (f/^(i1-'1)
) } /\ union { LSeg((f|i2),j) : 1 <= j & j+1 <= len (f|i2)} by A63,
XBOOLE_0:def 4;
then {f.1} c= union { LSeg((f/^(i1-'1)),i):1<=i & i+1 <= len (f /^(i1
-'1)) } /\ union { LSeg((f|i2),j) : 1 <= j & j+1 <= len (f|i2) } by
ZFMISC_1:31;
hence thesis by A65,XBOOLE_0:def 10;
end;
then L~(f/^(i1-'1)) /\ L~mid(f,1,i2) ={f.1} by A14,A34,A26,FINSEQ_6:116;
then
A113: L~f1 /\ L~mid(f,1,i2)={mid(f,1,i2).1} by A12,A18,FINSEQ_6:117;
mid(f,1,i2) is being_S-Seq by A16,A39,Th39;
hence mid(f1,1,len f1-'1)^mid(f,1,i2) is being_S-Seq by A15,A19,A113,
JORDAN3:45;
end;
case
i2=1;
then
A114: mid(f,1,i2)=f|1 by FINSEQ_6:116
.=<*f.1*> by FINSEQ_5:20;
A115: mid(f1,1,len f1-'1)=f1|(len f1-'1) by A23,FINSEQ_6:116;
A116: len f1-'1+1=len f1 by A20,NAT_D:34;
1 <= len f1 by A20,NAT_1:11; then
len f1 in dom f1 by FINSEQ_3:25; then
Z: f1/.len f1 = f1.len f1 by PARTFUN1:def 6;
<*f.1*>=<*f1.len f1*> by Z1,A13,A10,A35;
hence mid(f1,1,len f1-'1)^mid(f,1,i2) is being_S-Seq
by Z,A15,A114,A115,A116,FINSEQ_5:21;
end;
end;
A117: 1<=len f1 by A20,NAT_1:11;
then len mid(f1,1,len f1-'1)=len f1-'1-'1+1 by A23,A22,FINSEQ_6:118
.=len f-'i1+1-'1-'1+1 by A4,A9,A12,FINSEQ_6:118;
then
A118: len mid(f1,1,len f1-'1)=len mid(f,i1,len f-'1) by A25,A32,NAT_D:34;
for k be Nat st 1<=k & k<=len mid(f,i1,len f-'1) holds mid(f1,1,len f1
-'1).k=mid(f,i1,len f-'1).k
proof
A119: len mid(f,i1,len f)=len f-'i1+1 by A4,A9,A12,FINSEQ_6:118;
let k be Nat;
assume that
A120: 1<=k and
A121: k<=len mid(f,i1,len f-'1);
k<=len f-'i1 by A12,A32,A121,XREAL_1:233;
then
A122: k<len mid(f,i1,len f) by A119,NAT_1:13;
mid(f1,1,len f1-'1).k=f1.(k+1-'1) by A117,A23,A22,A118,A120,A121,
FINSEQ_6:118
.=f1.k by NAT_D:34
.=f.(k+i1-'1) by A4,A9,A12,A120,A122,FINSEQ_6:118;
hence thesis by A4,A28,A12,A30,A31,A27,A120,A121,FINSEQ_6:118;
end;
then mid(f1,1,len f1-'1)=mid(f,i1,len f-'1) by A118,FINSEQ_1:14;
then g is being_S-Seq by A1,A2,A38,Th26;
hence thesis by A33,A21,TOPREAL4:def 1;
end;
theorem
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part<_of f,i1,i2 & i1>i2 holds
L~g is_S-P_arc_joining f/.i1,f/.i2
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part<_of f,i1,i2 and
A2: i1>i2;
reconsider P=L~g as Subset of TOP-REAL 2;
reconsider p2=f/.i2,p1=f/.i1 as Point of TOP-REAL 2;
L~Rev g is_S-P_arc_joining f/.i2,f/.i1 by A1,A2,Th30,Th44;
then P is_S-P_arc_joining p2,p1 by SPPOL_2:22;
hence thesis by SPPOL_2:49;
end;
theorem Th46:
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part>_of f,i1,i2 & i1<>i2 holds
L~g is_S-P_arc_joining f/.i1,f/.i2
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part>_of f,i1,i2 and
A2: i1<>i2;
now
per cases;
case
i1<i2;
hence thesis by A1,Th44;
end;
case
i1>=i2;
then i1>i2 by A2,XXREAL_0:1;
hence thesis by A1,Lm1;
end;
end;
hence thesis;
end;
theorem Th47:
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part<_of f,i1,i2 & i1<>i2 holds
L~g is_S-P_arc_joining f/.i1,f/.i2
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part<_of f,i1,i2 and
A2: i1<>i2;
now
per cases;
case
A3: i1>i2;
reconsider P=L~g as Subset of TOP-REAL 2;
reconsider p2=f/.i2,p1=f/.i1 as Point of TOP-REAL 2;
L~Rev g is_S-P_arc_joining f/.i2,f/.i1 by A1,A3,Th30,Th44;
then P is_S-P_arc_joining p2,p1 by SPPOL_2:22;
hence thesis by SPPOL_2:49;
end;
case
A4: i1<=i2;
reconsider P=L~g as Subset of TOP-REAL 2;
reconsider p2=f/.i2,p1=f/.i1 as Point of TOP-REAL 2;
i1<i2 by A2,A4,XXREAL_0:1;
then L~(Rev g) is_S-P_arc_joining f/.i2,f/.i1 by A1,Lm1,Th30;
then P is_S-P_arc_joining p2,p1 by SPPOL_2:22;
hence thesis by SPPOL_2:49;
end;
end;
hence thesis;
end;
theorem Th48:
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part_of f,i1,i2 & i1<>i2 holds
L~g is_S-P_arc_joining f/.i1,f/.i2
proof
let f be non constant standard special_circular_sequence, g be FinSequence
of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part_of f,i1,i2 and
A2: i1<>i2;
now
per cases by A1;
case
g is_a_part>_of f,i1,i2;
hence thesis by A2,Th46;
end;
case
g is_a_part<_of f,i1,i2;
hence thesis by A2,Th47;
end;
end;
hence thesis;
end;
theorem
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part_of f,i1,i2 & g.1<>g.len g holds
L~g is_S-P_arc_joining f/.i1,f/.i2
proof
let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
assume that
A1: g is_a_part_of f,i1,i2 and
A2: g.1<>g.len g;
now
per cases by A1;
case
A3: g is_a_part>_of f,i1,i2;
then i1+1<=len f;
then
A4: i1+1-1<=len f-1 by XREAL_1:9;
A5: 1<=i1 by A3;
A6: 1<=len g by A3;
len g<len f by A3;
then
A7: i1<=len f-'1 by A6,A4,XREAL_1:233,XXREAL_0:2;
now
assume
A8: i1=i2;
g.1=f.S_Drop((i1+1)-'1,f) by A3
.=f.S_Drop(i1,f) by NAT_D:34
.=f.i1 by A5,A7,Th22;
hence contradiction by A2,A3,A8;
end;
hence thesis by A1,Th48;
end;
case
A9: g is_a_part<_of f,i1,i2;
then
A10: 1<=i1;
A11: 1<=len g by A9;
A12: len g<len f by A9;
i1+1<=len f by A9;
then i1+1-1<=len f-1 by XREAL_1:9;
then
A13: i1<=len f-'1 by A11,A12,XREAL_1:233,XXREAL_0:2;
now
assume
A14: i1=i2;
g.1=f.S_Drop(len f+i1-'1,f) by A9
.=f.S_Drop(len f-'1+1+i1-'1,f) by A11,A12,XREAL_1:235,XXREAL_0:2
.=f.S_Drop(len f-'1+i1+1-'1,f)
.=f.S_Drop(len f-'1+i1,f) by NAT_D:34
.=f.S_Drop(i1,f) by Th23
.=f.i1 by A10,A13,Th22;
hence contradiction by A2,A9,A14;
end;
hence thesis by A1,Th48;
end;
end;
hence thesis;
end;
theorem Th50:
for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f & i1<>i2
ex g1,g2 being FinSequence of TOP-REAL 2 st g1 is_a_part_of f,i1,i2 &
g2 is_a_part_of f,i1,i2 &
(L~g1)/\(L~g2)={f.i1,f.i2} & (L~g1) \/ (L~g2)=L~f &
L~g1 is_S-P_arc_joining f/.i1,f/.i2 & L~g2 is_S-P_arc_joining f/.i1,f/.i2 &
for g being FinSequence of TOP-REAL 2 st g is_a_part_of f,i1,i2 holds
g=g1 or g=g2
proof
let f be non constant standard special_circular_sequence, i1,i2 be Nat;
assume that
A1: 1<=i1 and
A2: i1+1<=len f and
A3: 1<=i2 and
A4: i2+1<=len f and
A5: i1<>i2;
now
per cases;
case
A6: i1<=i2;
set h1=mid(f,i1,i2),h2=mid(f,i1,1)^mid(f,len f-'1,i2);
A7: i2<len f by A4,NAT_1:13;
then
A8: mid(f,i1,i2) is_a_part>_of f,i1,i2 by A1,A6,Th31;
then
A9: h1 is_a_part_of f,i1,i2;
A10: i1<i2 by A5,A6,XXREAL_0:1;
then
A11: L~h1 is_S-P_arc_joining f/.i1,f/.i2 by A8,Th44;
A12: for g being FinSequence of TOP-REAL 2 st g is_a_part_of f,i1,i2
holds g=h1 or g=h2
proof
let g be FinSequence of TOP-REAL 2;
assume
A13: g is_a_part_of f,i1,i2;
now
per cases by A13;
case
g is_a_part>_of f,i1,i2;
hence thesis by A6,Th25;
end;
case
g is_a_part<_of f,i1,i2;
hence thesis by A10,Th28;
end;
end;
hence thesis;
end;
A14: (L~h1) \/ (L~h2)=L~f by A1,A10,A7,Th43;
A15: (L~h1)/\(L~h2)={f.i1,f.i2} by A1,A10,A7,Th43;
mid(f,i1,1)^mid(f,len f-'1,i2) is_a_part<_of f,i1,i2 by A1,A10,A7,Th34;
then
A16: h2 is_a_part_of f,i1,i2;
then L~h2 is_S-P_arc_joining f/.i1,f/.i2 by A5,Th48;
hence thesis by A9,A16,A15,A14,A11,A12;
end;
case
A17: i1>i2;
set h1=mid(f,i2,i1),h2=mid(f,i2,1)^mid(f,len f-'1,i1);
set h3=Rev h1,h4=Rev h2;
A18: L~h1=L~h3 by SPPOL_2:22;
A19: for g being FinSequence of TOP-REAL 2 st g is_a_part_of f,i1,i2
holds g=h3 or g=h4
proof
let g be FinSequence of TOP-REAL 2;
assume
A20: g is_a_part_of f,i1,i2;
now
per cases by A20;
case
g is_a_part>_of f,i1,i2;
then Rev g is_a_part<_of f,i2,i1 by Th29;
then Rev g= mid(f,i2,1)^mid(f,len f-'1,i1) by A17,Th28;
hence thesis;
end;
case
g is_a_part<_of f,i1,i2;
then Rev g is_a_part>_of f,i2,i1 by Th30;
then Rev g= mid(f,i2,i1) by A17,Th25;
hence thesis;
end;
end;
hence thesis;
end;
A21: i1<len f by A2,NAT_1:13;
then mid(f,i2,i1) is_a_part>_of f,i2,i1 by A3,A17,Th31;
then
A22: L~h3 is_S-P_arc_joining f/.i1,f/.i2 by A17,Th29,Th47;
(L~h1) \/ (L~h2)=L~f by A3,A17,A21,Th43;
then
A23: (L~h3) \/ (L~h4)=L~f by A18,SPPOL_2:22;
(L~h1)/\(L~h2)={f.i2,f.i1} by A3,A17,A21,Th43;
then
A24: (L~h3)/\(L~h4)={f.i1,f.i2} by A18,SPPOL_2:22;
Rev mid(f,i2,i1) is_a_part<_of f,i1,i2 by A3,A17,A21,Th29,Th31;
then
A25: h3 is_a_part_of f,i1,i2;
Rev (mid(f,i2,1)^mid(f,len f-'1,i1)) is_a_part>_of f,i1,i2 by A3,A17,A21
,Th30,Th34;
then
A26: h4 is_a_part_of f,i1,i2;
then L~h4 is_S-P_arc_joining f/.i1,f/.i2 by A5,Th48;
hence thesis by A25,A26,A24,A23,A22,A19;
end;
end;
hence thesis;
end;
reserve g, g1, g2 for FinSequence of TOP-REAL 2;
theorem
for f being non constant standard special_circular_sequence,
P being non empty Subset of TOP-REAL 2 st
P = L~f holds P is being_simple_closed_curve
proof
set i1=1,i2=1+1;
let f be non constant standard special_circular_sequence,
P be non empty Subset of TOP-REAL 2 such that
A1: P = L~f;
A2: 1+1<len f by GOBOARD7:34,XXREAL_0:2;
then
A3: f/.i1<>f/.i2 by GOBOARD7:36;
1+1+1<=len f by GOBOARD7:34,XXREAL_0:2;
then consider g1,g2 being FinSequence of TOP-REAL 2 such that
g1 is_a_part_of f,i1,i2 and
g2 is_a_part_of f,i1,i2 and
A4: (L~g1)/\(L~g2)={f.i1,f.i2} and
A5: (L~g1) \/ (L~g2)=L~f and
A6: L~g1 is_S-P_arc_joining f/.i1,f/.i2 and
A7: L~g2 is_S-P_arc_joining f/.i1,f/.i2 and
for g being FinSequence of TOP-REAL 2 st g is_a_part_of f,i1,i2 holds g=
g1 or g=g2 by A2,Th50;
reconsider L1 = L~g1, L2 = L~g2 as non empty Subset of TOP-REAL 2 by A4;
A8: L2 is_an_arc_of f/.i1,f/.i2 by A7,TOPREAL4:2;
1<=len f by GOBOARD7:34,XXREAL_0:2;
then
A9: f.i1=f/.i1 by FINSEQ_4:15;
then f/.i1 in (L~g1)/\(L~g2) by A4,TARSKI:def 2;
then f/.i1 in (L~g1) by XBOOLE_0:def 4;
then
A10: f/.i1 in P by A1,A5,XBOOLE_0:def 3;
A11: f.i2=f/.i2 by A2,FINSEQ_4:15;
then f/.i2 in (L~g1)/\(L~g2) by A4,TARSKI:def 2;
then f/.i2 in (L~g2) by XBOOLE_0:def 4;
then
A12: f/.i2 in P by A1,A5,XBOOLE_0:def 3;
L1 is_an_arc_of f/.i1,f/.i2 by A6,TOPREAL4:2;
hence thesis by A1,A4,A5,A8,A9,A11,A3,A10,A12,TOPREAL2:6;
end;
theorem Th52:
for f being non constant standard special_circular_sequence,
g1,g2 st g1 is_a_part>_of f,i1,i2 & g2 is_a_part>_of f,i1,i2 holds
g1=g2
proof
let f be non constant standard special_circular_sequence, g1,g2;
assume that
A1: g1 is_a_part>_of f,i1,i2 and
A2: g2 is_a_part>_of f,i1,i2;
now
per cases;
case
A3: i1<=i2;
then g1=mid(f,i1,i2) by A1,Th25;
hence thesis by A2,A3,Th25;
end;
case
A4: i1>i2;
then g1=mid(f,i1,len f-'1)^mid(f,1,i2) by A1,Th26;
hence thesis by A2,A4,Th26;
end;
end;
hence thesis;
end;
theorem Th53:
for f being non constant standard special_circular_sequence,
g1,g2 st g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds
g1=g2
proof
let f be non constant standard special_circular_sequence, g1,g2;
assume that
A1: g1 is_a_part<_of f,i1,i2 and
A2: g2 is_a_part<_of f,i1,i2;
per cases;
suppose
A3: i1>=i2;
then g1=mid(f,i1,i2) by A1,Th27;
hence thesis by A2,A3,Th27;
end;
suppose
A4: i1<i2;
then g1=mid(f,i1,1)^mid(f,len f-'1,i2) by A1,Th28;
hence thesis by A2,A4,Th28;
end;
end;
theorem Th54:
for f being non constant standard special_circular_sequence,
g1,g2 st i1<>i2 &
g1 is_a_part>_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds
g1.2<>g2.2
proof
let f be non constant standard special_circular_sequence, g1,g2;
assume that
A1: i1<>i2 and
A2: g1 is_a_part>_of f,i1,i2 and
A3: g2 is_a_part<_of f,i1,i2;
A4: 1<=i1 by A2;
A5: i2+1<=len f by A2;
then
A6: i2<len f by NAT_1:13;
A7: len f-'1<len f-'1+1 by NAT_1:13;
A8: 1<=i2 by A2;
A9: i1+1<=len f by A2;
then
A10: i1<len f by NAT_1:13;
A11: 1<=1+i1 by NAT_1:11;
then
A12: len f-'1=len f-1 by A9,XREAL_1:233,XXREAL_0:2;
A13: 1<=len f by A9,A11,XXREAL_0:2;
now
per cases;
case
A14: i1<=i2;
now
per cases by A14,XXREAL_0:1;
case
i1=i2;
hence contradiction by A1;
end;
case
A15: i1<i2;
A16: len mid(f,i1,1)=i1-'1+1 by A4,A10,FINSEQ_6:187;
i1+1-1<=len f-1 by A9,XREAL_1:9;
then
A17: 1<=len f-'1 by A4,A12,XXREAL_0:2;
A18: g2=mid(f,i1,1)^mid(f,len f-'1,i2) by A3,A15,Th28;
now
per cases by A4,XXREAL_0:1;
case
A19: 1<i1;
then 1+1<=i1-1+1 by NAT_1:13;
then
A20: 2<=len mid(f,i1,1) by A4,A16,XREAL_1:233;
A21: 1+1<=i1 by A19,NAT_1:13;
A22: g2.2=(mid(f,i1,1)^mid(f,len f-'1,i2)).2 by A3,A15,Th28
.=mid(f,i1,1).2 by A20,FINSEQ_1:64
.=f.(i1-'2+1) by A13,A10,A19,A20,FINSEQ_6:118
.=f.(i1-(1+1)+1) by A21,XREAL_1:233
.=f.(i1-1)
.=f.(i1-'1) by A4,XREAL_1:233;
1+1<=i1 by A19,NAT_1:13;
then
A23: 1+1-1<=i1-1 by XREAL_1:9;
then
A24: 1<=i1-'1 by NAT_D:39;
i1+1<=i2 by A15,NAT_1:13;
then 1+i1-i1<=i2-i1 by XREAL_1:9;
then 1<=i2-'i1 by NAT_D:39;
then 1+1<=i2-'i1+1 by XREAL_1:6;
then
A25: 2<=len mid(f,i1,i2) by A4,A8,A6,A10,A15,FINSEQ_6:118;
A26: g1.2=mid(f,i1,i2).2 by A2,A15,Th25
.=f.(2+i1-'1) by A4,A8,A6,A10,A15,A25,FINSEQ_6:118
.=f.(1+1+i1-1) by NAT_D:37
.=f.(i1+1);
A27: now
assume that
A28: 1=i1-'1 and
A29: i1+1=len f;
1=i1-1 by A28,NAT_D:39;
hence contradiction by A29,GOBOARD7:34;
end;
now
per cases by A27;
case
A30: 1<>i1-'1;
A31: 1<i1+1 by A4,NAT_1:13;
i1-'1<i1-'1+1 by NAT_1:13;
then i1-'1<i1 by A4,XREAL_1:235;
then
A32: i1-'1<i1+1 by NAT_1:13;
A33: i1+1<=len f by A2;
then i1-'1<len f by A32,XXREAL_0:2;
then
A34: f.(i1-'1)=f/.(i1-'1) by A24,FINSEQ_4:15;
1<i1-'1 by A24,A30,XXREAL_0:1;
then f/.(i1-'1)<>f/.(i1+1) by A32,A33,GOBOARD7:37;
hence thesis by A9,A22,A26,A34,A31,FINSEQ_4:15;
end;
case
A35: i1+1<>len f;
A36: 1<=i1-'1 by A23,NAT_D:39;
i1-'1<i1-'1+1 by NAT_1:13;
then i1-'1<i1 by A4,XREAL_1:235;
then
A37: i1-'1<i1+1 by NAT_1:13;
then i1-'1<len f by A9,XXREAL_0:2;
then
A38: f.(i1-'1)=f/.(i1-'1) by A36,FINSEQ_4:15;
A39: 1<i1+1 by A4,NAT_1:13;
i1+1<len f by A9,A35,XXREAL_0:1;
then f/.(i1-'1)<>f/.(i1+1) by A36,A37,GOBOARD7:36;
hence thesis by A9,A22,A26,A38,A39,FINSEQ_4:15;
end;
end;
hence thesis;
end;
case
A40: 1=i1;
len f>4 by GOBOARD7:34;
then len f-1>3+1-1 by XREAL_1:9;
then i1+1<len f-'1 by A12,A40,XXREAL_0:2;
then
A41: f/.(i1+1)<>f/.(len f-'1) by A12,A7,A40,GOBOARD7:37;
i1+1<=i2 by A15,NAT_1:13;
then 1+i1-i1<=i2-i1 by XREAL_1:9;
then 1<=i2-'i1 by NAT_D:39;
then 1+1<=i2-'i1+1 by XREAL_1:6;
then
A42: 2<=len mid(f,i1,i2) by A4,A8,A6,A10,A15,FINSEQ_6:118;
A43: f.(len f-'1)=f/.(len f-'1) by A12,A7,A17,FINSEQ_4:15;
A44: len mid(f,i1,1)=i1-'1+1 by A4,A10,FINSEQ_6:187
.=0+1 by A40,XREAL_1:232
.=1;
i2+1+1<=len f+1 by A5,XREAL_1:6;
then
A45: 1+i2+1-i2<=len f+1-i2 by XREAL_1:9;
A46: len mid(f,i1,1)=i1-'1+1 by A4,A10,FINSEQ_6:187
.=0+1 by A40,XREAL_1:232
.=1;
len g2=len f+i1-'i2 by A3,A15,Th28
.=len f+1-i2 by A6,A40,NAT_D:37;
then
A47: g2
.2 =mid(f,len f-'1,i2).(2-len mid(f,i1,1)) by A18,A44,A45,FINSEQ_6:108
.=f.(len f-'1) by A8,A12,A7,A6,A17,A46,FINSEQ_6:118;
A48: 1<i1+1 by A4,NAT_1:13;
g1.2=mid(f,i1,i2).2 by A2,A15,Th25
.=f.(2+i1-'1) by A4,A8,A6,A10,A15,A42,FINSEQ_6:118
.=f.(1+1+i1-1) by NAT_D:37
.=f.(i1+1);
hence thesis by A9,A47,A41,A43,A48,FINSEQ_4:15;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
A49: i1>i2;
then i2+1<=i1 by NAT_1:13;
then 1+i2-i2<=i1-i2 by XREAL_1:9;
then 1<=i1-'i2 by NAT_D:39;
then 1+1<=i1-'i2+1 by XREAL_1:6;
then
A50: 2<=len mid(f,i1,i2) by A4,A8,A6,A10,A49,FINSEQ_6:118;
1<i1 by A8,A49,XXREAL_0:2;
then
A51: 1+1<=i1 by NAT_1:13;
A52: g2.2=mid(f,i1,i2).2 by A3,A49,Th27
.=f.(i1-'2+1) by A4,A8,A6,A10,A49,A50,FINSEQ_6:118
.=f.(i1-(1+1)+1) by A51,XREAL_1:233
.=f.(i1-1)
.=f.(i1-'1) by A4,XREAL_1:233;
1<i1 by A8,A49,XXREAL_0:2;
then 1+1<=i1 by NAT_1:13;
then
A53: 1+1-1<=i1-1 by XREAL_1:9;
then
A54: 1<=i1-'1 by NAT_D:39;
A55: i1+1-1<=len f-1 by A9,XREAL_1:9;
then 1<=len f-'1 by A4,A12,XXREAL_0:2;
then
A56: len mid(f,i1,len f-'1)=len f-'1-'i1+1 by A4,A12,A7,A10,A55,FINSEQ_6:118;
A57: i1+1-1<=len f-1 by A9,XREAL_1:9;
A58: g1=mid(f,i1,len f-'1)^mid(f,1,i2) by A2,A49,Th26;
A59: now
per cases by A55,XXREAL_0:1;
case
i1<len f-1;
then i1+1<=len f-'1 by A12,NAT_1:13;
then
A60: 1+(i1+1)<=1+(len f-'1) by XREAL_1:6;
then
A61: 1+(i1+1)-i1<=1+(len f-'1)-i1 by XREAL_1:9;
1+1+i1-i1<=1+(len f-'1)-i1 by A60,XREAL_1:9;
then 1+1<=1+((len f-'1)-i1);
then
A62: 2<=len mid(f,i1,len f-'1) by A12,A56,A57,XREAL_1:233;
thus g1.2=(mid(f,i1,len f-'1)^mid(f,1,i2)).2 by A2,A49,Th26
.=mid(f,i1,len f-'1).2 by A62,FINSEQ_1:64
.=f.(1+1+i1-1) by A4,A12,A7,A57,A61,FINSEQ_6:122
.=f.(i1+1);
end;
case
A63: i1=len f-1;
then
A64: len mid(f,i1,len f-'1)=len f-'1-'(len f-'1)+1 by A4,A12,A7,
FINSEQ_6:118
.=0+1 by XREAL_1:232
.=1;
A65: 1+1<=i2+1 by A8,XREAL_1:6;
A66: len mid(f,i1,len f-'1)=len f-'1-'(len f-'1)+1 by A4,A12,A7,A63,
FINSEQ_6:118
.=0+1 by XREAL_1:232
.=1;
len g1=len f-'1+1+i2-'(len f-'1) by A2,A12,A49,A63,Th26
.=len f-'1+(1+i2)-'(len f-'1)
.=1+i2 by NAT_D:34;
hence g1.2 =mid(f,1,i2).(2-len mid(f,i1,len f-'1)) by A58,A64,A65,
FINSEQ_6:108
.=f.1 by A8,A13,A6,A66,FINSEQ_6:118
.=f.(i1+1) by A63,FINSEQ_6:184,NAT_1:11;
end;
end;
A67: now
assume that
A68: 1=i1-'1 and
A69: i1+1=len f;
1=i1-1 by A68,NAT_D:39;
hence contradiction by A69,GOBOARD7:34;
end;
now
per cases by A67;
case
A70: 1<>i1-'1;
A71: 1<i1+1 by A4,NAT_1:13;
i1-'1<i1-'1+1 by NAT_1:13;
then i1-'1<i1 by A4,XREAL_1:235;
then
A72: i1-'1<i1+1 by NAT_1:13;
A73: i1+1<=len f by A2;
then i1-'1<len f by A72,XXREAL_0:2;
then
A74: f.(i1-'1)=f/.(i1-'1) by A54,FINSEQ_4:15;
1<i1-'1 by A54,A70,XXREAL_0:1;
then f/.(i1-'1)<>f/.(i1+1) by A72,A73,GOBOARD7:37;
hence thesis by A9,A59,A52,A74,A71,FINSEQ_4:15;
end;
case
A75: i1+1<>len f;
A76: 1<=i1-'1 by A53,NAT_D:39;
i1-'1<i1-'1+1 by NAT_1:13;
then i1-'1<i1 by A4,XREAL_1:235;
then
A77: i1-'1<i1+1 by NAT_1:13;
then i1-'1<len f by A9,XXREAL_0:2;
then
A78: f.(i1-'1)=f/.(i1-'1) by A76,FINSEQ_4:15;
A79: 1<i1+1 by A4,NAT_1:13;
i1+1<len f by A9,A75,XXREAL_0:1;
then f/.(i1-'1)<>f/.(i1+1) by A76,A77,GOBOARD7:36;
hence thesis by A9,A59,A52,A78,A79,FINSEQ_4:15;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th55:
for f being non constant standard special_circular_sequence,
g1,g2 st i1<>i2 &
g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & g1.2=g2.2
holds g1=g2
proof
let f be non constant standard special_circular_sequence, g1,g2;
assume that
A1: i1<>i2 and
A2: g1 is_a_part_of f,i1,i2 and
A3: g2 is_a_part_of f,i1,i2 and
A4: g1.2=g2.2;
per cases by A2;
suppose
A5: g1 is_a_part>_of f,i1,i2;
now
per cases by A3;
case
g2 is_a_part>_of f,i1,i2;
hence thesis by A5,Th52;
end;
case
g2 is_a_part<_of f,i1,i2;
hence contradiction by A1,A4,A5,Th54;
end;
end;
hence thesis;
end;
suppose
A6: g1 is_a_part<_of f,i1,i2;
now
per cases by A3;
case
g2 is_a_part>_of f,i1,i2;
hence contradiction by A1,A4,A6,Th54;
end;
case
g2 is_a_part<_of f,i1,i2;
hence thesis by A6,Th53;
end;
end;
hence thesis;
end;
end;
definition
let f be non constant standard special_circular_sequence,
i1,i2 be Element of NAT;
assume that
A1: 1<=i1 and
A2: i1+1<=len f and
A3: 1<=i2 and
A4: i2+1<=len f and
A5: i1<>i2;
func Lower (f,i1,i2) -> FinSequence of TOP-REAL 2 means
it is_a_part_of f,i1
,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+1))`2<(f/.i1)`2 implies it.2=f.(i1+1)
)& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))`2>=(f/.i1)`2 implies it.2=f.S_Drop(
i1-'1,f));
correctness
proof
A6: i1+1-1<=len f-1 by A2,XREAL_1:9;
A7: i1-'1=i1-1 by A1,XREAL_1:233;
A8: i2+1-1<=len f-1 by A4,XREAL_1:9;
A9: i2<len f by A4,NAT_1:13;
len f<len f+1 by NAT_1:13;
then
A10: len f-1<len f+1-1 by XREAL_1:9;
A11: i1<len f by A2,NAT_1:13;
then
A12: len f-'1=len f-1 by A1,XREAL_1:233,XXREAL_0:2;
A13: 1<len f by A1,A11,XXREAL_0:2;
then 1+1<=len f by NAT_1:13;
then
A14: 1+1-1<=len f-1 by XREAL_1:9;
then
A15: 1<=len f-'1 by NAT_D:39;
now
per cases;
case
A16: i1<=i2;
then
A17: i1<i2 by A5,XXREAL_0:1;
now
per cases;
case
A18: (f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+1))`2<(f/.i1)`2;
set g=mid(f,i1,i2);
i1+1<=i2 by A17,NAT_1:13;
then (1+i1)+1<=i2+1 by XREAL_1:6;
then 2+i1-i1<=i2+1-i1 by XREAL_1:9;
then
A19: 2+i1-i1<=i2-i1+1;
len mid(f,i1,i2)=i2-'i1+1 by A1,A3,A11,A9,A16,FINSEQ_6:118;
then 2<=len mid(f,i1,i2) by A16,A19,XREAL_1:233;
then
A20: g.2=f.(2+i1-'1) by A1,A3,A11,A9,A16,FINSEQ_6:118
.=f.(i1+1+1-1) by NAT_D:37
.=f.(i1+1);
g is_a_part>_of f,i1,i2 by A1,A9,A16,Th31;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+
1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))
`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A18,A20;
end;
case
A21: (f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))`2>=(f/.i1)`2;
set g=mid(f,i1,1)^mid(f,len f-'1,i2);
A22: len mid(f,i1,1)=i1-'1+1 by A1,A11,FINSEQ_6:187;
A23: g is_a_part<_of f,i1,i2 by A1,A9,A17,Th34;
now
per cases;
case
A24: 1<i1;
then 1+1<=i1-1+1 by NAT_1:13;
then
A25: 2<=len mid(f,i1,1) by A1,A22,XREAL_1:233;
A26: i1-'1<=len f-'1 by A11,A7,A12,XREAL_1:9;
A27: 1+1<=i1 by A24,NAT_1:13;
then
A28: 1+1-1<=i1-1 by XREAL_1:9;
A29: f.(i1-'(1+1)+1)=f.(i1-(1+1)+1) by A27,XREAL_1:233
.=f.(i1-1)
.=f.(i1-'1) by A1,XREAL_1:233;
g.2 =mid(f,i1,1).2 by A7,A22,A27,FINSEQ_1:64
.=f.(i1-'(1+1)+1) by A11,A13,A24,A25,FINSEQ_6:118;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.
(i1+1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+
1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A7,A21,A23,A29,A28,A26,Th22;
end;
case
A30: 1>=i1;
then i1=1 by A1,XXREAL_0:1;
then
A31: i1-'1=0 by XREAL_1:232;
A32: S_Drop(i1-'1,f)=S_Drop(i1-'1+(len f-'1),f) by Th23
.=len f-'1 by A15,A31,Th22;
A33: 1<=len f-'1-'i2+1 by NAT_1:11;
A34: len f-i2>=i2+1-i2 by A4,XREAL_1:9;
1 <= len f by A13; then
Z1: 1 in dom f by FINSEQ_3:25;
A35: len mid(f,i1,1)=len mid(f,1,1) by A1,A30,XXREAL_0:1
.=1 by Z1,FINSEQ_6:193;
len mid(f,len f-'1,i2)=len f-'1-'i2+1 by A3,A12,A8,A10,
FINSEQ_6:187
.=len f-1-i2+1 by A12,A8,XREAL_1:233
.=len f-i2;
then 1+1<=len mid(f,i1,1)+len mid(f,len f-'1,i2 ) by A35,A34,
XREAL_1:6;
then g .2 =mid(f,len f-'1,i2).(2-len mid(f,i1,1)) by A35,
FINSEQ_6:108
.=mid(f,len f-'1,i2).(2-(i1-'1+1)) by A1,A11,FINSEQ_6:187
.=mid(f,len f-'1,i2).(1+1-(1-'1+1)) by A1,A30,XXREAL_0:1
.=mid(f,len f-'1,i2).(1+1-(0+1)) by XREAL_1:232
.=f.(len f-'1-'1+1) by A3,A12,A8,A10,A33,FINSEQ_6:190
.=f.(len f-'1) by A15,XREAL_1:235;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.
(i1+1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+
1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A21,A23,A32;
end;
end;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+
1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))
`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f));
end;
end;
hence
ex g st g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.
(i1+1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+
1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f));
end;
case
A36: i1>i2;
then i1>1 by A3,XXREAL_0:2;
then
A37: 1+1<=i1 by NAT_1:13;
then
A38: 1+1-1<=i1-1 by XREAL_1:9;
now
per cases;
case
A39: (f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))`2>=(f/.i1)`2;
set g=mid(f,i1,i2);
A40: i1-1<len f-1 by A11,XREAL_1:9;
i2+1<=i1 by A36,NAT_1:13;
then (1+i2)+1<=i1+1 by XREAL_1:6;
then 2+i2-i2<=i1+1-i2 by XREAL_1:9;
then
A41: 2+i2-i2<=i1-i2+1;
len mid(f,i1,i2)=i1-'i2+1 by A1,A3,A11,A9,A36,FINSEQ_6:118;
then 2<=len mid(f,i1,i2) by A36,A41,XREAL_1:233;
then
A42: g.2=f.(i1-'2+1) by A1,A3,A11,A9,A36,FINSEQ_6:118
.=f.(i1-(1+1)+1) by A37,XREAL_1:233
.=f.(i1-1)
.=f.(i1-'1) by A1,XREAL_1:233;
g is_a_part<_of f,i1,i2 by A3,A11,A36,Th32;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+
1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))
`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A7,A12,A38,A39,A42,A40,Th22;
end;
case
A43: (f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+1))`2<(f/.i1)`2;
set g=mid(f,i1,len f-'1)^mid(f,1,i2);
A44: g is_a_part>_of f,i1,i2 by A3,A11,A36,Th33;
A45: len mid(f,i1,len f-'1)=len f-'1-'i1+1 by A1,A11,A14,A12,A6,A10,
FINSEQ_6:118
.=len f-1-i1+1 by A12,A6,XREAL_1:233
.=len f-i1;
now
per cases;
case
i1+1<len f;
then i1+1+1<=len f by NAT_1:13;
then
A46: i1+2-i1<=len f-i1 by XREAL_1:9;
then g.2 =mid(f,i1,len f-'1).2 by A45,FINSEQ_1:64
.=f.(2+i1-'1) by A1,A11,A14,A12,A6,A10,A45,A46,FINSEQ_6:118
.=f.(1+1+i1-1) by NAT_D:37
.=f.(i1+1);
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.
(i1+1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+
1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A43,A44;
end;
case
A47: i1+1>=len f;
then F1: i1+1=len f by A2,XXREAL_0:1;
then
i1 <= len f by NAT_1:13; then
i1 in dom f by A1,FINSEQ_3:25; then
A48: len mid(f,i1,len f-'1)=1 by A12,F1,FINSEQ_6:193;
len mid(f,1,i2)=i2-'1+1 by A3,A13,A9,FINSEQ_6:118
.=i2-1+1 by A3,XREAL_1:233
.=i2;
then
1+1<=len mid(f,i1,len f-'1)+len mid(f,1,i2) by A3,A48,XREAL_1:6;
then g.2 =mid(f,1,i2).(2-(i1+1-i1)) by A48,FINSEQ_6:108
.=f.1 by A3,A13,A9,FINSEQ_6:118
.=f/.1 by A13,FINSEQ_4:15
.=f/.len f by FINSEQ_6:def 1
.=f.len f by A13,FINSEQ_4:15;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.
(i1+1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+
1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A43,A44,A47,
XXREAL_0:1;
end;
end;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+
1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))
`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f));
end;
end;
hence
ex g st g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.
(i1+1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+
1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f));
end;
end;
hence
ex g st g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+
1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))
`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f));
thus thesis by A5,Th55;
end;
func Upper (f,i1,i2) -> FinSequence of TOP-REAL 2 means
it is_a_part_of f,i1
,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+1))`2>(f/.i1)`2 implies it.2=f.(i1+1)
)& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))`2<=(f/.i1)`2 implies it.2=f.S_Drop(
i1-'1,f));
correctness
proof
len f<len f+1 by NAT_1:13;
then
A49: len f-1<len f+1-1 by XREAL_1:9;
A50: i2+1-1<=len f-1 by A4,XREAL_1:9;
A51: i2<len f by A4,NAT_1:13;
A52: i1+1-1<=len f-1 by A2,XREAL_1:9;
A53: i1-'1=i1-1 by A1,XREAL_1:233;
A54: i1<len f by A2,NAT_1:13;
then
A55: len f-'1=len f-1 by A1,XREAL_1:233,XXREAL_0:2;
A56: 1<len f by A1,A54,XXREAL_0:2;
then 1+1<=len f by NAT_1:13;
then
A57: 1+1-1<=len f-1 by XREAL_1:9;
then
A58: 1<=len f-'1 by NAT_D:39;
now
per cases;
case
A59: i1<=i2;
then
A60: i1<i2 by A5,XXREAL_0:1;
now
per cases;
case
A61: (f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+1))`2>(f/.i1)`2;
set g=mid(f,i1,i2);
i1+1<=i2 by A60,NAT_1:13;
then (1+i1)+1<=i2+1 by XREAL_1:6;
then 2+i1-i1<=i2+1-i1 by XREAL_1:9;
then
A62: 2+i1-i1<=i2-i1+1;
len mid(f,i1,i2)=i2-'i1+1 by A1,A3,A54,A51,A59,FINSEQ_6:118;
then 2<=len mid(f,i1,i2) by A59,A62,XREAL_1:233;
then
A63: g.2=f.(2+i1-'1) by A1,A3,A54,A51,A59,FINSEQ_6:118
.=f.(i1+1+1-1) by NAT_D:37
.=f.(i1+1);
g is_a_part>_of f,i1,i2 by A1,A51,A59,Th31;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+
1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))
`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A61,A63;
end;
case
A64: (f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))`2<=(f/.i1)`2;
set g=mid(f,i1,1)^mid(f,len f-'1,i2);
A65: len mid(f,i1,1)=i1-'1+1 by A1,A54,FINSEQ_6:187;
A66: g is_a_part<_of f,i1,i2 by A1,A51,A60,Th34;
now
per cases;
case
A67: 1<i1;
then 1+1<=i1-1+1 by NAT_1:13;
then
A68: 2<=len mid(f,i1,1) by A1,A65,XREAL_1:233;
A69: i1-'1<=len f-'1 by A54,A53,A55,XREAL_1:9;
A70: 1+1<=i1 by A67,NAT_1:13;
then
A71: 1+1-1<=i1-1 by XREAL_1:9;
A72: f.(i1-'(1+1)+1)=f.(i1-(1+1)+1) by A70,XREAL_1:233
.=f.(i1-1)
.=f.(i1-'1) by A1,XREAL_1:233;
g.2 =mid(f,i1,1).2 by A53,A65,A70,FINSEQ_1:64
.=f.(i1-'(1+1)+1) by A54,A56,A67,A68,FINSEQ_6:118;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.
(i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+
1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A53,A64,A66,A72,A71,A69,Th22
;
end;
case
A73: 1>=i1;
then i1=1 by A1,XXREAL_0:1;
then
A74: i1-'1=0 by XREAL_1:232;
A75: S_Drop(i1-'1,f)=S_Drop(i1-'1+(len f-'1),f) by Th23
.=len f-'1 by A58,A74,Th22;
A76: 1<=len f-'1-'i2+1 by NAT_1:11;
A77: i2+1-1<=len f-1 by A4,XREAL_1:9;
A78: len f-i2>=i2+1-i2 by A4,XREAL_1:9;
1 <= len f by A56; then
S1: 1 in dom f by FINSEQ_3:25;
A79: len mid(f,i1,1)=len mid(f,1,1) by A1,A73,XXREAL_0:1
.=1 by S1,FINSEQ_6:193;
len mid(f,len f-'1,i2)=len f-'1-'i2+1 by A3,A55,A50,A49,
FINSEQ_6:187
.=len f-1-i2+1 by A55,A50,XREAL_1:233
.=len f-i2;
then 1+1<=len mid(f,i1,1)+len mid(f,len f-'1,i2 ) by A79,A78,
XREAL_1:6;
then g .2 =mid(f,len f-'1,i2).(2-len mid(f,i1,1)) by A79,
FINSEQ_6:108
.=mid(f,len f-'1,i2).(2-(i1-'1+1)) by A1,A54,FINSEQ_6:187
.=mid(f,len f-'1,i2).(1+1-(1-'1+1)) by A1,A73,XXREAL_0:1
.=mid(f,len f-'1,i2).(1+1-(0+1)) by XREAL_1:232
.=f.(len f-'1-'1+1) by A3,A55,A49,A77,A76,FINSEQ_6:190
.=f.(len f-'1) by A58,XREAL_1:235;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.
(i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+
1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A64,A66,A75;
end;
end;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+
1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))
`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f));
end;
end;
hence
ex g st g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.
(i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+
1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f));
end;
case
A80: i1>i2;
then i1>1 by A3,XXREAL_0:2;
then
A81: 1+1<=i1 by NAT_1:13;
then
A82: 1+1-1<=i1-1 by XREAL_1:9;
now
per cases;
case
A83: (f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))`2<=(f/.i1)`2;
set g=mid(f,i1,i2);
A84: i1-'1<=len f-'1 by A54,A53,A55,XREAL_1:9;
i2+1<=i1 by A80,NAT_1:13;
then (1+i2)+1<=i1+1 by XREAL_1:6;
then 2+i2-i2<=i1+1-i2 by XREAL_1:9;
then
A85: 2+i2-i2<=i1-i2+1;
len mid(f,i1,i2)=i1-'i2+1 by A1,A3,A54,A51,A80,FINSEQ_6:118;
then 2<=len mid(f,i1,i2) by A80,A85,XREAL_1:233;
then
A86: g.2=f.(i1-'2+1) by A1,A3,A54,A51,A80,FINSEQ_6:118
.=f.(i1-(1+1)+1) by A81,XREAL_1:233
.=f.(i1-1)
.=f.(i1-'1) by A1,XREAL_1:233;
g is_a_part<_of f,i1,i2 by A3,A54,A80,Th32;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+
1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))
`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A53,A82,A83,A86,A84,Th22;
end;
case
A87: (f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+1))`2>(f/.i1)`2;
set g=mid(f,i1,len f-'1)^mid(f,1,i2);
A88: g is_a_part>_of f,i1,i2 by A3,A54,A80,Th33;
A89: len mid(f,i1,len f-'1)=len f-'1-'i1+1 by A1,A54,A57,A55,A52,A49,
FINSEQ_6:118
.=len f-1-i1+1 by A55,A52,XREAL_1:233
.=len f-i1;
now
per cases;
case
i1+1<len f;
then i1+1+1<=len f by NAT_1:13;
then
A90: i1+2-i1<=len f-i1 by XREAL_1:9;
then g.2 =mid(f,i1,len f-'1).2 by A89,FINSEQ_1:64
.=f.(2+i1-'1) by A1,A54,A57,A55,A52,A49,A89,A90,FINSEQ_6:118
.=f.(1+1+i1-1) by NAT_D:37
.=f.(1+i1);
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.
(i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1)) & ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1
+1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A87,A88;
end;
case
A91: i1+1>=len f;
then S1: i1+1=len f by A2,XXREAL_0:1;
then
i1 <= len f by NAT_1:13; then
i1 in dom f by A1,FINSEQ_3:25; then
A92: len mid(f,i1,len f-'1)=1 by A55,S1,FINSEQ_6:193;
len mid(f,1,i2)=i2-'1+1 by A3,A56,A51,FINSEQ_6:118
.=i2-1+1 by A3,XREAL_1:233
.=i2;
then 1+1<=len mid(f,i1,len f-'1)+len mid(f,1,i2) by A3,A92,
XREAL_1:6;
then g.2 =mid(f,1,i2).(2-(i1+1-i1)) by A92,FINSEQ_6:108
.=f.1 by A3,A56,A51,FINSEQ_6:118
.=f/.1 by A56,FINSEQ_4:15
.=f/.len f by FINSEQ_6:def 1
.=f.len f by A56,FINSEQ_4:15;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.
(i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1)) & ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1
+1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A87,A88,A91,
XXREAL_0:1;
end;
end;
hence
g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+
1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))
`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f));
end;
end;
hence
ex g st g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.
(i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+
1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f));
end;
end;
hence thesis by A5,Th55;
end;
end;