:: Rotating and reversing.(Finite sequences)
:: by Andrzej Trybulec
::
:: Received January 21, 1999
:: Copyright (c) 1999-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, XBOOLE_0, FINSEQ_1, FUNCT_1, RELAT_1,
PARTFUN1, FINSEQ_4, ARYTM_3, FINSEQ_5, RFINSEQ, ORDINAL4, XXREAL_0,
ARYTM_1, FINSEQ_6, CARD_1, NAT_1, ZFMISC_1, EUCLID, JORDAN2C, FINSEQ_2,
SUPINF_2, TARSKI, GOBOARD1, MCART_1, PRE_TOPC, TOPREAL1, RLTOPSP1,
GOBOARD2, GOBOARD5, MATRIX_1, COMPLEX1, GOBOARD9, CONNSP_1, TOPS_1,
PSCOMP_1, SPRECT_2, TREES_1, JORDAN5D, RCOMP_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
NAT_1, COMPLEX1, NAT_D, CARD_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2,
MATRIX_0, MATRIX_1, FINSEQ_4, RFINSEQ, FINSEQ_5, FINSEQ_6, ZFMISC_1,
DOMAIN_1, SEQ_4, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1, COMPTS_1, EUCLID,
RLTOPSP1, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, PSCOMP_1,
JORDAN5D, SPRECT_2;
constructors FINSEQOP, FINSEQ_4, RFINSEQ, NAT_D, TOPS_1, CONNSP_1, COMPTS_1,
REALSET2, GOBOARD2, PSCOMP_1, GOBOARD9, SPRECT_2, JORDAN5D, REAL_1,
GOBOARD1, RELSET_1, SEQ_4, RVSUM_1, MATRIX_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_6,
STRUCT_0, GOBOARD2, GOBOARD9, SPRECT_1, SPRECT_2, CARD_1, COMPTS_1,
EUCLID, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TOPREAL1, GOBOARD5, SPRECT_2, TARSKI, FINSEQ_6, GOBOARD1,
XBOOLE_0, STRUCT_0;
equalities TOPREAL1;
expansions TARSKI, GOBOARD1, XBOOLE_0;
theorems FINSEQ_6, NAT_1, FINSEQ_5, FINSEQ_3, FINSEQ_4, NAT_2, FINSEQ_1,
SPRECT_3, RFINSEQ, TOPREAL1, GOBOARD5, SPPOL_2, TARSKI, SPRECT_2,
GOBOARD9, INT_1, SUBSET_1, JGRAPH_1, GOBOARD7, GOBOARD1, GOBOARD2,
FUNCT_1, PARTFUN2, RELAT_1, FINSEQ_2, JORDAN5D, PSCOMP_1, EUCLID,
TOPREAL3, XBOOLE_0, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, NAT_D, SEQM_3,
SEQ_4, MATRIX_0;
begin :: Preliminaries
reserve i,j,k,m,n for Nat,
D for non empty set,
p for Element of D,
f for FinSequence of D;
definition
::$CD 2
end;
::$CT 18
reserve D for non empty set,
p for Element of D,
f for FinSequence of D;
Th9:
p in rng f & 1 <= i & i <= len(f:-p) implies (Rotate(f,p))/.i = f
/.(i -' 1 + p..f) by FINSEQ_6:174;
Th10:
p in rng f & p..f <= i & i <= len f implies f/.i = (Rotate(f,p))
/.(i+1 -' p..f) by FINSEQ_6:175;
Th11:
p in rng f implies (Rotate(f,p))/.len(f:-p) = f/.len f
by FINSEQ_6:176;
Th14:
len Rotate(f,p) = len f by FINSEQ_6:179;
Th15:
dom Rotate(f,p) = dom f by FINSEQ_6:180;
Th16:
for D being non empty set, f being circular FinSequence of D, p
be Element of D st for i st 1 < i & i < len f holds f/.i <> f/.1 holds Rotate(
Rotate(f,p),f/.1) = f by FINSEQ_6:181;
begin :: Rotating circular
reserve f for circular FinSequence of D;
Th17:
p in rng f & len(f:-p) <= i & i <= len f implies (Rotate(f,p))/.
i = f/.(i + p..f -' len f) by FINSEQ_6:182;
Th18:
p in rng f & 1 <= i & i <= p..f implies f/.i = (Rotate(f,p))/.(i
+ len f -' p..f) by FINSEQ_6:183;
begin :: Finite sequences on the plane
theorem Th19:
for n being non zero Nat holds 0.REAL n <> 1.REAL n
proof
let n be non zero Nat;
1 <= n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:1;
then
A1: (n |-> 0).1 = 0 & (n |-> 1).1 = 1 by FINSEQ_2:57;
1.REAL n = 1*n by EUCLID:def 12
.= n |-> 1 by EUCLID:def 11;
hence thesis by A1,EUCLID:def 4;
end;
registration
let n be non zero Nat;
cluster TOP-REAL n -> non trivial;
coherence
proof
reconsider 1R = 1.REAL n as Element of TOP-REAL n;
take 1R;
0.REAL n = 0.TOP-REAL n by EUCLID:66;
hence 1R <> 0.TOP-REAL n by Th19;
end;
end;
reserve f,g for FinSequence of TOP-REAL 2;
theorem Th20:
rng f c= rng g implies rng X_axis f c= rng X_axis g
proof
assume
A1: rng f c= rng g;
A2: dom X_axis g = dom g by SPRECT_2:15;
let x be object;
assume x in rng X_axis f;
then consider y being object such that
A3: y in dom X_axis f and
A4: (X_axis f).y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A3;
A5: (X_axis f).y = (f/.y)`1 by A3,GOBOARD1:def 1;
dom X_axis f = dom f by SPRECT_2:15;
then f/.y in rng f by A3,PARTFUN2:2;
then consider z being object such that
A6: z in dom g and
A7: g.z = f/.y by A1,FUNCT_1:def 3;
reconsider z as Element of NAT by A6;
g/.z = f/.y by A6,A7,PARTFUN1:def 6;
then (X_axis g).z = (f/.y)`1 by A2,A6,GOBOARD1:def 1;
hence thesis by A4,A2,A5,A6,FUNCT_1:def 3;
end;
theorem Th21:
rng f = rng g implies rng X_axis f = rng X_axis g
by Th20;
theorem Th22:
rng f c= rng g implies rng Y_axis f c= rng Y_axis g
proof
assume
A1: rng f c= rng g;
A2: dom Y_axis g = dom g by SPRECT_2:16;
let x be object;
assume x in rng Y_axis f;
then consider y being object such that
A3: y in dom Y_axis f and
A4: (Y_axis f).y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A3;
A5: (Y_axis f).y = (f/.y)`2 by A3,GOBOARD1:def 2;
dom Y_axis f = dom f by SPRECT_2:16;
then f/.y in rng f by A3,PARTFUN2:2;
then consider z being object such that
A6: z in dom g and
A7: g.z = f/.y by A1,FUNCT_1:def 3;
reconsider z as Element of NAT by A6;
g/.z = f/.y by A6,A7,PARTFUN1:def 6;
then (Y_axis g).z = (f/.y)`2 by A2,A6,GOBOARD1:def 2;
hence thesis by A4,A2,A5,A6,FUNCT_1:def 3;
end;
theorem Th23:
rng f = rng g implies rng Y_axis f = rng Y_axis g
by Th22;
begin :: Rotating finite sequences on the plane
reserve p for Point of TOP-REAL 2,
f for FinSequence of TOP-REAL 2;
registration
let p be Point of TOP-REAL 2;
let f be special circular FinSequence of TOP-REAL 2;
cluster Rotate(f,p) -> special;
coherence
proof
per cases;
suppose
not p in rng f;
hence thesis by FINSEQ_6:def 2;
end;
suppose
A1: p in rng f;
A2: len Rotate(f,p) = len f by Th14;
let i be Nat such that
A3: 1 <= i and
A4: i+1 <= len Rotate(f,p);
A5: i+1 >= i by NAT_1:11;
now
A6: len (f:-p) = len f - p..f + 1 by A1,FINSEQ_5:50;
per cases;
suppose
A7: i < len(f:-p);
A8: i + 1 -' 1 + p..f = i + p..f by NAT_D:34
.= i -' 1 + 1 + p..f by A3,XREAL_1:235
.= i -' 1 + p..f + 1;
i+1 <= len(f:-p) by A7,NAT_1:13;
then
A9: (Rotate(f,p))/.(i+1) = f/.(i -' 1 + p..f + 1) by A1,A8,Th9,NAT_1:11;
0 <= i -' 1 & 1 <= p..f by A1,FINSEQ_4:21;
then
A10: 1 + 0 <= i -' 1 + p..f by XREAL_1:7;
i < len f + 1 - p..f by A6,A7;
then i + p..f < len f + 1 by XREAL_1:20;
then i + p..f <= len f by NAT_1:13;
then
A11: i -' 1 + 1 + p..f <= len f by A3,XREAL_1:235;
(Rotate(f,p))/.i = f/.(i -' 1 + p..f) by A1,A3,A7,Th9;
hence thesis by A9,A10,A11,TOPREAL1:def 5;
end;
suppose
A12: i >= len(f:-p);
i <= len f by A4,A5,A2,XXREAL_0:2;
then
A13: (Rotate(f,p))/.i = f/.(i + p..f -' len f) by A1,A12,Th17;
i - (len f - p..f) >= 1 by A6,A12,XREAL_1:19;
then i + p..f - len f >= 1;
then
A14: 1 <= i + p..f -' len f by NAT_D:39;
A15: i+1 >= len(f:-p) by A5,A12,XXREAL_0:2;
then i >= len f - p..f by A6,XREAL_1:6;
then
A16: len f <= i + p..f by XREAL_1:20;
i+1 + p..f -' len f = i + p..f+1 -' len f
.= i + p..f -' len f + 1 by A16,NAT_D:38;
then
A17: (Rotate(f,p))/.(i+1) = f/.(i + p..f -' len f + 1) by A1,A4,A2,A15
,Th17;
p..f <= len f by A1,FINSEQ_4:21;
then i + 1 + p..f <= len f + len f by A4,A2,XREAL_1:7;
then i + p..f + 1 - len f <= len f by XREAL_1:20;
then i + p..f - len f + 1 <= len f;
then i + p..f -' len f + 1 <= len f by A16,XREAL_1:233;
hence thesis by A13,A17,A14,TOPREAL1:def 5;
end;
end;
hence thesis;
end;
end;
end;
theorem Th24:
p in rng f & 1 <= i & i < len(f:-p) implies LSeg(Rotate(f,p),i)
= LSeg(f,i -' 1 + p..f)
proof
assume that
A1: p in rng f and
A2: 1 <= i and
A3: i < len(f:-p);
A4: i+1 <= len(f:-p) by A3,NAT_1:13;
A5: len(f:-p) = len f - p..f + 1 by A1,FINSEQ_5:50;
then i - 1 < len f - p..f by A3,XREAL_1:19;
then i -' 1 < len f - p..f by A2,XREAL_1:233;
then i -' 1 + p..f < len f by XREAL_1:20;
then
A6: i -' 1 + p..f + 1 <= len f by NAT_1:13;
p..f - 1 >= 0 by A1,FINSEQ_4:21,XREAL_1:48;
then len f - (p..f - 1) <= len f by XREAL_1:43;
then
A7: i+1 <= len f by A5,A4,XXREAL_0:2;
i -' 1 >= 0 & 1 <= p..f by A1,FINSEQ_4:21;
then
A8: 0+1 <= i -' 1 + p..f by XREAL_1:7;
i -' 1 + p..f + 1 = i -' 1 + 1 + p..f .= i + p..f by A2,XREAL_1:235
.= i + 1 -' 1 + p..f by NAT_D:34;
then
A9: (Rotate(f,p))/.(i+1) = f/.(i -' 1 + p..f + 1)by A1,A4,Th9,NAT_1:11;
A10: len Rotate(f,p) = len f by Th14;
(Rotate(f,p))/.i = f/.(i -' 1 + p..f) by A1,A2,A3,Th9;
hence LSeg(Rotate(f,p),i) = LSeg(f/.(i -' 1 + p..f),f/.(i -' 1 + p..f + 1))
by A2,A10,A9,A7,TOPREAL1:def 3
.= LSeg(f,i -' 1 + p..f) by A8,A6,TOPREAL1:def 3;
end;
theorem Th25:
p in rng f & p..f <= i & i < len f implies LSeg(f,i) = LSeg(
Rotate(f,p),i -' p..f+1)
proof
assume that
A1: p in rng f and
A2: p..f <= i and
A3: i < len f;
i - p..f < len f - p..f by A3,XREAL_1:9;
then i -' p..f < len f - p..f by A2,XREAL_1:233;
then i -' p..f+1 < len f - p..f + 1 by XREAL_1:6;
then
A4: i -' p..f+1 < len(f:-p) by A1,FINSEQ_5:50;
1 + p..f <= i + 1 by A2,XREAL_1:6;
then 1 <= i + 1 -' p..f by NAT_D:55;
then
A5: 1 <= i -' p..f+1 by A2,NAT_D:38;
i -' p..f+1 -' 1 + p..f =i -' p..f + p..f by NAT_D:34
.= i by A2,XREAL_1:235;
hence thesis by A1,A5,A4,Th24;
end;
theorem Th26:
for f being circular FinSequence of TOP-REAL 2 holds Incr X_axis
f = Incr X_axis Rotate(f,p)
proof
let f be circular FinSequence of TOP-REAL 2;
per cases;
suppose
not p in rng f;
hence thesis by FINSEQ_6:def 2;
end;
suppose
p in rng f;
then rng Rotate(f,p) = rng f by FINSEQ_6:90;
then rng X_axis Rotate(f,p) = rng X_axis f by Th21;
then
rng Incr X_axis Rotate(f,p) = rng X_axis f & len Incr X_axis Rotate(f,
p) = card rng X_axis f by SEQ_4:def 21;
hence thesis by SEQ_4:def 21;
end;
end;
theorem Th27:
for f being circular FinSequence of TOP-REAL 2 holds Incr Y_axis
f = Incr Y_axis Rotate(f,p)
proof
let f be circular FinSequence of TOP-REAL 2;
per cases;
suppose
not p in rng f;
hence thesis by FINSEQ_6:def 2;
end;
suppose
p in rng f;
then rng Rotate(f,p) = rng f by FINSEQ_6:90;
then rng Y_axis Rotate(f,p) = rng Y_axis f by Th23;
then
rng Incr Y_axis Rotate(f,p) = rng Y_axis f & len Incr Y_axis Rotate(f,
p) = card rng Y_axis f by SEQ_4:def 21;
hence thesis by SEQ_4:def 21;
end;
end;
theorem Th28:
for f being non empty circular FinSequence of TOP-REAL 2 holds
GoB Rotate(f,p) = GoB f
proof
let f be non empty circular FinSequence of TOP-REAL 2;
Incr X_axis f = Incr X_axis Rotate(f,p) & Incr Y_axis f = Incr Y_axis
Rotate (f,p) by Th26,Th27;
hence GoB Rotate(f,p) = GoB(Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 2
.= GoB f by GOBOARD2:def 2;
end;
theorem Th29:
for f being non constant standard special_circular_sequence
holds Rev Rotate(f,p) = Rotate(Rev f,p)
proof
let f be non constant standard special_circular_sequence;
per cases;
suppose
not p in rng f;
then Rotate(f,p) = f & not p in rng Rev f by FINSEQ_5:57,FINSEQ_6:def 2;
hence thesis by FINSEQ_6:def 2;
end;
suppose
A1: p = f/.1;
then
A2: p = (Rev f)/.len f by FINSEQ_5:65
.= (Rev f)/.len Rev f by FINSEQ_5:def 3
.= (Rev f)/.1 by FINSEQ_6:def 1;
Rotate(f,p) = f by A1,FINSEQ_6:89;
hence thesis by A2,FINSEQ_6:89;
end;
suppose that
A3: p in rng f and
A4: p <> f/.1;
f just_once_values p
proof
take p..f;
thus
A5: p..f in dom f by A3,FINSEQ_4:20;
thus
A6: p = f.(p..f) by A3,FINSEQ_4:19
.= f/.(p..f) by A5,PARTFUN1:def 6;
let z be set such that
A7: z in dom f and
A8: z <> p..f;
reconsider k = z as Element of NAT by A7;
per cases by A8,XXREAL_0:1;
suppose
A9: k < p..f;
p..f <= len f & p..f <> len f by A3,A4,A6,FINSEQ_4:21,FINSEQ_6:def 1;
then
A10: p..f < len f by XXREAL_0:1;
1 <= k by A7,FINSEQ_3:25;
hence thesis by A6,A9,A10,GOBOARD7:36;
end;
suppose
A11: k > p..f;
p..f >= 1 by A3,FINSEQ_4:21;
then
A12: p..f > 1 by A4,A6,XXREAL_0:1;
k <= len f by A7,FINSEQ_3:25;
hence thesis by A6,A11,A12,GOBOARD7:37;
end;
end;
hence thesis by FINSEQ_6:106;
end;
end;
begin :: Circular finite sequences of points of the plane
reserve f for circular FinSequence of TOP-REAL 2;
theorem Th30:
for f being circular s.c.c. FinSequence of TOP-REAL 2 st len f >
4 holds LSeg(f,len f -' 1) /\ LSeg(f,1) = {f/.1}
proof
let f be circular s.c.c. FinSequence of TOP-REAL 2;
assume
A1: len f > 4;
then
A2: len f -' 1 + 1 = len f by XREAL_1:235,XXREAL_0:2;
A3: len f >= 1+1 by A1,XXREAL_0:2;
then
A4: 1 <= len f -' 1 by NAT_D:55;
A5: len f >= 1+1+1 by A1,XXREAL_0:2;
thus LSeg(f,len f -' 1) /\ LSeg(f,1) c= {f/.1}
proof
assume not LSeg(f,len f -' 1) /\ LSeg(f,1) c= {f/.1};
then consider p being Point of TOP-REAL 2 such that
A6: p in LSeg(f,len f -' 1) /\ LSeg(f,1) and
A7: not p in {f/.1};
A8: p <> f/.1 by A7,TARSKI:def 1;
A9: LSeg(f,len f -' 1) = LSeg(f/.(len f -' 1),f/.len f) & LSeg(f,1) = LSeg
(f/.1, f/.(1+1)) by A3,A2,A4,TOPREAL1:def 3;
A10: f/.len f = f/.1 by FINSEQ_6:def 1;
per cases by A6,A9,A8,A10,JGRAPH_1:16;
suppose
A11: f/.(1+1) in LSeg(f,len f -' 1);
A12: f/.(1+1) in LSeg(f,1+1) by A5,TOPREAL1:21;
3+1 = 4;
then 1+1+1 < len f - 1 by A1,XREAL_1:20;
then
A13: 1+1+1 < len f -' 1 by A1,XREAL_1:233,XXREAL_0:2;
len f -' 1 < len f by A4,NAT_D:51;
then LSeg(f,1+1) misses LSeg(f,len f -' 1) by A13,GOBOARD5:def 4;
hence contradiction by A11,A12,XBOOLE_0:3;
end;
suppose
A14: f/.(len f -' 1) in LSeg(f,1);
A15: len f -' 2+1 = len f -' 1 -' 1+1 by NAT_D:45
.= len f -' 1 by A3,NAT_D:55,XREAL_1:235;
then
A16: len f -' 2+1 < len f by A4,NAT_D:51;
2 + 2 < len f by A1;
then 1+1 < len f - 2 by XREAL_1:20;
then 1+1 < len f -' 2 by A1,XREAL_1:233,XXREAL_0:2;
then
A17: LSeg(f,1) misses LSeg(f,len f -' 2) by A16,GOBOARD5:def 4;
1 <= len f - 2 by A5,XREAL_1:19;
then 1 <= len f -' 2 by NAT_D:39;
then f/.(len f -' 1) in LSeg(f,len f -' 2) by A15,A16,TOPREAL1:21;
hence contradiction by A14,A17,XBOOLE_0:3;
end;
end;
let x be object;
assume x in {f/.1};
then
A18: x = f/.1 by TARSKI:def 1;
then x = f/.len f by FINSEQ_6:def 1;
then
A19: x in LSeg(f,len f -' 1) by A2,A4,TOPREAL1:21;
x in LSeg(f,1) by A3,A18,TOPREAL1:21;
hence thesis by A19,XBOOLE_0:def 4;
end;
theorem Th31:
p in rng f & len(f:-p) <= i & i < len f implies LSeg(Rotate(f,p)
,i) = LSeg(f,i + p..f -' len f)
proof
assume that
A1: p in rng f and
A2: len(f:-p) <= i and
A3: i < len f;
A4: p..f <= len f by A1,FINSEQ_4:21;
A5: len(f:-p) = len f - p..f + 1 by A1,FINSEQ_5:50;
then len f -' p..f + 1 <= i by A2,A4,XREAL_1:233;
then len f + 1 -' p..f <= i by A4,NAT_D:38;
then
A6: len f + 1 <= i + p..f by NAT_D:52;
then
A7: 1 <= i + p..f -' len f by NAT_D:55;
len f - p..f >= 0 by A4,XREAL_1:48;
then len f - p..f + 1 >= 0 + 1 by XREAL_1:6;
then
A8: 0 + 1 <= 0 + i by A2,A5,XXREAL_0:2;
A9: len Rotate(f,p) = len f by Th14;
A10: len f <= len f + 1 by NAT_1:11;
A11: i + 1 <= len f by A3,NAT_1:13;
then i + 1 + p..f <= len f + len f by A4,XREAL_1:7;
then i + p..f + 1 -' len f <= len f by NAT_D:53;
then
A12: i + p..f -' len f + 1 <= len f by A6,A10,NAT_D:38,XXREAL_0:2;
i + 1 + p..f -' len f = i + p..f + 1 -' len f
.= i + p..f -' len f+1 by A6,A10,NAT_D:38,XXREAL_0:2;
then
A13: (Rotate(f,p))/.(i+1) = f/.(i + p..f -' len f+1) by A1,A2,A11,Th17,NAT_1:12
;
i+1 <= len f & (Rotate(f,p))/.i = f/.(i + p..f -' len f) by A1,A2,A3,Th17,
NAT_1:13;
hence
LSeg(Rotate(f,p),i) = LSeg(f/.(i + p..f -' len f),f/.(i + p..f -' len f
+ 1)) by A9,A13,A8,TOPREAL1:def 3
.= LSeg(f,i + p..f -' len f) by A7,A12,TOPREAL1:def 3;
end;
registration
let p be Point of TOP-REAL 2;
let f be circular s.c.c. FinSequence of TOP-REAL 2;
cluster Rotate(f,p) -> s.c.c.;
coherence
proof
set h = Rotate(f,p);
per cases;
suppose
not p in rng f;
hence thesis by FINSEQ_6:def 2;
end;
suppose
p in rng f & p..f = 1;
then p = f/.1 by FINSEQ_5:38;
hence thesis by FINSEQ_6:89;
end;
suppose
p in rng f & p..f = len f;
then p = f/.len f by FINSEQ_5:38;
then p = f/.1 by FINSEQ_6:def 1;
hence thesis by FINSEQ_6:89;
end;
suppose that
A1: p in rng f and
A2: p..f <> 1 and
A3: p..f <> len f;
A4: len(f:-p) = len f - p..f + 1 by A1,FINSEQ_5:50;
let i,j such that
A5: i+1 < j and
A6: i > 1 & j < len h or j+1 < len h;
1 <= p..f by A1,FINSEQ_4:21;
then p..f > 1 by A2,XXREAL_0:1;
then
A7: i -' 1 + p..f > 0+1 by XREAL_1:8;
i <= i+1 by NAT_1:11;
then
A8: i < j by A5,XXREAL_0:2;
A9: len f = len h by Th14;
A10: p..f <= len f by A1,FINSEQ_4:21;
then
A11: len f - p..f = len f -' p..f by XREAL_1:233;
j <= j+1 by NAT_1:11;
then
A12: j < len f by A9,A6,XXREAL_0:2;
then
A13: i < len f by A8,XXREAL_0:2;
now
per cases by NAT_1:14;
suppose
i = 0;
then LSeg(h,i) = {} by TOPREAL1:def 3;
hence thesis;
end;
suppose that
A14: i >= 1 and
A15: j < len(f:-p);
i < len(f:-p) by A8,A15,XXREAL_0:2;
then
A16: LSeg(h,i) = LSeg(f,i -' 1 + p..f) by A1,A14,Th24;
A17: 1 <= j by A8,A14,XXREAL_0:2;
then j -' 1 < len f -' p..f by A4,A11,A15,NAT_D:54;
then
A18: j -' 1 + p..f < len f by NAT_D:53;
i < j -' 1 by A5,NAT_D:52;
then
A19: i + 1 -' 1 < j -' 1 by NAT_D:34;
i -' 1 + p..f + 1 = i -' 1 + 1 + p..f .= i + p..f by A14,XREAL_1:235
.= i + 1 -' 1 + p..f by NAT_D:34;
then
A20: i -' 1 + p..f + 1 < j -' 1 + p..f by A19,XREAL_1:6;
LSeg(h,j) = LSeg(f,j -' 1 + p..f) by A1,A15,A17,Th24;
hence thesis by A7,A16,A20,A18,GOBOARD5:def 4;
end;
suppose that
A21: i >= 1 and
A22: j >= len(f:-p) and
A23: i < len(f:-p);
now
per cases by A6,Th14;
suppose
i > 1;
then i >= 1+1 by NAT_1:13;
then i -' 1 >= 1 by NAT_D:55;
hence j + 1 < i -' 1 + len f by A12,XREAL_1:8;
end;
suppose
A24: j+1 < len f;
0 + len f <= i -' 1 + len f by XREAL_1:6;
hence j + 1 < i -' 1 + len f by A24,XXREAL_0:2;
end;
end;
then j + 1 + p..f < i -' 1 + len f + p..f by XREAL_1:6;
then
A25: j + p..f+1 < i -' 1 + p..f + len f;
len f -' p..f <= len f -' p..f + 1 by NAT_1:11;
then len f - p..f <= j by A4,A11,A22,XXREAL_0:2;
then
A26: len f <= j + p..f by XREAL_1:20;
then len f <= j + p..f + 1 by NAT_1:12;
then j + p..f+1 -' len f < i -' 1 + p..f by A25,NAT_D:54;
then
A27: j + p..f -' len f+1 < i -' 1 + p..f by A26,NAT_D:38;
A28: LSeg(h,i) = LSeg(f,i -' 1 + p..f) & LSeg(h,j) = LSeg(f,j + p..f
-' len f) by A1,A12,A21,A22,A23,Th24,Th31;
now
per cases by A5,XXREAL_0:2;
suppose
j > len f - p..f + 1;
then 1 < j - (len f - p..f) by XREAL_1:20;
then 1 < j + p..f - len f;
then
A29: 1 < j + p..f -' len f by NAT_D:39;
i < len f -' p..f + 1 by A4,A10,A23,XREAL_1:233;
then i -' 1 < len f -' p..f by A21,NAT_D:54;
then i -' 1 + p..f < len f by NAT_D:53;
hence thesis by A28,A27,A29,GOBOARD5:def 4;
end;
suppose
i+1 < len f - p..f + 1;
then i < len f - p..f by XREAL_1:6;
then i + p..f < len f by XREAL_1:20;
then i -' 1 + 1 + p..f < len f by A21,XREAL_1:235;
then i -' 1 + p..f + 1 < len f;
hence thesis by A28,A27,GOBOARD5:def 4;
end;
end;
hence thesis;
end;
suppose
A30: i >= len(f:-p);
then j >= len(f:-p) by A8,XXREAL_0:2;
then
A31: LSeg(h,j) = LSeg(f,j + p..f -' len f) by A1,A12,Th31;
len f - p..f <= len f - p..f +1 by XREAL_1:29;
then
A32: len f - p..f <= i by A4,A30,XXREAL_0:2;
then
A33: len f <= i + p..f by A11,NAT_D:52;
A34: i + p..f < j + p..f by A8,XREAL_1:6;
then
A35: len f < j + p..f by A33,XXREAL_0:2;
j + 1 <= len f & p..f < len f by A3,A10,A9,A6,NAT_1:13,XXREAL_0:1;
then j + 1 + p..f < len f + len f by XREAL_1:8;
then j + (1 + p..f) - len f < len f by XREAL_1:19;
then j + p..f - len f + 1 < len f;
then
A36: j + p..f -' len f + 1 < len f by A33,A34,XREAL_1:233,XXREAL_0:2;
A37: i + 1 + p..f < j + p..f by A5,XREAL_1:6;
i + p..f -' len f + 1 = i + p..f + 1 -' len f by A11,A32,NAT_D:38,52
.= i + 1 + p..f -' len f;
then
A38: i + p..f -' len f + 1 < j + p..f -' len f by A35,A37,NAT_D:57;
LSeg(h,i) = LSeg(f,i + p..f -' len f) by A1,A13,A30,Th31;
hence thesis by A31,A38,A36,GOBOARD5:def 4;
end;
end;
hence thesis;
end;
end;
end;
registration
let p be Point of TOP-REAL 2;
let f be non constant standard special_circular_sequence;
cluster Rotate(f,p) -> unfolded;
coherence
proof
per cases;
suppose
not p in rng f;
hence thesis by FINSEQ_6:def 2;
end;
suppose
A1: p in rng f;
let i be Nat such that
A2: 1 <= i and
A3: i + 2 <= len Rotate(f,p);
A4: len f > 4 by GOBOARD7:34;
thus LSeg(Rotate(f,p),i) /\ LSeg(Rotate(f,p),i+1) = {(Rotate(f,p))/.(i+1
)}
proof
A5: i+1 -' 1 + p..f = i + p..f by NAT_D:34
.= i -' 1 + 1 + p..f by A2,XREAL_1:235
.= i -' 1 + p..f + 1;
A6: len f = len Rotate(f,p) by Th14;
i+1 < i+2 by XREAL_1:6;
then
A7: i+1 < len f by A3,A6,XXREAL_0:2;
A8: len (f:-p) = len f - p..f + 1 by A1,FINSEQ_5:50;
per cases by XXREAL_0:1;
suppose
A9: i+1 = len(f:-p);
len(f:-p) + p..f -' len f = len f + 1 - len f by A8,NAT_1:11
,XREAL_1:233
.= 1;
then
A10: LSeg(Rotate(f,p),len(f:-p)) = LSeg(f,1) by A1,A7,A9,Th31;
A11: i < len(f:-p) by A9,XREAL_1:29;
i -' 1 + p..f = len f - p..f + 1 - 1 - 1 + p..f by A2,A8,A9,
XREAL_1:233
.= len f - p..f + p..f - 1
.= len f -' 1 by A4,XREAL_1:233,XXREAL_0:2;
then LSeg(Rotate(f,p),i) = LSeg(f,len f -' 1) by A1,A2,A11,Th24;
hence LSeg(Rotate(f,p),i) /\ LSeg(Rotate(f,p),i+1) = {f/.1} by A9
,A10,Th30,GOBOARD7:34
.= {f/.len f} by FINSEQ_6:def 1
.= {(Rotate(f,p))/.(i+1)} by A1,A9,Th11;
end;
suppose
A12: i+1 < len(f:-p);
then i + 1 < len f - p..f + 1 by A1,FINSEQ_5:50;
then i < len f - p..f by XREAL_1:6;
then i + p..f < len f by XREAL_1:20;
then i -' 1 + 1 + p..f < len f by A2,XREAL_1:235;
then i -' 1 + p..f + 1 + 1 <= len f by NAT_1:13;
then
A13: i -' 1 + p..f + (1+1) <= len f;
i -' 1 + p..f >= p..f & p..f >= 1 by A1,FINSEQ_4:21,NAT_1:11;
then
A14: 1 <= i -' 1 + p..f by XXREAL_0:2;
i+0 < i+1 by XREAL_1:6;
then i < len(f:-p) by A12,XXREAL_0:2;
then
A15: LSeg(Rotate(f,p),i) = LSeg(f,i -' 1 + p..f) by A1,A2,Th24;
LSeg(Rotate(f,p),i+1) = LSeg(f,i+1 -' 1 + p..f) by A1,A12,Th24,
NAT_1:11;
hence LSeg(Rotate(f,p),i) /\ LSeg(Rotate(f,p),i+1) = {f/.(i+1 -' 1 +
p..f)} by A5,A15,A14,A13,TOPREAL1:def 6
.= {(Rotate(f,p))/.(i+1)} by A1,A12,Th9,NAT_1:11;
end;
suppose
A16: len(f:-p) < i+1;
p..f <= len f by A1,FINSEQ_4:21;
then i + 2 + p..f <= len f + len f by A3,A6,XREAL_1:7;
then i + p..f + 2 - len f <= len f by XREAL_1:20;
then
A17: i + p..f - len f + 2 <= len f;
i+1+1 <= len f by A3,Th14;
then
A18: i+1 < len f by NAT_1:13;
i + 1 > len f - p..f + 1 by A1,A16,FINSEQ_5:50;
then len f - p..f < i by XREAL_1:6;
then
A19: len f < i + p..f by XREAL_1:19;
then
A20: i + p..f -' len f = i + p..f - len f by XREAL_1:233;
0 < i + p..f - len f by A19,XREAL_1:50;
then
A21: 0+1 <= i + p..f -' len f by A20,NAT_1:13;
A22: i+1 + p..f -' len f = i + p..f + 1 -' len f
.= i + p..f -' len f + 1 by A19,NAT_D:38;
A23: len(f:-p) <= i by A16,NAT_1:13;
i+0 < i+1 by XREAL_1:6;
then i < len f by A18,XXREAL_0:2;
then
A24: LSeg(Rotate(f,p),i) = LSeg(f,i + p..f -' len f) by A1,A23,Th31;
LSeg (Rotate(f,p),i+1) = LSeg(f,i+1 + p..f -' len f) by A1,A16,A18
,Th31;
hence LSeg(Rotate(f,p),i) /\ LSeg(Rotate(f,p),i+1) = {f/.(i+1 + p..f
-' len f)} by A24,A20,A21,A22,A17,TOPREAL1:def 6
.= {(Rotate(f,p))/.(i+1)} by A1,A7,A16,Th17;
end;
end;
end;
end;
end;
theorem Th32:
p in rng f & 1 <= i & i < p..f implies LSeg(f,i) = LSeg(Rotate(f
,p),i + len f -' p..f)
proof
assume that
A1: p in rng f and
A2: 1 <= i and
A3: i < p..f;
A4: p..f <= len f by A1,FINSEQ_4:21;
A5: i + len f < len f + p..f by A3,XREAL_1:6;
A6: len f <= i + len f by NAT_1:11;
then p.. f <= i + len f by A4,XXREAL_0:2;
then
A7: i + len f -' p..f < len f by A5,NAT_D:54;
len f + 1 <= i + len f by A2,XREAL_1:6;
then len f + 1 -' p..f <= i + len f -' p..f by NAT_D:42;
then len f -' p..f + 1 <= i + len f -' p..f by A4,NAT_D:38;
then len f - p..f + 1 <= i + len f -' p..f by A4,XREAL_1:233;
then
A8: len(f:-p) <= i + len f -' p..f by A1,FINSEQ_5:50;
i + len f -' p..f + p..f -' len f = i + len f -' len f by A4,A6,XREAL_1:235
,XXREAL_0:2
.= i by NAT_D:34;
hence thesis by A1,A8,A7,Th31;
end;
theorem Th33:
L~Rotate(f,p) = L~f
proof
per cases;
suppose
not p in rng f;
hence thesis by FINSEQ_6:def 2;
end;
suppose
A1: p in rng f;
set B = { LSeg(f,i) : 1 <= i & i+1 <= len f };
set A = { LSeg(Rotate(f,p),i) : 1 <= i & i+1 <= len f };
A2: A = B
proof
A3: p..f <= len f by A1,FINSEQ_4:21;
thus A c= B
proof
A4: 1 <= p..f by A1,FINSEQ_4:21;
let x be object;
assume x in A;
then consider i such that
A5: x = LSeg(Rotate(f,p),i) and
A6: 1 <= i and
A7: i+1 <= len f;
A8: i < len f by A7,NAT_1:13;
per cases;
suppose
A9: i < len(f:-p);
then i < len f - p..f + 1 by A1,FINSEQ_5:50;
then i < len f -' p..f + 1 by A3,XREAL_1:233;
then i -' 1 < len f -' p..f by A6,NAT_D:54;
then i -' 1 + p..f < len f by NAT_D:53;
then
A10: i -' 1 + p..f + 1 <= len f by NAT_1:13;
1 + 1 <= i + p..f by A6,A4,XREAL_1:7;
then 1 <= i + p..f -' 1 by NAT_D:55;
then
A11: 1 <= i -' 1 + p..f by A6,NAT_D:38;
LSeg(Rotate(f,p),i) = LSeg(f,i -' 1 + p..f) by A1,A6,A9,Th24;
hence thesis by A5,A11,A10;
end;
suppose
A12: i >= len(f:-p);
then len f - p..f + 1 <= i by A1,FINSEQ_5:50;
then len f -' p..f + 1 <= i by A3,XREAL_1:233;
then 1 + len f -' p..f <= i by A3,NAT_D:38;
then
A13: 1 + len f <= i + p..f by NAT_D:52;
then
A14: 1 <= i + p..f -' len f by NAT_D:55;
i + 1 + p..f <= len f + len f by A3,A7,XREAL_1:7;
then len f <= len f + 1 & i + p..f + 1 -' len f <= len f by NAT_1:11
,NAT_D:53;
then
A15: i + p..f -' len f + 1 <= len f by A13,NAT_D:38,XXREAL_0:2;
LSeg(Rotate(f,p),i) = LSeg(f,i + p..f -' len f) by A1,A8,A12,Th31;
hence thesis by A5,A14,A15;
end;
end;
let x be object;
assume x in B;
then consider i such that
A16: x = LSeg(f,i) and
A17: 1 <= i and
A18: i+1 <= len f;
A19: i < len f by A18,NAT_1:13;
per cases;
suppose
A20: p..f <= i;
i <= i+1 by NAT_1:11;
then
A21: p..f <= i+1 by A20,XXREAL_0:2;
1 <= p..f by A1,FINSEQ_4:21;
then i + 1 < len f + p..f by A19,XREAL_1:8;
then i + 1 -' p..f < len f by A21,NAT_D:54;
then i -' p..f+1 < len f by A20,NAT_D:38;
then
A22: i -' p..f+1 +1 <= len f by NAT_1:13;
1 + p..f <= i+1 by A20,XREAL_1:6;
then 1 <= i+1 -' p..f by NAT_D:55;
then
A23: 1 <= i -' p..f+1 by A20,NAT_D:38;
LSeg(f,i) = LSeg(Rotate(f,p),i -' p..f+1) by A1,A19,A20,Th25;
hence thesis by A16,A23,A22;
end;
suppose
A24: i < p..f;
then i + 1 <= p..f by NAT_1:13;
then i + 1 + len f <= len f + p..f by XREAL_1:6;
then
A25: i + len f + 1 -' p..f <= len f by NAT_D:53;
p..f <= len f & len f <= i + len f by A1,FINSEQ_4:21,NAT_1:11;
then
A26: i + len f -' p..f + 1 <= len f by A25,NAT_D:38,XXREAL_0:2;
1 + p..f <= i + len f by A3,A17,XREAL_1:7;
then
A27: 1 <= i + len f -' p..f by NAT_D:55;
LSeg(f,i) = LSeg(Rotate(f,p),i + len f -' p..f) by A1,A17,A24,Th32;
hence thesis by A16,A27,A26;
end;
end;
len Rotate(f,p) = len f by Th14;
hence thesis by A2;
end;
end;
theorem Th34:
for G being Go-board holds f is_sequence_on G iff Rotate(f,p)
is_sequence_on G
proof
let G be Go-board;
A1: dom f = dom Rotate(f,p) by Th15;
A2: len f = len Rotate(f,p) by Th14;
per cases;
suppose
not p in rng f;
hence thesis by FINSEQ_6:def 2;
end;
suppose
A3: p in rng f;
then
A4: p..f <= len f by FINSEQ_4:21;
A5: 1 <= p..f by A3,FINSEQ_4:21;
thus f is_sequence_on G implies Rotate(f,p) is_sequence_on G
proof
assume
A6: f is_sequence_on G;
thus for n st n in dom Rotate(f,p) ex i,j st [i,j] in Indices G & (
Rotate(f,p))/.n = G*(i,j)
proof
let n;
assume
A7: n in dom Rotate(f,p);
then
A8: 1 <= n by FINSEQ_3:25;
A9: n <= len Rotate(f,p) by A7,FINSEQ_3:25;
per cases;
suppose
A10: len(f:-p) <= n;
then len f - p..f + 1 <= n by A3,FINSEQ_5:50;
then len f -' p..f + 1 <= n by A4,XREAL_1:233;
then len f + 1 -' p..f <= n by A4,NAT_D:38;
then len f + 1 <= n + p..f by NAT_D:52;
then
A11: 1 <= n + p..f -' len f by NAT_D:55;
n + p..f <= len f + len f by A2,A4,A9,XREAL_1:7;
then n + p..f -' len f <= len f by NAT_D:53;
then n + p..f -' len f in dom Rotate(f,p) by A2,A11,FINSEQ_3:25;
then consider i,j such that
A12: [i,j] in Indices G and
A13: f/.(n + p..f -' len f) = G*(i,j) by A1,A6;
take i,j;
thus [i,j] in Indices G by A12;
thus thesis by A2,A3,A9,A10,A13,Th17;
end;
suppose
A14: len(f:-p) >= n;
then len f - p..f + 1 >= n by A3,FINSEQ_5:50;
then len f -' p..f + 1 >= n by A4,XREAL_1:233;
then n -' 1 <= len f -' p..f by NAT_D:53;
then
A15: n -' 1 + p..f <= len f by A4,NAT_D:54;
1 + 1 <= n + p..f by A5,A8,XREAL_1:7;
then 1 <= n + p..f -' 1 by NAT_D:55;
then 1 <= n -' 1 + p..f by A8,NAT_D:38;
then n -' 1 + p..f in dom Rotate(f,p) by A2,A15,FINSEQ_3:25;
then consider i,j such that
A16: [i,j] in Indices G and
A17: f/.(n -' 1 + p..f) = G*(i,j) by A1,A6;
take i,j;
thus [i,j] in Indices G by A16;
thus thesis by A3,A8,A14,A17,Th9;
end;
end;
let n such that
A18: n in dom Rotate(f,p) and
A19: n+1 in dom Rotate(f,p);
A20: 1 <= n by A18,FINSEQ_3:25;
A21: n <= len f by A1,A18,FINSEQ_3:25;
A22: 1 <= n+1 by A19,FINSEQ_3:25;
A23: n+1 <= len f by A1,A19,FINSEQ_3:25;
let m,k,i,j such that
A24: [m,k] in Indices G & [i,j] in Indices G & (Rotate(f,p))/.n = G*
(m,k) & (Rotate(f,p))/.(n+1) = G*(i,j);
thus |.m-i.|+|.k-j.| = 1
proof
per cases;
suppose that
A25: len(f:-p) <= n;
len f - p..f + 1 <= n by A3,A25,FINSEQ_5:50;
then len f -' p..f + 1 <= n by A4,XREAL_1:233;
then len f + 1 -' p..f <= n by A4,NAT_D:38;
then len f + 1 <= n + p..f by NAT_D:52;
then
A26: 1 <= n + p..f -' len f by NAT_D:55;
n + p..f <= len f + len f by A4,A21,XREAL_1:7;
then n + p..f -' len f <= len f by NAT_D:53;
then
A27: n + p..f -' len f in dom f by A26,FINSEQ_3:25;
n <= n+1 by NAT_1:11;
then
A28: len(f:-p) <= n+1 by A25,XXREAL_0:2;
then
A29: len f - p..f + 1 <= n + 1 by A3,FINSEQ_5:50;
then len f - p..f <= n by XREAL_1:6;
then
A30: len f <= n + p..f by XREAL_1:20;
A31: (Rotate(f,p))/.(n+1) = f/.(n+1 + p..f -' len f) by A3,A23,A28,Th17;
A32: n+1 + p..f -' len f = n + p..f + 1 -' len f
.= n + p..f -' len f + 1 by A30,NAT_D:38;
len f -' p..f + 1 <= n+1 by A4,A29,XREAL_1:233;
then len f + 1 -' p..f <= n+1 by A4,NAT_D:38;
then len f + 1 <= n+1 + p..f by NAT_D:52;
then
A33: 1 <= n+1 + p..f -' len f by NAT_D:55;
n+1 + p..f <= len f + len f by A4,A23,XREAL_1:7;
then n+1 + p..f -' len f <= len f by NAT_D:53;
then
A34: n+1 + p..f -' len f in dom f by A33,FINSEQ_3:25;
(Rotate(f,p))/.n = f/.(n + p..f -' len f) by A3,A21,A25,Th17;
hence thesis by A6,A24,A31,A32,A27,A34;
end;
suppose
A35: len(f:-p) > n;
then n <= len f - p..f + 1 by A3,FINSEQ_5:50;
then n <= len f -' p..f + 1 by A4,XREAL_1:233;
then n -' 1 <= len f -' p..f by NAT_D:53;
then
A36: n -' 1 + p..f <= len f by A4,NAT_D:54;
1 + 1 <= n + p..f by A5,A20,XREAL_1:7;
then 1 <= n + p..f -' 1 by NAT_D:55;
then 1 <= n -' 1 + p..f by A20,NAT_D:38;
then
A37: n -' 1 + p..f in dom f by A36,FINSEQ_3:25;
A38: n+1 -' 1 + p..f = n + p..f by NAT_D:34
.= n -' 1 + 1 + p..f by A20,XREAL_1:235
.= n -' 1 + p..f + 1;
A39: len(f:-p) >= n+1 by A35,NAT_1:13;
then
A40: (Rotate(f,p))/.(n+1) = f/.(n+1 -' 1 + p..f) by A3,A22,Th9;
n+1 <= len f - p..f + 1 by A3,A39,FINSEQ_5:50;
then n+1 <= len f -' p..f + 1 by A4,XREAL_1:233;
then n+1 -' 1 <= len f -' p..f by NAT_D:53;
then
A41: n+1 -' 1 + p..f <= len f by A4,NAT_D:54;
1 + 1 <= n+1 + p..f by A5,A22,XREAL_1:7;
then 1 <= n+1 + p..f -' 1 by NAT_D:55;
then 1 <= n+1 -' 1 + p..f by A22,NAT_D:38;
then
A42: n+1 -' 1 + p..f in dom f by A41,FINSEQ_3:25;
(Rotate(f,p))/.n = f/.(n -' 1 + p..f) by A3,A20,A35,Th9;
hence thesis by A6,A24,A40,A38,A37,A42;
end;
end;
end;
assume
A43: Rotate(f,p) is_sequence_on G;
thus for n st n in dom f ex i,j st [i,j] in Indices G & f/.n = G*(i,j)
proof
let n;
assume
A44: n in dom f;
then
A45: 1 <= n by FINSEQ_3:25;
A46: n <= len f by A44,FINSEQ_3:25;
per cases;
suppose
A47: n <= p..f;
n <= n + (len f -' p..f) by NAT_1:11;
then 1 <= n + (len f -' p..f) by A45,XXREAL_0:2;
then
A48: 1 <= n + len f -' p..f by A4,NAT_D:38;
n + len f <= len f + p..f by A47,XREAL_1:6;
then n + len f -' p..f <= len f by NAT_D:53;
then n + len f -' p..f in dom f by A48,FINSEQ_3:25;
then consider i,j such that
A49: [i,j] in Indices G and
A50: (Rotate(f,p))/.(n + len f -' p..f) = G*(i,j) by A1,A43;
take i,j;
thus [i,j] in Indices G by A49;
thus thesis by A3,A45,A47,A50,Th18;
end;
suppose
A51: n >= p..f;
then 1 + p..f <= n + 1 by XREAL_1:6;
then
A52: 1 <= n + 1 -' p..f by NAT_D:55;
n + 1 <= len f + p..f by A5,A46,XREAL_1:7;
then n + 1 -' p..f <= len f by NAT_D:53;
then n + 1 -' p..f in dom f by A52,FINSEQ_3:25;
then consider i,j such that
A53: [i,j] in Indices G and
A54: (Rotate(f,p))/.(n + 1 -' p..f) = G*(i,j) by A1,A43;
take i,j;
thus [i,j] in Indices G by A53;
thus thesis by A3,A46,A51,A54,Th10;
end;
end;
let n such that
A55: n in dom f and
A56: n+1 in dom f;
A57: 1 <= n by A55,FINSEQ_3:25;
A58: 1 <= n+1 by A56,FINSEQ_3:25;
A59: n <= len f by A55,FINSEQ_3:25;
A60: n+1 <= len f by A56,FINSEQ_3:25;
let m,k,i,j such that
A61: [m,k] in Indices G & [i,j] in Indices G & f/.n = G*(m,k) & f/.(n
+1) = G*(i,j);
thus |.m-i.|+|.k-j.| = 1
proof
per cases;
suppose
A62: n < p..f;
n <= n + (len f -' p..f) by NAT_1:11;
then 1 <= n + (len f -' p..f) by A57,XXREAL_0:2;
then
A63: 1 <= n + len f -' p..f by A4,NAT_D:38;
n + len f <= len f + p..f by A62,XREAL_1:6;
then n + len f -' p..f <= len f by NAT_D:53;
then
A64: n + len f -' p..f in dom f by A63,FINSEQ_3:25;
A65: n+1 + len f -' p..f = len f -' p..f + (n+1) by A4,NAT_D:38
.= len f -' p..f + n+1
.= n + len f -' p..f + 1 by A4,NAT_D:38;
n+1 <= n+1 + (len f -' p..f) by NAT_1:11;
then 1 <= n+1 + (len f -' p..f) by A58,XXREAL_0:2;
then
A66: 1 <= n+1 + len f -' p..f by A4,NAT_D:38;
A67: n+1 <= p..f by A62,NAT_1:13;
then
A68: f/.(n+1) = (Rotate(f,p))/.(n+1 + len f -' p..f) by A3,A58,Th18;
n+1 + len f <= len f + p..f by A67,XREAL_1:6;
then n+1 + len f -' p..f <= len f by NAT_D:53;
then
A69: n+1 + len f -' p..f in dom f by A66,FINSEQ_3:25;
f/.n = (Rotate(f,p))/.(n + len f -' p..f) by A3,A57,A62,Th18;
hence thesis by A1,A43,A61,A68,A65,A64,A69;
end;
suppose
A70: n >= p..f;
then 1 + p..f <= n + 1 by XREAL_1:6;
then
A71: 1 <= n + 1 -' p..f by NAT_D:55;
n + 1 <= len f + p..f by A5,A59,XREAL_1:7;
then n + 1 -' p..f <= len f by NAT_D:53;
then
A72: n + 1 -' p..f in dom f by A71,FINSEQ_3:25;
A73: f/.n = (Rotate(f,p))/.(n + 1 -' p..f) by A3,A59,A70,Th10;
A74: n <= n+1 by NAT_1:11;
then
A75: n+1 + 1 -' p..f = n + 1 -' p..f + 1 by A70,NAT_D:38,XXREAL_0:2;
A76: n+1 >= p..f by A70,A74,XXREAL_0:2;
then 1 + p..f <= n+1 + 1 by XREAL_1:6;
then
A77: 1 <= n+1 + 1 -' p..f by NAT_D:55;
n+1 + 1 <= len f + p..f by A5,A60,XREAL_1:7;
then n+1 + 1 -' p..f <= len f by NAT_D:53;
then
A78: n+1 + 1 -' p..f in dom f by A77,FINSEQ_3:25;
f/.(n+1) = (Rotate(f,p))/.(n+1 + 1 -' p..f) by A3,A60,A76,Th10;
hence thesis by A1,A43,A61,A73,A75,A78,A72;
end;
end;
end;
end;
registration
let p be Point of TOP-REAL 2;
let f be standard non empty circular FinSequence of TOP-REAL 2;
cluster Rotate(f,p) -> standard;
coherence
proof
GoB Rotate(f,p) = GoB f & f is_sequence_on GoB f by Th28,GOBOARD5:def 5;
hence Rotate(f,p) is_sequence_on GoB Rotate(f,p) by Th34;
end;
end;
theorem Th35:
for f being non constant standard special_circular_sequence, p,k
st p in rng f & 1 <= k & k < p..f holds left_cell(f,k) = left_cell(Rotate(f,p),
k + len f -' p..f)
proof
let f be non constant standard special_circular_sequence, p,k such that
A1: p in rng f and
A2: 1 <= k and
A3: k < p..f;
set n = k + len f -' p..f;
A4: p..f <= len f by A1,FINSEQ_4:21;
then k < len f by A3,XXREAL_0:2;
then
A5: k+1 <= len f by NAT_1:13;
0 < k by A2;
then
A6: 0+1 < k+1 by XREAL_1:6;
len f <= k + len f by NAT_1:11;
then
A7: n+1 = k + len f + 1 -' p..f by A4,NAT_D:38,XXREAL_0:2;
A8: k+1 <= p..f by A3,NAT_1:13;
then k + 1 + len f <= len f + p..f by XREAL_1:6;
then n+1 <= len f by A7,NAT_D:53;
then
A9: n+1 <= len Rotate(f,p) by Th14;
A10: n+1 = k + 1 + len f -' p..f by A7;
A11: for i1,j1,i2,j2 being Nat st [i1,j1] in Indices GoB Rotate(f
,p) & [i2,j2] in Indices GoB Rotate(f,p) & (Rotate(f,p))/.n = (GoB Rotate(f,p))
*(i1,j1) & (Rotate(f,p))/.(n+1) = (GoB Rotate(f,p))*(i2,j2) holds i1 = i2 & j1+
1 = j2 & left_cell(f,k) = cell(GoB Rotate(f,p),i1-'1,j1) or i1+1 = i2 & j1 = j2
& left_cell(f,k) = cell(GoB Rotate(f,p),i1,j1) or i1 = i2+1 & j1 = j2 &
left_cell(f,k) = cell(GoB Rotate(f,p),i2,j2-'1) or i1 = i2 & j1 = j2+1 &
left_cell(f,k) = cell(GoB Rotate(f,p),i1,j2)
proof
A12: left_cell(f,k) = left_cell(f,k);
let i1,j1,i2,j2 be Nat such that
A13: [i1,j1] in Indices GoB Rotate(f,p) & [i2,j2] in Indices GoB
Rotate(f,p) and
A14: (Rotate(f,p))/.n = (GoB Rotate(f,p))*(i1,j1) & (Rotate(f,p))/.(n+
1) = (GoB Rotate(f,p))*(i2,j2);
A15: GoB Rotate(f,p) = GoB f by Th28;
then
A16: f/.k = (GoB f)*(i1,j1) & f/.(k+1) = (GoB f)*(i2,j2) by A1,A2,A3,A6,A8,A10
,A14,Th18;
then
A17: i1 = i2 & j1+1 = j2 & left_cell(f,k) = cell(GoB f,i1-'1,j1) or i1+1 =
i2 & j1 = j2 & left_cell(f,k) = cell(GoB f,i1,j1) or i1 = i2+1 & j1 = j2 &
left_cell(f,k) = cell(GoB f,i2,j2-'1) or i1 = i2 & j1 = j2+1 & left_cell(f,k) =
cell(GoB f,i1,j2) by A2,A5,A13,A15,A12,GOBOARD5:def 7;
per cases by A2,A5,A13,A15,A16,A12,GOBOARD5:def 7;
case
i1 = i2 & j1+1 = j2;
hence thesis by A17,Th28;
end;
case
i1+1 = i2 & j1 = j2;
hence thesis by A17,Th28;
end;
case
i1 = i2+1 & j1 = j2;
hence thesis by A17,Th28;
end;
case
i1 = i2 & j1 = j2+1;
hence thesis by A17,Th28;
end;
end;
1 + p..f <= k + len f by A2,A4,XREAL_1:7;
then 1 <= n by NAT_D:55;
hence thesis by A9,A11,GOBOARD5:def 7;
end;
theorem Th36:
for f being non constant standard special_circular_sequence
holds LeftComp Rotate(f,p) = LeftComp f
proof
let f be non constant standard special_circular_sequence;
A1: p in rng f implies p..f >= 1 by FINSEQ_4:21;
LeftComp Rotate(f,p) is_a_component_of (L~Rotate(f,p))` by GOBOARD9:def 1;
then
A2: LeftComp Rotate(f,p) is_a_component_of (L~f)` by Th33;
per cases by A1,XXREAL_0:1;
suppose
not p in rng f;
hence thesis by FINSEQ_6:def 2;
end;
suppose
p in rng f & p..f = 1;
then 1 in dom f & f.1 = p by FINSEQ_4:19,FINSEQ_5:6;
then f/.1 = p by PARTFUN1:def 6;
hence thesis by FINSEQ_6:89;
end;
suppose that
A3: p in rng f and
A4: 1 < p..f;
A5: p..f <= len f by A3,FINSEQ_4:21;
then
A6: 1 + p..f <= 1 + len f by XREAL_1:6;
1 + 1 <= p..f by A4,NAT_1:13;
then 1 + 1 + len f <= len f + p..f by XREAL_1:6;
then len f <= len f + 1 & 1 + len f + 1 -' p..f <= len f by NAT_1:11
,NAT_D:53;
then 1 + len f -' p..f + 1 <= len f by A5,NAT_D:38,XXREAL_0:2;
then
A7: 1 + len f -' p..f + 1 <= len Rotate(f,p) by Th14;
left_cell(f,1) = left_cell(Rotate(f,p),1 + len f -' p..f) by A3,A4,Th35;
then Int left_cell(f,1) c= LeftComp Rotate(f,p) by A6,A7,GOBOARD9:21
,NAT_D:55;
hence thesis by A2,GOBOARD9:def 1;
end;
end;
theorem
for f being non constant standard special_circular_sequence holds
RightComp Rotate(f,p) = RightComp f
proof
let f be non constant standard special_circular_sequence;
A1: RightComp f = LeftComp Rev f by GOBOARD9:23;
RightComp Rotate(f,p) = LeftComp Rev Rotate(f,p) by GOBOARD9:23
.= LeftComp Rotate(Rev f,p) by Th29;
hence thesis by A1,Th36;
end;
begin :: Clockwise oriented
Lm1: for f being non constant standard special_circular_sequence st f/.1 =
N-min L~f holds f is clockwise_oriented or Rev f is clockwise_oriented
proof
let f be non constant standard special_circular_sequence such that
A1: f/.1 = N-min L~f;
1+1+1 < len f by GOBOARD7:34,XXREAL_0:2;
then
A2: 2 < len f -' 1 by NAT_D:52;
A3: [i_w_n f, width GoB f] in Indices GoB f by JORDAN5D:def 7;
then
A4: i_w_n f <= len GoB f by MATRIX_0:32;
A5: 1 <= width GoB f by A3,MATRIX_0:32;
A6: (GoB f)*(i_w_n f,width GoB f) = N-min L~f by JORDAN5D:def 7;
A7: len f > 1+1 by GOBOARD7:34,XXREAL_0:2;
then
A8: 1+1 in dom f by FINSEQ_3:25;
then consider i1,j1 being Nat such that
A9: [i1,j1] in Indices GoB f and
A10: f/.2 = (GoB f)*(i1,j1) by GOBOARD5:11;
A11: j1 <= width GoB f by A9,MATRIX_0:32;
A12: 1 <= j1 by A9,MATRIX_0:32;
then
A13: 1 <= width GoB f by A11,XXREAL_0:2;
A14: 1 <= i1 by A9,MATRIX_0:32;
A15: i1 <= len GoB f by A9,MATRIX_0:32;
A16: now
assume
A17: width GoB f = j1;
then (GoB f)*(1,j1)`2 = N-bound L~f by JORDAN5D:40;
then (GoB f)*(i1,j1)`2 = N-bound L~f by A12,A11,A14,A15,GOBOARD5:1;
then (GoB f)*(i1,j1) in N-most L~f by A7,A8,A10,GOBOARD1:1,SPRECT_2:10;
then (N-min L~f)`1 <= (GoB f)*(i1,j1)`1 by PSCOMP_1:39;
hence i_w_n f <= i1 by A6,A12,A4,A14,A17,GOBOARD5:3;
end;
A18: len f > 1 by GOBOARD7:34,XXREAL_0:2;
then
A19: len f in dom f by FINSEQ_3:25;
1 in dom f by A18,FINSEQ_3:25;
then |.i_w_n f-i1.|+|.width GoB f-j1.| = 1 by A1,A3,A6,A8,A9,A10,
GOBOARD5:12;
then |.i_w_n f-i1.|=1 & width GoB f=j1 or |.width GoB f-j1.|=1 & i_w_n f=
i1 by SEQM_3:42;
then
A20: i1 = i_w_n f+1 & width GoB f = j1 or width GoB f = j1+1 & i_w_n f = i1
by A11,A16,SEQM_3:41;
i_e_n f <= len GoB f by JORDAN5D:45;
then i_w_n f < len GoB f by SPRECT_3:27,XXREAL_0:2;
then
A21: 1 <= i_w_n f +1 & i_w_n f +1 <= len GoB f by NAT_1:11,13;
A22: len f -' 1 <= len f by NAT_D:44;
1 <= len f -' 1 by A7,NAT_D:55;
then
A23: len f -' 1 in dom f by A22,FINSEQ_3:25;
then consider i2,j2 being Nat such that
A24: [i2,j2] in Indices GoB f and
A25: f/.(len f -' 1) = (GoB f)*(i2,j2) by GOBOARD5:11;
A26: j2 <= width GoB f by A24,MATRIX_0:32;
A27: 1 <= i2 by A24,MATRIX_0:32;
A28: 1 <= j2 & i2 <= len GoB f by A24,MATRIX_0:32;
A29: now
assume
A30: width GoB f = j2;
then (GoB f)*(1,j2)`2 = N-bound L~f by JORDAN5D:40;
then (GoB f)*(i2,j2)`2 = N-bound L~f by A26,A27,A28,GOBOARD5:1;
then (GoB f)*(i2,j2) in N-most L~f by A7,A23,A25,GOBOARD1:1,SPRECT_2:10;
then (N-min L~f)`1 <= (GoB f)*(i2,j2)`1 by PSCOMP_1:39;
hence i_w_n f <= i2 by A6,A4,A27,A13,A30,GOBOARD5:3;
end;
A31: len f > 4 by GOBOARD7:34;
then
A32: (GoB f)*(i2,j2) in L~f by A23,A25,GOBOARD1:1,XXREAL_0:2;
A33: len f -' 1 + 1 = len f by A31,XREAL_1:235,XXREAL_0:2;
then f/.(len f -' 1 + 1) = f/.1 by FINSEQ_6:def 1;
then |.i2-i_w_n f.|+|.j2-width GoB f.| = 1 by A1,A23,A3,A6,A24,A25,A19,A33,
GOBOARD5:12;
then |.i2-i_w_n f.|=1 & j2=width GoB f or |.j2-width GoB f.|=1 & i2=i_w_n
f by SEQM_3:42;
then i2 = i_w_n f+1 & j2 = width GoB f or j2+1 = width GoB f & i2 = i_w_n f
by A26,A29,SEQM_3:41;
then
(f/.2)`2 = (GoB f)*(1,width GoB f)`2 or (f/.(len f -' 1))`2 = (GoB f)*(
1,width GoB f)`2 by A22,A10,A25,A5,A20,A21,A2,GOBOARD5:1,GOBOARD7:37;
then (f/.2)`2 = N-bound L~f or (f/.(len f -' 1))`2 = N-bound L~f by
JORDAN5D:40;
then
A34: f/.2 in N-most L~f or f/.(len f -' 1) in N-most L~f by A7,A8,A25,A32,
GOBOARD1:1,SPRECT_2:10;
reconsider A = L~Rev f as non empty compact Subset of TOP-REAL 2;
A35: A = L~f by SPPOL_2:22;
len f -' 1 + (1+1) = len f -' 1 + 1 + 1
.= len f + 1 by A31,XREAL_1:235,XXREAL_0:2;
then
A36: (Rev f)/.2 = f/.(len f -' 1) by A23,FINSEQ_5:66;
(Rev f)/.1 = f/.len f by FINSEQ_5:65
.= N-min L~f by A1,FINSEQ_6:def 1
.= N-min A by SPPOL_2:22;
hence thesis by A1,A36,A35,A34,SPRECT_2:30;
end;
registration
let p be Point of TOP-REAL 2;
let f be clockwise_oriented non constant standard special_circular_sequence;
cluster Rotate(f,p) -> clockwise_oriented;
coherence
proof
A1: for i st 1 < i & i < len f holds f/.i <> f/.1 by GOBOARD7:36;
A2: L~Rotate(f,p) = L~f by Th33;
per cases;
suppose
A3: N-min L~f = f/.1;
then Rotate(Rotate(f,p),N-min L~f) = f by A1,Th16;
hence
(Rotate(Rotate(f,p),N-min L~Rotate(f,p)))/.2 in N-most L~Rotate(f,p
) by A2,A3,SPRECT_2:30;
end;
suppose
A4: N-min L~f <> f/.1;
A5: f just_once_values N-min L~f
proof
take n_w_n f;
n_w_n f + 1 <= len f by JORDAN5D:def 15;
then
A6: n_w_n f < len f by NAT_1:13;
A7: 1 <= n_w_n f by JORDAN5D:def 15;
hence
A8: n_w_n f in dom f by A6,FINSEQ_3:25;
thus
A9: N-min L~f = f.n_w_n f by JORDAN5D:def 15
.= f/.n_w_n f by A8,PARTFUN1:def 6;
let z be set;
assume
A10: z in dom f;
then reconsider k = z as Element of NAT;
assume
A11: z <> n_w_n f;
per cases by A11,XXREAL_0:1;
suppose
A12: k < n_w_n f;
1 <= k by A10,FINSEQ_3:25;
hence thesis by A6,A9,A12,GOBOARD7:36;
end;
suppose
A13: k > n_w_n f;
1 < n_w_n f & k <= len f by A4,A7,A9,A10,FINSEQ_3:25,XXREAL_0:1;
hence thesis by A9,A13,GOBOARD7:37;
end;
end;
(Rotate(f,N-min L~f))/.2 in N-most L~f by SPRECT_2:def 4;
hence
(Rotate(Rotate(f,p),N-min L~Rotate(f,p)))/.2 in N-most L~Rotate(f,p
) by A2,A5,FINSEQ_6:105;
end;
end;
end;
theorem
for f being non constant standard special_circular_sequence holds f is
clockwise_oriented or Rev f is clockwise_oriented
proof
let f be non constant standard special_circular_sequence;
per cases;
suppose
N-min L~f = f/.1;
hence thesis by Lm1;
end;
suppose
A1: N-min L~f <> f/.1;
thus thesis
proof
set g = Rotate(f,N-min L~f);
A2: for i st 1 < i & i < len f holds f/.i <> f/.1 by GOBOARD7:36;
N-min L~f in rng f & L~f = L~g by Th33,SPRECT_2:39;
then
A3: g/.1 = N-min L~g by FINSEQ_6:92;
per cases by A3,Lm1;
suppose
g is clockwise_oriented;
then reconsider g as clockwise_oriented non constant standard
special_circular_sequence;
f = Rotate(g,f/.1) by A2,Th16;
hence thesis;
end;
suppose
Rev g is clockwise_oriented;
then reconsider h = Rev g as clockwise_oriented non constant standard
special_circular_sequence;
A4: g just_once_values f/.1
proof
take (f/.1)..g;
N-min L~f in rng f by SPRECT_2:39;
then
A5: f/.1 <> g/.1 by A1,FINSEQ_6:92;
f/.1 in rng f by FINSEQ_6:42;
then
A6: f/.1 in rng g by FINSEQ_6:90,SPRECT_2:39;
hence
A7: (f/.1)..g in dom g by FINSEQ_4:20;
thus
A8: f/.1 = g.((f/.1)..g) by A6,FINSEQ_4:19
.= g/.((f/.1)..g) by A7,PARTFUN1:def 6;
let z be set such that
A9: z in dom g and
A10: z <> (f/.1)..g;
reconsider k = z as Element of NAT by A9;
per cases by A10,XXREAL_0:1;
suppose
A11: k < (f/.1)..g;
(f/.1)..g <= len g & (f/.1)..g <> len g by A6,A5,A8,FINSEQ_4:21
,FINSEQ_6:def 1;
then
A12: (f/.1)..g < len g by XXREAL_0:1;
1 <= k by A9,FINSEQ_3:25;
hence thesis by A8,A11,A12,GOBOARD7:36;
end;
suppose
A13: k > (f/.1)..g;
(f/.1)..g >= 1 by A6,FINSEQ_4:21;
then
A14: (f/.1)..g > 1 by A5,A8,XXREAL_0:1;
k <= len g by A9,FINSEQ_3:25;
hence thesis by A8,A13,A14,GOBOARD7:37;
end;
end;
Rev f = Rev Rotate(g,f/.1) by A2,Th16
.= Rotate(h,f/.1) by A4,FINSEQ_6:106;
hence thesis;
end;
end;
end;
end;