:: Left and Right Component of the Complement of a Special Closed Curve
:: by Andrzej Trybulec
::
:: Received October 29, 1995
:: Copyright (c) 1995-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, FUNCT_1, GOBOARD5, SUBSET_1, REAL_1, PRE_TOPC, EUCLID,
GOBOARD1, CONNSP_1, XBOOLE_0, RELAT_1, STRUCT_0, TARSKI, RELAT_2,
RLTOPSP1, CONVEX1, FINSEQ_1, FINSEQ_5, ARYTM_3, ARYTM_1, XXREAL_0,
PARTFUN1, MCART_1, GOBOARD2, CARD_1, MATRIX_1, COMPLEX1, TREES_1, TOPS_1,
TOPREAL1, GOBOARD9, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
COMPLEX1, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1,
MATRIX_0, SEQ_4, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1, RLVECT_1,
RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, FINSEQ_5, GOBOARD5,
XXREAL_0;
constructors REAL_1, FINSEQ_5, TOPS_1, CONNSP_1, GOBOARD2, GOBOARD5, GOBOARD1,
NAT_D, RELSET_1, CONVEX1, RVSUM_1, SEQ_4;
registrations RELSET_1, NUMBERS, XXREAL_0, FINSEQ_1, FINSEQ_6, STRUCT_0,
PRE_TOPC, EUCLID, GOBOARD2, GOBOARD5, ORDINAL1, RLTOPSP1, JORDAN1,
XREAL_0, INT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, GOBOARD5, GOBOARD1, JORDAN1, XBOOLE_0, SEQM_3;
equalities GOBOARD5, XBOOLE_0, STRUCT_0;
expansions GOBOARD1, XBOOLE_0;
theorems CONNSP_1, GOBOARD5, TOPS_1, SPPOL_2, PRE_TOPC, GOBOARD1, TARSKI,
TOPREAL1, GOBOARD2, FINSEQ_3, NAT_1, SUBSET_1, FINSEQ_6, GOBOARD6,
GOBOARD7, GOBOARD8, FINSEQ_1, FINSEQ_5, JORDAN1, TSEP_1, INT_1, XBOOLE_0,
XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, PARTFUN1, MATRIX_0, NAT_D, SEQM_3,
SEQ_4, XREAL_0;
schemes NAT_1;
begin
reserve f for non constant standard special_circular_sequence,
i,j,k,i1,i2,j1,j2 for Nat,
r,s,r1,s1,r2,s2 for Real,
p,q for Point of TOP-REAL 2,
G for Go-board;
theorem Th1:
for GX being TopSpace, A1,A2,B being Subset of GX
st A1 is_a_component_of B & A2 is_a_component_of B holds
A1 = A2 or A1 misses A2
proof
let GX be TopSpace, A1,A2,B be Subset of GX;
assume A1 is_a_component_of B;
then
A1: ex B1 being Subset of GX|B st B1 = A1& B1 is a_component by CONNSP_1:def 6;
assume A2 is_a_component_of B;
then ex B2 being Subset of GX|B st B2 = A2 & B2 is a_component
by CONNSP_1:def 6;
hence thesis by A1,CONNSP_1:35;
end;
theorem Th2:
for GX being TopSpace, A,B being Subset of GX,
AA being Subset of GX|B st A = AA holds GX|A = GX|B|AA
proof
let GX be TopSpace, A,B be Subset of GX;
let AA be Subset of GX|B;
assume
A1: A = AA;
the carrier of GX|A = [#](GX|A) .= A by PRE_TOPC:def 5;
then reconsider GY = GX|A as strict SubSpace of GX|B by A1,TSEP_1:4;
[#] GY = AA by A1,PRE_TOPC:def 5;
hence thesis by PRE_TOPC:def 5;
end;
theorem Th3:
for GX being non empty TopSpace, A, B being non empty Subset of GX
st A c= B & A is connected
ex C being Subset of GX st C is_a_component_of B & A c= C
proof
let GX be non empty TopSpace, A, B be non empty Subset of GX such that
A1: A c= B and
A2: A is connected;
consider p being object such that
A3: p in A by XBOOLE_0:def 1;
A4: B = [#](GX|B) by PRE_TOPC:def 5
.= the carrier of GX|B;
then reconsider p as Point of GX|B by A1,A3;
reconsider C = Component_of p as Subset of GX by PRE_TOPC:11;
take C;
A5: Component_of p is a_component by CONNSP_1:40;
hence C is_a_component_of B by CONNSP_1:def 6;
reconsider AA = A as Subset of GX|B by A1,A4;
GX|A is connected by A2,CONNSP_1:def 3;
then GX|B|AA is connected by Th2;
then
A6: AA is connected by CONNSP_1:def 3;
p in Component_of p by CONNSP_1:38;
then AA /\ Component_of p <> {}(GX|B) by A3,XBOOLE_0:def 4;
then AA meets Component_of p;
hence thesis by A5,A6,CONNSP_1:36;
end;
theorem Th4:
for GX being non empty TopSpace, A,B,C,D being Subset of GX
st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D
holds B c= C
proof
let GX be non empty TopSpace, A,B,C,D be Subset of GX such that
A1: B is connected and
A2: C is_a_component_of D and
A3: A c= C and
A4: A meets B and
A5: B c= D;
A6: A <> {} by A4;
A7: B <> {} by A4;
reconsider A,B as non empty Subset of GX by A4;
reconsider C,D as non empty Subset of GX by A3,A5,A6,A7,XBOOLE_1:3;
consider CC being Subset of GX such that
A8: CC is_a_component_of D and
A9: B c= CC by A1,A5,Th3;
A10: A meets CC by A4,A9,XBOOLE_1:63;
A11: ex C1 being Subset of GX|D st C1 = C & C1 is a_component
by A2,CONNSP_1:def 6;
ex CC1 being Subset of GX|D st CC1 = CC & CC1 is a_component
by A8,CONNSP_1:def 6;
hence thesis by A3,A9,A10,A11,CONNSP_1:35,XBOOLE_1:63;
end;
registration
cluster convex non empty for Subset of TOP-REAL 2;
existence
proof set p = the Point of TOP-REAL 2;
take LSeg(p,p);
thus thesis;
end;
end;
::$CT
theorem Th5: :: ouogolnic !!!
for P,Q being convex Subset of TOP-REAL 2 holds P /\ Q is convex
proof
let P,Q be convex Subset of TOP-REAL 2;
let p,q;
assume that
A1: p in P /\ Q and
A2: q in P /\ Q;
A3: p in P by A1,XBOOLE_0:def 4;
q in P by A2,XBOOLE_0:def 4;
then
A4: LSeg(p,q) c= P by A3,JORDAN1:def 1;
A5: p in Q by A1,XBOOLE_0:def 4;
q in Q by A2,XBOOLE_0:def 4;
then LSeg(p,q) c= Q by A5,JORDAN1:def 1;
hence thesis by A4,XBOOLE_1:19;
end;
theorem Th6:
for f being FinSequence of TOP-REAL 2 holds Rev X_axis f = X_axis Rev f
proof
let f be FinSequence of TOP-REAL 2;
A1: len Rev X_axis f = len X_axis f by FINSEQ_5:def 3
.= len f by GOBOARD1:def 1
.= len Rev f by FINSEQ_5:def 3;
len X_axis f = len f by GOBOARD1:def 1;
then
A2: dom X_axis f = dom f by FINSEQ_3:29;
A3: len f = len Rev f by FINSEQ_5:def 3;
now
let k such that
A4: k in dom Rev X_axis f;
set l = len f + 1 -' k;
A5: k <= len f by A1,A3,A4,FINSEQ_3:25;
len f < len f + 1 by NAT_1:13;
then
A6: l + k = len f + 1 by A5,XREAL_1:235,XXREAL_0:2;
A7: Rev Rev X_axis f = X_axis f;
then
A8: l in dom X_axis f by A1,A3,A4,A6,FINSEQ_5:59;
thus (Rev X_axis f).k = (Rev X_axis f)/.k by A4,PARTFUN1:def 6
.= (X_axis f)/.l by A1,A3,A4,A6,A7,FINSEQ_5:66
.= (X_axis f).l by A8,PARTFUN1:def 6
.= (f/.l)`1 by A8,GOBOARD1:def 1
.= ((Rev f)/.k)`1 by A1,A2,A3,A4,A6,A7,FINSEQ_5:59,66;
end;
hence thesis by A1,GOBOARD1:def 1;
end;
theorem Th7:
for f being FinSequence of TOP-REAL 2 holds Rev Y_axis f = Y_axis Rev f
proof
let f be FinSequence of TOP-REAL 2;
A1: len Rev Y_axis f = len Y_axis f by FINSEQ_5:def 3
.= len f by GOBOARD1:def 2
.= len Rev f by FINSEQ_5:def 3;
len Y_axis f = len f by GOBOARD1:def 2;
then
A2: dom Y_axis f = dom f by FINSEQ_3:29;
A3: len f = len Rev f by FINSEQ_5:def 3;
now
let k such that
A4: k in dom Rev Y_axis f;
set l = len f + 1 -' k;
A5: k <= len f by A1,A3,A4,FINSEQ_3:25;
len f < len f + 1 by NAT_1:13;
then
A6: l + k = len f + 1 by A5,XREAL_1:235,XXREAL_0:2;
A7: Rev Rev Y_axis f = Y_axis f;
then
A8: l in dom Y_axis f by A1,A3,A4,A6,FINSEQ_5:59;
thus (Rev Y_axis f).k = (Rev Y_axis f)/.k by A4,PARTFUN1:def 6
.= (Y_axis f)/.l by A1,A3,A4,A6,A7,FINSEQ_5:66
.= (Y_axis f).l by A8,PARTFUN1:def 6
.= (f/.l)`2 by A8,GOBOARD1:def 2
.= ((Rev f)/.k)`2 by A1,A2,A3,A4,A6,A7,FINSEQ_5:59,66;
end;
hence thesis by A1,GOBOARD1:def 2;
end;
Lm1: for f,ff being non empty FinSequence of TOP-REAL 2 st ff = Rev f
holds GoB ff = GoB f
proof
let f,ff be non empty FinSequence of TOP-REAL 2;
assume
A1: ff = Rev f;
then
A2: Rev X_axis f = X_axis ff by Th6;
A3: rng Incr X_axis ff = rng X_axis ff by SEQ_4:def 21
.= rng X_axis f by A2,FINSEQ_5:57;
len Incr X_axis ff = card rng X_axis ff by SEQ_4:def 21
.= card rng X_axis f by A2,FINSEQ_5:57;
then
A4: Incr X_axis f = Incr X_axis ff by A3,SEQ_4:def 21;
A5: Rev Y_axis f = Y_axis ff by A1,Th7;
A6: rng Incr Y_axis ff = rng Y_axis ff by SEQ_4:def 21
.= rng Y_axis f by A5,FINSEQ_5:57;
len Incr Y_axis ff = card rng Y_axis ff by SEQ_4:def 21
.= card rng Y_axis f by A5,FINSEQ_5:57;
then Incr Y_axis f = Incr Y_axis ff by A6,SEQ_4:def 21;
hence GoB ff = GoB(Incr X_axis f,Incr Y_axis f) by A4,GOBOARD2:def 2
.= GoB f by GOBOARD2:def 2;
end;
registration
cluster non constant for FinSequence;
existence
proof
take <*1,2*>,1,2;
A1: 1 in {1,2} by TARSKI:def 2;
2 in {1,2} by TARSKI:def 2;
hence 1 in dom <*1,2*> & 2 in dom <*1,2*> by A1,FINSEQ_1:2,89;
thus thesis;
end;
end;
registration
let f be non constant FinSequence;
cluster Rev f -> non constant;
coherence
proof
consider i,j such that
A1: i in dom f and
A2: j in dom f and
A3: f.i <> f.j by SEQM_3:def 10;
A4: i <= len f by A1,FINSEQ_3:25;
j <= len f by A2,FINSEQ_3:25;
then reconsider k1 = len f -i, l1 = len f -j as Element of NAT by A4,
INT_1:5;
take k = k1+1, l = l1+1;
k + i = len f +1;
hence k in dom Rev f by A1,FINSEQ_5:59;
then
A5: (Rev f).k = f.(len f -k +1) by FINSEQ_5:def 3
.= f.(0 + i);
l + j = len f +1;
hence l in dom Rev f by A2,FINSEQ_5:59;
then (Rev f).l = f.(len f -l +1) by FINSEQ_5:def 3
.= f.(0 + j);
hence thesis by A3,A5;
end;
end;
definition
let f be standard special_circular_sequence;
redefine func Rev f -> standard special_circular_sequence; :: redefines Rev (FINSEQ_5, definition)
coherence
proof
reconsider ff = Rev f as non empty FinSequence of TOP-REAL 2;
A1: Rev ff = f;
A2: GoB ff = GoB f by Lm1;
A3: f is_sequence_on GoB f by GOBOARD5:def 5;
A4: len f = len ff by FINSEQ_5:def 3;
A5: ff is standard
proof
hereby
let k such that
A6: k in dom ff;
set l = len f + 1 -' k;
A7: k <= len f by A4,A6,FINSEQ_3:25;
len f < len f + 1 by NAT_1:13;
then
A8: l + k = len f + 1 by A7,XREAL_1:235,XXREAL_0:2;
then l in dom f by A1,A4,A6,FINSEQ_5:59;
then consider i,j such that
A9: [i,j] in Indices GoB f and
A10: f/.l = (GoB f)*(i,j) by A3;
take i,j;
thus [i,j] in Indices GoB ff by A9,Lm1;
thus ff/.k = (GoB ff)*(i,j) by A1,A2,A4,A6,A8,A10,FINSEQ_5:66;
end;
let k such that
A11: k in dom ff and
A12: k+1 in dom ff;
set l = len f + 1 -' (k + 1);
k <= len f by A4,A11,FINSEQ_3:25;
then k+1 <= len f +1 by XREAL_1:6;
then
A13: l + (k+1) = len f + 1 by XREAL_1:235;
then
A14: l in dom f by A1,A4,A12,FINSEQ_5:59;
A15: l+1 + k = len f + 1 by A13;
then
A16: l+1 in dom f by A1,A4,A11,FINSEQ_5:59;
let i1,j1,i2,j2 such that
A17: [i1,j1] in Indices GoB ff and
A18: [i2,j2] in Indices GoB ff and
A19: ff/.k = (GoB ff)*(i1,j1) and
A20: ff/.(k+1) = (GoB ff)*(i2,j2);
A21: |.i2-i1.| = |.-(i1-i2).| .= |.i1-i2.| by COMPLEX1:52;
A22: |.j2-j1.| = |.-(j1-j2).| .= |.j1-j2.| by COMPLEX1:52;
A23: f/.l = (GoB f)*(i2,j2) by A1,A2,A4,A12,A13,A20,FINSEQ_5:66;
f/.(l+1) = (GoB f)*(i1,j1) by A1,A2,A4,A11,A15,A19,FINSEQ_5:66;
hence |.i1-i2.|+|.j1-j2.| = 1
by A2,A3,A14,A16,A17,A18,A21,A22,A23;
end;
A24: ff/.1 = f/.len f by FINSEQ_5:65
.= f/.1 by FINSEQ_6:def 1
.= ff/.len ff by A4,FINSEQ_5:65;
ff is s.c.c.
proof
let i,j such that
A25: i+1 < j and
A26: i > 1 & j < len ff or j+1 < len ff;
set k = len f -' i, l = len f -' j;
A27: j <= len f by A4,A26,NAT_1:13;
then
A28: l + j = len f by XREAL_1:235;
i < j by A25,NAT_1:13;
then
A29: k + i = len f by A27,XREAL_1:235,XXREAL_0:2;
then i+1+k = l+1+j by A28;
then l+1+j < j+k by A25,XREAL_1:6;
then
A30: l+1 < k by XREAL_1:6;
A31: j+1 <= len f by A4,A26,NAT_1:13;
per cases by A31,NAT_1:14,XXREAL_0:1;
suppose j+1 = len f;
then k+1 < len f by A26,A29,FINSEQ_5:def 3,XREAL_1:6;
then LSeg(f,k) misses LSeg(f,l) by A30,GOBOARD5:def 4;
then
A32: LSeg(f,k) /\ LSeg(f,l) = {};
LSeg(f,k) = LSeg(ff,i) by A29,SPPOL_2:2;
hence LSeg(ff,i) /\ LSeg(ff,j) = {} by A28,A32,SPPOL_2:2;
end;
suppose that
A33: i >= 1 and
A34: j+1 < len f;
A35: l > 1 by A28,A34,XREAL_1:6;
k+1 <= len f by A29,A33,XREAL_1:6;
then k < len f by NAT_1:13;
then LSeg(f,k) misses LSeg(f,l) by A30,A35,GOBOARD5:def 4;
then
A36: LSeg(f,k) /\ LSeg(f,l) = {};
LSeg(f,k) = LSeg(ff,i) by A29,SPPOL_2:2;
hence LSeg(ff,i) /\ LSeg(ff,j) = {} by A28,A36,SPPOL_2:2;
end;
suppose i = 0;
then LSeg(ff,i) = {} by TOPREAL1:def 3;
hence LSeg(ff,i) /\ LSeg(ff,j) = {};
end;
end;
hence thesis by A5,A24,FINSEQ_6:def 1,SPPOL_2:28,40;
end;
end;
theorem Th8:
i >= 1 & j >= 1 & i+j = len f implies left_cell(f,i) = right_cell(Rev f,j)
proof
assume that
A1: i >= 1 and
A2: j >= 1 and
A3: i+j = len f;
A4: i+1 <= len f by A2,A3,XREAL_1:6;
len f = len Rev f by FINSEQ_5:def 3;
then
A5: j+1 <= len Rev f by A1,A3,XREAL_1:6;
A6: GoB Rev f = GoB f by Lm1;
now
let i1,j1,i2,j2 be Nat such that
A7: [i1,j1] in Indices GoB f and
A8: [i2,j2] in Indices GoB f and
A9: f/.i = (GoB f)*(i1,j1) and
A10: f/.(i+1) = (GoB f)*(i2,j2);
1 <= i+1 by NAT_1:11;
then
A11: i+1 in dom f by A4,FINSEQ_3:25;
i+1+j = len f + 1 by A3;
then
A12: (Rev f)/.j = (GoB f)*(i2,j2) by A10,A11,FINSEQ_5:66;
i <= len f by A4,NAT_1:13;
then
A13: i in dom f by A1,FINSEQ_3:25;
j+1+i = len f + 1 by A3;
then
A14: (Rev f)/.(j+1) = (GoB f)*(i1,j1) by A9,A13,FINSEQ_5:66;
1 <= i1 by A7,MATRIX_0:32;
then
A15: i1-'1+1 = i1 by XREAL_1:235;
1 <= j1 by A7,MATRIX_0:32;
then
A16: j1-'1+1 = j1 by XREAL_1:235;
reconsider i19=i1, i29=i2, j19=j1, j29=j2 as Element of REAL
by XREAL_0:def 1;
f is_sequence_on GoB f by GOBOARD5:def 5;
then |.i1-i2.|+|.j1-j2.| = 1 by A7,A8,A9,A10,A11,A13;
then
A17: |.i19-i29.|=1 & j1=j2 or |.j19-j29.|=1 & i1=i2 by SEQM_3:42;
per cases by A17,SEQM_3:41;
case i1 = i2 & j1+1 = j2;
hence right_cell(Rev f,j) = cell(GoB f,i1-'1,j1)
by A2,A5,A6,A7,A8,A12,A14,A15,GOBOARD5:30;
end;
case i1+1 = i2 & j1 = j2;
hence right_cell(Rev f,j) = cell(GoB f,i1,j1)
by A2,A5,A6,A7,A8,A12,A14,A16,GOBOARD5:29;
end;
case i1 = i2+1 & j1 = j2;
hence right_cell(Rev f,j) = cell(GoB f,i2,j2-'1)
by A2,A5,A6,A7,A8,A12,A14,A16,GOBOARD5:28;
end;
case i1 = i2 & j1 = j2+1;
hence right_cell(Rev f,j) = cell(GoB f,i1,j2)
by A2,A5,A6,A7,A8,A12,A14,A15,GOBOARD5:27;
end;
end;
hence thesis by A1,A4,GOBOARD5:def 7;
end;
theorem Th9:
i >= 1 & j >= 1 & i+j = len f implies left_cell(Rev f,i) = right_cell(f,j)
proof
A1: len Rev f = len f by FINSEQ_5:def 3;
Rev Rev f = f;
hence thesis by A1,Th8;
end;
theorem Th10:
1 <= k & k+1 <= len f implies ex i,j st i <= len GoB f & j <= width GoB f &
cell(GoB f,i,j) = left_cell(f,k)
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f;
A3: f is_sequence_on GoB f by GOBOARD5:def 5;
k <= len f by A2,NAT_1:13;
then
A4: k in dom f by A1,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A5: [i1,j1] in Indices GoB f and
A6: f/.k = (GoB f)*(i1,j1) by A3;
1 <= k+1 by NAT_1:11;
then
A7: k+1 in dom f by A2,FINSEQ_3:25;
then consider i2,j2 being Nat such that
A8: [i2,j2] in Indices GoB f and
A9: f/.(k+1) = (GoB f)*(i2,j2) by A3;
1 <= i1 by A5,MATRIX_0:32;
then
A10: i1-'1+1 = i1 by XREAL_1:235;
1 <= j1 by A5,MATRIX_0:32;
then
A11: j1-'1+1 = j1 by XREAL_1:235;
reconsider i19=i1, i29=i2, j19=j1, j29=j2 as Element of REAL
by XREAL_0:def 1;
|.i1-i2.|+|.j1-j2.| = 1 by A3,A4,A5,A6,A7,A8,A9;
then
A12: |.i19-i29.|=1 & j1=j2 or |.j19-j29.|=1 & i1=i2 by SEQM_3:42;
A13: i1 <= len GoB f by A5,MATRIX_0:32;
A14: j1 <= width GoB f by A5,MATRIX_0:32;
per cases by A12,SEQM_3:41;
suppose
A15: i1 = i2 & j1+1 = j2;
take i1-'1,j1;
i1-'1 <= i1 by NAT_D:35;
hence i1-'1 <= len GoB f by A13,XXREAL_0:2;
thus j1 <= width GoB f by A5,MATRIX_0:32;
thus thesis by A1,A2,A5,A6,A8,A9,A10,A15,GOBOARD5:27;
end;
suppose
A16: i1+1 = i2 & j1 = j2;
take i1,j1;
thus i1 <= len GoB f by A5,MATRIX_0:32;
thus j1 <= width GoB f by A5,MATRIX_0:32;
thus thesis by A1,A2,A5,A6,A8,A9,A11,A16,GOBOARD5:28;
end;
suppose
A17: i1 = i2+1 & j1 = j2;
take i2,j1-'1;
thus i2 <= len GoB f by A8,MATRIX_0:32;
j1-'1 <= j1 by NAT_D:35;
hence j1-'1 <= width GoB f by A14,XXREAL_0:2;
thus thesis by A1,A2,A5,A6,A8,A9,A11,A17,GOBOARD5:29;
end;
suppose
A18: i1 = i2 & j1 = j2+1;
take i1,j2;
thus i1 <= len GoB f by A5,MATRIX_0:32;
thus j2 <= width GoB f by A8,MATRIX_0:32;
thus thesis by A1,A2,A5,A6,A8,A9,A10,A18,GOBOARD5:30;
end;
end;
theorem Th11:
j <= width G implies Int h_strip(G,j) is convex
proof
assume
A1: j <= width G;
per cases by A1,NAT_1:14,XXREAL_0:1;
suppose j = 0;
then Int h_strip(G,j) = { |[r,s]| : s < G*(1,1)`2 } by GOBOARD6:15;
hence thesis by JORDAN1:17;
end;
suppose j = width G;
then Int h_strip(G,j) = { |[r,s]| : G*(1,width G)`2 < s } by GOBOARD6:16;
hence thesis by JORDAN1:15;
end;
suppose 1 <= j & j < width G;
then
A2: Int h_strip(G,j) = { |[r,s]| : G*(1,j)`2 < s & s < G*(1,j+1)`2 }
by GOBOARD6:17;
A3: { |[r,s]| : G*(1,j)`2 < s} c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in { |[r,s]| : G*(1,j)`2 < s};
then ex r,s st x = |[r,s]| & G*(1,j)`2 < s;
hence thesis;
end;
{ |[r,s]| : s < G*(1,j+1)`2 } c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in { |[r,s]| : s < G*(1,j+1)`2 };
then ex r,s st x = |[r,s]| & s < G*(1,j+1)`2;
hence thesis;
end;
then reconsider P = { |[r,s]| : G*(1,j)`2 < s},
Q = { |[r,s]| : s < G*(1,j+1)`2 } as Subset of TOP-REAL 2 by A3;
A4: Int h_strip(G,j) = P /\ Q
proof
hereby
let x be object;
assume x in Int h_strip(G,j);
then
A5: ex r,s st x = |[r,s]| & G*(1,j)`2 < s & s < G*(1,j+1)`2 by A2;
then
A6: x in P;
x in Q by A5;
hence x in P /\ Q by A6,XBOOLE_0:def 4;
end;
let x be object;
assume
A7: x in P /\ Q;
then x in P by XBOOLE_0:def 4;
then consider r1,s1 such that
A8: x = |[r1,s1]| and
A9: G*(1,j)`2 < s1;
x in Q by A7,XBOOLE_0:def 4;
then consider r2,s2 such that
A10: x = |[r2,s2]| and
A11: s2 < G*(1,j+1)`2;
s1 = s2 by A8,A10,SPPOL_2:1;
hence thesis by A2,A8,A9,A11;
end;
A12: P is convex by JORDAN1:15;
Q is convex by JORDAN1:17;
hence thesis by A4,A12,Th5;
end;
end;
theorem Th12:
i <= len G implies Int v_strip(G,i) is convex
proof
assume
A1: i <= len G;
per cases by A1,NAT_1:14,XXREAL_0:1;
suppose i = 0;
then Int v_strip(G,i) = { |[r,s]| : r < G*(1,1)`1 } by GOBOARD6:12;
hence thesis by JORDAN1:13;
end;
suppose i = len G;
then Int v_strip(G,i) = { |[r,s]| : G*(len G,1)`1 < r } by GOBOARD6:13;
hence thesis by JORDAN1:11;
end;
suppose 1 <= i & i < len G;
then
A2: Int v_strip(G,i) = { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 }
by GOBOARD6:14;
A3: { |[r,s]| : G*(i,1)`1 < r} c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in { |[r,s]| : G*(i,1)`1 < r};
then ex r,s st x = |[r,s]| & G*(i,1)`1 < r;
hence thesis;
end;
{ |[r,s]| : r < G*(i+1,1)`1 } c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in { |[r,s]| : r < G*(i+1,1)`1 };
then ex r,s st x = |[r,s]| & r < G*(i+1,1)`1;
hence thesis;
end;
then reconsider P = { |[r,s]| : G*(i,1)`1 < r},
Q = { |[r,s]| : r < G*(i+1,1)`1 } as Subset of TOP-REAL 2 by A3;
A4: Int v_strip(G,i) = P /\ Q
proof
hereby
let x be object;
assume x in Int v_strip(G,i);
then
A5: ex r,s st x = |[r,s]| & G*(i,1)`1 < r & r < G*(i+1,1)`1 by A2;
then
A6: x in P;
x in Q by A5;
hence x in P /\ Q by A6,XBOOLE_0:def 4;
end;
let x be object;
assume
A7: x in P /\ Q;
then x in P by XBOOLE_0:def 4;
then consider r1,s1 such that
A8: x = |[r1,s1]| and
A9: G*(i,1)`1 < r1;
x in Q by A7,XBOOLE_0:def 4;
then consider r2,s2 such that
A10: x = |[r2,s2]| and
A11: r2 < G*(i+1,1)`1;
r1 = r2 by A8,A10,SPPOL_2:1;
hence thesis by A2,A8,A9,A11;
end;
A12: P is convex by JORDAN1:11;
Q is convex by JORDAN1:13;
hence thesis by A4,A12,Th5;
end;
end;
theorem Th13:
i <= len G & j <= width G implies Int cell(G,i,j) <> {}
proof
assume that
A1: i <= len G and
A2: j <= width G;
A3: j = width G or j < width G by A2,XXREAL_0:1;
A4: i = len G or i < len G by A1,XXREAL_0:1;
set p = the Point of TOP-REAL 2;
per cases by A3,A4,NAT_1:13,14;
suppose 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G;
then LSeg(1/2*(G*(i,j)+G*
(i+1,j+1)),p) meets Int cell(G,i,j) by GOBOARD6:82;
hence thesis;
end;
suppose 1 <= i & i+1 <= len G & j = width G;
then LSeg(p,1/2*(G*(i,j)+G*(i+1,j))+|[0,1]|) meets Int cell(G,i,j)
by GOBOARD6:83;
hence thesis;
end;
suppose 1 <= i & i+1 <= len G & j = 0;
then LSeg(1/2*(G*(i,j+1)+G*(i+1,j+1))- |[0,1]|,p) meets Int cell(G,i,j)
by GOBOARD6:84;
hence thesis;
end;
suppose 1 <= j & j+1 <= width G & i = 0;
then LSeg(1/2*(G*(i+1,j)+G*(i+1,j+1))- |[1,0]|,p) meets Int cell(G,i,j)
by GOBOARD6:85;
hence thesis;
end;
suppose 1 <= j & j+1 <= width G & i = len G;
then LSeg(p,1/2*(G*(i,j)+G*(i,j+1))+|[1,0]|) meets Int cell(G,i,j)
by GOBOARD6:86;
hence thesis;
end;
suppose i = 0 & j = 0;
then LSeg(p,G*(i+1,j+1)- |[1,1]|) meets Int cell(G,i,j) by GOBOARD6:87;
hence thesis;
end;
suppose i = len G & j = width G;
then LSeg(p,G*(i,j)+|[1,1]|) meets Int cell(G,i,j) by GOBOARD6:88;
hence thesis;
end;
suppose i = 0 & j = width G;
then LSeg(p,G*(i+1,j)+|[-1,1]|) meets Int cell(G,i,j) by GOBOARD6:89;
hence thesis;
end;
suppose i = len G & j = 0;
then LSeg(p,G*(i,j+1)+|[1,-1]|) meets Int cell(G,i,j) by GOBOARD6:90;
hence thesis;
end;
end;
theorem Th14:
1 <= k & k+1 <= len f implies Int left_cell(f,k) <> {}
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f;
ex i,j st i <= len GoB f & j <=
width GoB f & cell(GoB f,i,j) = left_cell(f,k) by A1,A2,Th10;
hence thesis by Th13;
end;
theorem Th15:
1 <= k & k+1 <= len f implies Int right_cell(f,k) <> {}
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f;
A3: len f = len Rev f by FINSEQ_5:def 3;
k <= len f by A2,NAT_1:13;
then
A4: len f-'k+k = len f by XREAL_1:235;
then
A5: len f-'k+1 <= len f by A1,XREAL_1:6;
A6: len f-'k >= 1 by A2,A4,XREAL_1:6;
then right_cell(f,k) = left_cell(Rev f,len f-'k) by A1,A4,Th9;
hence thesis by A3,A5,A6,Th14;
end;
theorem Th16:
i <= len G & j <= width G implies Int cell(G,i,j) is convex
proof
assume that
A1: i <= len G and
A2: j <= width G;
set P = Int cell(G,i,j);
A3: P = Int v_strip(G,i) /\ Int h_strip(G,j) by TOPS_1:17;
A4: Int v_strip(G,i) is convex by A1,Th12;
Int h_strip(G,j) is convex by A2,Th11;
hence thesis by A3,A4,Th5;
end;
::$CT
theorem Th17:
1 <= k & k+1 <= len f implies Int left_cell(f,k) is convex
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f;
ex i,j st i <= len GoB f & j <=
width GoB f & cell(GoB f,i,j) = left_cell(f,k) by A1,A2,Th10;
hence thesis by Th16;
end;
theorem Th18:
1 <= k & k+1 <= len f implies Int right_cell(f,k) is convex
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f;
A3: len f = len Rev f by FINSEQ_5:def 3;
k <= len f by A2,NAT_1:13;
then
A4: len f-'k+k = len f by XREAL_1:235;
then
A5: len f-'k+1 <= len f by A1,XREAL_1:6;
A6: len f-'k >= 1 by A2,A4,XREAL_1:6;
then right_cell(f,k) = left_cell(Rev f,len f-'k) by A1,A4,Th9;
hence thesis by A3,A5,A6,Th17;
end;
definition
let f;
A1: 1+1 < len f by GOBOARD7:34,XXREAL_0:2;
then
A2: Int left_cell(f,1) <> {} by Th14;
A3: Int right_cell(f,1) <> {} by A1,Th15;
func LeftComp f -> Subset of TOP-REAL 2 means
:Def1:
it is_a_component_of (L~f)` & Int left_cell(f,1) c= it;
existence
proof
A4: Int left_cell(f,1) is convex by A1,Th17;
Int left_cell(f,1) misses L~f by A1,GOBOARD8:37;
then
A5: Int left_cell(f,1) c= (L~f)` by SUBSET_1:23;
then (L~f)` <> {} by A1,Th14,XBOOLE_1:3;
hence thesis by A2,A4,A5,Th3;
end;
uniqueness by A2,Th1,XBOOLE_1:67;
func RightComp f -> Subset of TOP-REAL 2 means
:Def2:
it is_a_component_of (L~f)` & Int right_cell(f,1) c= it;
existence
proof
A6: Int right_cell(f,1) is convex by A1,Th18;
Int right_cell(f,1) misses L~f by A1,GOBOARD8:38;
then
A7: Int right_cell(f,1) c= (L~f)` by SUBSET_1:23;
then (L~f)` <> {} by A1,Th15,XBOOLE_1:3;
hence thesis by A3,A6,A7,Th3;
end;
uniqueness by A3,Th1,XBOOLE_1:67;
end;
theorem Th19:
for k st 1 <= k & k+1 <= len f holds Int left_cell(f,k) c= LeftComp f
proof
defpred P[Nat] means
1 <= $1 & $1+1 <= len f implies Int left_cell(f,$1) c= LeftComp f;
A1: P[0];
A2: now
let k such that
A3: P[k];
thus P[k+1]
proof
assume that
A4: 1 <= k+1 and
A5: k+1+1 <= len f;
per cases by NAT_1:14;
suppose k = 0;
hence thesis by Def1;
end;
suppose
A6: k >= 1;
A7: k+1 <= len f by A5,NAT_1:13;
A8: k <= k+1 by NAT_1:11;
then k <= len f by A7,XXREAL_0:2;
then
A9: k in dom f by A6,FINSEQ_3:25;
then consider i0,j0 being Nat such that
A10: [i0,j0] in Indices GoB f and
A11: f/.k = (GoB f)*(i0,j0) by GOBOARD2:14;
A12: k+1 in dom f by A4,A7,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A13: [i1,j1] in Indices GoB f and
A14: f/.(k+1) = (GoB f)*(i1,j1) by GOBOARD2:14;
k+1+1 >= 1 by NAT_1:11;
then
A15: k+1+1 in dom f by A5,FINSEQ_3:25;
then consider i2,j2 being Nat such that
A16: [i2,j2] in Indices GoB f and
A17: f/.(k+1+1) = (GoB f)*(i2,j2) by GOBOARD2:14;
A18: 1 <= i0 by A10,MATRIX_0:32;
A19: i0 <= len GoB f by A10,MATRIX_0:32;
A20: 1 <= i1 by A13,MATRIX_0:32;
A21: i1 <= len GoB f by A13,MATRIX_0:32;
A22: 1 <= i2 by A16,MATRIX_0:32;
A23: i2 <= len GoB f by A16,MATRIX_0:32;
A24: 1 <= j0 by A10,MATRIX_0:32;
A25: j0 <= width GoB f by A10,MATRIX_0:32;
A26: 1 <= j1 by A13,MATRIX_0:32;
A27: j1 <= width GoB f by A13,MATRIX_0:32;
A28: 1 <= j2 by A16,MATRIX_0:32;
A29: j2 <= width GoB f by A16,MATRIX_0:32;
A30: i0 = i1 or j0 = j1 by A9,A10,A11,A12,A13,A14,GOBOARD2:11;
A31: i1 = i2 or j1 = j2 by A12,A13,A14,A15,A16,A17,GOBOARD2:11;
reconsider i19=i1, i09=i0, i29=i2, j19=j1, j09=j0, j29=j2
as Element of REAL by XREAL_0:def 1;
A32: f is_sequence_on GoB f by GOBOARD5:def 5;
then |.i0-i1.|+|.j0-j1.| = 1 by A9,A10,A11,A12,A13,A14;
then
A33: |.i09-i19.|=1 & j0 = j1 or |.j09-j19.|=1 & i0=i1 by SEQM_3:42;
then
A34: i0 = i1 or i0 = i1+1 or i0+1 = i1 by SEQM_3:41;
|.i1-i2.|+|.j1-j2.| = 1 by A12,A13,A14,A15,A16,A17,A32;
then
A35: |.i19-i29.|=1 & j1 = j2 or |.j19-j29.|=1 & i1=i2 by SEQM_3:42;
then
A36: i1 = i2 or i1 = i2+1 or i1+1 = i2 by SEQM_3:41;
A37: j0 = j1 or j0 = j1+1 or j0+1 = j1 by A33,SEQM_3:41;
A38: j1 = j2 or j1 = j2+1 or j1+1 = j2 by A35,SEQM_3:41;
A39: now
assume that
A40: i0 = i2 and
A41: j0 = j2;
A42: now
assume k <= 1;
then
A43: k = 1 by A6,XXREAL_0:1;
assume k+1+1 >= len f;
then k+1+1 = len f by A5,XXREAL_0:1;
hence contradiction by A43,GOBOARD7:34;
end;
A44: k < k+1+1 by A8,NAT_1:13;
per cases by A42;
suppose k > 1;
hence contradiction by A5,A11,A17,A40,A41,A44,GOBOARD7:37;
end;
suppose k+1+1 < len f;
hence contradiction by A6,A11,A17,A40,A41,A44,GOBOARD7:36;
end;
end;
i1 >= 1 by A13,MATRIX_0:32;
then
A45: i1 = i1 -' 1 + 1 by XREAL_1:235;
j1 >= 1 by A13,MATRIX_0:32;
then
A46: j1 = j1 -' 1 + 1 by XREAL_1:235;
then j1 -' 1 <= j1 by NAT_1:11;
then
A47: j1 -' 1 <= width GoB f by A27,XXREAL_0:2;
len GoB f > 1 by GOBOARD7:32;
then
A48: len GoB f -'1 + 1 = len GoB f by XREAL_1:235;
width GoB f >= 1 by GOBOARD7:33;
then
A49: width GoB f -'1 + 1 = width GoB f by XREAL_1:235;
A50: k+1+1 = k+(1+1);
A51: i0+1+1 = i0+(1+1);
A52: i2+1+1 = i2+(1+1);
A53: j0+1+1 = j0+(1+1);
A54: j2+1+1 = j2+(1+1);
A55: LeftComp f is_a_component_of (L~f)` by Def1;
A56: 0+1 = 1;
now per cases by A9,A11,A12,A14,A15,A17,A34,A36,A37,A38,A39,GOBOARD7:29;
suppose that
A57: i0 = i1+1 and
A58: i1 = i2+1 and
A59: j0 = 1;
A60: left_cell(f,k) = cell(GoB f,i1,0)
by A6,A7,A10,A11,A13,A14,A30,A56,A57,A59,GOBOARD5:29;
0+1 = j2 by A30,A31,A57,A58,A59;
then
A61: left_cell(f,k+1) = cell(GoB f,i2,0)
by A4,A5,A13,A14,A16,A17,A30,A57,A58,A59,GOBOARD5:29;
A62: LSeg(1/2*((GoB f)*(i1,1)+(GoB f)*(i0,1))- |[0,1]|,
1/2*((GoB f)*(i2,1)+(GoB f)*(i1,1))- |[0,1]|)
meets Int cell(GoB f,i1,0) by A19,A20,A57,GOBOARD6:84;
LSeg(1/2*((GoB f)*(i1,1)+(GoB f)*(i0,1))- |[0,1]|,
1/2*((GoB f)*(i2,1)+(GoB f)*(i1,1))- |[0,1]|) misses L~f
by A19,A22,A52,A57,A58,GOBOARD8:25;
then LSeg(1/2*((GoB f)*(i1,1)+(GoB f)*(i0,1))- |[0,1]|,
1/2*((GoB f)*(i2,1)+(GoB f)*(i1,1))- |[0,1]|) c= (L~f)`
by SUBSET_1:23;
then
A63: LSeg(1/2*((GoB f)*(i1,1)+(GoB f)*(i0,1))- |[0,1]|,
1/2*((GoB f)*(i2,1)+(GoB f)*(i1,1))- |[0,1]|) c= LeftComp f
by A3,A5,A6,A55,A60,A62,Th4,NAT_1:13;
A64: Int left_cell(f,k+1) is convex by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A61,A63,A21,A22,A58,Th4,A64,GOBOARD6:84;
end;
suppose that
A65: i0 = i1+1 and
A66: i1 = i2+1 and
A67: j0 <> 1;
A68: left_cell(f,k) = cell(GoB f,i1,j1-'1)
by A6,A7,A10,A11,A13,A14,A30,A46,A65,GOBOARD5:29;
1 < j0 by A24,A67,XXREAL_0:1;
then
A69: 1 <= j0-'1 by A30,A46,A65,NAT_1:13;
A70: left_cell(f,k+1) = cell(GoB f,i2,j1-'1)
by A4,A5,A13,A14,A16,A17,A31,A46,A66,GOBOARD5:29;
A71: LSeg(1/2*((GoB f)*(i1,j0-'1)+(GoB f)*(i0,j0)),
1/2*((GoB f)*(i2,j0-'1)+(GoB f)*(i1,j0)))
meets Int cell(GoB f,i1,j1-'1)
by A19,A20,A27,A30,A46,A65,A69,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i1,j0-'1)+(GoB f)*(i0,j0)),
1/2*((GoB f)*(i2,j0-'1)+(GoB f)*(i1,j0))) misses L~f
by A5,A6,A11,A14,A17,A19,A22,A25,A30,A31,A46,A50,A52,A65,A66,A69,
GOBOARD8:11;
then LSeg(1/2*((GoB f)*(i1,j0-'1)+(GoB f)*(i0,j0)),
1/2*((GoB f)*(i2,j0-'1)+(GoB f)*(i1,j0))) c= (L~f)` by SUBSET_1:23;
then
A72: LSeg(1/2*((GoB f)*(i1,j0-'1)+(GoB f)*(i0,j0)),
1/2*((GoB f)*(i2,j0-'1)+(GoB f)*(i1,j0))) c= LeftComp f
by A3,A5,A6,A55,A68,A71,Th4,NAT_1:13;
A73: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A30,A55,A65,A66,A70,A72,A21,A22,A25,A46,A69,Th4,A73
,GOBOARD6:82;
end;
suppose that
A74: i0 = i1+1 and
A75: j1 = j2+1;
left_cell(f,k) = cell(GoB f,i1,j2)
by A6,A7,A10,A11,A13,A14,A30,A74,A75,GOBOARD5:29
.= left_cell(f,k+1) by A4,A5,A13,A14,A16,A17,A31,A45,A75,GOBOARD5:30;
hence thesis by A3,A5,A6,NAT_1:13;
end;
suppose that
A76: j0 = j1+1 and
A77: i1 = i2+1 and
A78: i0 = len GoB f and
A79: j1 = 1;
A80: left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A45,A76,GOBOARD5:30;
A81: LSeg((GoB f)*(len GoB f,1)+|[1,-1]|,
1/2*((GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2))+|[1,0]|)
meets Int cell(GoB f,i0,j1) by A25,A76,A78,A79,GOBOARD6:86;
LSeg((GoB f)*(len GoB f,1)+|[1,-1]|,
1/2*((GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2))+|[1,0]|)
misses L~f by GOBOARD8:35;
then LSeg((GoB f)*(len GoB f,1)+|[1,-1]|,
1/2*((GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2))+|[1,0]|)
c= (L~f)` by SUBSET_1:23;
then
A82: LSeg((GoB f)*(len GoB f,1)+|[1,-1]|,
1/2*((GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2))+|[1,0]|)
c= LeftComp f by A3,A5,A6,A55,A80,A81,Th4,NAT_1:13;
A83: Int cell(GoB f,i1,0) is convex by A21,A26,A27,Th16;
Int cell(GoB f,i1,0) misses L~f by A21,A26,A27,GOBOARD7:12;
then Int cell(GoB f,i1,0) c= (L~f)` by SUBSET_1:23;
then
A84: Int cell(GoB f,i1,0) c= LeftComp f
by A55,A82,A30,A76,A78,Th4,A83,GOBOARD6:90;
A85: left_cell(f,k+1) = cell(GoB f,i2,0)
by A4,A5,A13,A14,A16,A17,A31,A46,A77,A79,GOBOARD5:29;
A86: LSeg
(1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))- |[0,1]|,
(GoB f)*(len GoB f,1)+|[1,-1]|)
meets Int cell(GoB f,i1,0) by A30,A76,A78,GOBOARD6:90;
LSeg(1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))- |[0,1]|,
(GoB f)*(len GoB f,1)+|[1,-1]|) misses L~f by GOBOARD8:27;
then LSeg(1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*
(len GoB f,1))- |[0,1]|,
(GoB f)*(len GoB f,1)+|[1,-1]|) c= (L~f)` by SUBSET_1:23;
then
A87: LSeg(1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*
(len GoB f,1))- |[0,1]|,
(GoB f)*(len GoB f,1)+|[1,-1]|) c= LeftComp f
by A55,A84,A86,Th4;
A88: Int left_cell(f,k+1) is convex by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A85,A87,A22,A30,A45,A76,A77,A78,Th4,A88,
GOBOARD6:84;
end;
suppose that
A89: j0 = j1+1 and
A90: i1 = i2+1 and
A91: i0 <> len GoB f and
A92: j1 = 1;
A93: left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A45,A89,GOBOARD5:30;
len GoB f > i0 by A19,A91,XXREAL_0:1;
then
A94: len GoB f >= i0+1 by NAT_1:13;
A95: LSeg(1/2*((GoB f)*(i0,1)+(GoB f)*(i0+1,1))- |[0,1]|,
1/2*((GoB f)*(i1,1)+(GoB f)*(i1+1,1+1)))
meets Int cell(GoB f,i0,j1)
by A20,A25,A30,A89,A92,A94,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i0,1)+(GoB f)*(i0+1,1))- |[0,1]|,
1/2*((GoB f)*(i1,1)+(GoB f)*(i1+1,2))) misses L~f
by A5,A6,A11,A14,A17,A22,A30,A31,A50,A52,A89,A90,A92,A94,GOBOARD8:8;
then LSeg(1/2*((GoB f)*(i0,1)+(GoB f)*(i0+1,1))- |[0,1]|,
1/2*((GoB f)*(i1,1)+(GoB f)*(i1+1,2))) c= (L~f)` by SUBSET_1:23;
then
A96: LSeg(1/2*((GoB f)*(i0,1)+(GoB f)*(i0+1,1))- |[0,1 ]|,
1/2*((GoB f)*(i1,1)+(GoB f)*(i1+1,2))) c= LeftComp f
by A3,A5,A6,A55,A93,A95,Th4,NAT_1:13;
A97: Int cell(GoB f,i1,0) is convex
by A21,A26,A27,Th16;
Int cell(GoB f,i1,0) misses L~f by A21,A26,A27,GOBOARD7:12;
then Int cell(GoB f,i1,0) c= (L~f)` by SUBSET_1:23;
then
A98: Int cell(GoB f,i1,0) c= LeftComp f by A55,A96,A20,A30,A89,A94,Th4
,A97,GOBOARD6:84;
A99: left_cell(f,k+1) = cell(GoB f,i2,0)
by A4,A5,A13,A14,A16,A17,A31,A46,A90,A92,GOBOARD5:29;
A100: LSeg(1/2*((GoB f)*(i2,1)+(GoB f)*(i2+1,1))- |[0,1]|,
1/2*((GoB f)*(i2+1,1)+(GoB f)*(i2+2,1))- |[0,1]|)
meets Int cell(GoB f,i1,0) by A20,A30,A89,A90,A94,GOBOARD6:84;
LSeg(1/2*((GoB f)*(i2,1)+(GoB f)*(i2+1,1))- |[0,1]|,
1/2*((GoB f)*(i2+1,1)+(GoB f)*(i2+2,1))- |[0,1]|) misses L~f
by A22,A30,A89,A90,A94,GOBOARD8:25;
then LSeg(1/2*((GoB f)*(i2,1)+(GoB f)*(i2+1,1))- |[0,1]|,
1/2*((GoB f)*(i2+1,1)+(GoB f)*(i2+2,1))- |[0,1]|) c= (L~f)`
by SUBSET_1:23;
then
A101: LSeg(1/2*((GoB f)*(i2,1)+(GoB f)*(i2+1,1))- |[0,1 ]|,
1/2*((GoB f)*(i2+1,1)+(GoB f)*(i2+2,1))- |[0,1]|) c= LeftComp f
by A55,A98,A100,Th4;
A102: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A99,A101,A21,A22,A90,Th4,A102,GOBOARD6:84;
end;
suppose that
A103: j0 = j1+1 and
A104: i1 = i2+1 and
A105: i0 = len GoB f and
A106: j1 <> 1;
A107: left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A45,A103,GOBOARD5:30;
1 < j1 by A26,A106,XXREAL_0:1;
then
A108: 1 <= j1-'1 by A46,NAT_1:13;
A109: j1+1 = j1-'1+(1+1) by A46;
A110: LSeg
(1/2*((GoB f)*(len GoB f,j1-'1)+(GoB f)*(len GoB f,j1))+|[1,0]|,
1/2*((GoB f)*(len GoB f,j1)+(GoB f)*(len GoB f,j1+1))+|[1,0]|)
meets Int cell(GoB f,i0,j1) by A25,A26,A103,A105,GOBOARD6:86;
LSeg(1/2*((GoB f)*(len GoB f,j1-'1)+(GoB f)*(len GoB f,j1))+|[1,0]|,
1/2*((GoB f)*(len GoB f,j1)+(GoB f)*(len GoB f,j1+1))+|[1,0]|)
misses L~f by A25,A46,A103,A108,A109,GOBOARD8:34;
then LSeg(1/2*((GoB f)*(len GoB f,j1-'1)+(GoB f)*
(len GoB f,j1))+|[1,0]|,
1/2*((GoB f)*(len GoB f,j1)+(GoB f)*(len GoB f,j1+1))+|[1,0]|)
c= (L~f)` by SUBSET_1:23;
then
A111: LSeg
(1/2*((GoB f)*(len GoB f,j1-'1)+(GoB f)*(len GoB f,j1))+|[1
,0]|,
1/2*((GoB f)*(len GoB f,j1)+(GoB f)*(len GoB f,j1+1))+|[1,0]|)
c= LeftComp f by A3,A5,A6,A55,A107,A110,Th4,NAT_1:13;
j1 > 1 by A26,A106,XXREAL_0:1;
then
A112: 1 <= j1-'1 by A46,NAT_1:13;
A113: Int cell(GoB f,i1,j1-'1) is convex by A21,A47,Th16;
Int cell(GoB f,i1,j1-'1) misses L~f by A21,A47,GOBOARD7:12;
then Int cell(GoB f,i1,j1-'1) c= (L~f)` by SUBSET_1:23;
then
A114: Int cell(GoB f,i1,j1-'1) c= LeftComp f by A55,A111,A27,A30,A46,A103
,A105,Th4,A113,A112,GOBOARD6:86;
A115: left_cell(f,k+1) = cell(GoB f,i2,j1-'1)
by A4,A5,A13,A14,A16,A17,A31,A46,A104,GOBOARD5:29;
A116: LSeg(1/2*((GoB f)*(i1 -' 1,j1-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1,j1-'1)+(GoB f)*(i1,j1))+|[1,0]|)
meets Int cell(GoB f,i1,j1-'1) by A27,A30,A46,A103,A105,A108,
GOBOARD6:86;
A117: i1-'1 = i2 by A104,NAT_D:34;
then LSeg(1/2*((GoB f)*(i1 -' 1,j1-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1,j1-'1)+(GoB f)*(i1,j1))+|[1,0]|) misses L~f
by A5,A6,A11,A14,A17,A25,A30,A31,A46,A50,A103,A104,A105,A108,A109,
GOBOARD8:19;
then LSeg(1/2*((GoB f)*(i1 -' 1,j1-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1,j1-'1)+(GoB f)*(i1,j1))+|[1,0]|) c= (L~f)`
by SUBSET_1:23;
then
A118: LSeg(1/2*((GoB f)*(i1 -' 1,j1-'1)+(GoB f)*(i1,j1)) ,
1/2*((GoB f)*(i1,j1-'1)+(GoB f)*(i1,j1))+|[1,0]|) c= LeftComp f
by A55,A114,A116,Th4;
A119: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A115,A118,A21,A22,A27,A46,A104,A108,A117,Th4
,A119,GOBOARD6:82;
end;
suppose that
A120: j0 = j1+1 and
A121: i1 = i2+1 and
A122: i0 <> len GoB f and
A123: j1 <> 1;
A124: left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A45,A120,GOBOARD5:30;
1 < j1 by A26,A123,XXREAL_0:1;
then
A125: 1 <= j1-'1 by A46,NAT_1:13;
len GoB f > i0 by A19,A122,XXREAL_0:1;
then
A126: len GoB f >= i0+1 by NAT_1:13;
A127: j1+1 = j1-'1+(1+1) by A46;
A128: LSeg(1/2*((GoB f)*(i0,j1-'1)+(GoB f)*(i0+1,j1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1+1,j1+1)))
meets Int cell(GoB f,i0,j1) by A20,A25,A26,A30,A120,A126,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i0,j1-'1)+(GoB f)*(i0+1,j1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1+1,j1+1))) misses L~f
by A5,A6,A11,A14,A17,A22,A25,A30,A31,A46,A50,A52,A120,A121,A125,A126,A127,
GOBOARD8:5;
then LSeg(1/2*((GoB f)*(i0,j1-'1)+(GoB f)*(i0+1,j1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1+1,j1+1))) c= (L~f)` by SUBSET_1:23;
then
A129: LSeg(1/2*((GoB f)*(i0,j1-'1)+(GoB f)*(i0+1,j1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1+1,j1+1))) c= LeftComp f
by A3,A5,A6,A55,A124,A128,Th4,NAT_1:13;
j1 > 1 by A26,A123,XXREAL_0:1;
then
A130: 1 <= j1-'1 by A46,NAT_1:13;
A131: Int cell(GoB f,i1,j1-'1) is convex by A21,A47,Th16;
Int cell(GoB f,i1,j1-'1) misses L~f by A21,A47,GOBOARD7:12;
then Int cell(GoB f,i1,j1-'1) c= (L~f)` by SUBSET_1:23;
then
A132: Int cell(GoB f,i1,j1-'1) c= LeftComp f by A30,A55,A120,A129,A20,A27
,A46,A126,Th4,A131,A130,GOBOARD6:82;
A133: left_cell(f,k+1) = cell(GoB f,i2,j1-'1)
by A4,A5,A13,A14,A16,A17,A31,A46,A121,GOBOARD5:29;
A134: LSeg(1/2*((GoB f)*(i1,j1-'1)+(GoB f)*(i1+1,j1)),
1/2*((GoB f)*(i2,j1-'1)+(GoB f)*(i1,j1)))
meets Int cell(GoB f,i1,j1-'1) by A20,A27,A30,A46,A120,A125,A126,
GOBOARD6:82;
i1 < len GoB f by A21,A30,A120,A122,XXREAL_0:1;
then i1+1 <= len GoB f by NAT_1:13;
then LSeg(1/2*((GoB f)*(i1,j1-'1)+(GoB f)*(i1+1,j1)),
1/2*((GoB f)*(i2,j1-'1)+(GoB f)*(i1,j1))) misses L~f
by A5,A6,A11,A14,A17,A22,A25,A30,A31,A46,A50,A52,A120,A121,A125,A127,
GOBOARD8:13;
then LSeg(1/2*((GoB f)*(i1,j1-'1)+(GoB f)*(i1+1,j1)),
1/2*((GoB f)*(i2,j1-'1)+(GoB f)*(i1,j1))) c= (L~f)` by SUBSET_1:23;
then
A135: LSeg(1/2*((GoB f)*(i1,j1-'1)+(GoB f)*(i1+1,j1)),
1/2*((GoB f)*(i2,j1-'1)+(GoB f)*(i1,j1))) c= LeftComp f
by A55,A132,A134,Th4;
A136: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A121,A133,A135,A21,A22,A27,A46,A125,Th4,A136,
GOBOARD6:82;
end;
suppose that
A137: j0 = j1+1 and
A138: j1 = j2+1 and
A139: i0 = len GoB f;
A140: left_cell(f,k) = cell(GoB f,len GoB f,j1)
by A6,A7,A10,A11,A13,A14,A30,A48,A137,A139,GOBOARD5:30;
A141: left_cell(f,k+1) = cell(GoB f,len GoB f,j2)
by A4,A5,A13,A14,A16,A17,A30,A31,A48,A137,A138,A139,GOBOARD5:30;
A142: LSeg(1/2*((GoB f)*(len GoB f,j2)+(GoB f)*(len GoB f,j2+1))+|[1,0]|,
1/2*((GoB f)*(len GoB f,j2+1)+(GoB f)*(len GoB f,j2+2))+|[1,0]|)
meets Int cell(GoB f,len GoB f,j1)
by A25,A26,A137,A138,GOBOARD6:86;
LSeg(1/2*((GoB f)*(len GoB f,j2)+(GoB f)*(len GoB f,j2+1))+|[1,0]|
, 1/2*((GoB f)*(len GoB f,j2+1)+(GoB f)*(len GoB f,j2+2))+|[1,0]|)
misses L~f by A25,A28,A137,A138,GOBOARD8:34;
then LSeg(1/2*((GoB f)*(len GoB f,j2)+(GoB f)*(len GoB f,j2+1))+|[1,0]|,
1/2*((GoB f)*(len GoB f,j2+1)+(GoB f)* (len GoB f,j2+2))+|[1,0]|)
c= (L~f)` by SUBSET_1:23;
then
A143: LSeg
(1/2*((GoB f)*(len GoB f,j2)+(GoB f)*(len GoB f,j2+1))+|[1,
0]|,
1/2*((GoB f)*(len GoB f,j2+1)+(GoB f)*(len GoB f,j2+2))+|[1,0]|)
c= LeftComp f by A3,A5,A6,A55,A140,A142,Th4,NAT_1:13;
A144: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A141,A143,A27,A28,A138,Th4,A144,GOBOARD6:86;
end;
suppose that
A145: j0 = j1+1 and
A146: j1 = j2+1 and
A147: i0 <> len GoB f;
A148: left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A45,A145,GOBOARD5:30;
len GoB f > i0 by A19,A147,XXREAL_0:1;
then
A149: len GoB f >= i0+1 by NAT_1:13;
A150: left_cell(f,k+1) = cell(GoB f,i1,j2)
by A4,A5,A13,A14,A16,A17,A31,A45,A146,GOBOARD5:30;
A151: LSeg(1/2*((GoB f)*(i0,j2)+(GoB f)*(i0+1,j2+1)),
1/2*((GoB f)*(i1,j2+1)+(GoB f)*(i1+1,j2+2)))
meets Int cell(GoB f,i0,j1)
by A20,A25,A26,A30,A145,A146,A149,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i0,j2)+(GoB f)*(i0+1,j2+1)),
1/2*((GoB f)*(i1,j2+1)+(GoB f)*(i1+1,j2+2))) misses L~f
by A5,A6,A11,A14,A17,A18,A25,A28,A30,A31,A50,A145,A146,A149,GOBOARD8:4;
then LSeg(1/2*((GoB f)*(i0,j2)+(GoB f)*(i0+1,j2+1)),
1/2*((GoB f)*(i1,j2+1)+(GoB f)*
(i1+1,j2+2))) c= (L~f)` by SUBSET_1:23;
then
A152: LSeg(1/2*((GoB f)*(i0,j2)+(GoB f)*(i0+1,j2+1)),
1/2*((GoB f)*(i1,j2+1)+(GoB f)*(i1+1,j2+2))) c= LeftComp f
by A3,A5,A6,A55,A148,A151,Th4,NAT_1:13;
A153: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A150,A152,A20,A27,A28,A30,A145,A146,A149,Th4
,A153,GOBOARD6:82;
end;
suppose that
A154: i0+1 = i1 and
A155: j1 = j2+1 and
A156: i1 = len GoB f and
A157: j0 = width GoB f;
A158: left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A46,A154,GOBOARD5:28;
A159: LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i1,j0))+|[0,1]|,
(GoB f)*(i1,j0)+|[1,1]|)
meets Int cell(GoB f,i0,j1) by A18,A21,A30,A154,A157,GOBOARD6:83;
LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i1,j0))+|[0,1]|,
(GoB f)*(i1,j0)+|[1,1]|)
misses L~f by A48,A154,A156,A157,GOBOARD8:30;
then LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i1,j0))+|[0,1]|,
(GoB f)*(i1,j0)+|[1,1]|) c= (L~f)` by SUBSET_1:23;
then
A160: LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i1,j0))+|[0,1]| ,
(GoB f)*(i1,j0)+|[1,1]|) c= LeftComp f by A3,A5,A6,A55,A158,A159,Th4,NAT_1:13;
A161: Int cell(GoB f,i1,j1) is convex by A21,A27,Th16;
Int cell(GoB f,i1,j1) misses L~f by A21,A27,GOBOARD7:12;
then Int cell(GoB f,i1,j1) c= (L~f)` by SUBSET_1:23;
then
A162: Int cell(GoB f,i1,j1) c= LeftComp f by A55,A160,A30,A154,A156,A157
,Th4,A161,GOBOARD6:88;
A163: left_cell(f,k+1) = cell(GoB f,i1,j2)
by A4,A5,A13,A14,A16,A17,A31,A45,A155,GOBOARD5:30;
A164: LSeg(1/2*((GoB f)*(i1,j2)+(GoB f)*(i1,j1))+|[1,0]|,
(GoB f)*(i1,j1)+|[1,1]|) meets Int cell(GoB f,i1,j1)
by A30,A154,A156,A157,GOBOARD6:88;
LSeg(1/2*((GoB f)*(i1,j2)+(GoB f)*(i1,j1))+|[1,0]|, (GoB f)*
(i1,j1)+|[1,1]|) misses L~f by A30,A49,A154,A155,A156,A157,GOBOARD8:36;
then LSeg(1/2*((GoB f)*(i1,j2)+(GoB f)*(i1,j1))+|[1,0]|,
(GoB f)*(i1,j1)+|[1,1]|) c= (L~f)` by SUBSET_1:23;
then
A165: LSeg(1/2*((GoB f)*(i1,j2)+(GoB f)*(i1,j1))+|[1,0]| ,
(GoB f)*(i1,j1)+|[1,1]|) c= LeftComp f by A55,A162,A164,Th4;
A166: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A163,A165,A27,A28,A155,A156,Th4,A166,
GOBOARD6:86;
end;
suppose that
A167: i0+1 = i1 and
A168: j1 = j2+1 and
A169: i1 <> len GoB f and
A170: j0 = width GoB f;
A171: left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A46,A167,GOBOARD5:28;
len GoB f > i1 by A21,A169,XXREAL_0:1;
then
A172: i1+1 <= len GoB f by NAT_1:13;
A173: LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0+1,j0))+|[0,1]|,
1/2*((GoB f)*(i0+1,j0)+(GoB f)*(i0+2,j0))+|[0,1]|)
meets Int cell(GoB f,i0,j1) by A18,A21,A30,A167,A170,GOBOARD6:83;
LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0+1,j0))+|[0,1]|,
1/2*((GoB f)*(i0+1,j0)+(GoB f)*(i0+2,j0))+|[0,1]|)
misses L~f by A18,A167,A170,A172,GOBOARD8:28;
then LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0+1,j0))+|[0,1]|,
1/2*((GoB f)*(i0+1,j0)+(GoB f)*(i0+2,j0))+|[0,1]|)
c= (L~f)` by SUBSET_1:23;
then
A174: LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0+1,j0))+|[0,1 ]|,
1/2*((GoB f)*(i0+1,j0)+(GoB f)*(i0+2,j0))+|[0,1]|) c= LeftComp f
by A3,A5,A6,A55,A171,A173,Th4,NAT_1:13;
A175: Int cell(GoB f,i1,j1) is convex by A21,A27,Th16;
Int cell(GoB f,i1,j1) misses L~f by A21,A27,GOBOARD7:12;
then Int cell(GoB f,i1,j1) c= (L~f)` by SUBSET_1:23;
then
A176: Int cell(GoB f,i1,j1) c= LeftComp f by A55,A174,A20,A30,A167,A170
,A172,Th4,A175,GOBOARD6:83;
A177: left_cell(f,k+1) = cell(GoB f,i1,j2)
by A4,A5,A13,A14,A16,A17,A31,A45,A168,GOBOARD5:30;
A178: LSeg(1/2*((GoB f)*(i0+1,j2)+(GoB f)*(i1+1,j0)),
1/2*((GoB f)*(i0+1,j0)+(GoB f)*(i1+1,j0))+|[0,1]|)
meets Int cell(GoB f,i1,j1) by A20,A30,A167,A170,A172,GOBOARD6:83;
LSeg(1/2*((GoB f)*(i0+1,j2)+(GoB f)*(i1+1,j0)),
1/2*((GoB f)*(i0+1,j0)+(GoB f)*(i1+1,j0))+|[0,1]|) misses L~f
by A5,A6,A11,A14,A17,A18,A30,A31,A49,A50,A51,A167,A168,A170,A172,
GOBOARD8:10;
then LSeg(1/2*((GoB f)*(i0+1,j2)+(GoB f)*(i1+1,j0)),
1/2*((GoB f)*(i0+1,j0)+(GoB f)*(i1+1,j0))+|[0,1]|) c= (L~f)`
by SUBSET_1:23;
then
A179: LSeg(1/2*((GoB f)*(i0+1,j2)+(GoB f)*(i1+1,j0)),
1/2*((GoB f)*(i0+1,j0)+(GoB f)*(i1+1,j0))+|[0,1]|) c= LeftComp f
by A55,A176,A178,Th4;
A180: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A177,A179,A20,A28,A30,A167,A168,A170,A172,Th4
,A180,GOBOARD6:82;
end;
suppose that
A181: i0+1 = i1 and
A182: j1 = j2+1 and
A183: i1 = len GoB f and
A184: j0 <> width GoB f;
A185: left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A46,A181,GOBOARD5:28;
width GoB f > j0 by A25,A184,XXREAL_0:1;
then
A186: width GoB f >= j0+1 by NAT_1:13;
A187: LSeg(1/2*((GoB f)*(i0,j1)+(GoB f)*(i1,j1+1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1,j1+1))+|[1,0]|)
meets Int cell(GoB f,i0,j1) by A18,A21,A26,A30,A181,A186,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i0,j1)+(GoB f)*(i1,j1+1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1,j1+1))+|[1,0]|) misses L~f
by A5,A6,A11,A14,A17,A28,A30,A31,A48,A50,A54,A181,A182,A183,A186,
GOBOARD8:20;
then LSeg(1/2*((GoB f)*(i0,j1)+(GoB f)*(i1,j1+1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1,j1+1))+|[1,0]|)
c= (L~f)` by SUBSET_1:23;
then
A188: LSeg(1/2*((GoB f)*(i0,j1)+(GoB f)*(i1,j1+1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1,j1+1))+|[1,0]|) c= LeftComp f
by A3,A5,A6,A55,A185,A187,Th4,NAT_1:13;
A189: Int cell(GoB f,i1,j1) is convex by A21,A27,Th16;
Int cell(GoB f,i1,j1) misses L~f by A21,A27,GOBOARD7:12;
then Int cell(GoB f,i1,j1) c= (L~f)` by SUBSET_1:23;
then
A190: Int cell(GoB f,i1,j1) c= LeftComp f by A55,A188,A26,A30,A181,A183
,A186,Th4,A189,GOBOARD6:86;
A191: left_cell(f,k+1) = cell(GoB f,i1,j2)
by A4,A5,A13,A14,A16,A17,A31,A45,A182,GOBOARD5:30;
A192: LSeg(1/2*((GoB f)*(len GoB f,j2)+(GoB f)*(len GoB f,j1))+|[1,0]|,
1/2*((GoB f)*(len GoB f,j1)+(GoB f)*(len GoB f,j1+1))+|[1,0]|)
meets Int cell(GoB f,i1,j1) by A26,A30,A181,A183,A186,GOBOARD6:86;
LSeg(1/2*((GoB f)*(len GoB f,j2)+(GoB f)*(len GoB f,j1))+|[1,0]|,
1/2*((GoB f)*(len GoB f,j1)+(GoB f)*(len GoB f,j1+1))+|[1,0]|)
misses L~f by A28,A30,A54,A181,A182,A186,GOBOARD8:34;
then LSeg(1/2*((GoB f)*(len GoB f,j2)+(GoB f)*(len GoB f,j1))+|[1,0]|,
1/2*((GoB f)*(len GoB f,j1)+(GoB f)*(len GoB f,j1+1))+|[1,0]|)
c= (L~f)` by SUBSET_1:23;
then
A193: LSeg
(1/2*((GoB f)*(len GoB f,j2)+(GoB f)*(len GoB f,j1))+|[1,0 ]|,
1/2*((GoB f)*(len GoB f,j1)+(GoB f)*(len GoB f,j1+1))+|[1,0]|)
c= LeftComp f by A55,A190,A192,Th4;
A194: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A191,A193,A27,A28,A182,A183,Th4,A194,
GOBOARD6:86;
end;
suppose that
A195: i0+1 = i1 and
A196: j1 = j2+1 and
A197: i1 <> len GoB f and
A198: j0 <> width GoB f;
A199: left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A46,A195,GOBOARD5:28;
len GoB f > i1 by A21,A197,XXREAL_0:1;
then
A200: i1+1 <= len GoB f by NAT_1:13;
width GoB f > j0 by A25,A198,XXREAL_0:1;
then
A201: width GoB f >= j0+1 by NAT_1:13;
A202: LSeg(1/2*((GoB f)*(i0,j2+1)+(GoB f)*(i0+1,j1+1)),
1/2*((GoB f)*(i0+1,j2+1)+(GoB f)*(i1+1,j1+1)))
meets Int cell(GoB f,i0,j1) by A18,A21,A26,A30,A195,A196,A201,
GOBOARD6:82;
LSeg(1/2*((GoB f)*(i0,j2+1)+(GoB f)*(i0+1,j1+1)),
1/2*((GoB f)*(i0+1,j2+1)+(GoB f)*(i1+1,j1+1))) misses L~f
by A5,A6,A11,A14,A17,A18,A28,A30,A31,A50,A51,A54,A195,A196,A200,A201,
GOBOARD8:16;
then LSeg(1/2*((GoB f)*(i0,j2+1)+(GoB f)*(i0+1,j1+1)),
1/2*((GoB f)*(i0+1,j2+1)+(GoB f)*(i1+1,j1+1)))
c= (L~f)` by SUBSET_1:23;
then
A203: LSeg(1/2*((GoB f)*(i0,j2+1)+(GoB f)*(i0+1,j1+1)),
1/2*((GoB f)*(i0+1,j2+1)+(GoB f)*(i1+1,j1+1))) c= LeftComp f
by A3,A5,A6,A55,A199,A202,Th4,NAT_1:13;
A204: Int cell(GoB f,i1,j1) is convex by A21,A27,Th16;
Int cell(GoB f,i1,j1) misses L~f by A21,A27,GOBOARD7:12;
then Int cell(GoB f,i1,j1) c= (L~f)` by SUBSET_1:23;
then
A205: Int cell(GoB f,i1,j1) c= LeftComp f by A55,A203,A20,A26,A30,A195
,A196,A200,A201,Th4,A204,GOBOARD6:82;
A206: left_cell(f,k+1) = cell(GoB f,i1,j2)
by A4,A5,A13,A14,A16,A17,A31,A45,A196,GOBOARD5:30;
A207: LSeg(1/2*((GoB f)*(i0+1,j2)+(GoB f)*(i1+1,j2+1)),
1/2*((GoB f)*(i0+1,j2+1)+(GoB f)*(i1+1,j1+1)))
meets Int cell(GoB f,i1,j1)
by A20,A26,A30,A195,A196,A200,A201,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i0+1,j2)+(GoB f)*(i1+1,j2+1)),
1/2*((GoB f)*(i0+1,j2+1)+(GoB f)*(i1+1,j1+1))) misses L~f
by A5,A6,A11,A14,A17,A18,A28,A30,A31,A50,A51,A54,A195,A196,A200,A201,GOBOARD8:6
;
then LSeg(1/2*((GoB f)*(i0+1,j2)+(GoB f)*(i1+1,j2+1)),
1/2*((GoB f)*(i0+1,j2+1)+(GoB f)*(i1+1,j1+1))) c= (L~f)`
by SUBSET_1:23;
then
A208: LSeg(1/2*((GoB f)*(i0+1,j2)+(GoB f)*(i1+1,j2+1)),
1/2*((GoB f)*(i0+1,j2+1)+(GoB f)*(i1+1,j1+1))) c= LeftComp f
by A55,A205,A207,Th4;
A209: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A206,A208,A20,A27,A28,A195,A196,A200,Th4,A209,
GOBOARD6:82;
end;
suppose that
A210: j0+1 = j1 and
A211: i1 = i2+1;
left_cell(f,k) = cell(GoB f,i2,j0)
by A6,A7,A10,A11,A13,A14,A30,A210,A211,GOBOARD5:27
.= left_cell(f,k+1) by A4,A5,A13,A14,A16,A17,A31,A210,A211,GOBOARD5:29;
hence thesis by A3,A5,A6,NAT_1:13;
end;
suppose that
A212: i0 = i1+1 and
A213: j1+1 = j2 and
A214: i1 = 1 and
A215: j1 = 1;
A216: left_cell(f,k) = cell(GoB f,i1,j1-'1)
by A6,A7,A10,A11,A13,A14,A30,A46,A212,GOBOARD5:29;
i1-'1 <= i1 by NAT_D:35;
then
A217: i1-'1 <= len GoB f by A21,XXREAL_0:2;
A218: j1-'1 = 0 by A215,XREAL_1:232;
A219: i1-'1 = 0 by A214,XREAL_1:232;
j1-'1 <= j1 by NAT_D:35;
then
A220: j1-'1 <= width GoB f by A27,XXREAL_0:2;
A221: LSeg((GoB f)*(i1,j1)- |[1,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i0,j1))- |[0,1]|)
meets Int cell(GoB f,i1,j1-'1) by A19,A20,A212,A215,A218,GOBOARD6:84;
LSeg((GoB f)*(i1,j1)- |[1,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i0,j1))- |[0,1]|)
misses L~f by A212,A214,A215,GOBOARD8:26;
then LSeg((GoB f)*(i1,j1)- |[1,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i0,j1))- |[0,1]|) c= (L~f)`
by SUBSET_1:23;
then
A222: LSeg((GoB f)*(i1,j1)- |[1,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i0,j1))- |[0,1]|) c= LeftComp f
by A3,A5,A6,A55,A216,A221,Th4,NAT_1:13;
A223: Int cell(GoB f,i1-'1,j1-'1) is convex
by A217,A220,Th16;
Int cell(GoB f,i1-'1,j1-'1) misses L~f by A217,A220,GOBOARD7:12;
then Int cell(GoB f,i1-'1,j1-'1) c= (L~f)` by SUBSET_1:23;
then
A224: Int cell(GoB f,i1-'1,j1-'1) c= LeftComp f
by A55,A222,A214,A215,A218,Th4,A223,GOBOARD6:87;
A225: left_cell(f,k+1) = cell(GoB f,i1-'1,j1)
by A4,A5,A13,A14,A16,A17,A31,A45,A213,GOBOARD5:27;
A226: LSeg((GoB f)*(i1,j1)- |[1,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1,j2))- |[1,0]|)
meets Int cell(GoB f,i1-'1,j1-'1) by A214,A215,A218,GOBOARD6:87;
LSeg((GoB f)*(i1,j1)- |[1,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1,j2))- |[1,0]|)
misses L~f by A213,A214,A215,GOBOARD8:32;
then LSeg((GoB f)*(i1,j1)- |[1,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1,j2))- |[1,0]|) c= (L~f)`
by SUBSET_1:23;
then
A227: LSeg((GoB f)*(i1,j1)- |[1,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i1,j2))- |[1,0]|) c= LeftComp f
by A55,A224,A226,Th4;
A228: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A225,A227,A26,A29,A213,A214,A219,Th4,A228,
GOBOARD6:85;
end;
suppose that
A229: i0 = i1+1 and
A230: j1+1 = j2 and
A231: i1 <> 1 and
A232: j1 = 1;
A233: left_cell(f,k) = cell(GoB f,i1,j1-'1)
by A6,A7,A10,A11,A13,A14,A30,A46,A229,GOBOARD5:29;
1 < i1 by A20,A231,XXREAL_0:1;
then
A234: 1 <= i1-'1 by A45,NAT_1:13;
A235: i1-'1+(1+1) = i0 by A45,A229;
i1-'1 <= i1 by NAT_D:35;
then
A236: i1-'1 <= len GoB f by A21,XXREAL_0:2;
A237: j1-'1 = 0 by A232,XREAL_1:232;
j1-'1 <= j1 by NAT_D:35;
then
A238: j1-'1 <= width GoB f by A27,XXREAL_0:2;
A239: LSeg(1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,1))- |[0,1]|,
1/2*((GoB f)*(i1,1)+(GoB f)*(i0,1))- |[0,1]|)
meets Int cell(GoB f,i1,j1-'1) by A19,A20,A229,A237,GOBOARD6:84;
LSeg(1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,1))- |[0,1]|,
1/2*((GoB f)*(i1,1)+(GoB f)*(i0,1))- |[0,1]|) misses L~f
by A19,A45,A234,A235,GOBOARD8:25;
then LSeg(1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,1))- |[0,1]|,
1/2*((GoB f)*(i1,1)+(GoB f)*
(i0,1))- |[0,1]|) c= (L~f)` by SUBSET_1:23;
then
A240: LSeg(1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,1))- |[0,1 ]|,
1/2*((GoB f)*(i1,1)+(GoB f)*(i0,1))- |[0,1]|) c= LeftComp f
by A3,A5,A6,A55,A233,A239,Th4,NAT_1:13;
A241: Int cell(GoB f,i1-'1,j1-'1) is convex
by A236,A238,Th16;
Int cell(GoB f,i1-'1,j1-'1) misses L~f by A236,A238,GOBOARD7:12;
then Int cell(GoB f,i1-'1,j1-'1) c= (L~f)` by SUBSET_1:23;
then
A242: Int cell(GoB f,i1-'1,j1-'1) c= LeftComp f
by A55,A240,A21,A45,A234,A237,Th4,A241,GOBOARD6:84;
A243: left_cell(f,k+1) = cell(GoB f,i1-'1,j1)
by A4,A5,A13,A14,A16,A17,A31,A45,A230,GOBOARD5:27;
A244: LSeg(1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,1))- |[0,1]|,
1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,2)))
meets Int cell(GoB f,i1-'1,j1-'1) by A21,A45,A234,A237,GOBOARD6:84;
LSeg(1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,1))- |[0,1]|,
1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,2))) misses L~f
by A5,A6,A11,A14,A17,A19,A30,A31,A45,A50,A230,A232,A234,A235,
GOBOARD8:7;
then LSeg(1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,1))- |[0,1]|,
1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,2))) c= (L~f)` by SUBSET_1:23;
then
A245: LSeg(1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,1))- |[0,1 ]|,
1/2*((GoB f)*(i1-'1,1)+(GoB f)*(i1,2))) c= LeftComp f
by A55,A242,A244,Th4;
A246: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A243,A245,A21,A29,A45,A230,A232,A234,Th4,A246,
GOBOARD6:82;
end;
suppose that
A247: i0 = i1+1 and
A248: j1+1 = j2 and
A249: i1 = 1 and
A250: j1 <> 1;
A251: left_cell(f,k) = cell(GoB f,i1,j1-'1)
by A6,A7,A10,A11,A13,A14,A30,A46,A247,GOBOARD5:29;
1 < j0 by A24,A30,A247,A250,XXREAL_0:1;
then
A252: 1 <= j0-'1 by A30,A46,A247,NAT_1:13;
A253: j0-'1+(1+1) = j2 by A30,A46,A247,A248;
A254: LSeg(1/2*((GoB f)*(1,j1-'1)+(GoB f)*(1,j1-'1+1))- |[1,0]|,
1/2*((GoB f)*(1,j1-'1)+(GoB f)*(2,j1-'1+1)))
meets Int cell(GoB f,i1,j1-'1)
by A19,A27,A30,A46,A247,A249,A252,GOBOARD6:82;
LSeg(1/2*((GoB f)*(1,j1-'1)+(GoB f)*(1,j1-'1+1))- |[1,0]|,
1/2*((GoB f)*(1,j1-'1)+(GoB f)*(2,j1-'1+1))) misses L~f
by A5,A6,A11,A14,A17,A29,A30,A31,A46,A50,A247,A248,A249,A252,A253,
GOBOARD8:17;
then LSeg(1/2*((GoB f)*(1,j1-'1)+(GoB f)*(1,j1-'1+1))- |[1,0]|,
1/2*((GoB f)*(1,j1-'1)+(GoB f)*(2,j1-'1+1))) c= (L~f)`
by SUBSET_1:23;
then
A255: LSeg
(1/2*((GoB f)*(1,j1-'1)+(GoB f)*(1,j1-'1+1))- |[1,0]|,
1/2*((GoB f)*(1,j1-'1)+(GoB f)*(2,j1-'1+1))) c= LeftComp f
by A3,A5,A6,A55,A251,A254,Th4,NAT_1:13;
i1-'1 <= i1 by NAT_D:35;
then
A256: i1-'1 <= len GoB f by A21,XXREAL_0:2;
A257: i1-'1 = 0 by A249,XREAL_1:232;
j1-'1 <= j1 by NAT_D:35;
then
A258: j1-'1 <= width GoB f by A27,XXREAL_0:2;
A259: Int cell(GoB f,i1-'1,j1-'1) is convex
by A256,A258,Th16;
Int cell(GoB f,i1-'1,j1-'1) misses L~f by A256,A258,GOBOARD7:12;
then Int cell(GoB f,i1-'1,j1-'1) c= (L~f)` by SUBSET_1:23;
then
A260: Int cell(GoB f,i1-'1,j1-'1) c= LeftComp f
by A30,A55,A247,A255,A27,A46,A252,A257,Th4,A259,GOBOARD6:85;
A261: left_cell(f,k+1) = cell(GoB f,i1-'1,j1)
by A4,A5,A13,A14,A16,A17,A31,A45,A248,GOBOARD5:27;
A262: LSeg(1/2*((GoB f)*(1,j1-'1)+(GoB f)*(1,j1-'1+1))- |[1,0]|,
1/2*((GoB f)*(1,j1-'1+1)+(GoB f)*(1,j1-'1+2))- |[1,0]|)
meets Int cell(GoB f,i1-'1,j1-'1)
by A27,A30,A46,A247,A252,A257,GOBOARD6:85;
LSeg(1/2*((GoB f)*(1,j1-'1)+(GoB f)*(1,j1-'1+1))- |[1,0]|,
1/2*((GoB f)*(1,j1-'1+1)+(GoB f)*(1,j1-'1+2))- |[1,0]|) misses L~f
by A29,A30,A46,A247,A248,A252,GOBOARD8:31;
then LSeg(1/2*((GoB f)*(1,j1-'1)+(GoB f)*(1,j1-'1+1))- |[1,0]|,
1/2*((GoB f)*(1,j1-'1+1)+(GoB f)*(1,j1-'1+2))- |[1,0]|) c= (L~f)`
by SUBSET_1:23;
then
A263: LSeg
(1/2*((GoB f)*(1,j1-'1)+(GoB f)*(1,j1-'1+1))- |[1,0]|,
1/2*((GoB f)*(1,j1-'1+1)+(GoB f)*(1,j1-'1+2))- |[1,0]|) c= LeftComp f
by A55,A260,A262,Th4;
A264: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A261,A263,A26,A29,A46,A248,A257,Th4,A264,
GOBOARD6:85;
end;
suppose that
A265: i0 = i1+1 and
A266: j1+1 = j2 and
A267: i1 <> 1 and
A268: j1 <> 1;
A269: left_cell(f,k) = cell(GoB f,i1,j1-'1)
by A6,A7,A10,A11,A13,A14,A30,A46,A265,GOBOARD5:29;
1 < j0 by A24,A30,A265,A268,XXREAL_0:1;
then
A270: 1 <= j0-'1 by A30,A46,A265,NAT_1:13;
1 < i1 by A20,A267,XXREAL_0:1;
then
A271: 1 <= i1-'1 by A45,NAT_1:13;
A272: i1-'1+(1+1) = i0 by A45,A265;
A273: j0-'1+(1+1) = j2 by A30,A46,A265,A266;
A274: LSeg(1/2*((GoB f)*(i1-'1,j0-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1,j0-'1)+(GoB f)*(i0,j1)))
meets Int cell(GoB f,i1,j1-'1)
by A19,A20,A27,A30,A46,A265,A270,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i1-'1,j0-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1,j0-'1)+(GoB f)*(i0,j1))) misses L~f
by A5,A6,A11,A14,A17,A19,A29,A30,A31,A45,A46,A50,A266,A270,A271,A272,A273,
GOBOARD8:12;
then LSeg(1/2*((GoB f)*(i1-'1,j0-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1,j0-'1)+(GoB f)*(i0,j1))) c= (L~f)` by SUBSET_1:23;
then
A275: LSeg(1/2*((GoB f)*(i1-'1,j0-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1,j0-'1)+(GoB f)*(i0,j1))) c= LeftComp f
by A3,A5,A6,A55,A269,A274,Th4,NAT_1:13;
i1-'1 <= i1 by NAT_D:35;
then
A276: i1-'1 <= len GoB f by A21,XXREAL_0:2;
j1-'1 <= j1 by NAT_D:35;
then
A277: j1-'1 <= width GoB f by A27,XXREAL_0:2;
A278: Int cell(GoB f,i1-'1,j1-'1) is convex
by A276,A277,Th16;
Int cell(GoB f,i1-'1,j1-'1) misses L~f by A276,A277,GOBOARD7:12;
then Int cell(GoB f,i1-'1,j1-'1) c= (L~f)` by SUBSET_1:23;
then
A279: Int cell(GoB f,i1-'1,j1-'1) c= LeftComp f
by A30,A55,A265,A275,A21,A27,A45,A46,A270,A271,Th4,A278,GOBOARD6:82
;
A280: left_cell(f,k+1) = cell(GoB f,i1-'1,j1)
by A4,A5,A13,A14,A16,A17,A31,A45,A266,GOBOARD5:27;
A281: LSeg(1/2*((GoB f)*(i1-'1,j1-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j2)))
meets Int cell(GoB f,i1-'1,j1-'1)
by A21,A27,A30,A45,A46,A265,A270,A271,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i1-'1,j1-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j2))) misses L~f
by A5,A6,A11,A14,A17,A19,A29,A30,A31,A45,A46,A50,A266,A270,A271,A272,A273,
GOBOARD8:2;
then LSeg(1/2*((GoB f)*(i1-'1,j1-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j2))) c= (L~f)` by SUBSET_1:23;
then
A282: LSeg(1/2*((GoB f)*(i1-'1,j1-'1)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j2))) c= LeftComp f
by A55,A279,A281,Th4;
A283: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A280,A282,A21,A26,A29,A45,A266,A271,Th4,A283,
GOBOARD6:82;
end;
suppose that
A284: j0 = j1+1 and
A285: i1+1 = i2;
left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A45,A284,GOBOARD5:30
.= left_cell(f,k+1)
by A4,A5,A13,A14,A16,A17,A30,A31,A46,A284,A285,GOBOARD5:28;
hence thesis by A3,A5,A6,NAT_1:13;
end;
suppose that
A286: i0+1 = i1 and
A287: i1+1 = i2 and
A288: j0 = width GoB f;
A289: left_cell(f,k) = cell(GoB f,i0,width GoB f)
by A6,A7,A10,A11,A13,A14,A30,A49,A286,A288,GOBOARD5:28;
A290: left_cell(f,k+1) = cell(GoB f,i1,width GoB f)
by A4,A5,A13,A14,A16,A17,A30,A31,A49,A286,A287,A288,GOBOARD5:28;
A291: LSeg
(1/2*((GoB f)*(i0,width GoB f)+(GoB f)*(i0+1,width GoB f))+|[0,1]|,
1/2*((GoB f)*(i1,width GoB f)+(GoB f)*(i1+1,width GoB f))+|[0,1]|)
meets Int cell(GoB f,i0,width GoB f) by A18,A21,A286,GOBOARD6:83;
LSeg(1/2*((GoB f)*(i0,width GoB f)+(GoB f)*(i0+1,width GoB f))+|[0,1 ]| ,
1/2*((GoB f)*(i1,width GoB f)+(GoB f)*(i1+1,width GoB f))+|[0,1]|)
misses L~f by A18,A23,A51,A286,A287,GOBOARD8:28;
then LSeg(1/2*((GoB f)*(i0,width GoB f)+(GoB f)*(i0+1,width GoB f))+|[0,1 ]|,
1/2*((GoB f)*(i1,width GoB f)+(GoB f)*(i1+1,width GoB f))+|[0,1]|)
c= (L~f)` by SUBSET_1:23;
then
A292: LSeg
(1/2*((GoB f)*(i0,width GoB f)+(GoB f)*(i0+1, width GoB f))+
|[0,1]|,
1/2*((GoB f)*(i1,width GoB f)+(GoB f)*(i1+1,width GoB f))+|[0,1]|)
c= LeftComp f by A3,A5,A6,A55,A289,A291,Th4,NAT_1:13;
A293: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A290,A292,A20,A23,A287,Th4,A293,GOBOARD6:83;
end;
suppose that
A294: i0+1 = i1 and
A295: i1+1 = i2 and
A296: j0 <> width GoB f;
A297: left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A46,A294,GOBOARD5:28;
width GoB f > j0 by A25,A296,XXREAL_0:1;
then
A298: width GoB f >= j0+1 by NAT_1:13;
A299: left_cell(f,k+1) = cell(GoB f,i1,j1)
by A4,A5,A13,A14,A16,A17,A31,A46,A295,GOBOARD5:28;
A300: LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0+1,j0+1)),
1/2*((GoB f)*(i1,j0)+(GoB f)*(i1+1,j0+1)))
meets Int cell(GoB f,i0,j1)
by A18,A21,A26,A30,A294,A298,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0+1,j0+1)),
1/2*((GoB f)*(i1,j0)+(GoB f)*(i1+1,j0+1))) misses L~f
by A5,A6,A11,A14,A17,A18,A23,A24,A30,A31,A50,A51,A294,A295,A298,
GOBOARD8:14;
then LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0+1,j0+1)),
1/2*((GoB f)*(i1,j0)+(GoB f)*
(i1+1,j0+1))) c= (L~f)` by SUBSET_1:23;
then
A301: LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0+1,j0+1)),
1/2*((GoB f)*(i1,j0)+(GoB f)*(i1+1,j0+1))) c= LeftComp f
by A3,A5,A6,A55,A297,A300,Th4,NAT_1:13;
A302: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A299,A301,A20,A23,A24,A30,A294,A295,A298,Th4
,A302,GOBOARD6:82;
end;
suppose that
A303: i0+1 = i1 and
A304: j1+1 = j2;
left_cell(f,k) = cell(GoB f,i0,j1)
by A6,A7,A10,A11,A13,A14,A30,A46,A303,GOBOARD5:28
.= left_cell(f,k+1) by A4,A5,A13,A14,A16,A17,A31,A303,A304,GOBOARD5:27;
hence thesis by A3,A5,A6,NAT_1:13;
end;
suppose that
A305: j0+1 = j1 and
A306: i1+1 = i2 and
A307: i0 = 1 and
A308: j1 = width GoB f;
A309: left_cell(f,k) = cell(GoB f,i1-'1,j0)
by A6,A7,A10,A11,A13,A14,A30,A45,A305,GOBOARD5:27;
A310: i0-'1 = 0 by A307,XREAL_1:232;
A311: j1-'1 = j0 by A305,NAT_D:34;
A312: LSeg(1/2*((GoB f)*(1,j0)+(GoB f)*(1,j1))- |[1,0]|,
(GoB f)*(1,j1)+|[-1,1]|) meets Int cell(GoB f,i1-'1,j0)
by A24,A27,A30,A305,A310,GOBOARD6:85;
LSeg(1/2*((GoB f)*(1,j0)+(GoB f)*(1,j1))- |[1,0]|,
(GoB f)*(1,j1)+|[-1,1]|) misses L~f by A308,A311,GOBOARD8:33;
then LSeg(1/2*((GoB f)*(1,j0)+(GoB f)*(1,j1))- |[1,0]|,
(GoB f)*(1,j1)+|[-1,1]|) c= (L~f)` by SUBSET_1:23;
then
A313: LSeg(1/2*((GoB f)*(1,j0)+(GoB f)*(1,j1))- |[1,0]|,
(GoB f)*(1,j1)+|[-1,1]|) c= LeftComp f
by A3,A5,A6,A55,A309,A312,Th4,NAT_1:13;
i1-'1 <= i1 by NAT_D:35;
then
A314: i1-'1 <= len GoB f by A21,XXREAL_0:2;
A315: Int cell(GoB f,i1-'1,j1) is convex by A27,A314,Th16;
Int cell(GoB f,i1-'1,j1) misses L~f by A27,A314,GOBOARD7:12;
then Int cell(GoB f,i1-'1,j1) c= (L~f)` by SUBSET_1:23;
then
A316: Int cell(GoB f,i1-'1,j1) c= LeftComp f by A30,A55,A305,A313,A308
,A310,Th4,A315,GOBOARD6:89;
A317: left_cell(f,k+1) = cell(GoB f,i1,j1)
by A4,A5,A13,A14,A16,A17,A31,A305,A306,GOBOARD5:28;
A318: LSeg((GoB f)*(1,j1)+|[-1,1]|,
1/2*((GoB f)*(1,j1)+(GoB f)*(2,j1))+|[0,1]|)
meets Int cell(GoB f,i1-'1,j1) by A30,A305,A308,A310,GOBOARD6:89;
LSeg((GoB f)*(1,j1)+|[-1,1]|,
1/2*((GoB f)*(1,j1)+(GoB f)*(2,j1))+|[0,1]|) misses L~f
by A308,GOBOARD8:29;
then LSeg((GoB f)*(1,j1)+|[-1,1]|,
1/2*((GoB f)*(1,j1)+(GoB f)*(2,j1))+|[0,1]|) c= (L~f)`
by SUBSET_1:23;
then
A319: LSeg((GoB f)*(1,j1)+|[-1,1]|,
1/2*((GoB f)*(1,j1)+(GoB f)*(2,j1))+|[0,1]|) c= LeftComp f
by A55,A316,A318,Th4;
A320: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A317,A319,A23,A30,A305,A306,A307,A308,Th4,A320,
GOBOARD6:83;
end;
suppose that
A321: j0+1 = j1 and
A322: i1+1 = i2 and
A323: i0 <> 1 and
A324: j1 = width GoB f;
A325: left_cell(f,k) = cell(GoB f,i1-'1,j0)
by A6,A7,A10,A11,A13,A14,A30,A45,A321,GOBOARD5:27;
1 < i0 by A18,A323,XXREAL_0:1;
then
A326: 1 <= i0-'1 by A30,A45,A321,NAT_1:13;
A327: j1-'1 = j0 by A321,NAT_D:34;
A328: i1-'1+(1+1) = i2 by A45,A322;
A329: LSeg(1/2*((GoB f)*(i1-'1,j0)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1))+|[0,1]|)
meets Int cell(GoB f,i1-'1,j0)
by A21,A24,A27,A30,A45,A321,A326,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i1-'1,j0)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1))+|[0,1]|) misses L~f
by A5,A6,A11,A14,A17,A23,A30,A31,A45,A50,A321,A324,A326,A327,A328,
GOBOARD8:9;
then LSeg(1/2*((GoB f)*(i1-'1,j0)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1))+|[0,1]|) c= (L~f)`
by SUBSET_1:23;
then
A330: LSeg(1/2*((GoB f)*(i1-'1,j0)+(GoB f)*(i1,j1)),
1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1))+|[0,1]|) c= LeftComp f
by A3,A5,A6,A55,A325,A329,Th4,NAT_1:13;
i1-'1 <= i1 by NAT_D:35;
then
A331: i1-'1 <= len GoB f by A21,XXREAL_0:2;
A332: Int cell(GoB f,i1-'1,j1) is convex by A27,A331,Th16;
Int cell(GoB f,i1-'1,j1) misses L~f by A27,A331,GOBOARD7:12;
then Int cell(GoB f,i1-'1,j1) c= (L~f)` by SUBSET_1:23;
then
A333: Int cell(GoB f,i1-'1,j1) c= LeftComp f by A30,A55,A321,A330,A19,A45
,A324,A326,Th4,A332,GOBOARD6:83;
A334: left_cell(f,k+1) = cell(GoB f,i1,j1)
by A4,A5,A13,A14,A16,A17,A31,A321,A322,GOBOARD5:28;
A335: LSeg(1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1))+|[0,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i2,j1))+|[0,1]|)
meets Int cell(GoB f,i1-'1,j1) by A21,A30,A45,A321,A324,A326,
GOBOARD6:83;
LSeg(1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1))+|[0,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i2,j1))+|[0,1]|) misses L~f
by A23,A30,A45,A321,A324,A326,A328,GOBOARD8:28;
then LSeg(1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1))+|[0,1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i2,j1))+|[0,1]|) c= (L~f)`
by SUBSET_1:23;
then
A336: LSeg(1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1))+|[0, 1]|,
1/2*((GoB f)*(i1,j1)+(GoB f)*(i2,j1))+|[0,1]|) c= LeftComp f
by A55,A333,A335,Th4;
A337: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A334,A336,A20,A23,A322,A324,Th4,A337,
GOBOARD6:83;
end;
suppose that
A338: j0+1 = j1 and
A339: i1+1 = i2 and
A340: i0 = 1 and
A341: j1 <> width GoB f;
A342: left_cell(f,k) = cell(GoB f,i1-'1,j0)
by A6,A7,A10,A11,A13,A14,A30,A45,A338,GOBOARD5:27;
width GoB f > j1 by A27,A341,XXREAL_0:1;
then
A343: width GoB f >= j1+1 by NAT_1:13;
A344: i0-'1 = 0 by A340,XREAL_1:232;
A345: LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0,j1))- |[1,0]|,
1/2*((GoB f)*(i0,j1)+(GoB f)*(i0,j1+1))- |[1,0]|)
meets Int cell(GoB f,i1-'1,j0)
by A24,A27,A30,A338,A340,A344,GOBOARD6:85;
LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0,j1))- |[1,0]|,
1/2*((GoB f)*(i0,j1)+(GoB f)*(i0,j1+1))- |[1,0]|) misses L~f
by A24,A53,A338,A340,A343,GOBOARD8:31;
then LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0,j1))- |[1,0]|,
1/2*((GoB f)*(i0,j1)+(GoB f)*(i0,j1+1))- |[1,0]|) c= (L~f)`
by SUBSET_1:23;
then
A346: LSeg(1/2*((GoB f)*(i0,j0)+(GoB f)*(i0,j1))- |[1,0 ]|,
1/2*((GoB f)*(i0,j1)+(GoB f)*(i0,j1+1))- |[1,0]|) c= LeftComp f
by A3,A5,A6,A55,A342,A345,Th4,NAT_1:13;
i1-'1 <= i1 by NAT_D:35;
then
A347: i1-'1 <= len GoB f by A21,XXREAL_0:2;
A348: Int cell(GoB f,i1-'1,j1) is convex by A27,A347,Th16;
Int cell(GoB f,i1-'1,j1) misses L~f by A27,A347,GOBOARD7:12;
then Int cell(GoB f,i1-'1,j1) c= (L~f)` by SUBSET_1:23;
then
A349: Int cell(GoB f,i1-'1,j1) c= LeftComp f by A30,A55,A338,A346,A26
,A340,A343,A344,Th4,A348,GOBOARD6:85;
A350: left_cell(f,k+1) = cell(GoB f,i1,j1)
by A4,A5,A13,A14,A16,A17,A31,A338,A339,GOBOARD5:28;
A351: LSeg(1/2*((GoB f)*(i1,j0+1)+(GoB f)*(i1,j0+2))- |[1,0]|,
1/2*((GoB f)*(i1,j0+1)+(GoB f)*(i2,j0+2)))
meets Int cell(GoB f,i1-'1,j1)
by A26,A30,A338,A340,A343,A344,GOBOARD6:85;
LSeg(1/2*((GoB f)*(i1,j0+1)+(GoB f)*(i1,j0+2))- |[1,0]|,
1/2*((GoB f)*(i1,j0+1)+(GoB f)*(i2,j0+2))) misses L~f
by A5,A6,A11,A14,A17,A24,A30,A31,A50,A338,A339,A340,A343,GOBOARD8:18;
then LSeg(1/2*((GoB f)*(i1,j0+1)+(GoB f)*(i1,j0+2))- |[1,0]|,
1/2*((GoB f)*(i1,j0+1)+(GoB f)*
(i2,j0+2))) c= (L~f)` by SUBSET_1:23;
then
A352: LSeg
(1/2*((GoB f)*(i1,j0+1)+(GoB f)*(i1,j0+2))- |[ 1,0]|,
1/2*((GoB f)*(i1,j0+1)+(GoB f)*(i2,j0+2))) c= LeftComp f
by A55,A349,A351,Th4;
A353: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A350,A352,A20,A23,A26,A338,A339,A343,Th4,A353,
GOBOARD6:82;
end;
suppose that
A354: j0+1 = j1 and
A355: i1+1 = i2 and
A356: i0 <> 1 and
A357: j1 <> width GoB f;
A358: left_cell(f,k) = cell(GoB f,i1-'1,j0)
by A6,A7,A10,A11,A13,A14,A30,A45,A354,GOBOARD5:27;
1 < i0 by A18,A356,XXREAL_0:1;
then
A359: 1 <= i0-'1 by A30,A45,A354,NAT_1:13;
width GoB f > j1 by A27,A357,XXREAL_0:1;
then
A360: width GoB f >= j1+1 by NAT_1:13;
A361: i1-'1+(1+1) = i2 by A45,A355;
A362: LSeg(1/2*((GoB f)*(i0-'1,j0)+(GoB f)*(i0,j1)),
1/2*((GoB f)*(i0-'1,j1)+(GoB f)*(i0,j1+1)))
meets Int cell(GoB f,i1-'1,j0)
by A21,A24,A27,A30,A45,A354,A359,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i0-'1,j0)+(GoB f)*(i0,j1)),
1/2*((GoB f)*(i0-'1,j1)+(GoB f)*(i0,j1+1))) misses L~f
by A5,A6,A11,A14,A17,A23,A24,A30,A31,A45,A50,A53,A354,A359,A360
,A361,GOBOARD8:3;
then LSeg(1/2*((GoB f)*(i0-'1,j0)+(GoB f)*(i0,j1)),
1/2*((GoB f)*(i0-'1,j1)+(GoB f)*
(i0,j1+1))) c= (L~f)` by SUBSET_1:23;
then
A363: LSeg(1/2*((GoB f)*(i0-'1,j0)+(GoB f)*(i0,j1)),
1/2*((GoB f)*(i0-'1,j1)+(GoB f)*(i0,j1+1))) c= LeftComp f
by A3,A5,A6,A55,A358,A362,Th4,NAT_1:13;
i1-'1 <= i1 by NAT_D:35;
then
A364: i1-'1 <= len GoB f by A21,XXREAL_0:2;
A365: Int cell(GoB f,i1-'1,j1) is convex by A27,A364,Th16;
Int cell(GoB f,i1-'1,j1) misses L~f by A27,A364,GOBOARD7:12;
then Int cell(GoB f,i1-'1,j1) c= (L~f)` by SUBSET_1:23;
then
A366: Int cell(GoB f,i1-'1,j1) c= LeftComp f by A30,A55,A354,A363,A19,A26
,A45,A359,A360,Th4,A365,GOBOARD6:82;
A367: left_cell(f,k+1) = cell(GoB f,i1,j1)
by A4,A5,A13,A14,A16,A17,A31,A354,A355,GOBOARD5:28;
A368: LSeg(1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1+1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i2,j1+1)))
meets Int cell(GoB f,i1-'1,j1) by A21,A26,A30,A45,A354,A359,A360,
GOBOARD6:82;
LSeg(1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1+1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i2,j1+1))) misses L~f
by A5,A6,A11,A14,A17,A23,A24,A30,A31,A45,A50,A53,A354,A359,A360,A361,
GOBOARD8:15;
then LSeg(1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1+1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i2,j1+1))) c= (L~f)` by SUBSET_1:23;
then
A369: LSeg(1/2*((GoB f)*(i1-'1,j1)+(GoB f)*(i1,j1+1)),
1/2*((GoB f)*(i1,j1)+(GoB f)*(i2,j1+1))) c= LeftComp f
by A55,A366,A368,Th4;
A370: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A367,A369,A20,A23,A26,A355,A360,Th4,A370,
GOBOARD6:82;
end;
suppose that
A371: j0+1 = j1 and
A372: j1+1 = j2 and
A373: i0 = 1;
A374: left_cell(f,k) = cell(GoB f,0,j0)
by A6,A7,A10,A11,A13,A14,A30,A56,A371,A373,GOBOARD5:27;
A375: left_cell(f,k+1) = cell(GoB f,0,j1)
by A4,A5,A13,A14,A16,A17,A30,A31,A56,A371,A372,A373,GOBOARD5:27;
A376: LSeg(1/2*((GoB f)*(1,j0)+(GoB f)*(1,j1))- |[1,0]|,
1/2*((GoB f)*(1,j1)+(GoB f)*(1,j2))- |[1,0]|)
meets Int cell(GoB f,0,j0) by A24,A27,A371,GOBOARD6:85;
LSeg(1/2*((GoB f)*(1,j0)+(GoB f)*(1,j1))- |[1,0]|,
1/2*((GoB f)*(1,j1)+(GoB f)*(1,j2))- |[1,0]|) misses L~f
by A24,A29,A53,A371,A372,GOBOARD8:31;
then LSeg(1/2*((GoB f)*(1,j0)+(GoB f)*(1,j1))- |[1,0]|,
1/2*((GoB f)*(1,j1)+(GoB f)*(1,j2))- |[1,0]|) c= (L~f)`
by SUBSET_1:23;
then
A377: LSeg(1/2*((GoB f)*(1,j0)+(GoB f)*(1,j1))- |[1,0]|,
1/2*((GoB f)*(1,j1)+(GoB f)*(1,j2))- |[1,0]|) c= LeftComp f
by A3,A5,A6,A55,A374,A376,Th4,NAT_1:13;
A378: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A55,A375,A377,A26,A29,A372,Th4,A378,GOBOARD6:85;
end;
suppose that
A379: j0+1 = j1 and
A380: j1+1 = j2 and
A381: i0 <> 1;
A382: left_cell(f,k) = cell(GoB f,i1-'1,j0)
by A6,A7,A10,A11,A13,A14,A30,A45,A379,GOBOARD5:27;
1 < i0 by A18,A381,XXREAL_0:1;
then
A383: 1 <= i0-'1 by A30,A45,A379,NAT_1:13;
A384: left_cell(f,k+1) = cell(GoB f,i1-'1,j1)
by A4,A5,A13,A14,A16,A17,A31,A45,A380,GOBOARD5:27;
A385: LSeg(1/2*((GoB f)*(i0-'1,j0)+(GoB f)*(i0,j1)),
1/2*((GoB f)*(i0-'1,j1)+(GoB f)*(i0,j2)))
meets Int cell(GoB f,i1-'1,j0)
by A21,A24,A27,A30,A45,A379,A383,GOBOARD6:82;
LSeg(1/2*((GoB f)*(i0-'1,j0)+(GoB f)*(i0,j1)),
1/2*((GoB f)*(i0-'1,j1)+(GoB f)*(i0,j2))) misses L~f
by A5,A6,A11,A14,A17,A19,A24,A29,A30,A31,A45,A50,A53,A379,A380,A383,GOBOARD8:1;
then LSeg(1/2*((GoB f)*(i0-'1,j0)+(GoB f)*(i0,j1)),
1/2*((GoB f)*(i0-'1,j1)+(GoB f)*(i0,j2))) c= (L~f)` by SUBSET_1:23;
then
A386: LSeg(1/2*((GoB f)*(i0-'1,j0)+(GoB f)*(i0,j1)),
1/2*((GoB f)*(i0-'1,j1)+(GoB f)*(i0,j2))) c= LeftComp f
by A3,A5,A6,A55,A382,A385,Th4,NAT_1:13;
A387: Int left_cell(f,k+1) is convex
by A4,A5,Th17;
Int left_cell(f,k+1) misses L~f by A4,A5,GOBOARD8:37;
then Int left_cell(f,k+1) c= (L~f)` by SUBSET_1:23;
hence thesis by A30,A55,A379,A384,A386,A19,A26,A29,A45,A380,A383
,Th4,A387,GOBOARD6:82;
end;
end;
hence thesis;
end;
end;
end;
thus for k holds P[k] from NAT_1:sch 2(A1,A2);
end;
theorem
GoB Rev f = GoB f by Lm1;
theorem Th21:
RightComp f = LeftComp Rev f
proof
LeftComp Rev f is_a_component_of (L~Rev f)` by Def1;
then
A1: LeftComp Rev f is_a_component_of (L~f)` by SPPOL_2:22;
A2: len f >= 4 by GOBOARD7:34;
A3: len f >= 1+1 by GOBOARD7:34,XXREAL_0:2;
A4: len f -' 1 + 1 = len f by A2,XREAL_1:235,XXREAL_0:2;
then
A5: 1 <= len f -' 1 by A3,XREAL_1:6;
A6: len f -' 1 + 1 <= len Rev f by A4,FINSEQ_5:def 3;
right_cell(f,1) = left_cell(Rev f,len f -' 1) by A4,A5,Th9;
then Int right_cell(f,1) c= LeftComp Rev f by A5,A6,Th19;
hence thesis by A1,Def2;
end;
theorem
RightComp Rev f = LeftComp f proof Rev Rev f = f;
hence thesis by Th21;
end;
theorem
for k st 1 <= k & k+1 <= len f holds Int right_cell(f,k) c= RightComp f
proof
let k such that
A1: 1 <= k and
A2: k+1 <= len f;
A3: len f = len Rev f by FINSEQ_5:def 3;
k <= len f by A2,NAT_1:13;
then
A4: len f-'k+k = len f by XREAL_1:235;
then
A5: 1 <= len f-'k by A2,XREAL_1:6;
A6: len f-'k+1 <= len f by A1,A4,XREAL_1:6;
A7: right_cell(f,k) = left_cell(Rev f,len f-'k) by A1,A4,A5,Th9;
RightComp f = LeftComp Rev f by Th21;
hence thesis by A3,A5,A6,A7,Th19;
end;