:: Introducing Spans
:: by Andrzej Trybulec
::
:: Received May 27, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, 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;