:: Some Remarks on Clockwise Oriented Sequences on Go-boards
:: by Adam Naumowicz and Robert Milewski
::
:: Received March 1, 2002
:: Copyright (c) 2002-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, RCOMP_1, RELAT_2, SPPOL_1, EUCLID, PSCOMP_1,
TOPREAL1, JORDAN9, FINSEQ_4, XXREAL_0, PARTFUN1, ARYTM_3, FUNCT_1,
GOBOARD5, PRE_TOPC, RELAT_1, FINSEQ_6, FINSEQ_1, MATRIX_1, GOBOARD2,
ARYTM_1, XBOOLE_0, JORDAN8, TREES_1, GOBOARD1, MCART_1, COMPLEX1, CARD_1,
RLTOPSP1, TARSKI, SPRECT_2, GOBOARD9, JORDAN2C, TOPS_1, REAL_1, JORDAN5D,
CONNSP_1, TOPREAL2, JORDAN1A, JORDAN6, JORDAN1E, SEQ_4, XXREAL_2, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1,
XREAL_0, REAL_1, NAT_1, FUNCT_1, NAT_D, RELSET_1, PARTFUN1, FINSEQ_1,
FINSEQ_4, MATRIX_0, FINSEQ_6, SEQ_4, STRUCT_0, PRE_TOPC, TOPS_1,
TOPREAL2, CONNSP_1, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, PSCOMP_1,
SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13,
SPPOL_1, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN5D, JORDAN1A,
JORDAN1E, XXREAL_0;
constructors REAL_1, FINSEQ_4, NEWTON, TOPS_1, CONNSP_1, GOBOARD2, PSCOMP_1,
GOBOARD9, JORDAN6, JORDAN5D, JORDAN2C, JORDAN8, GOBRD13, JORDAN9,
JORDAN1A, JORDAN1E, NAT_D, SEQ_4, RELSET_1;
registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_6, STRUCT_0, GOBOARD2,
SPRECT_1, SPRECT_2, REVROT_1, TOPREAL6, JORDAN8, JORDAN1A, FUNCT_1,
EUCLID, JORDAN2C, XREAL_0;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI;
equalities PSCOMP_1;
theorems EUCLID, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, TOPREAL6, GOBOARD5,
JORDAN4, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7, GOBOARD9,
SPPOL_2, REVROT_1, TOPREAL1, GOBRD13, JORDAN9, JORDAN2C, ABSVALUE,
GOBOARD1, TARSKI, TOPREAL3, FINSEQ_3, UNIFORM1, FUNCT_1, JORDAN1B,
SPRECT_5, JORDAN5D, JORDAN1E, JORDAN1F, JORDAN1G, JORDAN1H, TOPREAL8,
GOBRD14, JORDAN1D, GOBOARD6, SPRECT_1, XBOOLE_0, XBOOLE_1, XREAL_1,
JORDAN6, XXREAL_0, PARTFUN1, MATRIX_0, NAT_D, XREAL_0, RLTOPSP1, SEQM_3;
begin :: Preliminaries
reserve i,j,k,n for Nat;
theorem Th1:
for C being compact connected non vertical non horizontal Subset
of TOP-REAL 2 holds (W-min L~Cage(C,n))..Cage(C,n) > 1
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
A1: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:32;
then 1 < (N-max L~Cage(C,n))..Cage(C,n) by SPRECT_2:69;
then 1 < (E-max L~Cage(C,n))..Cage(C,n) by A1,SPRECT_2:70,XXREAL_0:2;
then 1 < (E-min L~Cage(C,n))..Cage(C,n) by A1,SPRECT_2:71,XXREAL_0:2;
then 1 < (S-max L~Cage(C,n))..Cage(C,n) by A1,SPRECT_2:72,XXREAL_0:2;
then 1 < (S-min L~Cage(C,n))..Cage(C,n) by A1,SPRECT_2:73,XXREAL_0:2;
hence thesis by A1,SPRECT_2:74,XXREAL_0:2;
end;
theorem Th2:
for C being compact connected non vertical non horizontal Subset
of TOP-REAL 2 holds (E-max L~Cage(C,n))..Cage(C,n) > 1
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
A1: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:32;
then 1 < (N-max L~Cage(C,n))..Cage(C,n) by SPRECT_2:69;
hence thesis by A1,SPRECT_2:70,XXREAL_0:2;
end;
theorem Th3:
for C being compact connected non vertical non horizontal Subset
of TOP-REAL 2 holds (S-max L~Cage(C,n))..Cage(C,n) > 1
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
A1: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:32;
then 1 < (N-max L~Cage(C,n))..Cage(C,n) by SPRECT_2:69;
then 1 < (E-max L~Cage(C,n))..Cage(C,n) by A1,SPRECT_2:70,XXREAL_0:2;
then 1 < (E-min L~Cage(C,n))..Cage(C,n) by A1,SPRECT_2:71,XXREAL_0:2;
hence thesis by A1,SPRECT_2:72,XXREAL_0:2;
end;
begin :: On bounding points of circular sequences
theorem
for f being non constant standard special_circular_sequence, p being
Point of TOP-REAL 2 st p in rng f holds left_cell(f,p..f) = left_cell(Rotate(f,
p),1)
proof
set n = 1;
let f be non constant standard special_circular_sequence, p be Point of
TOP-REAL 2 such that
A1: p in rng f;
set k = p..f;
len f > 1 by GOBOARD7:34,XXREAL_0:2;
then k < len f by A1,SPRECT_5:7;
then
A2: k+1 <= len f by NAT_1:13;
A3: 1 <= k by A1,FINSEQ_4:21;
A4: 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
Rotate(f,p)/.(1 + 1 + k -' p..f) = Rotate(f,p)/.(n+1) by NAT_D:34;
then
A5: Rotate(f,p)/.(k+1 + 1 -' p..f) = Rotate(f,p)/.(n+1);
A6: left_cell(f,k) = left_cell(f,k );
let i1,j1,i2,j2 be Nat such that
A7: [i1,j1] in Indices GoB Rotate(f,p) & [i2,j2] in Indices GoB Rotate
(f,p) and
A8: Rotate(f,p)/.n = (GoB Rotate(f,p))*(i1,j1) and
A9: Rotate(f,p)/.(n+1) = (GoB Rotate(f,p))*(i2,j2);
A10: GoB Rotate(f,p) = GoB f by REVROT_1:28;
len Rotate(f,p) = len f by FINSEQ_6:179;
then Rotate(f,p)/.(len f) = Rotate(f,p)/.1 by FINSEQ_6:def 1;
then Rotate(f,p)/.(k + len f -' p..f) = Rotate(f,p)/.1 by NAT_D:34;
then
A11: f/.k = (GoB f)*(i1,j1) by A1,A3,A8,A10,FINSEQ_6:183;
k < k+1 by NAT_1:13;
then
A12: f/.(k+1) = (GoB f)*(i2,j2) by A1,A2,A9,A10,A5,FINSEQ_6:175;
then
A13: 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 A3,A2,A7,A10,A11,A6,GOBOARD5:def 7;
per cases by A3,A2,A7,A10,A11,A12,A6,GOBOARD5:def 7;
case
i1 = i2 & j1+1 = j2;
hence thesis by A13,REVROT_1:28;
end;
case
i1+1 = i2 & j1 = j2;
hence thesis by A13,REVROT_1:28;
end;
case
i1 = i2+1 & j1 = j2;
hence thesis by A13,REVROT_1:28;
end;
case
i1 = i2 & j1 = j2+1;
hence thesis by A13,REVROT_1:28;
end;
end;
n+1 <= len Rotate(f,p) by GOBOARD7:34,XXREAL_0:2;
hence thesis by A4,GOBOARD5:def 7;
end;
theorem Th5:
for f being non constant standard special_circular_sequence, p
being Point of TOP-REAL 2 st p in rng f holds right_cell(f,p..f) = right_cell(
Rotate(f,p),1)
proof
set n = 1;
let f be non constant standard special_circular_sequence, p be Point of
TOP-REAL 2 such that
A1: p in rng f;
set k = p..f;
len f > 1 by GOBOARD7:34,XXREAL_0:2;
then k < len f by A1,SPRECT_5:7;
then
A2: k+1 <= len f by NAT_1:13;
A3: 1 <= k by A1,FINSEQ_4:21;
A4: 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 & right_cell(f,k) = cell(GoB Rotate(f,p),i1,j1) or i1+1 = i2 & j1 = j2 &
right_cell(f,k) = cell(GoB Rotate(f,p),i1,j1-'1) or i1 = i2+1 & j1 = j2 &
right_cell(f,k) = cell(GoB Rotate(f,p),i2,j2) or i1 = i2 & j1 = j2+1 &
right_cell(f,k) = cell(GoB Rotate(f,p),i1-'1,j2)
proof
Rotate(f,p)/.(1 + 1 + k -' p..f) = Rotate(f,p)/.(n+1) by NAT_D:34;
then
A5: Rotate(f,p)/.(k+1 + 1 -' p..f) = Rotate(f,p)/.(n+1);
A6: right_cell(f,k) = right_cell(f,k );
let i1,j1,i2,j2 be Nat such that
A7: [i1,j1] in Indices GoB Rotate(f,p) & [i2,j2] in Indices GoB Rotate
(f,p) and
A8: Rotate(f,p)/.n = (GoB Rotate(f,p))*(i1,j1) and
A9: Rotate(f,p)/.(n+1) = (GoB Rotate(f,p))*(i2,j2);
A10: GoB Rotate(f,p) = GoB f by REVROT_1:28;
len Rotate(f,p) = len f by FINSEQ_6:179;
then Rotate(f,p)/.(len f) = Rotate(f,p)/.1 by FINSEQ_6:def 1;
then Rotate(f,p)/.(k + len f -' p..f) = Rotate(f,p)/.1 by NAT_D:34;
then
A11: f/.k = (GoB f)*(i1,j1) by A1,A3,A8,A10,FINSEQ_6:183;
k < k+1 by NAT_1:13;
then
A12: f/.(k+1) = (GoB f)*(i2,j2) by A1,A2,A9,A10,A5,FINSEQ_6:175;
then
A13: i1 = i2 & j1+1 = j2 & right_cell(f,k) = cell(GoB f,i1,j1) or i1+1 =
i2 & j1 = j2 & right_cell(f,k) = cell(GoB f,i1,j1-'1) or i1 = i2+1 & j1 = j2 &
right_cell(f,k) = cell(GoB f,i2,j2) or i1 = i2 & j1 = j2+1 & right_cell(f,k) =
cell(GoB f,i1-'1,j2) by A3,A2,A7,A10,A11,A6,GOBOARD5:def 6;
per cases by A3,A2,A7,A10,A11,A12,A6,GOBOARD5:def 6;
case
i1 = i2 & j1+1 = j2;
hence thesis by A13,REVROT_1:28;
end;
case
i1+1 = i2 & j1 = j2;
hence thesis by A13,REVROT_1:28;
end;
case
i1 = i2+1 & j1 = j2;
hence thesis by A13,REVROT_1:28;
end;
case
i1 = i2 & j1 = j2+1;
hence thesis by A13,REVROT_1:28;
end;
end;
n+1 <= len Rotate(f,p) by GOBOARD7:34,XXREAL_0:2;
hence thesis by A4,GOBOARD5:def 6;
end;
theorem
for C being compact connected non vertical non horizontal non empty
Subset of TOP-REAL 2 holds W-min C in right_cell(Rotate(Cage(C,n),W-min L~Cage(
C,n)),1)
proof
let C be compact connected non vertical non horizontal non empty Subset of
TOP-REAL 2;
set f = Cage(C,n);
set G = Gauge(C,n);
consider j being Nat such that
A1: 1 <= j and
A2: j <= width G and
A3: W-min L~f = G*(1,j) by JORDAN1D:30;
A4: len G >= 4 by JORDAN8:10;
then
A5: 1 <= len G by XXREAL_0:2;
set k = (W-min L~f)..f;
A6: W-min L~f in rng f by SPRECT_2:43;
then
A7: k in dom f & f.k = W-min L~f by FINSEQ_4:19,20;
then
A8: f/.k = W-min L~f by PARTFUN1:def 6;
A9: now
A10: 1 < (W-min L~f)..f by Th1;
A11: 1 in dom f by A6,FINSEQ_3:31;
assume k = len f;
then f/.1 = W-min L~f by A8,FINSEQ_6:def 1;
then f.1 = W-min L~f by A11,PARTFUN1:def 6;
hence contradiction by A11,A10,FINSEQ_4:24;
end;
1 <= len G by A4,XXREAL_0:2;
then
A12: [1,j] in Indices G by A1,A2,MATRIX_0:30;
then
A13: [1,j] in Indices GoB f by JORDAN1H:44;
k <= len f by A6,FINSEQ_4:21;
then k < len f by A9,XXREAL_0:1;
then
A14: k+1 <= len f by NAT_1:13;
f/.k = G*(1,j) by A3,A7,PARTFUN1:def 6;
then
A15: f/.k = (GoB f)*(1,j) by JORDAN1H:44;
set p = W-min C;
A16: f is_sequence_on G by JORDAN9:def 1;
A17: 1 <= k+1 by NAT_1:11;
then
A18: k+1 in dom f by A14,FINSEQ_3:25;
A19: k+1 in dom f by A14,A17,FINSEQ_3:25;
then consider ki,kj being Nat such that
A20: [ki,kj] in Indices G and
A21: f/.(k+1) = G*(ki,kj) by A16,GOBOARD1:def 9;
A22: 1 <= kj & ki <= len G by A20,MATRIX_0:32;
A23: 1 <= k by Th1;
then
A24: (f/.(k+1))`1 = W-bound L~Cage(C,n) by A8,A14,JORDAN1E:22;
then G*(1,j)`1 = G*(ki,kj)`1 by A3,A21,EUCLID:52;
then
A25: ki = 1 by A20,A12,JORDAN1G:7;
2 <= len f by GOBOARD7:34,XXREAL_0:2;
then f/.(k+1) in W-most L~f by A24,A19,GOBOARD1:1,SPRECT_2:12;
then G*(1,j)`2 <= G*(ki,kj)`2 by A3,A21,PSCOMP_1:31;
then
A26: j <= kj by A2,A25,A22,GOBOARD5:4;
[ki,kj] in Indices GoB f & f/.(k+1) = (GoB f)*(ki,kj) by A20,A21,JORDAN1H:44;
then |.1-ki.|+|.j-kj.| = 1 by A6,A18,A13,A15,FINSEQ_4:20,GOBOARD5:12;
then
A27: 0+|.j-kj.| = 1 by A25,ABSVALUE:2;
then
A28: f/.(k+1) = G*(1,j+1) by A21,A25,A26,SEQM_3:41;
A29: kj = j+1 by A26,A27,SEQM_3:41;
then 1 <= j+1 & j+1 <= width G by A20,MATRIX_0:32;
then [1,j+1] in Indices G by A5,MATRIX_0:30;
then
A30: right_cell(f,k,G) = cell(G,1,j) by A3,A16,A23,A8,A14,A12,A28,GOBRD13:22;
A31: now
len G = width G by JORDAN8:def 1;
then
A32: j+1 <= len G by A20,A29,MATRIX_0:32;
1 <= j+1 by A20,A29,MATRIX_0:32;
then
A33: G*(2,j+1)`1 = W-bound C by A32,JORDAN8:11;
assume
A34: not p in right_cell(f,k,G);
j+1 <= width G by A20,A29,MATRIX_0:32;
then
A35: j < width G by NAT_1:13;
A36: 2 <= len G by A4,XXREAL_0:2;
1 < len G by A4,XXREAL_0:2;
then LSeg(G*(1+1,j),G*(1+1,j+1)) c= cell(G,1,j) by A1,A35,GOBOARD5:18;
then
A37: not p in LSeg(G*(2,j),G*(2,j+1)) by A30,A34;
A38: 1 <= j+1 & j+1 <= width G by A20,A29,MATRIX_0:32;
j <= len G by A2,JORDAN8:def 1;
then
A39: G*(2,j)`1 = W-bound C by A1,JORDAN8:11;
p`1 = W-bound C by EUCLID:52;
then
A40: p`2 > G*(2,j+1)`2 or p`2 < G*(2,j)`2 by A37,A39,A33,GOBOARD7:7;
per cases by A1,A2,A40,A38,A36,GOBOARD5:1;
suppose
A41: p`2 > G*(1,j+1)`2;
cell(G,1,j) meets C by A23,A14,A30,JORDAN9:31;
then cell(G,1,j) /\ C <> {} by XBOOLE_0:def 7;
then consider c being object such that
A42: c in cell(G,1,j) /\ C by XBOOLE_0:def 1;
reconsider c as Element of TOP-REAL 2 by A42;
A43: c in cell(G,1,j) by A42,XBOOLE_0:def 4;
A44: c in C by A42,XBOOLE_0:def 4;
then
A45: c`1 >= W-bound C by PSCOMP_1:24;
A46: 1+1 <= len G & j+1 <= width G by A4,A20,A29,MATRIX_0:32,XXREAL_0:2;
then c`1 <= G*(1+1,j)`1 by A1,A43,JORDAN9:17;
then c in W-most C by A39,A44,A45,SPRECT_2:12,XXREAL_0:1;
then
A47: c`2 >= p`2 by PSCOMP_1:31;
c`2 <= G*(1,j+1)`2 by A1,A43,A46,JORDAN9:17;
hence contradiction by A41,A47,XXREAL_0:2;
end;
suppose
A48: p`2 < G*(1,j)`2;
west_halfline p meets L~f by JORDAN1A:54,SPRECT_1:13;
then consider r being object such that
A49: r in west_halfline p and
A50: r in L~f by XBOOLE_0:3;
reconsider r as Element of TOP-REAL 2 by A49;
r in west_halfline p /\ L~f by A49,A50,XBOOLE_0:def 4;
then r`1 = W-bound L~f by JORDAN1A:85,PSCOMP_1:34;
then r in W-most L~f by A50,SPRECT_2:12;
then (W-min L~f)`2 <= r`2 by PSCOMP_1:31;
hence contradiction by A3,A48,A49,TOPREAL1:def 13;
end;
end;
GoB f = G by JORDAN1H:44;
then p in right_cell(f,k) by A23,A14,A31,JORDAN1H:23;
hence thesis by A6,Th5;
end;
theorem
for C being compact connected non vertical non horizontal non empty
Subset of TOP-REAL 2 holds E-max C in right_cell(Rotate(Cage(C,n),E-max L~Cage(
C,n)),1)
proof
let C be compact connected non vertical non horizontal non empty Subset of
TOP-REAL 2;
set f = Cage(C,n);
set G = Gauge(C,n);
consider j being Nat such that
A1: 1 <= j and
A2: j <= width G and
A3: E-max L~f = G*(len G,j) by JORDAN1D:25;
A4: len G >= 4 by JORDAN8:10;
then
A5: 1 <= len G by XXREAL_0:2;
set k = (E-max L~f)..f;
A6: E-max L~f in rng f by SPRECT_2:46;
then
A7: k in dom f & f.k = E-max L~f by FINSEQ_4:19,20;
then
A8: f/.k = E-max L~f by PARTFUN1:def 6;
A9: now
A10: 1 < (E-max L~f)..f by Th2;
A11: 1 in dom f by A6,FINSEQ_3:31;
assume k = len f;
then f/.1 = E-max L~f by A8,FINSEQ_6:def 1;
then f.1 = E-max L~f by A11,PARTFUN1:def 6;
hence contradiction by A11,A10,FINSEQ_4:24;
end;
f/.k = G*(len G,j) by A3,A7,PARTFUN1:def 6;
then
A12: f/.k = (GoB f)*(len G,j) by JORDAN1H:44;
k <= len f by A6,FINSEQ_4:21;
then k < len f by A9,XXREAL_0:1;
then
A13: k+1 <= len f by NAT_1:13;
A14: 1 <= len G by A4,XXREAL_0:2;
then
A15: [len G,j] in Indices G by A1,A2,MATRIX_0:30;
1 <= (j-'1)+1 & (j-'1)+1 <= width G by A1,A2,XREAL_1:235;
then
A16: [len G,(j-'1)+1] in Indices G by A14,MATRIX_0:30;
set p = E-max C;
A17: f is_sequence_on G by JORDAN9:def 1;
A18: 1 <= k+1 by NAT_1:11;
then
A19: k+1 in dom f by A13,FINSEQ_3:25;
A20: k+1 in dom f by A13,A18,FINSEQ_3:25;
then consider ki,kj being Nat such that
A21: [ki,kj] in Indices G and
A22: f/.(k+1) = G*(ki,kj) by A17,GOBOARD1:def 9;
A23: [ki,kj] in Indices GoB f & f/.(k+1) = (GoB f)*(ki,kj) by A21,A22,
JORDAN1H:44;
A24: 1 <= k by Th2;
then
A25: (f/.(k+1))`1 = E-bound L~Cage(C,n) by A8,A13,JORDAN1E:20;
then G*(len G,j)`1 = G*(ki,kj)`1 by A3,A22,EUCLID:52;
then
A26: ki = len G by A21,A15,JORDAN1G:7;
A27: kj <= width G & 1 <= ki by A21,MATRIX_0:32;
[len G,j] in Indices GoB f by A15,JORDAN1H:44;
then |.len G-ki.|+|.j-kj.| = 1 by A6,A19,A12,A23,FINSEQ_4:20,GOBOARD5:12;
then
A28: 0+|.j-kj.| = 1 by A26,ABSVALUE:2;
2 <= len f by GOBOARD7:34,XXREAL_0:2;
then f/.(k+1) in E-most L~f by A25,A20,GOBOARD1:1,SPRECT_2:13;
then G*(len G,j)`2 >= G*(ki,kj)`2 by A3,A22,PSCOMP_1:47;
then j >= kj by A1,A26,A27,GOBOARD5:4;
then j=kj+1 by A28,SEQM_3:41;
then kj = j-1;
then
A29: kj = j-'1 by A1,XREAL_1:233;
then
A30: 1 <= j-'1 by A21,MATRIX_0:32;
A31: j-'1 <= width G by A21,A29,MATRIX_0:32;
f/.k = G*(len G,(j-'1)+1) by A1,A3,A8,XREAL_1:235;
then
A32: right_cell(f,k,G) = cell(G,len G-'1,j-'1) by A17,A24,A13,A21,A22,A26,A29
,A16,GOBRD13:28;
A33: now
j-'1 <= len G by A31,JORDAN8:def 1;
then
A34: G*(len G-'1,j-'1)`1 = E-bound C by A30,JORDAN8:12;
j <= len G by A2,JORDAN8:def 1;
then
A35: G*(len G-'1,j)`1 = E-bound C by A1,JORDAN8:12;
assume
A36: not p in right_cell(f,k,G);
A37: 1 < len G by A4,XXREAL_0:2;
then
A38: 1<=len G-'1 by NAT_D:49;
A39: len G-'1 <= len G by NAT_D:50;
then
A40: G*(1,j)`2 = G*(len G-'1,j)`2 & G*(1,j-'1)`2 = G*(len G-'1,j-'1)`2 by A1,A2
,A30,A31,A38,GOBOARD5:1;
j-'1<j by A30,NAT_D:51;
then j-'1 < width G by A2,XXREAL_0:2;
then LSeg(G*(len G-'1,j-'1),G*(len G-'1,j-'1+1)) c= cell(G,len G-'1,j-'1)
by A30,A38,A39,GOBOARD5:19;
then not p in LSeg(G*(len G-'1,j-'1),G*(len G-'1,j-'1+1)) by A32,A36;
then
A41: not p in LSeg(G*(len G-'1,j-'1),G*(len G-'1,j)) by A1,XREAL_1:235;
p`1 = E-bound C by EUCLID:52;
then
A42: p`2 > G*(len G-'1,j)`2 or p`2 < G*(len G-'1,j-'1)`2 by A41,A34,A35,
GOBOARD7:7;
per cases by A1,A2,A5,A30,A31,A42,A40,GOBOARD5:1;
suppose
A43: p`2 < G*(len G,j-'1)`2;
A44: 1 <= j-'1 & (j-'1)+1 <= width G by A1,A2,A21,A29,MATRIX_0:32,XREAL_1:235;
cell(G,len G-'1,j-'1) meets C by A24,A13,A32,JORDAN9:31;
then cell(G,len G-'1,j-'1) /\ C <> {} by XBOOLE_0:def 7;
then consider c being object such that
A45: c in cell(G,len G-'1,j-'1) /\ C by XBOOLE_0:def 1;
reconsider c as Element of TOP-REAL 2 by A45;
A46: 1<=len G-'1 & (len G-'1)+1 <= len G by A37,NAT_D:49,XREAL_1:235;
A47: c in cell(G,len G-'1,j-'1) by A45,XBOOLE_0:def 4;
then
A48: G*(len G-'1,j-'1)`1 <= c`1 by A46,A44,JORDAN9:17;
A49: c in C by A45,XBOOLE_0:def 4;
then c`1 <= E-bound C by PSCOMP_1:24;
then c in E-most C by A34,A49,A48,SPRECT_2:13,XXREAL_0:1;
then
A50: c`2 <= p`2 by PSCOMP_1:47;
G*(len G-'1,j-'1)`2 <= c`2 by A47,A46,A44,JORDAN9:17;
then G*(1,j-'1)`2 <= c`2 by A30,A31,A38,A39,GOBOARD5:1;
then G*(len G,j-'1)`2 <= c`2 by A5,A30,A31,GOBOARD5:1;
hence contradiction by A43,A50,XXREAL_0:2;
end;
suppose
A51: p`2 > G*(len G,j)`2;
east_halfline p meets L~f by JORDAN1A:52,SPRECT_1:14;
then consider r being object such that
A52: r in east_halfline p and
A53: r in L~f by XBOOLE_0:3;
reconsider r as Element of TOP-REAL 2 by A52;
r in east_halfline p /\ L~f by A52,A53,XBOOLE_0:def 4;
then r`1 = E-bound L~f by JORDAN1A:83,PSCOMP_1:50;
then r in E-most L~f by A53,SPRECT_2:13;
then (E-max L~f)`2 >= r`2 by PSCOMP_1:47;
hence contradiction by A3,A51,A52,TOPREAL1:def 11;
end;
end;
GoB f = G by JORDAN1H:44;
then p in right_cell(f,k) by A24,A13,A33,JORDAN1H:23;
hence thesis by A6,Th5;
end;
theorem
for C being compact connected non vertical non horizontal non empty
Subset of TOP-REAL 2 holds S-max C in right_cell(Rotate(Cage(C,n),S-max L~Cage(
C,n)),1)
proof
let C be compact connected non vertical non horizontal non empty Subset of
TOP-REAL 2;
set f = Cage(C,n);
set G = Gauge(C,n);
consider j being Nat such that
A1: 1 <= j and
A2: j <= len G and
A3: S-max L~f = G*(j,1) by JORDAN1D:28;
A4: f is_sequence_on G by JORDAN9:def 1;
set k = (S-max L~f)..f;
A5: S-max L~f in rng f by SPRECT_2:42;
then
A6: k in dom f & f.k = S-max L~f by FINSEQ_4:19,20;
then
A7: f/.k = S-max L~f by PARTFUN1:def 6;
A8: now
A9: 1 < (S-max L~f)..f by Th3;
A10: 1 in dom f by A5,FINSEQ_3:31;
assume k = len f;
then f/.1 = S-max L~f by A7,FINSEQ_6:def 1;
then f.1 = S-max L~f by A10,PARTFUN1:def 6;
hence contradiction by A10,A9,FINSEQ_4:24;
end;
k <= len f by A5,FINSEQ_4:21;
then k < len f by A8,XXREAL_0:1;
then
A11: k+1 <= len f by NAT_1:13;
A12: f/.k = G*(j-'1+1,1) by A1,A3,A7,XREAL_1:235;
f/.k = G*(j,1) by A3,A6,PARTFUN1:def 6;
then
A13: f/.k = (GoB f)*(j,1) by JORDAN1H:44;
set p = S-max C;
A14: len G = width G by JORDAN8:def 1;
A15: len G >= 4 by JORDAN8:10;
then
A16: 1 <= len G by XXREAL_0:2;
A17: 1 <= k+1 by NAT_1:11;
then
A18: k+1 in dom f by A11,FINSEQ_3:25;
A19: k+1 in dom f by A11,A17,FINSEQ_3:25;
then consider kj,ki being Nat such that
A20: [kj,ki] in Indices G and
A21: f/.(k+1) = G*(kj,ki) by A4,GOBOARD1:def 9;
A22: [kj,ki] in Indices GoB f & f/.(k+1) = (GoB f)*(kj,ki) by A20,A21,
JORDAN1H:44;
A23: ki <= width G by A20,MATRIX_0:32;
A24: 1 <= kj by A20,MATRIX_0:32;
len G = width G by JORDAN8:def 1;
then
A25: [j,1] in Indices G by A1,A2,A16,MATRIX_0:30;
then
A26: [j-'1+1,1] in Indices G by A1,XREAL_1:235;
A27: 1 <= k by Th3;
then
A28: (f/.(k+1))`2 = S-bound L~Cage(C,n) by A7,A11,JORDAN1E:21;
then G*(j,1)`2 = G*(kj,ki)`2 by A3,A21,EUCLID:52;
then
A29: ki = 1 by A20,A25,JORDAN1G:6;
[j,1] in Indices GoB f by A25,JORDAN1H:44;
then |.1-ki.|+|.j-kj.| = 1 by A5,A18,A13,A22,FINSEQ_4:20,GOBOARD5:12;
then
A30: 0+|.j-kj.| = 1 by A29,ABSVALUE:2;
A31: kj <= len G by A20,MATRIX_0:32;
2 <= len f by GOBOARD7:34,XXREAL_0:2;
then f/.(k+1) in S-most L~f by A28,A19,GOBOARD1:1,SPRECT_2:11;
then G*(j,1)`1 >= G*(kj,ki)`1 by A3,A21,PSCOMP_1:55;
then kj <= j by A1,A29,A23,A31,GOBOARD5:3;
then kj+1 = j by A30,SEQM_3:41;
then
A32: kj = j-1;
then kj = j-'1 by A24,NAT_D:39;
then
A33: [j-'1,1] in Indices G by A16,A24,A31,A14,MATRIX_0:30;
f/.(k+1) = G*(j-'1,1) by A21,A29,A24,A32,NAT_D:39;
then
A34: right_cell(f,k,G) = cell(G,j-'1,1) by A4,A27,A11,A33,A26,A12,GOBRD13:26;
A35: now
1 < len G by A15,XXREAL_0:2;
then
A36: 1 < width G by JORDAN8:def 1;
assume
A37: not p in right_cell(f,k,G);
A38: 1 <= j-'1 by A24,A32,NAT_D:39;
then j-'1 < j by NAT_D:51;
then j-'1 < len G by A2,XXREAL_0:2;
then LSeg(G*(j-'1,1+1),G*(j-'1+1,1+1)) c= cell(G,j-'1,1) by A36,A38,
GOBOARD5:21;
then LSeg(G*(j-'1,2),G*(j,2)) c= cell(G,j-'1,1) by A1,XREAL_1:235;
then
A39: not p in LSeg(G*(j-'1,2),G*(j,2)) by A34,A37;
len G = width G by JORDAN8:def 1;
then
A40: 2 <= width G by A15,XXREAL_0:2;
A41: len G = width G by JORDAN8:def 1;
A42: j-'1 <= len G by A24,A31,A32,NAT_D:39;
then
A43: G*(j-'1,2)`2 = S-bound C by A38,JORDAN8:13;
G*(j,2)`2 = S-bound C & p`2 = S-bound C by A1,A2,EUCLID:52,JORDAN8:13;
then
A44: p`1 > G*(j,2)`1 or p`1 < G*(j-'1,2)`1 by A39,A43,GOBOARD7:8;
per cases by A1,A2,A38,A42,A44,A40,GOBOARD5:2;
suppose
A45: p`1 < G*(j-'1,1)`1;
cell(G,j-'1,1) meets C by A27,A11,A34,JORDAN9:31;
then cell(G,j-'1,1) /\ C <> {} by XBOOLE_0:def 7;
then consider c being object such that
A46: c in cell(G,j-'1,1) /\ C by XBOOLE_0:def 1;
reconsider c as Element of TOP-REAL 2 by A46;
A47: c in cell(G,j-'1,1) by A46,XBOOLE_0:def 4;
A48: c in C by A46,XBOOLE_0:def 4;
then
A49: c`2 >= S-bound C by PSCOMP_1:24;
A50: j-'1+1 <= len G & 1+1 <= width G by A1,A2,A15,A41,XREAL_1:235,XXREAL_0:2;
then c`2 <= G*(j-'1,1+1)`2 by A38,A47,JORDAN9:17;
then c in S-most C by A43,A48,A49,SPRECT_2:11,XXREAL_0:1;
then
A51: c`1 <= p`1 by PSCOMP_1:55;
G*(j-'1,1)`1 <= c`1 by A38,A47,A50,JORDAN9:17;
hence contradiction by A45,A51,XXREAL_0:2;
end;
suppose
A52: p`1 > G*(j,1)`1;
south_halfline p meets L~f by JORDAN1A:53,SPRECT_1:12;
then consider r being object such that
A53: r in south_halfline p and
A54: r in L~f by XBOOLE_0:3;
reconsider r as Element of TOP-REAL 2 by A53;
r in south_halfline p /\ L~f by A53,A54,XBOOLE_0:def 4;
then r`2 = S-bound L~f by JORDAN1A:84,PSCOMP_1:58;
then r in S-most L~f by A54,SPRECT_2:11;
then (S-max L~f)`1 >= r`1 by PSCOMP_1:55;
hence contradiction by A3,A52,A53,TOPREAL1:def 12;
end;
end;
GoB f = G by JORDAN1H:44;
then p in right_cell(f,k) by A27,A11,A35,JORDAN1H:23;
hence thesis by A5,Th5;
end;
begin :: On clockwise oriented sequences
theorem Th9:
for f being clockwise_oriented non constant standard
special_circular_sequence for p being Point of TOP-REAL 2 st p`1 < W-bound (L~f
) holds p in LeftComp f
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let p be Point of TOP-REAL 2;
set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
assume
A2: p`1 < W-bound (L~f);
N-min L~f in rng f by SPRECT_2:39;
then g/.1 = N-min L~g by A1,FINSEQ_6:92;
then p in LeftComp g by A1,A2,JORDAN2C:110;
hence thesis by REVROT_1:36;
end;
theorem Th10:
for f being clockwise_oriented non constant standard
special_circular_sequence for p being Point of TOP-REAL 2 st p`1 > E-bound (L~f
) holds p in LeftComp f
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let p be Point of TOP-REAL 2;
set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
assume
A2: p`1 > E-bound (L~f);
N-min L~f in rng f by SPRECT_2:39;
then g/.1 = N-min L~g by A1,FINSEQ_6:92;
then p in LeftComp g by A1,A2,JORDAN2C:111;
hence thesis by REVROT_1:36;
end;
theorem Th11:
for f being clockwise_oriented non constant standard
special_circular_sequence for p being Point of TOP-REAL 2 st p`2 < S-bound (L~f
) holds p in LeftComp f
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let p be Point of TOP-REAL 2;
set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
assume
A2: p`2 < S-bound (L~f);
N-min L~f in rng f by SPRECT_2:39;
then g/.1 = N-min L~g by A1,FINSEQ_6:92;
then p in LeftComp g by A1,A2,JORDAN2C:112;
hence thesis by REVROT_1:36;
end;
theorem Th12:
for f being clockwise_oriented non constant standard
special_circular_sequence for p being Point of TOP-REAL 2 st p`2 > N-bound (L~f
) holds p in LeftComp f
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let p be Point of TOP-REAL 2;
set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
assume
A2: p`2 > N-bound (L~f);
N-min L~f in rng f by SPRECT_2:39;
then g/.1 = N-min L~g by A1,FINSEQ_6:92;
then p in LeftComp g by A1,A2,JORDAN2C:113;
hence thesis by REVROT_1:36;
end;
theorem Th13:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G for i,j,k
being Nat st 1 <= k & k+1 <= len f & [i,j] in Indices G & [i+1,j] in
Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j) holds j < width G
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
assume
A1: f is_sequence_on G;
let i,j,k be Nat;
assume that
A2: 1 <= k & k+1 <= len f and
A3: [i,j] in Indices G and
A4: [i+1,j] in Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j);
assume
A5: j >= width G;
j <= width G by A3,MATRIX_0:32;
then
A6: j = width G by A5,XXREAL_0:1;
A7: i <= len G by A3,MATRIX_0:32;
right_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,A4,GOBRD13:26;
then right_cell(f,k,G)\L~f is not bounded by A7,A6,JORDAN1A:27,TOPREAL6:90;
then RightComp f is not bounded by A1,A2,JORDAN9:27,RLTOPSP1:42;
then BDD L~f is not bounded by GOBRD14:37;
hence contradiction by JORDAN2C:106;
end;
theorem Th14:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G for i,j,k
being Nat st 1 <= k & k+1 <= len f & [i,j] in Indices G & [i,j+1] in
Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1) holds i < len G
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
assume
A1: f is_sequence_on G;
let i,j,k be Nat;
assume that
A2: 1 <= k & k+1 <= len f and
A3: [i,j] in Indices G and
A4: [i,j+1] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1);
assume
A5: i >= len G;
i <= len G by A3,MATRIX_0:32;
then
A6: i = len G by A5,XXREAL_0:1;
A7: j <= width G by A3,MATRIX_0:32;
right_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,A4,GOBRD13:22;
then right_cell(f,k,G)\L~f is not bounded by A7,A6,JORDAN1B:34,TOPREAL6:90;
then RightComp f is not bounded by A1,A2,JORDAN9:27,RLTOPSP1:42;
then BDD L~f is not bounded by GOBRD14:37;
hence contradiction by JORDAN2C:106;
end;
theorem Th15:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G for i,j,k
being Nat st 1 <= k & k+1 <= len f & [i,j] in Indices G & [i+1,j] in
Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j) holds j > 1
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
assume
A1: f is_sequence_on G;
let i,j,k be Nat;
assume that
A2: 1 <= k & k+1 <= len f and
A3: [i,j] in Indices G and
A4: [i+1,j] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j);
assume
A5: j <= 1;
1 <= j by A3,MATRIX_0:32;
then j = 1 by A5,XXREAL_0:1;
then
A6: j-'1 = 0 by XREAL_1:232;
A7: i <= len G by A3,MATRIX_0:32;
right_cell(f,k,G) = cell(G,i,j-'1) by A1,A2,A3,A4,GOBRD13:24;
then right_cell(f,k,G)\L~f is not bounded by A7,A6,JORDAN1A:26,TOPREAL6:90;
then RightComp f is not bounded by A1,A2,JORDAN9:27,RLTOPSP1:42;
then BDD L~f is not bounded by GOBRD14:37;
hence contradiction by JORDAN2C:106;
end;
theorem Th16:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G for i,j,k
being Nat st 1 <= k & k+1 <= len f & [i,j] in Indices G & [i,j+1] in
Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j) holds i > 1
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
assume
A1: f is_sequence_on G;
let i,j,k be Nat;
assume that
A2: 1 <= k & k+1 <= len f and
A3: [i,j] in Indices G and
A4: [i,j+1] in Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j);
assume
A5: i <= 1;
1 <= i by A3,MATRIX_0:32;
then i = 1 by A5,XXREAL_0:1;
then
A6: i-'1 = 0 by XREAL_1:232;
A7: j <= width G by A3,MATRIX_0:32;
right_cell(f,k,G) = cell(G,i-'1,j) by A1,A2,A3,A4,GOBRD13:28;
then right_cell(f,k,G)\L~f is not bounded by A7,A6,JORDAN1B:33,TOPREAL6:90;
then RightComp f is not bounded by A1,A2,JORDAN9:27,RLTOPSP1:42;
then BDD L~f is not bounded by GOBRD14:37;
hence contradiction by JORDAN2C:106;
end;
theorem Th17:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G for i,j,k
being Nat st 1 <= k & k+1 <= len f & [i,j] in Indices G & [i+1,j] in
Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j) holds (f/.k)`2 <> N-bound L~f
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
assume
A1: f is_sequence_on G;
let i,j,k be Nat;
assume that
A2: 1 <= k & k+1 <= len f and
A3: [i,j] in Indices G and
A4: [i+1,j] in Indices G and
A5: f/.k = G*(i+1,j) and
A6: f/.(k+1) = G*(i,j) and
A7: (f/.k)`2 = N-bound L~f;
A8: right_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,A4,A5,A6,GOBRD13:26;
A9: j <= width G by A4,MATRIX_0:32;
A10: 1 <= i+1 & 1 <= j by A4,MATRIX_0:32;
set p = 1/2*(G*(i,j)+G*(i+1,j+1));
A11: 0+1 <= i & 1 <= j by A3,MATRIX_0:32;
A12: j <= width G by A3,MATRIX_0:32;
A13: i+1 <= len G by A4,MATRIX_0:32;
per cases by A12,XXREAL_0:1;
suppose
j = width G;
hence contradiction by A1,A2,A3,A4,A5,A6,Th13;
end;
suppose
A14: j < width G;
i < len G by A13,NAT_1:13;
then
A15: Int cell(G,i,j) = {|[r,s]| where r,s is Real:
G*(i,1)`1 < r & r < G*
(i+1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2 } by A11,A14,GOBOARD6:26;
j+1 <= width G by A14,NAT_1:13;
then
A16: p in Int right_cell(f,k,G) by A11,A13,A8,GOBOARD6:31;
then consider r,s be Real such that
A17: p = |[r,s]| and
G*(i,1)`1 < r and
r < G*(i+1,1)`1 and
A18: G*(1,j)`2 < s and
s < G*(1,j+1)`2 by A8,A15;
p`2 = s by A17,EUCLID:52;
then p`2 > N-bound L~f by A5,A7,A13,A10,A9,A18,GOBOARD5:1;
then
A19: p in LeftComp f by Th12;
Int right_cell(f,k,G) c= RightComp f by A1,A2,JORDAN1H:25;
then p in LeftComp f /\ RightComp f by A16,A19,XBOOLE_0:def 4;
then LeftComp f meets RightComp f by XBOOLE_0:def 7;
hence contradiction by GOBRD14:14;
end;
end;
theorem Th18:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G for i,j,k
being Nat st 1 <= k & k+1 <= len f & [i,j] in Indices G & [i,j+1] in
Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1) holds (f/.k)`1 <> E-bound L~f
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
assume
A1: f is_sequence_on G;
let i,j,k be Nat;
assume that
A2: 1 <= k & k+1 <= len f and
A3: [i,j] in Indices G and
A4: [i,j+1] in Indices G and
A5: f/.k = G*(i,j) and
A6: f/.(k+1) = G*(i,j+1) and
A7: (f/.k)`1 = E-bound L~f;
A8: right_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,A4,A5,A6,GOBRD13:22;
A9: j <= width G by A3,MATRIX_0:32;
A10: 0+1 <= i & 1 <= j by A3,MATRIX_0:32;
set p = 1/2*(G*(i,j)+G*(i+1,j+1));
A11: i <= len G by A3,MATRIX_0:32;
A12: j+1 <= width G by A4,MATRIX_0:32;
per cases by A11,XXREAL_0:1;
suppose
i = len G;
hence contradiction by A1,A2,A3,A4,A5,A6,Th14;
end;
suppose
A13: i < len G;
j < width G by A12,NAT_1:13;
then
A14: Int cell(G,i,j) = {|[r,s]| where r,s is Real:
G*(i,1)`1 < r & r < G*
(i+1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2 } by A10,A13,GOBOARD6:26;
i+1 <= len G by A13,NAT_1:13;
then
A15: p in Int right_cell(f,k,G) by A10,A12,A8,GOBOARD6:31;
then consider r,s be Real such that
A16: p = |[r,s]| and
A17: G*(i,1)`1 < r and
r < G*(i+1,1)`1 and
G*(1,j)`2 < s and
s < G*(1,j+1)`2 by A8,A14;
p`1 = r by A16,EUCLID:52;
then p`1 > E-bound L~f by A5,A7,A11,A10,A9,A17,GOBOARD5:2;
then
A18: p in LeftComp f by Th10;
Int right_cell(f,k,G) c= RightComp f by A1,A2,JORDAN1H:25;
then p in LeftComp f /\ RightComp f by A15,A18,XBOOLE_0:def 4;
then LeftComp f meets RightComp f by XBOOLE_0:def 7;
hence contradiction by GOBRD14:14;
end;
end;
theorem Th19:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G for i,j,k
being Nat st 1 <= k & k+1 <= len f & [i,j] in Indices G & [i+1,j] in
Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j) holds (f/.k)`2 <> S-bound L~f
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
assume
A1: f is_sequence_on G;
let i,j,k be Nat;
assume that
A2: 1 <= k & k+1 <= len f and
A3: [i,j] in Indices G and
A4: [i+1,j] in Indices G and
A5: f/.k = G*(i,j) and
A6: f/.(k+1) = G*(i+1,j) and
A7: (f/.k)`2 = S-bound L~f;
A8: right_cell(f,k,G) = cell(G,i,j-'1) by A1,A2,A3,A4,A5,A6,GOBRD13:24;
A9: i <= len G by A3,MATRIX_0:32;
A10: j <= width G by A3,MATRIX_0:32;
A11: i+1 <= len G by A4,MATRIX_0:32;
set p = 1/2*(G*(i,j-'1)+G*(i+1,j));
A12: 0+1 <= i by A3,MATRIX_0:32;
A13: 1 <= j by A3,MATRIX_0:32;
then
A14: j-'1+1 = j by XREAL_1:235;
per cases by A13,XXREAL_0:1;
suppose
j = 1;
hence contradiction by A1,A2,A3,A4,A5,A6,Th15;
end;
suppose
j > 1;
then j >= 1+1 by NAT_1:13;
then
A15: j-1 >= 1+1-1 by XREAL_1:9;
j < width G + 1 by A10,NAT_1:13;
then
A16: j-1 < width G+1-1 by XREAL_1:9;
i < len G by A11,NAT_1:13;
then
A17: Int cell(G,i,j-'1) = {|[r,s]| where r,s is Real:
G*(i,1)`1 < r & r <
G*(i+1,1)`1 & G*(1,j-'1)`2 < s & s < G*(1,j)`2 } by A12,A14,A15,A16,GOBOARD6:26
;
A18: p in Int right_cell(f,k,G) by A12,A10,A11,A8,A14,A15,GOBOARD6:31;
then consider r,s be Real such that
A19: p = |[r,s]| and
G*(i,1)`1 < r and
r < G*(i+1,1)`1 and
G*(1,j-'1)`2 < s and
A20: s < G*(1,j)`2 by A8,A17;
p`2 = s by A19,EUCLID:52;
then p`2 < S-bound L~f by A5,A7,A12,A9,A13,A10,A20,GOBOARD5:1;
then
A21: p in LeftComp f by Th11;
Int right_cell(f,k,G) c= RightComp f by A1,A2,JORDAN1H:25;
then p in LeftComp f /\ RightComp f by A18,A21,XBOOLE_0:def 4;
then LeftComp f meets RightComp f by XBOOLE_0:def 7;
hence contradiction by GOBRD14:14;
end;
end;
theorem Th20:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G for i,j,k
being Nat st 1 <= k & k+1 <= len f & [i,j] in Indices G & [i,j+1] in
Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j) holds (f/.k)`1 <> W-bound L~f
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
assume
A1: f is_sequence_on G;
let i,j,k be Nat;
assume that
A2: 1 <= k & k+1 <= len f and
A3: [i,j] in Indices G and
A4: [i,j+1] in Indices G and
A5: f/.k = G*(i,j+1) and
A6: f/.(k+1) = G*(i,j) and
A7: (f/.k)`1 = W-bound L~f;
A8: right_cell(f,k,G) = cell(G,i-'1,j) by A1,A2,A3,A4,A5,A6,GOBRD13:28;
A9: 1 <= i & i <= len G by A4,MATRIX_0:32;
A10: 1 <= j by A3,MATRIX_0:32;
A11: 1 <= j+1 by A4,MATRIX_0:32;
A12: j+1 <= width G by A4,MATRIX_0:32;
set p = 1/2*(G*(i-'1,j)+G*(i,j+1));
A13: i <= len G by A3,MATRIX_0:32;
A14: 0+1 <= i by A3,MATRIX_0:32;
then
A15: i-'1+1 = i by XREAL_1:235;
per cases by A14,XXREAL_0:1;
suppose
i = 1;
hence contradiction by A1,A2,A3,A4,A5,A6,Th16;
end;
suppose
i > 1;
then i >= 1+1 by NAT_1:13;
then
A16: i-1 >= 1+1-1 by XREAL_1:9;
i < len G + 1 by A13,NAT_1:13;
then
A17: i-1 < len G+1-1 by XREAL_1:9;
j < width G by A12,NAT_1:13;
then
A18: Int cell(G,i-'1,j) = {|[r,s]| where r,s is Real:
G*(i-'1,1)`1 < r &
r < G*(i,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2 } by A10,A15,A16,A17,
GOBOARD6:26;
A19: p in Int right_cell(f,k,G) by A13,A10,A12,A8,A15,A16,GOBOARD6:31;
then consider r,s be Real such that
A20: p = |[r,s]| and
G*(i-'1,1)`1 < r and
A21: r < G*(i,1)`1 and
G*(1,j)`2 < s and
s < G*(1,j+1)`2 by A8,A18;
p`1 = r by A20,EUCLID:52;
then p`1 < W-bound L~f by A5,A7,A9,A11,A12,A21,GOBOARD5:2;
then
A22: p in LeftComp f by Th9;
Int right_cell(f,k,G) c= RightComp f by A1,A2,JORDAN1H:25;
then p in LeftComp f /\ RightComp f by A19,A22,XBOOLE_0:def 4;
then LeftComp f meets RightComp f by XBOOLE_0:def 7;
hence contradiction by GOBRD14:14;
end;
end;
theorem Th21:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board for k being Nat st f
is_sequence_on G & 1 <= k & k+1 <= len f & f/.k = W-min L~f
ex i,j be Nat
st [i,j] in Indices G & [i,j+1] in Indices G & f/.k = G*(i,j) & f/.(k+1)
= G*(i,j+1)
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
let k be Nat;
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k+1 <= len f and
A4: f/.k = W-min L~f;
consider i1,j1,i2,j2 be Nat such that
A5: [i1,j1] in Indices G and
A6: f/.k = G*(i1,j1) and
A7: [i2,j2] in Indices G and
A8: f/.(k+1) = G*(i2,j2) and
A9: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or
i1 = i2 & j1 = j2+1 by A1,A2,A3,JORDAN8:3;
A10: G*(i1,j1)`1 = W-bound L~f by A4,A6,EUCLID:52;
A11: 1 <= j2 by A7,MATRIX_0:32;
A12: 1 <= i2 by A7,MATRIX_0:32;
take i1,j1;
A13: 1 <= i1 by A5,MATRIX_0:32;
A14: k+1 >= 1+1 by A2,XREAL_1:7;
then
A15: len f >= 2 by A3,XXREAL_0:2;
k+1 >= 1 by NAT_1:11;
then
A16: k+1 in dom f by A3,FINSEQ_3:25;
then f/.(k+1) in L~f by A3,A14,GOBOARD1:1,XXREAL_0:2;
then
A17: G*(i1,j1)`1 <= G*(i2,j2)`1 by A8,A10,PSCOMP_1:24;
A18: i1 <= len G & j1 <= width G by A5,MATRIX_0:32;
A19: k < len f by A3,NAT_1:13;
then
A20: k in dom f by A2,FINSEQ_3:25;
A21: i2 <= len G & j2 <= width G by A7,MATRIX_0:32;
A22: 1 <= j1 by A5,MATRIX_0:32;
per cases by A9;
suppose
A23: i1 = i2 & j1+1 = j2;
thus [i1,j1] in Indices G by A5;
thus [i1,j1+1] in Indices G by A7,A23;
thus f/.k = G*(i1,j1) by A6;
thus thesis by A8,A23;
end;
suppose
A24: i1+1 = i2 & j1 = j2 & k <> 1;
reconsider k9=k-1 as Nat by A20,FINSEQ_3:26;
k > 1 by A2,A24,XXREAL_0:1;
then k >= 1+1 by NAT_1:13;
then
A25: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A26: [i3,j3] in Indices G and
A27: f/.k9 = G*(i3,j3) and
A28: [i4,j4] in Indices G and
A29: f/.(k9+1) = G*(i4,j4) and
A30: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 = j4
or i3 = i4 & j3 = j4+1 by A1,A19,JORDAN8:3;
A31: i1 = i4 by A5,A6,A28,A29,GOBOARD1:5;
k9+1 < len f by A3,NAT_1:13;
then k9 < len f by NAT_1:13;
then
A32: k9 in dom f by A25,FINSEQ_3:25;
A33: 1 <= i3 by A26,MATRIX_0:32;
A34: j1 = j4 by A5,A6,A28,A29,GOBOARD1:5;
A35: 1 <= j3 by A26,MATRIX_0:32;
A36: i3 <= len G & j3 <= width G by A26,MATRIX_0:32;
A37: j3 = j4
proof
assume
A38: j3 <> j4;
per cases by A30,A38;
suppose
A39: i3 = i4 & j3 = j4+1;
then G*(i3,j3)`1 <> W-bound L~f by A1,A19,A25,A26,A27,A28,A29,Th20;
then G*(i3,1)`1 <> W-bound L~f by A33,A35,A36,GOBOARD5:2;
then (W-min L~f)`1 <> W-bound L~f by A4,A6,A13,A22,A18,A31,A39,
GOBOARD5:2;
hence contradiction by EUCLID:52;
end;
suppose
A40: i3 = i4 & j3+1 = j4;
G*(i3,j3)`1 = G*(i3,1)`1 by A33,A35,A36,GOBOARD5:2
.= (W-min L~f)`1 by A4,A6,A13,A22,A18,A31,A40,GOBOARD5:2
.= W-bound L~f by EUCLID:52;
then G*(i3,j3) in W-most L~f by A15,A27,A32,GOBOARD1:1,SPRECT_2:12;
then G*(i4,j4)`2 <= G*(i3,j3)`2 by A4,A29,PSCOMP_1:31;
then j3 >= j3+1 by A13,A18,A31,A34,A35,A40,GOBOARD5:4;
hence contradiction by NAT_1:13;
end;
end;
A41: k9+1 = k;
f/.k9 in L~f by A3,A14,A32,GOBOARD1:1,XXREAL_0:2;
then
A42: G*(i1,j1)`1 <= G*(i3,j3)`1 by A10,A27,PSCOMP_1:24;
now
per cases by A30,A37;
suppose
i3+1 = i4;
then i3 >= i3+1 by A22,A18,A31,A34,A33,A42,A37,GOBOARD5:3;
hence contradiction by NAT_1:13;
end;
suppose
A43: i3 = i4+1;
k9+(1+1) <= len f by A3;
then
A44: LSeg(f,k9) /\ LSeg(f,k) = {f/.k} by A25,A41,TOPREAL1:def 6;
f/.k9 in LSeg(f,k9) & f/.(k+1) in LSeg(f,k) by A2,A3,A19,A25,A41,
TOPREAL1:21;
then f/.(k+1) in {f/.k} by A8,A24,A27,A31,A34,A37,A43,A44,
XBOOLE_0:def 4;
then
A45: f/.(k+1) = f/.k by TARSKI:def 1;
i1 <> i2 by A24;
hence contradiction by A5,A6,A7,A8,A45,GOBOARD1:5;
end;
end;
hence thesis;
end;
suppose
A46: i1+1 = i2 & j1 = j2 & k = 1;
set k1 = len f;
k < len f by A3,NAT_1:13;
then
A47: len f > 1+0 by A2,XXREAL_0:2;
then len f in dom f by FINSEQ_3:25;
then reconsider k9=len f-1 as Nat by FINSEQ_3:26;
k+1 >= 1+1 by A2,XREAL_1:7;
then len f >= 1+1 by A3,XXREAL_0:2;
then
A48: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A49: [i3,j3] in Indices G and
A50: f/.k9 = G*(i3,j3) and
A51: [i4,j4] in Indices G and
A52: f/.(k9+1) = G*(i4,j4) and
A53: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 = j4
or i3 = i4 & j3 = j4+1 by A1,JORDAN8:3;
A54: f/.k1 = f/.1 by FINSEQ_6:def 1;
then
A55: i1 = i4 by A5,A6,A46,A51,A52,GOBOARD1:5;
A56: j1 = j4 by A5,A6,A46,A54,A51,A52,GOBOARD1:5;
A57: 1 <= j3 by A49,MATRIX_0:32;
k9+1 <= len f;
then k9 < len f by NAT_1:13;
then
A58: k9 in dom f by A48,FINSEQ_3:25;
then f/.k9 in L~f by A3,A14,GOBOARD1:1,XXREAL_0:2;
then
A59: G*(i1,j1)`1 <= G*(i3,j3)`1 by A10,A50,PSCOMP_1:24;
A60: 1 <= i3 by A49,MATRIX_0:32;
A61: i3 <= len G & j3 <= width G by A49,MATRIX_0:32;
A62: j3 = j4
proof
assume
A63: j3 <> j4;
per cases by A53,A63;
suppose
A64: i3 = i4 & j3 = j4+1;
then G*(i3,j3)`1 <> W-bound L~f by A1,A48,A49,A50,A51,A52,Th20;
then G*(i3,1)`1 <> W-bound L~f by A60,A57,A61,GOBOARD5:2;
then (W-min L~f)`1 <> W-bound L~f by A4,A6,A13,A22,A18,A55,A64,
GOBOARD5:2;
hence contradiction by EUCLID:52;
end;
suppose
A65: i3 = i4 & j3+1 = j4;
G*(i3,j3)`1 = G*(i3,1)`1 by A60,A57,A61,GOBOARD5:2
.= (W-min L~f)`1 by A4,A6,A13,A22,A18,A55,A65,GOBOARD5:2
.= W-bound L~f by EUCLID:52;
then G*(i3,j3) in W-most L~f by A15,A50,A58,GOBOARD1:1,SPRECT_2:12;
then G*(i4,j4)`2 <= G*(i3,j3)`2 by A4,A46,A54,A52,PSCOMP_1:31;
then j3 >= j3+1 by A13,A18,A55,A56,A57,A65,GOBOARD5:4;
hence contradiction by NAT_1:13;
end;
end;
A66: k9+1 = k1;
now
per cases by A53,A62;
suppose
i3+1 = i4;
then i3 >= i3+1 by A22,A18,A55,A56,A60,A59,A62,GOBOARD5:3;
hence contradiction by NAT_1:13;
end;
suppose
A67: i3 = i4+1;
len f-1 >= 0 by A47,XREAL_1:19;
then len f-'1 = len f-1 by XREAL_0:def 2;
then
A68: LSeg(f,k) /\ LSeg(f,k9) = {f.k} by A46,JORDAN4:42
.= {f/.k} by A20,PARTFUN1:def 6;
f/.k9 in LSeg(f,k9) & f/.(k+1) in LSeg(f,k) by A2,A3,A48,A66,
TOPREAL1:21;
then f/.(k+1) in {f/.k} by A8,A46,A50,A55,A56,A62,A67,A68,
XBOOLE_0:def 4;
then
A69: f/.(k+1) = f/.k by TARSKI:def 1;
i1 <> i2 by A46;
hence contradiction by A5,A6,A7,A8,A69,GOBOARD1:5;
end;
end;
hence thesis;
end;
suppose
i1 = i2+1 & j1 = j2;
then i2 >= i2+1 by A22,A18,A12,A17,GOBOARD5:3;
hence thesis by NAT_1:13;
end;
suppose
A70: i1 = i2 & j1 = j2+1;
G*(i2,j2)`1 = G*(i2,1)`1 by A12,A11,A21,GOBOARD5:2
.= W-bound L~f by A13,A22,A18,A10,A70,GOBOARD5:2;
then G*(i2,j2) in W-most L~f by A8,A15,A16,GOBOARD1:1,SPRECT_2:12;
then G*(i1,j1)`2 <= G*(i2,j2)`2 by A4,A6,PSCOMP_1:31;
then j2 >= j2+1 by A13,A18,A11,A70,GOBOARD5:4;
hence thesis by NAT_1:13;
end;
end;
theorem
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board for k being Nat st f
is_sequence_on G & 1 <= k & k+1 <= len f & f/.k = N-min L~f
ex i,j be Nat
st [i,j] in Indices G & [i+1,j] in Indices G & f/.k = G*(i,j) & f/.(k+1)
= G*(i+1,j)
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
let k be Nat;
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k+1 <= len f and
A4: f/.k = N-min L~f;
consider i1,j1,i2,j2 be Nat such that
A5: [i1,j1] in Indices G and
A6: f/.k = G*(i1,j1) and
A7: [i2,j2] in Indices G and
A8: f/.(k+1) = G*(i2,j2) and
A9: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or
i1 = i2 & j1 = j2+1 by A1,A2,A3,JORDAN8:3;
A10: G*(i1,j1)`2 = N-bound L~f by A4,A6,EUCLID:52;
A11: j2 <= width G by A7,MATRIX_0:32;
A12: 1 <= i2 by A7,MATRIX_0:32;
take i1,j1;
A13: 1 <= i1 by A5,MATRIX_0:32;
A14: k+1 >= 1+1 by A2,XREAL_1:7;
then
A15: len f >= 2 by A3,XXREAL_0:2;
k+1 >= 1 by NAT_1:11;
then
A16: k+1 in dom f by A3,FINSEQ_3:25;
then f/.(k+1) in L~f by A3,A14,GOBOARD1:1,XXREAL_0:2;
then
A17: G*(i1,j1)`2 >= G*(i2,j2)`2 by A8,A10,PSCOMP_1:24;
A18: j1 <= width G by A5,MATRIX_0:32;
A19: k < len f by A3,NAT_1:13;
then
A20: k in dom f by A2,FINSEQ_3:25;
A21: i2 <= len G & 1 <= j2 by A7,MATRIX_0:32;
A22: i1 <= len G & 1 <= j1 by A5,MATRIX_0:32;
per cases by A9;
suppose
A23: i1+1 = i2 & j1 = j2;
thus [i1,j1] in Indices G by A5;
thus [i1+1,j1] in Indices G by A7,A23;
thus f/.k = G*(i1,j1) by A6;
thus thesis by A8,A23;
end;
suppose
A24: i1 = i2 & j2+1 = j1 & k <> 1;
reconsider k9=k-1 as Nat by A20,FINSEQ_3:26;
k > 1 by A2,A24,XXREAL_0:1;
then k >= 1+1 by NAT_1:13;
then
A25: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A26: [i3,j3] in Indices G and
A27: f/.k9 = G*(i3,j3) and
A28: [i4,j4] in Indices G and
A29: f/.(k9+1) = G*(i4,j4) and
A30: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 = j4
or i3 = i4 & j3 = j4+1 by A1,A19,JORDAN8:3;
A31: i1 = i4 by A5,A6,A28,A29,GOBOARD1:5;
k9+1 < len f by A3,NAT_1:13;
then k9 < len f by NAT_1:13;
then
A32: k9 in dom f by A25,FINSEQ_3:25;
A33: 1 <= i3 by A26,MATRIX_0:32;
A34: j3 <= width G by A26,MATRIX_0:32;
A35: j1 = j4 by A5,A6,A28,A29,GOBOARD1:5;
A36: i3 <= len G & 1 <= j3 by A26,MATRIX_0:32;
A37: i3 = i4
proof
assume
A38: i3 <> i4;
per cases by A30,A38;
suppose
A39: j3 = j4 & i3 = i4+1;
then G*(i3,j3)`2 <> N-bound L~f by A1,A19,A25,A26,A27,A28,A29,Th17;
then G*(1,j3)`2 <> N-bound L~f by A33,A36,A34,GOBOARD5:1;
then (N-min L~f)`2 <> N-bound L~f by A4,A6,A13,A22,A18,A35,A39,
GOBOARD5:1;
hence contradiction by EUCLID:52;
end;
suppose
A40: j3 = j4 & i3+1 = i4;
G*(i3,j3)`2 = G*(1,j3)`2 by A33,A36,A34,GOBOARD5:1
.= (N-min L~f)`2 by A4,A6,A13,A22,A18,A35,A40,GOBOARD5:1
.= N-bound L~f by EUCLID:52;
then G*(i3,j3) in N-most L~f by A15,A27,A32,GOBOARD1:1,SPRECT_2:10;
then G*(i4,j4)`1 <= G*(i3,j3)`1 by A4,A29,PSCOMP_1:39;
then i3 >= i3+1 by A22,A18,A31,A35,A33,A40,GOBOARD5:3;
hence contradiction by NAT_1:13;
end;
end;
A41: k9+1 = k;
f/.k9 in L~f by A3,A14,A32,GOBOARD1:1,XXREAL_0:2;
then
A42: G*(i1,j1)`2 >= G*(i3,j3)`2 by A10,A27,PSCOMP_1:24;
now
per cases by A30,A37;
suppose
j4+1 = j3;
then j4 >= j4+1 by A13,A22,A31,A35,A34,A42,A37,GOBOARD5:4;
hence contradiction by NAT_1:13;
end;
suppose
A43: j4 = j3+1;
k9+(1+1) <= len f by A3;
then
A44: LSeg(f,k9) /\ LSeg(f,k) = {f/.k} by A25,A41,TOPREAL1:def 6;
f/.k9 in LSeg(f,k9) & f/.(k+1) in LSeg(f,k) by A2,A3,A19,A25,A41,
TOPREAL1:21;
then f/.(k+1) in {f/.k} by A8,A24,A27,A31,A35,A37,A43,A44,
XBOOLE_0:def 4;
then
A45: f/.(k+1) = f/.k by TARSKI:def 1;
j1 <> j2 by A24;
hence contradiction by A5,A6,A7,A8,A45,GOBOARD1:5;
end;
end;
hence thesis;
end;
suppose
A46: i1 = i2 & j2+1 = j1 & k = 1;
set k1 = len f;
k < len f by A3,NAT_1:13;
then
A47: len f > 1+0 by A2,XXREAL_0:2;
then len f in dom f by FINSEQ_3:25;
then reconsider k9=len f-1 as Nat by FINSEQ_3:26;
k+1 >= 1+1 by A2,XREAL_1:7;
then len f >= 1+1 by A3,XXREAL_0:2;
then
A48: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A49: [i3,j3] in Indices G and
A50: f/.k9 = G*(i3,j3) and
A51: [i4,j4] in Indices G and
A52: f/.(k9+1) = G*(i4,j4) and
A53: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 = j4
or i3 = i4 & j3 = j4+1 by A1,JORDAN8:3;
A54: f/.k1 = f/.1 by FINSEQ_6:def 1;
then
A55: i1 = i4 by A5,A6,A46,A51,A52,GOBOARD1:5;
k9+1 <= len f;
then k9 < len f by NAT_1:13;
then
A56: k9 in dom f by A48,FINSEQ_3:25;
then f/.k9 in L~f by A3,A14,GOBOARD1:1,XXREAL_0:2;
then
A57: G*(i1,j1)`2 >= G*(i3,j3)`2 by A10,A50,PSCOMP_1:24;
A58: 1 <= i3 by A49,MATRIX_0:32;
A59: j1 = j4 by A5,A6,A46,A54,A51,A52,GOBOARD1:5;
A60: j3 <= width G by A49,MATRIX_0:32;
A61: i3 <= len G & 1 <= j3 by A49,MATRIX_0:32;
A62: i3 = i4
proof
assume
A63: i3 <> i4;
per cases by A53,A63;
suppose
A64: j3 = j4 & i3 = i4+1;
then G*(i3,j3)`2 <> N-bound L~f by A1,A48,A49,A50,A51,A52,Th17;
then G*(1,j3)`2 <> N-bound L~f by A58,A61,A60,GOBOARD5:1;
then (N-min L~f)`2 <> N-bound L~f by A4,A6,A13,A22,A18,A59,A64,
GOBOARD5:1;
hence contradiction by EUCLID:52;
end;
suppose
A65: j3 = j4 & i3+1 = i4;
G*(i3,j3)`2 = G*(1,j3)`2 by A58,A61,A60,GOBOARD5:1
.= (N-min L~f)`2 by A4,A6,A13,A22,A18,A59,A65,GOBOARD5:1
.= N-bound L~f by EUCLID:52;
then G*(i3,j3) in N-most L~f by A15,A50,A56,GOBOARD1:1,SPRECT_2:10;
then G*(i4,j4)`1 <= G*(i3,j3)`1 by A4,A46,A54,A52,PSCOMP_1:39;
then i3 >= i3+1 by A22,A18,A55,A59,A58,A65,GOBOARD5:3;
hence contradiction by NAT_1:13;
end;
end;
A66: k9+1 = k1;
now
per cases by A53,A62;
suppose
j4+1 = j3;
then j4 >= j4+1 by A13,A22,A55,A59,A60,A57,A62,GOBOARD5:4;
hence contradiction by NAT_1:13;
end;
suppose
A67: j4 = j3+1;
len f-1 >= 0 by A47,XREAL_1:19;
then len f-'1 = len f-1 by XREAL_0:def 2;
then
A68: LSeg(f,k) /\ LSeg(f,k9) = {f.k} by A46,JORDAN4:42
.= {f/.k} by A20,PARTFUN1:def 6;
f/.k9 in LSeg(f,k9) & f/.(k+1) in LSeg(f,k) by A2,A3,A48,A66,
TOPREAL1:21;
then f/.(k+1) in {f/.k} by A8,A46,A50,A55,A59,A62,A67,A68,
XBOOLE_0:def 4;
then
A69: f/.(k+1) = f/.k by TARSKI:def 1;
j1 <> j2 by A46;
hence contradiction by A5,A6,A7,A8,A69,GOBOARD1:5;
end;
end;
hence thesis;
end;
suppose
i1 = i2 & j2 = j1+1;
then j1 >= j1+1 by A13,A22,A11,A17,GOBOARD5:4;
hence thesis by NAT_1:13;
end;
suppose
A70: i1 = i2+1 & j1 = j2;
G*(i2,j2)`2 = G*(1,j2)`2 by A12,A21,A11,GOBOARD5:1
.= N-bound L~f by A13,A22,A18,A10,A70,GOBOARD5:1;
then G*(i2,j2) in N-most L~f by A8,A15,A16,GOBOARD1:1,SPRECT_2:10;
then G*(i1,j1)`1 <= G*(i2,j2)`1 by A4,A6,PSCOMP_1:39;
then i2 >= i2+1 by A22,A18,A12,A70,GOBOARD5:3;
hence thesis by NAT_1:13;
end;
end;
theorem Th23:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board for k being Nat st f
is_sequence_on G & 1 <= k & k+1 <= len f & f/.k = E-max L~f
ex i,j be Nat
st [i,j+1] in Indices G & [i,j] in Indices G & f/.k = G*(i,j+1) & f/.(k+
1) = G*(i,j)
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
let k be Nat;
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k+1 <= len f and
A4: f/.k = E-max L~f;
consider i1,j1,i2,j2 be Nat such that
A5: [i1,j1] in Indices G and
A6: f/.k = G*(i1,j1) and
A7: [i2,j2] in Indices G and
A8: f/.(k+1) = G*(i2,j2) and
A9: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or
i1 = i2 & j1 = j2+1 by A1,A2,A3,JORDAN8:3;
A10: G*(i1,j1)`1 = E-bound L~f by A4,A6,EUCLID:52;
A11: j2 <= width G by A7,MATRIX_0:32;
take i2,j2;
A12: i1 <= len G by A5,MATRIX_0:32;
A13: k+1 >= 1+1 by A2,XREAL_1:7;
then
A14: len f >= 2 by A3,XXREAL_0:2;
k+1 >= 1 by NAT_1:11;
then
A15: k+1 in dom f by A3,FINSEQ_3:25;
then f/.(k+1) in L~f by A3,A13,GOBOARD1:1,XXREAL_0:2;
then
A16: G*(i1,j1)`1 >= G*(i2,j2)`1 by A8,A10,PSCOMP_1:24;
A17: 1 <= i1 & 1 <= j1 by A5,MATRIX_0:32;
A18: k < len f by A3,NAT_1:13;
then
A19: k in dom f by A2,FINSEQ_3:25;
A20: i2 <= len G by A7,MATRIX_0:32;
A21: j1 <= width G by A5,MATRIX_0:32;
A22: 1 <= i2 & 1 <= j2 by A7,MATRIX_0:32;
now
per cases by A9;
suppose
i1 = i2 & j2+1 = j1;
hence [i2,j2] in Indices G & [i2,j2+1] in Indices G & f/.k = G*(i2,j2+1)
by A5,A6,A7;
end;
suppose
A23: i2+1 = i1 & j2 = j1 & k <> 1;
reconsider k9=k-1 as Nat by A19,FINSEQ_3:26;
k > 1 by A2,A23,XXREAL_0:1;
then k >= 1+1 by NAT_1:13;
then
A24: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A25: [i3,j3] in Indices G and
A26: f/.k9 = G*(i3,j3) and
A27: [i4,j4] in Indices G and
A28: f/.(k9+1) = G*(i4,j4) and
A29: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 =
j4 or i3 = i4 & j3 = j4+1 by A1,A18,JORDAN8:3;
A30: i1 = i4 by A5,A6,A27,A28,GOBOARD1:5;
k9+1 < len f by A3,NAT_1:13;
then k9 < len f by NAT_1:13;
then
A31: k9 in dom f by A24,FINSEQ_3:25;
A32: i3 <= len G by A25,MATRIX_0:32;
A33: j1 = j4 by A5,A6,A27,A28,GOBOARD1:5;
A34: j3 <= width G by A25,MATRIX_0:32;
A35: 1 <= i3 & 1 <= j3 by A25,MATRIX_0:32;
A36: j3 = j4
proof
assume
A37: j3 <> j4;
per cases by A29,A37;
suppose
A38: i3 = i4 & j4 = j3+1;
then G*(i3,j3)`1 <> E-bound L~f by A1,A18,A24,A25,A26,A27,A28,Th18;
then G*(i3,1)`1 <> E-bound L~f by A32,A35,A34,GOBOARD5:2;
then (E-max L~f)`1 <> E-bound L~f by A4,A6,A12,A17,A21,A30,A38,
GOBOARD5:2;
hence contradiction by EUCLID:52;
end;
suppose
A39: i3 = i4 & j4+1 = j3;
G*(i3,j3)`1 = G*(i3,1)`1 by A32,A35,A34,GOBOARD5:2
.= (E-max L~f)`1 by A4,A6,A12,A17,A21,A30,A39,GOBOARD5:2
.= E-bound L~f by EUCLID:52;
then G*(i3,j3) in E-most L~f by A14,A26,A31,GOBOARD1:1,SPRECT_2:13;
then G*(i4,j4)`2 >= G*(i3,j3)`2 by A4,A28,PSCOMP_1:47;
then j4 >= j4+1 by A12,A17,A30,A33,A34,A39,GOBOARD5:4;
hence contradiction by NAT_1:13;
end;
end;
A40: k9+1 = k;
f/.k9 in L~f by A3,A13,A31,GOBOARD1:1,XXREAL_0:2;
then
A41: G*(i1,j1)`1 >= G*(i3,j3)`1 by A10,A26,PSCOMP_1:24;
now
per cases by A29,A36;
suppose
i4+1 = i3;
then i4 >= i4+1 by A17,A21,A30,A33,A32,A41,A36,GOBOARD5:3;
hence contradiction by NAT_1:13;
end;
suppose
A42: i4 = i3+1;
k9+(1+1) <= len f by A3;
then
A43: LSeg(f,k9) /\ LSeg(f,k) = {f/.k} by A24,A40,TOPREAL1:def 6;
f/.k9 in LSeg(f,k9) & f/.(k+1) in LSeg(f,k) by A2,A3,A18,A24,A40,
TOPREAL1:21;
then f/.(k+1) in {f/.k} by A8,A23,A26,A30,A33,A36,A42,A43,
XBOOLE_0:def 4;
then
A44: f/.(k+1) = f/.k by TARSKI:def 1;
i1 <> i2 by A23;
hence contradiction by A5,A6,A7,A8,A44,GOBOARD1:5;
end;
end;
hence [i2,j2] in Indices G & [i2,j2+1] in Indices G & f/.k = G*(i2,j2+1);
end;
suppose
A45: i2+1 = i1 & j2 = j1 & k = 1;
set k1 = len f;
k < len f by A3,NAT_1:13;
then
A46: len f > 1+0 by A2,XXREAL_0:2;
then len f in dom f by FINSEQ_3:25;
then reconsider k9=len f-1 as Nat by FINSEQ_3:26;
k+1 >= 1+1 by A2,XREAL_1:7;
then len f >= 1+1 by A3,XXREAL_0:2;
then
A47: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A48: [i3,j3] in Indices G and
A49: f/.k9 = G*(i3,j3) and
A50: [i4,j4] in Indices G and
A51: f/.(k9+1) = G*(i4,j4) and
A52: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 =
j4 or i3 = i4 & j3 = j4+1 by A1,JORDAN8:3;
A53: f/.k1 = f/.1 by FINSEQ_6:def 1;
then
A54: i1 = i4 by A5,A6,A45,A50,A51,GOBOARD1:5;
A55: j1 = j4 by A5,A6,A45,A53,A50,A51,GOBOARD1:5;
A56: j3 <= width G by A48,MATRIX_0:32;
k9+1 <= len f;
then k9 < len f by NAT_1:13;
then
A57: k9 in dom f by A47,FINSEQ_3:25;
then f/.k9 in L~f by A3,A13,GOBOARD1:1,XXREAL_0:2;
then
A58: G*(i1,j1)`1 >= G*(i3,j3)`1 by A10,A49,PSCOMP_1:24;
A59: i3 <= len G by A48,MATRIX_0:32;
A60: 1 <= i3 & 1 <= j3 by A48,MATRIX_0:32;
A61: j3 = j4
proof
assume
A62: j3 <> j4;
per cases by A52,A62;
suppose
A63: i3 = i4 & j4 = j3+1;
then G*(i3,j3)`1 <> E-bound L~f by A1,A47,A48,A49,A50,A51,Th18;
then G*(i3,1)`1 <> E-bound L~f by A59,A60,A56,GOBOARD5:2;
then (E-max L~f)`1 <> E-bound L~f by A4,A6,A12,A17,A21,A54,A63,
GOBOARD5:2;
hence contradiction by EUCLID:52;
end;
suppose
A64: i3 = i4 & j4+1 = j3;
G*(i3,j3)`1 = G*(i3,1)`1 by A59,A60,A56,GOBOARD5:2
.= (E-max L~f)`1 by A4,A6,A12,A17,A21,A54,A64,GOBOARD5:2
.= E-bound L~f by EUCLID:52;
then G*(i3,j3) in E-most L~f by A14,A49,A57,GOBOARD1:1,SPRECT_2:13;
then G*(i4,j4)`2 >= G*(i3,j3)`2 by A4,A45,A53,A51,PSCOMP_1:47;
then j4 >= j4+1 by A12,A17,A54,A55,A56,A64,GOBOARD5:4;
hence contradiction by NAT_1:13;
end;
end;
A65: k9+1 = k1;
now
per cases by A52,A61;
suppose
i4+1 = i3;
then i4 >= i4+1 by A17,A21,A54,A55,A59,A58,A61,GOBOARD5:3;
hence contradiction by NAT_1:13;
end;
suppose
A66: i4 = i3+1;
len f-1 >= 0 by A46,XREAL_1:19;
then len f-'1 = len f-1 by XREAL_0:def 2;
then
A67: LSeg(f,k) /\ LSeg(f,k9) = {f.k} by A45,JORDAN4:42
.= {f/.k} by A19,PARTFUN1:def 6;
f/.k9 in LSeg(f,k9) & f/.(k+1) in LSeg(f,k) by A2,A3,A47,A65,
TOPREAL1:21;
then f/.(k+1) in {f/.k} by A8,A45,A49,A54,A55,A61,A66,A67,
XBOOLE_0:def 4;
then
A68: f/.(k+1) = f/.k by TARSKI:def 1;
i1 <> i2 by A45;
hence contradiction by A5,A6,A7,A8,A68,GOBOARD1:5;
end;
end;
hence [i2,j2] in Indices G & [i2,j2+1] in Indices G & f/.k = G*(i2,j2+1);
end;
suppose
i2 = i1+1 & j1 = j2;
then i1 >= i1+1 by A17,A21,A20,A16,GOBOARD5:3;
hence [i2,j2] in Indices G & [i2,j2+1] in Indices G & f/.k = G*(i2,j2+1)
by NAT_1:13;
end;
suppose
A69: i1 = i2 & j2 = j1+1;
G*(i2,j2)`1 = G*(i2,1)`1 by A20,A22,A11,GOBOARD5:2
.= E-bound L~f by A12,A17,A21,A10,A69,GOBOARD5:2;
then G*(i2,j2) in E-most L~f by A8,A14,A15,GOBOARD1:1,SPRECT_2:13;
then G*(i1,j1)`2 >= G*(i2,j2)`2 by A4,A6,PSCOMP_1:47;
then j1 >= j1+1 by A12,A17,A11,A69,GOBOARD5:4;
hence [i2,j2] in Indices G & [i2,j2+1] in Indices G & f/.k = G*(i2,j2+1)
by NAT_1:13;
end;
end;
hence [i2,j2+1] in Indices G & [i2,j2] in Indices G & f/.k = G*(i2,j2+1);
thus thesis by A8;
end;
theorem Th24:
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board for k being Nat st f
is_sequence_on G & 1 <= k & k+1 <= len f & f/.k = S-max L~f
ex i,j be Nat
st [i+1,j] in Indices G & [i,j] in Indices G & f/.k = G*(i+1,j) & f/.(k+
1) = G*(i,j)
proof
let f be clockwise_oriented non constant standard special_circular_sequence;
let G be Go-board;
let k be Nat;
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k+1 <= len f and
A4: f/.k = S-max L~f;
consider i1,j1,i2,j2 be Nat such that
A5: [i1,j1] in Indices G and
A6: f/.k = G*(i1,j1) and
A7: [i2,j2] in Indices G and
A8: f/.(k+1) = G*(i2,j2) and
A9: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or
i1 = i2 & j1 = j2+1 by A1,A2,A3,JORDAN8:3;
A10: G*(i1,j1)`2 = S-bound L~f by A4,A6,EUCLID:52;
A11: 1 <= j2 by A7,MATRIX_0:32;
take i2,j2;
A12: i1 <= len G by A5,MATRIX_0:32;
A13: k+1 >= 1+1 by A2,XREAL_1:7;
then
A14: len f >= 2 by A3,XXREAL_0:2;
k+1 >= 1 by NAT_1:11;
then
A15: k+1 in dom f by A3,FINSEQ_3:25;
then f/.(k+1) in L~f by A3,A13,GOBOARD1:1,XXREAL_0:2;
then
A16: G*(i1,j1)`2 <= G*(i2,j2)`2 by A8,A10,PSCOMP_1:24;
A17: 1 <= j1 by A5,MATRIX_0:32;
A18: k < len f by A3,NAT_1:13;
then
A19: k in dom f by A2,FINSEQ_3:25;
A20: i2 <= len G by A7,MATRIX_0:32;
A21: 1 <= i1 & j1 <= width G by A5,MATRIX_0:32;
A22: 1 <= i2 & j2 <= width G by A7,MATRIX_0:32;
now
per cases by A9;
suppose
i2+1 = i1 & j1 = j2;
hence [i2+1,j2] in Indices G & [i2,j2] in Indices G & f/.k = G*(i2+1,j2)
by A5,A6,A7;
end;
suppose
A23: i1 = i2 & j1+1 = j2 & k <> 1;
reconsider k9=k-1 as Nat by A19,FINSEQ_3:26;
k > 1 by A2,A23,XXREAL_0:1;
then k >= 1+1 by NAT_1:13;
then
A24: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A25: [i3,j3] in Indices G and
A26: f/.k9 = G*(i3,j3) and
A27: [i4,j4] in Indices G and
A28: f/.(k9+1) = G*(i4,j4) and
A29: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 =
j4 or i3 = i4 & j3 = j4+1 by A1,A18,JORDAN8:3;
A30: i1 = i4 by A5,A6,A27,A28,GOBOARD1:5;
k9+1 < len f by A3,NAT_1:13;
then k9 < len f by NAT_1:13;
then
A31: k9 in dom f by A24,FINSEQ_3:25;
A32: i3 <= len G by A25,MATRIX_0:32;
A33: 1 <= j3 by A25,MATRIX_0:32;
A34: j1 = j4 by A5,A6,A27,A28,GOBOARD1:5;
A35: 1 <= i3 & j3 <= width G by A25,MATRIX_0:32;
A36: i3 = i4
proof
assume
A37: i3 <> i4;
per cases by A29,A37;
suppose
A38: j3 = j4 & i4 = i3+1;
then G*(i3,j3)`2 <> S-bound L~f by A1,A18,A24,A25,A26,A27,A28,Th19;
then G*(1,j3)`2 <> S-bound L~f by A32,A33,A35,GOBOARD5:1;
then (S-max L~f)`2 <> S-bound L~f by A4,A6,A12,A17,A21,A34,A38,
GOBOARD5:1;
hence contradiction by EUCLID:52;
end;
suppose
A39: j3 = j4 & i4+1 = i3;
G*(i3,j3)`2 = G*(1,j3)`2 by A32,A33,A35,GOBOARD5:1
.= (S-max L~f)`2 by A4,A6,A12,A17,A21,A34,A39,GOBOARD5:1
.= S-bound L~f by EUCLID:52;
then G*(i3,j3) in S-most L~f by A14,A26,A31,GOBOARD1:1,SPRECT_2:11;
then G*(i4,j4)`1 >= G*(i3,j3)`1 by A4,A28,PSCOMP_1:55;
then i4 >= i4+1 by A17,A21,A30,A34,A32,A39,GOBOARD5:3;
hence contradiction by NAT_1:13;
end;
end;
A40: k9+1 = k;
f/.k9 in L~f by A3,A13,A31,GOBOARD1:1,XXREAL_0:2;
then
A41: G*(i1,j1)`2 <= G*(i3,j3)`2 by A10,A26,PSCOMP_1:24;
now
per cases by A29,A36;
suppose
j3+1 = j4;
then j3 >= j3+1 by A12,A21,A30,A34,A33,A41,A36,GOBOARD5:4;
hence contradiction by NAT_1:13;
end;
suppose
A42: j3 = j4+1;
k9+(1+1) <= len f by A3;
then
A43: LSeg(f,k9) /\ LSeg(f,k) = {f/.k} by A24,A40,TOPREAL1:def 6;
f/.k9 in LSeg(f,k9) & f/.(k+1) in LSeg(f,k) by A2,A3,A18,A24,A40,
TOPREAL1:21;
then f/.(k+1) in {f/.k} by A8,A23,A26,A30,A34,A36,A42,A43,
XBOOLE_0:def 4;
then
A44: f/.(k+1) = f/.k by TARSKI:def 1;
j1 <> j2 by A23;
hence contradiction by A5,A6,A7,A8,A44,GOBOARD1:5;
end;
end;
hence [i2+1,j2] in Indices G & [i2,j2] in Indices G & f/.k = G*(i2+1,j2);
end;
suppose
A45: i1 = i2 & j1+1 = j2 & k = 1;
set k1 = len f;
k < len f by A3,NAT_1:13;
then
A46: len f > 1+0 by A2,XXREAL_0:2;
then len f in dom f by FINSEQ_3:25;
then reconsider k9=len f-1 as Nat by FINSEQ_3:26;
k+1 >= 1+1 by A2,XREAL_1:7;
then len f >= 1+1 by A3,XXREAL_0:2;
then
A47: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A48: [i3,j3] in Indices G and
A49: f/.k9 = G*(i3,j3) and
A50: [i4,j4] in Indices G and
A51: f/.(k9+1) = G*(i4,j4) and
A52: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 =
j4 or i3 = i4 & j3 = j4+1 by A1,JORDAN8:3;
A53: f/.k1 = f/.1 by FINSEQ_6:def 1;
then
A54: i1 = i4 by A5,A6,A45,A50,A51,GOBOARD1:5;
k9+1 <= len f;
then k9 < len f by NAT_1:13;
then
A55: k9 in dom f by A47,FINSEQ_3:25;
then f/.k9 in L~f by A3,A13,GOBOARD1:1,XXREAL_0:2;
then
A56: G*(i1,j1)`2 <= G*(i3,j3)`2 by A10,A49,PSCOMP_1:24;
A57: i3 <= len G by A48,MATRIX_0:32;
A58: j1 = j4 by A5,A6,A45,A53,A50,A51,GOBOARD1:5;
A59: 1 <= j3 by A48,MATRIX_0:32;
A60: 1 <= i3 & j3 <= width G by A48,MATRIX_0:32;
A61: i3 = i4
proof
assume
A62: i3 <> i4;
per cases by A52,A62;
suppose
A63: j3 = j4 & i4 = i3+1;
then G*(i3,j3)`2 <> S-bound L~f by A1,A47,A48,A49,A50,A51,Th19;
then G*(1,j3)`2 <> S-bound L~f by A57,A59,A60,GOBOARD5:1;
then (S-max L~f)`2 <> S-bound L~f by A4,A6,A12,A17,A21,A58,A63,
GOBOARD5:1;
hence contradiction by EUCLID:52;
end;
suppose
A64: j3 = j4 & i4+1 = i3;
G*(i3,j3)`2 = G*(1,j3)`2 by A57,A59,A60,GOBOARD5:1
.= (S-max L~f)`2 by A4,A6,A12,A17,A21,A58,A64,GOBOARD5:1
.= S-bound L~f by EUCLID:52;
then G*(i3,j3) in S-most L~f by A14,A49,A55,GOBOARD1:1,SPRECT_2:11;
then G*(i4,j4)`1 >= G*(i3,j3)`1 by A4,A45,A53,A51,PSCOMP_1:55;
then i4 >= i4+1 by A17,A21,A54,A58,A57,A64,GOBOARD5:3;
hence contradiction by NAT_1:13;
end;
end;
A65: k9+1 = k1;
now
per cases by A52,A61;
suppose
j3+1 = j4;
then j3 >= j3+1 by A12,A21,A54,A58,A59,A56,A61,GOBOARD5:4;
hence contradiction by NAT_1:13;
end;
suppose
A66: j3 = j4+1;
len f-1 >= 0 by A46,XREAL_1:19;
then len f-'1 = len f-1 by XREAL_0:def 2;
then
A67: LSeg(f,k) /\ LSeg(f,k9) = {f.k} by A45,JORDAN4:42
.= {f/.k} by A19,PARTFUN1:def 6;
f/.k9 in LSeg(f,k9) & f/.(k+1) in LSeg(f,k) by A2,A3,A47,A65,
TOPREAL1:21;
then f/.(k+1) in {f/.k} by A8,A45,A49,A54,A58,A61,A66,A67,
XBOOLE_0:def 4;
then
A68: f/.(k+1) = f/.k by TARSKI:def 1;
j1 <> j2 by A45;
hence contradiction by A5,A6,A7,A8,A68,GOBOARD1:5;
end;
end;
hence [i2+1,j2] in Indices G & [i2,j2] in Indices G & f/.k = G*(i2+1,j2);
end;
suppose
i1 = i2 & j1 = j2+1;
then j2 >= j2+1 by A12,A21,A11,A16,GOBOARD5:4;
hence [i2+1,j2] in Indices G & [i2,j2] in Indices G & f/.k = G*(i2+1,j2)
by NAT_1:13;
end;
suppose
A69: i2 = i1+1 & j1 = j2;
G*(i2,j2)`2 = G*(1,j2)`2 by A20,A11,A22,GOBOARD5:1
.= S-bound L~f by A12,A17,A21,A10,A69,GOBOARD5:1;
then G*(i2,j2) in S-most L~f by A8,A14,A15,GOBOARD1:1,SPRECT_2:11;
then G*(i1,j1)`1 >= G*(i2,j2)`1 by A4,A6,PSCOMP_1:55;
then i1 >= i1+1 by A17,A21,A20,A69,GOBOARD5:3;
hence [i2+1,j2] in Indices G & [i2,j2] in Indices G & f/.k = G*(i2+1,j2)
by NAT_1:13;
end;
end;
hence [i2+1,j2] in Indices G & [i2,j2] in Indices G & f/.k = G*(i2+1,j2);
thus thesis by A8;
end;
theorem
for f being non constant standard special_circular_sequence holds f is
clockwise_oriented iff Rotate(f,W-min L~f)/.2 in W-most L~f
proof
set i = 1;
let f be non constant standard special_circular_sequence;
set r = Rotate(f,W-min L~f);
A1: r is_sequence_on GoB r by GOBOARD5:def 5;
A2: 1+1 <= len r by TOPREAL8:3;
then
A3: Int left_cell(r,1) c= LeftComp r by GOBOARD9:21;
set j = i_s_w r;
A4: W-min L~f in rng f by SPRECT_2:43;
then
A5: r/.1 = W-min L~f by FINSEQ_6:92;
A6: 2 <= len f by TOPREAL8:3;
thus f is clockwise_oriented implies r/.2 in W-most L~f
proof
set k = (W-min L~f)..f;
k < len f by SPRECT_5:20;
then
A7: k+1 <= len f by NAT_1:13;
1 <= k+1 by NAT_1:11;
then
A8: k+1 in dom f by A7,FINSEQ_3:25;
then f/.(k+1) = f.(k+1) by PARTFUN1:def 6;
then
A9: f/.(k+1) in rng f by A8,FUNCT_1:3;
A10: rng f c= L~f by A6,SPPOL_2:18;
A11: f/.k = W-min L~f by A4,FINSEQ_5:38;
k <= k+1 by NAT_1:13;
then
A12: f/.(k+1) = r/.(k+1+1 -' k) by A4,A7,FINSEQ_6:175
.= r/.(k+(1+1) -' k)
.= r/.2 by NAT_D:34;
f is_sequence_on GoB f by GOBOARD5:def 5;
then
A13: f is_sequence_on GoB r by REVROT_1:28;
assume f is clockwise_oriented;
then consider i,j being Nat such that
A14: [i,j] in Indices GoB r and
A15: [i,j+1] in Indices GoB r and
A16: f/.k = (GoB r)*(i,j) and
A17: f/.(k+1) = (GoB r)*(i,j+1) by A4,A7,A11,A13,Th21,FINSEQ_4:21;
A18: 1 <= i & i <= len GoB r by A14,MATRIX_0:32;
A19: 1 <= j+1 & j+1 <= width GoB r by A15,MATRIX_0:32;
A20: 1 <= j & j <= width GoB r by A14,MATRIX_0:32;
1 <= i & i <= len GoB r by A14,MATRIX_0:32;
then (f/.(k+1))`1 = (GoB r)*(i,1)`1 by A17,A19,GOBOARD5:2
.= (f/.k)`1 by A16,A18,A20,GOBOARD5:2
.= W-bound L~f by A11,EUCLID:52;
hence thesis by A12,A9,A10,SPRECT_2:12;
end;
A21: [i,j] in Indices GoB r by JORDAN5D:def 1;
then
A22: i <= len GoB r & j <= width GoB r by MATRIX_0:32;
len r > 2 by TOPREAL8:3;
then
A23: 1+1 in dom r by FINSEQ_3:25;
then consider i2,j2 being Nat such that
A24: [i2,j2] in Indices GoB r and
A25: r/.(1+1) = (GoB r)*(i2,j2) by A1,GOBOARD1:def 9;
A26: 1 <= j2 by A24,MATRIX_0:32;
A27: L~r = L~f by REVROT_1:33;
then
A28: (GoB r)*(i,j) = r/.1 by A5,JORDAN5D:def 1;
assume
A29: r/.2 in W-most L~f;
then (GoB r)*(i2,j2)`1 = (GoB r)*(1,j)`1 by A5,A28,A25,PSCOMP_1:31;
then
A30: i2 = 1 by A21,A24,JORDAN1G:7;
rng r = rng f by FINSEQ_6:90,SPRECT_2:43;
then 1 in dom r by FINSEQ_3:31,SPRECT_2:43;
then |.1-1.|+|.j-j2.| = 1 by A1,A21,A28,A23,A24,A25,A30,GOBOARD1:def 9;
then 0+|.j-j2.| = 1 by ABSVALUE:2;
then
A31: |.j2-j.|=1 by UNIFORM1:11;
(GoB r)*(1,j)`2 <= (GoB r)*(i2,j2)`2 by A5,A28,A29,A25,PSCOMP_1:31;
then j2 - j >= 0 by A22,A30,A26,GOBOARD5:4,XREAL_1:48;
then
A32: j2 - j = 1 by A31,ABSVALUE:def 1;
then j2 = j+1;
then
i-'1 = 1-1 & left_cell(r,1,GoB r) = cell(GoB r,i-'1,j) by A2,A1,A21,A28,A24
,A25,A30,GOBRD13:21,XREAL_1:233;
then
A33: left_cell(r,1) = cell(GoB r,0,j) by A2,JORDAN1H:21;
Int left_cell(r,1) <> {} by A2,GOBOARD9:15;
then consider p being object such that
A34: p in Int left_cell(r,1) by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL2 by A34;
A35: LeftComp r is_a_component_of (L~r)` & UBD L~r is_a_component_of (L~r)`
by GOBOARD9:def 1,JORDAN2C:124;
A36: 1 <= j by A21,MATRIX_0:32;
j+1 <= width GoB r by A24,A32,MATRIX_0:32;
then j < width GoB r by NAT_1:13;
then Int left_cell(r,1) = { |[t,s]| where t,s is Real:
t < (GoB r)*(1,1)`1
& (GoB r)*(1,j)`2 < s & s < (GoB r)*(1,j+1)`2 } by A36,A33,GOBOARD6:20;
then consider t,s being Real such that
A37: p = |[t,s]| and
A38: t < (GoB r)*(1,1)`1 and
(GoB r)*(1,j)`2 < s and
s < (GoB r)*(1,j+1)`2 by A34;
now
A39: (GoB r)*(1,j)`1 = (GoB r)*(1,1)`1 by A36,A22,GOBOARD5:2;
assume west_halfline p meets L~r;
then (west_halfline p) /\ L~r <> {} by XBOOLE_0:def 7;
then consider a being object such that
A40: a in (west_halfline p) /\ L~r by XBOOLE_0:def 1;
A41: a in L~r by A40,XBOOLE_0:def 4;
A42: a in (west_halfline p) by A40,XBOOLE_0:def 4;
reconsider a as Point of TOP-REAL2 by A40;
a`1 <= p`1 by A42,TOPREAL1:def 13;
then a`1 <= t by A37,EUCLID:52;
then a`1 < (GoB r)*(i,j)`1 by A38,A39,XXREAL_0:2;
then a`1 < W-bound L~r by A27,A5,A28,EUCLID:52;
hence contradiction by A41,PSCOMP_1:24;
end;
then
A43: west_halfline p c= UBD L~r by JORDAN2C:126;
p in west_halfline p by TOPREAL1:38;
then LeftComp r meets UBD L~r by A3,A34,A43,XBOOLE_0:3;
then r is clockwise_oriented by A35,GOBOARD9:1,JORDAN1H:41;
hence thesis by JORDAN1H:40;
end;
theorem
for f being non constant standard special_circular_sequence holds f is
clockwise_oriented iff Rotate(f,E-max L~f)/.2 in E-most L~f
proof
let f be non constant standard special_circular_sequence;
set r = Rotate(f,E-max L~f);
set j = i_n_e r;
set i = len GoB r;
A1: 1+1 <= len r & r is_sequence_on GoB r by GOBOARD5:def 5,TOPREAL8:3;
A2: E-max L~f in rng f by SPRECT_2:46;
then
A3: r/.1 = E-max L~f by FINSEQ_6:92;
A4: 2 <= len f by TOPREAL8:3;
thus f is clockwise_oriented implies r/.2 in E-most L~f
proof
set k = (E-max L~f)..f;
k < len f by SPRECT_5:16;
then
A5: k+1 <= len f by NAT_1:13;
1 <= k+1 by NAT_1:11;
then
A6: k+1 in dom f by A5,FINSEQ_3:25;
then f/.(k+1) = f.(k+1) by PARTFUN1:def 6;
then
A7: f/.(k+1) in rng f by A6,FUNCT_1:3;
A8: rng f c= L~f by A4,SPPOL_2:18;
A9: f/.k = E-max L~f by A2,FINSEQ_5:38;
k <= k+1 by NAT_1:13;
then
A10: f/.(k+1) = r/.(k+1+1 -' k) by A2,A5,FINSEQ_6:175
.= r/.(k+(1+1) -' k)
.= r/.2 by NAT_D:34;
f is_sequence_on GoB f by GOBOARD5:def 5;
then
A11: f is_sequence_on GoB r by REVROT_1:28;
assume f is clockwise_oriented;
then consider i,j being Nat such that
A12: [i,j+1] in Indices GoB r and
A13: [i,j] in Indices GoB r and
A14: f/.k = (GoB r)*(i,j+1) and
A15: f/.(k+1) = (GoB r)*(i,j) by A2,A5,A9,A11,Th23,FINSEQ_4:21;
A16: 1 <= j & j <= width GoB r by A13,MATRIX_0:32;
A17: 1 <= j+1 & j+1 <= width GoB r by A12,MATRIX_0:32;
A18: 1 <= i & i <= len GoB r by A12,MATRIX_0:32;
1 <= i & i <= len GoB r by A12,MATRIX_0:32;
then (f/.(k+1))`1 = (GoB r)*(i,1)`1 by A15,A16,GOBOARD5:2
.= (f/.k)`1 by A14,A18,A17,GOBOARD5:2
.= E-bound L~f by A9,EUCLID:52;
hence thesis by A10,A7,A8,SPRECT_2:13;
end;
assume
A19: r/.2 in E-most L~f;
len r > 2 by TOPREAL8:3;
then
A20: r is_sequence_on GoB r & 1+1 in dom r by FINSEQ_3:25,GOBOARD5:def 5;
then consider i2,j2 being Nat such that
A21: [i2,j2] in Indices GoB r and
A22: r/.(1+1) = (GoB r)*(i2,j2) by GOBOARD1:def 9;
A23: j2 <= width GoB r by A21,MATRIX_0:32;
A24: [i,j] in Indices GoB r by JORDAN5D:def 4;
then
A25: 1 <= j by MATRIX_0:32;
then
A26: [i,j-'1+1] in Indices GoB r by A24,XREAL_1:235;
A27: L~r = L~f by REVROT_1:33;
then
A28: (GoB r)*(i,j) = r/.1 by A3,JORDAN5D:def 4;
then
A29: r/.1 = (GoB r)*(i,j-'1+1) by A25,XREAL_1:235;
(GoB r)*(i,j) in E-most L~r by A27,A3,A28,PSCOMP_1:50;
then (GoB r)*(i,j)`1 = (E-min L~r)`1 by PSCOMP_1:47;
then
A30: (GoB r)*(i2,j2)`1 = (GoB r)*(i,j)`1 by A27,A19,A22,PSCOMP_1:47;
then
A31: i2 = i by A24,A21,JORDAN1G:7;
A32: 1+1 <= len r by TOPREAL8:3;
then
A33: Int left_cell(r,1) c= LeftComp r by GOBOARD9:21;
Int left_cell(r,1) <> {} by A32,GOBOARD9:15;
then consider p being object such that
A34: p in Int left_cell(r,1) by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL2 by A34;
A35: LeftComp r is_a_component_of (L~r)` & UBD L~r is_a_component_of (L~r)`
by GOBOARD9:def 1,JORDAN2C:124;
A36: 1 <= j2 by A21,MATRIX_0:32;
A37: j <= width GoB r by A24,MATRIX_0:32;
rng r = rng f by FINSEQ_6:90,SPRECT_2:46;
then 1 in dom r by FINSEQ_3:31,SPRECT_2:46;
then |.i2-i2.|+|.j-j2.| = 1 by A24,A28,A20,A21,A22,A31,GOBOARD1:def 9;
then
A38: 0+|.j-j2.| = 1 by ABSVALUE:2;
A39: 1 <= i by A24,MATRIX_0:32;
(GoB r)*(i,j)`2 >= (GoB r)*(i2,j2)`2 by A3,A28,A19,A22,PSCOMP_1:47;
then j - j2 >= 0 by A39,A25,A31,A23,GOBOARD5:4,XREAL_1:48;
then
A40: j - j2 = 1 by A38,ABSVALUE:def 1;
then j2 = j-1;
then
A41: j2 = j-'1 by A25,XREAL_1:233;
then [i,j-'1] in Indices GoB r & r/.(1+1) = (GoB r)*(i,j-'1) by A24,A21,A22
,A30,JORDAN1G:7;
then left_cell(r,1,GoB r) = cell(GoB r,i,j-'1) by A1,A26,A29,GOBRD13:27;
then
A42: left_cell(r,1) = cell(GoB r,i,j-'1) by A32,JORDAN1H:21;
j-1 < j-0 by XREAL_1:15;
then j-'1 < width GoB r by A37,A40,A41,XXREAL_0:2;
then Int left_cell(r,1) = { |[t,s]| where t,s is Real:
(GoB r)*(i,1)`1 < t
& (GoB r)*(1,j-'1)`2 < s & s < (GoB r)*(1,j-'1+1)`2 } by A36,A41,A42,
GOBOARD6:23;
then consider t,s being Real such that
A43: p = |[t,s]| and
A44: (GoB r)*(i,1)`1 < t and
(GoB r)*(1,j-'1)`2 < s and
s < (GoB r)*(1,j-'1+1)`2 by A34;
now
assume east_halfline p meets L~r;
then (east_halfline p) /\ L~r <> {} by XBOOLE_0:def 7;
then consider a being object such that
A45: a in (east_halfline p) /\ L~r by XBOOLE_0:def 1;
A46: a in L~r by A45,XBOOLE_0:def 4;
A47: a in (east_halfline p) by A45,XBOOLE_0:def 4;
reconsider a as Point of TOP-REAL2 by A45;
a`1 >= p`1 by A47,TOPREAL1:def 11;
then
A48: a`1 >= t by A43,EUCLID:52;
(GoB r)*(i,1)`1 = (GoB r)*(i,j)`1 by A39,A25,A37,GOBOARD5:2;
then a`1 > (GoB r)*(i,j)`1 by A44,A48,XXREAL_0:2;
then a`1 > E-bound L~r by A27,A3,A28,EUCLID:52;
hence contradiction by A46,PSCOMP_1:24;
end;
then
A49: east_halfline p c= UBD L~r by JORDAN2C:127;
p in east_halfline p by TOPREAL1:38;
then LeftComp r meets UBD L~r by A33,A34,A49,XBOOLE_0:3;
then r is clockwise_oriented by A35,GOBOARD9:1,JORDAN1H:41;
hence thesis by JORDAN1H:40;
end;
theorem
for f being non constant standard special_circular_sequence holds f is
clockwise_oriented iff Rotate(f,S-max L~f)/.2 in S-most L~f
proof
set j = 1;
let f be non constant standard special_circular_sequence;
set r = Rotate(f,S-max L~f);
A1: r is_sequence_on GoB r by GOBOARD5:def 5;
len r > 2 by TOPREAL8:3;
then
A2: 1+1 in dom r by FINSEQ_3:25;
then consider i2,j2 being Nat such that
A3: [i2,j2] in Indices GoB r and
A4: r/.(1+1) = (GoB r)*(i2,j2) by A1,GOBOARD1:def 9;
A5: i2 <= len GoB r by A3,MATRIX_0:32;
set i = i_e_s r;
A6: S-max L~f in rng f by SPRECT_2:42;
then
A7: r/.1 = S-max L~f by FINSEQ_6:92;
A8: 2 <= len f by TOPREAL8:3;
thus f is clockwise_oriented implies r/.2 in S-most L~f
proof
set k = (S-max L~f)..f;
k < len f by SPRECT_5:14;
then
A9: k+1 <= len f by NAT_1:13;
1 <= k+1 by NAT_1:11;
then
A10: k+1 in dom f by A9,FINSEQ_3:25;
then f/.(k+1) = f.(k+1) by PARTFUN1:def 6;
then
A11: f/.(k+1) in rng f by A10,FUNCT_1:3;
A12: rng f c= L~f by A8,SPPOL_2:18;
A13: f/.k = S-max L~f by A6,FINSEQ_5:38;
k <= k+1 by NAT_1:13;
then
A14: f/.(k+1) = r/.(k+1+1 -' k) by A6,A9,FINSEQ_6:175
.= r/.(k+(1+1) -' k)
.= r/.2 by NAT_D:34;
f is_sequence_on GoB f by GOBOARD5:def 5;
then
A15: f is_sequence_on GoB r by REVROT_1:28;
assume f is clockwise_oriented;
then consider i,j being Nat such that
A16: [i+1,j] in Indices GoB r and
A17: [i,j] in Indices GoB r and
A18: f/.k = (GoB r)*(i+1,j) and
A19: f/.(k+1) = (GoB r)*(i,j) by A6,A9,A13,A15,Th24,FINSEQ_4:21;
A20: 1 <= i+1 & i+1 <= len GoB r by A16,MATRIX_0:32;
A21: 1 <= j & j <= width GoB r by A16,MATRIX_0:32;
A22: 1 <= j & j <= width GoB r by A16,MATRIX_0:32;
1 <= i & i <= len GoB r by A17,MATRIX_0:32;
then (f/.(k+1))`2 = (GoB r)*(1,j)`2 by A19,A21,GOBOARD5:1
.= (f/.k)`2 by A18,A20,A22,GOBOARD5:1
.= S-bound L~f by A13,EUCLID:52;
hence thesis by A14,A11,A12,SPRECT_2:11;
end;
assume
A23: r/.2 in S-most L~f;
A24: [i,j] in Indices GoB r by JORDAN5D:def 6;
then
A25: 1 <= i by MATRIX_0:32;
A26: L~r = L~f by REVROT_1:33;
then
A27: (GoB r)*(i,j) = r/.1 by A7,JORDAN5D:def 6;
then (GoB r)*(i,1)`2 = S-bound L~f by A7,EUCLID:52
.= (S-min L~f)`2 by EUCLID:52;
then (GoB r)*(i2,j2)`2 = (GoB r)*(i,1)`2 by A23,A4,PSCOMP_1:55;
then
A28: j2 = 1 by A24,A3,JORDAN1G:6;
A29: j <= width GoB r by A24,MATRIX_0:32;
rng r = rng f by FINSEQ_6:90,SPRECT_2:42;
then 1 in dom r by FINSEQ_3:31,SPRECT_2:42;
then |.1-1.|+|.i-i2.| = 1 by A1,A24,A27,A2,A3,A4,A28,GOBOARD1:def 9;
then
A30: 0+|.i-i2.| = 1 by ABSVALUE:2;
(GoB r)*(i2,j2)`1 <= (GoB r)*(i,1)`1 by A7,A27,A23,A4,PSCOMP_1:55;
then i - i2 >= 0 by A25,A29,A28,A5,GOBOARD5:3,XREAL_1:48;
then
A31: i - i2 = 1 by A30,ABSVALUE:def 1;
then i2 = i-1;
then
A32: i2 = i-'1 by A25,XREAL_1:233;
then
A33: 1 <= i-'1 by A3,MATRIX_0:32;
A34: i <= len GoB r by A24,MATRIX_0:32;
A35: 1+1 <= len r by TOPREAL8:3;
then
A36: Int left_cell(r,1) c= LeftComp r by GOBOARD9:21;
Int left_cell(r,1) <> {} by A35,GOBOARD9:15;
then consider p being object such that
A37: p in Int left_cell(r,1) by XBOOLE_0:def 1;
[i-'1+1,j] in Indices GoB r by A24,A25,XREAL_1:235;
then
j-'1 = 1-1 & left_cell(r,1,GoB r) = cell(GoB r,i-'1,j-'1) by A35,A1,A27,A3,A4
,A28,A31,A32,GOBRD13:25,XREAL_1:233;
then
A38: left_cell(r,1) = cell(GoB r,i-'1,0) by A35,JORDAN1H:21;
i - 1 < i by XREAL_1:146;
then i-'1 < len GoB r by A34,A31,A32,XXREAL_0:2;
then
A39: Int left_cell(r,1) = { |[t,s]| where t,s is Real:
(GoB r)*(i-'1,1)`1 <
t & t < (GoB r)*(i-'1+1,1)`1 & s < (GoB r)*(1,1)`2} by A33,A38,GOBOARD6:24;
reconsider p as Point of TOP-REAL2 by A37;
A40: LeftComp r is_a_component_of (L~r)` & UBD L~r is_a_component_of (L~r)`
by GOBOARD9:def 1,JORDAN2C:124;
consider t,s being Real such that
A41: p = |[t,s]| and
(GoB r)*(i-'1,1)`1 < t and
t < (GoB r)*(i-'1+1,1)`1 and
A42: s < (GoB r)*(1,1)`2 by A39,A37;
now
assume south_halfline p meets L~r;
then (south_halfline p) /\ L~r <> {} by XBOOLE_0:def 7;
then consider a being object such that
A43: a in (south_halfline p) /\ L~r by XBOOLE_0:def 1;
A44: a in L~r by A43,XBOOLE_0:def 4;
A45: a in (south_halfline p) by A43,XBOOLE_0:def 4;
reconsider a as Point of TOP-REAL2 by A43;
a`2 <= p`2 by A45,TOPREAL1:def 12;
then a`2 <= s by A41,EUCLID:52;
then
A46: a`2 < (GoB r)*(1,1)`2 by A42,XXREAL_0:2;
(GoB r)*(i,1)`2 = (GoB r)*(1,1)`2 by A25,A34,A29,GOBOARD5:1;
then a`2 < S-bound L~r by A26,A7,A27,A46,EUCLID:52;
hence contradiction by A44,PSCOMP_1:24;
end;
then
A47: south_halfline p c= UBD L~r by JORDAN2C:128;
p in south_halfline p by TOPREAL1:38;
then LeftComp r meets UBD L~r by A36,A37,A47,XBOOLE_0:3;
then r is clockwise_oriented by A40,GOBOARD9:1,JORDAN1H:41;
hence thesis by JORDAN1H:40;
end;
theorem
for C being compact non vertical non horizontal non empty
being_simple_closed_curve Subset of TOP-REAL 2 for p being Point of TOP-REAL 2
holds p`1 = (W-bound C + E-bound C)/2 & i > 0 & 1 <= k & k <= width Gauge(C,i)
& Gauge(C,i)*(Center Gauge(C,i),k) in Upper_Arc L~Cage(C,i) & p`2
= upper_bound(proj2.:
(LSeg(Gauge(C,1)*(Center Gauge(C,1),1), Gauge(C,i)*(Center Gauge(C,i),k)) /\
Lower_Arc L~Cage(C,i))) implies ex j st 1 <= j & j <= width Gauge(C,i) & p =
Gauge(C,i)*(Center Gauge(C,i),j)
proof
let C be compact non vertical non horizontal non empty
being_simple_closed_curve Subset of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: p`1 = (W-bound C + E-bound C)/2 and
A2: i > 0 and
A3: 1 <= k and
A4: k <= width Gauge(C,i) and
A5: Gauge(C,i)*(Center Gauge(C,i),k) in Upper_Arc L~Cage(C,i) and
A6: p`2 = upper_bound(proj2.:(LSeg(Gauge(C,1)*(Center Gauge(C,1),1),
Gauge(C,i)*
(Center Gauge(C,i),k)) /\ Lower_Arc L~Cage(C,i)));
set f=Lower_Seq(C,i);
set G=Gauge(C,i);
A7: Center Gauge(C,i) <= len G by JORDAN1B:13;
4 <= len G by JORDAN8:10;
then
A8: 1 <= len G by XXREAL_0:2;
4 <= len Gauge(C,1) by JORDAN8:10;
then 1 <= len Gauge(C,1) by XXREAL_0:2;
then
A9: Gauge(C,1)*(Center Gauge(C,1),1)`1 = G*(Center G,1)`1 by A2,A8,JORDAN1A:36;
A10: 1 <= Center Gauge(C,1) & Center Gauge(C,1) <= len Gauge(C,1) by
JORDAN1B:11,13;
A11: 1 <= Center Gauge(C,i) by JORDAN1B:11;
then
A12: G*(Center G,k)`1 = G*(Center G,1)`1 by A3,A4,A7,GOBOARD5:2;
0+1 <= i by A2,NAT_1:13;
then
A13: Gauge(C,1)*(Center Gauge(C,1),1)`2 <= G*(Center G,1)`2 by A11,A7,A10,
JORDAN1A:43;
A14: LSeg(Gauge(C,1)*(Center Gauge(C,1),1),G*(Center G,k)) /\ L~f c= LSeg(G*
(Center G,1),G*(Center G,k)) /\ L~f
proof
let a be object;
assume
A15: a in LSeg(Gauge(C,1)*(Center Gauge(C,1),1),G*(Center G,k)) /\ L~f;
then reconsider q=a as Point of TOP-REAL 2;
A16: a in LSeg(Gauge(C,1)*(Center Gauge(C,1),1),G*(Center G,k)) by A15,
XBOOLE_0:def 4;
A17: a in L~f by A15,XBOOLE_0:def 4;
then q in L~f \/ L~Upper_Seq(C,i) by XBOOLE_0:def 3;
then q in L~Cage(C,i) by JORDAN1E:13;
then S-bound L~Cage(C,i) <= q`2 by PSCOMP_1:24;
then
A18: G*(Center G,1)`2 <= q`2 by A7,JORDAN1A:72,JORDAN1B:11;
G*(Center G,1)`2 <= G*(Center G,k)`2 by A3,A4,A11,A7,JORDAN1A:19;
then Gauge(C,1)*(Center Gauge(C,1),1)`2 <= G*(Center G,k)`2 by A13,
XXREAL_0:2;
then
A19: q`2 <= G*(Center G,k) `2 by A16,TOPREAL1:4;
q`1 = G*(Center G,1)`1 by A9,A12,A16,GOBOARD7:5;
then q in LSeg(G*(Center G,1),G*(Center G,k)) by A12,A19,A18,GOBOARD7:7;
hence thesis by A17,XBOOLE_0:def 4;
end;
A20: G*(Center G,k) in LSeg(Gauge(C,1)*(Center Gauge(C,1),1),G*(Center G,k))
by RLTOPSP1:68;
G*(Center G,1)`2 <= G*(Center G,k)`2 by A3,A4,A11,A7,JORDAN1A:19;
then
G*(Center G,1) in LSeg(Gauge(C,1)*(Center Gauge(C,1),1),G*(Center G,k )
) by A9,A12,A13,GOBOARD7:7;
then
LSeg(G*(Center G,1),G*(Center G,k)) c= LSeg(Gauge(C,1)*(Center Gauge(C,
1),1),G*(Center G,k)) by A20,TOPREAL1:6;
then LSeg(G*(Center G,1),G*(Center G,k)) /\ L~f c= LSeg(Gauge(C,1)*(Center
Gauge(C,1),1),G*(Center G,k)) /\ L~f by XBOOLE_1:27;
then LSeg(G*(Center G,1),G*(Center G,k)) /\ L~f = LSeg(Gauge(C,1)*(Center
Gauge(C,1),1),G*(Center G,k))/\L~f by A14,XBOOLE_0:def 10;
then
A21: upper_bound(proj2.:(LSeg(G*(Center Gauge(C,i),1),
G*(Center Gauge(C,i),k)) /\ L~
f)) = upper_bound(proj2.:(LSeg(Gauge(C,1)*(Center Gauge(C,1),1),
Gauge(C,i)*(Center
Gauge(C,i),k)) /\ Lower_Arc L~Cage(C,i))) by A2,JORDAN1G:56;
A22: f is_sequence_on G & Upper_Arc L~Cage(C,i) c= L~Cage(C,i) by JORDAN1F:12
,JORDAN6:61;
len G >= 4 by JORDAN8:10;
then width G >= 4 by JORDAN8:def 1;
then 1 <= width G by XXREAL_0:2;
then
A23: [Center Gauge(C,i),1] in Indices G by A11,A7,MATRIX_0:30;
[Center Gauge(C,i),k] in Indices G by A3,A4,A11,A7,MATRIX_0:30;
then consider n such that
A24: 1 <= n and
A25: n <= k and
A26: G*(Center Gauge(C,i),n)`2 =
upper_bound(proj2.:(LSeg(G*(Center Gauge(C,i),1
),G*(Center Gauge(C,i),k)) /\ L~f)) by A3,A4,A5,A11,A7,A23,A22,JORDAN1F:2
,JORDAN1G:46;
take n;
thus 1 <= n by A24;
thus n <= width Gauge(C,i) by A4,A25,XXREAL_0:2;
then p`1 = (Gauge(C,i)*(Center Gauge(C,i),n))`1 by A1,A2,A24,JORDAN1G:35;
hence thesis by A6,A26,A21,TOPREAL3:6;
end;