:: Introducing Spans :: by Andrzej Trybulec :: :: Received May 27, 2002 :: Copyright (c) 2002-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, SPPOL_1, XBOOLE_0, TOPREAL2, EUCLID, JORDAN1H, SPRECT_2, GOBOARD5, FUNCT_1, GOBOARD1, JORDAN8, PARTFUN1, RELAT_1, JORDAN11, ARYTM_1, XXREAL_0, ARYTM_3, FINSEQ_1, GOBRD13, NEWTON, CARD_1, ORDINAL4, PRE_TOPC, PCOMPS_1, MATRIX_1, TREES_1, STRUCT_0, TARSKI, COMPLEX1, NAT_1, TOPREAL1, RLTOPSP1, RFINSEQ, CONNSP_1, TOPS_1, RELAT_2, GOBOARD9, RCOMP_1, METRIC_1, REAL_1, FINSEQ_5, JORDAN2C, JORDAN13, CONVEX1, XXREAL_2; notations TARSKI, GOBOARD5, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, NAT_D, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, COMPLEX1, NEWTON, FINSEQ_1, FINSEQ_2, FINSEQ_4, STRUCT_0, RFINSEQ, MATRIX_0, METRIC_1, PRE_TOPC, TOPS_1, CONNSP_1, PCOMPS_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, SPPOL_1, SPRECT_2, GOBOARD9, JORDAN8, GOBRD13, JORDAN2C, JORDAN1H, JORDAN11; constructors REAL_1, FINSEQ_4, NEWTON, RFINSEQ, NAT_D, TOPS_1, CONNSP_1, TOPREAL4, PSCOMP_1, GOBOARD9, SPRECT_2, JORDAN2C, JORDAN8, JORDAN1H, JORDAN11, RELSET_1, PCOMPS_1, FUNCSDOM, CONVEX1, GOBRD13, JORDAN9, DOMAIN_1; registrations RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, TOPREAL2, SPPOL_2, GOBOARD9, SPRECT_2, SPRECT_3, TOPREAL6, JORDAN8, MATRIX_0, JORDAN1A, FINSET_1, SPPOL_1, JORDAN1, JORDAN2C, NEWTON; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; definitions TARSKI, XBOOLE_0, GOBOARD5, SEQM_3; equalities XBOOLE_0; expansions TARSKI; theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, SPPOL_2, JORDAN3, FINSEQ_5, FINSEQ_6, GOBOARD7, TOPREAL1, XBOOLE_0, XBOOLE_1, ABSVALUE, FUNCT_1, FUNCT_2, GOBOARD9, FINSEQ_2, UNIFORM1, SUBSET_1, GOBRD11, SPRECT_3, CARD_1, RFINSEQ, GOBOARD6, TOPREAL3, TOPMETR, TOPS_1, JORDAN8, GOBRD13, SPRECT_4, CONNSP_1, GOBRD14, JORDAN9, JORDAN5B, JORDAN2C, PARTFUN2, RELSET_1, TBSP_1, JORDAN1H, JORDAN11, XREAL_0, ZFMISC_1, XREAL_1, XXREAL_0, PARTFUN1, MATRIX_0, NAT_D, SEQ_4, RLTOPSP1; schemes NAT_1, RECDEF_1; begin :: Spans reserve i, j, k, l, m, n, i1, i2, j1, j2 for Nat; definition let C be non vertical non horizontal non empty being_simple_closed_curve Subset of TOP-REAL 2, n be Nat; assume A1: n is_sufficiently_large_for C; func Span(C,n) -> clockwise_oriented standard non constant special_circular_sequence means it is_sequence_on Gauge(C,n) & it/.1 = Gauge(C ,n)*(X-SpanStart(C,n),Y-SpanStart(C,n)) & it/.2 = Gauge(C,n)*(X-SpanStart(C,n) -'1,Y-SpanStart(C,n)) & for k being Nat st 1 <= k & k+2 <= len it holds (front_right_cell(it,k,Gauge(C,n)) misses C & front_left_cell(it,k,Gauge( C,n)) misses C implies it turns_left k,Gauge(C,n)) & (front_right_cell(it,k, Gauge(C,n)) misses C & front_left_cell(it,k,Gauge(C,n)) meets C implies it goes_straight k,Gauge(C,n)) & (front_right_cell(it,k,Gauge(C,n)) meets C implies it turns_right k,Gauge(C,n)); existence proof set XS = X-SpanStart(C,n), YS = Y-SpanStart(C,n); set G = Gauge(C,n); A2: len G = 2|^n+3 by JORDAN8:def 1; defpred P[Nat,set,set] means ($1 = 0 implies $3 = <*G*( X-SpanStart(C,n),Y-SpanStart(C,n))*>) & ($1 = 1 implies $3 = <*G*(X-SpanStart(C ,n),Y-SpanStart(C,n)), G*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n))*>) & ($1 > 1 & $2 is FinSequence of TOP-REAL 2 implies for f being FinSequence of TOP-REAL 2 st $2 = f holds (len f = $1 implies (f is_sequence_on G & left_cell(f,len f-'1, G) meets C implies (front_right_cell(f,(len f)-'1,G) misses C & front_left_cell (f,(len f)-'1,G) misses C implies ex i,j st f^<*G*(i,j)*> turns_left (len f)-'1 ,G & $3 = f^<*G*(i,j)*>) & (front_right_cell(f,(len f)-'1,G) misses C & front_left_cell(f,(len f)-'1,G) meets C implies ex i,j st f^<*G*(i,j)*> goes_straight (len f)-'1,G & $3 = f^<*G*(i,j)*>) & (front_right_cell(f,(len f) -'1,G) meets C implies ex i,j st f^<*G*(i,j)*> turns_right (len f)-'1,G & $3 = f^<*G*(i,j)*>)) & (not f is_sequence_on G or left_cell(f,len f-'1,G) misses C implies $3 = f^<*G*(1,1)*>)) & (len f <> $1 implies $3 = {})) & ($1 > 1 & $2 is not FinSequence of TOP-REAL 2 implies $3 = {}); A3: 1+1 <= XS by JORDAN1H:49; A4: the TopStruct of TOP-REAL 2 = TopSpaceMetr (Euclid 2) by EUCLID:def 8; A5: [X-SpanStart(C,n),Y-SpanStart(C,n)] in Indices G by A1,JORDAN11:8; A6: len G = width G by JORDAN8:def 1; A7: for k being Nat, x being set ex y being set st P[k,x,y] proof let k be Nat, x be set; per cases by NAT_1:25; suppose A8: k=0; take <*G*(X-SpanStart(C,n),Y-SpanStart(C,n))*>; thus thesis by A8; end; suppose A9: k = 1; take <*G*(X-SpanStart(C,n),Y-SpanStart(C,n)), G*(X-SpanStart(C,n)-'1, Y-SpanStart(C,n))*>; thus thesis by A9; end; suppose that A10: k > 1 and A11: x is FinSequence of TOP-REAL 2; reconsider f = x as FinSequence of TOP-REAL 2 by A11; thus thesis proof per cases; suppose A12: len f = k; thus thesis proof per cases; suppose A13: f is_sequence_on G & left_cell(f,len f-'1,G) meets C; A14: (len f) -'1 +1 = len f by A10,A12,XREAL_1:235; then A15: (len f)-'1+(1+1) = (len f)+1; A16: (len f)-'1+1 in dom f by A10,A12,A14,FINSEQ_3:25; A17: 1 <= (len f)-'1 by A10,A12,NAT_D:49; then consider i1,j1,i2,j2 being Nat such that A18: [i1,j1] in Indices G and A19: f/.((len f)-'1) = G*(i1,j1) and A20: [i2,j2] in Indices G and A21: f/.((len f) -'1+1) = G*(i2,j2) and A22: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2 +1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A13,A14,JORDAN8:3; A23: i1 <= len G by A18,MATRIX_0:32; A24: 1 <= j2+1 by NAT_1:12; A25: 1 <= i2 by A20,MATRIX_0:32; A26: j1 <= width G by A18,MATRIX_0:32; A27: 1 <= i2+1 by NAT_1:12; A28: 1 <= j2 by A20,MATRIX_0:32; (len f)-'1 <= len f by NAT_D:35; then A29: (len f)-'1 in dom f by A17,FINSEQ_3:25; A30: j2 <= width G by A20,MATRIX_0:32; then A31: j2-'1 <= width G by NAT_D:44; A32: i2 <= len G by A20,MATRIX_0:32; then A33: i2-'1 <= len G by NAT_D:44; thus thesis proof per cases; suppose A34: front_right_cell(f,(len f)-'1,G) misses C & front_left_cell(f,(len f)-'1,G) misses C; thus thesis proof per cases by A22; suppose A35: i1 = i2 & j1+1 = j2; take f1 = f^<*G*(i2-'1,j2)*>; now take i=i2-'1 ,j=j2; now A36: now assume i2-'1 < 1; then i2 <= 1 by NAT_1:14,NAT_D:36; then i2 = 1 by A25,XXREAL_0:1; then cell(G,1-'1,j1) meets C by A13,A17,A14,A18,A19 ,A20,A21,A35,GOBRD13:21; then cell(G,0,j1) meets C by XREAL_1:232; hence contradiction by A6,A26,JORDAN8:18; end; let i19,j19,i29,j29 be Nat; assume that A37: [i19,j19] in Indices G and A38: [i29,j29] in Indices G and A39: f1/.((len f)-'1) = G*(i19,j19) and A40: f1/.((len f)-'1+1) = G*(i29,j29); A41: f/.((len f)-'1) = G*(i19,j19) by A29,A39, FINSEQ_4:68; A42: f/.((len f)-'1+1) = G*(i29,j29) by A16,A40, FINSEQ_4:68; then A43: j2 = j29 by A20,A21,A38,GOBOARD1:5; i2 = i29 by A20,A21,A38,A42,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1,j29) or i19+1 = i29 & j19 = j29 & [ i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19 = i29+1 & j19 = j29 & [i29,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29-'1) or i19 = i29 & j19 = j29+1 & [i29+1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29 +1,j29) by A18,A19,A28,A30,A33,A15,A35,A37,A41,A43,A36,FINSEQ_4:67,GOBOARD1:5 ,MATRIX_0:30; end; hence f1 turns_left (len f)-'1,G by GOBRD13:def 7; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A34; end; suppose A44: i1+1 = i2 & j1 = j2; take f1 = f^<*G*(i2,j2+1)*>; now take i=i2,j=j2+1; now A45: now assume j2+1 > len G; then A46: (len G)+1 <= j2+1 by NAT_1:13; j2+1 <= (len G)+1 by A6,A30,XREAL_1:6; then j2+1 = (len G)+1 by A46,XXREAL_0:1; then cell(G,i1,len G) meets C by A13,A17,A14,A18,A19 ,A20,A21,A44,GOBRD13:23; hence contradiction by A23,JORDAN8:15; end; let i19,j19,i29,j29 be Nat; assume that A47: [i19,j19] in Indices G and A48: [i29,j29] in Indices G and A49: f1/.((len f)-'1) = G*(i19,j19) and A50: f1/.((len f)-'1+1) = G*(i29,j29); A51: f/.((len f)-'1) = G*(i19,j19) by A29,A49, FINSEQ_4:68; A52: f/.((len f)-'1+1) = G*(i29,j29) by A16,A50, FINSEQ_4:68; then A53: j2 = j29 by A20,A21,A48,GOBOARD1:5; i2 = i29 by A20,A21,A48,A52,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1,j29) or i19+1 = i29 & j19 = j29 & [ i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19 = i29+1 & j19 = j29 & [i29,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29-'1) or i19 = i29 & j19 = j29+1 & [i29+1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29 +1,j29) by A6,A18,A19,A25,A32,A24,A15,A44,A47,A51,A53,A45,FINSEQ_4:67 ,GOBOARD1:5,MATRIX_0:30; end; hence f1 turns_left (len f)-'1,G by GOBRD13:def 7; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A34; end; suppose A54: i1 = i2+1 & j1 = j2; take f1 = f^<*G*(i2,j2-'1)*>; now take i=i2,j=j2-'1; now A55: now assume j2-'1 < 1; then j2 <= 1 by NAT_1:14,NAT_D:36; then j2 = 1 by A28,XXREAL_0:1; then cell(G,i2,1-'1) meets C by A13,A17,A14,A18,A19 ,A20,A21,A54,GOBRD13:25; then cell(G,i2,0) meets C by XREAL_1:232; hence contradiction by A32,JORDAN8:17; end; let i19,j19,i29,j29 be Nat; assume that A56: [i19,j19] in Indices G and A57: [i29,j29] in Indices G and A58: f1/.((len f)-'1) = G*(i19,j19) and A59: f1/.((len f)-'1+1) = G*(i29,j29); A60: f/.((len f)-'1) = G*(i19,j19) by A29,A58, FINSEQ_4:68; A61: f/.((len f)-'1+1) = G*(i29,j29) by A16,A59, FINSEQ_4:68; then A62: j2 = j29 by A20,A21,A57,GOBOARD1:5; i2 = i29 by A20,A21,A57,A61,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1,j29) or i19+1 = i29 & j19 = j29 & [ i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19 = i29+1 & j19 = j29 & [i29,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29-'1) or i19 = i29 & j19 = j29+1 & [i29+1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29 +1,j29) by A18,A19,A25,A32,A31,A15,A54,A56,A60,A62,A55,FINSEQ_4:67,GOBOARD1:5 ,MATRIX_0:30; end; hence f1 turns_left (len f)-'1,G by GOBRD13:def 7; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A34; end; suppose A63: i1 = i2 & j1 = j2+1; take f1 = f^<*G*(i2+1,j2)*>; now take i=i2+1 ,j=j2; now A64: now assume i2+1 > len G; then A65: (len G)+1 <= i2+1 by NAT_1:13; i2+1 <= (len G)+1 by A32,XREAL_1:6; then i2+1 = (len G)+1 by A65,XXREAL_0:1; then cell(G,len G,j2) meets C by A13,A17,A14,A18 ,A19,A20,A21,A63,GOBRD13:27; hence contradiction by A6,A30,JORDAN8:16; end; let i19,j19,i29,j29 be Nat; assume that A66: [i19,j19] in Indices G and A67: [i29,j29] in Indices G and A68: f1/.((len f)-'1) = G*(i19,j19) and A69: f1/.((len f)-'1+1) = G*(i29,j29); A70: f/.((len f)-'1) = G*(i19,j19) by A29,A68, FINSEQ_4:68; A71: f/.((len f)-'1+1) = G*(i29,j29) by A16,A69, FINSEQ_4:68; then A72: j2 = j29 by A20,A21,A67,GOBOARD1:5; i2 = i29 by A20,A21,A67,A71,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1,j29) or i19+1 = i29 & j19 = j29 & [ i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19 = i29+1 & j19 = j29 & [i29,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29-'1) or i19 = i29 & j19 = j29+1 & [i29+1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29 +1,j29) by A18,A19,A28,A30,A27,A15,A63,A66,A70,A72,A64,FINSEQ_4:67,GOBOARD1:5 ,MATRIX_0:30; end; hence f1 turns_left (len f)-'1,G by GOBRD13:def 7; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A34; end; end; end; suppose A73: front_right_cell(f,(len f)-'1,G) misses C & front_left_cell(f,(len f)-'1,G) meets C; thus thesis proof per cases by A22; suppose A74: i1 = i2 & j1+1 = j2; take f1 = f^<*G*(i2,j2+1)*>; now take i=i2,j=j2+1; now A75: now assume j2+1 > len G; then A76: (len G)+1 <= j2+1 by NAT_1:13; j2+1 <= (len G)+1 by A6,A30,XREAL_1:6; then j2+1 = (len G)+1 by A76,XXREAL_0:1; then cell(G,i1-'1,len G) meets C by A13,A17,A14 ,A18,A19,A20,A21,A73,A74,GOBRD13:34; hence contradiction by A23,JORDAN8:15,NAT_D:44; end; let i19,j19,i29,j29 be Nat; assume that A77: [i19,j19] in Indices G and A78: [i29,j29] in Indices G and A79: f1/.((len f)-'1) = G*(i19,j19) and A80: f1/.((len f)-'1+1) = G*(i29,j29); A81: f/.((len f)-'1) = G*(i19,j19) by A29,A79, FINSEQ_4:68; A82: f/.((len f)-'1+1) = G*(i29,j29) by A16,A80, FINSEQ_4:68; then A83: j2 = j29 by A20,A21,A78,GOBOARD1:5; i2 = i29 by A20,A21,A78,A82,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19+1 = i29 & j19 = j29 & [i29 +1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29+1,j29) or i19 = i29+1 & j19 = j29 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1,j29) or i19 = i29 & j19 = j29+1 & [i29,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29 -'1) by A6,A18,A19,A25,A32,A24,A15,A74,A77,A81,A83,A75,FINSEQ_4:67,GOBOARD1:5 ,MATRIX_0:30; end; hence f1 goes_straight (len f)-'1,G by GOBRD13:def 8; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A73; end; suppose A84: i1+1 = i2 & j1 = j2; take f1 = f^<*G*(i2+1,j2)*>; now take i=i2+1 ,j=j2; now A85: now assume i2+1 > len G; then A86: (len G)+1 <= i2+1 by NAT_1:13; i2+1 <= (len G)+1 by A32,XREAL_1:6; then i2+1 = (len G)+1 by A86,XXREAL_0:1; then cell(G,len G,j1) meets C by A13,A17,A14,A18 ,A19,A20,A21,A73,A84,GOBRD13:36; hence contradiction by A6,A26,JORDAN8:16; end; let i19,j19,i29,j29 be Nat; assume that A87: [i19,j19] in Indices G and A88: [i29,j29] in Indices G and A89: f1/.((len f)-'1) = G*(i19,j19) and A90: f1/.((len f)-'1+1) = G*(i29,j29); A91: f/.((len f)-'1) = G*(i19,j19) by A29,A89, FINSEQ_4:68; A92: f/.((len f)-'1+1) = G*(i29,j29) by A16,A90, FINSEQ_4:68; then A93: j2 = j29 by A20,A21,A88,GOBOARD1:5; i2 = i29 by A20,A21,A88,A92,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19+1 = i29 & j19 = j29 & [i29 +1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29+1,j29) or i19 = i29+1 & j19 = j29 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1,j29) or i19 = i29 & j19 = j29+1 & [i29,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29 -'1) by A18,A19,A28,A30,A27,A15,A84,A87,A91,A93,A85,FINSEQ_4:67,GOBOARD1:5 ,MATRIX_0:30; end; hence f1 goes_straight (len f)-'1,G by GOBRD13:def 8; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A73; end; suppose A94: i1 = i2+1 & j1 = j2; take f1 = f^<*G*(i2-'1,j2)*>; now take i=i2-'1 ,j=j2; now A95: now assume i2-'1 < 1; then i2 <= 1 by NAT_1:14,NAT_D:36; then i2 = 1 by A25,XXREAL_0:1; then cell(G,1-'1,j1-'1) meets C by A13,A17,A14 ,A18,A19,A20,A21,A73,A94,GOBRD13:38; then cell(G,0,j1-'1) meets C by XREAL_1:232; hence contradiction by A6,A26,JORDAN8:18,NAT_D:44 ; end; let i19,j19,i29,j29 be Nat; assume that A96: [i19,j19] in Indices G and A97: [i29,j29] in Indices G and A98: f1/.((len f)-'1) = G*(i19,j19) and A99: f1/.((len f)-'1+1) = G*(i29,j29); A100: f/.((len f)-'1) = G*(i19,j19) by A29,A98, FINSEQ_4:68; A101: f/.((len f)-'1+1) = G*(i29,j29) by A16,A99, FINSEQ_4:68; then A102: j2 = j29 by A20,A21,A97,GOBOARD1:5; i2 = i29 by A20,A21,A97,A101,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19+1 = i29 & j19 = j29 & [i29 +1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29+1,j29) or i19 = i29+1 & j19 = j29 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1,j29) or i19 = i29 & j19 = j29+1 & [i29,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29 -'1) by A18,A19,A28,A30,A33,A15,A94,A96,A100,A102,A95,FINSEQ_4:67,GOBOARD1:5 ,MATRIX_0:30; end; hence f1 goes_straight (len f)-'1,G by GOBRD13:def 8; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A73; end; suppose A103: i1 = i2 & j1 = j2+1; take f1 = f^<*G*(i2,j2-'1)*>; now take i=i2,j=j2-'1; now A104: now assume j2-'1 < 1; then j2 <= 1 by NAT_1:14,NAT_D:36; then j2 = 1 by A28,XXREAL_0:1; then cell(G,i1,1-'1) meets C by A13,A17,A14,A18 ,A19,A20,A21,A73,A103,GOBRD13:40; then cell(G,i1,0) meets C by XREAL_1:232; hence contradiction by A23,JORDAN8:17; end; let i19,j19,i29,j29 be Nat; assume that A105: [i19,j19] in Indices G and A106: [i29,j29] in Indices G and A107: f1/.((len f)-'1) = G*(i19,j19) and A108: f1/.((len f)-'1+1) = G*(i29,j29); A109: f/.((len f)-'1) = G*(i19,j19) by A29,A107, FINSEQ_4:68; A110: f/.((len f)-'1+1) = G*(i29,j29) by A16,A108, FINSEQ_4:68; then A111: j2 = j29 by A20,A21,A106,GOBOARD1:5; i2 = i29 by A20,A21,A106,A110,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19+1 = i29 & j19 = j29 & [i29 +1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29+1,j29) or i19 = i29+1 & j19 = j29 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1,j29) or i19 = i29 & j19 = j29+1 & [i29,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29 -'1) by A18,A19,A25,A32,A31,A15,A103,A105,A109,A111,A104,FINSEQ_4:67,GOBOARD1:5 ,MATRIX_0:30; end; hence f1 goes_straight (len f)-'1,G by GOBRD13:def 8; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A73; end; end; end; suppose A112: front_right_cell(f,(len f)-'1,G) meets C; thus thesis proof per cases by A22; suppose A113: i1 = i2 & j1+1 = j2; take f1 = f^<*G*(i2+1,j2)*>; now take i=i2+1 ,j=j2; now A114: now assume i2+1 > len G; then A115: (len G)+1 <= i2+1 by NAT_1:13; i2+1 <= (len G)+1 by A32,XREAL_1:6; then i2+1 = (len G)+1 by A115,XXREAL_0:1; then cell(G,len G,j2) meets C by A13,A17,A14,A18 ,A19,A20,A21,A112,A113,GOBRD13:35; hence contradiction by A6,A30,JORDAN8:16; end; let i19,j19,i29,j29 be Nat; assume that A116: [i19,j19] in Indices G and A117: [i29,j29] in Indices G and A118: f1/.((len f)-'1) = G*(i19,j19) and A119: f1/.((len f)-'1+1) = G*(i29,j29); A120: f/.((len f)-'1) = G*(i19,j19) by A29,A118, FINSEQ_4:68; A121: f/.((len f)-'1+1) = G*(i29,j29) by A16,A119, FINSEQ_4:68; then A122: j2 = j29 by A20,A21,A117,GOBOARD1:5; i2 = i29 by A20,A21,A117,A121,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29+1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29+1,j29) or i19+1 = i29 & j19 = j29 & [i29 ,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29-'1) or i19 = i29+1 & j19 = j29 & [i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19 = i29 & j19 = j29+1 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1, j29) by A18,A19,A28,A30,A27,A15,A113,A116,A120,A122,A114,FINSEQ_4:67,GOBOARD1:5 ,MATRIX_0:30; end; hence f1 turns_right (len f)-'1,G by GOBRD13:def 6; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A112; end; suppose A123: i1+1 = i2 & j1 = j2; take f1 = f^<*G*(i2,j2-'1)*>; now take i=i2,j=j2-'1; now A124: now assume j2-'1 < 1; then j2 <= 1 by NAT_1:14,NAT_D:36; then j2 = 1 by A28,XXREAL_0:1; then cell(G,i2,1-'1) meets C by A13,A17,A14,A18 ,A19,A20,A21,A112,A123,GOBRD13:37; then cell(G,i2,0) meets C by XREAL_1:232; hence contradiction by A32,JORDAN8:17; end; let i19,j19,i29,j29 be Nat; assume that A125: [i19,j19] in Indices G and A126: [i29,j29] in Indices G and A127: f1/.((len f)-'1) = G*(i19,j19) and A128: f1/.((len f)-'1+1) = G*(i29,j29); A129: f/.((len f)-'1) = G*(i19,j19) by A29,A127, FINSEQ_4:68; A130: f/.((len f)-'1+1) = G*(i29,j29) by A16,A128, FINSEQ_4:68; then A131: j2 = j29 by A20,A21,A126,GOBOARD1:5; i2 = i29 by A20,A21,A126,A130,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29+1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29+1,j29) or i19+1 = i29 & j19 = j29 & [i29 ,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29-'1) or i19 = i29+1 & j19 = j29 & [i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19 = i29 & j19 = j29+1 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1, j29) by A18,A19,A25,A32,A31,A15,A123,A125,A129,A131,A124,FINSEQ_4:67,GOBOARD1:5 ,MATRIX_0:30; end; hence f1 turns_right (len f)-'1,G by GOBRD13:def 6; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A112; end; suppose A132: i1 = i2+1 & j1 = j2; take f1 = f^<*G*(i2,j2+1)*>; now take i=i2,j=j2+1; now A133: now assume j2+1 > len G; then A134: (len G)+1 <= j2+1 by NAT_1:13; j2+1 <= (len G)+1 by A6,A30,XREAL_1:6; then j2+1 = (len G)+1 by A134,XXREAL_0:1; then cell(G,i2-'1,len G) meets C by A13,A17,A14 ,A18,A19,A20,A21,A112,A132,GOBRD13:39; hence contradiction by A32,JORDAN8:15,NAT_D:44; end; let i19,j19,i29,j29 be Nat; assume that A135: [i19,j19] in Indices G and A136: [i29,j29] in Indices G and A137: f1/.((len f)-'1) = G*(i19,j19) and A138: f1/.((len f)-'1+1) = G*(i29,j29); A139: f/.((len f)-'1) = G*(i19,j19) by A29,A137, FINSEQ_4:68; A140: f/.((len f)-'1+1) = G*(i29,j29) by A16,A138, FINSEQ_4:68; then A141: j2 = j29 by A20,A21,A136,GOBOARD1:5; i2 = i29 by A20,A21,A136,A140,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29+1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29+1,j29) or i19+1 = i29 & j19 = j29 & [i29 ,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29-'1) or i19 = i29+1 & j19 = j29 & [i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19 = i29 & j19 = j29+1 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1, j29) by A6,A18,A19,A25,A32,A24,A15,A132,A135,A139,A141,A133,FINSEQ_4:67 ,GOBOARD1:5,MATRIX_0:30; end; hence f1 turns_right (len f)-'1,G by GOBRD13:def 6; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A112; end; suppose A142: i1 = i2 & j1 = j2+1; take f1 = f^<*G*(i2-'1,j2)*>; now take i=i2-'1 ,j=j2; now A143: now assume i2-'1 < 1; then i2 <= 1 by NAT_1:14,NAT_D:36; then i2 = 1 by A25,XXREAL_0:1; then cell(G,1-'1,j2-'1) meets C by A13,A17,A14 ,A18,A19,A20,A21,A112,A142,GOBRD13:41; then cell(G,0,j2-'1) meets C by XREAL_1:232; hence contradiction by A6,A30,JORDAN8:18,NAT_D:44 ; end; let i19,j19,i29,j29 be Nat; assume that A144: [i19,j19] in Indices G and A145: [i29,j29] in Indices G and A146: f1/.((len f)-'1) = G*(i19,j19) and A147: f1/.((len f)-'1+1) = G*(i29,j29); A148: f/.((len f)-'1) = G*(i19,j19) by A29,A146, FINSEQ_4:68; A149: f/.((len f)-'1+1) = G*(i29,j29) by A16,A147, FINSEQ_4:68; then A150: j2 = j29 by A20,A21,A145,GOBOARD1:5; i2 = i29 by A20,A21,A145,A149,GOBOARD1:5; hence i19 = i29 & j19+1 = j29 & [i29+1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29+1,j29) or i19+1 = i29 & j19 = j29 & [i29 ,j29-'1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29-'1) or i19 = i29+1 & j19 = j29 & [i29,j29+1] in Indices G & f1/.(len f -'1+2) = G*(i29,j29+1) or i19 = i29 & j19 = j29+1 & [i29-'1,j29] in Indices G & f1/.(len f -'1+2) = G*(i29-'1, j29) by A18,A19,A28,A30,A33,A15,A142,A144,A148,A150,A143,FINSEQ_4:67,GOBOARD1:5 ,MATRIX_0:30; end; hence f1 turns_right (len f)-'1,G by GOBRD13:def 6; thus f1 = f^<*G*(i,j)*>; end; hence thesis by A10,A12,A13,A112; end; end; end; end; end; suppose A151: not f is_sequence_on G or left_cell(f,len f-'1,G) misses C; take f^<*G*(1,1)*>; thus thesis by A10,A12,A151; end; end; end; suppose A152: len f <> k; take {}; thus thesis by A10,A152; end; end; end; suppose A153: k > 1 & x is not FinSequence of TOP-REAL 2; take {}; thus thesis by A153; end; end; consider F being Function such that A154: dom F = NAT and A155: F.0 = {} and A156: for k being Nat holds P[k,F.k,F.(k+1)] from RECDEF_1:sch 1(A7); defpred P[Nat] means F.$1 is FinSequence of TOP-REAL 2; A157: {} = <*>(the carrier of TOP-REAL 2); A158: for k st P[k] holds P[k+1] proof let k such that A159: F.k is FinSequence of TOP-REAL 2; per cases by NAT_1:25; suppose k = 0; hence thesis by A156; end; suppose k = 1; hence thesis by A156; end; suppose A160: k > 1; reconsider f = F.k as FinSequence of TOP-REAL 2 by A159; per cases; suppose A161: len f = k; per cases; suppose A162: f is_sequence_on G & left_cell(f,len f-'1,G) meets C; then A163: front_right_cell(f,(len f)-'1,G) meets C implies ex i,j st f^<*G*(i,j )*> turns_right (len f)-'1,G & F.(k+1) = f^<*G*(i,j)*> by A156 ,A160,A161; A164: front_right_cell(f,(len f)-'1,G) misses C & front_left_cell(f,(len f) -'1,G) meets C implies ex i,j st f^<*G*(i,j)*> goes_straight (len f)-'1,G & F.( k+1) = f^<*G*(i,j)*> by A156,A160,A161,A162; front_right_cell(f,(len f)-'1,G) misses C & front_left_cell(f,(len f) -'1,G) misses C implies ex i,j st f^<*G*(i,j)*> turns_left (len f)-'1,G & F.(k+ 1) = f^<*G*(i,j)*> by A156,A160,A161,A162; hence thesis by A164,A163; end; suppose A165: not f is_sequence_on G or left_cell(f,len f-'1,G) misses C; f^<*G*(1,1)*> is FinSequence of TOP-REAL 2; hence thesis by A156,A160,A161,A165; end; end; suppose A166: len f <> k; thus thesis by A156,A157,A160,A166; end; end; end; A167: P[0] by A155,A157; A168: for k holds P[k] from NAT_1:sch 2(A167,A158); rng F c= (the carrier of TOP-REAL 2)* proof let y be object; assume y in rng F; then ex x being object st x in dom F & F.x = y by FUNCT_1:def 3; then y is FinSequence of TOP-REAL 2 by A154,A168; hence thesis by FINSEQ_1:def 11; end; then reconsider F as sequence of (the carrier of TOP-REAL 2)* by A154, FUNCT_2:def 1,RELSET_1:4; defpred P[Nat] means len(F.$1 qua FinSequence of TOP-REAL 2) = $1; A169: for k st P[k] holds P[k+1] proof let k such that A170: len(F.k) = k; A171: P[k,F.k,F.(k+1)] by A156; per cases by NAT_1:25; suppose k = 0; hence thesis by A171,FINSEQ_1:39; end; suppose k = 1; hence thesis by A171,FINSEQ_1:44; end; suppose A172: k > 1; thus thesis proof per cases; suppose A173: F.k is_sequence_on G & left_cell(F.k,len(F.k)-'1,G) meets C; then A174: front_right_cell(F.k,(len(F.k))-'1,G) meets C implies ex i,j st (F.k) ^<*G*(i,j)*> turns_right (len(F.k))-'1,G & F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A170,A172; A175: front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k, (len(F.k))-'1,G) meets C implies ex i,j st (F.k)^<*G*(i,j) *> goes_straight (len (F.k))-'1,G & F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A170 ,A172,A173; front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k, (len(F.k))-'1,G) misses C implies ex i,j st (F.k)^<*G*(i,j )*> turns_left (len(F .k))-'1,G & F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A170,A172 ,A173; hence thesis by A170,A175,A174,FINSEQ_2:16; end; suppose not F.k is_sequence_on G or left_cell(F.k,len(F.k)-'1,G) misses C; then F.(k+1) = (F.k)^<*G*(1,1)*> by A156,A170,A172; hence thesis by A170,FINSEQ_2:16; end; end; end; end; defpred Q[Nat] means F.$1 is_sequence_on G & for m st 1 <= m & m+1 <= len(F.$1) holds right_cell(F.$1,m,G) misses C & left_cell(F.$1,m,G) meets C; A176: P[0] by A155,CARD_1:27; A177: for k holds P[k] from NAT_1:sch 2(A176,A169); A178: 1 <= XS by JORDAN1H:49,XXREAL_0:2; A179: for k st Q[k] holds Q[k+1] proof let k such that A180: F.k is_sequence_on G and A181: for m st 1 <= m & m+1 <= len(F.k) holds right_cell(F.k,m,G) misses C & left_cell(F.k,m,G) meets C; A182: len(F.k) = k by A177; A183: len(F.(k+1)) = k+1 by A177; per cases by NAT_1:25; suppose A184: k = 0; then A185: F.(k+1) = <*G*(X-SpanStart(C,n),Y-SpanStart(C,n))*> by A156; A186: now let l; assume A187: l in dom(F.(k+1)); then A188: 1 <= l by FINSEQ_3:25; l <= 1 by A183,A184,A187,FINSEQ_3:25; then l = 1 by A188,XXREAL_0:1; hence ex i,j st [i,j] in Indices G & (F.(k+1))/.l = G*(i,j) by A5 ,A185,FINSEQ_4:16; end; now let l; assume that A189: l in dom(F.(k+1)) and A190: l+1 in dom(F.(k+1)); A191: 1 <= l by A189,FINSEQ_3:25; l <= 1 by A183,A184,A189,FINSEQ_3:25; then l = 1 by A191,XXREAL_0:1; hence for i1,j1,i2,j2 st [i1,j1] in Indices G & [i2,j2] in Indices G & (F.(k+1))/.l = G*(i1,j1) & (F.(k+1))/.(l+1) = G*(i2,j2) holds |.i1-i2.|+|.j1-j2.| = 1 by A183,A184,A190,FINSEQ_3:25; end; hence F.(k+1) is_sequence_on G by A186,GOBOARD1:def 9; let m; assume that A192: 1 <= m and A193: m+1 <= len(F.(k+1)); 1 <= m+1 by NAT_1:12; then m+1 = 0+1 by A183,A184,A193,XXREAL_0:1; hence thesis by A192; end; suppose A194: k = 1; A195: XS-'1 < XS by A178,JORDAN5B:1; A196: XS <= XS+1 by NAT_1:11; A197: [X-SpanStart(C,n),Y-SpanStart(C,n)] in Indices G by A1,JORDAN11:8; A198: F.(k+1) = <*G*(X-SpanStart(C,n),Y-SpanStart(C,n)), G*( X-SpanStart(C,n)-'1,Y-SpanStart(C,n))*> by A156,A194; then A199: (F.(k+1))/.1 = G*(X-SpanStart(C,n),Y-SpanStart(C,n)) by FINSEQ_4:17; A200: [X-SpanStart(C,n)-'1,Y-SpanStart(C,n)] in Indices G by A1,JORDAN11:9; A201: (F.(k+1))/.2 = G*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) by A198, FINSEQ_4:17; A202: now let l; assume that A203: l in dom(F.(k+1)) and A204: l+1 in dom(F.(k+1)); let i1,j1,i2,j2 be Nat such that A205: [i1,j1] in Indices G and A206: [i2,j2]in Indices G and A207: (F.(k+1))/.l = G*(i1,j1) and A208: (F.(k+1))/.(l+1) = G*(i2,j2); l <= 2 by A183,A194,A203,FINSEQ_3:25; then A209: l = 0 or ... or l = 2; then A210: i2 = XS-'1 by A183,A194,A201,A200,A203,A204,A206,A208,FINSEQ_3:25 ,GOBOARD1:5; A211: j1 = YS by A199,A201,A197,A200,A203,A209,A205,A207,FINSEQ_3:25 ,GOBOARD1:5; j2 = YS by A183,A194,A199,A201,A197,A200,A204,A209,A206,A208, FINSEQ_3:25,GOBOARD1:5; then A212: |.j1-j2.| = 0 by A211,ABSVALUE:def 1; i1 = XS by A183,A194,A199,A197,A203,A204,A209,A205,A207,FINSEQ_3:25 ,GOBOARD1:5; then i2+1 = i1 by A3,A210,NAT_D:43,55; hence |.i1-i2.|+|.j1-j2.| = 1 by A212,ABSVALUE:def 1; end; now let l; assume A213: l in dom(F.(k+1)); then l <= 2 by A183,A194,FINSEQ_3:25; then l = 0 or ... or l = 2; hence ex i,j st [i,j] in Indices G & (F.(k+1))/.l = G*(i,j) by A199 ,A201,A197,A200,A213,FINSEQ_3:25; end; hence A214: F.(k+1) is_sequence_on G by A202,GOBOARD1:def 9; let m; assume that A215: 1 <= m and A216: m+1 <= len(F.(k+1)); 1+1 <= m+1 by A215,XREAL_1:6; then A217: m+1 = 1+1 by A183,A194,A216,XXREAL_0:1; then right_cell(F.(k+1),m,G) = cell(G,XS-'1,YS) by A199,A201,A197,A200 ,A214,A216,A195,A196,GOBRD13:def 2; hence right_cell(F.(k+1),m,G) misses C by A1,JORDAN11:11; left_cell(F.(k+1),m,G) = cell(G,XS-'1,YS-'1) by A199,A201,A197,A200 ,A214,A216,A217,A195,A196,GOBRD13:def 3; hence thesis by A1,JORDAN11:10; end; suppose A218: k > 1; then A219: len(F.k) in dom(F.k) by A182,FINSEQ_3:25; A220: (len(F.k)) -'1 +1 = len(F.k) by A182,A218,XREAL_1:235; then A221: (len(F.k))-'1+(1+1) = (len(F.k))+1; A222: 1 <= (len(F.k))-'1 by A182,A218,NAT_D:49; then consider i1,j1,i2,j2 being Nat such that A223: [i1,j1] in Indices G and A224: (F.k)/.(len(F.k)-'1) = G*(i1,j1) and A225: [i2,j2] in Indices G and A226: (F.k)/.len(F.k) = G*(i2,j2) and i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A180,A220,JORDAN8:3; A227: front_left_cell(F.k,(len(F.k))-'1,G) meets C & i1 = i2+1 & j1 = j2 implies [i2-'1,j2] in Indices G by A180,A182,A218,A223,A224,A225,A226, JORDAN1H:58; i1+1+1 = i1+2; then A228: front_left_cell(F.k,(len(F.k))-'1,G) meets C & i1+1 = i2 & j1 = j2 implies [i2+1,j2] in Indices G by A180,A182,A218,A223,A224,A225,A226, JORDAN1H:57; j1+1+1 = j1+2; then A229: front_left_cell(F.k,(len(F.k))-'1,G) meets C & i1 = i2 & j1+1 = j2 implies [i1,j2+1] in Indices G by A180,A182,A218,A223,A224,A225,A226, JORDAN1H:56; A230: front_right_cell(F.k,(len(F.k))-'1,G) meets C & i1 = i2 & j1 = j2+1 implies [i2-'1,j2] in Indices G by A180,A182,A218,A223,A224,A225,A226, JORDAN1H:63; (len(F.k))-'1 <= len(F.k) by NAT_D:35; then A231: (len(F.k))-'1 in dom(F.k) by A222,FINSEQ_3:25; A232: front_right_cell(F.k,(len(F.k))-'1,G) meets C & i1 = i2+1 & j1 = j2 implies [i2,j2+1] in Indices G by A180,A182,A218,A223,A224,A225,A226, JORDAN1H:62; A233: front_right_cell(F.k,(len(F.k))-'1,G) meets C & i1+1 = i2 & j1 = j2 implies [i2,j2-'1] in Indices G by A180,A182,A218,A223,A224,A225,A226, JORDAN1H:61; A234: front_right_cell(F.k,(len(F.k))-'1,G) meets C & i1 = i2 & j1+1 = j2 implies [i2+1,j2] in Indices G by A180,A182,A218,A223,A224,A225,A226, JORDAN1H:60; A235: front_left_cell(F.k,(len(F.k))-'1,G) meets C & i1 = i2 & j1 = j2 +1 implies [i2,j2-'1] in Indices G by A180,A182,A218,A223,A224,A225,A226, JORDAN1H:59; A236: 1 <= j2 by A225,MATRIX_0:32; A237: left_cell(F.k,(len(F.k))-'1,G) meets C by A181,A222,A220; then A238: i1 = i2 & j1+1 = j2 implies [i1-'1,j1+1] in Indices G by A180,A182,A218 ,A223,A224,A225,A226,JORDAN1H:52; A239: i1 = i2 & j1 = j2+1 implies [i1+1,j2] in Indices G by A180,A182,A218 ,A223,A224,A225,A226,A237,JORDAN1H:55; A240: i1 = i2+1 & j1 = j2 implies [i2,j1-'1] in Indices G by A180,A182,A218 ,A223,A224,A225,A226,A237,JORDAN1H:54; A241: i1+1 = i2 & j1 = j2 implies [i1+1,j1+1] in Indices G by A180,A182,A218 ,A223,A224,A225,A226,A237,JORDAN1H:53; A242: 1 <= i2 by A225,MATRIX_0:32; thus A243: F.(k+1) is_sequence_on G proof per cases; suppose front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k))-'1,G) misses C; then consider i,j such that A244: (F.k)^<*G*(i,j)*> turns_left (len(F.k))-'1,G and A245: F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A180,A182,A218,A237; set f = (F.k)^<*G*(i,j)*>; A246: f/.(len(F.k)+1) = G*(i,j) by FINSEQ_4:67; A247: f/.len(F.k) = G*(i2,j2) by A226,A219,FINSEQ_4:68; A248: f/.(len(F.k)-'1) = G*(i1,j1) by A224,A231,FINSEQ_4:68; thus thesis proof per cases by A220,A223,A225,A221,A244,A248,A247,GOBRD13:def 7; suppose that A249: i1 = i2 & j1+1 = j2 and A250: f/.(len(F.k)+1) = G*(i2-'1,j2); now let i19,j19,i29,j29 be Nat; assume that A251: [i19,j19] in Indices G and A252: [i29,j29] in Indices G and A253: (F.k)/.len(F.k) = G*(i19,j19) and A254: G*(i2-'1,j2) = G*(i29,j29); A255: i2-'1 = i29 by A238,A249,A252,A254,GOBOARD1:5; i2 = i19 by A225,A226,A251,A253,GOBOARD1:5; then i19-i29 = i2-(i2-1) by A242,A255,XREAL_1:233; then A256: |.i19-i29.| = 1 by ABSVALUE:def 1; A257: j2 = j29 by A238,A249,A252,A254,GOBOARD1:5; j2 = j19 by A225,A226,A251,A253,GOBOARD1:5; then |.j29-j19.| = 0 by A257,ABSVALUE:def 1; hence |.i29-i19.|+|.j29-j19.| = 1 by A256,UNIFORM1:11; end; hence thesis by A180,A182,A218,A238,A245,A246,A249,A250, CARD_1:27,JORDAN8:6; end; suppose that A258: i1+1 = i2 & j1 = j2 and A259: f/.(len(F.k)+1) = G*(i2,j2+1); now let i19,j19,i29,j29 be Nat; assume that A260: [i19,j19] in Indices G and A261: [i29,j29] in Indices G and A262: (F.k)/.len(F.k) = G*(i19,j19) and A263: G*(i2,j2+1) = G*(i29,j29); A264: i2 = i29 by A241,A258,A261,A263,GOBOARD1:5; i2 = i19 by A225,A226,A260,A262,GOBOARD1:5; then A265: |.i29-i19.| = 0 by A264,ABSVALUE:def 1; A266: j2+1 = j29 by A241,A258,A261,A263,GOBOARD1:5; j2 = j19 by A225,A226,A260,A262,GOBOARD1:5; hence |.i29-i19.|+|.j29-j19.| = 1 by A266,A265, ABSVALUE:def 1; end; hence thesis by A180,A182,A218,A241,A245,A246,A258,A259, CARD_1:27,JORDAN8:6; end; suppose that A267: i1 = i2+1 & j1 = j2 and A268: f/.(len(F.k)+1) = G*(i2,j2-'1); now let i19,j19,i29,j29 be Nat; assume that A269: [i19,j19] in Indices G and A270: [i29,j29] in Indices G and A271: (F.k)/.len(F.k) = G*(i19,j19) and A272: G*(i2,j2-'1) = G*(i29,j29); A273: j2-'1 = j29 by A240,A267,A270,A272,GOBOARD1:5; j2 = j19 by A225,A226,A269,A271,GOBOARD1:5; then j19-j29 = j2-(j2-1) by A236,A273,XREAL_1:233; then A274: |.j19-j29.| = 1 by ABSVALUE:def 1; A275: i2 = i29 by A240,A267,A270,A272,GOBOARD1:5; i2 = i19 by A225,A226,A269,A271,GOBOARD1:5; then |.i29-i19.| = 0 by A275,ABSVALUE:def 1; hence |.i29-i19.|+|.j29-j19.| = 1 by A274,UNIFORM1:11; end; hence thesis by A180,A182,A218,A240,A245,A246,A267,A268, CARD_1:27,JORDAN8:6; end; suppose that A276: i1 = i2 & j1 = j2+1 and A277: f/.(len(F.k)+1) = G*(i2+1,j2); now let i19,j19,i29,j29 be Nat; assume that A278: [i19,j19] in Indices G and A279: [i29,j29] in Indices G and A280: (F.k)/.len(F.k) = G*(i19,j19) and A281: G*(i2+1,j2) = G*(i29,j29); A282: j2 = j29 by A239,A276,A279,A281,GOBOARD1:5; j2 = j19 by A225,A226,A278,A280,GOBOARD1:5; then A283: |.j29-j19.| = 0 by A282,ABSVALUE:def 1; A284: i2+1 = i29 by A239,A276,A279,A281,GOBOARD1:5; i2 = i19 by A225,A226,A278,A280,GOBOARD1:5; hence |.i29-i19.|+|.j29-j19.| = 1 by A284,A283, ABSVALUE:def 1; end; hence thesis by A180,A182,A218,A239,A245,A246,A276,A277, CARD_1:27,JORDAN8:6; end; end; end; suppose A285: front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k))-'1,G) meets C; then consider i,j such that A286: (F.k)^<*G*(i,j)*> goes_straight (len(F.k))-'1,G and A287: F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A180,A182,A218,A237; set f = (F.k)^<*G*(i,j)*>; A288: f/.(len(F.k)+1) = G*(i,j) by FINSEQ_4:67; A289: f/.len(F.k) = G*(i2,j2) by A226,A219,FINSEQ_4:68; A290: f/.(len(F.k)-'1) = G*(i1,j1) by A224,A231,FINSEQ_4:68; thus thesis proof per cases by A220,A223,A225,A221,A286,A290,A289,GOBRD13:def 8; suppose that A291: i1 = i2 & j1+1 = j2 and A292: f/.(len(F.k)+1) = G*(i2,j2+1); now let i19,j19,i29,j29 be Nat; assume that A293: [i19,j19] in Indices G and A294: [i29,j29] in Indices G and A295: (F.k)/.len(F.k) = G*(i19,j19) and A296: G*(i2,j2+1) = G*(i29,j29); A297: i2 = i19 by A225,A226,A293,A295,GOBOARD1:5; i2 = i29 by A229,A285,A291,A294,A296,GOBOARD1:5; then A298: |.i29-i19.| = 0 by A297,ABSVALUE:def 1; A299: j2 = j19 by A225,A226,A293,A295,GOBOARD1:5; j2+1 = j29 by A229,A285,A291,A294,A296,GOBOARD1:5; hence |.i29-i19.|+|.j29-j19.| = 1 by A299,A298, ABSVALUE:def 1; end; hence thesis by A180,A182,A218,A229,A285,A287,A288,A291,A292, CARD_1:27,JORDAN8:6; end; suppose that A300: i1+1 = i2 & j1 = j2 and A301: f/.(len(F.k)+1) = G*(i2+1,j2); now let i19,j19,i29,j29 be Nat; assume that A302: [i19,j19] in Indices G and A303: [i29,j29] in Indices G and A304: (F.k)/.len(F.k) = G*(i19,j19) and A305: G*(i2+1,j2) = G*(i29,j29); A306: j2 = j19 by A225,A226,A302,A304,GOBOARD1:5; j2 = j29 by A228,A285,A300,A303,A305,GOBOARD1:5; then A307: |.j29-j19.| = 0 by A306,ABSVALUE:def 1; A308: i2 = i19 by A225,A226,A302,A304,GOBOARD1:5; i2+1 = i29 by A228,A285,A300,A303,A305,GOBOARD1:5; hence |.i29-i19.|+|.j29-j19.| = 1 by A308,A307, ABSVALUE:def 1; end; hence thesis by A180,A182,A218,A228,A285,A287,A288,A300,A301, CARD_1:27,JORDAN8:6; end; suppose that A309: i1 = i2+1 & j1 = j2 and A310: f/.(len(F.k)+1) = G*(i2-'1,j2); now let i19,j19,i29,j29 be Nat; assume that A311: [i19,j19] in Indices G and A312: [i29,j29] in Indices G and A313: (F.k)/.len(F.k) = G*(i19,j19) and A314: G*(i2-'1,j2) = G*(i29,j29); A315: i2 = i19 by A225,A226,A311,A313,GOBOARD1:5; i2-'1 = i29 by A227,A285,A309,A312,A314,GOBOARD1:5; then i19-i29 = i2-(i2-1) by A242,A315,XREAL_1:233; then A316: |.i19-i29.| = 1 by ABSVALUE:def 1; A317: j2 = j19 by A225,A226,A311,A313,GOBOARD1:5; j2 = j29 by A227,A285,A309,A312,A314,GOBOARD1:5; then |.j29-j19.| = 0 by A317,ABSVALUE:def 1; hence |.i29-i19.|+|.j29-j19.| = 1 by A316,UNIFORM1:11; end; hence thesis by A180,A182,A218,A227,A285,A287,A288,A309,A310, CARD_1:27,JORDAN8:6; end; suppose that A318: i1 = i2 & j1 = j2+1 and A319: f/.(len(F.k)+1) = G*(i2,j2-'1); now let i19,j19,i29,j29 be Nat; assume that A320: [i19,j19] in Indices G and A321: [i29,j29] in Indices G and A322: (F.k)/.len(F.k) = G*(i19,j19) and A323: G*(i2,j2-'1) = G*(i29,j29); A324: j2 = j19 by A225,A226,A320,A322,GOBOARD1:5; j2-'1 = j29 by A235,A285,A318,A321,A323,GOBOARD1:5; then j19-j29 = j2-(j2-1) by A236,A324,XREAL_1:233; then A325: |.j19-j29.| = 1 by ABSVALUE:def 1; A326: i2 = i19 by A225,A226,A320,A322,GOBOARD1:5; i2 = i29 by A235,A285,A318,A321,A323,GOBOARD1:5; then |.i29-i19.| = 0 by A326,ABSVALUE:def 1; hence |.i29-i19.|+|.j29-j19.| = 1 by A325,UNIFORM1:11; end; hence thesis by A180,A182,A218,A235,A285,A287,A288,A318,A319, CARD_1:27,JORDAN8:6; end; end; end; suppose A327: front_right_cell(F.k,(len(F.k))-'1,G) meets C; then consider i,j such that A328: (F.k)^<*G*(i,j)*> turns_right (len(F.k))-'1,G and A329: F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A180,A182,A218,A237; set f = (F.k)^<*G*(i,j)*>; A330: f/.(len(F.k)+1) = G*(i,j) by FINSEQ_4:67; A331: f/.len(F.k) = G*(i2,j2) by A226,A219,FINSEQ_4:68; A332: f/.(len(F.k)-'1) = G*(i1,j1) by A224,A231,FINSEQ_4:68; thus thesis proof per cases by A220,A223,A225,A221,A328,A332,A331,GOBRD13:def 6; suppose that A333: i1 = i2 & j1+1 = j2 and A334: f/.(len(F.k)+1) = G*(i2+1,j2); now let i19,j19,i29,j29 be Nat; assume that A335: [i19,j19] in Indices G and A336: [i29,j29] in Indices G and A337: (F.k)/.len(F.k) = G*(i19,j19) and A338: G*(i2+1,j2) = G*(i29,j29); A339: j2 = j19 by A225,A226,A335,A337,GOBOARD1:5; j2 = j29 by A234,A327,A333,A336,A338,GOBOARD1:5; then A340: |.j29-j19.| = 0 by A339,ABSVALUE:def 1; A341: i2 = i19 by A225,A226,A335,A337,GOBOARD1:5; i2+1 = i29 by A234,A327,A333,A336,A338,GOBOARD1:5; hence |.i29-i19.|+|.j29-j19.| = 1 by A341,A340, ABSVALUE:def 1; end; hence thesis by A180,A182,A218,A234,A327,A329,A330,A333,A334, CARD_1:27,JORDAN8:6; end; suppose that A342: i1+1 = i2 & j1 = j2 and A343: f/.(len(F.k)+1) = G*(i2,j2-'1); now let i19,j19,i29,j29 be Nat; assume that A344: [i19,j19] in Indices G and A345: [i29,j29] in Indices G and A346: (F.k)/.len(F.k) = G*(i19,j19) and A347: G*(i2,j2-'1) = G*(i29,j29); A348: j2 = j19 by A225,A226,A344,A346,GOBOARD1:5; j2-'1 = j29 by A233,A327,A342,A345,A347,GOBOARD1:5; then j19-j29 = j2-(j2-1) by A236,A348,XREAL_1:233; then A349: |.j19-j29.| = 1 by ABSVALUE:def 1; A350: i2 = i19 by A225,A226,A344,A346,GOBOARD1:5; i2 = i29 by A233,A327,A342,A345,A347,GOBOARD1:5; then |.i29-i19.| = 0 by A350,ABSVALUE:def 1; hence |.i29-i19.|+|.j29-j19.| = 1 by A349,UNIFORM1:11; end; hence thesis by A180,A182,A218,A233,A327,A329,A330,A342,A343, CARD_1:27,JORDAN8:6; end; suppose that A351: i1 = i2+1 & j1 = j2 and A352: f/.(len(F.k)+1) = G*(i2,j2+1); now let i19,j19,i29,j29 be Nat; assume that A353: [i19,j19] in Indices G and A354: [i29,j29] in Indices G and A355: (F.k)/.len(F.k) = G*(i19,j19) and A356: G*(i2,j2+1) = G*(i29,j29); A357: i2 = i19 by A225,A226,A353,A355,GOBOARD1:5; i2 = i29 by A232,A327,A351,A354,A356,GOBOARD1:5; then A358: |.i29-i19.| = 0 by A357,ABSVALUE:def 1; A359: j2 = j19 by A225,A226,A353,A355,GOBOARD1:5; j2+1 = j29 by A232,A327,A351,A354,A356,GOBOARD1:5; hence |.i29-i19.|+|.j29-j19.| = 1 by A359,A358, ABSVALUE:def 1; end; hence thesis by A180,A182,A218,A232,A327,A329,A330,A351,A352, CARD_1:27,JORDAN8:6; end; suppose that A360: i1 = i2 & j1 = j2+1 and A361: f/.(len(F.k)+1) = G*(i2-'1,j2); now let i19,j19,i29,j29 be Nat; assume that A362: [i19,j19] in Indices G and A363: [i29,j29] in Indices G and A364: (F.k)/.len(F.k) = G*(i19,j19) and A365: G*(i2-'1,j2) = G*(i29,j29); A366: i2 = i19 by A225,A226,A362,A364,GOBOARD1:5; i2-'1 = i29 by A230,A327,A360,A363,A365,GOBOARD1:5; then i19-i29 = i2-(i2-1) by A242,A366,XREAL_1:233; then A367: |.i19-i29.| = 1 by ABSVALUE:def 1; A368: j2 = j19 by A225,A226,A362,A364,GOBOARD1:5; j2 = j29 by A230,A327,A360,A363,A365,GOBOARD1:5; then |.j29-j19.| = 0 by A368,ABSVALUE:def 1; hence |.i29-i19.|+|.j29-j19.| = 1 by A367,UNIFORM1:11; end; hence thesis by A180,A182,A218,A230,A327,A329,A330,A360,A361, CARD_1:27,JORDAN8:6; end; end; end; end; let m such that A369: 1 <= m and A370: m+1 <= len(F.(k+1)); A371: right_cell(F.k,(len(F.k))-'1,G) misses C by A181,A222,A220; now per cases; suppose A372: m+1 = len(F.(k+1)); A373: (j2-'1)+1 = j2 by A236,XREAL_1:235; A374: (i2-'1)+1 = i2 by A242,XREAL_1:235; thus thesis proof per cases; suppose A375: front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k))-'1,G) misses C; then A376: ex i,j st (F.k)^<*G*(i,j)*> turns_left (len(F.k))-'1,G & F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A180,A182,A218,A237; then A377: (F.(k+1))/.len(F.k) = G*(i2,j2) by A226,A219,FINSEQ_4:68; A378: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) by A224,A231,A376, FINSEQ_4:68; now per cases by A220,A223,A225,A221,A376,A378,A377,GOBRD13:def 7 ; suppose that A379: i1 = i2 & j1+1 = j2 and A380: (F.(k+1))/.(len(F.k)+1) = G*(i2-'1,j2); front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i1-'1, j2) by A180,A222,A220,A223,A224,A225,A226,A379,GOBRD13:34; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A238,A243,A369,A372,A374,A375,A377,A379,A380,GOBRD13:26; A381: j2-'1 = j1 by A379,NAT_D:34; cell(G,i1-'1,j1) meets C by A180,A222,A220,A223,A224,A225 ,A226,A237,A379,GOBRD13:21; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A238,A243 ,A369,A372,A374,A377,A379,A380,A381,GOBRD13:25; end; suppose that A382: i1+1 = i2 & j1 = j2 and A383: (F.(k+1))/.(len(F.k)+1) = G*(i2,j2+1); front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2) by A180,A222,A220,A223,A224,A225,A226,A382,GOBRD13:36; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A241,A243,A369,A372,A375,A377,A382,A383,GOBRD13:22; A384: i1+1-'1 = i1 by NAT_D:34; cell(G,i1,j1) meets C by A180,A222,A220,A223,A224,A225,A226 ,A237,A382,GOBRD13:23; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A241,A243 ,A369,A372,A377,A382,A383,A384,GOBRD13:21; end; suppose that A385: i1 = i2+1 & j1 = j2 and A386: (F.(k+1))/.(len(F.k)+1) = G*(i2,j2-'1); front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i2-'1, j2-'1) by A180,A222,A220,A223,A224,A225,A226,A385,GOBRD13:38; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A240,A243,A369,A372,A373,A375,A377,A385,A386,GOBRD13:28; cell(G,i2,j2-'1) meets C by A180,A222,A220,A223,A224,A225 ,A226,A237,A385,GOBRD13:25; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A240,A243 ,A369,A372,A373,A377,A385,A386,GOBRD13:27; end; suppose that A387: i1 = i2 & j1 = j2+1 and A388: (F.(k+1))/.(len(F.k)+1) = G*(i2+1,j2); front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2 -'1) by A180,A222,A220,A223,A224,A225,A226,A387,GOBRD13:40; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A239,A243,A369,A372,A375,A377,A387,A388,GOBRD13:24; cell(G,i2,j2) meets C by A180,A222,A220,A223,A224,A225,A226 ,A237,A387,GOBRD13:27; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A239,A243 ,A369,A372,A377,A387,A388,GOBRD13:23; end; end; hence thesis; end; suppose A389: front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k))-'1,G) meets C; then A390: ex i,j st (F.k)^<*G*(i,j)*> goes_straight (len(F.k))-'1 ,G & F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A180,A182,A218,A237; then A391: (F.(k+1))/.len(F.k) = G*(i2,j2) by A226,A219,FINSEQ_4:68; A392: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) by A224,A231,A390, FINSEQ_4:68; now per cases by A220,A223,A225,A221,A390,A392,A391,GOBRD13:def 8 ; suppose that A393: i1 = i2 & j1+1 = j2 and A394: (F.(k+1))/.(len(F.k)+1) = G*(i2,j2+1); front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i1,j2 ) by A180,A222,A220,A223,A224,A225,A226,A393,GOBRD13:35; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A229,A243,A369,A372,A389,A391,A393,A394,GOBRD13:22; front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i1-'1, j2) by A180,A222,A220,A223,A224,A225,A226,A393,GOBRD13:34; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A229,A243 ,A369,A372,A389,A391,A393,A394,GOBRD13:21; end; suppose that A395: i1+1 = i2 & j1 = j2 and A396: (F.(k+1))/.(len(F.k)+1) = G*(i2+1,j2); front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2 -'1) by A180,A222,A220,A223,A224,A225,A226,A395,GOBRD13:37; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A228,A243,A369,A372,A389,A391,A395,A396,GOBRD13:24; front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2) by A180,A222,A220,A223,A224,A225,A226,A395,GOBRD13:36; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A228,A243 ,A369,A372,A389,A391,A395,A396,GOBRD13:23; end; suppose that A397: i1 = i2+1 & j1 = j2 and A398: (F.(k+1))/.(len(F.k)+1) = G*(i2-'1,j2); front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2-'1 ,j2) by A180,A222,A220,A223,A224,A225,A226,A397,GOBRD13:39; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A227,A243,A369,A372,A374,A389,A391,A397,A398,GOBRD13:26; front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i2-'1, j2-'1) by A180,A222,A220,A223,A224,A225,A226,A397,GOBRD13:38; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A227,A243 ,A369,A372,A374,A389,A391,A397,A398,GOBRD13:25; end; suppose that A399: i1 = i2 & j1 = j2+1 and A400: (F.(k+1))/.(len(F.k)+1) = G*(i2,j2-'1); front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2-'1 ,j2-'1 ) by A180,A222,A220,A223,A224,A225,A226,A399,GOBRD13:41; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A235,A243,A369,A372,A373,A389,A391,A399,A400,GOBRD13:28; front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2 -'1) by A180,A222,A220,A223,A224,A225,A226,A399,GOBRD13:40; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A235,A243 ,A369,A372,A373,A389,A391,A399,A400,GOBRD13:27; end; end; hence thesis; end; suppose A401: front_right_cell(F.k,(len(F.k))-'1,G) meets C; then A402: ex i,j st (F.k)^<*G*(i,j)*> turns_right (len(F.k))-'1,G & F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A180,A182,A218,A237; then A403: (F.(k+1))/.len(F.k) = G*(i2,j2) by A226,A219,FINSEQ_4:68; A404: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) by A224,A231,A402, FINSEQ_4:68; now per cases by A220,A223,A225,A221,A402,A404,A403,GOBRD13:def 6 ; suppose that A405: i1 = i2 & j1+1 = j2 and A406: (F.(k+1))/.(len(F.k)+1) = G*(i2+1,j2); A407: j2 -'1 = j1 by A405,NAT_D:34; cell(G,i1,j1) misses C by A180,A222,A220,A223,A224,A225 ,A226,A371,A405,GOBRD13:22; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A234,A243,A369,A372,A401,A403,A405,A406,A407,GOBRD13:24; front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2 ) by A180,A222,A220,A223,A224,A225,A226,A405,GOBRD13:35; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A234,A243 ,A369,A372,A401,A403,A405,A406,GOBRD13:23; end; suppose that A408: i1+1 = i2 & j1 = j2 and A409: (F.(k+1))/.(len(F.k)+1) = G*(i2,j2-'1); A410: i2 -'1 = i1 by A408,NAT_D:34; cell(G,i1,j1-'1) misses C by A180,A222,A220,A223,A224,A225 ,A226,A371,A408,GOBRD13:24; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A233,A243,A369,A372,A373,A401,A403,A408,A409,A410,GOBRD13:28; front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2 -'1) by A180,A222,A220,A223,A224,A225,A226,A408,GOBRD13:37; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A233,A243 ,A369,A372,A373,A401,A403,A408,A409,GOBRD13:27; end; suppose that A411: i1 = i2+1 & j1 = j2 and A412: (F.(k+1))/.(len(F.k)+1) = G*(i2,j2+1); cell(G,i2,j2) misses C by A180,A222,A220,A223,A224,A225 ,A226,A371,A411,GOBRD13:26; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A232,A243,A369,A372,A401,A403,A411,A412,GOBRD13:22; front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2-'1 ,j2) by A180,A222,A220,A223,A224,A225,A226,A411,GOBRD13:39; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A232,A243 ,A369,A372,A401,A403,A411,A412,GOBRD13:21; end; suppose that A413: i1 = i2 & j1 = j2+1 and A414: (F.(k+1))/.(len(F.k)+1) = G*(i2-'1,j2); cell(G,i2-'1,j2) misses C by A180,A222,A220,A223,A224,A225 ,A226,A371,A413,GOBRD13:28; hence right_cell(F.(k+1),m,G) misses C by A182,A183,A225 ,A230,A243,A369,A372,A374,A401,A403,A413,A414,GOBRD13:26; front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2-'1 ,j2-'1 ) by A180,A222,A220,A223,A224,A225,A226,A413,GOBRD13:41; hence left_cell(F.(k+1),m,G) meets C by A182,A183,A225,A230,A243 ,A369,A372,A374,A401,A403,A413,A414,GOBRD13:25; end; end; hence thesis; end; end; end; suppose m+1 <> len(F.(k+1)); then m+1 < len(F.(k+1)) by A370,XXREAL_0:1; then A415: m+1 <= len(F.k)by A182,A183,NAT_1:13; then consider i1,j1,i2,j2 being Nat such that A416: [i1,j1] in Indices G and A417: (F.k)/.m = G*(i1,j1) and A418: [i2,j2] in Indices G and A419: (F.k)/.(m+1) = G*(i2,j2) and A420: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A180,A369,JORDAN8:3; A421: right_cell(F.k,m,G) misses C by A181,A369,A415; A422: now per cases; suppose front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k))-'1,G) misses C; then consider i,j such that (F.k)^<*G*(i,j)*> turns_left (len(F.k))-'1,G and A423: F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A180,A182,A218,A237; take i,j; thus F.(k+1) = (F.k)^<*G*(i,j)*> by A423; end; suppose front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k))-'1,G) meets C; then consider i,j such that (F.k)^<*G*(i,j)*> goes_straight (len(F.k))-'1,G and A424: F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A180,A182,A218,A237; take i,j; thus F.(k+1) = (F.k)^<*G*(i,j)*> by A424; end; suppose front_right_cell(F.k,(len(F.k))-'1,G) meets C; then consider i,j such that (F.k)^<*G*(i,j)*> turns_right (len(F.k))-'1,G and A425: F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A180,A182,A218,A237; take i,j; thus F.(k+1) = (F.k)^<*G*(i,j)*> by A425; end; end; 1 <= m+1 by NAT_1:12; then m+1 in dom(F.k) by A415,FINSEQ_3:25; then A426: (F.(k+1))/.(m+1) = G*(i2,j2) by A419,A422,FINSEQ_4:68; A427: left_cell(F.k,m,G) meets C by A181,A369,A415; m <= len(F.k) by A415,NAT_1:13; then m in dom(F.k) by A369,FINSEQ_3:25; then A428: (F.(k+1))/.m = G*(i1,j1) by A417,A422,FINSEQ_4:68; now per cases by A420; suppose A429: i1 = i2 & j1+1 = j2; then A430: right_cell(F.k,m,G) = cell(G,i1,j1) by A180,A369,A415,A416,A417 ,A418,A419,GOBRD13:22; left_cell(F.k,m,G) = cell(G,i1-'1,j1) by A180,A369,A415,A416 ,A417,A418,A419,A429,GOBRD13:21; hence thesis by A243,A369,A370,A416,A418,A421,A427,A428,A426 ,A429,A430,GOBRD13:21,22; end; suppose A431: i1+1 = i2 & j1 = j2; then A432: right_cell(F.k,m,G) = cell(G,i1,j1-'1) by A180,A369,A415,A416 ,A417,A418,A419,GOBRD13:24; left_cell(F.k,m,G) = cell(G,i1,j1) by A180,A369,A415,A416,A417 ,A418,A419,A431,GOBRD13:23; hence thesis by A243,A369,A370,A416,A418,A421,A427,A428,A426 ,A431,A432,GOBRD13:23,24; end; suppose A433: i1 = i2+1 & j1 = j2; then A434: right_cell(F.k,m,G) = cell(G,i2,j2) by A180,A369,A415,A416,A417 ,A418,A419,GOBRD13:26; left_cell(F.k,m,G) = cell(G,i2,j2-'1) by A180,A369,A415,A416 ,A417,A418,A419,A433,GOBRD13:25; hence thesis by A243,A369,A370,A416,A418,A421,A427,A428,A426 ,A433,A434,GOBRD13:25,26; end; suppose A435: i1 = i2 & j1 = j2+1; then A436: right_cell(F.k,m,G) = cell(G,i1-'1,j2) by A180,A369,A415,A416 ,A417,A418,A419,GOBRD13:28; left_cell(F.k,m,G) = cell(G,i2,j2) by A180,A369,A415,A416,A417 ,A418,A419,A435,GOBRD13:27; hence thesis by A243,A369,A370,A416,A418,A421,A427,A428,A426 ,A435,A436,GOBRD13:27,28; end; end; hence thesis; end; end; hence thesis; end; end; A437: Q[0] proof A438: for n st n in dom(F.0) & n+1 in dom(F.0) holds for m,k,i,j st [m,k ] in Indices G & [i,j] in Indices G & (F.0)/.n = G*(m,k) & (F.0)/.(n+1) = G*(i, j) holds |.m-i.|+|.k-j.| = 1 by A155; for n st n in dom(F.0) ex i,j st [i,j] in Indices G & (F.0)/.n = G *(i,j) by A155; hence F.0 is_sequence_on G by A438,GOBOARD1:def 9; let m; assume that 1 <= m and A439: m+1 <= len(F.0); thus thesis by A155,A439,CARD_1:27; end; A440: for k holds Q[k] from NAT_1:sch 2(A437,A179); A441: for k,i1,i2,j1,j2 st k > 1 & [i1,j1] in Indices G & (F.k)/.(len(F.k) -'1) = G*(i1,j1) & [i2,j2] in Indices G & (F.k)/.len(F.k) = G*(i2,j2) holds ( front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k)) -'1,G) misses C implies F.(k+1) turns_left (len(F.k))-'1,G & (i1 = i2 & j1+1 = j2 implies [i2-'1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2-'1,j2)*>) & (i1+1 = i2 & j1 = j2 implies [i2,j2+1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2+1)*> ) & (i1 = i2+1 & j1 = j2 implies [i2,j2-'1] in Indices G & F.(k+1) = (F.k)^<*G* (i2,j2-'1)*>)& (i1 = i2 & j1 = j2+1 implies [i2+1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2+1,j2)*>)) proof let k,i1,i2,j1,j2 such that A442: k > 1 and A443: [i1,j1] in Indices G and A444: (F.k)/.(len(F.k)-'1) = G*(i1,j1) and A445: [i2,j2] in Indices G and A446: (F.k)/.len(F.k) = G*(i2,j2); A447: len(F.k) = k by A177; then A448: 1 <= (len(F.k))-'1 by A442,NAT_D:49; (len(F.k))-'1 <= len(F.k) by NAT_D:35; then A449: (len(F.k))-'1 in dom(F.k) by A448,FINSEQ_3:25; A450: i1+1 > i1 by NAT_1:13; A451: F.k is_sequence_on G by A440; A452: j1+1 > j1 by NAT_1:13; A453: len(F.k) in dom(F.k) by A442,A447,FINSEQ_3:25; A454: i2+1 > i2 by NAT_1:13; A455: j2+1 > j2 by NAT_1:13; A456: (len(F.k)) -'1 +1 = len(F.k) by A442,A447,XREAL_1:235; then A457: (len(F.k))-'1+(1+1) = (len(F.k))+1; A458: left_cell(F.k,(len(F.k))-'1,G) meets C by A440,A448,A456; hereby assume that A459: front_right_cell(F.k,(len(F.k))-'1,G) misses C and A460: front_left_cell(F.k,(len(F.k))-'1,G) misses C; consider i,j such that A461: (F.k)^<*G*(i,j)*> turns_left (len(F.k))-'1,G and A462: F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A442,A451,A447,A458,A459,A460; thus F.(k+1) turns_left (len(F.k))-'1,G by A461,A462; A463: (F.(k+1))/.(len(F.k)+1) = G*(i,j) by A462,FINSEQ_4:67; A464: (F.(k+1))/.len(F.k) = G*(i2,j2) by A446,A453,A462,FINSEQ_4:68; A465: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) by A444,A449,A462,FINSEQ_4:68; hence i1 = i2 & j1+1 = j2 implies [i2-'1,j2] in Indices G & F.(k+1) = ( F.k)^<*G*(i2-'1,j2)*> by A443,A445,A456,A457,A452,A455,A461,A462,A464,A463, GOBRD13:def 7; thus i1+1 = i2 & j1 = j2 implies [i2,j2+1] in Indices G & F.(k+1) = (F .k)^<*G*(i2,j2+1)*> by A443,A445,A456,A457,A450,A454,A461,A462,A465,A464,A463, GOBRD13:def 7; thus i1 = i2+1 & j1 = j2 implies [i2,j2-'1] in Indices G & F.(k+1) = ( F.k)^<*G*(i2,j2-'1)*> by A443,A445,A456,A457,A450,A454,A461,A462,A465,A464,A463 ,GOBRD13:def 7; thus i1 = i2 & j1 = j2+1 implies [i2+1,j2] in Indices G & F.(k+1) = (F .k)^<*G*(i2+1,j2)*> by A443,A445,A456,A457,A452,A455,A461,A462,A465,A464,A463, GOBRD13:def 7; end; end; defpred P[Nat] means for m st m <= $1 holds (F.$1)|m = F.m; A466: P[0] proof let m; assume m <= 0; then 0 = m; hence thesis by A155; end; defpred K[Nat] means ex w being Nat st w = $1 & $1 >= 1 & ex m st m in dom(F.w) & m <> len(F.w) & (F.w)/.m = (F.w)/.len(F.w); A467: P[0,F.0,F.(0+1)] by A156; A468: for k,i1,i2,j1,j2 st k > 1 & [i1,j1] in Indices G & (F.k)/.(len(F.k) -'1) = G*(i1,j1) & [i2,j2] in Indices G & (F.k)/.len(F.k) = G*(i2,j2) holds ( front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k)) -'1,G) meets C implies F.(k+1) goes_straight (len(F.k))-'1,G & (i1 = i2 & j1+1 = j2 implies [i2,j2+1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2+1)*>) & (i1+1 = i2 & j1 = j2 implies [i2+1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2+1,j2)*> ) & (i1 = i2+1 & j1 = j2 implies [i2-'1,j2] in Indices G & F.(k+1) = (F.k)^<*G* (i2-'1,j2)*>)& (i1 = i2 & j1 = j2+1 implies [i2,j2-'1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2-'1)*>)) proof let k,i1,i2,j1,j2 such that A469: k > 1 and A470: [i1,j1] in Indices G and A471: (F.k)/.(len(F.k)-'1) = G*(i1,j1) and A472: [i2,j2] in Indices G and A473: (F.k)/.len(F.k) = G*(i2,j2); A474: len(F.k) = k by A177; then A475: 1 <= (len(F.k))-'1 by A469,NAT_D:49; (len(F.k))-'1 <= len(F.k) by NAT_D:35; then A476: (len(F.k))-'1 in dom(F.k) by A475,FINSEQ_3:25; A477: i1+1 > i1 by NAT_1:13; A478: F.k is_sequence_on G by A440; A479: j1+1 > j1 by NAT_1:13; A480: len(F.k) in dom(F.k) by A469,A474,FINSEQ_3:25; A481: i2+1 > i2 by NAT_1:13; A482: j2+1 > j2 by NAT_1:13; A483: (len(F.k)) -'1 +1 = len(F.k) by A469,A474,XREAL_1:235; then A484: (len(F.k))-'1+(1+1) = (len(F.k))+1; A485: left_cell(F.k,(len(F.k))-'1,G) meets C by A440,A475,A483; hereby assume that A486: front_right_cell(F.k,(len(F.k))-'1,G) misses C and A487: front_left_cell(F.k,(len(F.k))-'1,G) meets C; consider i,j such that A488: (F.k)^<*G*(i,j)*> goes_straight (len(F.k))-'1,G and A489: F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A469,A478,A474,A485,A486,A487; thus F.(k+1) goes_straight (len(F.k))-'1,G by A488,A489; A490: (F.(k+1))/.(len(F.k)+1) = G*(i,j) by A489,FINSEQ_4:67; A491: (F.(k+1))/.len(F.k) = G*(i2,j2) by A473,A480,A489,FINSEQ_4:68; A492: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) by A471,A476,A489,FINSEQ_4:68; hence i1 = i2 & j1+1 = j2 implies [i2,j2+1] in Indices G & F.(k+1) = (F .k)^<*G*(i2,j2+1)*> by A470,A472,A483,A484,A479,A482,A488,A489,A491,A490, GOBRD13:def 8; thus i1+1 = i2 & j1 = j2 implies [i2+1,j2] in Indices G & F.(k+1) = (F .k)^<*G*(i2+1,j2)*> by A470,A472,A483,A484,A477,A481,A488,A489,A492,A491,A490, GOBRD13:def 8; thus i1 = i2+1 & j1 = j2 implies [i2-'1,j2] in Indices G & F.(k+1) = ( F.k)^<*G*(i2-'1,j2)*> by A470,A472,A483,A484,A477,A481,A488,A489,A492,A491,A490 ,GOBRD13:def 8; thus i1 = i2 & j1 = j2+1 implies [i2,j2-'1] in Indices G & F.(k+1) = ( F.k)^<*G*(i2,j2-'1)*> by A470,A472,A483,A484,A479,A482,A488,A489,A492,A491,A490 ,GOBRD13:def 8; end; end; A493: for k,i1,i2,j1,j2 st k > 1 & [i1,j1] in Indices G & (F.k)/.(len(F.k) -'1) = G*(i1,j1) & [i2,j2] in Indices G & (F.k)/.len(F.k) = G*(i2,j2) holds ( front_right_cell(F.k,(len(F.k))-'1,G) meets C implies F.(k+1) turns_right (len( F.k))-'1,G & (i1 = i2 & j1+1 = j2 implies [i2+1,j2] in Indices G & F.(k+1) = (F .k)^<*G*(i2+1,j2)*>) & (i1+1 = i2 & j1 = j2 implies [i2,j2-'1] in Indices G & F .(k+1) = (F.k)^<*G*(i2,j2-'1)*>) & (i1 = i2+1 & j1 = j2 implies [i2,j2+1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2+1)*>)& (i1 = i2 & j1 = j2+1 implies [i2 -'1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2-'1,j2)*>)) proof let k,i1,i2,j1,j2 such that A494: k > 1 and A495: [i1,j1] in Indices G and A496: (F.k)/.(len(F.k)-'1) = G*(i1,j1) and A497: [i2,j2] in Indices G and A498: (F.k)/.len(F.k) = G*(i2,j2); A499: len(F.k) = k by A177; then A500: (len(F.k)) -'1 +1 = len(F.k) by A494,XREAL_1:235; then A501: (len(F.k))-'1+(1+1) = (len(F.k))+1; A502: F.k is_sequence_on G by A440; assume A503: front_right_cell(F.k,(len(F.k))-'1,G) meets C; A504: 1 <= (len(F.k))-'1 by A494,A499,NAT_D:49; then left_cell(F.k,(len(F.k))-'1,G) meets C by A440,A500; then consider i,j such that A505: (F.k)^<*G*(i,j)*> turns_right (len(F.k))-'1,G and A506: F.(k+1) = (F.k)^<*G*(i,j)*> by A156,A494,A502,A499,A503; len(F.k) in dom(F.k) by A494,A499,FINSEQ_3:25; then A507: (F.(k+1))/.len(F.k) = G*(i2,j2) by A498,A506,FINSEQ_4:68; (len(F.k))-'1 <= len(F.k) by NAT_D:35; then (len(F.k))-'1 in dom(F.k) by A504,FINSEQ_3:25; then A508: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) by A496,A506,FINSEQ_4:68; thus F.(k+1) turns_right (len(F.k))-'1,G by A505,A506; A509: (F.(k+1))/.(len(F.k)+1) = G*(i,j) by A506,FINSEQ_4:67; A510: j2+1 > j2 by NAT_1:13; A511: i2+1 > i2 by NAT_1:13; A512: j1+1 > j1 by NAT_1:13; hence i1 = i2 & j1+1 = j2 implies [i2+1,j2] in Indices G & F.(k+1) = (F.k )^<*G*(i2+1,j2)*> by A495,A497,A500,A501,A510,A505,A506,A508,A507,A509, GOBRD13:def 6; A513: i1+1 > i1 by NAT_1:13; hence i1+1 = i2 & j1 = j2 implies [i2,j2-'1] in Indices G & F.(k+1) = (F. k)^<*G*(i2,j2-'1)*> by A495,A497,A500,A501,A511,A505,A506,A508,A507,A509, GOBRD13:def 6; thus i1 = i2+1 & j1 = j2 implies [i2,j2+1] in Indices G & F.(k+1) = (F.k )^<*G*(i2,j2+1)*> by A495,A497,A500,A501,A513,A511,A505,A506,A508,A507,A509, GOBRD13:def 6; thus thesis by A495,A497,A500,A501,A512,A510,A505,A506,A508,A507,A509, GOBRD13:def 6; end; A514: for k st k > 1 holds (front_right_cell(F.k,k-'1,Gauge(C,n)) misses C & front_left_cell(F.k,k-'1,Gauge(C,n)) misses C implies F.(k+1) turns_left k-'1 ,Gauge(C,n)) & (front_right_cell(F.k,k-'1,Gauge(C,n)) misses C & front_left_cell(F.k,k-'1,Gauge(C,n)) meets C implies F.(k+1) goes_straight k-'1 ,Gauge(C,n)) & (front_right_cell(F.k,k-'1,Gauge(C,n)) meets C implies F.(k+1) turns_right k-'1,Gauge(C,n)) proof let k such that A515: k > 1; A516: F.k is_sequence_on G by A440; A517: len(F.k) = k by A177; then A518: (len(F.k)) -'1 +1 = len(F.k) by A515,XREAL_1:235; 1 <= (len(F.k))-'1 by A515,A517,NAT_D:49; then ex i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & (F.k )/.(len(F.k)-'1) = G*(i1,j1) & [i2,j2] in Indices G & (F.k)/.len(F.k) = G*(i2, j2) & (i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1) by A516,A518,JORDAN8:3; hence thesis by A441,A468,A493,A515,A517; end; A519: P[1,F.1,F.(1+1)] by A156; A520: for k holds ex i,j st [i,j] in Indices G & F.(k+1) = (F.k)^<*G*(i,j) *> proof let k; A521: F.k is_sequence_on G by A440; A522: len(F.k) = k by A177; per cases by XXREAL_0:1; suppose A523: k < 1; take X-SpanStart(C,n),Y-SpanStart(C,n); thus [X-SpanStart(C,n),Y-SpanStart(C,n)] in Indices G by A1,JORDAN11:8; k = 0 by A523,NAT_1:14; hence thesis by A155,A467,FINSEQ_1:34; end; suppose A524: k = 1; take X-SpanStart(C,n)-'1,Y-SpanStart(C,n); thus [X-SpanStart(C,n)-'1,Y-SpanStart(C,n)] in Indices G by A1, JORDAN11:9; thus thesis by A467,A519,A524,FINSEQ_1:def 9; end; suppose A525: k > 1; then A526: (len(F.k)) -'1 +1 = len(F.k) by A522,XREAL_1:235; 1 <= (len(F.k))-'1 by A522,A525,NAT_D:49; then consider i1,j1,i2,j2 being Nat such that A527: [i1,j1] in Indices G and A528: (F.k)/.(len(F.k)-'1) = G*(i1,j1) and A529: [i2,j2] in Indices G and A530: (F.k)/.len(F.k) = G*(i2,j2) and A531: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A521,A526,JORDAN8:3; now per cases; suppose A532: front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k))-'1,G) misses C; now per cases by A531; suppose A533: i1 = i2 & j1+1 = j2; then A534: F.(k+1) = (F.k)^<*G*(i2-'1,j2) *> by A441,A525,A527,A528,A529 ,A530,A532; [i2-'1,j2] in Indices G by A441,A525,A527,A528,A529,A530,A532 ,A533; hence thesis by A534; end; suppose A535: i1+1 = i2 & j1 = j2; then A536: F.(k+1) = (F.k)^<*G*(i2,j2+1)*> by A441,A525,A527,A528,A529 ,A530,A532; [i2,j2+1] in Indices G by A441,A525,A527,A528,A529,A530,A532 ,A535; hence thesis by A536; end; suppose A537: i1 = i2+1 & j1 = j2; then A538: F.(k+1) = (F.k)^<*G*(i2,j2-'1) *> by A441,A525,A527,A528,A529 ,A530,A532; [i2,j2-'1] in Indices G by A441,A525,A527,A528,A529,A530,A532 ,A537; hence thesis by A538; end; suppose A539: i1 = i2 & j1 = j2+1; then A540: F.(k+1) = (F.k)^<*G*(i2+1,j2)*> by A441,A525,A527,A528,A529 ,A530,A532; [i2+1,j2] in Indices G by A441,A525,A527,A528,A529,A530,A532 ,A539; hence thesis by A540; end; end; hence thesis; end; suppose A541: front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k))-'1,G) meets C; now per cases by A531; suppose A542: i1 = i2 & j1+1 = j2; then A543: F.(k+1) = (F.k)^<*G*(i2,j2+1)*> by A468,A525,A527,A528,A529 ,A530,A541; [i2,j2+1] in Indices G by A468,A525,A527,A528,A529,A530,A541 ,A542; hence thesis by A543; end; suppose A544: i1+1 = i2 & j1 = j2; then A545: F.(k+1) = (F.k)^<*G*(i2+1,j2)*> by A468,A525,A527,A528,A529 ,A530,A541; [i2+1,j2] in Indices G by A468,A525,A527,A528,A529,A530,A541 ,A544; hence thesis by A545; end; suppose A546: i1 = i2+1 & j1 = j2; then A547: F.(k+1) = (F.k)^<*G*(i2-'1,j2) *> by A468,A525,A527,A528,A529 ,A530,A541; [i2-'1,j2] in Indices G by A468,A525,A527,A528,A529,A530,A541 ,A546; hence thesis by A547; end; suppose A548: i1 = i2 & j1 = j2+1; then A549: F.(k+1) = (F.k)^<*G*(i2,j2-'1) *> by A468,A525,A527,A528,A529 ,A530,A541; [i2,j2-'1] in Indices G by A468,A525,A527,A528,A529,A530,A541 ,A548; hence thesis by A549; end; end; hence thesis; end; suppose A550: front_right_cell(F.k,(len(F.k))-'1,G) meets C; now per cases by A531; suppose A551: i1 = i2 & j1+1 = j2; then A552: F.(k+1) = (F.k)^<*G*(i2+1,j2)*> by A493,A525,A527,A528,A529 ,A530,A550; [i2+1,j2] in Indices G by A493,A525,A527,A528,A529,A530,A550 ,A551; hence thesis by A552; end; suppose A553: i1+1 = i2 & j1 = j2; then A554: F.(k+1) = (F.k)^<*G*(i2,j2-'1) *> by A493,A525,A527,A528,A529 ,A530,A550; [i2,j2-'1] in Indices G by A493,A525,A527,A528,A529,A530,A550 ,A553; hence thesis by A554; end; suppose A555: i1 = i2+1 & j1 = j2; then A556: F.(k+1) = (F.k)^<*G*(i2,j2+1)*> by A493,A525,A527,A528,A529 ,A530,A550; [i2,j2+1] in Indices G by A493,A525,A527,A528,A529,A530,A550 ,A555; hence thesis by A556; end; suppose A557: i1 = i2 & j1 = j2+1; then A558: F.(k+1) = (F.k)^<*G*(i2-'1,j2) *> by A493,A525,A527,A528,A529 ,A530,A550; [i2-'1,j2] in Indices G by A493,A525,A527,A528,A529,A530,A550 ,A557; hence thesis by A558; end; end; hence thesis; end; end; hence thesis; end; end; A559: for k st P[k] holds P[k+1] proof let k such that A560: for m st m <= k holds (F.k)|m = F.m; let m such that A561: m <= k+1; per cases by A561,XXREAL_0:1; suppose m < k+1; then A562: m <= k by NAT_1:13; A563: ex i,j st [i,j] in Indices G & F.(k+1) = F.k^<*G*(i,j)*> by A520; len(F.k) = k by A177; then (F.(k+1))|m = (F.k)|m by A562,A563,FINSEQ_5:22; hence thesis by A560,A562; end; suppose A564: m = k+1; len(F.(k+1)) = k+1 by A177; hence thesis by A564,FINSEQ_1:58; end; end; A565: for k holds P[k] from NAT_1:sch 2(A466,A559); A566: for j,k st 1 <= j & j <= k holds (F.k)/.j = (F.j)/.j proof let j,k; assume that A567: 1 <= j and A568: j <= k; j <= len(F.k) by A177,A568; then len(F.k|j) = j by FINSEQ_1:59; then A569: j in dom((F.k)|j) by A567,FINSEQ_3:25; (F.k)|j = F.j by A565,A568; hence thesis by A569,FINSEQ_4:70; end; defpred P[Nat] means F.$1 is unfolded; A570: for k st P[k] holds P[k+1] proof let k such that A571: F.k is unfolded; A572: F.k is_sequence_on G by A440; per cases; suppose k <= 1; then k+1 <= 1+1 by XREAL_1:6; then len(F.(k+1)) <= 2 by A177; hence thesis by SPPOL_2:26; end; suppose A573: k > 1; set m = k-'1; A574: m+1 = k by A573,XREAL_1:235; A575: len(F.k) = k by A177; A576: 1 <= m by A573,NAT_D:49; then consider i1,j1,i2,j2 being Nat such that A577: [i1,j1] in Indices G and A578: (F.k)/.m = G*(i1,j1) and A579: [i2,j2] in Indices G and A580: (F.k)/.len(F.k) = G*(i2,j2) and A581: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A572,A574,A575,JORDAN8:3; A582: LSeg(F.k,m) = LSeg(G*(i1,j1),G*(i2,j2)) by A576,A574,A575,A578,A580, TOPREAL1:def 3; A583: 1 <= j2 by A579,MATRIX_0:32; then A584: (j2-'1)+1 = j2 by XREAL_1:235; A585: 1 <= j1 by A577,MATRIX_0:32; A586: 1 <= i2 by A579,MATRIX_0:32; then A587: (i2-'1)+1 = i2 by XREAL_1:235; A588: i1 <= len G by A577,MATRIX_0:32; A589: j2 <= width G by A579,MATRIX_0:32; A590: 1 <= i1 by A577,MATRIX_0:32; A591: j1 <= width G by A577,MATRIX_0:32; A592: i2 <= len G by A579,MATRIX_0:32; now per cases; suppose A593: front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k))-'1,G) misses C; now per cases by A581; suppose A594: i1 = i2 & j1+1 = j2; then [i2-'1,j2] in Indices G by A441,A573,A575,A577,A578,A579 ,A580,A593; then 1 <= i2-'1 by MATRIX_0:32; then A595: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2-'1,j2)) = {(F. k)/.len(F.k)} by A580,A588,A585,A589,A587,A582,A594,GOBOARD7:16; F.(k+1) = (F.k)^ <*G*(i2-'1,j2)*> by A441,A573,A575,A577,A578 ,A579,A580,A593,A594; hence thesis by A571,A574,A575,A595,SPPOL_2:30; end; suppose A596: i1+1 = i2 & j1 = j2; then [i2,j2+1] in Indices G by A441,A573,A575,A577,A578,A579 ,A580,A593; then j2+1 <= width G by MATRIX_0:32; then A597: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2+1)) = {(F.k )/.len(F .k)} by A580,A590,A585,A592,A582,A596,GOBOARD7:18; F.(k+1) = (F.k)^ <*G*(i2,j2+1)*> by A441,A573,A575,A577,A578 ,A579,A580,A593,A596; hence thesis by A571,A574,A575,A597,SPPOL_2:30; end; suppose A598: i1 = i2+1 & j1 = j2; then [i2,j2-'1] in Indices G by A441,A573,A575,A577,A578,A579 ,A580,A593; then 1 <= j2-'1 by MATRIX_0:32; then A599: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2-'1)) = {(F. k)/.len(F.k)} by A580,A588,A591,A586,A584,A582,A598,GOBOARD7:15; F.(k+1) = (F.k)^ <*G*(i2,j2-'1)*> by A441,A573,A575,A577,A578 ,A579,A580,A593,A598; hence thesis by A571,A574,A575,A599,SPPOL_2:30; end; suppose A600: i1 = i2 & j1 = j2+1; then [i2+1,j2] in Indices G by A441,A573,A575,A577,A578,A579 ,A580,A593; then i2+1 <= len G by MATRIX_0:32; then A601: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2+1,j2)) = {(F.k )/.len(F .k)} by A580,A590,A591,A583,A582,A600,GOBOARD7:17; F.(k+1) = (F.k)^ <*G*(i2+1,j2)*> by A441,A573,A575,A577,A578 ,A579,A580,A593,A600; hence thesis by A571,A574,A575,A601,SPPOL_2:30; end; end; hence thesis; end; suppose A602: front_right_cell(F.k,(len(F.k))-'1,G) misses C & front_left_cell(F.k,(len(F.k))-'1,G) meets C; now per cases by A581; suppose A603: i1 = i2 & j1+1 = j2; then [i2,j2+1] in Indices G by A468,A573,A575,A577,A578,A579 ,A580,A602; then A604: j2+1 <= width G by MATRIX_0:32; j2+1 = j1+(1+1) by A603; then A605: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2+1)) = {(F.k )/.len(F .k)} by A580,A590,A588,A585,A582,A603,A604,GOBOARD7:13; F.(k+1) = (F.k)^ <*G*(i2,j2+1)*> by A468,A573,A575,A577,A578 ,A579,A580,A602,A603; hence thesis by A571,A574,A575,A605,SPPOL_2:30; end; suppose A606: i1+1 = i2 & j1 = j2; then [i2+1,j2] in Indices G by A468,A573,A575,A577,A578,A579 ,A580,A602; then A607: i2+1 <= len G by MATRIX_0:32; i2+1 = i1+(1+1) by A606; then A608: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2+1,j2)) = {(F.k )/.len(F .k)} by A580,A590,A585,A591,A582,A606,A607,GOBOARD7:14; F.(k+1) = (F.k)^ <*G*(i2+1,j2)*> by A468,A573,A575,A577,A578 ,A579,A580,A602,A606; hence thesis by A571,A574,A575,A608,SPPOL_2:30; end; suppose A609: i1 = i2+1 & j1 = j2; then [i2-'1,j2] in Indices G by A468,A573,A575,A577,A578,A579 ,A580,A602; then A610: 1 <= i2-'1 by MATRIX_0:32; i2-'1+1+1 = i2-'1+(1+1); then A611: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2-'1,j2)) = {(F. k)/.len(F.k)} by A580,A588,A585,A591,A587,A582,A609,A610,GOBOARD7:14; F.(k+1) = (F.k)^ <*G*(i2-'1,j2)*> by A468,A573,A575,A577,A578 ,A579,A580,A602,A609; hence thesis by A571,A574,A575,A611,SPPOL_2:30; end; suppose A612: i1 = i2 & j1 = j2+1; then [i2,j2-'1] in Indices G by A468,A573,A575,A577,A578,A579 ,A580,A602; then A613: 1 <= j2-'1 by MATRIX_0:32; j2-'1+1+1 = j2-'1+(1+1); then A614: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2-'1)) = {(F. k)/.len(F.k)} by A580,A590,A588,A591,A584,A582,A612,A613,GOBOARD7:13; F.(k+1) = (F.k)^ <*G*(i2,j2-'1)*> by A468,A573,A575,A577,A578 ,A579,A580,A602,A612; hence thesis by A571,A574,A575,A614,SPPOL_2:30; end; end; hence thesis; end; suppose A615: front_right_cell(F.k,(len(F.k))-'1,G) meets C; now per cases by A581; suppose A616: i1 = i2 & j1+1 = j2; then [i2+1,j2] in Indices G by A493,A573,A575,A577,A578,A579 ,A580,A615; then i2+1 <= len G by MATRIX_0:32; then A617: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2+1,j2)) = {(F.k )/.len(F .k)} by A580,A590,A585,A589,A582,A616,GOBOARD7:15; F.(k+1) = (F.k)^ <*G*(i2+1,j2)*> by A493,A573,A575,A577,A578 ,A579,A580,A615,A616; hence thesis by A571,A574,A575,A617,SPPOL_2:30; end; suppose A618: i1+1 = i2 & j1 = j2; then [i2,j2-'1] in Indices G by A493,A573,A575,A577,A578,A579 ,A580,A615; then 1 <= j2-'1 by MATRIX_0:32; then A619: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2-'1)) = {(F. k)/.len(F.k)} by A580,A590,A591,A592,A584,A582,A618,GOBOARD7:16; F.(k+1) = (F.k)^ <*G*(i2,j2-'1)*> by A493,A573,A575,A577,A578 ,A579,A580,A615,A618; hence thesis by A571,A574,A575,A619,SPPOL_2:30; end; suppose A620: i1 = i2+1 & j1 = j2; then [i2,j2+1] in Indices G by A493,A573,A575,A577,A578,A579 ,A580,A615; then j2+1 <= width G by MATRIX_0:32; then A621: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2+1)) = {(F.k )/.len(F .k)} by A580,A588,A585,A586,A582,A620,GOBOARD7:17; F.(k+1) = (F.k)^ <*G*(i2,j2+1)*> by A493,A573,A575,A577,A578 ,A579,A580,A615,A620; hence thesis by A571,A574,A575,A621,SPPOL_2:30; end; suppose A622: i1 = i2 & j1 = j2+1; then [i2-'1,j2] in Indices G by A493,A573,A575,A577,A578,A579 ,A580,A615; then 1 <= i2-'1 by MATRIX_0:32; then A623: LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2-'1,j2)) = {(F. k)/.len(F.k)} by A580,A588,A591,A583,A587,A582,A622,GOBOARD7:18; F.(k+1) = (F.k)^ <*G*(i2-'1,j2)*> by A493,A573,A575,A577,A578 ,A579,A580,A615,A622; hence thesis by A571,A574,A575,A623,SPPOL_2:30; end; end; hence thesis; end; end; hence thesis; end; end; now defpred P[Nat] means F.$1 is one-to-one; assume A624: for k st k >= 1 holds for m st m in dom(F.k) & m <> len(F.k) holds (F.k)/.m <> (F.k)/.len(F.k); A625: for k st P[k] holds P[k+1] proof let k; assume A626: F.k is one-to-one; now let n,m be Element of NAT such that A627: n in dom(F.(k+1)) and A628: m in dom(F.(k+1)) and A629: (F.(k+1))/.n = (F.(k+1))/.m; A630: 1 <= n by A627,FINSEQ_3:25; A631: m <= len(F.(k+1)) by A628,FINSEQ_3:25; A632: 1 <= m by A628,FINSEQ_3:25; A633: n <= len(F.(k+1)) by A627,FINSEQ_3:25; A634: ex i,j st [i,j] in Indices G & F.(k+1) = (F.k)^<*G*(i,j) *> by A520; A635: len(F.k) = k by A177; A636: len(F.(k+1)) = k+1 by A177; per cases by A633,A631,A636,NAT_1:8; suppose A637: n <= k & m <= k; then A638: m in dom(F.k) by A632,A635,FINSEQ_3:25; then A639: (F.(k+1))/.m = (F.k)/.m by A634,FINSEQ_4:68; A640: n in dom(F.k) by A630,A635,A637,FINSEQ_3:25; then (F.(k+1))/.n = (F.k)/.n by A634,FINSEQ_4:68; hence n = m by A626,A629,A640,A638,A639,PARTFUN2:10; end; suppose n = k+1 & m <= k; hence n = m by A624,A628,A629,A636,NAT_1:12; end; suppose n <= k & m = k+1; hence n = m by A624,A627,A629,A636,NAT_1:12; end; suppose n = k+1 & m = k+1; hence n = m; end; end; hence thesis by PARTFUN2:9; end; A641: P[0] by A155; A642: for k holds P[k] from NAT_1:sch 2(A641,A625); A643: for k holds card rng(F.k) = k proof let k; F.k is one-to-one by A642; hence card rng(F.k) = len(F.k) by FINSEQ_4:62 .= k by A177; end; reconsider k = (len G)*(width G)+1 as Nat; A644: k > (len G)*(width G) by NAT_1:13; F.k is_sequence_on G by A440; then A645: card rng(F.k) <= card Values G by GOBRD13:8,NAT_1:43; card Values G <= (len G)*(width G) by MATRIX_0:40; then card rng(F.k) <= (len G)*(width G) by A645,XXREAL_0:2; hence contradiction by A643,A644; end; then A646: ex k be Nat st K[k]; consider k be Nat such that A647: K[k] and A648: for l be Nat st K[l] holds k <= l from NAT_1:sch 5(A646); reconsider k as Nat; consider m such that A649: m in dom(F.k) and A650: m <> len(F.k) and A651: (F.k)/.m = (F.k)/.len(F.k) by A647; A652: 1 <= m by A649,FINSEQ_3:25; reconsider f = F.k as non empty FinSequence of TOP-REAL 2 by A647; A653: f is_sequence_on G by A440; A654: m <= len f by A649,FINSEQ_3:25; then A655: m < len f by A650,XXREAL_0:1; then 1 < len f by A652,XXREAL_0:2; then A656: len f >= 1+1 by NAT_1:13; then A657: k >= 2 by A177; A658: P[0] by A155,CARD_1:27,SPPOL_2:26; for k holds P[k] from NAT_1:sch 2(A658,A570); then reconsider f as non constant special unfolded non empty FinSequence of TOP-REAL 2 by A653,A656,JORDAN8:4,5; set g = f/^(m-'1); A659: m+1 <= len f by A655,NAT_1:13; A660: for h being standard non constant special_circular_sequence st L~h c= L~f for Comp being Subset of TOP-REAL 2 st Comp is_a_component_of (L~h)` for n st 1 <= n & n+1 <= len f & f/.n in Comp & not f/.n in L~h holds C meets Comp proof let h be standard non constant special_circular_sequence such that A661: L~h c= L~f; let Comp be Subset of TOP-REAL 2 such that A662: Comp is_a_component_of (L~h)`; let n such that A663: 1 <= n and A664: n+1 <= len f and A665: f/.n in Comp and A666: not f/.n in L~h; set rc=left_cell(f,n,G)\L~h; reconsider rc as Subset of TOP-REAL 2; A667: Int left_cell(f,n,G) c= left_cell(f,n,G) by TOPS_1:16; f/.n in left_cell(f,n,G) by A653,A663,A664,JORDAN9:8; then f/.n in rc by A666,XBOOLE_0:def 5; then A668: rc meets Comp by A665,XBOOLE_0:3; A669: rc = left_cell(f,n,G) /\ (L~h)` by SUBSET_1:13; then A670: rc c= (L~h)` by XBOOLE_1:17; Int left_cell(f,n,G) misses L~f by A653,A663,A664,JORDAN9:15; then Int left_cell(f,n,G) misses L~h by A661,XBOOLE_1:63; then A671: Int left_cell(f,n,G) c= (L~h)` by SUBSET_1:23; rc c= left_cell(f,n,G) by XBOOLE_1:36; then A672: rc c= Cl Int left_cell(f,n,G) by A653,A663,A664,JORDAN9:11; A673: rc meets C proof left_cell(f,n,G) meets C by A440,A663,A664; then consider p being object such that A674: p in left_cell(f,n,G) and A675: p in C by XBOOLE_0:3; reconsider p as Element of TOP-REAL 2 by A674; now take p; now assume p in L~h; then consider j such that A676: 1 <= j and A677: j+1 <= len f and A678: p in LSeg(f,j) by A661,SPPOL_2:13; p in right_cell(f,j,G) /\ left_cell(f,j,G) by A440,A676,A677,A678, GOBRD13:29; then A679: p in right_cell(f,j,G) by XBOOLE_0:def 4; right_cell(f,j,G) misses C by A440,A676,A677; hence contradiction by A675,A679,XBOOLE_0:3; end; hence p in rc by A674,XBOOLE_0:def 5; thus p in C by A675; end; hence thesis by XBOOLE_0:3; end; Int left_cell(f,n,G) is convex by A653,A663,A664,JORDAN9:10; then rc is connected by A669,A671,A667,A672,CONNSP_1:18,XBOOLE_1:19; then rc c= Comp by A662,A668,A670,GOBOARD9:4; hence thesis by A673,XBOOLE_1:63; end; A680: for i st 1 <= i & i+1 <= len f holds left_cell(f,i,G) = Cl Int left_cell(f,i,G) proof let i such that A681: 1 <= i and A682: i+1 <= len f; consider i1,j1,i2,j2 such that A683: [i1,j1] in Indices G and A684: f/.i = G*(i1,j1) and A685: [i2,j2] in Indices G and A686: f/.(i+1) = G*(i2,j2) and A687: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A653,A681,A682,JORDAN8:3; A688: i1 <= len G by A683,MATRIX_0:32; A689: i2 <= len G by A685,MATRIX_0:32; A690: i1+1 > i1 by NAT_1:13; A691: j1 <= width G by A683,MATRIX_0:32; A692: j1+1 > j1 by NAT_1:13; A693: j2 <= width G by A685,MATRIX_0:32; A694: i2+1 > i2 by NAT_1:13; A695: j2+1 > j2 by NAT_1:13; per cases by A687; suppose A696: i1 = i2 & j1+1 = j2; A697: i1-'1 <= len G by A688,NAT_D:44; left_cell(f,i,G) = cell(G,i1-'1,j1) by A653,A681,A682,A683,A684,A685 ,A686,A692,A695,A696,GOBRD13:def 3; hence thesis by A691,A697,GOBRD11:35; end; suppose i1+1 = i2 & j1 = j2; then left_cell(f,i,G) = cell(G,i1,j1) by A653,A681,A682,A683,A684,A685 ,A686,A690,A694,GOBRD13:def 3; hence thesis by A688,A691,GOBRD11:35; end; suppose A698: i1 = i2+1 & j1 = j2; A699: j2-'1 <= width G by A693,NAT_D:44; left_cell(f,i,G) = cell(G,i2,j2-'1) by A653,A681,A682,A683,A684,A685 ,A686,A690,A694,A698,GOBRD13:def 3; hence thesis by A689,A699,GOBRD11:35; end; suppose i1 = i2 & j1 = j2+1; then left_cell(f,i,G) = cell(G,i1,j2) by A653,A681,A682,A683,A684,A685 ,A686,A692,A695,GOBRD13:def 3; hence thesis by A688,A693,GOBRD11:35; end; end; m-'1 <= m by NAT_D:44; then m-'1 < m+1 by NAT_1:13; then A700: m-'1 < len f by A659,XXREAL_0:2; then A701: len g = len f - (m-'1) by RFINSEQ:def 1; then (m-'1)-(m-'1) < len g by A700,XREAL_1:9; then reconsider g as non empty FinSequence of TOP-REAL 2 by CARD_1:27; len g in dom g by FINSEQ_5:6; then A702: g/.len g = f/.(m-'1+len g) by FINSEQ_5:27 .= f/.len f by A701; m+1-(m-'1) <= len g by A659,A701,XREAL_1:9; then A703: m+1-(m-1) <= len g by A652,XREAL_1:233; then A704: 1+m-m+1 <= len g; A705: g is_sequence_on G by A440,JORDAN8:2; then A706: g is standard by JORDAN8:4; A707: g is non constant proof take 1,2; thus A708: 1 in dom g by FINSEQ_5:6; thus A709: 2 in dom g by A703,FINSEQ_3:25; then g/.1 <> g/.(1+1) by A706,FINSEQ_5:6,GOBOARD7:29; then g.1 <> g/.(1+1) by A708,PARTFUN1:def 6; hence thesis by A709,PARTFUN1:def 6; end; A710: len(F.k) = k by A177; A711: for i st 1 <= i & i < len g & 1 <= j & j < len g & g/.i = g/.j holds i = j proof let i such that A712: 1 <= i and A713: i < len g and A714: 1 <= j and A715: j < len g and A716: g/.i = g/.j and A717: i <> j; A718: i in dom g by A712,A713,FINSEQ_3:25; then A719: g/.i = f/.(m-'1+i) by FINSEQ_5:27; A720: j in dom g by A714,A715,FINSEQ_3:25; then A721: g/.j = f/.(m-'1+j) by FINSEQ_5:27; per cases by A717,XXREAL_0:1; suppose A722: i < j; set l = m-'1+j, m9= m-'1+i; A723: m9 < l by A722,XREAL_1:6; A724: len(F.l) = l by A177; A725: l < k by A710,A701,A715,XREAL_1:20; then A726: f|l = F.l by A565; 0+j <= l by XREAL_1:6; then A727: 1 <= l by A714,XXREAL_0:2; then l in dom(F.l) by A724,FINSEQ_3:25; then A728: (F.l)/.l = f/.l by A726,FINSEQ_4:70; 0+i <= m9 by XREAL_1:6; then 1 <= m9 by A712,XXREAL_0:2; then A729: m9 in dom(F.l) by A723,A724,FINSEQ_3:25; then (F.l)/.m9 = f/.m9 by A726,FINSEQ_4:70; hence contradiction by A648,A716,A719,A720,A723,A725,A727,A724,A729 ,A728,FINSEQ_5:27; end; suppose A730: j < i; set l = m-'1+i, m9= m-'1+j; A731: m9 < l by A730,XREAL_1:6; A732: len(F.l) = l by A177; A733: l < k by A710,A701,A713,XREAL_1:20; then A734: f|l = F.l by A565; 0+i <= l by XREAL_1:6; then A735: 1 <= l by A712,XXREAL_0:2; then l in dom(F.l) by A732,FINSEQ_3:25; then A736: (F.l)/.l = f/.l by A734,FINSEQ_4:70; 0+j <= m9 by XREAL_1:6; then 1 <= m9 by A714,XXREAL_0:2; then A737: m9 in dom(F.l) by A731,A732,FINSEQ_3:25; then (F.l)/.m9 = f/.m9 by A734,FINSEQ_4:70; hence contradiction by A648,A716,A718,A721,A731,A733,A735,A732,A737,A736, FINSEQ_5:27; end; end; 1 in dom g by FINSEQ_5:6; then A738: g/.1 = f/.(m-'1+1) by FINSEQ_5:27 .= f/.m by A652,XREAL_1:235; A739: for i st 1 < i & i < j & j <= len g holds g/.i <> g/.j proof let i such that A740: 1 < i and A741: i < j and A742: j <= len g and A743: g/.i = g/.j; A744: 1 < j by A740,A741,XXREAL_0:2; A745: i < len g by A741,A742,XXREAL_0:2; then A746: 1 < len g by A740,XXREAL_0:2; per cases; suppose j <> len g; then j < len g by A742,XXREAL_0:1; hence contradiction by A711,A740,A741,A743,A744,A745; end; suppose j = len g; hence contradiction by A651,A738,A702,A711,A740,A741,A743,A746; end; end; A747: for i st 1 <= i & i < j & j < len g holds g/.i <> g/.j proof let i such that A748: 1 <= i and A749: i < j and A750: j < len g and A751: g/.i = g/.j; A752: i < len g by A749,A750,XXREAL_0:2; 1 < j by A748,A749,XXREAL_0:2; hence contradiction by A711,A748,A749,A750,A751,A752; end; g is s.c.c. proof let i,j such that A753: i+1 < j and A754: i > 1 & j < len g or j+1 < len g; A755: 1 < j by A753,NAT_1:12; A756: 1 <= i+1 by NAT_1:12; A757: j <= j+1 by NAT_1:12; then A758: i+1 < j+1 by A753,XXREAL_0:2; i < j by A753,NAT_1:13; then A759: i < j+1 by A757,XXREAL_0:2; per cases by A754,NAT_1:14; suppose A760: i > 1 & j < len g; then A761: i+1 < len g by A753,XXREAL_0:2; then A762: LSeg(g,i) = LSeg(g/.i,g/.(i+1)) by A760,TOPREAL1:def 3; A763: i < len g by A761,NAT_1:13; consider i1,j1,i2,j2 such that A764: [i1,j1] in Indices G and A765: g/.i = G*(i1,j1) and A766: [i2,j2] in Indices G and A767: g/.(i+1) = G*(i2,j2) and A768: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A705,A760,A761,JORDAN8:3; A769: 1 <= i1 by A764,MATRIX_0:32; A770: j2 <= width G by A766,MATRIX_0:32; A771: 1 <= i2 by A766,MATRIX_0:32; A772: i1 <= len G by A764,MATRIX_0:32; A773: 1 <= j2 by A766,MATRIX_0:32; A774: j1 <= width G by A764,MATRIX_0:32; A775: i2 <= len G by A766,MATRIX_0:32; A776: 1 <= j1 by A764,MATRIX_0:32; A777: 1 < i+1 by A760,NAT_1:13; A778: j+1 <= len g by A760,NAT_1:13; then A779: LSeg(g,j) = LSeg(g/.j,g/.(j+1)) by A755,TOPREAL1:def 3; consider i19,j19,i29,j29 being Nat such that A780: [i19,j19] in Indices G and A781: g/.j = G*(i19,j19) and A782: [i29,j29] in Indices G and A783: g/.(j+1) = G*(i29,j29) and A784: i19 = i29 & j19+1 = j29 or i19+1 = i29 & j19 = j29 or i19 = i29+1 & j19 = j29 or i19 = i29 & j19 = j29+1 by A705,A755,A778,JORDAN8:3; A785: 1 <= i19 by A780,MATRIX_0:32; A786: j29 <= width G by A782,MATRIX_0:32; A787: j19 <= width G by A780,MATRIX_0:32; A788: 1 <= j29 by A782,MATRIX_0:32; A789: 1 <= j19 by A780,MATRIX_0:32; A790: i29 <= len G by A782,MATRIX_0:32; A791: i19 <= len G by A780,MATRIX_0:32; assume LSeg(g,i) /\ LSeg(g,j) <> {}; then A792: LSeg(g,i) meets LSeg(g,j) by XBOOLE_0:def 7; A793: 1 <= i29 by A782,MATRIX_0:32; now per cases by A768,A784; suppose A794: i1 = i2 & j1+1 = j2 & i19 = i29 & j19+1 = j29; then A795: i1 = i19 by A762,A765,A767,A769,A772,A776,A770,A779,A781,A783,A785 ,A791,A789,A786,A792,GOBOARD7:19; now per cases by A762,A765,A767,A769,A772,A776,A770,A779,A781,A783 ,A785,A791,A789,A786,A792,A794,GOBOARD7:22; suppose j1 = j19; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A795; end; suppose j1 = j19+1; hence contradiction by A739,A759,A760,A765,A778,A783,A794,A795; end; suppose j1+1 = j19; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A794 ,A795; end; end; hence contradiction; end; suppose A796: i1 = i2 & j1+1 = j2 & i19+1 = i29 & j19 = j29; now per cases by A762,A765,A767,A769,A772,A776,A770,A779,A781,A783 ,A785,A789,A787,A790,A792,A796,GOBOARD7:21; suppose i1 = i19 & j1 = j19; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781; end; suppose i1 = i19 & j1+1 = j19; hence contradiction by A739,A753,A760,A777,A767,A781,A796; end; suppose i1 = i19+1 & j1 = j19; hence contradiction by A739,A759,A760,A765,A778,A783,A796; end; suppose i1 = i19+1 & j1+1 = j19; hence contradiction by A739,A758,A777,A767,A778,A783,A796; end; end; hence contradiction; end; suppose A797: i1 = i2 & j1+1 = j2 & i19 = i29+1 & j19 = j29; now per cases by A762,A765,A767,A769,A772,A776,A770,A779,A781,A783 ,A791,A789,A787,A793,A792,A797,GOBOARD7:21; suppose i1 = i29 & j19 = j1; hence contradiction by A739,A759,A760,A765,A778,A783,A797; end; suppose i1 = i29 & j1+1 = j19; hence contradiction by A739,A758,A777,A767,A778,A783,A797; end; suppose i1 = i29+1 & j19 = j1; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A797; end; suppose i1 = i29+1 & j1+1 = j19; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A797; end; end; hence contradiction; end; suppose A798: i1 = i2 & j1+1 = j2 & i19 = i29 & j19 = j29+1; then A799: i1 = i19 by A762,A765,A767,A769,A772,A776,A770,A779,A781,A783,A785 ,A791,A787,A788,A792,GOBOARD7:19; now per cases by A762,A765,A767,A769,A772,A776,A770,A779,A781,A783 ,A785,A791,A787,A788,A792,A798,GOBOARD7:22; suppose j1 = j29; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A798 ,A799; end; suppose j1 = j29+1; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A798 ,A799; end; suppose j1+1 = j29; hence contradiction by A739,A758,A777,A767,A778,A783,A798,A799; end; end; hence contradiction; end; suppose A800: i1+1 = i2 & j1 = j2 & i19 = i29 & j19+1 = j29; now per cases by A762,A765,A767,A769,A776,A774,A775,A779,A781,A783 ,A785,A791,A789,A786,A792,A800,GOBOARD7:21; suppose i19 = i1 & j1 = j19; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781; end; suppose i19 = i1 & j19+1 = j1; hence contradiction by A739,A759,A760,A765,A778,A783,A800; end; suppose i19 = i1+1 & j1 = j19; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A800; end; suppose i19 = i1+1 & j19+1 = j1; hence contradiction by A739,A758,A777,A767,A778,A783,A800; end; end; hence contradiction; end; suppose A801: i1+1 = i2 & j1 = j2 & i19+1 = i29 & j19 = j29; then A802: j1 = j19 by A762,A765,A767,A769,A776,A774,A775,A779,A781,A783,A785 ,A789,A787,A790,A792,GOBOARD7:20; now per cases by A762,A765,A767,A769,A776,A774,A775,A779,A781,A783 ,A785,A789,A787,A790,A792,A801,GOBOARD7:23; suppose i1 = i19; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A802; end; suppose i1 = i19+1; hence contradiction by A739,A759,A760,A765,A778,A783,A801,A802; end; suppose i1+1 = i19; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A801 ,A802; end; end; hence contradiction; end; suppose A803: i1+1 = i2 & j1 = j2 & i19 = i29+1 & j19 = j29; then A804: j1 = j19 by A762,A765,A767,A769,A776,A774,A775,A779,A781,A783,A791 ,A789,A787,A793,A792,GOBOARD7:20; now per cases by A762,A765,A767,A769,A776,A774,A775,A779,A781,A783 ,A791,A789,A787,A793,A792,A803,GOBOARD7:23; suppose i1 = i29; hence contradiction by A739,A759,A760,A765,A778,A783,A803,A804; end; suppose i1 = i29+1; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A803 ,A804; end; suppose i1+1 = i29; hence contradiction by A739,A758,A777,A767,A778,A783,A803,A804; end; end; hence contradiction; end; suppose A805: i1+1 = i2 & j1 = j2 & i19 = i29 & j19 = j29+1; now per cases by A762,A765,A767,A769,A776,A774,A775,A779,A781,A783 ,A785,A791,A787,A788,A792,A805,GOBOARD7:21; suppose i19 = i1 & j1 = j29; hence contradiction by A739,A759,A760,A765,A778,A783,A805; end; suppose i19 = i1 & j29+1 = j1; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A805; end; suppose i19 = i1+1 & j1 = j29; hence contradiction by A739,A758,A777,A767,A778,A783,A805; end; suppose i19 = i1+1 & j29+1 = j1; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A805; end; end; hence contradiction; end; suppose A806: i1 = i2+1 & j1 = j2 & i19 = i29 & j19+1 = j29; now per cases by A762,A765,A767,A772,A776,A774,A771,A779,A781,A783 ,A785,A791,A789,A786,A792,A806,GOBOARD7:21; suppose i19 = i2 & j19 = j1; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A806; end; suppose i19 = i2 & j19+1 = j1; hence contradiction by A739,A758,A777,A767,A778,A783,A806; end; suppose i19 = i2+1 & j19 = j1; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A806; end; suppose i19 = i2+1 & j19+1 = j1; hence contradiction by A739,A759,A760,A765,A778,A783,A806; end; end; hence contradiction; end; suppose A807: i1 = i2+1 & j1 = j2 & i19+1 = i29 & j19 = j29; then A808: j1 = j19 by A762,A765,A767,A772,A776,A774,A771,A779,A781,A783,A785 ,A789,A787,A790,A792,GOBOARD7:20; now per cases by A762,A765,A767,A772,A776,A774,A771,A779,A781,A783 ,A785,A789,A787,A790,A792,A807,GOBOARD7:23; suppose i2 = i19; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A807 ,A808; end; suppose i2 = i19+1; hence contradiction by A739,A758,A777,A767,A778,A783,A807,A808; end; suppose i2+1 = i19; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A807 ,A808; end; end; hence contradiction; end; suppose A809: i1 = i2+1 & j1 = j2 & i19 = i29+1 & j19 = j29; then A810: j1 = j19 by A762,A765,A767,A772,A776,A774,A771,A779,A781,A783,A791 ,A789,A787,A793,A792,GOBOARD7:20; now per cases by A762,A765,A767,A772,A776,A774,A771,A779,A781,A783 ,A791,A789,A787,A793,A792,A809,GOBOARD7:23; suppose i2 = i29; hence contradiction by A739,A758,A777,A767,A778,A783,A809,A810; end; suppose i2 = i29+1; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A809 ,A810; end; suppose i2+1 = i29; hence contradiction by A739,A759,A760,A765,A778,A783,A809,A810; end; end; hence contradiction; end; suppose A811: i1 = i2+1 & j1 = j2 & i19 = i29 & j19 = j29+1; now per cases by A762,A765,A767,A772,A776,A774,A771,A779,A781,A783 ,A785,A791,A787,A788,A792,A811,GOBOARD7:21; suppose i19 = i2 & j29 = j1; hence contradiction by A739,A758,A777,A767,A778,A783,A811; end; suppose i19 = i2 & j29+1 = j1; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A811; end; suppose i19 = i2+1 & j29 = j1; hence contradiction by A739,A759,A760,A765,A778,A783,A811; end; suppose i19 = i2+1 & j29+1 = j1; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A811; end; end; hence contradiction; end; suppose A812: i1 = i2 & j1 = j2+1 & i19 = i29 & j19+1 = j29; then A813: i1 = i19 by A762,A765,A767,A769,A772,A774,A773,A779,A781,A783,A785 ,A791,A789,A786,A792,GOBOARD7:19; now per cases by A762,A765,A767,A769,A772,A774,A773,A779,A781,A783 ,A785,A791,A789,A786,A792,A812,GOBOARD7:22; suppose j2 = j19; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A812 ,A813; end; suppose j2 = j19+1; hence contradiction by A739,A758,A777,A767,A778,A783,A812,A813; end; suppose j2+1 = j19; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A812 ,A813; end; end; hence contradiction; end; suppose A814: i1 = i2 & j1 = j2+1 & i19+1 = i29 & j19 = j29; now per cases by A762,A765,A767,A769,A772,A774,A773,A779,A781,A783 ,A785,A789,A787,A790,A792,A814,GOBOARD7:21; suppose i1 = i19 & j2 = j19; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A814; end; suppose i1 = i19 & j2+1 = j19; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A814; end; suppose i1 = i19+1 & j2 = j19; hence contradiction by A739,A758,A777,A767,A778,A783,A814; end; suppose i1 = i19+1 & j2+1 = j19; hence contradiction by A739,A759,A760,A765,A778,A783,A814; end; end; hence contradiction; end; suppose A815: i1 = i2 & j1 = j2+1 & i19 = i29+1 & j19 = j29; now per cases by A762,A765,A767,A769,A772,A774,A773,A779,A781,A783 ,A791,A789,A787,A793,A792,A815,GOBOARD7:21; suppose i1 = i29 & j2 = j19; hence contradiction by A739,A758,A777,A767,A778,A783,A815; end; suppose i1 = i29 & j2+1 = j19; hence contradiction by A739,A759,A760,A765,A778,A783,A815; end; suppose i1 = i29+1 & j2 = j19; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A815; end; suppose i1 = i29+1 & j2+1 = j19; hence contradiction by A711,A753,A757,A755,A760,A763,A765,A781,A815; end; end; hence contradiction; end; suppose A816: i1 = i2 & j1 = j2+1 & i19 = i29 & j19 = j29+1; then A817: i1 = i19 by A762,A765,A767,A769,A772,A774,A773,A779,A781,A783,A785 ,A791,A787,A788,A792,GOBOARD7:19; now per cases by A762,A765,A767,A769,A772,A774,A773,A779,A781,A783 ,A785,A791,A787,A788,A792,A816,GOBOARD7:22; suppose j2 = j29; hence contradiction by A739,A758,A777,A767,A778,A783,A816,A817; end; suppose j2 = j29+1; hence contradiction by A711,A753,A756,A755,A760,A761,A767,A781,A816 ,A817; end; suppose j2+1 = j29; hence contradiction by A739,A759,A760,A765,A778,A783,A816,A817; end; end; hence contradiction; end; end; hence contradiction; end; suppose i = 0 & j+1 < len g; then LSeg(g,i) = {} by TOPREAL1:def 3; hence LSeg(g,i) /\ LSeg(g,j) = {}; end; suppose A818: 1 <= i & j+1 < len g; then consider i19,j19,i29,j29 being Nat such that A819: [i19,j19] in Indices G and A820: g/.j = G*(i19,j19) and A821: [i29,j29] in Indices G and A822: g/.(j+1) = G*(i29,j29) and A823: i19 = i29 & j19+1 = j29 or i19+1 = i29 & j19 = j29 or i19 = i29+1 & j19 = j29 or i19 = i29 & j19 = j29+1 by A705,A755,JORDAN8:3; A824: 1 <= i19 by A819,MATRIX_0:32; A825: j29 <= width G by A821,MATRIX_0:32; A826: 1 <= i29 by A821,MATRIX_0:32; A827: i19 <= len G by A819,MATRIX_0:32; A828: 1 <= j29 by A821,MATRIX_0:32; A829: j19 <= width G by A819,MATRIX_0:32; A830: i29 <= len G by A821,MATRIX_0:32; A831: 1 <= j19 by A819,MATRIX_0:32; assume LSeg(g,i) /\ LSeg(g,j) <> {}; then A832: LSeg(g,i) meets LSeg(g,j) by XBOOLE_0:def 7; A833: 1 < i+1 by A818,NAT_1:13; A834: j < len g by A818,NAT_1:12; A835: i+1 < len g by A758,A818,XXREAL_0:2; then A836: LSeg(g,i) = LSeg(g/.i,g/.(i+1)) by A818,TOPREAL1:def 3; A837: i < len g by A835,NAT_1:13; consider i1,j1,i2,j2 such that A838: [i1,j1] in Indices G and A839: g/.i = G*(i1,j1) and A840: [i2,j2] in Indices G and A841: g/.(i+1) = G*(i2,j2) and A842: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A705,A818,A835,JORDAN8:3; A843: 1 <= i1 by A838,MATRIX_0:32; A844: j2 <= width G by A840,MATRIX_0:32; A845: j1 <= width G by A838,MATRIX_0:32; A846: 1 <= j2 by A840,MATRIX_0:32; A847: 1 <= j1 by A838,MATRIX_0:32; A848: i2 <= len G by A840,MATRIX_0:32; A849: i1 <= len G by A838,MATRIX_0:32; A850: LSeg(g,j) = LSeg(g/.j,g/.(j+1)) by A755,A818,TOPREAL1:def 3; A851: 1 <= i2 by A840,MATRIX_0:32; now per cases by A842,A823; suppose A852: i1 = i2 & j1+1 = j2 & i19 = i29 & j19+1 = j29; then A853: i1 = i19 by A836,A839,A841,A843,A849,A847,A844,A850,A820,A822,A824 ,A827,A831,A825,A832,GOBOARD7:19; now per cases by A836,A839,A841,A843,A849,A847,A844,A850,A820,A822 ,A824,A827,A831,A825,A832,A852,GOBOARD7:22; suppose j1 = j19; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A853; end; suppose j1 = j19+1; hence contradiction by A747,A759,A818,A839,A822,A852,A853; end; suppose j1+1 = j19; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A852 ,A853; end; end; hence contradiction; end; suppose A854: i1 = i2 & j1+1 = j2 & i19+1 = i29 & j19 = j29; now per cases by A836,A839,A841,A843,A849,A847,A844,A850,A820,A822 ,A824,A831,A829,A830,A832,A854,GOBOARD7:21; suppose i1 = i19 & j1 = j19; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820; end; suppose i1 = i19 & j1+1 = j19; hence contradiction by A739,A753,A833,A834,A841,A820,A854; end; suppose i1 = i19+1 & j1 = j19; hence contradiction by A747,A759,A818,A839,A822,A854; end; suppose i1 = i19+1 & j1+1 = j19; hence contradiction by A739,A758,A818,A833,A841,A822,A854; end; end; hence contradiction; end; suppose A855: i1 = i2 & j1+1 = j2 & i19 = i29+1 & j19 = j29; now per cases by A836,A839,A841,A843,A849,A847,A844,A850,A820,A822 ,A827,A831,A829,A826,A832,A855,GOBOARD7:21; suppose i1 = i29 & j19 = j1; hence contradiction by A747,A759,A818,A839,A822,A855; end; suppose i1 = i29 & j1+1 = j19; hence contradiction by A739,A758,A818,A833,A841,A822,A855; end; suppose i1 = i29+1 & j19 = j1; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A855; end; suppose i1 = i29+1 & j1+1 = j19; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A855; end; end; hence contradiction; end; suppose A856: i1 = i2 & j1+1 = j2 & i19 = i29 & j19 = j29+1; then A857: i1 = i19 by A836,A839,A841,A843,A849,A847,A844,A850,A820,A822,A824 ,A827,A829,A828,A832,GOBOARD7:19; now per cases by A836,A839,A841,A843,A849,A847,A844,A850,A820,A822 ,A824,A827,A829,A828,A832,A856,GOBOARD7:22; suppose j1 = j29; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A856 ,A857; end; suppose j1 = j29+1; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A856,A857; end; suppose j1+1 = j29; hence contradiction by A739,A758,A818,A833,A841,A822,A856,A857; end; end; hence contradiction; end; suppose A858: i1+1 = i2 & j1 = j2 & i19 = i29 & j19+1 = j29; now per cases by A836,A839,A841,A843,A847,A845,A848,A850,A820,A822 ,A824,A827,A831,A825,A832,A858,GOBOARD7:21; suppose i19 = i1 & j1 = j19; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820; end; suppose i19 = i1 & j19+1 = j1; hence contradiction by A747,A759,A818,A839,A822,A858; end; suppose i19 = i1+1 & j1 = j19; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A858; end; suppose i19 = i1+1 & j19+1 = j1; hence contradiction by A739,A758,A818,A833,A841,A822,A858; end; end; hence contradiction; end; suppose A859: i1+1 = i2 & j1 = j2 & i19+1 = i29 & j19 = j29; then A860: j1 = j19 by A836,A839,A841,A843,A847,A845,A848,A850,A820,A822,A824 ,A831,A829,A830,A832,GOBOARD7:20; now per cases by A836,A839,A841,A843,A847,A845,A848,A850,A820,A822 ,A824,A831,A829,A830,A832,A859,GOBOARD7:23; suppose i1 = i19; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A860; end; suppose i1 = i19+1; hence contradiction by A747,A759,A818,A839,A822,A859,A860; end; suppose i1+1 = i19; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A859 ,A860; end; end; hence contradiction; end; suppose A861: i1+1 = i2 & j1 = j2 & i19 = i29+1 & j19 = j29; then A862: j1 = j19 by A836,A839,A841,A843,A847,A845,A848,A850,A820,A822,A827 ,A831,A829,A826,A832,GOBOARD7:20; now per cases by A836,A839,A841,A843,A847,A845,A848,A850,A820,A822 ,A827,A831,A829,A826,A832,A861,GOBOARD7:23; suppose i1 = i29; hence contradiction by A747,A759,A818,A839,A822,A861,A862; end; suppose i1 = i29+1; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A861,A862; end; suppose i1+1 = i29; hence contradiction by A739,A758,A818,A833,A841,A822,A861,A862; end; end; hence contradiction; end; suppose A863: i1+1 = i2 & j1 = j2 & i19 = i29 & j19 = j29+1; now per cases by A836,A839,A841,A843,A847,A845,A848,A850,A820,A822 ,A824,A827,A829,A828,A832,A863,GOBOARD7:21; suppose i19 = i1 & j1 = j29; hence contradiction by A747,A759,A818,A839,A822,A863; end; suppose i19 = i1 & j29+1 = j1; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A863; end; suppose i19 = i1+1 & j1 = j29; hence contradiction by A739,A758,A818,A833,A841,A822,A863; end; suppose i19 = i1+1 & j29+1 = j1; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A863; end; end; hence contradiction; end; suppose A864: i1 = i2+1 & j1 = j2 & i19 = i29 & j19+1 = j29; now per cases by A836,A839,A841,A849,A847,A845,A851,A850,A820,A822 ,A824,A827,A831,A825,A832,A864,GOBOARD7:21; suppose i19 = i2 & j19 = j1; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A864; end; suppose i19 = i2 & j19+1 = j1; hence contradiction by A739,A758,A818,A833,A841,A822,A864; end; suppose i19 = i2+1 & j19 = j1; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A864; end; suppose i19 = i2+1 & j19+1 = j1; hence contradiction by A747,A759,A818,A839,A822,A864; end; end; hence contradiction; end; suppose A865: i1 = i2+1 & j1 = j2 & i19+1 = i29 & j19 = j29; then A866: j1 = j19 by A836,A839,A841,A849,A847,A845,A851,A850,A820,A822,A824 ,A831,A829,A830,A832,GOBOARD7:20; now per cases by A836,A839,A841,A849,A847,A845,A851,A850,A820,A822 ,A824,A831,A829,A830,A832,A865,GOBOARD7:23; suppose i2 = i19; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A865 ,A866; end; suppose i2 = i19+1; hence contradiction by A739,A758,A818,A833,A841,A822,A865,A866; end; suppose i2+1 = i19; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A865,A866; end; end; hence contradiction; end; suppose A867: i1 = i2+1 & j1 = j2 & i19 = i29+1 & j19 = j29; then A868: j1 = j19 by A836,A839,A841,A849,A847,A845,A851,A850,A820,A822,A827 ,A831,A829,A826,A832,GOBOARD7:20; now per cases by A836,A839,A841,A849,A847,A845,A851,A850,A820,A822 ,A827,A831,A829,A826,A832,A867,GOBOARD7:23; suppose i2 = i29; hence contradiction by A739,A758,A818,A833,A841,A822,A867,A868; end; suppose i2 = i29+1; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A867 ,A868; end; suppose i2+1 = i29; hence contradiction by A747,A759,A818,A839,A822,A867,A868; end; end; hence contradiction; end; suppose A869: i1 = i2+1 & j1 = j2 & i19 = i29 & j19 = j29+1; now per cases by A836,A839,A841,A849,A847,A845,A851,A850,A820,A822 ,A824,A827,A829,A828,A832,A869,GOBOARD7:21; suppose i19 = i2 & j29 = j1; hence contradiction by A739,A758,A818,A833,A841,A822,A869; end; suppose i19 = i2 & j29+1 = j1; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A869; end; suppose i19 = i2+1 & j29 = j1; hence contradiction by A747,A759,A818,A839,A822,A869; end; suppose i19 = i2+1 & j29+1 = j1; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A869; end; end; hence contradiction; end; suppose A870: i1 = i2 & j1 = j2+1 & i19 = i29 & j19+1 = j29; then A871: i1 = i19 by A836,A839,A841,A843,A849,A845,A846,A850,A820,A822,A824 ,A827,A831,A825,A832,GOBOARD7:19; now per cases by A836,A839,A841,A843,A849,A845,A846,A850,A820,A822 ,A824,A827,A831,A825,A832,A870,GOBOARD7:22; suppose j2 = j19; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A870 ,A871; end; suppose j2 = j19+1; hence contradiction by A739,A758,A818,A833,A841,A822,A870,A871; end; suppose j2+1 = j19; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A870,A871; end; end; hence contradiction; end; suppose A872: i1 = i2 & j1 = j2+1 & i19+1 = i29 & j19 = j29; now per cases by A836,A839,A841,A843,A849,A845,A846,A850,A820,A822 ,A824,A831,A829,A830,A832,A872,GOBOARD7:21; suppose i1 = i19 & j2 = j19; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A872; end; suppose i1 = i19 & j2+1 = j19; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A872; end; suppose i1 = i19+1 & j2 = j19; hence contradiction by A739,A758,A818,A833,A841,A822,A872; end; suppose i1 = i19+1 & j2+1 = j19; hence contradiction by A747,A759,A818,A839,A822,A872; end; end; hence contradiction; end; suppose A873: i1 = i2 & j1 = j2+1 & i19 = i29+1 & j19 = j29; now per cases by A836,A839,A841,A843,A849,A845,A846,A850,A820,A822 ,A827,A831,A829,A826,A832,A873,GOBOARD7:21; suppose i1 = i29 & j2 = j19; hence contradiction by A739,A758,A818,A833,A841,A822,A873; end; suppose i1 = i29 & j2+1 = j19; hence contradiction by A747,A759,A818,A839,A822,A873; end; suppose i1 = i29+1 & j2 = j19; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A873; end; suppose i1 = i29+1 & j2+1 = j19; hence contradiction by A711,A753,A757,A755,A818,A837,A834,A839,A820 ,A873; end; end; hence contradiction; end; suppose A874: i1 = i2 & j1 = j2+1 & i19 = i29 & j19 = j29+1; then A875: i1 = i19 by A836,A839,A841,A843,A849,A845,A846,A850,A820,A822,A824 ,A827,A829,A828,A832,GOBOARD7:19; now per cases by A836,A839,A841,A843,A849,A845,A846,A850,A820,A822 ,A824,A827,A829,A828,A832,A874,GOBOARD7:22; suppose j2 = j29; hence contradiction by A739,A758,A818,A833,A841,A822,A874,A875; end; suppose j2 = j29+1; hence contradiction by A711,A753,A756,A755,A835,A834,A841,A820,A874 ,A875; end; suppose j2+1 = j29; hence contradiction by A747,A759,A818,A839,A822,A874,A875; end; end; hence contradiction; end; end; hence contradiction; end; end; then reconsider g as standard non constant special_circular_sequence by A651,A738,A702,A705 ,A707,FINSEQ_6:def 1,JORDAN8:4; reconsider Lg9 = (L~g)` as Subset of TOP-REAL 2; A876: C c= Lg9 proof let c be object; assume that A877: c in C and A878: not c in Lg9; reconsider c as Point of TOP-REAL 2 by A877; consider i such that A879: 1 <= i and A880: i+1 <= len g and A881: c in LSeg(g/.i,g/.(i+1)) by A878,SPPOL_2:14,SUBSET_1:29; A882: 1 <= i+(m-'1) by A879,NAT_1:12; i+1 in dom g by A879,A880,SEQ_4:134; then A883: g/.(i+1) = f/.(i+1+(m-'1)) by FINSEQ_5:27; i+1+(m-'1) = i+(m-'1)+1; then A884: i+(m-'1)+1 <= (len g)+(m-'1) by A880,XREAL_1:6; i in dom g by A879,A880,SEQ_4:134; then g/.i = f/.(i+(m-'1)) by FINSEQ_5:27; then c in LSeg(f,i+(m-'1)) by A701,A881,A883,A882,A884,TOPREAL1:def 3; then c in right_cell(f,i+(m-'1),G) /\ left_cell(f,i+(m-'1),G) by A440 ,A701,A882,A884,GOBRD13:29; then c in right_cell(f,i+(m-'1),G) by XBOOLE_0:def 4; then right_cell(f,i+(m-'1),G) meets C by A877,XBOOLE_0:3; hence contradiction by A440,A701,A882,A884; end; A885: LeftComp g is_a_component_of (L~g)` by GOBOARD9:def 1; (L~g)` is open by TOPS_1:3; then A886: (L~g)` = Int (L~g)` by TOPS_1:23; A887: C meets LeftComp g proof left_cell(f,m,G) meets C by A440,A652,A659; then consider p being object such that A888: p in left_cell(f,m,G) and A889: p in C by XBOOLE_0:3; reconsider p as Element of TOP-REAL 2 by A888; now reconsider u = p as Element of Euclid 2 by TOPREAL3:8; take p; thus p in C by A889; A890: Int left_cell(g,1) c= LeftComp g by A704,GOBOARD9:21; Int left_cell(g,1,G) c= Int left_cell(g,1) by A705,A704,GOBRD13:33 ,TOPS_1:19; then Int left_cell(g,1,G) c= LeftComp g by A890; then Int left_cell(f,m-'1+1,G) c= LeftComp g by A653,A700,A704, GOBRD13:32; then A891: Int left_cell(f,m,G) c= LeftComp g by A652,XREAL_1:235; consider r being Real such that A892: r > 0 and A893: Ball(u,r) c= (L~g)` by A876,A886,A889,GOBOARD6:5; reconsider r as Real; reconsider B = Ball(u,r) as non empty Subset of TOP-REAL 2 by A4,A892, TBSP_1:11,TOPMETR:12; A894: B is open by GOBOARD6:3; A895: left_cell(f,m,G) = Cl Int left_cell(f,m,G) by A652,A659,A680; p in Ball(u,r) by A892,TBSP_1:11; then A896: Int left_cell(f,m,G) meets B by A888,A895,A894,TOPS_1:12; A897: p in B by A892,TBSP_1:11; B is connected by SPRECT_3:7; then B c= LeftComp g by A885,A893,A891,A896,GOBOARD9:4; hence p in LeftComp g by A897; end; hence thesis by XBOOLE_0:3; end; A898: L~g c= L~f by JORDAN3:40; A899: RightComp g is_a_component_of (L~g)` by GOBOARD9:def 2; m = 1 proof A900: for n st 1 <= n holds n-'1+2 = n+1 proof let n; assume 1 <= n; hence n-'1+2 = n+2-'1 by NAT_D:38 .= n+1+1 - 1 by NAT_D:37 .= n+1; end; assume m <> 1; then A901: 1 < m by A652,XXREAL_0:1; A902: for n st 1 <= n & n <= m-'1 holds not f/.n in L~g proof A903: 2 <= len G by A2,NAT_1:12; let n such that A904: 1 <= n and A905: n <= m-'1; set p = f/.n; A906: n <= len f by A700,A905,XXREAL_0:2; then A907: p in Values G by A440,A904,JORDAN9:6; assume p in L~g; then consider j such that A908: m-'1+1 <= j and A909: j+1 <= len f and A910: p in LSeg(f,j) by A700,JORDAN9:7; A911: j+1 <= k by A177,A909; A912: j < k by A710,A909,NAT_1:13; A913: n < m-'1+1 by A905,NAT_1:13; then A914: n < j by A908,XXREAL_0:2; A915: m-'1+1=m by A652,XREAL_1:235; then A916: 1 < j by A901,A908,XXREAL_0:2; per cases by A6,A440,A909,A910,A916,A903,A907,JORDAN9:23; suppose A917: p = f/.j; A918: n <> len(F.j) by A177,A908,A913; n <= len(F.j) by A177,A914; then A919: n in dom(F.j) by A904,FINSEQ_3:25; (F.j)/.n = (F.n)/.n by A566,A904,A914 .= p by A710,A566,A904,A906 .= (F.j)/.j by A566,A916,A912,A917 .= (F.j)/.len(F.j) by A177; hence contradiction by A648,A916,A912,A919,A918; end; suppose A920: p = f/.(j+1); now per cases by A911,XXREAL_0:1; suppose A921: j+1 = k; A922: n <> len(F.m) by A177,A913,A915; n <= len(F.m) by A177,A913,A915; then A923: n in dom(F.m) by A904,FINSEQ_3:25; (F.m)/.n = (F.n)/.n by A566,A904,A913,A915 .= p by A710,A566,A904,A906 .= (F.m)/.m by A651,A710,A652,A654,A566,A920,A921 .= (F.m)/.len(F.m) by A177; hence contradiction by A648,A710,A652,A655,A923,A922; end; suppose A924: j+1 < k; set l = j+1; A925: 1 <= l by NAT_1:11; A926: n < n+1 by XREAL_1:29; A927: n+1 < l by A914,XREAL_1:6; then A928: n <> len(F.l) by A177,A926; A929: n < l by A926,A927,XXREAL_0:2; then n <= len(F.l) by A177; then A930: n in dom(F.l) by A904,FINSEQ_3:25; (F.l)/.n = (F.n)/.n by A566,A904,A929 .= p by A710,A566,A904,A906 .= (F.l)/.l by A566,A920,A924,A925 .= (F.l)/.len(F.l) by A177; hence contradiction by A648,A924,A930,A928,NAT_1:11; end; end; hence contradiction; end; end; C meets LeftComp Rev g proof 1 <= len g by A704,XREAL_1:145; then A931: len g-'1+2 = len g+1 by A900; A932: 1 - 1 < m - 1 by A901,XREAL_1:9; A933: m-'1+2 = m+1 by A652,A900; set l = (m-'1)+(len g-'1); set a = f/.(m-'1); set rg = Rev g; set p = rg/.1, q = rg/.2; A934: 1+1 - 1 <= len g - 1 by A703,XREAL_1:9; 1+1-'1 <= len g-'1 by A703,NAT_D:42; then A935: 1 <= len g-'1 by NAT_D:34; then (m-'1)+1 <= l by XREAL_1:6; then m-'1 < l by NAT_1:13; then A936: m-'1 <> len(F.l) by A177; A937: 1+1 <= len rg by A703,FINSEQ_5:def 3; then 1+1-'1 <= len rg-'1 by NAT_D:42; then A938: 1 <= len rg -'1 by NAT_D:34; A939: rg is_sequence_on G by A705,JORDAN9:5; then consider p1,p2,q1,q2 being Nat such that A940: [p1,p2] in Indices G and A941: p = G*(p1,p2) and A942: [q1,q2] in Indices G and A943: q = G*(q1,q2) and A944: p1 = q1 & p2+1 = q2 or p1+1 = q1 & p2 = q2 or p1 = q1+1 & p2 = q2 or p1 = q1 & p2 = q2+1 by A937,JORDAN8:3; A945: 1 <= p1 by A940,MATRIX_0:32; A946: p2 <= width G by A940,MATRIX_0:32; A947: p1 <= len G by A940,MATRIX_0:32; A948: 1 <= p2 by A940,MATRIX_0:32; A949: p = f/.m by A651,A702,FINSEQ_5:65; len g-'1 <= len g by NAT_D:44; then A950: len g-'1 in dom g by A935,FINSEQ_3:25; then A951: q = g/.(len g -'1) by A931,FINSEQ_5:66 .= f/.l by A950,FINSEQ_5:27; 1 < len rg by A937,NAT_1:13; then A952: len rg -'1+1 = len rg by XREAL_1:235; A953: l = m+(len g -'1)-'1 by A652,NAT_D:38 .= (len g -'1)+m - 1 by A935,NAT_D:37 .= (len g - 1)+m - 1 by A934,XREAL_0:def 2 .= ((k - (m - 1)) - 1)+m - 1 by A710,A701,A932,XREAL_0:def 2 .= k - 1; then A954: p = f/.(l+1) by A710,A702,FINSEQ_5:65; A955: m-'1+1 = m by A652,XREAL_1:235; then A956: 1 <= m-'1 by A901,NAT_1:13; then A957: left_cell(f,m-'1,G) meets C by A440,A654,A955; m-'1 <= l by NAT_1:11; then m-'1 <= len(F.l) by A177; then A958: m-'1 in dom(F.l) by A956,FINSEQ_3:25; not a in L~g by A902,A956; then A959: not a in L~rg by SPPOL_2:22; A960: k = l+1 by A953; then A961: l < k by XREAL_1:29; len g-'1 <= l by NAT_1:11; then A962: 1 <= l by A935,XXREAL_0:2; then A963: left_cell(f,l,G) meets C by A440,A710,A960; per cases by A944; suppose A964: p1 = q1 & p2+1 = q2; consider a1,a2,p91,p92 being Nat such that A965: [a1,a2] in Indices G and A966: a = G*(a1,a2) and A967: [p91,p92] in Indices G and A968: p = G*(p91,p92) and A969: a1 = p91 & a2+1 = p92 or a1+1 = p91 & a2 = p92 or a1 = p91+1 & a2 = p92 or a1 = p91 & a2 = p92+1 by A653,A654,A949,A955,A956,JORDAN8:3 ; A970: 1 <= a2 by A965,MATRIX_0:32; thus thesis proof per cases by A969; suppose A971: a1 = p91 & a2+1 = p92; A972: m-'1 <= m by A955,NAT_1:11; A973: f/.(m-'1) = (F.(m-'1))/.(m-'1) by A710,A700,A566,A956 .= (F.m)/.(m-'1) by A566,A956,A972; A974: 2 in dom g by A703,FINSEQ_3:25; len rg-'1+2 = len g +1 by A931,FINSEQ_5:def 3; then A975: rg/.(len rg -' 1) = g/.2 by A974,FINSEQ_5:66 .= f/.(m+1) by A933,A974,FINSEQ_5:27; A976: L~rg c= L~f by A898,SPPOL_2:22; A977: p = g/.1 by A651,A738,A702,FINSEQ_5:65 .= rg/.len g by FINSEQ_5:65 .= rg/.len rg by FINSEQ_5:def 3; A978: F.k|(m+1)=F.(m+1) by A565,A710,A659; A979: a1 = p1 by A940,A941,A967,A968,A971,GOBOARD1:5; A980: f/.(m-'1+1) = (F.m)/.m by A710,A652,A654,A566,A955; A981: m-'1+1 <= len (F.m) by A177,A955; set rc = left_cell(rg,len rg-'1,G)\L~rg; A982: a2+1 > a2 by NAT_1:13; A983: a2+1 = p2 by A940,A941,A967,A968,A971,GOBOARD1:5; then A984: p2-'1 = a2 by NAT_D:34; left_cell(f,l,G) = cell(G,p1,p2) by A440,A710,A953,A962,A951,A954 ,A940,A941,A942,A943,A964,GOBRD13:27 .= front_right_cell(F.m,m-'1,G) by A440,A949,A955,A956,A940 ,A941,A965,A966,A979,A983,A981,A973,A980,GOBRD13:35; then F.(m+1) turns_right m-'1,G by A514,A901,A963; then A985: f turns_right m-'1,G by A956,A933,A978,GOBRD13:43; A986: p2+1 > a2+1 by A983,NAT_1:13; then A987: [p1+1,p2] in Indices G by A949,A955,A940,A941,A965,A966,A982,A985 ,GOBRD13:def 6; then A988: p1+1 <= len G by MATRIX_0:32; f/.(m+1) = G*(p1+1,p2) by A949,A955,A933,A940,A941,A965,A966,A986 ,A982,A985,GOBRD13:def 6; then left_cell(rg,len rg-'1,G) = cell(G,p1,a2) by A939,A938,A952 ,A940,A941,A987,A984,A975,A977,GOBRD13:25; then a in left_cell(rg,len rg-'1,G) by A945,A946,A966,A970,A979 ,A983,A988,JORDAN9:20; then A989: a in rc by A959,XBOOLE_0:def 5; A990: LeftComp rg is_a_component_of (L~rg)` by GOBOARD9:def 1; rc c= LeftComp rg by A939,A938,A952,JORDAN9:27; hence thesis by A654,A660,A955,A956,A959,A989,A976,A990; end; suppose A991: a1+1 = p91 & a2 = p92; then a1+1 = p1 by A940,A941,A967,A968,GOBOARD1:5; then A992: q1-'1 = a1 by A964,NAT_D:34; a2 = p2 by A940,A941,A967,A968,A991,GOBOARD1:5; then right_cell(f,l,G) = cell(G,a1,a2) by A440,A710,A953,A962 ,A951,A954,A940,A941,A942,A943,A964,A992,GOBRD13:28 .= left_cell(f,m-'1,G) by A440,A654,A949,A955,A956,A965,A966 ,A967,A968,A991,GOBRD13:23; hence thesis by A440,A710,A960,A962,A957; end; suppose A993: a1 = p91+1 & a2 = p92; then A994: a2 = p2 by A940,A941,A967,A968,GOBOARD1:5; a1 = p1+1 by A940,A941,A967,A968,A993,GOBOARD1:5; then right_cell(f,m-'1,G) = cell(G,p1,p2) by A651,A653,A654,A702 ,A955,A956,A940,A941,A965,A966,A994,FINSEQ_5:65,GOBRD13:26 .= left_cell(f,l,G) by A440,A710,A953,A962,A951,A954,A940,A941 ,A942,A943,A964,GOBRD13:27; hence thesis by A440,A654,A955,A956,A963; end; suppose A995: a1 = p91 & a2 = p92+1; then A996: a2 = q2 by A940,A941,A964,A967,A968,GOBOARD1:5; A997: a1 = q1 by A940,A941,A964,A967,A968,A995,GOBOARD1:5; (F.l)/.(m-'1) = (F.(m-'1))/.(m-'1) by A566,A956,NAT_1:11 .= q by A710,A700,A566,A956,A943,A966,A997,A996 .= (F.l)/.l by A566,A961,A962,A951 .= (F.l)/.len(F.l) by A177; hence thesis by A648,A961,A962,A958,A936; end; end; end; suppose A998: p1+1 = q1 & p2 = q2; consider a1,a2,p91,p92 being Nat such that A999: [a1,a2] in Indices G and A1000: a = G*(a1,a2) and A1001: [p91,p92] in Indices G and A1002: p = G*(p91,p92) and A1003: a1 = p91 & a2+1 = p92 or a1+1 = p91 & a2 = p92 or a1 = p91+1 & a2 = p92 or a1 = p91 & a2 = p92+1 by A653,A654,A949,A955,A956,JORDAN8:3 ; A1004: 1 <= a2 by A999,MATRIX_0:32; A1005: a2 <= width G by A999,MATRIX_0:32; A1006: 1 <= a1 by A999,MATRIX_0:32; thus thesis proof per cases by A1003; suppose A1007: a1 = p91 & a2+1 = p92; then a2+1 = p2 by A940,A941,A1001,A1002,GOBOARD1:5; then A1008: q2-'1 = a2 by A998,NAT_D:34; A1009: a1 = p1 by A940,A941,A1001,A1002,A1007,GOBOARD1:5; right_cell(f,m-'1,G) = cell(G,a1,a2) by A440,A654,A949,A955,A956 ,A999,A1000,A1001,A1002,A1007,GOBRD13:22 .= left_cell(f,l,G) by A440,A710,A953,A962,A951,A954,A940,A941 ,A942,A943,A998,A1009,A1008,GOBRD13:25; hence thesis by A440,A654,A955,A956,A963; end; suppose A1010: a1+1 = p91 & a2 = p92; A1011: m-'1 <= m by A955,NAT_1:11; A1012: f/.(m-'1) = (F.(m-'1))/.(m-'1) by A710,A700,A566,A956 .= (F.m)/.(m-'1) by A566,A956,A1011; A1013: 2 in dom g by A703,FINSEQ_3:25; len rg-'1+2 = len g +1 by A931,FINSEQ_5:def 3; then A1014: rg/.(len rg -' 1) = g/.2 by A1013,FINSEQ_5:66 .= f/.(m+1) by A933,A1013,FINSEQ_5:27; A1015: L~rg c= L~f by A898,SPPOL_2:22; A1016: F.k|(m+1)=F.(m+1) by A565,A710,A659; A1017: m-'1+1 <= len (F.m) by A177,A955; A1018: a2 = p2 by A940,A941,A1001,A1002,A1010,GOBOARD1:5; A1019: p = g/.1 by A651,A738,A702,FINSEQ_5:65 .= rg/.len g by FINSEQ_5:65 .= rg/.len rg by FINSEQ_5:def 3; set rc = left_cell(rg,len rg-'1,G)\L~rg; A1020: p1 < p1+1 by XREAL_1:29; A1021: f/.(m-'1+1) = (F.m)/.m by A710,A652,A654,A566,A955; A1022: a2-'1+1 = a2 by A1004,XREAL_1:235; A1023: a1+1 = p1 by A940,A941,A1001,A1002,A1010,GOBOARD1:5; then A1024: a1 = p1-'1 by NAT_D:34; left_cell(f,l,G) = cell(G,p1,p2-'1) by A440,A710,A953,A962,A951 ,A954,A940,A941,A942,A943,A998,GOBRD13:25 .= front_right_cell(F.m,m-'1,G) by A440,A949,A955,A956,A940 ,A941,A999,A1000,A1023,A1018,A1017,A1012,A1021,GOBRD13:37; then F.(m+1) turns_right m-'1,G by A514,A901,A963; then A1025: f turns_right m-'1,G by A956,A933,A1016,GOBRD13:43; A1026: a1 < a1+1 by XREAL_1:29; then A1027: [p1,p2-'1] in Indices G by A949,A955,A940,A941,A999,A1000,A1023 ,A1020,A1025,GOBRD13:def 6; then A1028: 1 <= a2-'1 by A1018,MATRIX_0:32; f/.(m+1) = G*(p1,p2-'1) by A949,A955,A933,A940,A941,A999,A1000 ,A1023,A1026,A1020,A1025,GOBRD13:def 6; then left_cell(rg,len rg-'1,G) = cell(G,a1,a2-'1) by A939,A938 ,A952,A940,A941,A1018,A1027,A1024,A1014,A1022,A1019,GOBRD13:21; then a in left_cell(rg,len rg-'1,G) by A947,A1000,A1006,A1005 ,A1023,A1022,A1028,JORDAN9:20; then A1029: a in rc by A959,XBOOLE_0:def 5; A1030: LeftComp rg is_a_component_of (L~rg)` by GOBOARD9:def 1; rc c= LeftComp rg by A939,A938,A952,JORDAN9:27; hence thesis by A654,A660,A955,A956,A959,A1029,A1015,A1030; end; suppose A1031: a1 = p91+1 & a2 = p92; then A1032: a2 = q2 by A940,A941,A998,A1001,A1002,GOBOARD1:5; A1033: a1 = q1 by A940,A941,A998,A1001,A1002,A1031,GOBOARD1:5; (F.l)/.(m-'1) = (F.(m-'1))/.(m-'1) by A566,A956,NAT_1:11 .= q by A710,A700,A566,A956,A943,A1000,A1033,A1032 .= (F.l)/.l by A566,A961,A962,A951 .= (F.l)/.len(F.l) by A177; hence thesis by A648,A961,A962,A958,A936; end; suppose A1034: a1 = p91 & a2 = p92+1; then A1035: a2 = p2+1 by A940,A941,A1001,A1002,GOBOARD1:5; A1036: a1 = p1 by A940,A941,A1001,A1002,A1034,GOBOARD1:5; right_cell(f,l,G) = cell(G,p1,p2) by A440,A710,A953,A962,A951 ,A954,A940,A941,A942,A943,A998,GOBRD13:26 .= left_cell(f,m-'1,G) by A651,A653,A654,A702,A955,A956,A940 ,A941,A999,A1000,A1036,A1035,FINSEQ_5:65,GOBRD13:27; hence thesis by A440,A710,A960,A962,A957; end; end; end; suppose A1037: p1 = q1+1 & p2 = q2; consider a1,a2,p91,p92 being Nat such that A1038: [a1,a2] in Indices G and A1039: a = G*(a1,a2) and A1040: [p91,p92] in Indices G and A1041: p = G*(p91,p92) and A1042: a1 = p91 & a2+1 = p92 or a1+1 = p91 & a2 = p92 or a1 = p91+1 & a2 = p92 or a1 = p91 & a2 = p92+1 by A653,A654,A949,A955,A956,JORDAN8:3 ; A1043: a1 <= len G by A1038,MATRIX_0:32; thus thesis proof per cases by A1042; suppose A1044: a1 = p91 & a2+1 = p92; then a2+1 = p2 by A940,A941,A1040,A1041,GOBOARD1:5; then A1045: q2-'1 = a2 by A1037,NAT_D:34; a1 = p1 by A940,A941,A1040,A1041,A1044,GOBOARD1:5; then A1046: q1 = a1-'1 by A1037,NAT_D:34; right_cell(f,l,G) = cell(G,q1,q2-'1) by A440,A710,A953,A962,A951 ,A954,A940,A941,A942,A943,A1037,GOBRD13:24 .= left_cell(f,m-'1,G) by A440,A654,A949,A955,A956,A1038,A1039 ,A1040,A1041,A1044,A1046,A1045,GOBRD13:21; hence thesis by A440,A710,A960,A962,A957; end; suppose A1047: a1+1 = p91 & a2 = p92; then A1048: a2 = p2 by A940,A941,A1040,A1041,GOBOARD1:5; A1049: a1+1 = p1 by A940,A941,A1040,A1041,A1047,GOBOARD1:5; (F.l)/.(m-'1) = (F.(m-'1))/.(m-'1) by A566,A956,NAT_1:11 .= q by A710,A700,A566,A956,A943,A1037,A1039,A1049,A1048 .= (F.l)/.l by A566,A961,A962,A951 .= (F.l)/.len(F.l) by A177; hence thesis by A648,A961,A962,A958,A936; end; suppose A1050: a1 = p91+1 & a2 = p92; A1051: m-'1 <= m by A955,NAT_1:11; A1052: f/.(m-'1) = (F.(m-'1))/.(m-'1) by A710,A700,A566,A956 .= (F.m)/.(m-'1) by A566,A956,A1051; A1053: 2 in dom g by A703,FINSEQ_3:25; len rg-'1+2 = len g +1 by A931,FINSEQ_5:def 3; then A1054: rg/.(len rg -' 1) = g/.2 by A1053,FINSEQ_5:66 .= f/.(m+1) by A933,A1053,FINSEQ_5:27; A1055: L~rg c= L~f by A898,SPPOL_2:22; set rc = left_cell(rg,len rg-'1,G)\L~rg; A1056: LeftComp rg is_a_component_of (L~rg)` by GOBOARD9:def 1; A1057: p1-'1 = q1 by A1037,NAT_D:34; A1058: F.k|(m+1)=F.(m+1) by A565,A710,A659; A1059: a1 = p1+1 by A940,A941,A1040,A1041,A1050,GOBOARD1:5; A1060: f/.(m-'1+1) = (F.m)/.m by A710,A652,A654,A566,A955; A1061: m-'1+1 <= len (F.m) by A177,A955; A1062: a2 = p2 by A940,A941,A1040,A1041,A1050,GOBOARD1:5; left_cell(f,l,G) = cell(G,q1,q2) by A440,A710,A953,A962,A951,A954 ,A940,A941,A942,A943,A1037,GOBRD13:23 .= front_right_cell(F.m,m-'1,G) by A440,A949,A955,A956,A940 ,A941,A1037,A1038,A1039,A1059,A1062,A1057,A1061,A1052,A1060,GOBRD13:39; then F.(m+1) turns_right m-'1,G by A514,A901,A963; then A1063: f turns_right m-'1,G by A956,A933,A1058,GOBRD13:43; p1+1>p1 by XREAL_1:29; then A1064: a1+1 > p1 by A1059,NAT_1:13; then A1065: [p1,p2+1] in Indices G by A949,A955,A940,A941,A1038,A1039,A1062 ,A1063,GOBRD13:def 6; then A1066: p2+1 <= width G by MATRIX_0:32; a2+1 > p2 by A1062,NAT_1:13; then A1067: f/.(m+1) = G*(p1,p2+1) by A949,A955,A933,A940,A941,A1038,A1039 ,A1062,A1064,A1063,GOBRD13:def 6; p = g/.1 by A651,A738,A702,FINSEQ_5:65 .= rg/.len g by FINSEQ_5:65 .= rg/.len rg by FINSEQ_5:def 3; then left_cell(rg,len rg-'1,G) = cell(G,p1,p2) by A939,A938,A952 ,A940,A941,A1067,A1065,A1054,GOBRD13:27; then a in left_cell(rg,len rg-'1,G) by A945,A948,A1039,A1043 ,A1059,A1062,A1066,JORDAN9:20; then A1068: a in rc by A959,XBOOLE_0:def 5; rc c= LeftComp rg by A939,A938,A952,JORDAN9:27; hence thesis by A654,A660,A955,A956,A959,A1068,A1055,A1056; end; suppose A1069: a1 = p91 & a2 = p92+1; then a1 = p1 by A940,A941,A1040,A1041,GOBOARD1:5; then A1070: q1 = a1-'1 by A1037,NAT_D:34; a2 = p2+1 by A940,A941,A1040,A1041,A1069,GOBOARD1:5; then right_cell(f,m-'1,G) = cell(G,q1,q2) by A651,A653,A654,A702 ,A955,A956,A1037,A1038,A1039,A1040,A1041,A1069,A1070,FINSEQ_5:65,GOBRD13:28 .= left_cell(f,l,G) by A440,A710,A953,A962,A951,A954,A940,A941 ,A942,A943,A1037,GOBRD13:23; hence thesis by A440,A654,A955,A956,A963; end; end; end; suppose A1071: p1 = q1 & p2 = q2+1; consider a1,a2,p91,p92 being Nat such that A1072: [a1,a2] in Indices G and A1073: a = G*(a1,a2) and A1074: [p91,p92] in Indices G and A1075: p = G*(p91,p92) and A1076: a1 = p91 & a2+1 = p92 or a1+1 = p91 & a2 = p92 or a1 = p91+1 & a2 = p92 or a1 = p91 & a2 = p92+1 by A653,A654,A949,A955,A956,JORDAN8:3 ; A1077: a2 <= width G by A1072,MATRIX_0:32; thus thesis proof per cases by A1076; suppose A1078: a1 = p91 & a2+1 = p92; then A1079: a2+1 = p2 by A940,A941,A1074,A1075,GOBOARD1:5; A1080: a1 = p1 by A940,A941,A1074,A1075,A1078,GOBOARD1:5; (F.l)/.(m-'1) = (F.(m-'1))/.(m-'1) by A566,A956,NAT_1:11 .= q by A710,A700,A566,A956,A943,A1071,A1073,A1080,A1079 .= (F.l)/.l by A566,A961,A962,A951 .= (F.l)/.len(F.l) by A177; hence thesis by A648,A961,A962,A958,A936; end; suppose A1081: a1+1 = p91 & a2 = p92; then a2 = p2 by A940,A941,A1074,A1075,GOBOARD1:5; then A1082: a2-'1 = q2 by A1071,NAT_D:34; a1+1 = p1 by A940,A941,A1074,A1075,A1081,GOBOARD1:5; then A1083: a1 = q1-'1 by A1071,NAT_D:34; right_cell(f,m-'1,G) = cell(G,a1,a2-'1) by A440,A654,A949,A955 ,A956,A1072,A1073,A1074,A1075,A1081,GOBRD13:24 .= left_cell(f,l,G) by A440,A710,A953,A962,A951,A954,A940,A941 ,A942,A943,A1071,A1083,A1082,GOBRD13:21; hence thesis by A440,A654,A955,A956,A963; end; suppose A1084: a1 = p91+1 & a2 = p92; then a2 = p2 by A940,A941,A1074,A1075,GOBOARD1:5; then A1085: a2-'1 = q2 by A1071,NAT_D:34; A1086: a1 = p1+1 by A940,A941,A1074,A1075,A1084,GOBOARD1:5; right_cell(f,l,G) = cell(G,q1,q2) by A440,A710,A953,A962,A951 ,A954,A940,A941,A942,A943,A1071,GOBRD13:22 .= left_cell(f,m-'1,G) by A651,A653,A654,A702,A955,A956,A1071 ,A1072,A1073,A1074,A1075,A1084,A1086,A1085,FINSEQ_5:65,GOBRD13:25; hence thesis by A440,A710,A960,A962,A957; end; suppose A1087: a1 = p91 & a2 = p92+1; then A1088: a2 = p2+1 by A940,A941,A1074,A1075,GOBOARD1:5; A1089: f/.(m-'1+1) = (F.m)/.m by A710,A652,A654,A566,A955; A1090: 2 in dom g by A703,FINSEQ_3:25; len rg-'1+2 = len g +1 by A931,FINSEQ_5:def 3; then A1091: rg/.(len rg -' 1) = g/.2 by A1090,FINSEQ_5:66 .= f/.(m+1) by A933,A1090,FINSEQ_5:27; A1092: p1-'1+1 = p1 by A945,XREAL_1:235; A1093: m-'1 <= m by A955,NAT_1:11; A1094: f/.(m-'1) = (F.(m-'1))/.(m-'1) by A710,A700,A566,A956 .= (F.m)/.(m-'1) by A566,A956,A1093; A1095: p2-'1 = q2 by A1071,NAT_D:34; set rc = left_cell(rg,len rg-'1,G)\L~rg; A1096: p2+1>p2 by NAT_1:13; A1097: p = g/.1 by A651,A738,A702,FINSEQ_5:65 .= rg/.len g by FINSEQ_5:65 .= rg/.len rg by FINSEQ_5:def 3; A1098: m-'1+1 <= len (F.m) by A177,A955; A1099: F.k|(m+1)=F.(m+1) by A565,A710,A659; A1100: L~rg c= L~f by A898,SPPOL_2:22; A1101: a1 = p1 by A940,A941,A1074,A1075,A1087,GOBOARD1:5; left_cell(f,l,G) = cell(G,q1-'1,q2) by A440,A710,A953,A962,A951 ,A954,A940,A941,A942,A943,A1071,GOBRD13:21 .= front_right_cell(F.m,m-'1,G) by A440,A949,A955,A956,A940 ,A941,A1071,A1072,A1073,A1101,A1088,A1095,A1098,A1094,A1089,GOBRD13:41; then F.(m+1) turns_right m-'1,G by A514,A901,A963; then A1102: f turns_right m-'1,G by A956,A933,A1099,GOBRD13:43; A1103: a2+1>p2+1 by A1088,NAT_1:13; then A1104: [p1-'1,p2] in Indices G by A949,A955,A940,A941,A1072,A1073,A1096 ,A1102,GOBRD13:def 6; then A1105: 1 <= p1-'1 by MATRIX_0:32; f/.(m+1) = G*(p1-'1,p2) by A949,A955,A933,A940,A941,A1072,A1073 ,A1103,A1096,A1102,GOBRD13:def 6; then left_cell(rg,len rg-'1,G) = cell(G,p1-'1,p2) by A939,A938 ,A952,A940,A941,A1104,A1091,A1097,A1092,GOBRD13:23; then a in left_cell(rg,len rg-'1,G) by A947,A948,A1073,A1077 ,A1101,A1088,A1105,A1092,JORDAN9:20; then A1106: a in rc by A959,XBOOLE_0:def 5; A1107: LeftComp rg is_a_component_of (L~rg)` by GOBOARD9:def 1; rc c= LeftComp rg by A939,A938,A952,JORDAN9:27; hence thesis by A654,A660,A955,A956,A959,A1106,A1100,A1107; end; end; end; end; then C meets RightComp g by GOBOARD9:23; hence contradiction by A876,A885,A899,A887,JORDAN9:1,SPRECT_4:6; end; then A1108: g = f/^0 by XREAL_1:232 .= f by FINSEQ_5:28; then reconsider f as standard non constant special_circular_sequence; F.(0+1) = <*G*(XS,YS)*> by A156; then A1109: G*(XS,YS) = (F.1)/.1 by FINSEQ_4:16 .= f/.1 by A647,A566; F.(1+1) = <*G*(XS,YS),G*(XS-'1,YS)*> by A156; then A1110: G*(XS-'1,YS) = (F.2)/.2 by FINSEQ_4:17 .= f/.2 by A657,A566; A1111: 2 < XS by JORDAN1H:49; f is clockwise_oriented proof LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1; then C c= LeftComp f by A876,A887,A1108,GOBOARD9:4; then RightComp f misses C by GOBRD14:14,XBOOLE_1:63; then A1112: RightComp f c= C` by SUBSET_1:23; UBD L~f is_outside_component_of L~f by JORDAN2C:68; then UBD L~f is_a_component_of (L~f)` by JORDAN2C:def 3; then A1113: UBD L~f = RightComp f or UBD L~f = LeftComp f by JORDAN1H:24; A1114: XS-'1+1 = XS by A1111,XREAL_1:235,XXREAL_0:2; set W = {B where B is Subset of TOP-REAL 2: B is_inside_component_of C}; A1115: Int right_cell(f,1,G) c= right_cell(f,1,G) by TOPS_1:16; A1116: BDD C = union W by JORDAN2C:def 4; A1117: Int right_cell(f,1,G) <> {} by A653,A656,JORDAN9:9; A1118: [XS-'1,YS] in Indices G by A1,JORDAN11:9; cell(G,XS-'1,YS) c= BDD C by A1,JORDAN11:6; then right_cell(f,1,G) c= BDD C by A5,A440,A656,A1109,A1110,A1114,A1118, GOBRD13:26; then A1119: Int right_cell(f,1,G) c= BDD C by A1115; Int right_cell(f,1,G) c= RightComp f by A653,A656,JORDAN1H:25; then BDD C meets RightComp f by A1119,A1117,XBOOLE_1:68; then consider e being set such that A1120: e in W and A1121: RightComp f meets e by A1116,ZFMISC_1:80; consider B being Subset of TOP-REAL 2 such that A1122: e = B and A1123: B is_inside_component_of C by A1120; A1124: B is bounded by A1123,JORDAN2C:def 2; B is_a_component_of C` by A1123,JORDAN2C:def 2; then RightComp f is bounded by A1121,A1122,A1112,A1124,GOBOARD9:4 ,RLTOPSP1:42; hence thesis by A1113,JORDAN1H:39,41; end; then reconsider f as clockwise_oriented standard non constant special_circular_sequence; take f; thus f is_sequence_on G by A440; thus f/.1 = G*(XS,YS) by A1109; thus f/.2 = G*(XS-'1,YS) by A1110; let m such that A1125: 1 <= m and A1126: m+2 <= len f; A1127: F.(m+1+1) = f|(m+1+1) by A565,A710,A1126; A1128: m+1 < m+2 by XREAL_1:6; then A1129: f|(m+1) = F.(m+1) by A565,A710,A1126,XXREAL_0:2; A1130: m+1 <= len f by A1126,A1128,XXREAL_0:2; then A1131: front_right_cell(F.(m+1),m,G) = front_right_cell(f,m,G) by A653,A1125 ,A1129,GOBRD13:42; A1132: m+1 > 1 by A1125,NAT_1:13; A1133: m = m+1-'1 by NAT_D:34; A1134: front_left_cell(F.(m+1),m,G) = front_left_cell(f,m,G) by A653,A1125 ,A1130,A1129,GOBRD13:42; hereby assume that A1135: front_right_cell(f,m,G) misses C and A1136: front_left_cell(f,m,G) misses C; F.(m+1+1) turns_left m,G by A514,A1133,A1132,A1131,A1134,A1135,A1136; hence f turns_left m,G by A1125,A1126,A1127,GOBRD13:44; end; hereby assume that A1137: front_right_cell(f,m,G) misses C and A1138: front_left_cell(f,m,G) meets C; F.(m+1+1) goes_straight m,G by A514,A1133,A1132,A1131,A1134,A1137,A1138; hence f goes_straight m,G by A1125,A1126,A1127,GOBRD13:45; end; assume front_right_cell(f,m,G) meets C; then F.(m+1+1) turns_right m,G by A514,A1133,A1132,A1131; hence thesis by A1125,A1126,A1127,GOBRD13:43; end; uniqueness proof let f1,f2 be clockwise_oriented standard non constant special_circular_sequence such that A1139: f1 is_sequence_on Gauge(C,n) and A1140: f1/.1 = Gauge(C,n)*(X-SpanStart(C,n),Y-SpanStart(C,n)) and A1141: f1/.2 = Gauge(C,n)*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) and A1142: for k st 1 <= k & k+2 <= len f1 holds (front_right_cell(f1,k, Gauge(C,n)) misses C & front_left_cell(f1,k,Gauge(C,n)) misses C implies f1 turns_left k,Gauge(C,n)) & (front_right_cell(f1,k,Gauge(C,n)) misses C & front_left_cell(f1,k,Gauge(C,n)) meets C implies f1 goes_straight k,Gauge(C,n)) & (front_right_cell(f1,k,Gauge(C,n)) meets C implies f1 turns_right k,Gauge(C,n )) and A1143: f2 is_sequence_on Gauge(C,n) and A1144: f2/.1 = Gauge(C,n)*(X-SpanStart(C,n),Y-SpanStart(C,n)) and A1145: f2/.2 = Gauge(C,n)*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) and A1146: for k st 1 <= k & k+2 <= len f2 holds (front_right_cell(f2,k, Gauge(C,n)) misses C & front_left_cell(f2,k,Gauge(C,n)) misses C implies f2 turns_left k,Gauge(C,n)) & (front_right_cell(f2,k,Gauge(C,n)) misses C & front_left_cell(f2,k,Gauge(C,n)) meets C implies f2 goes_straight k,Gauge(C,n)) & (front_right_cell(f2,k,Gauge(C,n)) meets C implies f2 turns_right k,Gauge(C,n )); defpred P[Nat] means f1|$1 = f2|$1; A1147: for k st P[k] holds P[k+1] proof A1148: len f2 > 4 by GOBOARD7:34; A1149: len f1 > 4 by GOBOARD7:34; let k such that A1151: f1|k = f2|k; per cases by NAT_1:25; suppose W: k = 0; 1 <= len f1 & 1 <= len f2 by A1148,A1149,XXREAL_0:2; then 1 in dom f1 & 1 in dom f2 by FINSEQ_3:25; then W2: <*f1.1 *> = <*f1/.1 *> & <*f2.1 *> = <*f2/.1 *> by PARTFUN1:def 6; W1: <*f1.1 *> = f1|1 & <*f2.1 *> = f2|1 by FINSEQ_5:20; <*f1.1 *> = <*f2.1 *> by A1140,A1144,W2; then f1|1 = f2|1 by W1; hence thesis by W; end; suppose A1152: k = 1; f1|2 = <*f1/.1,f1/.2*> by A1149,FINSEQ_5:81,XXREAL_0:2; hence thesis by A1140,A1141,A1144,A1145,A1148,A1152,FINSEQ_5:81 ,XXREAL_0:2; end; suppose A1153: k > 1; A1154: f2/.1 = f2/.len f2 by FINSEQ_6:def 1; A1155: f1/.1 = f1/.len f1 by FINSEQ_6:def 1; now per cases; suppose A1156: len f1 > k; set m = k-'1; A1157: 1 <= m by A1153,NAT_D:49; then A1158: m+1 = k by NAT_D:43; then A1159: front_right_cell(f1,m,Gauge(C,n)) = front_right_cell(f1|k,m ,Gauge(C,n)) by A1139,A1156,A1157,GOBRD13:42; A1160: k+1 <= len f1 by A1156,NAT_1:13; A1161: now A1162: 1 < len f2 by GOBOARD7:34,XXREAL_0:2; assume A1163: len f2 <= k; then A1164: f2 = f2|k by FINSEQ_1:58; then A1165: 1 in dom(f2|k) by FINSEQ_5:6; len f2 in dom(f2|k) by A1164,FINSEQ_5:6; then A1166: (f1|k)/.len f2 = f1/.len f2 by A1151,FINSEQ_4:70; len f2 <= len f1 by A1151,A1164,FINSEQ_5:16; hence contradiction by A1151,A1155,A1154,A1156,A1163,A1164,A1165,A1166 ,A1162,FINSEQ_4:70,GOBOARD7:38; end; then A1167: k+1 <= len f2 by NAT_1:13; A1168: front_left_cell(f2,m,Gauge(C,n)) = front_left_cell(f2|k,m, Gauge(C,n)) by A1143,A1157,A1158,A1161,GOBRD13:42; A1169: front_right_cell(f2,m,Gauge(C,n)) = front_right_cell(f2|k,m ,Gauge(C,n)) by A1143,A1157,A1158,A1161,GOBRD13:42; A1170: m+(1+1) = k+1 by A1158; A1171: front_left_cell(f1,m,Gauge(C,n)) = front_left_cell(f1|k,m, Gauge(C,n)) by A1139,A1156,A1157,A1158,GOBRD13:42; now per cases; suppose A1172: front_right_cell(f1,m,Gauge(C,n)) misses C & front_left_cell(f1,m,Gauge(C,n)) misses C; then A1173: f1 turns_left m,Gauge(C,n) by A1142,A1157,A1160,A1170; f2 turns_left m,Gauge(C,n) by A1146,A1151,A1157,A1167,A1159 ,A1171,A1169,A1168,A1170,A1172; hence thesis by A1143,A1151,A1153,A1167,A1160,A1173,GOBRD13:47; end; suppose A1174: front_right_cell(f1,m,Gauge(C,n)) misses C & front_left_cell(f1,m,Gauge(C,n)) meets C; then A1175: f1 goes_straight m,Gauge(C,n) by A1142,A1157,A1160,A1170; f2 goes_straight m,Gauge(C,n) by A1146,A1151,A1157,A1167,A1159 ,A1171,A1169,A1168,A1170,A1174; hence thesis by A1143,A1151,A1153,A1167,A1160,A1175,GOBRD13:48; end; suppose A1176: front_right_cell(f1,m,Gauge(C,n)) meets C; then A1177: f1 turns_right m,Gauge(C,n) by A1142,A1157,A1160,A1170; f2 turns_right m,Gauge(C,n) by A1146,A1151,A1157,A1167,A1159 ,A1169,A1170,A1176; hence thesis by A1143,A1151,A1153,A1167,A1160,A1177,GOBRD13:46; end; end; hence thesis; end; suppose A1178: k >= len f1; A1179: 1 < len f1 by GOBOARD7:34,XXREAL_0:2; A1180: f1 = f1|k by A1178,FINSEQ_1:58; then A1181: 1 in dom(f1|k) by FINSEQ_5:6; len f1 in dom(f1|k) by A1180,FINSEQ_5:6; then A1182: (f2|k)/.len f1 = f2/.len f1 by A1151,FINSEQ_4:70; len f1 <= len f2 by A1151,A1180,FINSEQ_5:16; then len f2 = len f1 by A1151,A1155,A1154,A1180,A1181,A1182,A1179, FINSEQ_4:70,GOBOARD7:38; hence thesis by A1151,A1178,A1180,FINSEQ_1:58; end; end; hence thesis; end; end; A1183: P[0]; for k holds P[k] from NAT_1:sch 2(A1183,A1147); hence thesis by JORDAN9:2; end; end;