:: Left and Right Component of the Complement of a Special Closed Curve :: by Andrzej Trybulec :: :: Received October 29, 1995 :: Copyright (c) 1995-2012 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; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, NUMBERS, COMPLEX1, REAL_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, MATRIX_1, 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, SEQ_1, GOBOARD1, NAT_D, RELSET_1, CONVEX1, RVSUM_1, SEQ_4; registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, FINSEQ_1, FINSEQ_6, STRUCT_0, PRE_TOPC, EUCLID, GOBOARD2, GOBOARD5, ORDINAL1, RLTOPSP1, JORDAN1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, GOBOARD5, GOBOARD1, JORDAN1, XBOOLE_0, STRUCT_0, SEQM_3; 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_1, NAT_D, SEQM_3, SEQ_4; schemes NAT_1; begin reserve f for non constant standard special_circular_sequence, i,j,k,i1,i2,j1,j2 for Element of 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 set 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 by XBOOLE_0:def 7; 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,XBOOLE_1:65; A7: B <> {} by A4,XBOOLE_1:65; reconsider A,B as non empty Subset of GX by A4,XBOOLE_1:65; 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; canceled; theorem Th6: :: 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 Th7: 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 Th8: 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 Th7; 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,Th8; 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; <*1,2*>.1 = 1 by FINSEQ_1:44; hence thesis by FINSEQ_1:44; 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; 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,GOBOARD1:def 9; 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: abs(i2-i1) = abs(-(i1-i2)) .= abs(i1-i2) by COMPLEX1:52; A22: abs(j2-j1) = abs(-(j1-j2)) .= abs(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 abs(i1-i2)+abs(j1-j2) = 1 by A2,A3,A14,A16,A17,A18,A21,A22,A23,GOBOARD1:def 9; 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) = {} by XBOOLE_0:def 7; 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) = {} by XBOOLE_0:def 7; 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 Th9: 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 Element of 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_1:38; then A15: i1-'1+1 = i1 by XREAL_1:235; 1 <= j1 by A7,MATRIX_1:38; then A16: j1-'1+1 = j1 by XREAL_1:235; reconsider i19=i1, i29=i2, j19=j1, j29=j2 as Element of REAL; f is_sequence_on GoB f by GOBOARD5:def 5; then abs(i1-i2)+abs(j1-j2) = 1 by A7,A8,A9,A10,A11,A13,GOBOARD1:def 9; then A17: abs(i19-i29)=1 & j1=j2 or abs(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 Th10: 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,Th9; end; theorem Th11: 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 Element of NAT such that A5: [i1,j1] in Indices GoB f and A6: f/.k = (GoB f)*(i1,j1) by A3,GOBOARD1:def 9; 1 <= k+1 by NAT_1:11; then A7: k+1 in dom f by A2,FINSEQ_3:25; then consider i2,j2 being Element of NAT such that A8: [i2,j2] in Indices GoB f and A9: f/.(k+1) = (GoB f)*(i2,j2) by A3,GOBOARD1:def 9; 1 <= i1 by A5,MATRIX_1:38; then A10: i1-'1+1 = i1 by XREAL_1:235; 1 <= j1 by A5,MATRIX_1:38; then A11: j1-'1+1 = j1 by XREAL_1:235; reconsider i19=i1, i29=i2, j19=j1, j29=j2 as Element of REAL; abs(i1-i2)+abs(j1-j2) = 1 by A3,A4,A5,A6,A7,A8,A9,GOBOARD1:def 9; then A12: abs(i19-i29)=1 & j1=j2 or abs(j19-j29)=1 & i1=i2 by SEQM_3:42; A13: i1 <= len GoB f by A5,MATRIX_1:38; A14: j1 <= width GoB f by A5,MATRIX_1:38; 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_1:38; 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_1:38; thus j1 <= width GoB f by A5,MATRIX_1:38; 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_1:38; 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_1:38; thus j2 <= width GoB f by A8,MATRIX_1:38; thus thesis by A1,A2,A5,A6,A8,A9,A10,A18,GOBOARD5:30; end; end; theorem Th12: 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 set; 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 set; 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 set; 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 set; 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,Th6; end; end; theorem Th13: 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 set; 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 set; 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 set; 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 set; 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,Th6; end; end; theorem Th14: 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 by XBOOLE_1:65; 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 by XBOOLE_1:65; 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 by XBOOLE_1:65; 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 by XBOOLE_1:65; 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 by XBOOLE_1:65; 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 by XBOOLE_1:65; 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 by XBOOLE_1:65; 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 by XBOOLE_1:65; 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 by XBOOLE_1:65; end; end; theorem Th15: 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,Th11; hence thesis by Th14; end; theorem Th16: 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,Th10; hence thesis by A3,A5,A6,Th15; end; theorem Th17: 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,Th13; Int h_strip(G,j) is convex by A2,Th12; hence thesis by A3,A4,Th6; end; canceled; theorem Th19: 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,Th11; hence thesis by Th17; end; theorem Th20: 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,Th10; hence thesis by A3,A5,A6,Th19; end; definition let f; A1: 1+1 < len f by GOBOARD7:34,XXREAL_0:2; then A2: Int left_cell(f,1) <> {} by Th15; A3: Int right_cell(f,1) <> {} by A1,Th16; 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,Th19; 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,Th15,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,Th20; 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,Th16,XBOOLE_1:3; hence thesis by A3,A6,A7,Th3; end; uniqueness by A3,Th1,XBOOLE_1:67; end; theorem Th21: for k st 1 <= k & k+1 <= len f holds Int left_cell(f,k) c= LeftComp f proof defpred P[Element of 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 Element of 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 Element of 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 Element of 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_1:38; A19: i0 <= len GoB f by A10,MATRIX_1:38; A20: 1 <= i1 by A13,MATRIX_1:38; A21: i1 <= len GoB f by A13,MATRIX_1:38; A22: 1 <= i2 by A16,MATRIX_1:38; A23: i2 <= len GoB f by A16,MATRIX_1:38; A24: 1 <= j0 by A10,MATRIX_1:38; A25: j0 <= width GoB f by A10,MATRIX_1:38; A26: 1 <= j1 by A13,MATRIX_1:38; A27: j1 <= width GoB f by A13,MATRIX_1:38; A28: 1 <= j2 by A16,MATRIX_1:38; A29: j2 <= width GoB f by A16,MATRIX_1:38; 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; A32: f is_sequence_on GoB f by GOBOARD5:def 5; then abs(i0-i1)+abs(j0-j1) = 1 by A9,A10,A11,A12,A13,A14,GOBOARD1:def 9; then A33: abs(i09-i19)=1 & j0 = j1 or abs(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; abs(i1-i2)+abs(j1-j2) = 1 by A12,A13,A14,A15,A16,A17,A32,GOBOARD1:def 9; then A35: abs(i19-i29)=1 & j1 = j2 or abs(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_1:38; then A45: i1 = i1 -' 1 + 1 by XREAL_1:235; j1 >= 1 by A13,MATRIX_1:38; 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,Th19; 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,GOBOARD6:84,Th4,A64; 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,Th19; 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,GOBOARD6:82,Th4,A73; 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,Th17; 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,GOBOARD6:90,Th4,A83; 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,Th19; 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,GOBOARD6:84, Th4,A88; 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,Th17; 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, GOBOARD6:84,Th4,A97; 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,Th19; 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,GOBOARD6:84,Th4,A102; 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,Th17; 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,GOBOARD6:86,Th4,A113,A112; 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,Th19; 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, GOBOARD6:82,Th4,A119; 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,Th17; 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,GOBOARD6:82,Th4,A131,A130; 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,Th19; 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, GOBOARD6:82,Th4,A136; 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,Th19; 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,GOBOARD6:86,Th4,A144; 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,Th19; 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, GOBOARD6:82,Th4,A153; 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,Th17; 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,GOBOARD6:88,Th4,A161; 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,Th19; 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,GOBOARD6:86,Th4, A166; 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,Th17; 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,GOBOARD6:83,Th4,A175; 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,Th19; 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, GOBOARD6:82,Th4,A180; 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,Th17; 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,GOBOARD6:86,Th4,A189; 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,Th19; 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,GOBOARD6:86,Th4, A194; 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,Th17; 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,GOBOARD6:82,Th4 ,A204; 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,Th19; 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, GOBOARD6:82,Th4,A209; 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,Th17; 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,GOBOARD6:87,Th4,A223; 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,Th19; 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,GOBOARD6:85, Th4,A228; 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,Th17; 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, GOBOARD6:84,Th4,A241; 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,Th19; 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, GOBOARD6:82,Th4,A246; 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,Th17; 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, GOBOARD6:85,Th4,A259; 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,Th19; 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,GOBOARD6:85, Th4,A264; 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,Th17; 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, GOBOARD6:82,Th4,A278; 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,Th19; 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, GOBOARD6:82,Th4,A283; 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,Th19; 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,GOBOARD6:83,Th4,A293; 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,Th19; 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, GOBOARD6:82,Th4,A302; 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,Th17; 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,GOBOARD6:89,Th4,A315; 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,Th19; 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, GOBOARD6:83,Th4,A320; 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,Th17; 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,GOBOARD6:83,Th4,A332; 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,Th19; 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,GOBOARD6:83,Th4, A337; 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,Th17; 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,GOBOARD6:85,Th4,A348; 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,Th19; 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, GOBOARD6:82,Th4,A353; 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,Th17; 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, GOBOARD6:82,Th4,A365; 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,Th19; 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,GOBOARD6:82, Th4,A370; 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,Th19; 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,GOBOARD6:85,Th4,A378; 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,Th19; 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,GOBOARD6:82,Th4,A387; end; end; hence thesis; end; end; end; thus for k holds P[k] from NAT_1:sch 1(A1,A2); end; theorem GoB Rev f = GoB f by Lm1; theorem Th23: 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,Th10; then Int right_cell(f,1) c= LeftComp Rev f by A5,A6,Th21; hence thesis by A1,Def2; end; theorem RightComp Rev f = LeftComp f proof Rev Rev f = f; hence thesis by Th23; 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,Th10; RightComp f = LeftComp Rev f by Th23; hence thesis by A3,A5,A6,A7,Th21; end;