Copyright (c) 1999 Association of Mizar Users
environ
vocabulary FINSEQ_1, BOOLE, PRE_TOPC, RELAT_2, CONNSP_1, RELAT_1, FINSEQ_5,
ARYTM_1, GOBOARD1, EUCLID, MATRIX_1, ABSVALUE, GOBRD13, FUNCT_1,
TOPREAL1, RFINSEQ, GOBOARD5, TOPS_1, TREES_1, SPPOL_1, MCART_1, TARSKI,
SUBSET_1, SEQM_3, GOBOARD9, COMPTS_1, JORDAN8, PSCOMP_1, GROUP_1,
ARYTM_3, SPRECT_2, CARD_1, PCOMPS_1, METRIC_1, JORDAN9, FINSEQ_4, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, GOBOARD5, STRUCT_0, ORDINAL1, NUMBERS,
XREAL_0, REAL_1, NAT_1, BINARITH, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2,
CARD_1, CARD_4, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, RFINSEQ,
MATRIX_1, METRIC_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1,
EUCLID, TOPREAL1, GOBOARD1, SPPOL_1, PSCOMP_1, SPRECT_2, GOBOARD9,
JORDAN8, GOBRD13;
constructors REAL_1, FINSEQ_4, CARD_4, RFINSEQ, BINARITH, TOPS_1, CONNSP_1,
COMPTS_1, SPPOL_1, PSCOMP_1, REALSET1, SPRECT_2, GOBOARD9, JORDAN8,
GOBRD13, GROUP_1, MEMBERED;
clusters PSCOMP_1, RELSET_1, FINSEQ_1, SPPOL_2, REVROT_1, SPRECT_1, SPRECT_2,
XREAL_0, GOBOARD9, JORDAN8, GOBRD13, EUCLID, TOPREAL1, NAT_1, MEMBERED,
ZFMISC_1, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, GOBOARD1, GOBOARD5, GOBRD13, XBOOLE_0;
theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, AXIOMS,
REAL_1, REAL_2, HEINE, TOPREAL4, SPPOL_2, TARSKI, JORDAN3, SQUARE_1,
PSCOMP_1, FINSEQ_5, FINSEQ_6, CQC_THE1, GOBOARD7, TOPREAL1, BINARITH,
AMI_5, JORDAN5B, RLVECT_1, GOBOARD5, SPRECT_2, 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, PARTFUN2, RELSET_1, SCMFSA_7, SPRECT_1, XBOOLE_0, XBOOLE_1,
XREAL_0, XCMPLX_0, XCMPLX_1;
schemes NAT_1, LATTICE5;
begin :: Generalities
reserve i,j,k,n for Nat,
D for non empty set,
f, g for FinSequence of D;
Lm1: for n st 1 <= n holds n-'1+2 = n+1
proof
let n;
assume 1 <= n;
hence n-'1+2 = n+2-'1 by JORDAN4:3
.= n+(1+1) - 1 by JORDAN4:2
.= n+1+1 - 1 by XCMPLX_1:1
.= n+1 by XCMPLX_1:26;
end;
canceled 2;
theorem Th3:
for T being non empty TopSpace
for B,C1,C2,D being Subset of T st B is connected & C1 is_a_component_of D &
C2 is_a_component_of D & B meets C1 & B meets C2 & B c= D
holds C1 = C2
proof
let T be non empty TopSpace;
let B,C1,C2,D be Subset of T;
assume that
A1: B is connected and
A2: C1 is_a_component_of D and
A3: C2 is_a_component_of D and
A4: B meets C1 and
A5: B meets C2 and
A6: B c= D;
A7: B c= C1 by A1,A2,A4,A6,GOBOARD9:6;
A8: B c= C2 by A1,A3,A5,A6,GOBOARD9:6;
B <> {} by A4,XBOOLE_1:65;
then C1 meets C2 by A7,A8,XBOOLE_1:68;
hence C1 = C2 by A2,A3,GOBOARD9:3;
end;
theorem Th4:
(for n holds f|n = g|n) implies f = g
proof
assume
A1: for n holds f|n = g|n;
A2: now assume
A3: len f <> len g;
per cases by A3,REAL_1:def 5;
suppose
A4: len f < len g;
then f|len g = f & g|len g = g by TOPREAL1:2;
hence contradiction by A1,A4;
suppose
A5: len g < len f;
then f|len f = f & g|len f = g by TOPREAL1:2;
hence contradiction by A1,A5;
end;
f|len f = f & g|len g = g by TOPREAL1:2;
hence thesis by A1,A2;
end;
theorem Th5:
n in dom f implies
ex k st k in dom Rev f & n+k = len f+1 & f/.n = (Rev f)/.k
proof
assume
A1: n in dom f;
then A2: 1 <= n & n <= len f by FINSEQ_3:27;
take k = len f+1-'n;
n <= len f+1 by A2,SPPOL_1:5;
then A3: k+n = len f+1 by AMI_5:4;
then A4: k+n-'1 = len f by BINARITH:39;
n+1 <= len f+1 by A2,AXIOMS:24;
then A5: 1 <= k by SPRECT_3:8;
k+1 <= k+n by A2,AXIOMS:24;
then k+1-'1 <= k+n -'1 by JORDAN3:5;
then k <= len f by A4,BINARITH:39;
then k in dom f by A5,FINSEQ_3:27;
hence thesis by A1,A3,FINSEQ_5:60,69;
end;
theorem Th6:
n in dom Rev f implies
ex k st k in dom f & n+k = len f+1 & (Rev f)/.n = f/.k
proof
assume
n in dom Rev f;
then n in dom f by FINSEQ_5:60;
then consider k such that
A1: k in dom Rev f and
A2: n+k = len f+1 and
f/.n = (Rev f)/.k by Th5;
A3: len f = len Rev f & dom f = dom Rev f by FINSEQ_5:60,def 3;
then (Rev f)/.n = f/.k by A1,A2,FINSEQ_5:69;
hence thesis by A1,A2,A3;
end;
begin :: Go-board preliminaries
reserve G for Go-board,
f, g for FinSequence of TOP-REAL 2,
p for Point of TOP-REAL 2,
r, s for Real,
x for set;
theorem Th7:
for D being non empty set
for G being Matrix of D
for f being FinSequence of D holds
f is_sequence_on G iff Rev f is_sequence_on G
proof
let D be non empty set;
let G be Matrix of D;
let f be FinSequence of D;
hereby
assume
A1: f is_sequence_on G;
A2:for n st n in dom Rev f ex i,j st [i,j] in
Indices G & (Rev f)/.n = G*(i,j)
proof
let n;
assume n in dom Rev f;
then consider k such that
A3: k in dom f and
n+k = len f+1 and
A4: (Rev f)/.n = f/.k by Th6;
consider i,j such that
A5: [i,j] in Indices G and
A6: f/.k = G*(i,j) by A1,A3,GOBOARD1:def 11;
take i,j;
thus thesis by A4,A5,A6;
end;
for n st n in dom Rev f & n+1 in dom Rev f holds
for m,k,i,j being Nat st [m,k] in Indices G & [i,j] in Indices G &
(Rev f)/.n = G*(m,k) & (Rev f)/.(n+1) = G*(i,j) holds
abs(m-i)+abs(k-j) = 1
proof
let n such that
A7: n in dom Rev f and
A8: n+1 in dom Rev f;
let m,k,i,j be Nat such that
A9: [m,k] in Indices G and
A10: [i,j] in Indices G and
A11: (Rev f)/.n = G*(m,k) and
A12: (Rev f)/.(n+1) = G*(i,j);
consider l being Nat such that
A13: l in dom f and
A14: n+l = len f+1 and
A15: (Rev f)/.n = f/.l by A7,Th6;
consider l' being Nat such that
A16: l' in dom f and
A17: n+1+l' = len f+1 and
A18: (Rev f)/.(n+1) = f/.l' by A8,Th6;
n+(1+l') = n+l by A14,A17,XCMPLX_1:1;
then A19: l'+1 = l by XCMPLX_1:2;
abs(i-m) = abs(m-i) & abs(j-k) = abs(k-j) by UNIFORM1:13;
hence abs(m-i)+abs(k-j) = 1
by A1,A9,A10,A11,A12,A13,A15,A16,A18,A19,GOBOARD1:def 11;
end;
hence Rev f is_sequence_on G by A2,GOBOARD1:def 11;
end;
assume
A20: Rev f is_sequence_on G;
A21:for n st n in dom f ex i,j st [i,j] in Indices G & f/.n = G*(i,j)
proof
let n;
assume n in dom f;
then consider k such that
A22: k in dom Rev f and
n+k = len f+1 and
A23: f/.n = (Rev f)/.k by Th5;
consider i,j such that
A24: [i,j] in Indices G and
A25: (Rev f)/.k = G*(i,j) by A20,A22,GOBOARD1:def 11;
take i,j;
thus thesis by A23,A24,A25;
end;
for n st n in dom f & n+1 in dom f holds
for m,k,i,j being Nat st [m,k] in Indices G & [i,j] in Indices G &
f/.n = G*(m,k) & f/.(n+1) = G*(i,j) holds
abs(m-i)+abs(k-j) = 1
proof
let n such that
A26: n in dom f and
A27: n+1 in dom f;
let m,k,i,j be Nat such that
A28: [m,k] in Indices G and
A29: [i,j] in Indices G and
A30: f/.n = G*(m,k) and
A31: f/.(n+1) = G*(i,j);
consider l being Nat such that
A32: l in dom Rev f and
A33: n+l = len f+1 and
A34: f/.n = (Rev f)/.l by A26,Th5;
consider l' being Nat such that
A35: l' in dom Rev f and
A36: n+1+l' = len f+1 and
A37: f/.(n+1) = (Rev f)/.l' by A27,Th5;
n+(1+l') = n+l by A33,A36,XCMPLX_1:1;
then A38: l'+1 = l by XCMPLX_1:2;
abs(i-m) = abs(m-i) & abs(j-k) = abs(k-j) by UNIFORM1:13;
hence abs(m-i)+abs(k-j) = 1
by A20,A28,A29,A30,A31,A32,A34,A35,A37,A38,GOBOARD1:def 11;
end;
hence f is_sequence_on G by A21,GOBOARD1:def 11;
end;
theorem Th8:
for G being Matrix of TOP-REAL 2
for f being FinSequence of TOP-REAL 2 holds
f is_sequence_on G & 1 <= k & k <= len f implies f/.k in Values G
proof
let G be Matrix of TOP-REAL 2;
let f be FinSequence of TOP-REAL 2;
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k <= len f;
A4: k in dom f by A2,A3,FINSEQ_3:27;
then f/.k = f.k by FINSEQ_4:def 4;
then A5: f/.k in rng f by A4,FUNCT_1:def 5;
rng f c= Values G by A1,GOBRD13:9;
hence f/.k in Values G by A5;
end;
Lm2:
f is_sequence_on G & 1 <= k & k <= len f implies
ex i,j being Nat st [i,j] in Indices G & f/.k = G*(i,j)
proof
assume that
A1: f is_sequence_on G and
A2: 1 <= k & k <= len f;
k in dom f by A2,FINSEQ_3:27;
then consider i,j such that
A3: [i,j] in Indices G & f/.k = G*(i,j) by A1,GOBOARD1:def 11;
take i,j;
thus thesis by A3;
end;
theorem Th9:
n <= len f & x in L~(f/^n)
implies
ex i being Nat st n+1 <= i & i+1 <= len f & x in LSeg(f,i)
proof
assume that
A1: n <= len f and
A2: x in L~(f/^n);
consider j such that
A3: 1 <= j and
A4: j+1 <= len(f/^n) and
A5: x in LSeg(f/^n,j) by A2,SPPOL_2:13;
A6: j+1 <= len f - n by A1,A4,RFINSEQ:def 2;
take n+j;
j+1 <= len f - n by A1,A4,RFINSEQ:def 2;
then n+(j+1) <= len f by REAL_1:84;
hence thesis by A3,A5,A6,AXIOMS:24,SPPOL_2:5,XCMPLX_1:1;
end;
theorem Th10:
f is_sequence_on G & 1 <= k & k+1 <= len f
implies
f/.k in left_cell(f,k,G) & f/.k in right_cell(f,k,G)
proof
assume that
A1: f is_sequence_on G and
A2: 1 <= k & k+1 <= len f;
set p = f/.k;
LSeg(f,k) = LSeg(f/.k, f/.(k+1)) by A2,TOPREAL1:def 5;
then p in LSeg(f,k) by TOPREAL1:6;
then p in left_cell(f,k,G) /\ right_cell(f,k,G) by A1,A2,GOBRD13:30;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th11:
f is_sequence_on G & 1 <= k & k+1 <= len f
implies
Int left_cell(f,k,G) <> {} & Int right_cell(f,k,G) <> {}
proof
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k+1 <= len f;
consider i1,j1,i2,j2 being Nat such that
A4: [i1,j1] in Indices G and
A5: f/.k = G*(i1,j1) and
A6: [i2,j2] in Indices G and
A7: f/.(k+1) = G*(i2,j2) and
A8: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,A3,JORDAN8:6;
A9: i1+1 > i1 & j1+1 > j1 & i2+1 > i2 & j2+1 > j2 by NAT_1:38;
A10: i1 <= len G & j1 <= width G by A4,GOBOARD5:1;
A11: i2 <= len G & j2 <= width G by A6,GOBOARD5:1;
A12: i1-'1 <= len G & j1-'1 <= width G by A10,JORDAN3:7;
A13: i2-'1 <= len G & j2-'1 <= width G by A11,JORDAN3:7;
per cases by A8;
suppose
A14: i1 = i2 & j1+1 = j2;
then A15: right_cell(f,k,G) = cell(G,i1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1-'1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,A14,GOBRD13:def 3;
hence thesis by A10,A12,A15,GOBOARD9:17;
suppose
A16: i1+1 = i2 & j1 = j2;
then A17: right_cell(f,k,G) = cell(G,i1,j1-'1)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,A16,GOBRD13:def 3;
hence thesis by A10,A12,A17,GOBOARD9:17;
suppose
A18: i1 = i2+1 & j1 = j2;
then A19: right_cell(f,k,G) = cell(G,i2,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i2,j2-'1)
by A1,A2,A3,A4,A5,A6,A7,A9,A18,GOBRD13:def 3;
hence thesis by A11,A13,A19,GOBOARD9:17;
suppose
A20: i1 = i2 & j1 = j2+1;
then A21: right_cell(f,k,G) = cell(G,i1-'1,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,A20,GOBRD13:def 3;
hence thesis by A10,A11,A12,A21,GOBOARD9:17;
end;
theorem Th12:
f is_sequence_on G & 1 <= k & k+1 <= len f
implies
Int left_cell(f,k,G) is connected & Int right_cell(f,k,G) is connected
proof
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k+1 <= len f;
consider i1,j1,i2,j2 being Nat such that
A4: [i1,j1] in Indices G and
A5: f/.k = G*(i1,j1) and
A6: [i2,j2] in Indices G and
A7: f/.(k+1) = G*(i2,j2) and
A8: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,A3,JORDAN8:6;
A9: i1+1 > i1 & j1+1 > j1 & i2+1 > i2 & j2+1 > j2 by NAT_1:38;
A10: i1 <= len G & j1 <= width G by A4,GOBOARD5:1;
A11: i2 <= len G & j2 <= width G by A6,GOBOARD5:1;
A12: i1-'1 <= len G & j1-'1 <= width G by A10,JORDAN3:7;
A13: i2-'1 <= len G & j2-'1 <= width G by A11,JORDAN3:7;
per cases by A8;
suppose
A14: i1 = i2 & j1+1 = j2;
then A15: right_cell(f,k,G) = cell(G,i1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1-'1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,A14,GOBRD13:def 3;
hence thesis by A10,A12,A15,GOBOARD9:21;
suppose
A16: i1+1 = i2 & j1 = j2;
then A17: right_cell(f,k,G) = cell(G,i1,j1-'1)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,A16,GOBRD13:def 3;
hence thesis by A10,A12,A17,GOBOARD9:21;
suppose
A18: i1 = i2+1 & j1 = j2;
then A19: right_cell(f,k,G) = cell(G,i2,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i2,j2-'1)
by A1,A2,A3,A4,A5,A6,A7,A9,A18,GOBRD13:def 3;
hence thesis by A11,A13,A19,GOBOARD9:21;
suppose
A20: i1 = i2 & j1 = j2+1;
then A21: right_cell(f,k,G) = cell(G,i1-'1,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,A20,GOBRD13:def 3;
hence thesis by A10,A11,A12,A21,GOBOARD9:21;
end;
theorem Th13:
f is_sequence_on G & 1 <= k & k+1 <= len f
implies
Cl Int left_cell(f,k,G) = left_cell(f,k,G) &
Cl Int right_cell(f,k,G) = right_cell(f,k,G)
proof
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k+1 <= len f;
consider i1,j1,i2,j2 being Nat such that
A4: [i1,j1] in Indices G and
A5: f/.k = G*(i1,j1) and
A6: [i2,j2] in Indices G and
A7: f/.(k+1) = G*(i2,j2) and
A8: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,A3,JORDAN8:6;
A9: i1+1 > i1 & j1+1 > j1 & i2+1 > i2 & j2+1 > j2 by NAT_1:38;
A10: i1 <= len G & j1 <= width G by A4,GOBOARD5:1;
A11: i2 <= len G & j2 <= width G by A6,GOBOARD5:1;
A12: i1-'1 <= len G & j1-'1 <= width G by A10,JORDAN3:7;
A13: i2-'1 <= len G & j2-'1 <= width G by A11,JORDAN3:7;
per cases by A8;
suppose
A14: i1 = i2 & j1+1 = j2;
then A15: right_cell(f,k,G) = cell(G,i1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1-'1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,A14,GOBRD13:def 3;
hence thesis by A10,A12,A15,GOBRD11:35;
suppose
A16: i1+1 = i2 & j1 = j2;
then A17: right_cell(f,k,G) = cell(G,i1,j1-'1)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,A16,GOBRD13:def 3;
hence thesis by A10,A12,A17,GOBRD11:35;
suppose
A18: i1 = i2+1 & j1 = j2;
then A19: right_cell(f,k,G) = cell(G,i2,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i2,j2-'1)
by A1,A2,A3,A4,A5,A6,A7,A9,A18,GOBRD13:def 3;
hence thesis by A11,A13,A19,GOBRD11:35;
suppose
A20: i1 = i2 & j1 = j2+1;
then A21: right_cell(f,k,G) = cell(G,i1-'1,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,A20,GOBRD13:def 3;
hence thesis by A10,A11,A12,A21,GOBRD11:35;
end;
theorem Th14:
f is_sequence_on G & LSeg(f,k) is horizontal
implies
ex j st 1 <= j & j <= width G & for p st p in
LSeg(f,k) holds p`2 = G*(1,j)`2
proof
assume that
A1: f is_sequence_on G and
A2: LSeg(f,k) is horizontal;
per cases;
suppose
A3: 1 <= k & k+1 <= len f;
k <= k+1 by NAT_1:29;
then k <= len f by A3,AXIOMS:22;
then consider i,j such that
A4: [i,j] in Indices G and
A5: f/.k = G*(i,j) by A1,A3,Lm2;
take j;
thus
A6: 1 <= j & j <= width G by A4,GOBOARD5:1;
let p;
A7: 1 <= i & i <= len G by A4,GOBOARD5:1;
A8: f/.k in LSeg(f,k) by A3,TOPREAL1:27;
assume p in LSeg(f,k);
hence p`2 = (f/.k)`2 by A2,A8,SPPOL_1:def 2
.= G*(1,j)`2 by A5,A6,A7,GOBOARD5:2;
suppose
A9: not(1 <= k & k+1 <= len f);
take 1;
width G <> 0 by GOBOARD1:def 5;
hence 1 <= 1 & 1 <= width G by RLVECT_1:99;
thus thesis by A9,TOPREAL1:def 5;
end;
theorem Th15:
f is_sequence_on G & LSeg(f,k) is vertical
implies
ex i st 1 <= i & i <= len G & for p st p in LSeg(f,k) holds p`1 = G*(i,1)`1
proof
assume that
A1: f is_sequence_on G and
A2: LSeg(f,k) is vertical;
per cases;
suppose
A3: 1 <= k & k+1 <= len f;
k <= k+1 by NAT_1:29;
then k <= len f by A3,AXIOMS:22;
then consider i,j such that
A4: [i,j] in Indices G and
A5: f/.k = G*(i,j) by A1,A3,Lm2;
take i;
thus
A6: 1 <= i & i <= len G by A4,GOBOARD5:1;
let p;
A7: 1 <= j & j <= width G by A4,GOBOARD5:1;
A8: f/.k in LSeg(f,k) by A3,TOPREAL1:27;
assume p in LSeg(f,k);
hence p`1 = (f/.k)`1 by A2,A8,SPPOL_1:def 3
.= G*(i,1)`1 by A5,A6,A7,GOBOARD5:3;
suppose
A9: not(1 <= k & k+1 <= len f);
take 1;
0 <> len G by GOBOARD1:def 5;
hence 1 <= 1 & 1 <= len G by RLVECT_1:99;
thus thesis by A9,TOPREAL1:def 5;
end;
theorem Th16:
f is_sequence_on G & f is special & i <= len G & j <= width G
implies
Int cell(G,i,j) misses L~f
proof
assume that
A1: f is_sequence_on G and
A2: f is special and
A3: i <= len G and
A4: j <= width G;
assume Int cell(G,i,j) meets L~f;
then consider x being set such that
A5: x in Int cell(G,i,j) and
A6: x in L~f by XBOOLE_0:3;
L~f = union { LSeg(f,k) : 1 <= k & k+1 <= len f } by TOPREAL1:def 6;
then consider X being set such that
A7: x in X and
A8: X in { LSeg(f,k) : 1 <= k & k+1 <= len f } by A6,TARSKI:def 4;
consider k such that
A9: X = LSeg(f,k) and
1 <= k & k+1 <= len f by A8;
reconsider p = x as Point of TOP-REAL 2 by A7,A9;
A10: Int cell(G,i,j)
= Int(v_strip(G,i) /\ h_strip(G,j)) by GOBOARD5:def 3
.= Int v_strip(G,i) /\ Int h_strip(G,j) by TOPS_1:46;
per cases by A2,SPPOL_1:41;
suppose LSeg(f,k) is horizontal;
then consider j0 being Nat such that
A11: 1 <= j0 & j0 <= width G and
A12: for p being Point of TOP-REAL 2
st p in LSeg(f,k) holds p`2 = G*(1,j0)`2 by A1,Th14;
now assume
A13: p in Int h_strip(G,j);
A14: j0 > j implies j0 >= j+1 by NAT_1:38;
per cases by A14,REAL_1:def 5;
suppose
A15: j0 < j;
then j >= 1 by A11,AXIOMS:22;
then A16: p`2 > G*(1,j)`2 by A4,A13,GOBOARD6:30;
0 <> len G by GOBOARD1:def 5;
then 1 <= len G by RLVECT_1:99;
then G*(1,j)`2 > G*(1,j0)`2 by A4,A11,A15,GOBOARD5:5;
hence contradiction by A7,A9,A12,A16;
suppose j0 = j;
then p`2 > G*(1,j0)`2 by A11,A13,GOBOARD6:30;
hence contradiction by A7,A9,A12;
suppose
A17: j0 > j+1;
then j+1 <= width G by A11,AXIOMS:22;
then j < width G by NAT_1:38;
then A18: p`2 < G*(1,j+1)`2 by A13,GOBOARD6:31;
0 <> len G by GOBOARD1:def 5;
then 1 <= len G & j+1 >= 1 by RLVECT_1:99;
then G*(1,j+1)`2 < G*(1,j0)`2 by A11,A17,GOBOARD5:5;
hence contradiction by A7,A9,A12,A18;
suppose
A19: j0 = j+1;
then j < width G by A11,NAT_1:38;
then p`2 < G*(1,j0)`2 by A13,A19,GOBOARD6:31;
hence contradiction by A7,A9,A12;
end;
hence contradiction by A5,A10,XBOOLE_0:def 3;
suppose LSeg(f,k) is vertical;
then consider i0 being Nat such that
A20: 1 <= i0 & i0 <= len G and
A21: for p being Point of TOP-REAL 2
st p in LSeg(f,k) holds p`1 = G*(i0,1)`1 by A1,Th15;
now assume
A22: p in Int v_strip(G,i);
A23: i0 > i implies i0 >= i+1 by NAT_1:38;
per cases by A23,REAL_1:def 5;
suppose
A24: i0 < i;
then i >= 1 by A20,AXIOMS:22;
then A25: p`1 > G*(i,1)`1 by A3,A22,GOBOARD6:32;
0 <> width G by GOBOARD1:def 5;
then 1 <= width G by RLVECT_1:99;
then G*(i,1)`1 > G*(i0,1)`1 by A3,A20,A24,GOBOARD5:4;
hence contradiction by A7,A9,A21,A25;
suppose i0 = i;
then p`1 > G*(i0,1)`1 by A20,A22,GOBOARD6:32;
hence contradiction by A7,A9,A21;
suppose
A26: i0 > i+1;
then i+1 <= len G by A20,AXIOMS:22;
then i < len G by NAT_1:38;
then A27: p`1 < G*(i+1,1)`1 by A22,GOBOARD6:33;
0 <> width G by GOBOARD1:def 5;
then 1 <= width G & i+1 >= 1 by RLVECT_1:99;
then G*(i+1,1)`1 < G*(i0,1)`1 by A20,A26,GOBOARD5:4;
hence contradiction by A7,A9,A21,A27;
suppose
A28: i0 = i+1;
then i < len G by A20,NAT_1:38;
then p`1 < G*(i0,1)`1 by A22,A28,GOBOARD6:33;
hence contradiction by A7,A9,A21;
end;
hence contradiction by A5,A10,XBOOLE_0:def 3;
end;
theorem Th17:
f is_sequence_on G & f is special & 1 <= k & k+1 <= len f
implies
Int left_cell(f,k,G) misses L~f & Int right_cell(f,k,G) misses L~f
proof
assume that
A1: f is_sequence_on G & f is special and
A2: 1 <= k and
A3: k+1 <= len f;
consider i1,j1,i2,j2 being Nat such that
A4: [i1,j1] in Indices G and
A5: f/.k = G*(i1,j1) and
A6: [i2,j2] in Indices G and
A7: f/.(k+1) = G*(i2,j2) and
A8: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,A3,JORDAN8:6;
A9: i1+1 > i1 & j1+1 > j1 & i2+1 > i2 & j2+1 > j2 by NAT_1:38;
A10: i1 <= len G & j1 <= width G by A4,GOBOARD5:1;
A11: i2 <= len G & j2 <= width G by A6,GOBOARD5:1;
A12: i1-'1 <= len G & j1-'1 <= width G by A10,JORDAN3:7;
A13: i2-'1 <= len G & j2-'1 <= width G by A11,JORDAN3:7;
per cases by A8;
suppose
A14: i1 = i2 & j1+1 = j2;
then A15: right_cell(f,k,G) = cell(G,i1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1-'1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,A14,GOBRD13:def 3;
hence thesis by A1,A10,A12,A15,Th16;
suppose
A16: i1+1 = i2 & j1 = j2;
then A17: right_cell(f,k,G) = cell(G,i1,j1-'1)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1,j1)
by A1,A2,A3,A4,A5,A6,A7,A9,A16,GOBRD13:def 3;
hence thesis by A1,A10,A12,A17,Th16;
suppose
A18: i1 = i2+1 & j1 = j2;
then A19: right_cell(f,k,G) = cell(G,i2,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i2,j2-'1)
by A1,A2,A3,A4,A5,A6,A7,A9,A18,GOBRD13:def 3;
hence thesis by A1,A11,A13,A19,Th16;
suppose
A20: i1 = i2 & j1 = j2+1;
then A21: right_cell(f,k,G) = cell(G,i1-'1,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,GOBRD13:def 2;
left_cell(f,k,G) = cell(G,i1,j2)
by A1,A2,A3,A4,A5,A6,A7,A9,A20,GOBRD13:def 3;
hence thesis by A1,A10,A11,A12,A21,Th16;
end;
theorem Th18:
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G
implies
G*(i,j)`1 = G*(i,j+1)`1 & G*(i,j)`2 = G*(i+1,j)`2 &
G*(i+1,j+1)`1 = G*(i+1,j)`1 & G*(i+1,j+1)`2 = G*(i,j+1)`2
proof
assume that
A1: 1 <= i and
A2: i+1 <= len G and
A3: 1 <= j and
A4: j+1 <= width G;
A5: i < len G by A2,NAT_1:38;
A6: j < width G by A4,NAT_1:38;
A7: 1 <= i+1 by NAT_1:29;
A8: 1 <= j+1 by NAT_1:29;
thus G*(i,j)`1 = G*(i,1)`1 by A1,A3,A5,A6,GOBOARD5:3
.= G*(i,j+1)`1 by A1,A4,A5,A8,GOBOARD5:3;
thus G*(i,j)`2 = G*(1,j)`2 by A1,A3,A5,A6,GOBOARD5:2
.= G*(i+1,j)`2 by A2,A3,A6,A7,GOBOARD5:2;
thus G*(i+1,j+1)`1 = G*(i+1,1)`1 by A2,A4,A7,A8,GOBOARD5:3
.= G*(i+1,j)`1 by A2,A3,A6,A7,GOBOARD5:3;
thus G*(i+1,j+1)`2 = G*(1,j+1)`2 by A2,A4,A7,A8,GOBOARD5:2
.= G*(i,j+1)`2 by A1,A4,A5,A8,GOBOARD5:2;
end;
theorem Th19:
for i,j being Nat st 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G
holds
p in cell(G,i,j) iff
G*(i,j)`1 <= p`1 & p`1 <= G*(i+1,j)`1 & G*(i,j)`2 <= p`2 & p`2 <=
G*(i,j+1)`2
proof
let i,j be Nat such that
A1: 1 <= i & i+1 <= len G and
A2: 1 <= j & j+1 <= width G;
A3: i < len G by A1,NAT_1:38;
A4: j < width G by A2,NAT_1:38;
then A5: v_strip(G,i) = { |[r,s]| : G*(i,j)`1 <= r & r <= G*(i+1,j)`1 } by A1,
A2,A3,GOBOARD5:9;
A6: h_strip(G,j) = { |[r,s]| : G*(i,j)`2 <= s & s <= G*(i,j+1)`2 } by A1,A2,A3,
A4,GOBOARD5:6;
hereby
assume p in cell(G,i,j);
then p in v_strip(G,i) /\ h_strip(G,j) by GOBOARD5:def 3;
then A7: p in v_strip(G,i) & p in h_strip(G,j) by XBOOLE_0:def 3;
then ex r,s st |[r,s]| = p & G*(i,j)`1 <= r & r <= G*(i+1,j)`1 by A5;
hence G*(i,j)`1 <= p`1 & p`1 <= G*(i+1,j)`1 by EUCLID:56;
ex r,s st |[r,s]| = p & G*(i,j)`2 <= s & s <= G*(i,j+1)`2 by A6,A7;
hence G*(i,j)`2 <= p`2 & p`2 <= G*(i,j+1)`2 by EUCLID:56;
end;
assume that
A8: G*(i,j)`1 <= p`1 & p`1 <= G*(i+1,j)`1 and
A9: G*(i,j)`2 <= p`2 & p`2 <= G*(i,j+1)`2;
A10: p = |[p`1,p`2]| by EUCLID:57;
then A11: p in v_strip(G,i) by A5,A8;
p in h_strip(G,j) by A6,A9,A10;
then p in v_strip(G,i) /\ h_strip(G,j) by A11,XBOOLE_0:def 3;
hence thesis by GOBOARD5:def 3;
end;
theorem
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G
implies
cell(G,i,j) = { |[r,s]| : G*(i,j)`1 <= r & r <= G*(i+1,j)`1 &
G*(i,j)`2 <= s & s <= G*(i,j+1)`2 }
proof
assume that
A1: 1 <= i & i+1 <= len G and
A2: 1 <= j & j+1 <= width G;
set A = { |[r,s]| : G*(i,j)`1 <= r & r <= G*(i+1,j)`1 &
G*(i,j)`2 <= s & s <= G*(i,j+1)`2 };
now
let p be set;
assume
A3: p in cell(G,i,j);
then reconsider q=p as Point of TOP-REAL 2;
A4: p = |[q`1,q`2]| by EUCLID:57;
G*(i,j)`1 <= q`1 & q`1 <= G*(i+1,j)`1 & G*(i,j)`2 <= q`2 & q`2 <=
G*(i,j+1)`2
by A1,A2,A3,Th19;
hence p in A by A4;
end;
hence cell(G,i,j) c= A by TARSKI:def 3;
now
let p be set;
assume p in A;
then consider r,s such that
A5: |[r,s]| = p and
A6: G*(i,j)`1 <= r & r <= G*(i+1,j)`1 and
A7: G*(i,j)`2 <= s & s <= G*(i,j+1)`2;
reconsider q=p as Point of TOP-REAL 2 by A5;
r = q`1 & s = q`2 by A5,EUCLID:56;
hence p in cell(G,i,j) by A1,A2,A6,A7,Th19;
end;
hence A c= cell(G,i,j) by TARSKI:def 3;
end;
theorem Th21:
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G &
p in Values G & p in cell(G,i,j)
implies
p = G*(i,j) or p = G*(i,j+1) or p = G*(i+1,j+1) or p = G*(i+1,j)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len G and
A3: 1 <= j and
A4: j+1 <= width G and
A5: p in Values G and
A6: p in cell(G,i,j);
A7: Values G = { G*(k,l) where k,l is Nat: [k,l] in Indices G } by GOBRD13:7;
A8: i < len G by A2,NAT_1:38;
A9: j < width G by A4,NAT_1:38;
A10: 1 <= i+1 by NAT_1:29;
A11: 1 <= j+1 by NAT_1:29;
consider k,l being Nat such that
A12: p = G*(k,l) and
A13: [k,l] in Indices G by A5,A7;
A14: 1 <= k & k <= len G & 1 <= l & l <= width G by A13,GOBOARD5:1;
A15: now
assume
A16: k <> i & k <> i+1;
per cases by A16,NAT_1:27;
suppose
k < i;
then G*(k,l)`1 < G*(i,l)`1 by A8,A14,GOBOARD5:4;
then G*(k,l)`1 < G*(i,1)`1 by A1,A8,A14,GOBOARD5:3;
then G*(k,l)`1 < G*(i,j)`1 by A1,A3,A8,A9,GOBOARD5:3;
hence contradiction by A1,A2,A3,A4,A6,A12,Th19;
suppose
i+1 < k;
then G*(i+1,l)`1 < G*(k,l)`1 by A10,A14,GOBOARD5:4;
then G*(i+1,1)`1 < G*(k,l)`1 by A2,A10,A14,GOBOARD5:3;
then G*(i+1,j)`1 < G*(k,l)`1 by A2,A3,A9,A10,GOBOARD5:3;
hence contradiction by A1,A2,A3,A4,A6,A12,Th19;
end;
now
assume
A17: l <> j & l <> j+1;
per cases by A17,NAT_1:27;
suppose
l < j;
then G*(k,l)`2 < G*(k,j)`2 by A9,A14,GOBOARD5:5;
then G*(k,l)`2 < G*(1,j)`2 by A3,A9,A14,GOBOARD5:2;
then G*(k,l)`2 < G*(i,j)`2 by A1,A3,A8,A9,GOBOARD5:2;
hence contradiction by A1,A2,A3,A4,A6,A12,Th19;
suppose
j+1 < l;
then G*(k,j+1)`2 < G*(k,l)`2 by A11,A14,GOBOARD5:5;
then G*(1,j+1)`2 < G*(k,l)`2 by A4,A11,A14,GOBOARD5:2;
then G*(i,j+1)`2 < G*(k,l)`2 by A1,A4,A8,A11,GOBOARD5:2;
hence contradiction by A1,A2,A3,A4,A6,A12,Th19;
end;
hence thesis by A12,A15;
end;
theorem Th22:
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G
implies
G*(i,j) in cell(G,i,j) & G*(i,j+1) in cell(G,i,j) &
G*(i+1,j+1) in cell(G,i,j) & G*(i+1,j) in cell(G,i,j)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len G and
A3: 1 <= j and
A4: j+1 <= width G;
A5: i < i+1 & j < j+1 by NAT_1:38;
A6: i < len G by A2,NAT_1:38;
A7: j < width G by A4,NAT_1:38;
then A8: G*(i,j)`1 <= G*(i+1,j)`1 by A1,A2,A3,A5,GOBOARD5:4;
G*(i,j)`2 <= G*(i,j+1)`2 by A1,A3,A4,A5,A6,GOBOARD5:5;
hence G*(i,j) in cell(G,i,j) by A1,A2,A3,A4,A8,Th19;
A9: G*(i,j)`1 = G*(i,j+1)`1 by A1,A2,A3,A4,Th18;
then A10: G*(i,j+1)`1 <= G*(i+1,j)`1 by A1,A2,A3,A5,A7,GOBOARD5:4;
G*(i,j)`2 <= G*(i,j+1)`2 by A1,A3,A4,A5,A6,GOBOARD5:5;
hence G*(i,j+1) in cell(G,i,j) by A1,A2,A3,A4,A9,A10,Th19;
A11: G*(i+1,j+1)`1 = G*(i+1,j)`1 by A1,A2,A3,A4,Th18;
then A12: G*(i,j)`1 <= G*(i+1,j+1)`1 by A1,A2,A3,A5,A7,GOBOARD5:4;
A13: G*(i+1,j+1)`2 = G*(i,j+1)`2 by A1,A2,A3,A4,Th18;
then G*(i,j)`2 <= G*(i+1,j+1)`2 by A1,A3,A4,A5,A6,GOBOARD5:5;
hence G*(i+1,j+1) in cell(G,i,j) by A1,A2,A3,A4,A11,A12,A13,Th19;
A14: G*(i,j)`1 <= G*(i+1,j)`1 by A1,A2,A3,A5,A7,GOBOARD5:4;
A15: G*(i,j)`2 = G*(i+1,j)`2 by A1,A2,A3,A4,Th18;
then G*(i+1,j)`2 <= G*(i,j+1)`2 by A1,A3,A4,A5,A6,GOBOARD5:5;
hence G*(i+1,j) in cell(G,i,j) by A1,A2,A3,A4,A14,A15,Th19;
end;
theorem Th23:
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G &
p in Values G & p in cell(G,i,j)
implies
p is_extremal_in cell(G,i,j)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len G and
A3: 1 <= j and
A4: j+1 <= width G and
A5: p in Values G and
A6: p in cell(G,i,j);
for a,b being Point of TOP-REAL 2 st p in
LSeg(a,b) & LSeg(a,b) c= cell(G,i,j)
holds p = a or p = b
proof
let a,b be Point of TOP-REAL 2 such that
A7: p in LSeg(a,b) and
A8: LSeg(a,b) c= cell(G,i,j);
assume
A9: a <> p & b <> p;
A10: a in LSeg(a,b) & b in LSeg(a,b) by TOPREAL1:6;
per cases by A1,A2,A3,A4,A5,A6,Th21;
suppose
A11: p = G*(i,j);
then A12: p`1 <= a`1 & p`2 <= a`2 by A1,A2,A3,A4,A8,A10,Th19;
A13: p`1 <= b`1 & p`2 <= b`2 by A1,A2,A3,A4,A8,A10,A11,Th19;
now
per cases;
suppose
a`1 <= b`1 & a`2 <= b`2;
then a`1 <= p`1 & a`2 <= p`2 by A7,TOPREAL1:9,10;
then a`1 = p`1 & a`2 = p`2 by A12,REAL_1:def 5;
hence contradiction by A9,TOPREAL3:11;
suppose
a`1 <= b`1 & b`2 < a`2;
then a`1 <= p`1 & b`2 <= p`2 by A7,TOPREAL1:9,10;
then A14: a`1 = p`1 & b`2 = p`2 by A12,A13,REAL_1:def 5;
then a`2 <> p`2 by A9,TOPREAL3:11;
then LSeg(a,b) is vertical by A7,A10,A14,SPPOL_1:39;
then a`1 = b`1 by SPPOL_1:37;
hence contradiction by A9,A14,TOPREAL3:11;
suppose
b`1 < a`1 & a`2 <= b`2;
then b`1 <= p`1 & a`2 <= p`2 by A7,TOPREAL1:9,10;
then A15: b`1 = p`1 & a`2 = p`2 by A12,A13,REAL_1:def 5;
then b`2 <> p`2 by A9,TOPREAL3:11;
then LSeg(a,b) is vertical by A7,A10,A15,SPPOL_1:39;
then a`1 = b`1 by SPPOL_1:37;
hence contradiction by A9,A15,TOPREAL3:11;
suppose
b`1 < a`1 & b`2 < a`2;
then b`1 <= p`1 & b`2 <= p`2 by A7,TOPREAL1:9,10;
then b`1 = p`1 & b`2 = p`2 by A13,REAL_1:def 5;
hence contradiction by A9,TOPREAL3:11;
end;
hence contradiction;
suppose
A16: p = G*(i,j+1);
then A17: p`1 = G*(i,j)`1 by A1,A2,A3,A4,Th18;
then A18: p`1 <= a`1 & a`2 <= p`2 by A1,A2,A3,A4,A8,A10,A16,Th19;
A19: p`1 <= b`1 & b`2 <= p`2 by A1,A2,A3,A4,A8,A10,A16,A17,Th19;
now
per cases;
suppose
a`1 <= b`1 & a`2 <= b`2;
then a`1 <= p`1 & p`2 <= b`2 by A7,TOPREAL1:9,10;
then A20: a`1 = p`1 & b`2 = p`2 by A18,A19,REAL_1:def 5;
then a`2 <> p`2 by A9,TOPREAL3:11;
then LSeg(a,b) is vertical by A7,A10,A20,SPPOL_1:39;
then a`1 = b`1 by SPPOL_1:37;
hence contradiction by A9,A20,TOPREAL3:11;
suppose
a`1 <= b`1 & b`2 < a`2;
then a`1 <= p`1 & p`2 <= a`2 by A7,TOPREAL1:9,10;
then a`1 = p`1 & a`2 = p`2 by A18,REAL_1:def 5;
hence contradiction by A9,TOPREAL3:11;
suppose
b`1 < a`1 & a`2 <= b`2;
then b`1 <= p`1 & p`2 <= b`2 by A7,TOPREAL1:9,10;
then b`1 = p`1 & b`2 = p`2 by A19,REAL_1:def 5;
hence contradiction by A9,TOPREAL3:11;
suppose
b`1 < a`1 & b`2 < a`2;
then b`1 <= p`1 & p`2 <= a`2 by A7,TOPREAL1:9,10;
then A21: b`1 = p`1 & a`2 = p`2 by A18,A19,REAL_1:def 5;
then b`2 <> p`2 by A9,TOPREAL3:11;
then LSeg(a,b) is vertical by A7,A10,A21,SPPOL_1:39;
then a`1 = b`1 by SPPOL_1:37;
hence contradiction by A9,A21,TOPREAL3:11;
end;
hence contradiction;
suppose
p = G*(i+1,j+1);
then A22: p`1 = G*(i+1,j)`1 & p`2 = G*(i,j+1)`2 by A1,A2,A3,A4,Th18;
then A23: a`1 <= p`1 & a`2 <= p`2 by A1,A2,A3,A4,A8,A10,Th19;
A24: b`1 <= p`1 & b`2 <= p`2 by A1,A2,A3,A4,A8,A10,A22,Th19;
now
per cases;
suppose
a`1 <= b`1 & a`2 <= b`2;
then p`1 <= b`1 & p`2 <= b`2 by A7,TOPREAL1:9,10;
then b`1 = p`1 & b`2 = p`2 by A24,REAL_1:def 5;
hence contradiction by A9,TOPREAL3:11;
suppose
a`1 <= b`1 & b`2 < a`2;
then p`1 <= b`1 & p`2 <= a`2 by A7,TOPREAL1:9,10;
then A25: b`1 = p`1 & a`2 = p`2 by A23,A24,REAL_1:def 5;
then b`2 <> p`2 by A9,TOPREAL3:11;
then LSeg(a,b) is vertical by A7,A10,A25,SPPOL_1:39;
then a`1 = b`1 by SPPOL_1:37;
hence contradiction by A9,A25,TOPREAL3:11;
suppose
b`1 < a`1 & a`2 <= b`2;
then p`1 <= a`1 & p`2 <= b`2 by A7,TOPREAL1:9,10;
then A26: a`1 = p`1 & b`2 = p`2 by A23,A24,REAL_1:def 5;
then a`2 <> p`2 by A9,TOPREAL3:11;
then LSeg(a,b) is vertical by A7,A10,A26,SPPOL_1:39;
then a`1 = b`1 by SPPOL_1:37;
hence contradiction by A9,A26,TOPREAL3:11;
suppose
b`1 < a`1 & b`2 < a`2;
then p`1 <= a`1 & p`2 <= a`2 by A7,TOPREAL1:9,10;
then a`1 = p`1 & a`2 = p`2 by A23,REAL_1:def 5;
hence contradiction by A9,TOPREAL3:11;
end;
hence contradiction;
suppose
A27: p = G*(i+1,j);
then A28: p`2 = G*(i,j)`2 by A1,A2,A3,A4,Th18;
then A29: a`1 <= p`1 & p`2 <= a`2 by A1,A2,A3,A4,A8,A10,A27,Th19;
A30: b`1 <= p`1 & p`2 <= b`2 by A1,A2,A3,A4,A8,A10,A27,A28,Th19;
now
per cases;
suppose
a`1 <= b`1 & a`2 <= b`2;
then p`1 <= b`1 & a`2 <= p`2 by A7,TOPREAL1:9,10;
then A31: b`1 = p`1 & a`2 = p`2 by A29,A30,REAL_1:def 5;
then b`2 <> p`2 by A9,TOPREAL3:11;
then LSeg(a,b) is vertical by A7,A10,A31,SPPOL_1:39;
then a`1 = b`1 by SPPOL_1:37;
hence contradiction by A9,A31,TOPREAL3:11;
suppose
a`1 <= b`1 & b`2 < a`2;
then p`1 <= b`1 & b`2 <= p`2 by A7,TOPREAL1:9,10;
then b`1 = p`1 & b`2 = p`2 by A30,REAL_1:def 5;
hence contradiction by A9,TOPREAL3:11;
suppose
b`1 < a`1 & a`2 <= b`2;
then p`1 <= a`1 & a`2 <= p`2 by A7,TOPREAL1:9,10;
then a`1 = p`1 & a`2 = p`2 by A29,REAL_1:def 5;
hence contradiction by A9,TOPREAL3:11;
suppose
b`1 < a`1 & b`2 < a`2;
then p`1 <= a`1 & b`2 <= p`2 by A7,TOPREAL1:9,10;
then A32: a`1 = p`1 & b`2 = p`2 by A29,A30,REAL_1:def 5;
then a`2 <> p`2 by A9,TOPREAL3:11;
then LSeg(a,b) is vertical by A7,A10,A32,SPPOL_1:39;
then a`1 = b`1 by SPPOL_1:37;
hence contradiction by A9,A32,TOPREAL3:11;
end;
hence contradiction;
end;
hence thesis by A6,SPPOL_1:def 1;
end;
theorem Th24:
2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k+1 <= len f
implies
ex i,j st 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G &
LSeg(f,k) c= cell(G,i,j)
proof
assume that
A1: 2 <= len G and
A2: 2 <= width G and
A3: f is_sequence_on G and
A4: 1 <= k and
A5: k+1 <= len f;
A6: LSeg(f,k) = LSeg(f/.k, f/.(k+1)) by A4,A5,TOPREAL1:def 5;
consider i1,j1,i2,j2 being Nat such that
A7: [i1,j1] in Indices G and
A8: f/.k = G*(i1,j1) and
A9: [i2,j2] in Indices G and
A10: f/.(k+1) = G*(i2,j2) and
A11: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or
i1 = i2 & j1 = j2+1 by A3,A4,A5,JORDAN8:6;
A12: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A7,GOBOARD5:1;
A13: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A9,GOBOARD5:1;
per cases by A11;
suppose
A14: i1 = i2 & j1+1 = j2;
then A15: j1 < width G by A13,SPPOL_1:5;
now
per cases by A12,REAL_1:def 5;
suppose
i1 < len G;
then A16: i1+1 <= len G by NAT_1:38;
take i1,j1;
LSeg(f,k) c= cell(G,i1,j1) by A6,A8,A10,A12,A14,A15,GOBOARD5:20;
hence thesis by A12,A13,A14,A16;
suppose
A17: i1 = len G;
take i1'=i1-'1,j1;
2-1 <= 2-'1 & 2-'1 <= i1' by A1,A17,JORDAN3:3,5;
then A18: 1 <= i1' by AXIOMS:22;
A19: i1'+1 = i1 by A12,AMI_5:4;
then i1' < len G by A12,NAT_1:38;
then LSeg(f,k) c= cell(G,i1',j1) by A6,A8,A10,A12,A14,A15,A19,GOBOARD5:
19;
hence thesis by A12,A13,A14,A18,A19;
end;
hence thesis;
suppose
A20: i1+1 = i2 & j1 = j2;
then A21: i1 < len G by A13,SPPOL_1:5;
now
per cases by A12,REAL_1:def 5;
suppose
j1 < width G;
then A22: j1+1 <= width G by NAT_1:38;
take i1,j1;
LSeg(f,k) c= cell(G,i1,j1) by A6,A8,A10,A12,A20,A21,GOBOARD5:23;
hence thesis by A12,A13,A20,A22;
suppose
A23: j1 = width G;
take i1,j1'=j1-'1;
2-1 <= 2-'1 & 2-'1 <= j1' by A2,A23,JORDAN3:3,5;
then A24: 1 <= j1' by AXIOMS:22;
A25: j1'+1=j1 by A12,AMI_5:4;
then j1' < width G by A23,NAT_1:38;
then LSeg(f,k) c= cell(G,i1,j1') by A6,A8,A10,A12,A20,A21,A25,GOBOARD5:
22;
hence thesis by A12,A13,A20,A24,A25;
end;
hence thesis;
suppose
A26: i1 = i2+1 & j1 = j2;
then A27: i2 < len G by A12,SPPOL_1:5;
now
per cases by A12,REAL_1:def 5;
suppose
j1 < width G;
then A28: j1+1 <= width G by NAT_1:38;
take i2,j1;
LSeg(f,k) c= cell(G,i2,j1) by A6,A8,A10,A13,A26,A27,GOBOARD5:23;
hence thesis by A12,A13,A26,A28;
suppose
A29: j1 = width G;
take i2,j1'=j1-'1;
2-1 <= 2-'1 & 2-'1 <= j1' by A2,A29,JORDAN3:3,5;
then A30: 1 <= j1' by AXIOMS:22;
A31: j1'+1=j1 by A12,AMI_5:4;
then j1' < width G by A29,NAT_1:38;
then LSeg(f,k) c= cell(G,i2,j1') by A6,A8,A10,A13,A26,A27,A31,GOBOARD5:
22;
hence thesis by A12,A13,A26,A30,A31;
end;
hence thesis;
suppose
A32: i1 = i2 & j1 = j2+1;
then A33: j2 < width G by A12,SPPOL_1:5;
now
per cases by A12,REAL_1:def 5;
suppose
i1 < len G;
then A34: i1+1 <= len G by NAT_1:38;
take i1,j2;
LSeg(f,k) c= cell(G,i1,j2) by A6,A8,A10,A13,A32,A33,GOBOARD5:20;
hence thesis by A12,A13,A32,A34;
suppose
A35: i1 = len G;
take i1'=i1-'1,j2;
2-1 <= 2-'1 & 2-'1 <= i1' by A1,A35,JORDAN3:3,5;
then A36: 1 <= i1' by AXIOMS:22;
A37: i1'+1 = i1 by A12,AMI_5:4;
then i1' < len G by A12,NAT_1:38;
then LSeg(f,k) c= cell(G,i1',j2) by A6,A8,A10,A13,A32,A33,A37,GOBOARD5:
19;
hence thesis by A12,A13,A32,A36,A37;
end;
hence thesis;
end;
theorem Th25:
2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k+1 <= len f &
p in Values G & p in LSeg(f,k)
implies
p = f/.k or p = f/.(k+1)
proof
assume that
A1: 2 <= len G and
A2: 2 <= width G and
A3: f is_sequence_on G and
A4: 1 <= k and
A5: k+1 <= len f and
A6: p in Values G and
A7: p in LSeg(f,k);
consider i,j such that
A8: 1 <= i & i+1 <= len G and
A9: 1 <= j & j+1 <= width G and
A10: LSeg(f,k) c= cell(G,i,j) by A1,A2,A3,A4,A5,Th24;
A11: LSeg(f,k) = LSeg(f/.k, f/.(k+1)) by A4,A5,TOPREAL1:def 5;
p is_extremal_in cell(G,i,j) by A6,A7,A8,A9,A10,Th23;
hence thesis by A7,A10,A11,SPPOL_1:def 1;
end;
theorem
[i,j] in Indices G & 1 <= k & k <= width G implies G*(i,j)`1 <= G*
(len G,k)`1
proof
assume that
A1: [i,j] in Indices G and
A2: 1 <= k & k <= width G;
A3: 1 <= i & i <= len G & 1 <= j & j <= width G by A1,GOBOARD5:1;
then A4: G*(i,j)`1 = G*(i,1)`1 by GOBOARD5:3
.= G*(i,k)`1 by A2,A3,GOBOARD5:3;
i < len G or i = len G by A3,REAL_1:def 5;
hence thesis by A2,A3,A4,GOBOARD5:4;
end;
theorem
[i,j] in Indices G & 1 <= k & k <= len G implies G*(i,j)`2 <= G*
(k,width G)`2
proof
assume that
A1: [i,j] in Indices G and
A2: 1 <= k & k <= len G;
A3: 1 <= i & i <= len G & 1 <= j & j <= width G by A1,GOBOARD5:1;
then A4: G*(i,j)`2 = G*(1,j)`2 by GOBOARD5:2
.= G*(k,j)`2 by A2,A3,GOBOARD5:2;
j < width G or j = width G by A3,REAL_1:def 5;
hence thesis by A2,A3,A4,GOBOARD5:5;
end;
theorem Th28:
f is_sequence_on G & f is special & L~g c= L~f & 1 <= k & k+1 <= len f
implies
for A being Subset of TOP-REAL 2 st
A = right_cell(f,k,G)\L~g or A = left_cell(f,k,G)\L~g holds A is connected
proof
assume that
A1: f is_sequence_on G & f is special & L~g c= L~f and
A2: 1 <= k and
A3: k+1 <= len f;
let A be Subset of TOP-REAL 2 such that
A4: A = right_cell(f,k,G)\L~g or A = left_cell(f,k,G)\L~g;
per cases by A4;
suppose
A5: A = right_cell(f,k,G)\L~g;
then A6: A = right_cell(f,k,G) /\ (L~g)` by SUBSET_1:32;
A7: A c= right_cell(f,k,G) by A5,XBOOLE_1:36;
A8: Int right_cell(f,k,G) is connected by A1,A2,A3,Th12;
Int right_cell(f,k,G) misses L~f by A1,A2,A3,Th17;
then Int right_cell(f,k,G) misses L~g by A1,XBOOLE_1:63;
then A9: Int right_cell(f,k,G) c= (L~g)` by SUBSET_1:43;
Int right_cell(f,k,G) c= right_cell(f,k,G) by TOPS_1:44;
then A10: Int right_cell(f,k,G) c= A by A6,A9,XBOOLE_1:19;
A c= Cl Int right_cell(f,k,G) by A1,A2,A3,A7,Th13;
hence A is connected by A8,A10,CONNSP_1:19;
suppose
A11: A = left_cell(f,k,G)\L~g;
then A12: A = left_cell(f,k,G) /\ (L~g)` by SUBSET_1:32;
A13: A c= left_cell(f,k,G) by A11,XBOOLE_1:36;
A14: Int left_cell(f,k,G) is connected by A1,A2,A3,Th12;
Int left_cell(f,k,G) misses L~f by A1,A2,A3,Th17;
then Int left_cell(f,k,G) misses L~g by A1,XBOOLE_1:63;
then A15: Int left_cell(f,k,G) c= (L~g)` by SUBSET_1:43;
Int left_cell(f,k,G) c= left_cell(f,k,G) by TOPS_1:44;
then A16: Int left_cell(f,k,G) c= A by A12,A15,XBOOLE_1:19;
A c= Cl Int left_cell(f,k,G) by A1,A2,A3,A13,Th13;
hence A is connected by A14,A16,CONNSP_1:19;
end;
theorem Th29:
for f being non constant standard special_circular_sequence st
f is_sequence_on G
for k st 1 <= k & k+1 <= len f
holds
right_cell(f,k,G)\L~f c= RightComp f & left_cell(f,k,G)\L~f c= LeftComp f
proof
let f be non constant standard special_circular_sequence such that
A1: f is_sequence_on G;
let k such that
A2: 1 <= k & k+1 <= len f;
set rc = right_cell(f,k,G)\L~f;
A3: rc = right_cell(f,k,G) /\ (L~f)` by SUBSET_1:32;
A4: rc c= right_cell(f,k,G) by XBOOLE_1:36;
right_cell(f,k,G) c= right_cell(f,k) by A1,A2,GOBRD13:34;
then rc c= right_cell(f,k) by A4,XBOOLE_1:1;
then A5: Int rc c= Int right_cell(f,k) by TOPS_1:48;
Int right_cell(f,k) c= RightComp f by A2,GOBOARD9:28;
then A6: Int rc c= RightComp f by A5,XBOOLE_1:1;
A7: Int right_cell(f,k,G) <> {} by A1,A2,Th11;
A8: Int right_cell(f,k,G) misses L~f by A1,A2,Th17;
A9: Int right_cell(f,k,G) c= right_cell(f,k,G) by TOPS_1:44;
rc \/ L~f = right_cell(f,k,G) \/ L~f by XBOOLE_1:39;
then right_cell(f,k,G) c= rc \/ L~f by XBOOLE_1:7;
then Int right_cell(f,k,G) c= rc \/ L~f by A9,XBOOLE_1:1;
then A10: Int right_cell(f,k,G) c= rc by A8,XBOOLE_1:73;
then Int Int right_cell(f,k,G) c= Int rc by TOPS_1:48;
then Int right_cell(f,k,G) c= Int rc by TOPS_1:45;
then A11: rc meets Int rc by A7,A10,XBOOLE_1:68;
A12: rc is connected by A1,A2,Th28;
A13: RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
rc c= (L~f)` by A3,XBOOLE_1:17;
hence right_cell(f,k,G)\L~f c= RightComp f by A6,A11,A12,A13,GOBOARD9:6;
set lc = left_cell(f,k,G)\L~f;
A14: lc = left_cell(f,k,G) /\ (L~f)` by SUBSET_1:32;
A15: lc c= left_cell(f,k,G) by XBOOLE_1:36;
left_cell(f,k,G) c= left_cell(f,k) by A1,A2,GOBRD13:34;
then lc c= left_cell(f,k) by A15,XBOOLE_1:1;
then A16: Int lc c= Int left_cell(f,k) by TOPS_1:48;
Int left_cell(f,k) c= LeftComp f by A2,GOBOARD9:24;
then A17: Int lc c= LeftComp f by A16,XBOOLE_1:1;
A18: Int left_cell(f,k,G) <> {} by A1,A2,Th11;
A19: Int left_cell(f,k,G) misses L~f by A1,A2,Th17;
A20: Int left_cell(f,k,G) c= left_cell(f,k,G) by TOPS_1:44;
lc \/ L~f = left_cell(f,k,G) \/ L~f by XBOOLE_1:39;
then left_cell(f,k,G) c= lc \/ L~f by XBOOLE_1:7;
then Int left_cell(f,k,G) c= lc \/ L~f by A20,XBOOLE_1:1;
then A21: Int left_cell(f,k,G) c= lc by A19,XBOOLE_1:73;
then Int Int left_cell(f,k,G) c= Int lc by TOPS_1:48;
then Int left_cell(f,k,G) c= Int lc by TOPS_1:45;
then A22: lc meets Int lc by A18,A21,XBOOLE_1:68;
A23: lc is connected by A1,A2,Th28;
A24: LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
lc c= (L~f)` by A14,XBOOLE_1:17;
hence left_cell(f,k,G)\L~f c= LeftComp f by A17,A22,A23,A24,GOBOARD9:6;
end;
begin :: Cages
reserve
C for compact non vertical non horizontal non empty Subset of TOP-REAL 2,
l, m, i1, i2, j1, j2 for Nat;
theorem Th30:
ex i st 1 <= i & i+1 <= len Gauge(C,n) &
N-min C in cell(Gauge(C,n),i,width Gauge(C,n)-'1) &
N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-'1)
proof
set G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
defpred P[Nat]
means 1 <= $1 & $1 < len G & G*($1,(width G)-'1)`1 < (N-min C)`1;
A2: for k st P[k] holds k <= len G;
A3: len G = 2|^n+3 & len G = width G by JORDAN8:def 1;
A4: len G >= 4 by JORDAN8:13;
then A5: 1 < len G by AXIOMS:22;
then A6: 1 <= (len G)-'1 by JORDAN3:12;
A7: (len G)-'1 <= len G by GOBOARD9:2;
(NW-corner C)`1 <= (N-min C)`1 by PSCOMP_1:97;
then A8: W-bound C <= (N-min C)`1 by PSCOMP_1:74;
A9: 2 <= len G by A4,AXIOMS:22;
G*(2,(width G)-'1)`1 = W-bound C by A1,A6,A7,JORDAN8:14;
then G*(1,(width G)-'1)`1 < W-bound C by A3,A6,A7,A9,GOBOARD5:4;
then G*(1,(width G)-'1)`1 < (N-min C)`1 by A8,AXIOMS:22;
then A10: ex k st P[k] by A5;
ex i st P[i] & for n st P[n] holds n <= i from Max(A2,A10);
then consider i such that
A11: 1 <= i & i < len G and
A12: G*(i,(width G)-'1)`1 < (N-min C)`1 and
A13: for n st P[n] holds n <= i;
take i;
thus 1 <= i & i+1 <= len G by A11,NAT_1:38;
A14: LSeg(G*(i,(width G)-'1),G*(i+1,(width G)-'1)) c= cell(G,i,(width G)-'1)
by A3,A6,A7,A11,GOBOARD5:23;
A15: i+1 <= len G by A11,NAT_1:38;
A16: 1 <= i+1 by NAT_1:37;
(N-min C)`2 = N-bound C by PSCOMP_1:94;
then A17: G*(i,(width G)-'1)`2 = (N-min C)`2 & (N-min C)`2 = G*
(i+1,(width G)-'1)`2
by A1,A11,A15,A16,JORDAN8:17;
now assume i+1 = len G;
then len G-'1 = i by BINARITH:39;
then A18: G*(i,(width G)-'1)`1 = E-bound C by A1,A6,A7,JORDAN8:15;
(NE-corner C)`1 >= (N-min C)`1 by PSCOMP_1:97;
hence contradiction by A12,A18,PSCOMP_1:76;
end;
then i+1 < len G & i < i+1 by A15,NAT_1:38,REAL_1:def 5;
then (N-min C)`1 <= G*(i+1,(width G)-'1)`1 by A13,A16;
then N-min C in LSeg(G*(i,(width G)-'1),G*(i+1,(width G)-'1))
by A12,A17,GOBOARD7:9;
hence N-min C in cell(G,i,(width G)-'1) by A14;
thus N-min C <> G*(i,(width G)-'1) by A12;
end;
theorem Th31:
1 <= i1 & i1+1 <= len Gauge(C,n) &
N-min C in cell(Gauge(C,n),i1,width Gauge(C,n)-'1) &
N-min C <> Gauge(C,n)*(i1,width Gauge(C,n)-'1) &
1 <= i2 & i2+1 <= len Gauge(C,n) &
N-min C in cell(Gauge(C,n),i2,width Gauge(C,n)-'1) &
N-min C <> Gauge(C,n)*(i2,width Gauge(C,n)-'1)
implies
i1 = i2
proof
set G = Gauge(C,n), j = width G-'1;
assume that
A1: 1 <= i1 & i1+1 <= len G and
A2: N-min C in cell(G,i1,j) and
A3: N-min C <> G*(i1,j) and
A4: 1 <= i2 & i2+1 <= len G and
A5: N-min C in cell(G,i2,j) and
A6: N-min C <> G*(i2,j) and
A7: i1 <> i2;
A8: i1 < len G & i2 < len G & len G = width G by A1,A4,JORDAN8:def 1,NAT_1:38;
A9: cell(G,i1,j) meets cell(G,i2,j) by A2,A5,XBOOLE_0:3;
A10: len G = 2|^n+3 & len G = width G by JORDAN8:def 1;
A11: n+3 > 0 by NAT_1:19;
A12: 2|^n >= n+1 by HEINE:7;
then len G >= n+1+3 by A10,AXIOMS:24;
then len G >= 1+ (n+3) & 1+ (n+3) > 1+0 by A11,REAL_1:53,XCMPLX_1:1;
then A13: len G > 1 by AXIOMS:22;
then len G >= 1+1 by NAT_1:38;
then A14: 1 <= j by A8,JORDAN5B:2;
A15: j+1 = len G by A8,A13,AMI_5:4;
then A16: j < len G by NAT_1:38;
A17: (N-min C)`2 = N-bound C by PSCOMP_1:94;
per cases by A7,REAL_1:def 5;
suppose
A18: i1 < i2;
then A19: i2-'i1+i1 = i2 by AMI_5:4;
then i2-'i1 <= 1 by A8,A9,A14,A16,JORDAN8:10;
then i2-'i1 < 1 or i2-'i1 = 1 by REAL_1:def 5;
then i2-'i1 = 0 or i2-'i1 = 1 by RLVECT_1:98;
then cell(G,i1,j) /\ cell(G,i2,j) = LSeg(G*(i2,j),G*(i2,j+1))
by A8,A14,A16,A18,A19,GOBOARD5:26;
then A20: N-min C in LSeg(G*(i2,j),G*(i2,j+1)) by A2,A5,XBOOLE_0:def 3;
A21: [i2,j] in Indices G by A4,A8,A14,A16,GOBOARD7:10;
1 <= j+1 by NAT_1:37;
then A22: [i2,j+1] in Indices G by A4,A8,A15,GOBOARD7:10;
set x = (W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i2-2);
set y1 = (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2);
set y2 = (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-1);
A23: j+1-(1+1) = j+1-1-1 by XCMPLX_1:36
.= j-1 by XCMPLX_1:26;
A24: G*(i2,j) = |[x,y1]| by A21,JORDAN8:def 1;
G*(i2,j+1) = |[x,y2]| by A22,A23,JORDAN8:def 1;
then A25: G*(i2,j)`1 = x & G*(i2,j+1)`1 = x by A24,EUCLID:56;
then LSeg(G*(i2,j),G*(i2,j+1)) is vertical by SPPOL_1:37;
then A26: (N-min C)`1 = G*(i2,j)`1 by A20,SPRECT_3:20;
A27: 2|^n > 0 by A12,NAT_1:37;
j = (2|^n+(2+1))-'1 by A10
.= (2|^n+2+1)-'1 by XCMPLX_1:1
.= (2|^n+2) by BINARITH:39;
then j-2 = 2|^n by XCMPLX_1:26;
then (((N-bound C)-(S-bound C))/(2|^n))*(j-2) = (N-bound C)-(S-bound C)
by A27,XCMPLX_1:88;
then y1 = N-bound C by XCMPLX_1:27;
hence contradiction by A6,A17,A24,A25,A26,EUCLID:57;
suppose
A28: i2 < i1;
then A29: i1-'i2+i2 = i1 by AMI_5:4;
then i1-'i2 <= 1 by A8,A9,A14,A16,JORDAN8:10;
then i1-'i2 < 1 or i1-'i2 = 1 by REAL_1:def 5;
then i1-'i2 = 0 or i1-'i2 = 1 by RLVECT_1:98;
then cell(G,i2,j) /\ cell(G,i1,j) = LSeg(G*(i1,j),G*(i1,j+1))
by A8,A14,A16,A28,A29,GOBOARD5:26;
then A30: N-min C in LSeg(G*(i1,j),G*(i1,j+1)) by A2,A5,XBOOLE_0:def 3;
A31: [i1,j] in Indices G by A1,A8,A14,A16,GOBOARD7:10;
1 <= j+1 by NAT_1:37;
then A32: [i1,j+1] in Indices G by A1,A8,A15,GOBOARD7:10;
set x = (W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i1-2);
set y1 = (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2);
set y2 = (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-1);
A33: j+1-(1+1) = j+1-1-1 by XCMPLX_1:36
.= j-1 by XCMPLX_1:26;
A34: G*(i1,j) = |[x,y1]| by A31,JORDAN8:def 1;
G*(i1,j+1) = |[x,y2]| by A32,A33,JORDAN8:def 1;
then A35: G*(i1,j)`1 = x & G*(i1,j+1)`1 = x by A34,EUCLID:56;
then LSeg(G*(i1,j),G*(i1,j+1)) is vertical by SPPOL_1:37;
then A36: (N-min C)`1 = G*(i1,j)`1 by A30,SPRECT_3:20;
A37: 2|^n > 0 by A12,NAT_1:37;
j = (2|^n+(2+1))-'1 by A10
.= (2|^n+2+1)-'1 by XCMPLX_1:1
.= (2|^n+2) by BINARITH:39;
then j-2 = 2|^n by XCMPLX_1:26;
then (((N-bound C)-(S-bound C))/(2|^n))*(j-2) = (N-bound C)-(S-bound C)
by A37,XCMPLX_1:88;
then y1 = N-bound C by XCMPLX_1:27;
hence contradiction by A3,A17,A34,A35,A36,EUCLID:57;
end;
theorem Th32:
for f being standard non constant special_circular_sequence
st f is_sequence_on Gauge(C,n) &
(for k st 1 <= k & k+1 <= len f
holds
left_cell(f,k,Gauge(C,n)) misses C &
right_cell(f,k,Gauge(C,n)) meets C) &
(ex i st 1 <= i & i+1 <= len Gauge(C,n) &
f/.1 = Gauge(C,n)*(i,width Gauge(C,n)) &
f/.2 = Gauge(C,n)*(i+1,width Gauge(C,n)) &
N-min C in cell(Gauge(C,n),i,width Gauge(C,n)-'1) &
N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-'1))
holds
N-min L~f = f/.1
proof
set G = Gauge(C,n);
let f be standard non constant special_circular_sequence such that
A1: f is_sequence_on G and
A2: for k st 1 <= k & k+1 <= len f
holds left_cell(f,k,G) misses C & right_cell(f,k,G) meets C;
given i' being Nat such that
A3: 1 <= i' & i'+1 <= len G and
A4: f/.1 = G*(i',width G) and
A5: f/.2 = G*(i'+1,width G) and
A6: N-min C in cell(G,i',width G-'1) and
A7: N-min C <> G*(i',width G-'1);
A8: i' < len G & len G = width G by A3,JORDAN8:def 1,NAT_1:38;
len f > 4 by GOBOARD7:36;
then A9: len f >= 2 by AXIOMS:22;
A10: len G = 2|^n+3 & len G = width G by JORDAN8:def 1;
then len G >= 3 by NAT_1:37;
then A11: 1 < len G by AXIOMS:22;
set W = W-bound C, S = S-bound C, E = E-bound C, N = N-bound C;
N-min L~f in rng f by SPRECT_2:43;
then consider m such that
A12: m in dom f and
A13: f.m = N-min L~f by FINSEQ_2:11;
A14: f/.m = f.m by A12,FINSEQ_4:def 4;
A15: (N-min L~f)`2 = N-bound L~f by PSCOMP_1:94;
A16: 2|^n > 0 by HEINE:5;
N > S by JORDAN8:12;
then N-S > 0 by SQUARE_1:11;
then A17: (N-S)/(2|^n) > 0 by A16,REAL_2:127;
A18: 1 <= m & m <= len f by A12,FINSEQ_3:27;
consider i,j such that
A19: [i,j] in Indices G and
A20: f/.m = G*(i,j) by A1,A12,GOBOARD1:def 11;
A21: 1 <= i & i <= len G & 1 <= j & j <= width G by A19,GOBOARD5:1;
G*(i,j) = |[W+((E-W)/(2|^n))*(i-2), S+((N-S)/(2|^n))*(j-2)]|
by A19,JORDAN8:def 1;
then A22: S+((N-S)/(2|^n))*(j-2) = N-bound L~f by A13,A14,A15,A20,EUCLID:56
;
1 in dom f by FINSEQ_5:6;
then A23: f/.1 in L~f by A9,GOBOARD1:16;
then A24: N-bound L~f >= (f/.1)`2 by PSCOMP_1:71;
G*(i',j)`2 = G*(1,j)`2 & G*(i,j)`2 = G*
(1,j)`2 by A3,A8,A21,GOBOARD5:2;
then G*(i,j)`2 <= G*(i',len G)`2 by A3,A8,A21,SPRECT_3:24;
then A25: N-bound L~f = (f/.1)`2 by A4,A8,A13,A14,A15,A20,A24,AXIOMS:21;
[i',len G] in Indices G by A3,A8,A11,GOBOARD7:10;
then G*(i',len G)=|[W+((E-W)/(2|^n))*(i'-2),S+((N-S)/(2|^n))*(len G-2)]|
by JORDAN8:def 1;
then S+((N-S)/(2|^n))*(len G-2) = N-bound L~f by A4,A8,A25,EUCLID:56;
then ((N-S)/(2|^n))*(j-2) = ((N-S)/(2|^n))*(len G-2) by A22,XCMPLX_1:2;
then len G-2 = j-2 by A17,XCMPLX_1:5;
then A26: len G = j by XCMPLX_1:19;
A27: (NW-corner C)`1 = W & (NE-corner C)`1 = E &
(NW-corner C)`2 = N & (NE-corner C)`2 = N
by PSCOMP_1:74,75,76,77;
A28: G*(i',len G)`1 = G*(i',1)`1 by A3,A8,A21,A26,GOBOARD5:3;
A29: G*(i,len G)`1 = G*(i,1)`1 by A21,A26,GOBOARD5:3;
A30: (NW-corner L~f)`1 = W-bound L~f & (NE-corner L~f)`1 = E-bound L~f &
(NW-corner L~f)`2 = N-bound L~f & (NE-corner L~f)`2 = N-bound L~f
by PSCOMP_1:74,75,76,77;
W-bound L~f <= (f/.1)`1 & (f/.1)`1 <= E-bound L~f by A23,PSCOMP_1:71;
then f/.1 in LSeg(NW-corner L~f, NE-corner L~f) by A25,A30,GOBOARD7:9;
then f/.1 in LSeg(NW-corner L~f, NE-corner L~f) /\ L~f
by A23,XBOOLE_0:def 3;
then f/.1 in N-most L~f by PSCOMP_1:def 39;
then A31: (N-min L~f)`1 <= (f/.1)`1 by PSCOMP_1:98;
A32: 1 <= len G-'1 by A11,JORDAN3:12;
then A33: len G-'1 < len G by JORDAN3:14;
A34: len G-'1+1 = len G by A11,AMI_5:4;
then N-min C in { |[r',s']| where r',s' is Real:
G*(i',1)`1 <= r' & r' <= G*(i'+1,1)`1 &
G*(1,len G-'1)`2 <= s' & s' <= G*(1,len G)`2 }
by A3,A6,A8,A32,A33,GOBRD11:32;
then consider r',s' being Real such that
A35: N-min C = |[r',s']| and
A36: G*(i',1)`1 <= r' & r' <= G*(i'+1,1)`1 and
G*(1,len G-'1)`2 <= s' & s' <= G*(1,len G)`2;
A37: (f/.1)`1 <= (N-min C)`1 by A4,A8,A28,A35,A36,EUCLID:56;
then A38: (N-min L~f)`1 <= (N-min C)`1 by A31,AXIOMS:22;
A39: G*(i',len G-'1)`1 = G*(i',1)`1 by A3,A8,A32,A33,GOBOARD5:3;
A40: N-min C = |[(N-min C)`1,(N-min C)`2]| by EUCLID:57;
A41: G*(i',len G-'1) = |[G*(i',len G-'1)`1,G*(i',len G-'1)`2]|
by EUCLID:57;
A42: (N-min C)`2 = N by PSCOMP_1:94;
G*(i',len G-'1)`2 = N by A3,A8,JORDAN8:17;
then A43: G*(i',len G-'1)`1 < (N-min C)`1
by A4,A7,A8,A28,A37,A39,A40,A41,A42,REAL_1:def 5;
A44: i <= i' by A3,A4,A8,A13,A14,A20,A21,A26,A31,GOBOARD5:4;
then A45: i < len G by A8,AXIOMS:22;
then A46: i+1 <= len G by NAT_1:38;
per cases by A18,REAL_1:def 5;
suppose m = len f;
hence N-min L~f = f/.1 by A13,A14,FINSEQ_6:def 1;
suppose m < len f;
then A47: m+1 <= len f by NAT_1:38;
then A48: right_cell(f,m,G) meets C by A2,A18;
then consider p being set such that
A49: p in right_cell(f,m,G) & p in C by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A49;
consider i1,j1,i2,j2 being Nat such that
A50: [i1,j1] in Indices G & f/.m = G*(i1,j1) and
A51: [i2,j2] in Indices G & f/.(m+1) = G*(i2,j2) and
A52: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A18,A47,JORDAN8:6;
A53: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= len G by A10,A51,GOBOARD5:1;
A54: (N-min C)`2 = N by PSCOMP_1:94;
then A55: p`2 <= (N-min C)`2 by A49,PSCOMP_1:71;
A56: G*(1,len G-'1)`2 = N by A11,JORDAN8:17;
A57: G*(1,len G-'1)`2 < G*(1,len G)`2 by A10,A11,A32,A33,GOBOARD5:5;
A58: W <= p`1 & p`1 <= E by A49,PSCOMP_1:71;
now per cases by A19,A20,A26,A50,A52,GOBOARD1:21;
suppose i = i2 & len G+1 = j2;
hence N-min L~f = f/.1 by A53,NAT_1:38;
suppose i+1 = i2 & len G = j2;
then A59: right_cell(f,m,G) = cell(G,i,len G-'1)
by A1,A18,A19,A20,A26,A47,A51,GOBRD13:25;
A60: cell(G,i,len G-'1) = {|[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 &
G*(1,len G-'1)`2 <= s & s <= G*(1,len G-'1+1)`2 }
by A10,A21,A32,A33,A45,GOBRD11:32;
then consider r,s such that
A61: p = |[r,s]| and
A62: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 and
A63: G*(1,len G-'1)`2 <= s & s <= G*(1,len G-'1+1)`2 by A49,A59;
A64: p`1 = r & p`2 = s by A61,EUCLID:56;
then p`2 = N by A54,A55,A56,A63,AXIOMS:21;
then p in LSeg(NW-corner C, NE-corner C) by A27,A58,GOBOARD7:9;
then p in LSeg(NW-corner C, NE-corner C) /\ C
by A49,XBOOLE_0:def 3;
then p in N-most C by PSCOMP_1:def 39;
then (N-min C)`1 <= p`1 by PSCOMP_1:98;
then (N-min C)`1 <= G*(i+1,1)`1 by A62,A64,AXIOMS:22;
then A65: N-min C in cell(G,i,width G-'1)
by A8,A13,A14,A20,A26,A29,A34,A38,A40,A54,A56,A57,A60;
N-min C <> G*(i,len G-'1) by A8,A21,A32,A33,A43,A44,SPRECT_3:25;
hence N-min L~f = f/.1
by A3,A4,A6,A7,A8,A13,A14,A20,A21,A26,A46,A65,Th31;
suppose
A66: i = i2+1 & len G = j2;
then A67: right_cell(f,m,G) = cell(G,i2,len G)
by A1,A18,A19,A20,A26,A47,A51,GOBRD13:27;
i2 < len G by A21,A66,NAT_1:38;
hence N-min L~f = f/.1 by A48,A67,JORDAN8:18;
suppose
A68: i = i2 & len G = j2+1;
then A69: j2 = len G-'1 by BINARITH:39;
then A70: right_cell(f,m,G) = cell(G,i-'1,len G-'1)
by A1,A18,A19,A20,A26,A47,A51,A68,GOBRD13:29;
now assume
A71: m = 1;
1 <= i'+1 & i'+1<= len G by A3,NAT_1:38;
then G*(i',len G)`2 = G*(1,len G)`2 & G*(i'+1,len G)`2 = G*
(1,len G)`2 by A3,A8,A11,GOBOARD5:2;
hence contradiction
by A4,A5,A8,A20,A21,A26,A32,A33,A51,A68,A69,A71,GOBOARD5:5;
end;
then m > 1 by A18,REAL_1:def 5;
then A72: m-'1 >= 1 by JORDAN3:12;
A73: m-'1+1 = m by A18,AMI_5:4;
m-'1 <= m by GOBOARD9:2;
then A74: m-'1 <= len f by A18,AXIOMS:22;
consider i1',j1',i2',j2' being Nat such that
A75: [i1',j1'] in Indices G & f/.(m-'1) = G*(i1',j1') and
A76: [i2',j2'] in Indices G & f/.m = G*(i2',j2') and
A77: i1' = i2' & j1'+1 = j2' or i1'+1 = i2' & j1' = j2' or
i1' = i2'+1 & j1' = j2' or i1' = i2' & j1' = j2'+1
by A1,A18,A72,A73,JORDAN8:6;
A78: 1 <= i1' & i1' <= len G & 1 <= j1' &
j1' <= len G by A10,A75,GOBOARD5:1;
now per cases by A19,A20,A26,A76,A77,GOBOARD1:21;
suppose
A79: i1' = i & j1'+1 = len G;
then j1' = len G-'1 by BINARITH:39;
then left_cell(f,m-'1,G) = cell(G,i-'1,len G-'1)
by A1,A18,A19,A20,A26,A72,A73,A75,A79,GOBRD13:22;
hence contradiction by A2,A18,A48,A70,A72,A73;
suppose
A80: i1'+1 = i & j1' = len G;
then i1' < i by NAT_1:38;
then A81: (f/.(m-'1))`1 < (f/.m)`1 by A20,A21,A26,A75,A78,A80,GOBOARD5:4;
A82: G*(i1',j)`2 = G*(1,j)`2 & G*(i,j)`2 = G*(1,j)`2
by A21,A78,GOBOARD5:2;
m-'1 in dom f by A72,A74,FINSEQ_3:27;
then A83: f/.(m-'1) in L~f by A9,GOBOARD1:16;
then W-bound L~f <= (f/.(m-'1))`1 &
(f/.(m-'1))`1 <= E-bound L~f by PSCOMP_1:71;
then f/.(m-'1) in LSeg(NW-corner L~f, NE-corner L~f)
by A13,A14,A15,A20,A26,A30,A75,A80,A82,GOBOARD7:9;
then f/.(m-'1) in LSeg(NW-corner L~f, NE-corner L~f) /\ L~f
by A83,XBOOLE_0:def 3;
then f/.(m-'1) in N-most L~f by PSCOMP_1:def 39;
hence contradiction by A13,A14,A81,PSCOMP_1:98;
suppose i1' = i+1 & j1' = len G;
then right_cell(f,m-'1,G) = cell(G,i,len G)
by A1,A18,A19,A20,A26,A72,A73,A75,GOBRD13:27;
then cell(G,i,len G) meets C by A2,A18,A72,A73;
hence contradiction by A21,JORDAN8:18;
suppose i1' = i & j1' = len G+1;
then len G+1 <= len G+0 by A10,A75,GOBOARD5:1;
hence contradiction by REAL_1:53;
end;
hence N-min L~f = f/.1;
end;
hence N-min L~f = f/.1;
end;
definition
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n be Nat;
assume
A1: C is connected;
func Cage(C,n) -> clockwise_oriented
(standard non constant special_circular_sequence) means
:Def1:
it is_sequence_on Gauge(C,n) &
(ex i st 1 <= i & i+1 <= len Gauge(C,n) &
it/.1 = Gauge(C,n)*(i,width Gauge(C,n)) &
it/.2 = Gauge(C,n)*(i+1,width Gauge(C,n)) &
N-min C in cell(Gauge(C,n),i,width Gauge(C,n)-'1) &
N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-'1)) &
for k st 1 <= k & k+2 <= len it holds
(front_left_cell(it,k,Gauge(C,n)) misses C &
front_right_cell(it,k,Gauge(C,n)) misses C
implies
it turns_right k,Gauge(C,n)) &
(front_left_cell(it,k,Gauge(C,n)) misses C &
front_right_cell(it,k,Gauge(C,n)) meets C
implies
it goes_straight k,Gauge(C,n)) &
(front_left_cell(it,k,Gauge(C,n)) meets C
implies
it turns_left k,Gauge(C,n));
existence
proof
set G = Gauge(C,n);
set W = W-bound C, E = E-bound C, S = S-bound C, N = N-bound C;
A2: len G = 2|^n+3 & len G = width G by JORDAN8:def 1;
defpred P[Nat,set,set] means
($1 = 0 implies
ex i st 1 <= i & i+1 <= len G &
N-min C in cell(G,i,width G-'1) & N-min C <> G*(i,width G-'1) &
$3 = <*G*(i,width G)*>) &
($1 = 1 implies
ex i st 1 <= i & i+1 <= len G &
N-min C in cell(G,i,width G-'1) & N-min C <> G*(i,width G-'1) &
$3 = <*G*(i,width G),G*(i+1,width G)*>) &
($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 & right_cell(f,len f-'1,G) meets C implies
(front_left_cell(f,(len f)-'1,G) misses C &
front_right_cell(f,(len f)-'1,G) misses C
implies ex i,j st
f^<*G*(i,j)*> turns_right (len f)-'1,G &
$3 = f^<*G*(i,j)*>) &
(front_left_cell(f,(len f)-'1,G) misses C &
front_right_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_left_cell(f,(len f)-'1,G) meets C
implies ex i,j st
f^<*G*(i,j)*> turns_left (len f)-'1,G &
$3 = f^<*G*(i,j)*>)) &
(not f is_sequence_on G or right_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;
consider m being Nat such that
A4: 1 <= m & m+1 <= len G and
A5: N-min C in cell(G,m,width G-'1) &
N-min C <> G*(m,width G-'1) by Th30;
per cases by CQC_THE1:2;
suppose
A6: k=0;
take <*G*(m,width G)*>;
thus thesis by A4,A5,A6;
suppose
A7: k = 1;
take <*G*(m,width G),G*(m+1,width G)*>;
thus thesis by A4,A5,A7;
suppose that
A8: k > 1 and
A9: x is FinSequence of TOP-REAL 2;
reconsider f = x as FinSequence of TOP-REAL 2 by A9;
thus thesis
proof per cases;
suppose
A10: len f = k;
thus thesis
proof per cases;
suppose
A11: f is_sequence_on G & right_cell(f,len f-'1,G) meets C;
A12: 1 <= (len f)-'1 by A8,A10,JORDAN3:12;
A13: (len f) -'1 +1 = len f by A8,A10,AMI_5:4;
then consider i1,j1,i2,j2 being Nat such that
A14: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and
A15: [i2,j2] in Indices G & f/.((len f) -'1+1) = G*(i2,j2) and
A16: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A11,A12,JORDAN8:6;
A17: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A14,GOBOARD5:1;
A18: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A15,GOBOARD5:1;
A19: i1-'1 <= len G & j1-'1 <= width G by A17,JORDAN3:7;
A20: 1 <= i2+1 & 1 <= j2+1 by NAT_1:37;
A21: i2-'1 <= len G & j2-'1 <= width G by A18,JORDAN3:7;
(len f)-'1 <= len f by GOBOARD9:2;
then A22: (len f)-'1 in dom f & (len f)-'1+1 in dom f
by A8,A10,A12,A13,FINSEQ_3:27;
A23: (len f)-'1+(1+1) = (len f)+1 by A13,XCMPLX_1:1;
thus thesis
proof per cases;
suppose
A24: front_left_cell(f,(len f)-'1,G) misses C &
front_right_cell(f,(len f)-'1,G) misses C;
thus thesis
proof per cases by A16;
suppose
A25: i1 = i2 & j1+1 = j2;
take f1 = f^<*G*(i2+1,j2)*>;
now
take i=i2+1 ,j=j2;
thus f1 turns_right (len f)-'1,G
proof let i1',j1',i2',j2' be Nat;
assume that
A26: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A27: 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 A22,A27,GROUP_5:95;
then A28: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A26,GOBOARD1:21;
per cases by A16,A28;
case i1' = i2' & j1'+1 = j2';
now assume i2+1 > len G;
then i2+1 <= (len G)+1 & (len G)+1 <= i2+1
by A18,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 A11,A12,A13,A14,A15,A25,GOBRD13:23;
hence contradiction by A2,A17,JORDAN8:19;
end;
hence [i2'+1,j2'] in Indices G by A18,A20,A28,GOBOARD7:10;
thus thesis by A23,A28,TOPREAL4:1;
case i1'+1 = i2' & j1' = j2';
hence thesis by A25,A28,NAT_1:38;
case i1' = i2'+1 & j1' = j2';
hence thesis by A25,A28,NAT_1:38;
case
A29: i1' = i2' & j1' = j2'+1;
j1+1+1 = j1+(1+1) by XCMPLX_1:1;
hence thesis by A25,A28,A29,REAL_1:69;
end;
end;
hence thesis by A8,A10,A11,A24;
suppose
A30: i1+1 = i2 & j1 = j2;
take f1 = f^<*G*(i2,j2-'1)*>;
now
take i=i2 ,j=j2-'1;
thus f1 turns_right (len f)-'1,G
proof let i1',j1',i2',j2' be Nat;
assume that
A31: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A32: 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 A22,A32,GROUP_5:95;
then A33: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A31,GOBOARD1:21;
per cases by A16,A33;
case i1' = i2' & j1'+1 = j2';
hence thesis by A30,A33,NAT_1:38;
case i1'+1 = i2' & j1' = j2';
now assume j2-'1 < 1;
then j2-'1 = 0 by RLVECT_1:98;
then j2 <= 1 by JORDAN4:1;
then j2 = 1 by A18,AXIOMS:21;
then cell(G,i1,1-'1) meets C
by A11,A12,A13,A14,A15,A30,GOBRD13:25;
then cell(G,i1,0) meets C by GOBOARD9:1;
hence contradiction by A17,JORDAN8:20;
end;
hence [i2',j2'-'1] in Indices G by A18,A21,A33,GOBOARD7:10;
thus f1/.((len f)-'1+2) = G*(i2',j2'-'1)
by A23,A33,TOPREAL4:1;
case
A34: i1' = i2'+1 & j1' = j2';
i1+1+1 = i1+(1+1) by XCMPLX_1:1;
hence thesis by A30,A33,A34,REAL_1:69;
case i1' = i2' & j1' = j2'+1;
hence thesis by A30,A33,NAT_1:38;
end;
end;
hence thesis by A8,A10,A11,A24;
suppose
A35: i1 = i2+1 & j1 = j2;
take f1 = f^<*G*(i2,j2+1)*>;
now
take i=i2 ,j=j2+1;
thus f1 turns_right (len f)-'1,G
proof 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 A22,A37,GROUP_5:95;
then A38: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A36,GOBOARD1:21;
per cases by A16,A38;
case i1' = i2' & j1'+1 = j2';
hence thesis by A35,A38,NAT_1:38;
case
A39: i1'+1 = i2' & j1' = j2';
i1+1+1 = i1+(1+1) by XCMPLX_1:1;
hence thesis by A35,A38,A39,REAL_1:69;
case i1' = i2'+1 & j1' = j2';
now assume j2+1 > len G;
then j2+1 <= (len G)+1 & (len G)+1 <= j2+1
by A2,A18,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,len G) meets C
by A11,A12,A13,A14,A15,A35,GOBRD13:27;
hence contradiction by A18,JORDAN8:18;
end;
hence [i2',j2'+1] in Indices G by A2,A18,A20,A38,GOBOARD7:10
;
thus f1/.((len f)-'1+2) = G*(i2',j2'+1) by A23,A38,TOPREAL4:1
;
case i1' = i2' & j1' = j2'+1;
hence thesis by A35,A38,NAT_1:38;
end;
end;
hence thesis by A8,A10,A11,A24;
suppose
A40: i1 = i2 & j1 = j2+1;
take f1 = f^<*G*(i2-'1,j2)*>;
now
take i=i2-'1 ,j=j2;
thus f1 turns_right (len f)-'1,G
proof 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 A22,A42,GROUP_5:95;
then A43: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A41,GOBOARD1:21;
per cases by A16,A43;
case
A44: i1' = i2' & j1'+1 = j2';
j1+1+1 = j1+(1+1) by XCMPLX_1:1;
hence thesis by A40,A43,A44,REAL_1:69;
case i1'+1 = i2' & j1' = j2';
hence thesis by A40,A43,NAT_1:38;
case i1' = i2'+1 & j1' = j2';
hence thesis by A40,A43,NAT_1:38;
case i1' = i2' & j1' = j2'+1;
now assume i2-'1 < 1;
then i2-'1 = 0 by RLVECT_1:98;
then i2 <= 1 by JORDAN4:1;
then i2 = 1 by A18,AXIOMS:21;
then cell(G,1-'1,j2) meets C
by A11,A12,A13,A14,A15,A40,GOBRD13:29;
then cell(G,0,j2) meets C by GOBOARD9:1;
hence contradiction by A2,A18,JORDAN8:21;
end;
hence [i2'-'1,j2'] in Indices G by A18,A21,A43,GOBOARD7:10;
thus f1/.((len f)-'1+2) = G*(i2'-'1,j2')
by A23,A43,TOPREAL4:1;
end;
end;
hence thesis by A8,A10,A11,A24;
end;
suppose
A45: front_left_cell(f,(len f)-'1,G) misses C &
front_right_cell(f,(len f)-'1,G) meets C;
thus thesis
proof per cases by A16;
suppose
A46: i1 = i2 & j1+1 = j2;
take f1 = f^<*G*(i2,j2+1)*>;
now
take i=i2 ,j=j2+1;
thus f1 goes_straight (len f)-'1,G
proof let i1',j1',i2',j2' be Nat;
assume that
A47: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A48: 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 A22,A48,GROUP_5:95;
then A49: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A47,GOBOARD1:21;
per cases by A16,A49;
case i1' = i2' & j1'+1 = j2';
now assume j2+1 > len G;
then j2+1 <= (len G)+1 & (len G)+1 <= j2+1
by A2,A18,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 A11,A12,A13,A14,A15,A45,A46,GOBRD13:36;
hence contradiction by A17,JORDAN8:18;
end;
hence [i2',j2'+1] in Indices G by A2,A18,A20,A49,GOBOARD7:10
;
thus f1/.((len f)-'1+2) = G*(i2',j2'+1)
by A23,A49,TOPREAL4:1;
case i1'+1 = i2' & j1' = j2';
hence thesis by A46,A49,NAT_1:38;
case i1' = i2'+1 & j1' = j2';
hence thesis by A46,A49,NAT_1:38;
case
A50: i1' = i2' & j1' = j2'+1;
j1+1+1 = j1+(1+1) by XCMPLX_1:1;
hence thesis by A46,A49,A50,REAL_1:69;
end;
end;
hence thesis by A8,A10,A11,A45;
suppose
A51: i1+1 = i2 & j1 = j2;
take f1 = f^<*G*(i2+1,j2)*>;
now
take i=i2+1 ,j=j2;
thus f1 goes_straight (len f)-'1,G
proof let i1',j1',i2',j2' be Nat;
assume that
A52: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A53: 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 A22,A53,GROUP_5:95;
then A54: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A52,GOBOARD1:21;
per cases by A16,A54;
case i1' = i2' & j1'+1 = j2';
hence thesis by A51,A54,NAT_1:38;
case i1'+1 = i2' & j1' = j2';
now assume i2+1 > len G;
then i2+1 <= (len G)+1 & (len G)+1 <= i2+1
by A18,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-'1) meets C
by A11,A12,A13,A14,A15,A45,A51,GOBRD13:38;
hence contradiction by A2,A19,JORDAN8:19;
end;
hence [i2'+1,j2'] in Indices G by A18,A20,A54,GOBOARD7:10;
thus f1/.((len f)-'1+2) = G*(i2'+1,j2')
by A23,A54,TOPREAL4:1;
case
A55: i1' = i2'+1 & j1' = j2';
i1+1+1 = i1+(1+1) by XCMPLX_1:1;
hence thesis by A51,A54,A55,REAL_1:69;
case i1' = i2' & j1' = j2'+1;
hence thesis by A51,A54,NAT_1:38;
end;
end;
hence thesis by A8,A10,A11,A45;
suppose
A56: i1 = i2+1 & j1 = j2;
take f1 = f^<*G*(i2-'1,j2)*>;
now
take i=i2-'1 ,j=j2;
thus f1 goes_straight (len f)-'1,G
proof let i1',j1',i2',j2' be Nat;
assume that
A57: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A58: 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 A22,A58,GROUP_5:95;
then A59: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A57,GOBOARD1:21;
per cases by A16,A59;
case i1' = i2' & j1'+1 = j2';
hence thesis by A56,A59,NAT_1:38;
case
A60: i1'+1 = i2' & j1' = j2';
i1+1+1 = i1+(1+1) by XCMPLX_1:1;
hence thesis by A56,A59,A60,REAL_1:69;
case i1' = i2'+1 & j1' = j2';
now assume i2-'1 < 1;
then i2-'1 = 0 by RLVECT_1:98;
then i2 <= 1 by JORDAN4:1;
then i2 = 1 by A18,AXIOMS:21;
then cell(G,1-'1,j1) meets C
by A11,A12,A13,A14,A15,A45,A56,GOBRD13:40;
then cell(G,0,j1) meets C by GOBOARD9:1;
hence contradiction by A2,A17,JORDAN8:21;
end;
hence [i2'-'1,j2'] in Indices G by A18,A21,A59,GOBOARD7:10;
thus f1/.((len f)-'1+2) = G*(i2'-'1,j2')
by A23,A59,TOPREAL4:1;
case i1' = i2' & j1' = j2'+1;
hence thesis by A56,A59,NAT_1:38;
end;
end;
hence thesis by A8,A10,A11,A45;
suppose
A61: i1 = i2 & j1 = j2+1;
take f1 = f^<*G*(i2,j2-'1)*>;
now
take i=i2 ,j=j2-'1;
thus f1 goes_straight (len f)-'1,G
proof 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 A22,A63,GROUP_5:95;
then A64: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A62,GOBOARD1:21;
per cases by A16,A64;
case
A65: i1' = i2' & j1'+1 = j2';
j1+1+1 = j1+(1+1) by XCMPLX_1:1;
hence thesis by A61,A64,A65,REAL_1:69;
case i1'+1 = i2' & j1' = j2';
hence thesis by A61,A64,NAT_1:38;
case i1' = i2'+1 & j1' = j2';
hence thesis by A61,A64,NAT_1:38;
case i1' = i2' & j1' = j2'+1;
now assume j2-'1 < 1;
then j2-'1 = 0 by RLVECT_1:98;
then j2 <= 1 by JORDAN4:1;
then j2 = 1 by A18,AXIOMS:21;
then cell(G,i1-'1,1-'1) meets C
by A11,A12,A13,A14,A15,A45,A61,GOBRD13:42;
then cell(G,i1-'1,0) meets C by GOBOARD9:1;
hence contradiction by A19,JORDAN8:20;
end;
hence [i2',j2'-'1] in Indices G by A18,A21,A64,GOBOARD7:10;
thus f1/.((len f)-'1+2) = G*(i2',j2'-'1)
by A23,A64,TOPREAL4:1;
end;
end;
hence thesis by A8,A10,A11,A45;
end;
suppose
A66: front_left_cell(f,(len f)-'1,G) meets C;
thus thesis
proof per cases by A16;
suppose
A67: i1 = i2 & j1+1 = j2;
take f1 = f^<*G*(i2-'1,j2)*>;
now
take i=i2-'1 ,j=j2;
thus f1 turns_left (len f)-'1,G
proof let i1',j1',i2',j2' be Nat;
assume that
A68: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A69: 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 A22,A69,GROUP_5:95;
then A70: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A68,GOBOARD1:21;
per cases by A16,A70;
case i1' = i2' & j1'+1 = j2';
now assume i2-'1 < 1;
then i2-'1 = 0 by RLVECT_1:98;
then i2 <= 1 by JORDAN4:1;
then i2 = 1 by A18,AXIOMS:21;
then cell(G,1-'1,j2) meets C
by A11,A12,A13,A14,A15,A66,A67,GOBRD13:35;
then cell(G,0,j2) meets C by GOBOARD9:1;
hence contradiction by A2,A18,JORDAN8:21;
end;
hence [i2'-'1,j2'] in Indices G by A18,A21,A70,GOBOARD7:10;
thus f1/.((len f)-'1+2) = G*(i2'-'1,j2')
by A23,A70,TOPREAL4:1;
case i1'+1 = i2' & j1' = j2';
hence thesis by A67,A70,NAT_1:38;
case i1' = i2'+1 & j1' = j2';
hence thesis by A67,A70,NAT_1:38;
case
A71: i1' = i2' & j1' = j2'+1;
j1+1+1 = j1+(1+1) by XCMPLX_1:1;
hence thesis by A67,A70,A71,REAL_1:69;
end;
end;
hence thesis by A8,A10,A11,A66;
suppose
A72: i1+1 = i2 & j1 = j2;
take f1 = f^<*G*(i2,j2+1)*>;
now
take i=i2 ,j=j2+1;
thus f1 turns_left (len f)-'1,G
proof let i1',j1',i2',j2' be Nat;
assume that
A73: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A74: 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 A22,A74,GROUP_5:95;
then A75: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A73,GOBOARD1:21;
per cases by A16,A75;
case i1' = i2' & j1'+1 = j2';
hence thesis by A72,A75,NAT_1:38;
case i1'+1 = i2' & j1' = j2';
now assume j2+1 > len G;
then j2+1 <= (len G)+1 & (len G)+1 <= j2+1
by A2,A18,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,len G) meets C
by A11,A12,A13,A14,A15,A66,A72,GOBRD13:37;
hence contradiction by A18,JORDAN8:18;
end;
hence [i2',j2'+1] in Indices G by A2,A18,A20,A75,GOBOARD7:10
;
thus f1/.((len f)-'1+2) = G*(i2',j2'+1)
by A23,A75,TOPREAL4:1;
case
A76: i1' = i2'+1 & j1' = j2';
i1+1+1 = i1+(1+1) by XCMPLX_1:1;
hence thesis by A72,A75,A76,REAL_1:69;
case i1' = i2' & j1' = j2'+1;
hence thesis by A72,A75,NAT_1:38;
end;
end;
hence thesis by A8,A10,A11,A66;
suppose
A77: i1 = i2+1 & j1 = j2;
take f1 = f^<*G*(i2,j2-'1)*>;
now
take i=i2 ,j=j2-'1;
thus f1 turns_left (len f)-'1,G
proof let i1',j1',i2',j2' be Nat;
assume that
A78: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A79: 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 A22,A79,GROUP_5:95;
then A80: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A78,GOBOARD1:21;
per cases by A16,A80;
case i1' = i2' & j1'+1 = j2';
hence thesis by A77,A80,NAT_1:38;
case
A81: i1'+1 = i2' & j1' = j2';
i1+1+1 = i1+(1+1) by XCMPLX_1:1;
hence thesis by A77,A80,A81,REAL_1:69;
case i1' = i2'+1 & j1' = j2';
now assume j2-'1 < 1;
then j2-'1 = 0 by RLVECT_1:98;
then j2 <= 1 by JORDAN4:1;
then j2 = 1 by A18,AXIOMS:21;
then cell(G,i2-'1,1-'1) meets C
by A11,A12,A13,A14,A15,A66,A77,GOBRD13:39;
then cell(G,i2-'1,0) meets C by GOBOARD9:1;
hence contradiction by A21,JORDAN8:20;
end;
hence [i2',j2'-'1] in Indices G by A18,A21,A80,GOBOARD7:10;
thus f1/.((len f)-'1+2) = G*(i2',j2'-'1)
by A23,A80,TOPREAL4:1;
case i1' = i2' & j1' = j2'+1;
hence thesis by A77,A80,NAT_1:38;
end;
end;
hence thesis by A8,A10,A11,A66;
suppose
A82: i1 = i2 & j1 = j2+1;
take f1 = f^<*G*(i2+1,j2)*>;
now
take i=i2+1 ,j=j2;
thus f1 turns_left (len f)-'1,G
proof let i1',j1',i2',j2' be Nat;
assume that
A83: [i1',j1'] in Indices G & [i2',j2'] in Indices G and
A84: 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 A22,A84,GROUP_5:95;
then A85: i1 = i1' & j1 = j1' & i2 = i2' & j2 = j2'
by A14,A15,A83,GOBOARD1:21;
per cases by A16,A85;
case
A86: i1' = i2' & j1'+1 = j2';
j1+1+1 = j1+(1+1) by XCMPLX_1:1;
hence thesis by A82,A85,A86,REAL_1:69;
case i1'+1 = i2' & j1' = j2';
hence thesis by A82,A85,NAT_1:38;
case i1' = i2'+1 & j1' = j2';
hence thesis by A82,A85,NAT_1:38;
case i1' = i2' & j1' = j2'+1;
now assume i2+1 > len G;
then i2+1 <= (len G)+1 & (len G)+1 <= i2+1
by A18,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-'1) meets C
by A11,A12,A13,A14,A15,A66,A82,GOBRD13:41;
hence contradiction by A2,A21,JORDAN8:19;
end;
hence [i2'+1,j2'] in Indices G by A18,A20,A85,GOBOARD7:10;
thus f1/.((len f)-'1+2) = G*(i2'+1,j2')
by A23,A85,TOPREAL4:1;
end;
end;
hence thesis by A8,A10,A11,A66;
end;
end;
suppose
A87: not f is_sequence_on G or right_cell(f,len f-'1,G) misses C;
take f^<*G*(1,1)*>;
thus thesis by A8,A10,A87;
end;
suppose
A88: len f <> k;
take {};
thus thesis by A8,A88;
end;
suppose
A89: k > 1 & x is not FinSequence of TOP-REAL 2;
take {};
thus thesis by A89;
end;
consider F being Function such that
A90: dom F = NAT and
A91: F.0 = {} and
A92: 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;
A93: {} = <*>(the carrier of TOP-REAL 2);
then A94: P[0] by A91;
A95: for k st P[k] holds P[k+1]
proof let k such that
A96: F.k is FinSequence of TOP-REAL 2;
A97: P[k,F.k,F.(k+1)] by A92;
per cases by CQC_THE1:2;
suppose k = 0;
hence F.(k+1) is FinSequence of TOP-REAL 2 by A97;
suppose k = 1;
hence F.(k+1) is FinSequence of TOP-REAL 2 by A97;
suppose
A98: k > 1;
thus thesis
proof
reconsider f = F.k as FinSequence of TOP-REAL 2 by A96;
per cases;
suppose
A99: len f = k;
thus thesis
proof per cases;
suppose f is_sequence_on G & right_cell(f,len f-'1,G) meets C
;
then (front_left_cell(f,(len f)-'1,G) misses C &
front_right_cell(f,(len f)-'1,G) misses C
implies ex i,j st
f^<*G*(i,j)*> turns_right (len f)-'1,G &
F.(k+1) = f^<*G*(i,j)*>) &
(front_left_cell(f,(len f)-'1,G) misses C &
front_right_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_left_cell(f,(len f)-'1,G) meets C
implies ex i,j st
f^<*G*(i,j)*> turns_left (len f)-'1,G &
F.(k+1) = f^<*G*(i,j)*>) by A92,A98,A99;
hence F.(k+1) is FinSequence of TOP-REAL 2;
suppose
A100: not f is_sequence_on G or right_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 A92,A98,A99,A100;
end;
suppose len f <> k;
hence F.(k+1) is FinSequence of TOP-REAL 2 by A92,A93,A98;
end;
end;
A101: for k holds P[k] from Ind(A94,A95);
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 A90,A101;
hence thesis by FINSEQ_1:def 11;
end;
then reconsider F as Function of NAT,(the carrier of TOP-REAL 2)*
by A90,FUNCT_2:def 1,RELSET_1:11;
defpred P[Nat] means len(F.$1) = $1;
A102: P[0] by A91,FINSEQ_1:25;
A103: for k st P[k] holds P[k+1]
proof let k such that
A104: len(F.k) = k;
A105: P[k,F.k,F.(k+1)] by A92;
per cases by CQC_THE1:2;
suppose k = 0;
hence thesis by A105,FINSEQ_1:56;
suppose k = 1;
hence thesis by A105,FINSEQ_1:61;
suppose
A106: k > 1;
thus thesis
proof per cases;
suppose
F.k is_sequence_on G & right_cell(F.k,len(F.k)-'1,G) meets C;
then (front_left_cell(F.k,(len(F.k))-'1,G) misses C &
front_right_cell(F.k,(len(F.k))-'1,G) misses 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)*>) &
(front_left_cell(F.k,(len(F.k))-'1,G) misses C &
front_right_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_left_cell(F.k,(len(F.k))-'1,G) meets C
implies ex i,j st
(F.k)^<*G*(i,j)*> turns_left (len(F.k))-'1,G &
F.(k+1) = (F.k)^<*G*(i,j)*>) by A92,A104,A106;
hence thesis by A104,FINSEQ_2:19;
suppose
not F.k is_sequence_on G or right_cell(F.k,len(F.k)-'1,G) misses C;
then F.(k+1) = (F.k)^<*G*(1,1)*> by A92,A104,A106;
hence thesis by A104,FINSEQ_2:19;
end;
end;
A107: for k holds P[k] from Ind(A102,A103);
defpred P[Nat] means
F.$1 is_sequence_on G &
for m st 1 <= m & m+1 <= len(F.$1)
holds left_cell(F.$1,m,G) misses C & right_cell(F.$1,m,G) meets C;
A108:
P[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 A91,RELAT_1:60;
hence F.0 is_sequence_on G by GOBOARD1:def 11;
let m; assume
A109: 1 <= m & m+1 <= len(F.0);
1 <= m+1 by NAT_1:37;
then 1 <= len(F.0) by A109,AXIOMS:22;
then 1 <= 0 by A91,FINSEQ_1:25;
hence left_cell(F.0,m,G) misses C &
right_cell(F.0,m,G) meets C;
end;
A110: now let k such that
A111: F.k is_sequence_on G and
A112: for m st 1 <= m & m+1 <= len(F.k)
holds left_cell(F.k,m,G) misses C &
right_cell(F.k,m,G) meets C and
A113: k > 1;
let i1,j1,i2,j2 be Nat such that
A114: [i1,j1] in Indices G & (F.k)/.((len(F.k)) -'1) = G*(i1,j1) and
A115: [i2,j2] in Indices G & (F.k)/.len(F.k) = G*(i2,j2);
A116: len(F.k) = k by A107;
then A117: 1 <= (len(F.k))-'1 by A113,JORDAN3:12;
A118: (len(F.k)) -'1 +1 = len(F.k) by A113,A116,AMI_5:4;
then A119: left_cell(F.k,(len(F.k))-'1,G) misses C &
right_cell(F.k,(len(F.k))-'1,G) meets C by A112,A117;
A120: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A114,GOBOARD5:1;
A121: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A115,GOBOARD5:1;
A122: i1-'1 <= len G & j1-'1 <= width G by A120,JORDAN3:7;
A123: 1 <= i2+1 & 1 <= j2+1 by NAT_1:37;
A124: i2-'1 <= len G & j2-'1 <= width G by A121,JORDAN3:7;
hereby assume
A125: i1 = i2 & j1+1 = j2;
now assume i2+1 > len G;
then i2+1 <= (len G)+1 & (len G)+1 <= i2+1 by A121,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 A111,A114,A115,A117,A118,A119,A125,GOBRD13:23;
hence contradiction by A2,A120,JORDAN8:19;
end;
hence [i2+1,j2] in Indices G by A121,A123,GOBOARD7:10;
end;
hereby assume
A126: i1+1 = i2 & j1 = j2;
now assume j2-'1 < 1;
then j2-'1 = 0 by RLVECT_1:98;
then j2 <= 1 by JORDAN4:1;
then j2 = 1 by A121,AXIOMS:21;
then cell(G,i1,1-'1) meets C by A111,A114,A115,A117,A118,A119,A126,
GOBRD13:25;
then cell(G,i1,0) meets C by GOBOARD9:1;
hence contradiction by A120,JORDAN8:20;
end;
hence [i2,j2-'1] in Indices G by A121,A124,GOBOARD7:10;
end;
hereby assume
A127: i1 = i2+1 & j1 = j2;
now assume j2+1 > len G;
then j2+1 <= (len G)+1 & (len G)+1 <=
j2+1 by A2,A121,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,len G) meets C by A111,A114,A115,A117,A118,A119,A127,
GOBRD13:27;
hence contradiction by A121,JORDAN8:18;
end;
hence [i2,j2+1] in Indices G by A2,A121,A123,GOBOARD7:10;
end;
hereby assume
A128: i1 = i2 & j1 = j2+1;
now assume i2-'1 < 1;
then i2-'1 = 0 by RLVECT_1:98;
then i2 <= 1 by JORDAN4:1;
then i2 = 1 by A121,AXIOMS:21;
then cell(G,1-'1,j2) meets C by A111,A114,A115,A117,A118,A119,A128,
GOBRD13:29;
then cell(G,0,j2) meets C by GOBOARD9:1;
hence contradiction by A2,A121,JORDAN8:21;
end;
hence [i2-'1,j2] in Indices G by A121,A124,GOBOARD7:10;
end;
hereby assume that
A129: front_right_cell(F.k,(len(F.k))-'1,G) meets C and
A130: i1 = i2 & j1+1 = j2;
now assume j2+1 > len G;
then j2+1 <= (len G)+1 & (len G)+1 <=
j2+1 by A2,A121,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 A111,A114,A115,A117,A118,A129,A130,
GOBRD13:36;
hence contradiction by A120,JORDAN8:18;
end;
hence [i2,j2+1] in Indices G by A2,A121,A123,GOBOARD7:10;
end;
hereby assume that
A131: front_right_cell(F.k,(len(F.k))-'1,G) meets C and
A132: i1+1 = i2 & j1 = j2;
now assume i2+1 > len G;
then i2+1 <= (len G)+1 & (len G)+1 <= i2+1 by A121,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-'1) meets C
by A111,A114,A115,A117,A118,A131,A132,GOBRD13:38;
hence contradiction by A2,A122,JORDAN8:19;
end;
hence [i2+1,j2] in Indices G by A121,A123,GOBOARD7:10;
end;
hereby assume that
A133: front_right_cell(F.k,(len(F.k))-'1,G) meets C and
A134: i1 = i2+1 & j1 = j2;
now assume i2-'1 < 1;
then i2-'1 = 0 by RLVECT_1:98;
then i2 <= 1 by JORDAN4:1;
then i2 = 1 by A121,AXIOMS:21;
then cell(G,1-'1,j1) meets C by A111,A114,A115,A117,A118,A133,A134,
GOBRD13:40;
then cell(G,0,j1) meets C by GOBOARD9:1;
hence contradiction by A2,A120,JORDAN8:21;
end;
hence [i2-'1,j2] in Indices G by A121,A124,GOBOARD7:10;
end;
hereby assume that
A135: front_right_cell(F.k,(len(F.k))-'1,G) meets C and
A136: i1 = i2 & j1 = j2+1;
now assume j2-'1 < 1;
then j2-'1 = 0 by RLVECT_1:98;
then j2 <= 1 by JORDAN4:1;
then j2 = 1 by A121,AXIOMS:21;
then cell(G,i1-'1,1-'1) meets C
by A111,A114,A115,A117,A118,A135,A136,GOBRD13:42;
then cell(G,i1-'1,0) meets C by GOBOARD9:1;
hence contradiction by A122,JORDAN8:20;
end;
hence [i2,j2-'1] in Indices G by A121,A124,GOBOARD7:10;
end;
hereby assume that
A137: front_left_cell(F.k,(len(F.k))-'1,G) meets C and
A138: i1 = i2 & j1+1 = j2;
now assume i2-'1 < 1;
then i2-'1 = 0 by RLVECT_1:98;
then i2 <= 1 by JORDAN4:1;
then i2 = 1 by A121,AXIOMS:21;
then cell(G,1-'1,j2) meets C by A111,A114,A115,A117,A118,A137,A138,
GOBRD13:35;
then cell(G,0,j2) meets C by GOBOARD9:1;
hence contradiction by A2,A121,JORDAN8:21;
end;
hence [i2-'1,j2] in Indices G by A121,A124,GOBOARD7:10;
end;
hereby assume that
A139: front_left_cell(F.k,(len(F.k))-'1,G) meets C and
A140: i1+1 = i2 & j1 = j2;
now assume j2+1 > len G;
then j2+1 <= (len G)+1 & (len G)+1 <=
j2+1 by A2,A121,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,len G) meets C by A111,A114,A115,A117,A118,A139,A140,
GOBRD13:37;
hence contradiction by A121,JORDAN8:18;
end;
hence [i2,j2+1] in Indices G by A2,A121,A123,GOBOARD7:10;
end;
hereby assume that
A141: front_left_cell(F.k,(len(F.k))-'1,G) meets C and
A142: i1 = i2+1 & j1 = j2;
now assume j2-'1 < 1;
then j2-'1 = 0 by RLVECT_1:98;
then j2 <= 1 by JORDAN4:1;
then j2 = 1 by A121,AXIOMS:21;
then cell(G,i2-'1,1-'1) meets C
by A111,A114,A115,A117,A118,A141,A142,GOBRD13:39;
then cell(G,i2-'1,0) meets C by GOBOARD9:1;
hence contradiction by A124,JORDAN8:20;
end;
hence [i2,j2-'1] in Indices G by A121,A124,GOBOARD7:10;
end;
hereby assume that
A143: front_left_cell(F.k,(len(F.k))-'1,G) meets C and
A144: i1 = i2 & j1 = j2+1;
now assume i2+1 > len G;
then i2+1 <= (len G)+1 & (len G)+1 <= i2+1 by A121,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-'1) meets C
by A111,A114,A115,A117,A118,A143,A144,GOBRD13:41;
hence contradiction by A2,A124,JORDAN8:19;
end;
hence [i2+1,j2] in Indices G by A121,A123,GOBOARD7:10;
end;
end;
A145: for k st P[k] holds P[k+1]
proof let k such that
A146: F.k is_sequence_on G and
A147: for m st 1 <= m & m+1 <= len(F.k)
holds left_cell(F.k,m,G) misses C & right_cell(F.k,m,G) meets C;
A148: len(F.k) = k by A107;
A149: len(F.(k+1)) = k+1 by A107;
A150: 1 <= len G by A2,NAT_1:37;
A151: 2|^n > 0 by HEINE:5;
per cases by CQC_THE1:2;
suppose
A152: k = 0; then consider i such that
A153: 1 <= i & i+1 <= len G and
N-min C in cell(G,i,width G-'1) & N-min C <> G*(i,width G-'1) and
A154: F.(k+1) = <*G*(i,width G)*> by A92;
i < len G by A153,NAT_1:38;
then A155: [i,len G] in Indices G by A2,A150,A153,GOBOARD7:10;
A156: now let l;
assume l in dom(F.(k+1));
then 1 <= l & l <= 1 by A149,A152,FINSEQ_3:27;
then l = 1 by AXIOMS:21;
then (F.(k+1))/.l = G*(i,width G) by A154,FINSEQ_4:25;
hence ex i,j st [i,j] in Indices G & (F.(k+1))/.l = G*
(i,j) by A2,A155;
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 A149,A152,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 A156,GOBOARD1:def 11;
let m;
assume
A157: 1 <= m & m+1 <= len(F.(k+1));
1 <= m+1 by NAT_1:37;
then m+1 = 0+1 by A149,A152,A157,AXIOMS:21;
then m = 0 by XCMPLX_1:2;
hence left_cell(F.(k+1),m,G) misses C &
right_cell(F.(k+1),m,G) meets C by A157;
suppose
A158: k = 1; then consider i such that
A159: 1 <= i & i+1 <= len G and
A160: N-min C in cell(G,i,width G-'1) & N-min C <> G*(i,width G-'1) and
A161: F.(k+1) = <*G*(i,width G),G*(i+1,width G)*> by A92;
A162: (F.(k+1))/.1 = G*(i,width G) & (F.(k+1))/.2 = G*(i+1,width G)
by A161,FINSEQ_4:26;
A163: i < len G & 1 <= i+1 & i+1 <= len G by A159,NAT_1:38;
then A164: [i,len G] in Indices G & [i+1,len G] in Indices G
by A2,A150,A159,GOBOARD7:10;
A165: now let l;
assume A166: l in dom(F.(k+1));
then 1 <= l & l <= 2 by A149,A158,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 A2,A162,A164,A166,FINSEQ_3:27;
end;
now let l;
assume A167: 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 A149,A158,FINSEQ_3:27;
then A168: l = 0 or l = 1 or l = 2 by CQC_THE1:3;
let i1,j1,i2,j2 such that
A169: [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);
i1 = i & j1 = len G & i2 = i+1 & j2 = len G
by A2,A149,A158,A162,A164,A167,A168,A169,FINSEQ_3:27,GOBOARD1:21;
then i2-i1 = 1 & j1-j2 = 0 by XCMPLX_1:14,26;
then abs(i2-i1) = 1 & abs(j1-j2) = 0 by ABSVALUE:def 1;
hence abs(i1-i2)+abs(j1-j2) = 1 by UNIFORM1:13;
end;
hence
A170: F.(k+1) is_sequence_on G by A165,GOBOARD1:def 11;
let m;
assume
A171: 1 <= m & m+1 <= len(F.(k+1));
then 1+1 <= m+1 by AXIOMS:24;
then m+1 = 1+1 by A149,A158,A171,AXIOMS:21;
then A172: m = 1 by XCMPLX_1:2;
A173: i < i+1 & i+1 < (i+1)+1 by NAT_1:38;
then A174: left_cell(F.(k+1),m,G) = cell(G,i,len G)
by A2,A162,A164,A170,A171,A172,GOBRD13:def 3;
now assume left_cell(F.(k+1),m,G) meets C;
then consider p being set such that
A175: p in cell(G,i,len G) & p in C by A174,XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A175;
reconsider p as Element of TOP-REAL 2;
cell(G,i,len G) = { |[r,s]|: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 &
G*(1,len G)`2 <= s }
by A2,A159,A163,GOBRD11:31;
then consider r,s such that
A176: p = |[r,s]| and
G*(i,1)`1 <= r & r <= G*(i+1,1)`1 and
A177: G*(1,len G)`2 <= s by A175;
[1,len G] in Indices G by A2,A150,GOBOARD7:10;
then A178: G*
(1,len G) = |[W+((E-W)/(2|^n))*(1-2),S+((N-S)/(2|^n))*((len G)-2)]|
by JORDAN8:def 1;
2|^n+(2+1) = 2|^n+1+2 by XCMPLX_1:1;
then (len G) - 2 = 2|^n+1 by A2,XCMPLX_1:26;
then ((N-S)/(2|^n))*((len G)-2)
= ((N-S)/(2|^n))*(2|^n)+((N-S)/(2|^n))*1 by XCMPLX_1:8
.= (N-S)+(N-S)/(2|^n) by A151,XCMPLX_1:88;
then A179: S+((N-S)/(2|^n))*((len G) -2)
= S+(N-S)+(N-S)/(2|^n) by XCMPLX_1:1
.= N+(N-S)/(2|^n) by XCMPLX_1:27;
A180: G*(1,len G)`2 = S+((N-S)/(2|^n))*((len G)-2) by A178,EUCLID:56;
N > S by JORDAN8:12;
then N-S > S-S by REAL_1:54;
then N-S > 0 by XCMPLX_1:14;
then (N-S)/(2|^n) > 0 by A151,REAL_2:127;
then N+0 < N+(N-S)/(2|^n) by REAL_1:53;
then A181: N < s by A177,A179,A180,AXIOMS:22;
p`2 <= N by A175,PSCOMP_1:71;
hence contradiction by A176,A181,EUCLID:56;
end;
hence left_cell(F.(k+1),m,G) misses C;
A182: N-min C in C by SPRECT_1:13;
N-min C in right_cell(F.(k+1),m,G)
by A2,A160,A162,A164,A170,A171,A172,A173,GOBRD13:def 2;
hence right_cell(F.(k+1),m,G) meets C by A182,XBOOLE_0:3;
suppose
A183: k > 1;
then k > 0 by AXIOMS:22;
then A184: F.k is non empty by A148,FINSEQ_1:25;
A185: 1 <= (len(F.k))-'1 by A148,A183,JORDAN3:12;
A186: (len(F.k)) -'1 +1 = len(F.k) by A148,A183,AMI_5:4;
then consider i1,j1,i2,j2 being Nat such that
A187: [i1,j1] in Indices G & (F.k)/.((len(F.k)) -'1) = G*(i1,j1) and
A188: [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 A146,A185,JORDAN8:6;
A189: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A188,GOBOARD5:1;
(len(F.k))-'1 <= len(F.k) by GOBOARD9:2;
then A190: (len(F.k))-'1 in dom(F.k) & len(F.k) in dom(F.k)
by A148,A183,A185,FINSEQ_3:27;
A191: (len(F.k))-'1+(1+1) = (len(F.k))+1 by A186,XCMPLX_1:1;
A192: left_cell(F.k,(len(F.k))-'1,G) misses C &
right_cell(F.k,(len(F.k))-'1,G) meets C by A147,A185,A186;
A193: i1 = i2 & j1+1 = j2 implies [i2+1,j2] in Indices G by A110,A146,A147,A183
,A187,A188;
A194: i1+1 = i2 & j1 = j2 implies [i2,j2-'1] in Indices G by A110,A146,A147,
A183,A187,A188;
A195: i1 = i2+1 & j1 = j2 implies [i2,j2+1] in Indices G by A110,A146,A147,A183
,A187,A188;
A196: i1 = i2 & j1 = j2+1 implies [i2-'1,j2] in Indices G by A110,A146,A147,
A183,A187,A188;
A197: front_right_cell(F.k,(len(F.k))-'1,G) meets C &
i1 = i2 & j1+1 = j2 implies [i2,j2+1] in Indices G by A110,A146,A147,A183,
A187,A188;
A198: front_right_cell(F.k,(len(F.k))-'1,G) meets C &
i1+1 = i2 & j1 = j2 implies [i2+1,j2] in Indices G by A110,A146,A147,A183,
A187,A188;
A199: front_right_cell(F.k,(len(F.k))-'1,G) meets C &
i1 = i2+1 & j1 = j2 implies [i2-'1,j2] in Indices G by A110,A146,A147,A183
,A187,A188;
A200: front_right_cell(F.k,(len(F.k))-'1,G) meets C &
i1 = i2 & j1 = j2+1 implies [i2,j2-'1] in Indices G by A110,A146,A147,A183
,A187,A188;
A201: front_left_cell(F.k,(len(F.k))-'1,G) meets C &
i1 = i2 & j1+1 = j2 implies [i2-'1,j2] in Indices G by A110,A146,A147,A183
,A187,A188;
A202: front_left_cell(F.k,(len(F.k))-'1,G) meets C &
i1+1 = i2 & j1 = j2 implies [i2,j2+1] in Indices G by A110,A146,A147,A183,
A187,A188;
A203: front_left_cell(F.k,(len(F.k))-'1,G) meets C &
i1 = i2+1 & j1 = j2 implies [i2,j2-'1] in Indices G by A110,A146,A147,A183
,A187,A188;
A204: front_left_cell(F.k,(len(F.k))-'1,G) meets C &
i1 = i2 & j1 = j2+1 implies [i2+1,j2] in Indices G by A110,A146,A147,A183,
A187,A188;
thus
A205: F.(k+1) is_sequence_on G
proof
per cases;
suppose front_left_cell(F.k,(len(F.k))-'1,G) misses C &
front_right_cell(F.k,(len(F.k))-'1,G) misses C;
then consider i,j such that
A206: (F.k)^<*G*(i,j)*> turns_right (len(F.k))-'1,G and
A207: F.(k+1) = (F.k)^<*G*(i,j)*> by A92,A146,A148,A183,A192;
thus thesis
proof set f = (F.k)^<*G*(i,j)*>;
A208: f/.(len(F.k)-'1) = G*(i1,j1) & f/.len(F.k) = G*(i2,j2)
by A187,A188,A190,GROUP_5:95;
A209: f/.(len(F.k)+1) = G*(i,j) by TOPREAL4:1;
per cases by A186,A187,A188,A191,A206,A208,GOBRD13:def 6;
suppose that
A210: i1 = i2 & j1+1 = j2 and
A211: 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 A188,A193,A210,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 A146,A184,A193,A207,A209,A210,A211
,JORDAN8:9;
suppose that
A212: i1+1 = i2 & j1 = j2 and
A213: 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 A214: i2 = i1' & j2 = j1' & i2 = i2' & j2-'1 = j2'
by A188,A194,A212,GOBOARD1:21;
then j1'-j2' = j2-(j2-1) by A189,SCMFSA_7:3;
then i2'-i1' = 0 & j1'-j2' = 1 by A214,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 A146,A184,A194,A207,A209,A212,A213
,JORDAN8:9;
suppose that
A215: i1 = i2+1 & j1 = j2 and
A216: 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 A188,A195,A215,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 A146,A184,A195,A207,A209,A215,A216
,JORDAN8:9;
suppose that
A217: i1 = i2 & j1 = j2+1 and
A218: 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 A219: i2 = i1' & j2 = j1' & i2-'1 = i2' & j2 = j2'
by A188,A196,A217,GOBOARD1:21;
then i1'-i2' = i2-(i2-1) by A189,SCMFSA_7:3;
then j2'-j1' = 0 & i1'-i2' = 1 by A219,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 A146,A184,A196,A207,A209,A217,A218
,JORDAN8:9;
end;
suppose
A220: front_left_cell(F.k,(len(F.k))-'1,G) misses C &
front_right_cell(F.k,(len(F.k))-'1,G) meets C;
then consider i,j such that
A221: (F.k)^<*G*(i,j)*> goes_straight (len(F.k))-'1,G and
A222: F.(k+1) = (F.k)^<*G*(i,j)*> by A92,A146,A148,A183,A192;
thus thesis
proof set f = (F.k)^<*G*(i,j)*>;
A223: f/.(len(F.k)-'1) = G*(i1,j1) & f/.len(F.k) = G*(i2,j2)
by A187,A188,A190,GROUP_5:95;
A224: f/.(len(F.k)+1) = G*(i,j) by TOPREAL4:1;
per cases by A186,A187,A188,A191,A221,A223,GOBRD13:def 8;
suppose that
A225: i1 = i2 & j1+1 = j2 and
A226: 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 A188,A197,A220,A225,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 A146,A184,A197,A220,A222,A224,A225,
A226,JORDAN8:9;
suppose that
A227: i1+1 = i2 & j1 = j2 and
A228: 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 A188,A198,A220,A227,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 A146,A184,A198,A220,A222,A224,A227,
A228,JORDAN8:9;
suppose that
A229: i1 = i2+1 & j1 = j2 and
A230: 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 A231: i2 = i1' & j2 = j1' & i2-'1 = i2' & j2 = j2'
by A188,A199,A220,A229,GOBOARD1:21;
then i1'-i2' = i2-(i2-1) by A189,SCMFSA_7:3;
then j2'-j1' = 0 & i1'-i2' = 1 by A231,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 A146,A184,A199,A220,A222,A224,A229,
A230,JORDAN8:9;
suppose that
A232: i1 = i2 & j1 = j2+1 and
A233: 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 A234: i2 = i1' & j2 = j1' & i2 = i2' & j2-'1 = j2'
by A188,A200,A220,A232,GOBOARD1:21;
then j1'-j2' = j2-(j2-1) by A189,SCMFSA_7:3;
then i2'-i1' = 0 & j1'-j2' = 1 by A234,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 A146,A184,A200,A220,A222,A224,A232,
A233,JORDAN8:9;
end;
suppose
A235: front_left_cell(F.k,(len(F.k))-'1,G) meets C;
then consider i,j such that
A236: (F.k)^<*G*(i,j)*> turns_left (len(F.k))-'1,G and
A237: F.(k+1) = (F.k)^<*G*(i,j)*> by A92,A146,A148,A183,A192;
thus thesis
proof set f = (F.k)^<*G*(i,j)*>;
A238: f/.(len(F.k)-'1) = G*(i1,j1) & f/.len(F.k) = G*(i2,j2)
by A187,A188,A190,GROUP_5:95;
A239: f/.(len(F.k)+1) = G*(i,j) by TOPREAL4:1;
per cases by A186,A187,A188,A191,A236,A238,GOBRD13:def 7;
suppose that
A240: i1 = i2 & j1+1 = j2 and
A241: 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 A242: i2 = i1' & j2 = j1' & i2-'1 = i2' & j2 = j2'
by A188,A201,A235,A240,GOBOARD1:21;
then i1'-i2' = i2-(i2-1) by A189,SCMFSA_7:3;
then j2'-j1' = 0 & i1'-i2' = 1 by A242,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 A146,A184,A201,A235,A237,A239,A240,
A241,JORDAN8:9;
suppose that
A243: i1+1 = i2 & j1 = j2 and
A244: 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 A188,A202,A235,A243,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 A146,A184,A202,A235,A237,A239,A243,
A244,JORDAN8:9;
suppose that
A245: i1 = i2+1 & j1 = j2 and
A246: 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 A247: i2 = i1' & j2 = j1' & i2 = i2' & j2-'1 = j2'
by A188,A203,A235,A245,GOBOARD1:21;
then j1'-j2' = j2-(j2-1) by A189,SCMFSA_7:3;
then i2'-i1' = 0 & j1'-j2' = 1 by A247,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 A146,A184,A203,A235,A237,A239,A245,
A246,JORDAN8:9;
suppose that
A248: i1 = i2 & j1 = j2+1 and
A249: 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 A188,A204,A235,A248,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 A146,A184,A204,A235,A237,A239,A248,
A249,JORDAN8:9;
end;
end;
let m such that
A250: 1 <= m & m+1 <= len(F.(k+1));
now
per cases;
suppose m+1 = len(F.(k+1));
then A251: m = len(F.k) by A148,A149,XCMPLX_1:2;
A252: (i2-'1)+1 = i2 by A189,AMI_5:4;
A253: (j2-'1)+1 = j2 by A189,AMI_5:4;
thus thesis
proof per cases;
suppose
A254: front_left_cell(F.k,(len(F.k))-'1,G) misses C &
front_right_cell(F.k,(len(F.k))-'1,G) misses C;
then consider i,j such that
A255: (F.k)^<*G*(i,j)*> turns_right (len(F.k))-'1,G and
A256: F.(k+1) = (F.k)^<*G*(i,j)*> by A92,A146,A148,A183,A192;
A257: (F.(k+1))/.(len(F.k)-'1) = G*(i1,j1) & (F.(k+1))/.len(F.k) = G*
(i2,j2)
by A187,A188,A190,A256,GROUP_5:95;
now per cases by A186,A187,A188,A191,A255,A256,A257,GOBRD13:def 6;
suppose that
A258: i1 = i2 & j1+1 = j2 and
A259: (F.(k+1))/.((len(F.k))+1) = G*(i2+1,j2);
front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i1,j2)
by A146,A185,A186,A187,A188,A258,GOBRD13:36;
hence left_cell(F.(k+1),m,G) misses C
by A188,A193,A205,A250,A251,A254,A257,A258,A259,GOBRD13:24;
j2-'1 = j1 & cell(G,i1,j1) meets C
by A146,A185,A186,A187,A188,A192,A258,BINARITH:39,GOBRD13:23;
hence right_cell(F.(k+1),m,G) meets C
by A188,A193,A205,A250,A251,A257,A258,A259,GOBRD13:25;
suppose that
A260: i1+1 = i2 & j1 = j2 and
A261: (F.(k+1))/.((len(F.k))+1) = G*(i2,j2-'1);
front_right_cell(F.k,(len(F.k))-'1,G) = cell(G,i2,j2-'1)
by A146,A185,A186,A187,A188,A260,GOBRD13:38;
hence left_cell(F.(k+1),m,G) misses C
by A188,A194,A205,A250,A251,A253,A254,A257,A260,A261,GOBRD13:28;
i2-'1 = i1 & cell(G,i1,j1-'1) meets C
by A146,A185,A186,A187,A188,A192,A260,BINARITH:39,GOBRD13:25;
hence right_cell(F.(k+1),m,G) meets C
by A188,A194,A205,A250,A251,A253,A257,A260,A261,GOBRD13:29;
suppose that
A262: i1 = i2+1 & j1 = j2 and
A263: (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)
by A146,A185,A186,A187,A188,A262,GOBRD13:40;
hence left_cell(F.(k+1),m,G) misses C
by A188,A195,A205,A250,A251,A254,A257,A262,A263,GOBRD13:22;
cell(G,i2,j2) meets C
by A146,A185,A186,A187,A188,A192,A262,GOBRD13:27;
hence right_cell(F.(k+1),m,G) meets C
by A188,A195,A205,A250,A251,A257,A262,A263,GOBRD13:23;
suppose that
A264: i1 = i2 & j1 = j2+1 and
A265: (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-'1)
by A146,A185,A186,A187,A188,A264,GOBRD13:42;
hence left_cell(F.(k+1),m,G) misses C
by A188,A196,A205,A250,A251,A252,A254,A257,A264,A265,GOBRD13:26;
cell(G,i2-'1,j2) meets C
by A146,A185,A186,A187,A188,A192,A264,GOBRD13:29;
hence right_cell(F.(k+1),m,G) meets C
by A188,A196,A205,A250,A251,A252,A257,A264,A265,GOBRD13:27;
end;
hence thesis;
suppose
A266: front_left_cell(F.k,(len(F.k))-'1,G) misses C &
front_right_cell(F.k,(len(F.k))-'1,G) meets C;
then consider i,j such that
A267: (F.k)^<*G*(i,j)*> goes_