Copyright (c) 2002 Association of Mizar Users
environ
vocabulary JORDAN13, JORDAN11, FINSEQ_1, TOPREAL1, GOBOARD1, BOOLE, JORDAN1H,
FINSEQ_4, EUCLID, MATRIX_1, PRE_TOPC, SEQM_3, SPPOL_1, SPRECT_2,
GOBOARD5, ABSVALUE, CONNSP_1, TOPREAL2, ARYTM_1, TOPS_1, RELAT_1,
FUNCT_1, SUBSET_1, RELAT_2, RFINSEQ, GOBOARD9, TARSKI, TREES_1, CARD_1,
JORDAN8, GOBRD13, FINSEQ_5, JORDAN2C, METRIC_1, PCOMPS_1, GROUP_1, ARYTM;
notation TARSKI, GOBOARD5, XBOOLE_0, SUBSET_1, STRUCT_0, ORDINAL1, NUMBERS,
XREAL_0, REAL_1, NAT_1, BINARITH, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2,
CARD_1, CARD_4, PARTFUN1, FINSEQ_1, FINSEQ_2, FINSEQ_4, RFINSEQ,
MATRIX_1, METRIC_1, PRE_TOPC, TOPS_1, CONNSP_1, PCOMPS_1, EUCLID,
TOPREAL1, TOPREAL2, GOBOARD1, SPPOL_1, SPRECT_2, GOBOARD9, JORDAN8,
GOBRD13, JORDAN2C, JORDAN1H, JORDAN11;
constructors REAL_1, FINSEQ_4, CARD_4, RFINSEQ, BINARITH, TOPS_1, CONNSP_1,
PSCOMP_1, REALSET1, SPRECT_2, GOBOARD9, JORDAN8, JORDAN2C, JORDAN11,
GROUP_1, TOPREAL4, PARTFUN1, JORDAN1H, MEMBERED;
clusters RELSET_1, FINSEQ_1, SPPOL_2, REVROT_1, SPRECT_2, XREAL_0, GOBOARD9,
JORDAN8, GOBRD13, SUBSET_1, TOPREAL6, SPRECT_3, INT_1, EUCLID, JORDAN1A,
MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI, XBOOLE_0, GOBOARD1, GOBOARD5;
theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, AXIOMS,
REAL_1, TOPREAL4, SPPOL_2, JORDAN3, FINSEQ_5, FINSEQ_6, CQC_THE1,
GOBOARD7, TOPREAL1, BINARITH, AMI_5, XBOOLE_0, XBOOLE_1, RLVECT_1,
GOBOARD5, SPPOL_1, ABSVALUE, FUNCT_1, FUNCT_2, GROUP_5, GOBOARD9,
RELAT_1, FINSEQ_2, UNIFORM1, SUBSET_1, GOBRD11, JORDAN4, GOBOARD2,
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, SCMFSA_7, JORDAN1H, JORDAN11, XREAL_0,
ZFMISC_1, XCMPLX_0, XCMPLX_1;
schemes NAT_1, LATTICE5;
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 G = Gauge(C,n);
A2: len G = 2|^n+3 & len G = width G 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: 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 CQC_THE1:2;
suppose
A4: k=0;
take <*G*(X-SpanStart(C,n),Y-SpanStart(C,n))*>;
thus thesis by A4;
suppose
A5: 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 A5;
suppose that
A6: k > 1 and
A7: x is FinSequence of TOP-REAL 2;
reconsider f = x as FinSequence of TOP-REAL 2 by A7;
thus thesis
proof per cases;
suppose
A8: len f = k;
thus thesis
proof per cases;
suppose
A9: f is_sequence_on G & left_cell(f,len f-'1,G) meets C;
A10: 1 <= (len f)-'1 by A6,A8,JORDAN3:12;
A11: (len f) -'1 +1 = len f by A6,A8,AMI_5:4;
then consider i1,j1,i2,j2 being Nat such that
A12: [i1,j1] in Indices G & f/.((len f)-'1) = G*(i1,j1) and
A13: [i2,j2] in Indices G & f/.((len f) -'1+1) = G*(i2,j2) and
A14: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A9,A10,JORDAN8:6;
A15: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A12,GOBOARD5:1;
A16: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A13,GOBOARD5:1;
A17: i1-'1 <= len G & j1-'1 <= width G by A15,JORDAN3:7;
A18: 1 <= i2+1 & 1 <= j2+1 by NAT_1:37;
A19: i2-'1 <= len G & j2-'1 <= width G by A16,JORDAN3:7;
(len f)-'1 <= len f by GOBOARD9:2;
then A20: (len f)-'1 in dom f & (len f)-'1+1 in dom f
by A6,A8,A10,A11,FINSEQ_3:27;
A21: (len f)-'1+(1+1) = (len f)+1 by A11,XCMPLX_1:1;
thus thesis
proof per cases;
suppose
A22: 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 A14;
suppose
A23: i1 = i2 & j1+1 = j2;
take f1 = f^<*G*(i2-'1,j2)*>;
now
take i=i2-'1 ,j=j2;
now let i1',j1',i2',j2' be Nat;
assume that
A24: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A25: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A25,GROUP_5:95;
then A26: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A24,GOBOARD1:21;
now assume i2-'1 < 1;
then i2-'1 = 0 by RLVECT_1:98;
then i2 <= 1 by JORDAN4:1;
then i2 = 1 by A16,AXIOMS:21;
then cell(G,1-'1,j1) meets C
by A9,A10,A11,A12,A13,A23,GOBRD13:22;
then cell(G,0,j1) meets C by GOBOARD9:1;
hence contradiction by A2,A15,JORDAN8:21;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2') or
i1'+1 = i2' & j1' = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1' = i2'+1 & j1' = j2' & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1) or
i1' = i2' & j1' = j2'+1 & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2')
by A16,A19,A21,A23,A26,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 turns_left (len f)-'1,G by GOBRD13:def 7;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A22;
suppose
A27: i1+1 = i2 & j1 = j2;
take f1 = f^<*G*(i2,j2+1)*>;
now
take i=i2 ,j=j2+1;
now let i1',j1',i2',j2' be Nat;
assume that
A28: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A29: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A29,GROUP_5:95;
then A30: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A28,GOBOARD1:21;
now assume j2+1 > len G;
then j2+1 <= (len G)+1 & (len G)+1 <= j2+1
by A2,A16,AXIOMS:24,NAT_1:38;
then j2+1 = (len G)+1 by AXIOMS:21;
then j2 = len G by XCMPLX_1:2;
then cell(G,i1,len G) meets C
by A9,A10,A11,A12,A13,A27,GOBRD13:24;
hence contradiction by A15,JORDAN8:18;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2') or
i1'+1 = i2' & j1' = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1' = i2'+1 & j1' = j2' & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1) or
i1' = i2' & j1' = j2'+1 & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2')
by A2,A16,A18,A21,A27,A30,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 turns_left (len f)-'1,G by GOBRD13:def 7;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A22;
suppose
A31: i1 = i2+1 & j1 = j2;
take f1 = f^<*G*(i2,j2-'1)*>;
now
take i=i2 ,j=j2-'1;
now let i1',j1',i2',j2' be Nat;
assume that
A32: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A33: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A33,GROUP_5:95;
then A34: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A32,GOBOARD1:21;
now assume j2-'1 < 1;
then j2-'1 = 0 by RLVECT_1:98;
then j2 <= 1 by JORDAN4:1;
then j2 = 1 by A16,AXIOMS:21;
then cell(G,i2,1-'1) meets C
by A9,A10,A11,A12,A13,A31,GOBRD13:26;
then cell(G,i2,0) meets C by GOBOARD9:1;
hence contradiction by A16,JORDAN8:20;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2') or
i1'+1 = i2' & j1' = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1' = i2'+1 & j1' = j2' & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1) or
i1' = i2' & j1' = j2'+1 & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2')
by A16,A19,A21,A31,A34,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 turns_left (len f)-'1,G by GOBRD13:def 7;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A22;
suppose
A35: i1 = i2 & j1 = j2+1;
take f1 = f^<*G*(i2+1,j2)*>;
now
take i=i2+1 ,j=j2;
now let i1',j1',i2',j2' be Nat;
assume that
A36: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A37: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A37,GROUP_5:95;
then A38: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A36,GOBOARD1:21;
now assume i2+1 > len G;
then i2+1 <= (len G)+1 & (len G)+1 <= i2+1
by A16,AXIOMS:24,NAT_1:38;
then i2+1 = (len G)+1 by AXIOMS:21;
then i2 = len G by XCMPLX_1:2;
then cell(G,len G,j2) meets C
by A9,A10,A11,A12,A13,A35,GOBRD13:28;
hence contradiction by A2,A16,JORDAN8:19;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2') or
i1'+1 = i2' & j1' = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1' = i2'+1 & j1' = j2' & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1) or
i1' = i2' & j1' = j2'+1 & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2')
by A16,A18,A21,A35,A38,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 turns_left (len f)-'1,G by GOBRD13:def 7;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A22;
end;
suppose
A39: 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 A14;
suppose
A40: i1 = i2 & j1+1 = j2;
take f1 = f^<*G*(i2,j2+1)*>;
now
take i=i2 ,j=j2+1;
now let i1',j1',i2',j2' be Nat;
assume that
A41: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A42: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A42,GROUP_5:95;
then A43: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A41,GOBOARD1:21;
now assume j2+1 > len G;
then j2+1 <= (len G)+1 & (len G)+1 <= j2+1
by A2,A16,AXIOMS:24,NAT_1:38;
then j2+1 = (len G)+1 by AXIOMS:21;
then j2 = len G by XCMPLX_1:2;
then cell(G,i1-'1,len G) meets C
by A9,A10,A11,A12,A13,A39,A40,GOBRD13:35;
hence contradiction by A17,JORDAN8:18;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1'+1 = i2' & j1' = j2' & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2') or
i1' = i2'+1 & j1' = j2' & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2') or
i1' = i2' & j1' = j2'+1 & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1)
by A2,A16,A18,A21,A40,A43,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 goes_straight (len f)-'1,G by GOBRD13:def 8;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A39;
suppose
A44: i1+1 = i2 & j1 = j2;
take f1 = f^<*G*(i2+1,j2)*>;
now
take i=i2+1 ,j=j2;
now let i1',j1',i2',j2' be Nat;
assume that
A45: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A46: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A46,GROUP_5:95;
then A47: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A45,GOBOARD1:21;
now assume i2+1 > len G;
then i2+1 <= (len G)+1 & (len G)+1 <= i2+1
by A16,AXIOMS:24,NAT_1:38;
then i2+1 = (len G)+1 by AXIOMS:21;
then i2 = len G by XCMPLX_1:2;
then cell(G,len G,j1) meets C
by A9,A10,A11,A12,A13,A39,A44,GOBRD13:37;
hence contradiction by A2,A15,JORDAN8:19;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1'+1 = i2' & j1' = j2' & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2') or
i1' = i2'+1 & j1' = j2' & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2') or
i1' = i2' & j1' = j2'+1 & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1)
by A16,A18,A21,A44,A47,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 goes_straight (len f)-'1,G by GOBRD13:def 8;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A39;
suppose
A48: i1 = i2+1 & j1 = j2;
take f1 = f^<*G*(i2-'1,j2)*>;
now
take i=i2-'1 ,j=j2;
now let i1',j1',i2',j2' be Nat;
assume that
A49: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A50: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A50,GROUP_5:95;
then A51: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A49,GOBOARD1:21;
now assume i2-'1 < 1;
then i2-'1 = 0 by RLVECT_1:98;
then i2 <= 1 by JORDAN4:1;
then i2 = 1 by A16,AXIOMS:21;
then cell(G,1-'1,j1-'1) meets C
by A9,A10,A11,A12,A13,A39,A48,GOBRD13:39;
then cell(G,0,j1-'1) meets C by GOBOARD9:1;
hence contradiction by A2,A17,JORDAN8:21;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1'+1 = i2' & j1' = j2' & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2') or
i1' = i2'+1 & j1' = j2' & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2') or
i1' = i2' & j1' = j2'+1 & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1)
by A16,A19,A21,A48,A51,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 goes_straight (len f)-'1,G by GOBRD13:def 8;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A39;
suppose
A52: i1 = i2 & j1 = j2+1;
take f1 = f^<*G*(i2,j2-'1)*>;
now
take i=i2 ,j=j2-'1;
now let i1',j1',i2',j2' be Nat;
assume that
A53: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A54: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A54,GROUP_5:95;
then A55: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A53,GOBOARD1:21;
now assume j2-'1 < 1;
then j2-'1 = 0 by RLVECT_1:98;
then j2 <= 1 by JORDAN4:1;
then j2 = 1 by A16,AXIOMS:21;
then cell(G,i1,1-'1) meets C
by A9,A10,A11,A12,A13,A39,A52,GOBRD13:41;
then cell(G,i1,0) meets C by GOBOARD9:1;
hence contradiction by A15,JORDAN8:20;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1'+1 = i2' & j1' = j2' & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2') or
i1' = i2'+1 & j1' = j2' & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2') or
i1' = i2' & j1' = j2'+1 & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1)
by A16,A19,A21,A52,A55,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 goes_straight (len f)-'1,G by GOBRD13:def 8;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A39;
end;
suppose
A56: front_right_cell(f,(len f)-'1,G) meets C;
thus thesis
proof per cases by A14;
suppose
A57: i1 = i2 & j1+1 = j2;
take f1 = f^<*G*(i2+1,j2)*>;
now
take i=i2+1 ,j=j2;
now let i1',j1',i2',j2' be Nat;
assume that
A58: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A59: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A59,GROUP_5:95;
then A60: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A58,GOBOARD1:21;
now assume i2+1 > len G;
then i2+1 <= (len G)+1 & (len G)+1 <= i2+1
by A16,AXIOMS:24,NAT_1:38;
then i2+1 = (len G)+1 by AXIOMS:21;
then i2 = len G by XCMPLX_1:2;
then cell(G,len G,j2) meets C
by A9,A10,A11,A12,A13,A56,A57,GOBRD13:36;
hence contradiction by A2,A16,JORDAN8:19;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2') or
i1'+1 = i2' & j1' = j2' & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1) or
i1' = i2'+1 & j1' = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1' = i2' & j1' = j2'+1 & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2')
by A16,A18,A21,A57,A60,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 turns_right (len f)-'1,G by GOBRD13:def 6;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A56;
suppose
A61: i1+1 = i2 & j1 = j2;
take f1 = f^<*G*(i2,j2-'1)*>;
now
take i=i2 ,j=j2-'1;
now let i1',j1',i2',j2' be Nat;
assume that
A62: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A63: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A63,GROUP_5:95;
then A64: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A62,GOBOARD1:21;
now assume j2-'1 < 1;
then j2-'1 = 0 by RLVECT_1:98;
then j2 <= 1 by JORDAN4:1;
then j2 = 1 by A16,AXIOMS:21;
then cell(G,i2,1-'1) meets C
by A9,A10,A11,A12,A13,A56,A61,GOBRD13:38;
then cell(G,i2,0) meets C by GOBOARD9:1;
hence contradiction by A16,JORDAN8:20;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2') or
i1'+1 = i2' & j1' = j2' & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1) or
i1' = i2'+1 & j1' = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1' = i2' & j1' = j2'+1 & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2')
by A16,A19,A21,A61,A64,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 turns_right (len f)-'1,G by GOBRD13:def 6;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A56;
suppose
A65: i1 = i2+1 & j1 = j2;
take f1 = f^<*G*(i2,j2+1)*>;
now
take i=i2 ,j=j2+1;
now let i1',j1',i2',j2' be Nat;
assume that
A66: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A67: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A67,GROUP_5:95;
then A68: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A66,GOBOARD1:21;
now assume j2+1 > len G;
then j2+1 <= (len G)+1 & (len G)+1 <= j2+1
by A2,A16,AXIOMS:24,NAT_1:38;
then j2+1 = (len G)+1 by AXIOMS:21;
then j2 = len G by XCMPLX_1:2;
then cell(G,i2-'1,len G) meets C
by A9,A10,A11,A12,A13,A56,A65,GOBRD13:40;
hence contradiction by A19,JORDAN8:18;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2') or
i1'+1 = i2' & j1' = j2' & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1) or
i1' = i2'+1 & j1' = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1' = i2' & j1' = j2'+1 & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2')
by A2,A16,A18,A21,A65,A68,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 turns_right (len f)-'1,G by GOBRD13:def 6;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A56;
suppose
A69: i1 = i2 & j1 = j2+1;
take f1 = f^<*G*(i2-'1,j2)*>;
now
take i=i2-'1 ,j=j2;
now let i1',j1',i2',j2' be Nat;
assume that
A70: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A71: f1/.((len f)-'1) = G*(i1',j1') &
f1/.((len f)-'1+1) = G*(i2',j2');
f/.((len f)-'1) = G*(i1',j1') &
f/.((len f)-'1+1) = G*(i2',j2') by A20,A71,GROUP_5:95;
then A72: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A12,A13,A70,GOBOARD1:21;
now assume i2-'1 < 1;
then i2-'1 = 0 by RLVECT_1:98;
then i2 <= 1 by JORDAN4:1;
then i2 = 1 by A16,AXIOMS:21;
then cell(G,1-'1,j2-'1) meets C
by A9,A10,A11,A12,A13,A56,A69,GOBRD13:42;
then cell(G,0,j2-'1) meets C by GOBOARD9:1;
hence contradiction by A2,A19,JORDAN8:21;
end;
hence
i1' = i2' & j1'+1 = j2' & [i2'+1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'+1,j2') or
i1'+1 = i2' & j1' = j2' & [i2',j2'-'1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'-'1) or
i1' = i2'+1 & j1' = j2' & [i2',j2'+1] in Indices G &
f1/.(len f -'1+2) = G*(i2',j2'+1) or
i1' = i2' & j1' = j2'+1 & [i2'-'1,j2'] in Indices G &
f1/.(len f -'1+2) = G*(i2'-'1,j2')
by A16,A19,A21,A69,A72,GOBOARD7:10,TOPREAL4:1;
end;
hence f1 turns_right (len f)-'1,G by GOBRD13:def 6;
thus f1 = f^<*G*(i,j)*>;
end;
hence thesis by A6,A8,A9,A56;
end;
end;
suppose
A73: not f is_sequence_on G or left_cell(f,len f-'1,G) misses C;
take f^<*G*(1,1)*>;
thus thesis by A6,A8,A73;
end;
suppose
A74: len f <> k;
take {};
thus thesis by A6,A74;
end;
suppose
A75: k > 1 & x is not FinSequence of TOP-REAL 2;
take {};
thus thesis by A75;
end;
consider F being Function such that
A76: dom F = NAT and
A77: F.0 = {} and
A78: for k being Element of NAT holds P[k,F.k,F.(k+1)] from RecChoice(A3);
defpred P[Nat] means F.$1 is FinSequence of TOP-REAL 2;
A79: {} = <*>(the carrier of TOP-REAL 2);
then A80: P[0] by A77;
A81: for k st P[k] holds P[k+1]
proof let k such that
A82: F.k is FinSequence of TOP-REAL 2;
per cases by CQC_THE1:2;
suppose k = 0;
hence F.(k+1) is FinSequence of TOP-REAL 2 by A78;
suppose k = 1;
hence F.(k+1) is FinSequence of TOP-REAL 2 by A78;
suppose
A83: k > 1;
thus thesis
proof
reconsider f = F.k as FinSequence of TOP-REAL 2 by A82;
per cases;
suppose
A84: len f = k;
thus thesis
proof per cases;
suppose f is_sequence_on G & left_cell(f,len f-'1,G) meets C;
then (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)*>) &
(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)*>) &
(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 A78,A83,A84;
hence F.(k+1) is FinSequence of TOP-REAL 2;
suppose
A85: 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 F.(k+1) is FinSequence of TOP-REAL 2
by A78,A83,A84,A85;
end;
suppose len f <> k;
hence F.(k+1) is FinSequence of TOP-REAL 2 by A78,A79,A83;
end;
end;
A86: for k holds P[k] from Ind(A80,A81);
rng F c= (the carrier of TOP-REAL 2)*
proof let y be set;
assume y in rng F;
then ex x being set st x in dom F & F.x = y by FUNCT_1:def 5;
then y is FinSequence of TOP-REAL 2 by A76,A86;
hence thesis by FINSEQ_1:def 11;
end;
then reconsider F as Function of NAT,(the carrier of TOP-REAL 2)*
by A76,FUNCT_2:def 1,RELSET_1:11;
defpred P[Nat] means len(F.$1) = $1;
A87: P[0] by A77,FINSEQ_1:25;
A88: for k st P[k] holds P[k+1]
proof let k such that
A89: len(F.k) = k;
A90: P[k,F.k,F.(k+1)] by A78;
per cases by CQC_THE1:2;
suppose k = 0;
hence thesis by A90,FINSEQ_1:56;
suppose k = 1;
hence thesis by A90,FINSEQ_1:61;
suppose
A91: k > 1;
thus thesis
proof per cases;
suppose
F.k is_sequence_on G & left_cell(F.k,len(F.k)-'1,G) meets C;
then (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)*>) &
(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)*>) &
(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 A78,A89,A91;
hence thesis by A89,FINSEQ_2:19;
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 A78,A89,A91;
hence thesis by A89,FINSEQ_2:19;
end;
end;
A92: for k holds P[k] from Ind(A87,A88);
set XS = X-SpanStart(C,n), YS = Y-SpanStart(C,n);
2 < XS by JORDAN1H:58;
then A93: 1 <= XS by AXIOMS:22;
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;
A94: Q[0]
proof
(for n st n in dom(F.0)
ex i,j st [i,j] in Indices G & (F.0)/.n = G*(i,j)) &
(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
abs(m-i)+abs(k-j) = 1) by A77,RELAT_1:60;
hence F.0 is_sequence_on G by GOBOARD1:def 11;
let m; assume
A95: 1 <= m & m+1 <= len(F.0);
1 <= m+1 by NAT_1:37;
then 1 <= len(F.0) by A95,AXIOMS:22;
then 1 <= 0 by A77,FINSEQ_1:25;
hence right_cell(F.0,m,G) misses C & left_cell(F.0,m,G) meets C;
end;
A96: [X-SpanStart(C,n),Y-SpanStart(C,n)] in Indices G by A1,JORDAN11:8;
1+1 <= XS by JORDAN1H:58;
then A97: 1 <= XS-'1 & XS <= len G by JORDAN1H:58,SPRECT_3:8;
A98: for k st Q[k] holds Q[k+1]
proof let k such that
A99: F.k is_sequence_on G and
A100: 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;
A101: len(F.k) = k by A92;
A102: len(F.(k+1)) = k+1 by A92;
per cases by CQC_THE1:2;
suppose
A103: k = 0;
then A104: F.(k+1) = <*G*(X-SpanStart(C,n),Y-SpanStart(C,n))*> by A78;
A105: now let l;
assume l in dom(F.(k+1));
then 1 <= l & l <= 1 by A102,A103,FINSEQ_3:27;
then l = 1 by AXIOMS:21;
then (F.(k+1))/.l = G*(X-SpanStart(C,n),Y-SpanStart(C,n))
by A104,FINSEQ_4:25;
hence ex i,j st [i,j] in Indices G & (F.(k+1))/.l = G*(i,j) by A96;
end;
now let l;
assume l in dom(F.(k+1)) & l+1 in dom(F.(k+1));
then 1 <= l & l <= 1 & 1 <= l+1 & l+1 <= 1 by A102,A103,FINSEQ_3:27;
then l = 1 & 1 = l+1 by AXIOMS:21;
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 abs(i1-i2)+abs(j1-j2) = 1;
end;
hence F.(k+1) is_sequence_on G by A105,GOBOARD1:def 11;
let m;
assume
A106: 1 <= m & m+1 <= len(F.(k+1));
1 <= m+1 by NAT_1:37;
then m+1 = 0+1 by A102,A103,A106,AXIOMS:21;
then m = 0 by XCMPLX_1:2;
hence right_cell(F.(k+1),m,G) misses C &
left_cell(F.(k+1),m,G) meets C by A106;
suppose
A107: k = 1;
then F.(k+1) = <*G*(X-SpanStart(C,n),Y-SpanStart(C,n)),
G*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n))*> by A78;
then A108: (F.(k+1))/.1 = G*(X-SpanStart(C,n),Y-SpanStart(C,n)) &
(F.(k+1))/.2 = G*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n))
by FINSEQ_4:26;
A109: [X-SpanStart(C,n),Y-SpanStart(C,n)] in Indices G &
[X-SpanStart(C,n)-'1,Y-SpanStart(C,n)] in Indices G
by A1,JORDAN11:8,9;
A110: now let l;
assume
A111: l in dom(F.(k+1));
then 1 <= l & l <= 2 by A102,A107,FINSEQ_3:27;
then l = 0 or l = 1 or l = 2 by CQC_THE1:3;
hence ex i,j st [i,j] in Indices G & (F.(k+1))/.l = G*(i,j)
by A108,A109,A111,FINSEQ_3:27;
end;
now let l;
assume A112: l in dom(F.(k+1)) & l+1 in dom(F.(k+1));
then 1 <= l & l <= 2 & 1 <= l+1 & l+1 <= 2 by A102,A107,FINSEQ_3:27;
then A113: l = 0 or l = 1 or l = 2 by CQC_THE1:3;
let i1,j1,i2,j2 be Nat such that
A114: [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);
A115: i1 = XS & j1 = YS & i2 = XS-'1 & j2 = YS
by A102,A107,A108,A109,A112,A113,A114,FINSEQ_3:27,GOBOARD1:21;
then i2+1 = i1 by A97,JORDAN3:6;
then i1-i2 = 1 & j1-j2 = 0 by A115,XCMPLX_1:14,26;
then abs(i1-i2) = 1 & abs(j1-j2) = 0 by ABSVALUE:def 1;
hence abs(i1-i2)+abs(j1-j2) = 1;
end;
hence
A116: F.(k+1) is_sequence_on G by A110,GOBOARD1:def 11;
let m;
assume
A117: 1 <= m & m+1 <= len(F.(k+1));
then 1+1 <= m+1 by AXIOMS:24;
then m+1 = 1+1 by A102,A107,A117,AXIOMS:21;
then A118: m = 1 by XCMPLX_1:2;
A119: XS-'1 < XS & XS-'1 < XS-'1+1 by A93,JORDAN5B:1,NAT_1:38;
A120: XS <= XS+1 by NAT_1:29;
then A121: right_cell(F.(k+1),m,G) = cell(G,XS-'1,YS)
by A108,A109,A116,A117,A118,A119,GOBRD13:def 2;
A122: left_cell(F.(k+1),m,G) = cell(G,XS-'1,YS-'1)
by A108,A109,A116,A117,A118,A119,A120,GOBRD13:def 3;
thus right_cell(F.(k+1),m,G) misses C by A1,A121,JORDAN11:11;
thus left_cell(F.(k+1),m,G) meets C by A1,A122,JORDAN11:10;
suppose
A123: k > 1;
then k > 0 by AXIOMS:22;
then A124: F.k is non empty by A101,FINSEQ_1:25;
A125: 1 <= (len(F.k))-'1 by A101,A123,JORDAN3:12;
A126: (len(F.k)) -'1 +1 = len(F.k) by A101,A123,AMI_5:4;
then consider i1,j1,i2,j2 being Nat such that
A127: [i1,j1] in Indices G & (F.k)/.(len(F.k)-'1) = G*(i1,j1) and
A128: [i2,j2] in Indices G & (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 A99,A125,JORDAN8:6;
A129: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A128,GOBOARD5:1;
(len(F.k))-'1 <= len(F.k) by GOBOARD9:2;
then A130: (len(F.k))-'1 in dom(F.k) & len(F.k) in dom(F.k)
by A101,A123,A125,FINSEQ_3:27;
A131: (len(F.k))-'1+(1+1) = (len(F.k))+1 by A126,XCMPLX_1:1;
A132: right_cell(F.k,(len(F.k))-'1,G) misses C &
left_cell(F.k,(len(F.k))-'1,G) meets C by A100,A125,A126;
then A133: i1 = i2 & j1+1 = j2 implies [i1-'1,j1+1] in Indices G
by A99,A101,A123,A127,A128,JORDAN1H:61;
A134: i1+1 = i2 & j1 = j2 implies [i1+1,j1+1] in Indices G
by A99,A101,A123,A127,A128,A132,JORDAN1H:62;
A135: i1 = i2+1 & j1 = j2 implies [i2,j1-'1] in Indices G
by A99,A101,A123,A127,A128,A132,JORDAN1H:63;
A136: i1 = i2 & j1 = j2+1 implies [i1+1,j2] in Indices G
by A99,A101,A123,A127,A128,A132,JORDAN1H:64;
j1+1+1 = j1+(1+1) by XCMPLX_1:1 .= j1+2;
then A137: 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 A99,A101,A123,A127,A128,JORDAN1H:65;
i1+1+1 = i1+(1+1) by XCMPLX_1:1 .= i1+2;
then A138: 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 A99,A101,A123,A127,A128,JORDAN1H:66;
A139: 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 A99,A101,A123,A127,A128,JORDAN1H:67;
A140: 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 A99,A101,A123,A127,A128,JORDAN1H:68;
A141: 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 A99,A101,A123,A127,A128,JORDAN1H:69;
A142: 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 A99,A101,A123,A127,A128,JORDAN1H:70;
A143: 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 A99,A101,A123,A127,A128,JORDAN1H:71;
A144: 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 A99,A101,A123,A127,A128,JORDAN1H:72;
thus
A145: 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
A146: (F.k)^<*G*(i,j)*> turns_left (len(F.k))-'1,G and
A147: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A99,A101,A123,A132;
set f = (F.k)^<*G*(i,j)*>;
A148: f/.(len(F.k)-'1) = G*(i1,j1) & f/.len(F.k) = G*(i2,j2)
by A127,A128,A130,GROUP_5:95;
A149: f/.(len(F.k)+1) = G*(i,j) by TOPREAL4:1;
thus thesis
proof per cases by A126,A127,A128,A131,A146,A148,GOBRD13:def 7;
suppose that
A150: i1 = i2 & j1+1 = j2 and
A151: f/.(len(F.k)+1) = G*(i2-'1,j2);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2-'1,j2) = G*(i2',j2');
then A152: i2 = i1' & j2 = j1' & i2-'1 = i2' & j2 = j2'
by A128,A133,A150,GOBOARD1:21;
then i1'-i2' = i2-(i2-1) by A129,SCMFSA_7:3;
then j2'-j1' = 0 & i1'-i2' = 1 by A152,XCMPLX_1:14,18;
then abs(j2'-j1') = 0 & abs(i1'-i2') = 1 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1 by UNIFORM1:13;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A133,A147,A149,A150,A151,JORDAN8:9;
suppose that
A153: i1+1 = i2 & j1 = j2 and
A154: f/.(len(F.k)+1) = G*(i2,j2+1);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2,j2+1) = G*(i2',j2');
then i2 = i1' & j2 = j1' & i2 = i2' & j2+1 = j2'
by A128,A134,A153,GOBOARD1:21;
then i2'-i1' = 0 & j2'-j1' = 1 by XCMPLX_1:14,26;
then abs(i2'-i1') = 0 & abs(j2'-j1') = 1 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A134,A147,A149,A153,A154,JORDAN8:9;
suppose that
A155: i1 = i2+1 & j1 = j2 and
A156: f/.(len(F.k)+1) = G*(i2,j2-'1);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2,j2-'1) = G*(i2',j2');
then A157: i2 = i1' & j2 = j1' & i2 = i2' & j2-'1 = j2'
by A128,A135,A155,GOBOARD1:21;
then j1'-j2' = j2-(j2-1) by A129,SCMFSA_7:3;
then i2'-i1' = 0 & j1'-j2' = 1 by A157,XCMPLX_1:14,18;
then abs(i2'-i1') = 0 & abs(j1'-j2') = 1 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1 by UNIFORM1:13;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A135,A147,A149,A155,A156,JORDAN8:9;
suppose that
A158: i1 = i2 & j1 = j2+1 and
A159: f/.(len(F.k)+1) = G*(i2+1,j2);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2+1,j2) = G*(i2',j2');
then i2 = i1' & j2 = j1' & i2+1 = i2' & j2 = j2'
by A128,A136,A158,GOBOARD1:21;
then i2'-i1' = 1 & j2'-j1' = 0 by XCMPLX_1:14,26;
then abs(i2'-i1') = 1 & abs(j2'-j1') = 0 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A136,A147,A149,A158,A159,JORDAN8:9;
end;
suppose
A160: 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
A161: (F.k)^<*G*(i,j)*> goes_straight (len(F.k))-'1,G and
A162: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A99,A101,A123,A132;
set f = (F.k)^<*G*(i,j)*>;
A163: f/.(len(F.k)-'1) = G*(i1,j1) & f/.len(F.k) = G*(i2,j2)
by A127,A128,A130,GROUP_5:95;
A164: f/.(len(F.k)+1) = G*(i,j) by TOPREAL4:1;
thus thesis
proof per cases by A126,A127,A128,A131,A161,A163,GOBRD13:def 8;
suppose that
A165: i1 = i2 & j1+1 = j2 and
A166: f/.(len(F.k)+1) = G*(i2,j2+1);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2,j2+1) = G*(i2',j2');
then i2 = i1' & j2 = j1' & i2 = i2' & j2+1 = j2'
by A128,A137,A160,A165,GOBOARD1:21;
then i2'-i1' = 0 & j2'-j1' = 1 by XCMPLX_1:14,26;
then abs(i2'-i1') = 0 & abs(j2'-j1') = 1 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A137,A160,A162,A164,A165,A166,JORDAN8:9;
suppose that
A167: i1+1 = i2 & j1 = j2 and
A168: f/.(len(F.k)+1) = G*(i2+1,j2);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2+1,j2) = G*(i2',j2');
then i2 = i1' & j2 = j1' & i2+1 = i2' & j2 = j2'
by A128,A138,A160,A167,GOBOARD1:21;
then i2'-i1' = 1 & j2'-j1' = 0 by XCMPLX_1:14,26;
then abs(i2'-i1') = 1 & abs(j2'-j1') = 0 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A138,A160,A162,A164,A167,A168,JORDAN8:9;
suppose that
A169: i1 = i2+1 & j1 = j2 and
A170: f/.(len(F.k)+1) = G*(i2-'1,j2);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2-'1,j2) = G*(i2',j2');
then A171: i2 = i1' & j2 = j1' & i2-'1 = i2' & j2 = j2'
by A128,A139,A160,A169,GOBOARD1:21;
then i1'-i2' = i2-(i2-1) by A129,SCMFSA_7:3;
then j2'-j1' = 0 & i1'-i2' = 1 by A171,XCMPLX_1:14,18;
then abs(j2'-j1') = 0 & abs(i1'-i2') = 1 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1 by UNIFORM1:13;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A139,A160,A162,A164,A169,A170,JORDAN8:9;
suppose that
A172: i1 = i2 & j1 = j2+1 and
A173: f/.(len(F.k)+1) = G*(i2,j2-'1);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2,j2-'1) = G*(i2',j2');
then A174: i2 = i1' & j2 = j1' & i2 = i2' & j2-'1 = j2'
by A128,A140,A160,A172,GOBOARD1:21;
then j1'-j2' = j2-(j2-1) by A129,SCMFSA_7:3;
then i2'-i1' = 0 & j1'-j2' = 1 by A174,XCMPLX_1:14,18;
then abs(i2'-i1') = 0 & abs(j1'-j2') = 1 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1 by UNIFORM1:13;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A140,A160,A162,A164,A172,A173,JORDAN8:9;
end;
suppose
A175: front_right_cell(F.k,(len(F.k))-'1,G) meets C;
then consider i,j such that
A176: (F.k)^<*G*(i,j)*> turns_right (len(F.k))-'1,G and
A177: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A99,A101,A123,A132;
set f = (F.k)^<*G*(i,j)*>;
A178: f/.(len(F.k)-'1) = G*(i1,j1) & f/.len(F.k) = G*(i2,j2)
by A127,A128,A130,GROUP_5:95;
A179: f/.(len(F.k)+1) = G*(i,j) by TOPREAL4:1;
thus thesis
proof per cases by A126,A127,A128,A131,A176,A178,GOBRD13:def 6;
suppose that
A180: i1 = i2 & j1+1 = j2 and
A181: f/.(len(F.k)+1) = G*(i2+1,j2);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2+1,j2) = G*(i2',j2');
then i2 = i1' & j2 = j1' & i2+1 = i2' & j2 = j2'
by A128,A141,A175,A180,GOBOARD1:21;
then i2'-i1' = 1 & j2'-j1' = 0 by XCMPLX_1:14,26;
then abs(i2'-i1') = 1 & abs(j2'-j1') = 0 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A141,A175,A177,A179,A180,A181,JORDAN8:9;
suppose that
A182: i1+1 = i2 & j1 = j2 and
A183: f/.(len(F.k)+1) = G*(i2,j2-'1);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2,j2-'1) = G*(i2',j2');
then A184: i2 = i1' & j2 = j1' & i2 = i2' & j2-'1 = j2'
by A128,A142,A175,A182,GOBOARD1:21;
then j1'-j2' = j2-(j2-1) by A129,SCMFSA_7:3;
then i2'-i1' = 0 & j1'-j2' = 1 by A184,XCMPLX_1:14,18;
then abs(i2'-i1') = 0 & abs(j1'-j2') = 1 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1 by UNIFORM1:13;
end;
hence F.(k+1) is_sequence_on G by A99,A124,A142,A175,A177,A179,A182,
A183,JORDAN8:9;
suppose that
A185: i1 = i2+1 & j1 = j2 and
A186: f/.(len(F.k)+1) = G*(i2,j2+1);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2,j2+1) = G*(i2',j2');
then i2 = i1' & j2 = j1' & i2 = i2' & j2+1 = j2'
by A128,A143,A175,A185,GOBOARD1:21;
then i2'-i1' = 0 & j2'-j1' = 1 by XCMPLX_1:14,26;
then abs(i2'-i1') = 0 & abs(j2'-j1') = 1 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A143,A175,A177,A179,A185,A186,JORDAN8:9;
suppose that
A187: i1 = i2 & j1 = j2+1 and
A188: f/.(len(F.k)+1) = G*(i2-'1,j2);
now let i1',j1',i2',j2' be Nat;
assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
(F.k)/.len(F.k) = G*(i1',j1') & G*(i2-'1,j2) = G*(i2',j2');
then A189: i2 = i1' & j2 = j1' & i2-'1 = i2' & j2 = j2'
by A128,A144,A175,A187,GOBOARD1:21;
then i1'-i2' = i2-(i2-1) by A129,SCMFSA_7:3;
then j2'-j1' = 0 & i1'-i2' = 1 by A189,XCMPLX_1:14,18;
then abs(j2'-j1') = 0 & abs(i1'-i2') = 1 by ABSVALUE:def 1;
hence abs(i2'-i1')+abs(j2'-j1') = 1 by UNIFORM1:13;
end;
hence F.(k+1) is_sequence_on G
by A99,A124,A144,A175,A177,A179,A187,A188,JORDAN8:9;
end;
end;
let m such that
A190: 1 <= m & m+1 <= len(F.(k+1));
now per cases;
suppose m+1 = len(F.(k+1));
then A191: m = len(F.k) by A101,A102,XCMPLX_1:2;
A192: (i2-'1)+1 = i2 by A129,AMI_5:4;
A193: (j2-'1)+1 = j2 by A129,AMI_5:4;
thus thesis
proof per cases;
suppose
A194: 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
A195: (F.k)^<*G*(i,j)*> turns_left (len(F.k))-'1,G and
A196: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A99,A101,A123,A132;
A197: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) &
(F.(k+1))/.len(F.k) = G*(i2,j2)
by A127,A128,A130,A196,GROUP_5:95;
now per cases by A126,A127,A128,A131,A195,A196,A197,GOBRD13:def 7;
suppose that
A198: i1 = i2 & j1+1 = j2 and
A199: (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 A99,A125,A126,A127,A128,A198,GOBRD13:35;
hence right_cell(F.(k+1),m,G) misses C
by A128,A133,A145,A190,A191,A192,A194,A197,A198,A199,GOBRD13:27;
j2-'1 = j1 &
cell(G,i1-'1,j1) meets C
by A99,A125,A126,A127,A128,A132,A198,BINARITH:39,GOBRD13:22;
hence left_cell(F.(k+1),m,G) meets C
by A128,A133,A145,A190,A191,A192,A197,A198,A199,GOBRD13:26;
suppose that
A200: i1+1 = i2 & j1 = j2 and
A201: (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 A99,A125,A126,A127,A128,A200,GOBRD13:37;
hence right_cell(F.(k+1),m,G) misses C
by A128,A134,A145,A190,A191,A194,A197,A200,A201,GOBRD13:23;
i1+1-'1 = i1 & cell(G,i1,j1) meets C
by A99,A125,A126,A127,A128,A132,A200,BINARITH:39,GOBRD13:24;
hence left_cell(F.(k+1),m,G) meets C
by A128,A134,A145,A190,A191,A197,A200,A201,GOBRD13:22;
suppose that
A202: i1 = i2+1 & j1 = j2 and
A203: (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 A99,A125,A126,A127,A128,A202,GOBRD13:39;
hence right_cell(F.(k+1),m,G) misses C
by A128,A135,A145,A190,A191,A193,A194,A197,A202,A203,GOBRD13:29;
cell(G,i2,j2-'1) meets C by A99,A125,A126,A127,A128,A132,A202,
GOBRD13:26;
hence left_cell(F.(k+1),m,G) meets C
by A128,A135,A145,A190,A191,A193,A197,A202,A203,GOBRD13:28;
suppose that
A204: i1 = i2 & j1 = j2+1 and
A205: (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 A99,A125,A126,A127,A128,A204,GOBRD13:41;
hence right_cell(F.(k+1),m,G) misses C
by A128,A136,A145,A190,A191,A194,A197,A204,A205,GOBRD13:25;
cell(G,i2,j2) meets C by A99,A125,A126,A127,A128,A132,A204,
GOBRD13:28;
hence left_cell(F.(k+1),m,G) meets C
by A128,A136,A145,A190,A191,A197,A204,A205,GOBRD13:24;
end;
hence thesis;
suppose
A206: 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
A207: (F.k)^<*G*(i,j)*> goes_straight (len(F.k))-'1,G and
A208: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A99,A101,A123,A132;
A209: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) &
(F.(k+1))/.len(F.k) = G*(i2,j2)
by A127,A128,A130,A208,GROUP_5:95;
now per cases by A126,A127,A128,A131,A207,A208,A209,GOBRD13:def 8;
suppose that
A210: i1 = i2 & j1+1 = j2 and
A211: (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 A99,A125,A126,A127,A128,A210,GOBRD13:36;
hence right_cell(F.(k+1),m,G) misses C
by A128,A137,A145,A190,A191,A206,A209,A210,A211,GOBRD13:23;
front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i1-'1,j2)
by A99,A125,A126,A127,A128,A210,GOBRD13:35;
hence left_cell(F.(k+1),m,G) meets C
by A128,A137,A145,A190,A191,A206,A209,A210,A211,GOBRD13:22;
suppose that
A212: i1+1 = i2 & j1 = j2 and
A213: (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 A99,A125,A126,A127,A128,A212,GOBRD13:38;
hence right_cell(F.(k+1),m,G) misses C
by A128,A138,A145,A190,A191,A206,A209,A212,A213,GOBRD13:25;
front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2)
by A99,A125,A126,A127,A128,A212,GOBRD13:37;
hence left_cell(F.(k+1),m,G) meets C
by A128,A138,A145,A190,A191,A206,A209,A212,A213,GOBRD13:24;
suppose that
A214: i1 = i2+1 & j1 = j2 and
A215: (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 A99,A125,A126,A127,A128,A214,GOBRD13:40;
hence right_cell(F.(k+1),m,G) misses C
by A128,A139,A145,A190,A191,A192,A206,A209,A214,A215,GOBRD13:27;
front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i2-'1,j2-'1)
by A99,A125,A126,A127,A128,A214,GOBRD13:39;
hence left_cell(F.(k+1),m,G) meets C
by A128,A139,A145,A190,A191,A192,A206,A209,A214,A215,GOBRD13:26;
suppose that
A216: i1 = i2 & j1 = j2+1 and
A217: (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 A99,A125,A126,A127,A128,A216,GOBRD13:42;
hence right_cell(F.(k+1),m,G) misses C
by A128,A140,A145,A190,A191,A193,A206,A209,A216,A217,GOBRD13:29;
front_left_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2-'1)
by A99,A125,A126,A127,A128,A216,GOBRD13:41;
hence left_cell(F.(k+1),m,G) meets C
by A128,A140,A145,A190,A191,A193,A206,A209,A216,A217,GOBRD13:28;
end;
hence thesis;
suppose
A218: front_right_cell(F.k,(len(F.k))-'1,G) meets C;
then consider i,j such that
A219: (F.k)^<*G*(i,j)*> turns_right (len(F.k))-'1,G and
A220: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A99,A101,A123,A132;
A221: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) &
(F.(k+1))/.len(F.k) = G*(i2,j2)
by A127,A128,A130,A220,GROUP_5:95;
now per cases by A126,A127,A128,A131,A219,A220,A221,GOBRD13:def 6;
suppose that
A222: i1 = i2 & j1+1 = j2 and
A223: (F.(k+1))/.(len(F.k)+1) = G*(i2+1,j2);
j2 -'1 = j1 &
cell(G,i1,j1) misses C
by A99,A125,A126,A127,A128,A132,A222,BINARITH:39,GOBRD13:23;
hence right_cell(F.(k+1),m,G) misses C
by A128,A141,A145,A190,A191,A218,A221,A222,A223,GOBRD13:25;
front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2)
by A99,A125,A126,A127,A128,A222,GOBRD13:36;
hence left_cell(F.(k+1),m,G) meets C
by A128,A141,A145,A190,A191,A218,A221,A222,A223,GOBRD13:24;
suppose that
A224: i1+1 = i2 & j1 = j2 and
A225: (F.(k+1))/.(len(F.k)+1) = G*(i2,j2-'1);
i2 -'1 = i1 &
cell(G,i1,j1-'1) misses C
by A99,A125,A126,A127,A128,A132,A224,BINARITH:39,GOBRD13:25;
hence right_cell(F.(k+1),m,G) misses C
by A128,A142,A145,A190,A191,A193,A218,A221,A224,A225,GOBRD13:29;
front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2-'1)
by A99,A125,A126,A127,A128,A224,GOBRD13:38;
hence left_cell(F.(k+1),m,G) meets C
by A128,A142,A145,A190,A191,A193,A218,A221,A224,A225,GOBRD13:28;
suppose that
A226: i1 = i2+1 & j1 = j2 and
A227: (F.(k+1))/.(len(F.k)+1) = G*(i2,j2+1);
cell(G,i2,j2) misses C by A99,A125,A126,A127,A128,A132,A226,
GOBRD13:27;
hence right_cell(F.(k+1),m,G) misses C
by A128,A143,A145,A190,A191,A218,A221,A226,A227,GOBRD13:23;
front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2-'1,j2)
by A99,A125,A126,A127,A128,A226,GOBRD13:40;
hence left_cell(F.(k+1),m,G) meets C
by A128,A143,A145,A190,A191,A218,A221,A226,A227,GOBRD13:22;
suppose that
A228: i1 = i2 & j1 = j2+1 and
A229: (F.(k+1))/.(len(F.k)+1) = G*(i2-'1,j2);
cell(G,i2-'1,j2) misses C by A99,A125,A126,A127,A128,A132,A228,
GOBRD13:29;
hence right_cell(F.(k+1),m,G) misses C
by A128,A144,A145,A190,A191,A192,A218,A221,A228,A229,GOBRD13:27;
front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2-'1,j2-'1)
by A99,A125,A126,A127,A128,A228,GOBRD13:42;
hence left_cell(F.(k+1),m,G) meets C
by A128,A144,A145,A190,A191,A192,A218,A221,A228,A229,GOBRD13:26;
end;
hence thesis;
end;
suppose m+1 <> len(F.(k+1));
then m+1 < len(F.(k+1)) by A190,REAL_1:def 5;
then A230: m+1 <= len(F.k)by A101,A102,NAT_1:38;
then consider i1,j1,i2,j2 being Nat such that
A231: [i1,j1] in Indices G & (F.k)/.m = G*(i1,j1) and
A232: [i2,j2] in Indices G & (F.k)/.(m+1) = G*(i2,j2) and
A233: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A99,A190,JORDAN8:6;
A234: 1 <= m+1 by NAT_1:37;
m <= len(F.k) by A230,NAT_1:38;
then A235: m in dom(F.k) & m+1 in dom(F.k)
by A190,A230,A234,FINSEQ_3:27;
A236: right_cell(F.k,m,G) misses C & left_cell(F.k,m,G) meets C
by A100,A190,A230;
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
A237: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A99,A101,A123,A132;
take i,j;
thus F.(k+1) = (F.k)^<*G*(i,j)*> by A237;
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
A238: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A99,A101,A123,A132;
take i,j;
thus F.(k+1) = (F.k)^<*G*(i,j)*> by A238;
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
A239: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A99,A101,A123,A132;
take i,j;
thus F.(k+1) = (F.k)^<*G*(i,j)*> by A239;
end;
then consider i,j such that
A240: F.(k+1) = (F.k)^<*G*(i,j)*>;
A241: (F.(k+1))/.m = G*(i1,j1) & (F.(k+1))/.(m+1) = G*(i2,j2)
by A231,A232,A235,A240,GROUP_5:95;
now per cases by A233;
suppose
A242: i1 = i2 & j1+1 = j2;
then left_cell(F.k,m,G) = cell(G,i1-'1,j1) &
right_cell(F.k,m,G) = cell(G,i1,j1)
by A99,A190,A230,A231,A232,GOBRD13:22,23;
hence thesis by A145,A190,A231,A232,A236,A241,A242,GOBRD13:22,23;
suppose
A243: i1+1 = i2 & j1 = j2;
then left_cell(F.k,m,G) = cell(G,i1,j1) &
right_cell(F.k,m,G) = cell(G,i1,j1-'1)
by A99,A190,A230,A231,A232,GOBRD13:24,25;
hence thesis by A145,A190,A231,A232,A236,A241,A243,GOBRD13:24,25;
suppose
A244: i1 = i2+1 & j1 = j2;
then left_cell(F.k,m,G) = cell(G,i2,j2-'1) &
right_cell(F.k,m,G) = cell(G,i2,j2)
by A99,A190,A230,A231,A232,GOBRD13:26,27;
hence thesis by A145,A190,A231,A232,A236,A241,A244,GOBRD13:26,27;
suppose
A245: i1 = i2 & j1 = j2+1;
then left_cell(F.k,m,G) = cell(G,i2,j2) &
right_cell(F.k,m,G) = cell(G,i1-'1,j2)
by A99,A190,A230,A231,A232,GOBRD13:28,29;
hence thesis by A145,A190,A231,A232,A236,A241,A245,GOBRD13:28,29;
end;
hence thesis;
end;
hence thesis;
end;
A246: for k holds Q[k] from Ind(A94,A98);
A247: P[0,F.0,F.(0+1)] by A78;
A248: P[1,F.1,F.(1+1)] by A78;
A249: 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
A250: k > 1 and
A251: [i1,j1] in Indices G & (F.k)/.(len(F.k)-'1) = G*(i1,j1) and
A252: [i2,j2] in Indices G & (F.k)/.len(F.k) = G*(i2,j2);
A253: (len(F.k))-'1 <= len(F.k) by GOBOARD9:2;
A254: F.k is_sequence_on G by A246;
A255: len(F.k) = k by A92;
then A256: 1 <= (len(F.k))-'1 by A250,JORDAN3:12;
A257: (len(F.k)) -'1 +1 = len(F.k) by A250,A255,AMI_5:4;
then A258: left_cell(F.k,(len(F.k))-'1,G) meets C by A246,A256;
A259: (len(F.k))-'1 in dom(F.k) & len(F.k) in dom(F.k)
by A250,A253,A255,A256,FINSEQ_3:27;
A260: (len(F.k))-'1+(1+1) = (len(F.k))+1 by A257,XCMPLX_1:1;
A261: i1+1 > i1 & i2+1 > i2 & j1+1 > j1 & j2+1 > j2 by NAT_1:38;
hereby assume
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
A262: (F.k)^<*G*(i,j)*> turns_left (len(F.k))-'1,G and
A263: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A250,A254,A255,A258;
A264: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) & (F.(k+1))/.len(F.k) = G*(i2,j2)
by A251,A252,A259,A263,GROUP_5:95;
A265: (F.(k+1))/.(len(F.k)+1) = G*(i,j) by A263,TOPREAL4:1;
thus F.(k+1) turns_left (len(F.k))-'1,G by A262,A263;
thus i1 = i2 & j1+1 = j2 implies
[i2-'1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2-'1,j2)*>
by A251,A252,A257,A260,A261,A262,A263,A264,A265,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 A251,A252,A257,A260,A261,A262,A263,A264,A265,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 A251,A252,A257,A260,A261,A262,A263,A264,A265,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 A251,A252,A257,A260,A261,A262,A263,A264,A265,GOBRD13:def 7;
end;
end;
A266: 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
A267: k > 1 and
A268: [i1,j1] in Indices G & (F.k)/.(len(F.k)-'1) = G*(i1,j1) and
A269: [i2,j2] in Indices G & (F.k)/.len(F.k) = G*(i2,j2);
A270: (len(F.k))-'1 <= len(F.k) by GOBOARD9:2;
A271: F.k is_sequence_on G by A246;
A272: len(F.k) = k by A92;
then A273: 1 <= (len(F.k))-'1 by A267,JORDAN3:12;
A274: (len(F.k)) -'1 +1 = len(F.k) by A267,A272,AMI_5:4;
then A275: left_cell(F.k,(len(F.k))-'1,G) meets C by A246,A273;
A276: (len(F.k))-'1 in dom(F.k) & len(F.k) in dom(F.k)
by A267,A270,A272,A273,FINSEQ_3:27;
A277: (len(F.k))-'1+(1+1) = (len(F.k))+1 by A274,XCMPLX_1:1;
A278: i1+1 > i1 & i2+1 > i2 & j1+1 > j1 & j2+1 > j2 by NAT_1:38;
hereby assume 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
A279: (F.k)^<*G*(i,j)*> goes_straight (len(F.k))-'1,G and
A280: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A267,A271,A272,A275;
A281: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) & (F.(k+1))/.len(F.k) = G*(i2,j2)
by A268,A269,A276,A280,GROUP_5:95;
A282: (F.(k+1))/.(len(F.k)+1) = G*(i,j) by A280,TOPREAL4:1;
thus F.(k+1) goes_straight (len(F.k))-'1,G by A279,A280;
thus i1 = i2 & j1+1 = j2 implies
[i2,j2+1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2+1)*>
by A268,A269,A274,A277,A278,A279,A280,A281,A282,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 A268,A269,A274,A277,A278,A279,A280,A281,A282,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 A268,A269,A274,A277,A278,A279,A280,A281,A282,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 A268,A269,A274,A277,A278,A279,A280,A281,A282,GOBRD13:def 8;
end;
end;
A283: 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
A284: k > 1 and
A285: [i1,j1] in Indices G & (F.k)/.(len(F.k)-'1) = G*(i1,j1) and
A286: [i2,j2] in Indices G & (F.k)/.len(F.k) = G*(i2,j2);
A287: (len(F.k))-'1 <= len(F.k) by GOBOARD9:2;
A288: F.k is_sequence_on G by A246;
A289: len(F.k) = k by A92;
then A290: 1 <= (len(F.k))-'1 by A284,JORDAN3:12;
A291: (len(F.k)) -'1 +1 = len(F.k) by A284,A289,AMI_5:4;
then A292: left_cell(F.k,(len(F.k))-'1,G) meets C by A246,A290;
A293: (len(F.k))-'1 in dom(F.k) & len(F.k) in dom(F.k)
by A284,A287,A289,A290,FINSEQ_3:27;
A294: (len(F.k))-'1+(1+1) = (len(F.k))+1 by A291,XCMPLX_1:1;
A295: i1+1 > i1 & i2+1 > i2 & j1+1 > j1 & j2+1 > j2 by NAT_1:38;
assume front_right_cell(F.k,(len(F.k))-'1,G) meets C;
then consider i,j such that
A296: (F.k)^<*G*(i,j)*> turns_right (len(F.k))-'1,G and
A297: F.(k+1) = (F.k)^<*G*(i,j)*> by A78,A284,A288,A289,A292;
A298: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) & (F.(k+1))/.len(F.k) = G*(i2,j2)
by A285,A286,A293,A297,GROUP_5:95;
A299: (F.(k+1))/.(len(F.k)+1) = G*(i,j) by A297,TOPREAL4:1;
thus F.(k+1) turns_right (len(F.k))-'1,G by A296,A297;
thus i1 = i2 & j1+1 = j2 implies
[i2+1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2+1,j2)*>
by A285,A286,A291,A294,A295,A296,A297,A298,A299,GOBRD13:def 6;
thus i1+1 = i2 & j1 = j2 implies
[i2,j2-'1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2-'1)*>
by A285,A286,A291,A294,A295,A296,A297,A298,A299,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 A285,A286,A291,A294,A295,A296,A297,A298,A299,GOBRD13:def 6;
thus i1 = i2 & j1 = j2+1 implies
[i2-'1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2-'1,j2)*>
by A285,A286,A291,A294,A295,A296,A297,A298,A299,GOBRD13:def 6;
end;
A300:
for k holds ex i,j st [i,j] in Indices G & F.(k+1) = (F.k)^<*G*(i,j)*>
proof let k;
A301: F.k is_sequence_on G by A246;
A302: len(F.k) = k by A92;
per cases by REAL_1:def 5;
suppose k < 1;
then A303: k = 0 by RLVECT_1:98;
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;
thus thesis by A77,A247,A303,FINSEQ_1:47;
suppose
A304: 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 A247,A248,A304,FINSEQ_1:def 9;
suppose
A305: k > 1;
then A306: 1 <= (len(F.k))-'1 by A302,JORDAN3:12;
(len(F.k)) -'1 +1 = len(F.k) by A302,A305,AMI_5:4;
then consider i1,j1,i2,j2 being Nat such that
A307: [i1,j1] in Indices G & (F.k)/.(len(F.k)-'1) = G*(i1,j1) and
A308: [i2,j2] in Indices G & (F.k)/.len(F.k) = G*(i2,j2) and
A309: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A301,A306,JORDAN8:6;
now per cases;
suppose
A310: 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 A309;
suppose i1 = i2 & j1+1 = j2;
then [i2-'1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2-'1,j2)*>
by A249,A305,A307,A308,A310;
hence thesis;
suppose i1+1 = i2 & j1 = j2;
then [i2,j2+1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2+1)*>
by A249,A305,A307,A308,A310;
hence thesis;
suppose i1 = i2+1 & j1 = j2;
then [i2,j2-'1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2-'1)*>
by A249,A305,A307,A308,A310;
hence thesis;
suppose i1 = i2 & j1 = j2+1;
then [i2+1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2+1,j2)*>
by A249,A305,A307,A308,A310;
hence thesis;
end;
hence thesis;
suppose
A311: 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 A309;
suppose i1 = i2 & j1+1 = j2;
then [i2,j2+1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2+1)*>
by A266,A305,A307,A308,A311;
hence thesis;
suppose i1+1 = i2 & j1 = j2;
then [i2+1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2+1,j2)*>
by A266,A305,A307,A308,A311;
hence thesis;
suppose i1 = i2+1 & j1 = j2;
then [i2-'1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2-'1,j2)*>
by A266,A305,A307,A308,A311;
hence thesis;
suppose i1 = i2 & j1 = j2+1;
then [i2,j2-'1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2-'1)*>
by A266,A305,A307,A308,A311;
hence thesis;
end;
hence thesis;
suppose
A312: front_right_cell(F.k,(len(F.k))-'1,G) meets C;
now per cases by A309;
suppose i1 = i2 & j1+1 = j2;
then [i2+1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2+1,j2)*>
by A283,A305,A307,A308,A312;
hence thesis;
suppose i1+1 = i2 & j1 = j2;
then [i2,j2-'1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2-'1)*>
by A283,A305,A307,A308,A312;
hence thesis;
suppose i1 = i2+1 & j1 = j2;
then [i2,j2+1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2+1)*>
by A283,A305,A307,A308,A312;
hence thesis;
suppose i1 = i2 & j1 = j2+1;
then [i2-'1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2-'1,j2)*>
by A283,A305,A307,A308,A312;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
defpred P[Nat] means for m st m <= $1 holds (F.$1)|m = F.m;
A313: P[0]
proof let m;
assume
A314: m <= 0;
A315: 0 <= m by NAT_1:18;
0 = m by A314,NAT_1:18;
then (F.0)|m = (F.m)|Seg 0 by TOPREAL1:def 1;
then (F.0)|m = {} by FINSEQ_1:4,RELAT_1:110;
hence thesis by A77,A314,A315,AXIOMS:21;
end;
A316: for k st P[k] holds P[k+1]
proof let k such that
A317: for m st m <= k holds (F.k)|m = F.m;
let m such that
A318: m <= k+1;
per cases by A318,REAL_1:def 5;
suppose m < k+1;
then A319: m <= k by NAT_1:38;
A320: len(F.k) = k by A92;
consider i,j such that
[i,j] in Indices G and
A321: F.(k+1) = F.k^<*G*(i,j)*> by A300;
(F.(k+1))|m = (F.k)|m by A319,A320,A321,FINSEQ_5:25;
hence (F.(k+1))|m = F.m by A317,A319;
suppose
A322: m = k+1;
len(F.(k+1)) = k+1 by A92;
hence (F.(k+1))|m = F.m by A322,TOPREAL1:2;
end;
A323: for k holds P[k] from Ind(A313,A316);
A324: 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
A325: k > 1;
A326: F.k is_sequence_on G by A246;
A327: len(F.k) = k by A92;
then A328: 1 <= (len(F.k))-'1 by A325,JORDAN3:12;
(len(F.k)) -'1 +1 = len(F.k) by A325,A327,AMI_5:4;
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 A326,A328,JORDAN8:6;
hence thesis by A249,A266,A283,A325,A327;
end;
defpred P[Nat] means F.$1 is unfolded;
len(F.0) = 0 by A77,FINSEQ_1:25;
then A329: P[0] by SPPOL_2:27;
A330: for k st P[k] holds P[k+1]
proof let k such that
A331: F.k is unfolded;
A332: F.k is_sequence_on G by A246;
per cases;
suppose k <= 1;
then k+1 <= 1+1 by AXIOMS:24;
then len(F.(k+1)) <= 2 by A92;
hence F.(k+1) is unfolded by SPPOL_2:27;
suppose
A333: k > 1;
set m = k-'1;
A334: 1 <= m by A333,JORDAN3:12;
A335: m+1 = k by A333,AMI_5:4;
A336: len(F.k) = k by A92;
then consider i1,j1,i2,j2 being Nat such that
A337: [i1,j1] in Indices G & (F.k)/.m = G*(i1,j1) and
A338: [i2,j2] in Indices G & (F.k)/.len(F.k) = G*(i2,j2) and
A339: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A332,A334,A335,JORDAN8:6;
A340: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A337,GOBOARD5:1;
A341: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A338,GOBOARD5:1;
then A342: (i2-'1)+1 = i2 by AMI_5:4;
A343: (j2-'1)+1 = j2 by A341,AMI_5:4;
A344: LSeg(F.k,m) = LSeg(G*(i1,j1),G*(i2,j2)) by A334,A335,A336,A337,A338,
TOPREAL1:def 5;
now per cases;
suppose
A345: 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 A339;
suppose
A346: i1 = i2 & j1+1 = j2;
then A347: [i2-'1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2-'1,j2)*>
by A249,A333,A336,A337,A338,A345;
then 1 <= i2-'1 by GOBOARD5:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2-'1,j2)) =
{(F.k)/.len(F.k)}
by A338,A340,A341,A342,A344,A346,GOBOARD7:18;
hence F.(k+1) is unfolded by A331,A335,A336,A347,SPPOL_2:31;
suppose
A348: i1+1 = i2 & j1 = j2;
then A349: [i2,j2+1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2+1)*>
by A249,A333,A336,A337,A338,A345;
then j2+1 <= width G &
LSeg((F.k)/.len(F.k),G*(i2,j2+1))=LSeg(G*(i2,j2+1),(F.k)/.len(F.k))
by GOBOARD5:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2+1)) = {(F.k)/.len(F
.k)}
by A338,A340,A341,A344,A348,GOBOARD7:20;
hence F.(k+1) is unfolded by A331,A335,A336,A349,SPPOL_2:31;
suppose
A350: i1 = i2+1 & j1 = j2;
then A351: [i2,j2-'1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2-'1)*>
by A249,A333,A336,A337,A338,A345;
then 1 <= j2-'1 by GOBOARD5:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2-'1)) =
{(F.k)/.len(F.k)}
by A338,A340,A341,A343,A344,A350,GOBOARD7:17;
hence F.(k+1) is unfolded by A331,A335,A336,A351,SPPOL_2:31;
suppose
A352: i1 = i2 & j1 = j2+1;
then A353: [i2+1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2+1,j2)*>
by A249,A333,A336,A337,A338,A345;
then i2+1 <= len G by GOBOARD5:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2+1,j2)) = {(F.k)/.len(F
.k)}
by A338,A340,A341,A344,A352,GOBOARD7:19;
hence F.(k+1) is unfolded by A331,A335,A336,A353,SPPOL_2:31;
end;
hence F.(k+1) is unfolded;
suppose
A354: 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 A339;
suppose
A355: i1 = i2 & j1+1 = j2;
then A356: [i2,j2+1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2+1)*>
by A266,A333,A336,A337,A338,A354;
then 1 <= j2+1 & j2+1 <= width G & j2+1 = j1+(1+1)
by A355,GOBOARD5:1,XCMPLX_1:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2+1)) = {(F.k)/.len(F
.k)}
by A338,A340,A344,A355,GOBOARD7:15;
hence F.(k+1) is unfolded by A331,A335,A336,A356,SPPOL_2:31;
suppose
A357: i1+1 = i2 & j1 = j2;
then A358: [i2+1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2+1,j2)*>
by A266,A333,A336,A337,A338,A354;
then 1 <= i2+1 & i2+1 <= len G & i2+1 = i1+(1+1)
by A357,GOBOARD5:1,XCMPLX_1:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2+1,j2)) = {(F.k)/.len(F
.k)}
by A338,A340,A344,A357,GOBOARD7:16;
hence F.(k+1) is unfolded by A331,A335,A336,A358,SPPOL_2:31;
suppose
A359: i1 = i2+1 & j1 = j2;
then A360: [i2-'1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2-'1,j2)*>
by A266,A333,A336,A337,A338,A354;
then 1 <= i2-'1 & i2-'1+1+1 = i2-'1+(1+1)
by GOBOARD5:1,XCMPLX_1:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2-'1,j2)) =
{(F.k)/.len(F.k)}
by A338,A340,A342,A344,A359,GOBOARD7:16;
hence F.(k+1) is unfolded by A331,A335,A336,A360,SPPOL_2:31;
suppose
A361: i1 = i2 & j1 = j2+1;
then A362: [i2,j2-'1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2-'1)*>
by A266,A333,A336,A337,A338,A354;
then 1 <= j2-'1 & j2-'1+1+1 = j2-'1+(1+1)
by GOBOARD5:1,XCMPLX_1:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2-'1)) =
{(F.k)/.len(F.k)}
by A338,A340,A343,A344,A361,GOBOARD7:15;
hence F.(k+1) is unfolded by A331,A335,A336,A362,SPPOL_2:31;
end;
hence F.(k+1) is unfolded;
suppose
A363: front_right_cell(F.k,(len(F.k))-'1,G) meets C;
now per cases by A339;
suppose
A364: i1 = i2 & j1+1 = j2;
then A365: [i2+1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2+1,j2)*>
by A283,A333,A336,A337,A338,A363;
then i2+1 <= len G by GOBOARD5:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2+1,j2)) = {(F.k)/.len(F
.k)}
by A338,A340,A341,A344,A364,GOBOARD7:17;
hence F.(k+1) is unfolded by A331,A335,A336,A365,SPPOL_2:31;
suppose
A366: i1+1 = i2 & j1 = j2;
then A367: [i2,j2-'1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2-'1)*>
by A283,A333,A336,A337,A338,A363;
then 1 <= j2-'1 by GOBOARD5:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2-'1)) =
{(F.k)/.len(F.k)}
by A338,A340,A341,A343,A344,A366,GOBOARD7:18;
hence F.(k+1) is unfolded by A331,A335,A336,A367,SPPOL_2:31;
suppose
A368: i1 = i2+1 & j1 = j2;
then A369: [i2,j2+1] in Indices G & F.(k+1) = (F.k)^<*G*(i2,j2+1)*>
by A283,A333,A336,A337,A338,A363;
then j2+1 <= width G by GOBOARD5:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2,j2+1)) = {(F.k)/.len(F
.k)}
by A338,A340,A341,A344,A368,GOBOARD7:19;
hence F.(k+1) is unfolded by A331,A335,A336,A369,SPPOL_2:31;
suppose
A370: i1 = i2 & j1 = j2+1;
then A371: [i2-'1,j2] in Indices G & F.(k+1) = (F.k)^<*G*(i2-'1,j2)*>
by A283,A333,A336,A337,A338,A363;
then 1 <= i2-'1 by GOBOARD5:1;
then LSeg(F.k,m) /\ LSeg((F.k)/.len(F.k),G*(i2-'1,j2)) =
{(F.k)/.len(F.k)}
by A338,A340,A341,A342,A344,A370,GOBOARD7:20;
hence F.(k+1) is unfolded by A331,A335,A336,A371,SPPOL_2:31;
end;
hence F.(k+1) is unfolded;
end;
hence F.(k+1) is unfolded;
end;
A372: for k holds P[k] from Ind(A329,A330);
defpred K[Nat] means $1 >= 1 &
ex m st m in dom(F.$1) & m <> len(F.$1) & (F.$1)/.m = (F.$1)/.len(F.$1);
now assume
A373: 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);
defpred P[Nat] means F.$1 is one-to-one;
A374: P[0] by A77;
A375: for k st P[k] holds P[k+1]
proof let k; assume
A376: F.k is one-to-one;
now let n,m such that
A377: n in dom(F.(k+1)) & m in dom(F.(k+1)) and
A378: (F.(k+1))/.n = (F.(k+1))/.m;
consider i,j such that
[i,j] in Indices G and
A379: F.(k+1) = (F.k)^<*G*(i,j)*> by A300;
A380: 1 <= n & n <= len(F.(k+1)) & 1 <= m & m <= len(F.(k+1))
by A377,FINSEQ_3:27;
A381: len(F.k) = k & len(F.(k+1)) = k+1 by A92;
A382: 1 <= k+1 by NAT_1:37;
per cases by A380,A381,NAT_1:26;
suppose n <= k & m <= k;
then A383: n in dom(F.k) & m in dom(F.k) by A380,A381,FINSEQ_3:27;
then (F.(k+1))/.n = (F.k)/.n & (F.(k+1))/.m = (F.k)/.m
by A379,GROUP_5:95;
hence n = m by A376,A378,A383,PARTFUN2:17;
suppose n = k+1 & m <= k;
hence n = m by A373,A377,A378,A381,A382;
suppose n <= k & m = k+1;
hence n = m by A373,A377,A378,A381,A382;
suppose n = k+1 & m = k+1;
hence n = m;
end;
hence F.(k+1) is one-to-one by PARTFUN2:16;
end;
A384: for k holds P[k] from Ind(A374,A375);
A385: for k holds card rng(F.k) = k
proof let k;
F.k is one-to-one by A384;
hence card rng(F.k) = len(F.k) by FINSEQ_4:77
.= k by A92;
end;
set k = (len G)*(width G)+1;
A386: k > (len G)*(width G) by NAT_1:38;
A387: card Values G <= (len G)*(width G) by GOBRD13:8;
F.k is_sequence_on G by A246;
then rng(F.k) c= Values G by GOBRD13:9;
then card rng(F.k) <= card Values G by CARD_1:80;
then card rng(F.k) <= (len G)*(width G) by A387,AXIOMS:22;
hence contradiction by A385,A386;
end;
then A388: ex k st K[k];
consider k such that
A389: K[k] and
A390: for l st K[l]
holds k <= l from Min(A388);
consider m such that
A391: m in dom(F.k) and
A392: m <> len(F.k) and
A393: (F.k)/.m = (F.k)/.len(F.k) by A389;
A394: len(F.k) = k by A92;
0<k by A389,AXIOMS:22;
then reconsider f = F.k as non empty FinSequence of TOP-REAL 2 by A394,
FINSEQ_1:25;
A395: f is_sequence_on G by A246;
A396: 1 <= m & m <= len f by A391,FINSEQ_3:27;
then A397: m < len f by A392,REAL_1:def 5;
then 1 < len f by A396,AXIOMS:22;
then A398: len f >= 1+1 by NAT_1:38;
then A399: k >= 2 by A92;
reconsider f as non constant special unfolded non empty
FinSequence of TOP-REAL 2 by A372,A395,A398,JORDAN8:7,8;
set g = f/^(m-'1);
A400: m+1 <= len f by A397,NAT_1:38;
m-'1 <= m & m < m+1 by JORDAN3:7,NAT_1:38;
then m-'1 < m+1 by AXIOMS:22;
then A401: m-'1 < len f by A400,AXIOMS:22;
then A402: len g = len f - (m-'1) by RFINSEQ:def 2;
then (m-'1)-(m-'1) < len g by A401,REAL_1:54;
then len g > 0 by XCMPLX_1:14;
then reconsider g as non empty FinSequence of TOP-REAL 2
by FINSEQ_1:25;
1 in dom g by FINSEQ_5:6;
then A403: g/.1 = f/.(m-'1+1) by FINSEQ_5:30
.= f/.m by A396,AMI_5:4;
len g in dom g by FINSEQ_5:6;
then A404: g/.len g = f/.(m-'1+len g) by FINSEQ_5:30
.= f/.len f by A402,XCMPLX_1:27;
A405: g is_sequence_on G by A395,JORDAN8:5;
then A406: g is standard by JORDAN8:7;
A407: 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
A408: 1 <= i & i < len g and
A409: 1 <= j & j < len g and
A410: g/.i = g/.j and
A411: i <> j;
i in dom g by A408,FINSEQ_3:27;
then A412: g/.i = f/.(m-'1+i) by FINSEQ_5:30;
j in dom g by A409,FINSEQ_3:27;
then A413: g/.j = f/.(m-'1+j) by FINSEQ_5:30;
A414: 0 <= m-'1 by NAT_1:18;
per cases by A411,REAL_1:def 5;
suppose
A415: i < j;
set l = m-'1+j, m'= m-'1+i;
A416: m' < l by A415,REAL_1:53;
A417: l < k by A394,A402,A409,REAL_1:86;
then A418: f|l = F.l by A323;
0+j <= l by A414,AXIOMS:24;
then A419: 1 <= l by A409,AXIOMS:22;
A420: len(F.l) = l by A92;
0+i <= m' by A414,AXIOMS:24;
then 1 <= m' by A408,AXIOMS:22;
then A421: m' in dom(F.l) by A416,A420,FINSEQ_3:27;
then A422: (F.l)/.m' = f/.m' by A418,TOPREAL1:1;
l in dom(F.l) by A419,A420,FINSEQ_3:27;
then (F.l)/.l = f/.l by A418,TOPREAL1:1;
hence contradiction by A390,A410,A412,A413,A416,A417,A419,A420,A421,A422;
suppose
A423: j < i;
set l = m-'1+i, m'= m-'1+j;
A424: m' < l by A423,REAL_1:53;
A425: l < k by A394,A402,A408,REAL_1:86;
then A426: f|l = F.l by A323;
0+i <= l by A414,AXIOMS:24;
then A427: 1 <= l by A408,AXIOMS:22;
A428: len(F.l) = l by A92;
0+j <= m' by A414,AXIOMS:24;
then 1 <= m' by A409,AXIOMS:22;
then A429: m' in dom(F.l) by A424,A428,FINSEQ_3:27;
then A430: (F.l)/.m' = f/.m' by A426,TOPREAL1:1;
l in dom(F.l) by A427,A428,FINSEQ_3:27;
then (F.l)/.l = f/.l by A426,TOPREAL1:1;
hence contradiction by A390,A410,A412,A413,A424,A425,A427,A428,A429,A430;
end;
A431: for i st 1 < i & i < j & j <= len g holds g/.i <> g/.j
proof let i such that
A432: 1 < i and
A433: i < j and
A434: j <= len g and
A435: g/.i = g/.j;
A436: 1 < j by A432,A433,AXIOMS:22;
A437: i < len g by A433,A434,AXIOMS:22;
then A438: 1 < len g by A432,AXIOMS:22;
per cases;
suppose j <> len g;
then j < len g by A434,REAL_1:def 5;
hence contradiction by A407,A432,A433,A435,A436,A437;
suppose j = len g;
hence contradiction by A393,A403,A404,A407,A432,A433,A435,A438;
end;
A439: for i st 1 <= i & i < j & j < len g holds g/.i <> g/.j
proof let i such that
A440: 1 <= i and
A441: i < j and
A442: j < len g and
A443: g/.i = g/.j;
A444: 1 < j by A440,A441,AXIOMS:22;
i < len g by A441,A442,AXIOMS:22;
hence contradiction by A407,A440,A441,A442,A443,A444;
end;
A445: 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
A446: 1 <= i & i+1 <= len f;
consider i1,j1,i2,j2 such that
A447: [i1,j1] in Indices G and
A448: f/.i = G*(i1,j1) and
A449: [i2,j2] in Indices G and
A450: f/.(i+1) = G*(i2,j2) and
A451: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A395,A446,JORDAN8:6;
A452: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A447,GOBOARD5:1;
A453: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A449,GOBOARD5:1;
A454: i1+1 > i1 & j1+1 > j1 & i2+1 > i2 & j2+1 > j2 by NAT_1:38;
per cases by A451;
suppose
A455: i1 = i2 & j1+1 = j2;
A456: i1-'1 <= len G by A452,JORDAN3:7;
left_cell(f,i,G) = cell(G,i1-'1,j1)
by A395,A446,A447,A448,A449,A450,A454,A455,GOBRD13:def 3;
hence thesis by A452,A456,GOBRD11:35;
suppose
i1+1 = i2 & j1 = j2;
then left_cell(f,i,G) = cell(G,i1,j1)
by A395,A446,A447,A448,A449,A450,A454,GOBRD13:def 3;
hence thesis by A452,GOBRD11:35;
suppose
A457: i1 = i2+1 & j1 = j2;
A458: j2-'1 <= width G by A453,JORDAN3:7;
left_cell(f,i,G) = cell(G,i2,j2-'1)
by A395,A446,A447,A448,A449,A450,A454,A457,GOBRD13:def 3;
hence thesis by A453,A458,GOBRD11:35;
suppose
i1 = i2 & j1 = j2+1;
then left_cell(f,i,G) = cell(G,i1,j2)
by A395,A446,A447,A448,A449,A450,A454,GOBRD13:def 3;
hence thesis by A452,A453,GOBRD11:35;
end;
A459: g is s.c.c.
proof
let i,j such that
A460: i+1 < j and
A461: i > 1 & j < len g or j+1 < len g;
A462: j <= j+1 by NAT_1:37;
then A463: i+1 < j+1 by A460,AXIOMS:22;
A464: 1 <= i+1 by NAT_1:37;
A465: 1 < j by A460,NAT_1:37;
i < j by A460,NAT_1:38;
then A466: i < j+1 by A462,AXIOMS:22;
per cases by A461,RLVECT_1:99;
suppose
A467: i > 1 & j < len g;
then A468: i+1 < len g by A460,AXIOMS:22;
then A469: LSeg(g,i) = LSeg(g/.i,g/.(i+1)) by A467,TOPREAL1:def 5;
A470: 1 < i+1 by A467,NAT_1:38;
A471: i < len g by A468,NAT_1:38;
consider i1,j1,i2,j2 such that
A472: [i1,j1] in Indices G and
A473: g/.i = G*(i1,j1) and
A474: [i2,j2] in Indices G and
A475: g/.(i+1) = G*(i2,j2) and
A476: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A405,A467,A468,JORDAN8:6;
A477: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A472,GOBOARD5:1;
A478: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A474,GOBOARD5:1;
A479: j+1 <= len g by A467,NAT_1:38;
then A480: LSeg(g,j) = LSeg(g/.j,g/.(j+1)) by A465,TOPREAL1:def 5;
consider i1',j1',i2',j2' being Nat such that
A481: [i1',j1'] in Indices G and
A482: g/.j = G*(i1',j1') and
A483: [i2',j2'] in Indices G and
A484: g/.(j+1) = G*(i2',j2') and
A485: i1' = i2' & j1'+1 = j2' or i1'+1 = i2' & j1' = j2' or
i1' = i2'+1 & j1' = j2' or i1' = i2' & j1' = j2'+1
by A405,A465,A479,JORDAN8:6;
A486: 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G by A481,GOBOARD5:1
;
A487: 1 <= i2' & i2' <= len G & 1 <= j2' & j2' <= width G by A483,GOBOARD5:1
;
assume LSeg(g,i) /\ LSeg(g,j) <> {};
then A488: LSeg(g,i) meets LSeg(g,j) by XBOOLE_0:def 7;
now per cases by A476,A485;
suppose
A489: i1 = i2 & j1+1 = j2 & i1' = i2' & j1'+1 = j2';
then A490: i1 = i1' by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,GOBOARD7:21;
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A489,GOBOARD7:24;
suppose j1 = j1';
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A490;
suppose j1 = j1'+1;
hence contradiction by A431,A466,A467,A473,A479,A484,A489,A490;
suppose j1+1 = j1';
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A489,
A490;
end;
hence contradiction;
suppose
A491: i1 = i2 & j1+1 = j2 & i1'+1 = i2' & j1' = j2';
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A491,GOBOARD7:23;
suppose i1 = i1' & j1 = j1';
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482;
suppose i1 = i1' & j1+1 = j1';
hence contradiction by A431,A460,A467,A470,A475,A482,A491;
suppose i1 = i1'+1 & j1 = j1';
hence contradiction by A431,A466,A467,A473,A479,A484,A491;
suppose i1 = i1'+1 & j1+1 = j1';
hence contradiction by A431,A463,A470,A475,A479,A484,A491;
end;
hence contradiction;
suppose
A492: i1 = i2 & j1+1 = j2 & i1' = i2'+1 & j1' = j2';
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A492,GOBOARD7:23;
suppose i1 = i2' & j1' = j1;
hence contradiction by A431,A466,A467,A473,A479,A484,A492;
suppose i1 = i2' & j1+1 = j1';
hence contradiction by A431,A463,A470,A475,A479,A484,A492;
suppose i1 = i2'+1 & j1' = j1;
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A492;
suppose i1 = i2'+1 & j1+1 = j1';
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A492;
end;
hence contradiction;
suppose
A493: i1 = i2 & j1+1 = j2 & i1' = i2' & j1' = j2'+1;
then A494: i1 = i1' by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,GOBOARD7:21;
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A493,GOBOARD7:24;
suppose j1 = j2';
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A493,
A494;
suppose j1 = j2'+1;
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A493,
A494;
suppose j1+1 = j2';
hence contradiction by A431,A463,A470,A475,A479,A484,A493,A494;
end;
hence contradiction;
suppose
A495: i1+1 = i2 & j1 = j2 & i1' = i2' & j1'+1 = j2';
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A495,GOBOARD7:23;
suppose i1' = i1 & j1 = j1';
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482;
suppose i1' = i1 & j1'+1 = j1;
hence contradiction by A431,A466,A467,A473,A479,A484,A495;
suppose i1' = i1+1 & j1 = j1';
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A495;
suppose i1' = i1+1 & j1'+1 = j1;
hence contradiction by A431,A463,A470,A475,A479,A484,A495;
end;
hence contradiction;
suppose
A496: i1+1 = i2 & j1 = j2 & i1'+1 = i2' & j1' = j2';
then A497: j1 = j1' by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,GOBOARD7:22;
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A496,GOBOARD7:25;
suppose i1 = i1';
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A497;
suppose i1 = i1'+1;
hence contradiction by A431,A466,A467,A473,A479,A484,A496,A497;
suppose i1+1 = i1';
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A496,
A497;
end;
hence contradiction;
suppose
A498: i1+1 = i2 & j1 = j2 & i1' = i2'+1 & j1' = j2';
then A499: j1 = j1' by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,GOBOARD7:22;
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A498,GOBOARD7:25;
suppose i1 = i2';
hence contradiction by A431,A466,A467,A473,A479,A484,A498,A499;
suppose i1 = i2'+1;
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A498,
A499;
suppose i1+1 = i2';
hence contradiction by A431,A463,A470,A475,A479,A484,A498,A499;
end;
hence contradiction;
suppose
A500: i1+1 = i2 & j1 = j2 & i1' = i2' & j1' = j2'+1;
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A500,GOBOARD7:23;
suppose i1' = i1 & j1 = j2';
hence contradiction by A431,A466,A467,A473,A479,A484,A500;
suppose i1' = i1 & j2'+1 = j1;
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A500;
suppose i1' = i1+1 & j1 = j2';
hence contradiction by A431,A463,A470,A475,A479,A484,A500;
suppose i1' = i1+1 & j2'+1 = j1;
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A500;
end;
hence contradiction;
suppose
A501: i1 = i2+1 & j1 = j2 & i1' = i2' & j1'+1 = j2';
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A501,GOBOARD7:23;
suppose i1' = i2 & j1' = j1;
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A501;
suppose i1' = i2 & j1'+1 = j1;
hence contradiction by A431,A463,A470,A475,A479,A484,A501;
suppose i1' = i2+1 & j1' = j1;
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A501;
suppose i1' = i2+1 & j1'+1 = j1;
hence contradiction by A431,A466,A467,A473,A479,A484,A501;
end;
hence contradiction;
suppose
A502: i1 = i2+1 & j1 = j2 & i1'+1 = i2' & j1' = j2';
then A503: j1 = j1' by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,GOBOARD7:22;
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A502,GOBOARD7:25;
suppose i2 = i1';
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A502,
A503;
suppose i2 = i1'+1;
hence contradiction by A431,A463,A470,A475,A479,A484,A502,A503;
suppose i2+1 = i1';
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A502,
A503;
end;
hence contradiction;
suppose
A504: i1 = i2+1 & j1 = j2 & i1' = i2'+1 & j1' = j2';
then A505: j1 = j1' by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,GOBOARD7:22;
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A504,GOBOARD7:25;
suppose i2 = i2';
hence contradiction by A431,A463,A470,A475,A479,A484,A504,A505;
suppose i2 = i2'+1;
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A504,
A505;
suppose i2+1 = i2';
hence contradiction by A431,A466,A467,A473,A479,A484,A504,A505;
end;
hence contradiction;
suppose
A506: i1 = i2+1 & j1 = j2 & i1' = i2' & j1' = j2'+1;
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A506,GOBOARD7:23;
suppose i1' = i2 & j2' = j1;
hence contradiction by A431,A463,A470,A475,A479,A484,A506;
suppose i1' = i2 & j2'+1 = j1;
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A506;
suppose i1' = i2+1 & j2' = j1;
hence contradiction by A431,A466,A467,A473,A479,A484,A506;
suppose i1' = i2+1 & j2'+1 = j1;
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A506;
end;
hence contradiction;
suppose
A507: i1 = i2 & j1 = j2+1 & i1' = i2' & j1'+1 = j2';
then A508: i1 = i1' by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,GOBOARD7:21;
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A507,GOBOARD7:24;
suppose j2 = j1';
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A507,
A508;
suppose j2 = j1'+1;
hence contradiction by A431,A463,A470,A475,A479,A484,A507,A508;
suppose j2+1 = j1';
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A507,
A508;
end;
hence contradiction;
suppose
A509: i1 = i2 & j1 = j2+1 & i1'+1 = i2' & j1' = j2';
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A509,GOBOARD7:23;
suppose i1 = i1' & j2 = j1';
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A509;
suppose i1 = i1' & j2+1 = j1';
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A509;
suppose i1 = i1'+1 & j2 = j1';
hence contradiction by A431,A463,A470,A475,A479,A484,A509;
suppose i1 = i1'+1 & j2+1 = j1';
hence contradiction by A431,A466,A467,A473,A479,A484,A509;
end;
hence contradiction;
suppose
A510: i1 = i2 & j1 = j2+1 & i1' = i2'+1 & j1' = j2';
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A510,GOBOARD7:23;
suppose i1 = i2' & j2 = j1';
hence contradiction by A431,A463,A470,A475,A479,A484,A510;
suppose i1 = i2' & j2+1 = j1';
hence contradiction by A431,A466,A467,A473,A479,A484,A510;
suppose i1 = i2'+1 & j2 = j1';
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A510;
suppose i1 = i2'+1 & j2+1 = j1';
hence contradiction by A407,A460,A462,A465,A467,A471,A473,A482,A510;
end;
hence contradiction;
suppose
A511: i1 = i2 & j1 = j2+1 & i1' = i2' & j1' = j2'+1;
then A512: i1 = i1' by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,GOBOARD7:21;
now per cases by A469,A473,A475,A477,A478,A480,A482,A484,A486,A487,
A488,A511,GOBOARD7:24;
suppose j2 = j2';
hence contradiction by A431,A463,A470,A475,A479,A484,A511,A512;
suppose j2 = j2'+1;
hence contradiction by A407,A460,A464,A465,A467,A468,A475,A482,A511,
A512;
suppose j2+1 = j2';
hence contradiction by A431,A466,A467,A473,A479,A484,A511,A512;
end;
hence contradiction;
end;
hence contradiction;
suppose i = 0 & j+1 < len g;
then LSeg(g,i) = {} by TOPREAL1:def 5;
hence LSeg(g,i) /\ LSeg(g,j) = {};
suppose
A513: 1 <= i & j+1 < len g;
then A514: i+1 < len g by A463,AXIOMS:22;
then A515: LSeg(g,i) = LSeg(g/.i,g/.(i+1)) by A513,TOPREAL1:def 5;
A516: 1 < i+1 by A513,NAT_1:38;
A517: i < len g by A514,NAT_1:38;
A518: j < len g by A513,NAT_1:37;
consider i1,j1,i2,j2 such that
A519: [i1,j1] in Indices G and
A520: g/.i = G*(i1,j1) and
A521: [i2,j2] in Indices G and
A522: g/.(i+1) = G*(i2,j2) and
A523: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A405,A513,A514,JORDAN8:6;
A524: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A519,GOBOARD5:1;
A525: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A521,GOBOARD5:1;
A526: LSeg(g,j) = LSeg(g/.j,g/.(j+1)) by A465,A513,TOPREAL1:def 5;
consider i1',j1',i2',j2' being Nat such that
A527: [i1',j1'] in Indices G and
A528: g/.j = G*(i1',j1') and
A529: [i2',j2'] in Indices G and
A530: g/.(j+1) = 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 A405,A465,A513,JORDAN8:6;
A532: 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G by A527,GOBOARD5:1
;
A533: 1 <= i2' & i2' <= len G & 1 <= j2' & j2' <= width G by A529,GOBOARD5:1
;
assume LSeg(g,i) /\ LSeg(g,j) <> {};
then A534: LSeg(g,i) meets LSeg(g,j) by XBOOLE_0:def 7;
now per cases by A523,A531;
suppose
A535: i1 = i2 & j1+1 = j2 & i1' = i2' & j1'+1 = j2';
then A536: i1 = i1' by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,GOBOARD7:21;
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A535,GOBOARD7:24;
suppose j1 = j1';
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A536;
suppose j1 = j1'+1;
hence contradiction by A439,A466,A513,A520,A530,A535,A536;
suppose j1+1 = j1';
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A535,
A536;
end;
hence contradiction;
suppose
A537: i1 = i2 & j1+1 = j2 & i1'+1 = i2' & j1' = j2';
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A537,GOBOARD7:23;
suppose i1 = i1' & j1 = j1';
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528;
suppose i1 = i1' & j1+1 = j1';
hence contradiction by A431,A460,A516,A518,A522,A528,A537;
suppose i1 = i1'+1 & j1 = j1';
hence contradiction by A439,A466,A513,A520,A530,A537;
suppose i1 = i1'+1 & j1+1 = j1';
hence contradiction by A431,A463,A513,A516,A522,A530,A537;
end;
hence contradiction;
suppose
A538: i1 = i2 & j1+1 = j2 & i1' = i2'+1 & j1' = j2';
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A538,GOBOARD7:23;
suppose i1 = i2' & j1' = j1;
hence contradiction by A439,A466,A513,A520,A530,A538;
suppose i1 = i2' & j1+1 = j1';
hence contradiction by A431,A463,A513,A516,A522,A530,A538;
suppose i1 = i2'+1 & j1' = j1;
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A538;
suppose i1 = i2'+1 & j1+1 = j1';
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A538;
end;
hence contradiction;
suppose
A539: i1 = i2 & j1+1 = j2 & i1' = i2' & j1' = j2'+1;
then A540: i1 = i1' by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,GOBOARD7:21;
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A539,GOBOARD7:24;
suppose j1 = j2';
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A539,
A540;
suppose j1 = j2'+1;
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A539,A540;
suppose j1+1 = j2';
hence contradiction by A431,A463,A513,A516,A522,A530,A539,A540;
end;
hence contradiction;
suppose
A541: i1+1 = i2 & j1 = j2 & i1' = i2' & j1'+1 = j2';
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A541,GOBOARD7:23;
suppose i1' = i1 & j1 = j1';
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528;
suppose i1' = i1 & j1'+1 = j1;
hence contradiction by A439,A466,A513,A520,A530,A541;
suppose i1' = i1+1 & j1 = j1';
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A541;
suppose i1' = i1+1 & j1'+1 = j1;
hence contradiction by A431,A463,A513,A516,A522,A530,A541;
end;
hence contradiction;
suppose
A542: i1+1 = i2 & j1 = j2 & i1'+1 = i2' & j1' = j2';
then A543: j1 = j1' by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,GOBOARD7:22;
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A542,GOBOARD7:25;
suppose i1 = i1';
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A543;
suppose i1 = i1'+1;
hence contradiction by A439,A466,A513,A520,A530,A542,A543;
suppose i1+1 = i1';
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A542,
A543;
end;
hence contradiction;
suppose
A544: i1+1 = i2 & j1 = j2 & i1' = i2'+1 & j1' = j2';
then A545: j1 = j1' by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,GOBOARD7:22;
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A544,GOBOARD7:25;
suppose i1 = i2';
hence contradiction by A439,A466,A513,A520,A530,A544,A545;
suppose i1 = i2'+1;
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A544,A545;
suppose i1+1 = i2';
hence contradiction by A431,A463,A513,A516,A522,A530,A544,A545;
end;
hence contradiction;
suppose
A546: i1+1 = i2 & j1 = j2 & i1' = i2' & j1' = j2'+1;
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A546,GOBOARD7:23;
suppose i1' = i1 & j1 = j2';
hence contradiction by A439,A466,A513,A520,A530,A546;
suppose i1' = i1 & j2'+1 = j1;
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A546;
suppose i1' = i1+1 & j1 = j2';
hence contradiction by A431,A463,A513,A516,A522,A530,A546;
suppose i1' = i1+1 & j2'+1 = j1;
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A546;
end;
hence contradiction;
suppose
A547: i1 = i2+1 & j1 = j2 & i1' = i2' & j1'+1 = j2';
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A547,GOBOARD7:23;
suppose i1' = i2 & j1' = j1;
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A547;
suppose i1' = i2 & j1'+1 = j1;
hence contradiction by A431,A463,A513,A516,A522,A530,A547;
suppose i1' = i2+1 & j1' = j1;
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A547;
suppose i1' = i2+1 & j1'+1 = j1;
hence contradiction by A439,A466,A513,A520,A530,A547;
end;
hence contradiction;
suppose
A548: i1 = i2+1 & j1 = j2 & i1'+1 = i2' & j1' = j2';
then A549: j1 = j1' by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,GOBOARD7:22;
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A548,GOBOARD7:25;
suppose i2 = i1';
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A548,
A549;
suppose i2 = i1'+1;
hence contradiction by A431,A463,A513,A516,A522,A530,A548,A549;
suppose i2+1 = i1';
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A548,A549;
end;
hence contradiction;
suppose
A550: i1 = i2+1 & j1 = j2 & i1' = i2'+1 & j1' = j2';
then A551: j1 = j1' by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,GOBOARD7:22;
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A550,GOBOARD7:25;
suppose i2 = i2';
hence contradiction by A431,A463,A513,A516,A522,A530,A550,A551;
suppose i2 = i2'+1;
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A550,
A551;
suppose i2+1 = i2';
hence contradiction by A439,A466,A513,A520,A530,A550,A551;
end;
hence contradiction;
suppose
A552: i1 = i2+1 & j1 = j2 & i1' = i2' & j1' = j2'+1;
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A552,GOBOARD7:23;
suppose i1' = i2 & j2' = j1;
hence contradiction by A431,A463,A513,A516,A522,A530,A552;
suppose i1' = i2 & j2'+1 = j1;
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A552;
suppose i1' = i2+1 & j2' = j1;
hence contradiction by A439,A466,A513,A520,A530,A552;
suppose i1' = i2+1 & j2'+1 = j1;
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A552;
end;
hence contradiction;
suppose
A553: i1 = i2 & j1 = j2+1 & i1' = i2' & j1'+1 = j2';
then A554: i1 = i1' by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,GOBOARD7:21;
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A553,GOBOARD7:24;
suppose j2 = j1';
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A553,
A554;
suppose j2 = j1'+1;
hence contradiction by A431,A463,A513,A516,A522,A530,A553,A554;
suppose j2+1 = j1';
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A553,A554;
end;
hence contradiction;
suppose
A555: i1 = i2 & j1 = j2+1 & i1'+1 = i2' & j1' = j2';
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A555,GOBOARD7:23;
suppose i1 = i1' & j2 = j1';
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A555;
suppose i1 = i1' & j2+1 = j1';
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A555;
suppose i1 = i1'+1 & j2 = j1';
hence contradiction by A431,A463,A513,A516,A522,A530,A555;
suppose i1 = i1'+1 & j2+1 = j1';
hence contradiction by A439,A466,A513,A520,A530,A555;
end;
hence contradiction;
suppose
A556: i1 = i2 & j1 = j2+1 & i1' = i2'+1 & j1' = j2';
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A556,GOBOARD7:23;
suppose i1 = i2' & j2 = j1';
hence contradiction by A431,A463,A513,A516,A522,A530,A556;
suppose i1 = i2' & j2+1 = j1';
hence contradiction by A439,A466,A513,A520,A530,A556;
suppose i1 = i2'+1 & j2 = j1';
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A556;
suppose i1 = i2'+1 & j2+1 = j1';
hence contradiction by A407,A460,A462,A465,A513,A517,A518,A520,A528,
A556;
end;
hence contradiction;
suppose
A557: i1 = i2 & j1 = j2+1 & i1' = i2' & j1' = j2'+1;
then A558: i1 = i1' by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,GOBOARD7:21;
now per cases by A515,A520,A522,A524,A525,A526,A528,A530,A532,A533,
A534,A557,GOBOARD7:24;
suppose j2 = j2';
hence contradiction by A431,A463,A513,A516,A522,A530,A557,A558;
suppose j2 = j2'+1;
hence contradiction by A407,A460,A464,A465,A514,A518,A522,A528,A557,
A558;
suppose j2+1 = j2';
hence contradiction by A439,A466,A513,A520,A530,A557,A558;
end;
hence contradiction;
end;
hence contradiction;
end;
m+1-(m-'1) <= len g by A400,A402,REAL_1:49;
then m+1-(m-1) <= len g by A396,SCMFSA_7:3;
then 1+m-m+1 <= len g by XCMPLX_1:37;
then A559: 1+1 <= len g by XCMPLX_1:26;
g is non constant
proof
take 1,2;
thus
A560: 1 in dom g by FINSEQ_5:6;
thus
A561: 2 in dom g by A559,FINSEQ_3:27;
then g/.1 <> g/.(1+1) by A406,A560,GOBOARD7:31;
then g.1 <> g/.(1+1) by A560,FINSEQ_4:def 4;
hence g.1 <> g.2 by A561,FINSEQ_4:def 4;
end;
then reconsider g as standard non constant special_circular_sequence
by A393,A403,A404,A405,A459,FINSEQ_6:def 1,JORDAN8:7;
A562: for j,k st 1 <= j & j <= k holds (F.k)/.j = (F.j)/.j
proof
let j,k;
assume that
A563: 1 <= j and
A564: j <= k;
A565: (F.k)|j = F.j by A323,A564;
j <= len(F.k) by A92,A564;
then len(F.k|j) = j by TOPREAL1:3;
then j in dom((F.k)|j) by A563,FINSEQ_3:27;
hence (F.k)/.j = (F.j)/.j by A565,TOPREAL1:1;
end;
reconsider Lg' = (L~g)` as Subset of TOP-REAL 2;
A566: C c= Lg'
proof
let c be set;
assume that
A567: c in C and
A568: not c in Lg';
reconsider c as Point of TOP-REAL 2 by A567;
c in L~g by A568,SUBSET_1:50;
then consider i such that
A569: 1 <= i & i+1 <= len g and
A570: c in LSeg(g/.i,g/.(i+1)) by SPPOL_2:14;
i in dom g & i+1 in dom g by A569,GOBOARD2:3;
then A571: g/.i = f/.(i+(m-'1)) & g/.(i+1) = f/.(i+1+(m-'1)) by FINSEQ_5:30;
A572: 1 <= i+(m-'1) by A569,NAT_1:37;
A573: i+1+(m-'1) = i+(m-'1)+1 by XCMPLX_1:1;
then i+(m-'1)+1 <= (len g)+(m-'1) by A569,AXIOMS:24;
then A574: i+(m-'1)+1 <= len f by A402,XCMPLX_1:27;
then c in LSeg(f,i+(m-'1)) by A570,A571,A572,A573,TOPREAL1:def 5;
then c in right_cell(f,i+(m-'1),G) /\ left_cell(f,i+(m-'1),G)
by A395,A572,A574,GOBRD13:30;
then c in right_cell(f,i+(m-'1),G) by XBOOLE_0:def 3;
then right_cell(f,i+(m-'1),G) meets C by A567,XBOOLE_0:3;
hence contradiction by A246,A572,A574;
end;
A575: TOP-REAL 2 = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
A576: the carrier of TOP-REAL 2 = the carrier of Euclid 2 by TOPREAL3:13;
L~g is closed by SPPOL_1:49;
then (L~g)` is open by TOPS_1:29;
then Lg' is open;
then A577: (L~g)` = Int (L~g)` by TOPS_1:55;
A578: L~g c= L~f by JORDAN3:75;
A579: LeftComp g is_a_component_of (L~g)` &
RightComp g is_a_component_of (L~g)` by GOBOARD9:def 1,def 2;
A580: 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
A581: L~h c= L~f;
let Comp be Subset of TOP-REAL 2 such that
A582: Comp is_a_component_of (L~h)`;
let n such that
A583: 1 <= n & n+1 <= len f and
A584: f/.n in Comp and
A585: not f/.n in L~h;
set rc=left_cell(f,n,G)\L~h;
reconsider rc as Subset of TOP-REAL 2;
A586: rc c= left_cell(f,n,G) by XBOOLE_1:36;
A587: rc = left_cell(f,n,G) /\ (L~h)` by SUBSET_1:32;
A588: rc meets C
proof
left_cell(f,n,G) meets C by A246,A583;
then consider p being set such that
A589: p in left_cell(f,n,G) & p in C by XBOOLE_0:3;
reconsider p as Element of TOP-REAL 2 by A589;
now take p;
now
assume p in L~h;
then consider j such that
A590: 1 <= j and
A591: j+1 <= len f and
A592: p in LSeg(f,j) by A581,SPPOL_2:13;
p in right_cell(f,j,G) /\ left_cell(f,j,G) by A395,A590,A591,A592,
GOBRD13:30;
then A593: p in right_cell(f,j,G) by XBOOLE_0:def 3;
right_cell(f,j,G) misses C by A246,A590,A591;
hence contradiction by A589,A593,XBOOLE_0:3;
end;
hence p in rc by A589,XBOOLE_0:def 4;
thus p in C by A589;
end; hence thesis by XBOOLE_0:3;
end;
A594: Int left_cell(f,n,G) is connected by A395,A583,JORDAN9:12;
Int left_cell(f,n,G) misses L~f by A395,A583,JORDAN9:17;
then Int left_cell(f,n,G) misses L~h by A581,XBOOLE_1:63;
then A595: Int left_cell(f,n,G) c= (L~h)` by SUBSET_1:43;
Int left_cell(f,n,G) c= left_cell(f,n,G) by TOPS_1:44;
then A596: Int left_cell(f,n,G) c= rc by A587,A595,XBOOLE_1:19;
rc c= Cl Int left_cell(f,n,G) by A395,A583,A586,JORDAN9:13;
then A597: rc is connected by A594,A596,CONNSP_1:19;
f/.n in left_cell(f,n,G) by A395,A583,JORDAN9:10;
then f/.n in rc by A585,XBOOLE_0:def 4;
then A598: rc meets Comp by A584,XBOOLE_0:3;
rc c= (L~h)` by A587,XBOOLE_1:17;
then rc c= Comp by A582,A597,A598,GOBOARD9:6;
hence C meets Comp by A588,XBOOLE_1:63;
end;
A599:
C meets LeftComp g
proof
left_cell(f,m,G) meets C by A246,A396,A400;
then consider p being set such that
A600: p in left_cell(f,m,G) & p in C by XBOOLE_0:3;
reconsider p as Element of TOP-REAL 2 by A600;
now take p;
thus p in C by A600;
reconsider u = p as Element of Euclid 2 by A576;
consider r being real number such that
A601: r > 0 and
A602: Ball(u,r) c= (L~g)` by A566,A577,A600,GOBOARD6:8;
reconsider r as Real by XREAL_0:def 1;
A603: p in Ball(u,r) by A601,TBSP_1:16;
Ball(u,r) is Subset of TOP-REAL 2 by A575,TOPMETR:16;
then reconsider B = Ball(u,r) as non empty Subset of TOP-REAL 2
by A601,TBSP_1:16;
A604: B is connected by SPRECT_3:17;
left_cell(g,1,G) c= left_cell(g,1) by A405,A559,GOBRD13:34;
then A605: Int left_cell(g,1,G) c= Int left_cell(g,1) by TOPS_1:48;
Int left_cell(g,1) c= LeftComp g by A559,GOBOARD9:24;
then Int left_cell(g,1,G) c= LeftComp g by A605,XBOOLE_1:1;
then Int left_cell(f,m-'1+1,G) c= LeftComp g by A395,A401,A559,GOBRD13:33;
then A606: Int left_cell(f,m,G) c= LeftComp g by A396,AMI_5:4;
A607: left_cell(f,m,G) = Cl Int left_cell(f,m,G) by A396,A400,A445;
B is open by GOBOARD6:6;
then A608: Int left_cell(f,m,G) meets B by A600,A603,A607,TOPS_1:39;
A609: p in B by A601,TBSP_1:16;
B c= LeftComp g by A579,A602,A604,A606,A608,GOBOARD9:6;
hence p in LeftComp g by A609;
end; hence thesis by XBOOLE_0:3;
end;
m = 1
proof
assume m <> 1;
then