:: Decomposing a Go Board into Cells
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received May 26, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, PRE_TOPC, EUCLID, SUBSET_1, REAL_1, MATRIX_1, NAT_1,
RELAT_1, MCART_1, XXREAL_0, ARYTM_3, FINSEQ_1, TARSKI, STRUCT_0, TREES_1,
GOBOARD1, FUNCT_1, PARTFUN1, INCSP_1, ORDINAL2, CARD_1, XBOOLE_0,
RLTOPSP1, GOBOARD2, TOPREAL1, FINSEQ_6, ORDINAL4, ZFMISC_1, COMPLEX1,
ARYTM_1, GOBOARD5, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, ZFMISC_1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1,
PARTFUN1, FINSEQ_1, FINSEQ_4, MATRIX_0, MATRIX_1, SEQM_3, SEQ_4,
STRUCT_0, PRE_TOPC, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2,
FINSEQ_6, XXREAL_0;
constructors PARTFUN1, ENUMSET1, XXREAL_0, NAT_1, COMPLEX1, FINSEQ_4, NAT_D,
FINSEQ_6, MATRIX_1, TOPREAL1, GOBOARD2, GOBOARD1, SEQM_3, RELSET_1,
REAL_1, SEQ_4, RVSUM_1;
registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID,
GOBOARD2, VALUED_0, SEQ_4, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, TOPREAL1, GOBOARD1, FINSEQ_6, XBOOLE_0, SEQM_3;
equalities XBOOLE_0;
expansions GOBOARD1, XBOOLE_0, SEQM_3;
theorems GOBOARD1, FINSEQ_1, TOPREAL3, FINSEQ_4, FINSEQ_3, TOPREAL1, EUCLID,
NAT_1, ENUMSET1, CARD_2, TARSKI, GOBOARD2, MCART_1, ZFMISC_1, ABSVALUE,
MATRIX_0, SPPOL_2, FUNCT_1, FINSEQ_2, XBOOLE_0, XBOOLE_1, XREAL_1,
XXREAL_0, PARTFUN1, SEQM_3, NAT_D, SEQ_4, XTUPLE_0, XREAL_0;
begin
reserve p,q for Point of TOP-REAL 2,
i,i1,i2,j,j1,j2,k for Nat,
r,s for Real,
G for Matrix of TOP-REAL 2;
definition
let G be Matrix of TOP-REAL 2;
let i be Nat;
func v_strip(G,i) -> Subset of TOP-REAL 2 equals
:Def1:
{ |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 } if 1 <= i & i < len G,
{ |[r,s]| : G*(i,1)`1 <= r } if i >= len G
otherwise { |[r,s]| : r <= G*(i+1,1)`1 };
coherence
proof
hereby
assume that 1 <= i and i < len G;
set A = { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 };
A c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in A;
then ex r,s st x =|[r,s]| & G*(i,1)`1 <= r & r <= G*(i+1,1)`1;
hence thesis;
end;
hence A is Subset of TOP-REAL 2;
end;
hereby
assume i >= len G;
set A = { |[r,s]| : G*(i,1)`1 <= r };
A c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in A;
then ex r,s st x =|[r,s]| & G*(i,1)`1 <= r;
hence thesis;
end;
hence A is Subset of TOP-REAL 2;
end;
assume that not(1 <= i & i < len G) and i < len G;
set A = { |[r,s]| : r <= G*(i+1,1)`1 };
A c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in A;
then ex r,s st x =|[r,s]| & r <= G*(i+1,1)`1;
hence thesis;
end;
hence thesis;
end;
correctness;
func h_strip(G,i) -> Subset of TOP-REAL 2 equals
:Def2:
{ |[r,s]| : G*(1,i)`2 <= s & s <= G*(1,i+1)`2 } if 1 <= i & i < width G,
{ |[r,s]| : G*(1,i)`2 <= s } if i >= width G
otherwise { |[r,s]| : s <= G*(1,i+1)`2 };
coherence
proof
hereby
assume that 1 <= i and i < width G;
set A = { |[r,s]| : G*(1,i)`2 <= s & s <= G*(1,i+1)`2 };
A c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in A;
then ex r,s st x =|[r,s]| & G*(1,i)`2 <= s & s <= G*(1,i+1)`2;
hence thesis;
end;
hence A is Subset of TOP-REAL 2;
end;
hereby
assume i >= width G;
set A = { |[r,s]| : G*(1,i)`2 <= s };
A c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in A;
then ex r,s st x =|[r,s]| & G*(1,i)`2 <= s;
hence thesis;
end;
hence A is Subset of TOP-REAL 2;
end;
assume that not(1 <= i & i < width G) and i < width G;
set A = { |[r,s]| : s <= G*(1,i+1)`2 };
A c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in A;
then ex r,s st x =|[r,s]| & s <= G*(1,i+1)`2;
hence thesis;
end;
hence thesis;
end;
correctness;
end;
theorem Th1:
G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G
implies G*(i,j)`2 = G*(1,j)`2
proof
assume that
A1: G is Y_equal-in-column and
A2: 1 <= j and
A3: j <= width G and
A4: 1 <= i and
A5: i <= len G;
j in Seg width G by A2,A3,FINSEQ_1:1;
then
A6: Y_axis(Col(G,j)) is constant by A1;
reconsider c = Col(G,j) as FinSequence of TOP-REAL 2;
A7: i in dom G by A4,A5,FINSEQ_3:25;
A8: 1 <= len G by A4,A5,XXREAL_0:2;
then
A9: 1 in dom G by FINSEQ_3:25;
A10: len c = len G by MATRIX_0:def 8;
then 1 in dom c by A8,FINSEQ_3:25;
then
A11: c/.1 = c.1 by PARTFUN1:def 6;
i in dom c by A4,A5,A10,FINSEQ_3:25;
then
A12: c/.i = c.i by PARTFUN1:def 6;
A13: len(Y_axis Col(G,j)) = len c by GOBOARD1:def 2;
then
A14: 1 in dom(Y_axis Col(G,j)) by A8,A10,FINSEQ_3:25;
A15: i in dom(Y_axis Col(G,j)) by A4,A5,A10,A13,FINSEQ_3:25;
thus G*(i,j)`2 = (c/.i)`2 by A7,A12,MATRIX_0:def 8
.= (Y_axis Col(G,j)).i by A15,GOBOARD1:def 2
.= (Y_axis Col(G,j)).1 by A6,A14,A15
.= (c/.1)`2 by A14,GOBOARD1:def 2
.= G*(1,j)`2 by A9,A11,MATRIX_0:def 8;
end;
theorem Th2:
G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G
implies G*(i,j)`1 = G*(i,1)`1
proof
assume that
A1: G is X_equal-in-line and
A2: 1 <= j and
A3: j <= width G and
A4: 1 <= i and
A5: i <= len G;
i in dom G by A4,A5,FINSEQ_3:25;
then
A6: X_axis(Line(G,i)) is constant by A1;
reconsider c = Line(G,i) as FinSequence of TOP-REAL 2;
A7: j in Seg width G by A2,A3,FINSEQ_1:1;
A8: 1 <= width G by A2,A3,XXREAL_0:2;
then
A9: 1 in Seg width G by FINSEQ_1:1;
A10: len c = width G by MATRIX_0:def 7;
then 1 in dom c by A8,FINSEQ_3:25;
then
A11: c/.1 = c.1 by PARTFUN1:def 6;
j in dom c by A2,A3,A10,FINSEQ_3:25;
then
A12: c/.j = c.j by PARTFUN1:def 6;
A13: len(X_axis Line(G,i)) = len c by GOBOARD1:def 1;
then
A14: 1 in dom(X_axis Line(G,i)) by A8,A10,FINSEQ_3:25;
A15: j in dom(X_axis Line(G,i)) by A2,A3,A10,A13,FINSEQ_3:25;
thus G*(i,j)`1 = (c/.j)`1 by A7,A12,MATRIX_0:def 7
.= (X_axis Line(G,i)).j by A15,GOBOARD1:def 1
.= (X_axis Line(G,i)).1 by A6,A14,A15
.= (c/.1)`1 by A14,GOBOARD1:def 1
.= G*(i,1)`1 by A9,A11,MATRIX_0:def 7;
end;
theorem Th3:
G is X_increasing-in-column &
1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G
implies G*(i1,j)`1 < G*(i2,j)`1
proof
assume that
A1: G is X_increasing-in-column and
A2: 1 <= j and
A3: j <= width G and
A4: 1 <= i1 and
A5: i1 < i2 and
A6: i2 <= len G;
j in Seg width G by A2,A3,FINSEQ_1:1;
then
A7: X_axis(Col(G,j)) is increasing by A1;
reconsider c = Col(G,j) as FinSequence of TOP-REAL 2;
A8: i1 <= len G by A5,A6,XXREAL_0:2;
then
A9: i1 in dom G by A4,FINSEQ_3:25;
A10: 1 <= i2 by A4,A5,XXREAL_0:2;
then
A11: i2 in dom G by A6,FINSEQ_3:25;
A12: len c = len G by MATRIX_0:def 8;
then i1 in dom c by A4,A8,FINSEQ_3:25;
then
A13: c/.i1 = c.i1 by PARTFUN1:def 6;
i2 in dom c by A6,A10,A12,FINSEQ_3:25;
then
A14: c/.i2 = c.i2 by PARTFUN1:def 6;
A15: len(X_axis Col(G,j)) = len c by GOBOARD1:def 1;
then
A16: i1 in dom(X_axis Col(G,j)) by A4,A8,A12,FINSEQ_3:25;
A17: G*(i1,j)`1 = (c/.i1)`1 by A9,A13,MATRIX_0:def 8
.= (X_axis Col(G,j)).i1 by A16,GOBOARD1:def 1;
A18: i2 in dom(X_axis Col(G,j)) by A6,A10,A12,A15,FINSEQ_3:25;
then (X_axis Col(G,j)).i2 = (c/.i2)`1 by GOBOARD1:def 1
.= G*(i2,j)`1 by A11,A14,MATRIX_0:def 8;
hence thesis by A5,A7,A16,A17,A18;
end;
theorem Th4:
G is Y_increasing-in-line &
1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G
implies G*(i,j1)`2 < G*(i,j2)`2
proof
assume that
A1: G is Y_increasing-in-line and
A2: 1 <= j1 and
A3: j1 < j2 and
A4: j2 <= width G and
A5: 1 <= i and
A6: i <= len G;
i in dom G by A5,A6,FINSEQ_3:25;
then
A7: Y_axis(Line(G,i)) is increasing by A1;
reconsider c = Line(G,i) as FinSequence of TOP-REAL 2;
A8: j1 <= width G by A3,A4,XXREAL_0:2;
then
A9: j1 in Seg width G by A2,FINSEQ_1:1;
A10: 1 <= j2 by A2,A3,XXREAL_0:2;
then
A11: j2 in Seg width G by A4,FINSEQ_1:1;
A12: len c = width G by MATRIX_0:def 7;
then j1 in dom c by A2,A8,FINSEQ_3:25;
then
A13: c/.j1 = c.j1 by PARTFUN1:def 6;
j2 in dom c by A4,A10,A12,FINSEQ_3:25;
then
A14: c/.j2 = c.j2 by PARTFUN1:def 6;
A15: len Y_axis Line(G,i) = len c by GOBOARD1:def 2;
then
A16: j1 in dom(Y_axis Line(G,i)) by A2,A8,A12,FINSEQ_3:25;
A17: G*(i,j1)`2 = (c/.j1)`2 by A9,A13,MATRIX_0:def 7
.= (Y_axis Line(G,i)).j1 by A16,GOBOARD1:def 2;
A18: j2 in dom(Y_axis Line(G,i)) by A4,A10,A12,A15,FINSEQ_3:25;
then (Y_axis Line(G,i)).j2 = (c/.j2)`2 by GOBOARD1:def 2
.= G*(i,j2)`2 by A11,A14,MATRIX_0:def 7;
hence thesis by A3,A7,A16,A17,A18;
end;
theorem Th5:
G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G
implies h_strip(G,j) = { |[r,s]| : G*(i,j)`2 <= s & s <= G*(i,j+1)`2 }
proof
assume that
A1: G is Y_equal-in-column and
A2: 1 <= j and
A3: j < width G and
A4: 1 <= i and
A5: i <= len G;
A6: 1 <= j+1 by A2,NAT_1:13;
A7: j+1 <= width G by A3,NAT_1:13;
A8: G*(i,j)`2 = G*(1,j)`2 by A1,A2,A3,A4,A5,Th1;
G*(i,j+1)`2 = G*(1,j+1)`2 by A1,A4,A5,A6,A7,Th1;
hence thesis by A2,A3,A8,Def2;
end;
theorem Th6:
G is non empty-yielding Y_equal-in-column & 1 <= i & i <= len G
implies h_strip(G,width G) = { |[r,s]| : G*(i,width G)`2 <= s }
proof
assume that
A1: G is non empty-yielding Y_equal-in-column and
A2: 1 <= i and
A3: i <= len G;
width G <> 0 by A1,MATRIX_0:def 10;
then 1 <= width G by NAT_1:14;
then G*(i,width G)`2 = G*(1,width G)`2 by A1,A2,A3,Th1;
hence thesis by Def2;
end;
theorem Th7:
G is non empty-yielding Y_equal-in-column & 1 <= i & i <= len G
implies h_strip(G,0) = { |[r,s]| : s <= G*(i,1)`2 }
proof
assume that
A1: G is non empty-yielding Y_equal-in-column and
A2: 1 <= i and
A3: i <= len G;
set A = { |[r,s]| : G*(i,1)`2 >= s };
A4: 0 <> width G by A1,MATRIX_0:def 10;
then
A5: 0 < width G;
1 <= width G by A4,NAT_1:14;
then G*(i,1)`2 = G*(1,1)`2 by A1,A2,A3,Th1;
then A = { |[r,s]| : G*(1,1+0)`2 >= s };
hence thesis by A5,Def2;
end;
theorem Th8:
G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G
implies v_strip(G,i) = { |[r,s]| : G*(i,j)`1 <= r & r <= G*(i+1,j)`1 }
proof
assume that
A1: G is X_equal-in-line and
A2: 1 <= i and
A3: i < len G and
A4: 1 <= j and
A5: j <= width G;
A6: 1 <= i+1 by A2,NAT_1:13;
A7: i+1 <= len G by A3,NAT_1:13;
A8: G*(i,j)`1 = G*(i,1)`1 by A1,A2,A3,A4,A5,Th2;
G*(i+1,j)`1 = G*(i+1,1)`1 by A1,A4,A5,A6,A7,Th2;
hence thesis by A2,A3,A8,Def1;
end;
theorem Th9:
G is non empty-yielding X_equal-in-line & 1 <= j & j <= width G
implies v_strip(G,len G) = { |[r,s]| : G*(len G,j)`1 <= r }
proof
assume that
A1: G is non empty-yielding X_equal-in-line and
A2: 1 <= j and
A3: j <= width G;
len G <> 0 by A1,MATRIX_0:def 10;
then 1 <= len G by NAT_1:14;
then G*(len G,j)`1 = G*(len G,1)`1 by A1,A2,A3,Th2;
hence thesis by Def1;
end;
theorem Th10:
G is non empty-yielding X_equal-in-line & 1 <= j & j <= width G
implies v_strip(G,0) = { |[r,s]| : r <= G*(1,j)`1 }
proof
assume that
A1: G is non empty-yielding X_equal-in-line and
A2: 1 <= j and
A3: j <= width G;
set A = { |[r,s]| : G*(1,j)`1 >= r };
A4: 0 <> len G by A1,MATRIX_0:def 10;
then
A5: 0 < len G;
1 <= len G by A4,NAT_1:14;
then G*(1,j)`1 = G*(1,1)`1 by A1,A2,A3,Th2;
then A = { |[r,s]| : G*(1,1+0)`1 >= r };
hence thesis by A5,Def1;
end;
definition
let G be Matrix of TOP-REAL 2;
let i,j be Nat;
func cell(G,i,j) -> Subset of TOP-REAL 2 equals
v_strip(G,i) /\ h_strip(G,j);
correctness;
end;
definition
let IT be FinSequence of TOP-REAL 2;
attr IT is s.c.c. means
for i,j being Nat st i+1 < j & (i > 1 & j < len IT or j+1 < len IT)
holds LSeg(IT,i) misses LSeg(IT,j);
end;
definition
let IT be non empty FinSequence of TOP-REAL 2;
attr IT is standard means
:Def5:
IT is_sequence_on GoB IT;
end;
reconsider jj=1, zz=0 as Element of REAL by XREAL_0:def 1;
registration
cluster non constant special unfolded circular s.c.c.
standard for non empty FinSequence of TOP-REAL 2;
existence
proof
set f1 = <*|[ 0,0 ]|,|[ 0,1 ]|,|[ 1,1 ]|*>, f2 = <*|[ 1,0 ]|,|[ 0,0 ]|*>;
A1: len f1 = 3 by FINSEQ_1:45;
A2: len f2 = 2 by FINSEQ_1:44;
then
A3: len(f1^f2) = 3+2 by A1,FINSEQ_1:22;
reconsider f = f1^f2 as non empty FinSequence of TOP-REAL 2;
take f;
A4: 1 in dom f1 by A1,FINSEQ_3:25;
then
A5: f/.1 = f1/.1 by FINSEQ_4:68
.= |[ 0,0 ]| by FINSEQ_4:18;
A6: 2 in dom f1 by A1,FINSEQ_3:25;
then
A7: f/.2 = f1/.2 by FINSEQ_4:68
.= |[ 0,1 ]| by FINSEQ_4:18;
A8: dom f1 c= dom f by FINSEQ_1:26;
then
A9: f.1 = f/.1 by A4,PARTFUN1:def 6;
f.2 = f/.2 by A6,A8,PARTFUN1:def 6;
then f.1 <> f.2 by A5,A7,A9,SPPOL_2:1;
hence f is non constant by A4,A6,A8;
3 in dom f1 by A1,FINSEQ_3:25;
then
A10: f/.3 = f1/.3 by FINSEQ_4:68
.= |[ 1,1 ]| by FINSEQ_4:18;
1 in dom f2 by A2,FINSEQ_3:25;
then
A11: f/.(3+1) = f2/.1 by A1,FINSEQ_4:69
.= |[ 1,0 ]| by FINSEQ_4:17;
2 in dom f2 by A2,FINSEQ_3:25;
then
A12: f/.(3+2) = f2/.2 by A1,FINSEQ_4:69
.= |[ 0,0 ]| by FINSEQ_4:17;
1+1 = 2;
then
A13: LSeg(f,1) = LSeg(|[ 0,0 ]|,|[ 0,1 ]|) by A3,A5,A7,TOPREAL1:def 3;
2+1 = 3;
then
A14: LSeg(f,2) = LSeg(|[ 0,1 ]|,|[ 1,1 ]|) by A3,A7,A10,TOPREAL1:def 3;
A15: LSeg(f,3) = LSeg(|[ 1,1 ]|,|[ 1,0 ]|) by A3,A10,A11,TOPREAL1:def 3;
4+1 = 5;
then
A16: LSeg(f,4) = LSeg(|[ 1,0 ]|,|[ 0,0 ]|) by A3,A11,A12,TOPREAL1:def 3;
thus f is special
proof
let i be Nat;
assume 1 <= i;
then 1+1 <= i+1 by XREAL_1:6;
then
A17: 1 < i+1 by XXREAL_0:2;
assume i+1 <= len f;
then
A18: i+1 = 0 or ... or i+1 = 5 by A3;
per cases by A17,A18;
suppose
A19: i = 1;
(f/.1)`1 = 0 by A5,EUCLID:52
.= (f/.(1+1))`1 by A7,EUCLID:52;
hence thesis by A19;
end;
suppose
A20: i = 2;
(f/.2)`2 = 1 by A7,EUCLID:52
.= (f/.(2+1))`2 by A10,EUCLID:52;
hence thesis by A20;
end;
suppose
A21: i = 3;
(f/.3)`1 = 1 by A10,EUCLID:52
.= (f/.(3+1))`1 by A11,EUCLID:52;
hence thesis by A21;
end;
suppose
A22: i = 4;
(f/.4)`2 = 0 by A11,EUCLID:52
.= (f/.(4+1))`2 by A12,EUCLID:52;
hence thesis by A22;
end;
end;
thus f is unfolded
proof
let i be Nat;
assume 1 <= i;
then
1+2 <= i+2 by XREAL_1:6;
then
A23: 2 < i+2 by XXREAL_0:2;
assume i + 2 <= len f;
then
A24: i+2 = 0 or ... or i+2 = 5 by A3;
per cases by A23,A24;
suppose i = 1;
hence thesis by A3,A5,A7,A14,TOPREAL1:15,def 3;
end;
suppose i = 2;
hence thesis by A3,A7,A10,A15,TOPREAL1:18,def 3;
end;
suppose i = 3;
hence thesis by A3,A10,A11,A16,TOPREAL1:16,def 3;
end;
end;
thus
f/.1 = f/.len f by A1,A2,A5,A12,FINSEQ_1:22;
thus f is s.c.c.
proof
let i,j be Nat;
assume that
A25: i+1 < j and
A26: i > 1 & j < len f or j+1 < len f;
A27: i+1 >= 1 by NAT_1:11;
j+1 <= 5 by A3,A26,NAT_1:13;
then
A28: j+1 = 0 or ... or j+1 = 5;
A29: i+1+1 = i+(1+1);
then
A30: i+2 <= j by A25,NAT_1:13;
A31: i+2 <> 0+1 by A29;
A32: now per cases by A25,A27,A28;
case j = 2;
then i+2 = 0 or ... or i+2 = 2 by A30;
hence i = 0 by A25;
end;
case j = 3;
then i+2 = 0 or ... or i+2 = 3 by A30;
hence i = 0 or i = 1 by A25;
end;
case
A33: j = 4;
then i+2 = 0 or ... or i+2 = 4 by A30;
hence i = 0 or i = 2 by A3,A26,A31,A33;
end;
end;
per cases by A32;
suppose i = 0;
then LSeg(f,i) = {} by TOPREAL1:def 3;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
suppose i = 1 & j = 3;
hence LSeg(f,i) /\ LSeg(f,j) = {} by A13,A15,TOPREAL1:20;
end;
suppose i = 2 & j = 4;
hence LSeg(f,i) /\ LSeg(f,j) = {} by A14,A16,TOPREAL1:19;
end;
end;
set Xf1 = <*zz,zz,jj*>, Xf2 = <* jj,zz *>;
reconsider Xf = Xf1^Xf2 as FinSequence of REAL;
A34: len Xf1 = 3 by FINSEQ_1:45;
A35: len Xf2 = 2 by FINSEQ_1:44;
then
A36: len Xf = 3+2 by A34,FINSEQ_1:22;
1 in dom Xf1 by A34,FINSEQ_3:25;
then
A37: Xf.1 = Xf1.1 by FINSEQ_1:def 7
.= 0;
2 in dom Xf1 by A34,FINSEQ_3:25;
then
A38: Xf.2 = Xf1.2 by FINSEQ_1:def 7
.= 0;
3 in dom Xf1 by A34,FINSEQ_3:25;
then
A39: Xf.3 = Xf1.3 by FINSEQ_1:def 7
.= 1;
1 in dom Xf2 by A35,FINSEQ_3:25;
then
A40: Xf.(3+1) = Xf2.1 by A34,FINSEQ_1:def 7
.= 1;
2 in dom Xf2 by A35,FINSEQ_3:25;
then
A41: Xf.(3+2) = Xf2.2 by A34,FINSEQ_1:def 7
.= 0;
now
let n be Nat;
assume
A42: n in dom Xf;
then
A43: n <> 0 by FINSEQ_3:25;
n <= 5 by A36,A42,FINSEQ_3:25;
then n = 0 or ... or n = 5;
then per cases by A43;
suppose n = 1;
hence Xf.n = (f/.n)`1 by A5,A37,EUCLID:52;
end;
suppose n = 2;
hence Xf.n = (f/.n)`1 by A7,A38,EUCLID:52;
end;
suppose n = 3;
hence Xf.n = (f/.n)`1 by A10,A39,EUCLID:52;
end;
suppose n = 4;
hence Xf.n = (f/.n)`1 by A11,A40,EUCLID:52;
end;
suppose n = 5;
hence Xf.n = (f/.n)`1 by A12,A41,EUCLID:52;
end;
end;
then
A44: Xf = X_axis f by A3,A36,GOBOARD1:def 1;
A45: rng Xf1 = { 0,0,1 } by FINSEQ_2:128
.= { 0,1 } by ENUMSET1:30;
rng Xf2 = { 0,1 } by FINSEQ_2:127;
then
A46: rng Xf = { 0,1 } \/ { 0,1 } by A45,FINSEQ_1:31
.= { 0,1 };
then
A47: rng <*zz,jj*> = rng Xf by FINSEQ_2:127;
A48: len <*zz,jj*> = 2 by FINSEQ_1:44
.= card rng Xf by A46,CARD_2:57;
<*zz,jj*> is increasing
proof
let n,m be Nat;
len <*zz,jj*> = 2 by FINSEQ_1:44;
then
A49: dom <*zz,jj*> = { 1,2 } by FINSEQ_1:2,def 3;
assume that
A50: n in dom <*zz,jj*> and
A51: m in dom <*zz,jj*>;
A52: n = 1 or n = 2 by A49,A50,TARSKI:def 2;
A53: m = 1 or m = 2 by A49,A51,TARSKI:def 2;
assume
A54: n < m;
then
A55: <*0,jj*>.n = 0 by A52,A53;
<*0,jj*>.m = 1 by A52,A53,A54;
hence <*zz,jj*>.n < <*zz,jj*>.m by A55;
end;
then
A56: <*0,jj*> = Incr X_axis f by A44,A47,A48,SEQ_4:def 21;
set Yf1 = <*zz,jj,jj *>, Yf2 = <* zz,zz*>;
reconsider Yf = Yf1^Yf2 as FinSequence of REAL;
A57: len Yf1 = 3 by FINSEQ_1:45;
A58: len Yf2 = 2 by FINSEQ_1:44;
then
A59: len Yf = 3+2 by A57,FINSEQ_1:22;
1 in dom Yf1 by A57,FINSEQ_3:25;
then
A60: Yf.1 = Yf1.1 by FINSEQ_1:def 7
.= 0;
2 in dom Yf1 by A57,FINSEQ_3:25;
then
A61: Yf.2 = Yf1.2 by FINSEQ_1:def 7
.= 1;
3 in dom Yf1 by A57,FINSEQ_3:25;
then
A62: Yf.3 = Yf1.3 by FINSEQ_1:def 7
.= 1;
1 in dom Yf2 by A58,FINSEQ_3:25;
then
A63: Yf.(3+1) = Yf2.1 by A57,FINSEQ_1:def 7
.= 0;
2 in dom Yf2 by A58,FINSEQ_3:25;
then
A64: Yf.(3+2) = Yf2.2 by A57,FINSEQ_1:def 7
.= 0;
now
let n be Nat;
assume
A65: n in dom Yf;
then
A66: n <> 0 by FINSEQ_3:25;
n <= 5 by A59,A65,FINSEQ_3:25;
then n = 0 or ... or n = 5;
then per cases by A66;
suppose n = 1;
hence Yf.n = (f/.n)`2 by A5,A60,EUCLID:52;
end;
suppose n = 2;
hence Yf.n = (f/.n)`2 by A7,A61,EUCLID:52;
end;
suppose n = 3;
hence Yf.n = (f/.n)`2 by A10,A62,EUCLID:52;
end;
suppose n = 4;
hence Yf.n = (f/.n)`2 by A11,A63,EUCLID:52;
end;
suppose n = 5;
hence Yf.n = (f/.n)`2 by A12,A64,EUCLID:52;
end;
end;
then
A67: Yf = Y_axis f by A3,A59,GOBOARD1:def 2;
A68: rng Yf1 = { 0,1,1 } by FINSEQ_2:128
.= { 1,1,0 } by ENUMSET1:59
.= { 0,1 } by ENUMSET1:30;
rng Yf2 = { 0,0 } by FINSEQ_2:127
.= { 0 } by ENUMSET1:29;
then
A69: rng Yf = { 0,1 } \/ { 0 } by A68,FINSEQ_1:31
.= { 0,0,1 } by ENUMSET1:2
.= { 0,1 } by ENUMSET1:30;
then
A70: rng <*0,jj*> = rng Yf by FINSEQ_2:127;
A71: len <*0,jj*> = 2 by FINSEQ_1:44
.= card rng Yf by A69,CARD_2:57;
<*In(0,REAL),jj*> is increasing
proof
let n,m be Nat;
len <*0,jj*> = 2 by FINSEQ_1:44;
then
A72: dom <*0,jj*> = { 1,2 } by FINSEQ_1:2,def 3;
assume that
A73: n in dom <*In(0,REAL),jj*> and
A74: m in dom <*In(0,REAL),jj*>;
A75: n = 1 or n = 2 by A72,A73,TARSKI:def 2;
A76: m = 1 or m = 2 by A72,A74,TARSKI:def 2;
assume
A77: n < m;
then
A78: <*0,jj*>.n = 0 by A75,A76;
<*0,jj*>.m = 1 by A75,A76,A77;
hence <*In(0,REAL),jj*>.n < <*In(0,REAL),jj*>.m by A78;
end;
then
A79: <*0,jj*> = Incr Y_axis f by A67,A70,A71,SEQ_4:def 21;
set M = (|[0,0]|,|[0,1]|)][(|[1,0]|,|[1,1]|);
A80: len M = 2 by MATRIX_0:47
.= len Incr X_axis f by A56,FINSEQ_1:44;
A81: width M = 2 by MATRIX_0:47
.= len Incr Y_axis f by A79,FINSEQ_1:44;
for n,m being Nat st [n,m] in Indices M
holds M*(n,m) = |[(Incr X_axis f).n,(Incr Y_axis f).m]|
proof
let n,m be Nat;
assume [n,m] in Indices M;
then [n,m] in [:{ 1,2 },{ 1,2 }:] by FINSEQ_1:2,MATRIX_0:47;
then
A82: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:23;
per cases by A82,ENUMSET1:def 2;
suppose
A85: [n,m] = [1,1];
then
A86: n = 1 by XTUPLE_0:1;
m = 1 by A85,XTUPLE_0:1;
hence thesis by A56,A79,A86,MATRIX_0:50;
end;
suppose
A87: [n,m] = [1,2];
then
A88: n = 1 by XTUPLE_0:1;
m = 2 by A87,XTUPLE_0:1;
hence thesis by A56,A79,A88,MATRIX_0:50;
end;
suppose
A89: [n,m] = [2,1];
then
A90: n = 2 by XTUPLE_0:1;
m = 1 by A89,XTUPLE_0:1;
hence thesis by A56,A79,A90,MATRIX_0:50;
end;
suppose
A91: [n,m] = [2,2];
then
A92: n = 2 by XTUPLE_0:1;
m = 2 by A91,XTUPLE_0:1;
hence thesis by A56,A79,A92,MATRIX_0:50;
end;
end;
then
A93: (|[0,0]|,|[0,1]|)][(|[1,0]|,|[1,1]|)
= GoB(Incr X_axis f, Incr Y_axis f) by A80,A81,GOBOARD2:def 1
.= GoB f by GOBOARD2:def 2;
then
A94: f/.1 = (GoB f)*(1,1) by A5,MATRIX_0:50;
A95: f/.2 = (GoB f)*(1,2) by A7,A93,MATRIX_0:50;
A96: f/.3 = (GoB f)*(2,2) by A10,A93,MATRIX_0:50;
A97: f/.4 = (GoB f)*(2,1) by A11,A93,MATRIX_0:50;
thus for k st k in dom f
ex i,j st [i,j] in Indices GoB f & f/.k = (GoB f)*(i,j)
proof
let k;
assume
A98: k in dom f;
then
A99: k <= 5 by A3,FINSEQ_3:25;
A100: k <> 0 by A98,FINSEQ_3:25;
k = 0 or ... or k = 5 by A99;
then per cases by A100;
suppose
A101: k = 1;
take 1,1;
thus [1,1] in Indices GoB f by A93,MATRIX_0:48;
thus thesis by A5,A93,A101,MATRIX_0:50;
end;
suppose
A102: k = 2;
take 1,2;
thus [1,2] in Indices GoB f by A93,MATRIX_0:48;
thus thesis by A7,A93,A102,MATRIX_0:50;
end;
suppose
A103: k = 3;
take 2,2;
thus [2,2] in Indices GoB f by A93,MATRIX_0:48;
thus thesis by A10,A93,A103,MATRIX_0:50;
end;
suppose
A104: k = 4;
take 2,1;
thus [2,1] in Indices GoB f by A93,MATRIX_0:48;
thus thesis by A11,A93,A104,MATRIX_0:50;
end;
suppose
A105: k = 5;
take 1,1;
thus [1,1] in Indices GoB f by A93,MATRIX_0:48;
thus thesis by A12,A93,A105,MATRIX_0:50;
end;
end;
let n be Nat such that
A106: n in dom f and
A107: n+1 in dom f;
let m,k,i,j be Nat such that
A108: [m,k] in Indices GoB f and
A109: [i,j] in Indices GoB f and
A110: f/.n = (GoB f)*(m,k) and
A111: f/.(n+1) = (GoB f)*(i,j);
A112: n <> 0 by A106,FINSEQ_3:25;
n+1 <= 4+1 by A3,A107,FINSEQ_3:25;
then n = 0 or ... or n = 4 by NAT_1:60,XREAL_1:6;
then per cases by A112;
suppose
A113: n = 1;
A114: [1,1] in Indices GoB f by A93,MATRIX_0:48;
then
A115: m = 1 by A94,A108,A110,A113,GOBOARD1:5;
A116: k = 1 by A94,A108,A110,A113,A114,GOBOARD1:5;
A117: [1,2] in Indices GoB f by A93,MATRIX_0:48;
then
A118: i = 1 by A95,A109,A111,A113,GOBOARD1:5;
j = 1+1 by A95,A109,A111,A113,A117,GOBOARD1:5;
then |.k-j.| = 1 by A116,SEQM_3:41;
hence thesis by A115,A118,SEQM_3:42;
end;
suppose
A119: n = 2;
A120: [1,2] in Indices GoB f by A93,MATRIX_0:48;
then
A121: m = 1 by A95,A108,A110,A119,GOBOARD1:5;
A122: k = 2 by A95,A108,A110,A119,A120,GOBOARD1:5;
A123: [2,2] in Indices GoB f by A93,MATRIX_0:48;
then
A124: i = 1+1 by A96,A109,A111,A119,GOBOARD1:5;
A125: j = 2 by A96,A109,A111,A119,A123,GOBOARD1:5;
|.m-i.| = 1 by A121,A124,SEQM_3:41;
hence thesis by A122,A125,SEQM_3:42;
end;
suppose
A126: n = 3;
A127: [2,2] in Indices GoB f by A93,MATRIX_0:48;
then
A128: m = 2 by A96,A108,A110,A126,GOBOARD1:5;
A129: k = 1+1 by A96,A108,A110,A126,A127,GOBOARD1:5;
A130: [2,1] in Indices GoB f by A93,MATRIX_0:48;
then
A131: i = 2 by A97,A109,A111,A126,GOBOARD1:5;
j = 1 by A97,A109,A111,A126,A130,GOBOARD1:5;
then |.k-j.| = 1 by A129,SEQM_3:41;
hence thesis by A128,A131,SEQM_3:42;
end;
suppose
A132: n = 4;
A133: [2,1] in Indices GoB f by A93,MATRIX_0:48;
then
A134: m = 1+1 by A97,A108,A110,A132,GOBOARD1:5;
A135: k = 1 by A97,A108,A110,A132,A133,GOBOARD1:5;
A136: [1,1] in Indices GoB f by A93,MATRIX_0:48;
then
A137: i = 1 by A5,A12,A94,A109,A111,A132,GOBOARD1:5;
A138: j = 1 by A5,A12,A94,A109,A111,A132,A136,GOBOARD1:5;
|.m-i.| = 1 by A134,A137,SEQM_3:41;
hence thesis by A135,A138,SEQM_3:42;
end;
end;
end;
Lm1: for f being FinSequence of TOP-REAL 2 holds dom X_axis f = dom f
proof
let f be FinSequence of TOP-REAL 2;
len X_axis f = len f by GOBOARD1:def 1;
hence thesis by FINSEQ_3:29;
end;
Lm2: for f being FinSequence of TOP-REAL 2 holds dom Y_axis f = dom f
proof
let f be FinSequence of TOP-REAL 2;
len Y_axis f = len f by GOBOARD1:def 2;
hence thesis by FINSEQ_3:29;
end;
theorem Th11:
for f being non empty FinSequence of TOP-REAL 2
for n being Nat st n in dom f
ex i,j st [i,j] in Indices GoB f & f/.n = (GoB f)*(i,j)
proof
let f be non empty FinSequence of TOP-REAL 2;
let n be Nat such that
A1: n in dom f;
A2: GoB f = GoB(Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 2;
set x = (f/.n)`1, y = (f/.n)`2;
A3: n in dom X_axis f by A1,Lm1;
then (X_axis f).n = x by GOBOARD1:def 1;
then x in rng X_axis f by A3,FUNCT_1:def 3;
then x in rng Incr X_axis f by SEQ_4:def 21;
then consider i being Nat such that
A4: i in dom Incr X_axis f and
A5: (Incr X_axis f).i = x by FINSEQ_2:10;
A6: n in dom Y_axis f by A1,Lm2;
then (Y_axis f).n = y by GOBOARD1:def 2;
then y in rng Y_axis f by A6,FUNCT_1:def 3;
then y in rng Incr Y_axis f by SEQ_4:def 21;
then consider j being Nat such that
A7: j in dom Incr Y_axis f and
A8: (Incr Y_axis f).j = y by FINSEQ_2:10;
reconsider i,j as Nat;
take i,j;
i in Seg len Incr X_axis f by A4,FINSEQ_1:def 3;
then i in Seg len GoB(Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 1;
then
A9: i in dom GoB f by A2,FINSEQ_1:def 3;
j in Seg len Incr Y_axis f by A7,FINSEQ_1:def 3;
then j in Seg width GoB(Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 1;
then [i,j] in [:dom GoB f, Seg width GoB f:] by A2,A9,ZFMISC_1:87;
hence
A10: [i,j] in Indices GoB f by MATRIX_0:def 4;
thus f/.n = |[Incr(X_axis f).i,Incr(Y_axis f).j]| by A5,A8,EUCLID:53
.= (GoB f)*(i,j) by A2,A10,GOBOARD2:def 1;
end;
theorem Th12:
for f being standard non empty FinSequence of TOP-REAL 2,
n being Nat st n in dom f & n+1 in dom f
for m,k,i,j being Nat
st [m,k] in Indices GoB f & [i,j] in Indices GoB f &
f/.n = (GoB f)*(m,k) & f/.(n+1) = (GoB f)*(i,j) holds |.m-i.|+|.k-j.| = 1
proof
let f be standard non empty FinSequence of TOP-REAL 2, n be Nat such that
A1: n in dom f and
A2: n+1 in dom f;
f is_sequence_on GoB f by Def5;
hence thesis by A1,A2;
end;
definition
mode special_circular_sequence is
special unfolded circular s.c.c. non empty FinSequence of TOP-REAL 2;
end;
reserve f for standard special_circular_sequence;
definition
let f,k;
assume that
A1: 1 <= k and
A2: k+1 <= len f;
k <= k+1 by NAT_1:11;
then k <= len f by A2,XXREAL_0:2;
then
A3: k in dom f by A1,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A4: [i1,j1] in Indices GoB f and
A5: f/.k = (GoB f)*(i1,j1) by Th11;
A6: k+1 in dom f by A2,FINSEQ_3:25,NAT_1:11;
then consider i2,j2 being Nat such that
A7: [i2,j2] in Indices GoB f and
A8: f/.(k+1) = (GoB f)*(i2,j2) by Th11;
A9: |.i1-i2.|+|.j1-j2.| = 1 by A3,A4,A5,A6,A7,A8,Th12;
A10: now per cases by A9,SEQM_3:42;
case that
A11: |.i1-i2.| = 1 and
A12: j1 = j2;
i1-i2 = 1 or -(i1-i2) = 1 by A11,ABSVALUE:def 1;
hence i1 = i2+1 or i1+1 = i2;
thus j1 = j2 by A12;
end;
case that
A13: i1 = i2 and
A14: |.j1-j2.| = 1;
j1-j2 = 1 or -(j1-j2) = 1 by A14,ABSVALUE:def 1;
hence j1 = j2+1 or j1+1 = j2;
thus i1 = i2 by A13;
end;
end;
func right_cell(f,k) -> Subset of TOP-REAL 2 means
:Def6:
for i1,j1,i2,j2 being Nat st
[i1,j1] in Indices GoB f & [i2,j2] in Indices GoB f &
f/.k = (GoB f)*(i1,j1) & f/.(k+1) = (GoB f)*(i2,j2) holds
i1 = i2 & j1+1 = j2 & it = cell(GoB f,i1,j1) or
i1+1 = i2 & j1 = j2 & it = cell(GoB f,i1,j1-'1) or
i1 = i2+1 & j1 = j2 & it = cell(GoB f,i2,j2) or
i1 = i2 & j1 = j2+1 & it = cell(GoB f,i1-'1,j2);
existence
proof
per cases by A10;
suppose
A15: i1 = i2 & j1+1 = j2;
take cell(GoB f,i1,j1);
let i19,j19,i29,j29 be Nat;
assume that
A16: [i19,j19] in Indices GoB f and
A17: [i29,j29] in Indices GoB f and
A18: f/.k = (GoB f)*(i19,j19) and
A19: f/.(k+1) = (GoB f)*(i29,j29);
A20: i1 = i19 by A4,A5,A16,A18,GOBOARD1:5;
j1 = j19 by A4,A5,A16,A18,GOBOARD1:5;
hence thesis by A7,A8,A15,A17,A19,A20,GOBOARD1:5;
end;
suppose
A21: i1+1 = i2 & j1 = j2;
take cell(GoB f,i1,j1-'1);
let i19,j19,i29,j29 be Nat;
assume that
A22: [i19,j19] in Indices GoB f and
A23: [i29,j29] in Indices GoB f and
A24: f/.k = (GoB f)*(i19,j19) and
A25: f/.(k+1) = (GoB f)*(i29,j29);
A26: i1 = i19 by A4,A5,A22,A24,GOBOARD1:5;
j1 = j19 by A4,A5,A22,A24,GOBOARD1:5;
hence thesis by A7,A8,A21,A23,A25,A26,GOBOARD1:5;
end;
suppose
A27: i1 = i2+1 & j1 = j2;
take cell(GoB f,i2,j2);
let i19,j19,i29,j29 be Nat;
assume that
A28: [i19,j19] in Indices GoB f and
A29: [i29,j29] in Indices GoB f and
A30: f/.k = (GoB f)*(i19,j19) and
A31: f/.(k+1) = (GoB f)*(i29,j29);
A32: i2 = i29 by A7,A8,A29,A31,GOBOARD1:5;
j1 = j19 by A4,A5,A28,A30,GOBOARD1:5;
hence thesis by A4,A5,A7,A8,A27,A28,A29,A30,A31,A32,GOBOARD1:5;
end;
suppose
A33: i1 = i2 & j1 = j2+1;
take cell(GoB f,i1-'1,j2);
let i19,j19,i29,j29 be Nat;
assume that
A34: [i19,j19] in Indices GoB f and
A35: [i29,j29] in Indices GoB f and
A36: f/.k = (GoB f)*(i19,j19) and
A37: f/.(k+1) = (GoB f)*(i29,j29);
A38: i1 = i19 by A4,A5,A34,A36,GOBOARD1:5;
j1 = j19 by A4,A5,A34,A36,GOBOARD1:5;
hence thesis by A7,A8,A33,A35,A37,A38,GOBOARD1:5;
end;
end;
uniqueness
proof
let P1,P2 be Subset of TOP-REAL 2 such that
A39: for i1,j1,i2,j2 being Nat st
[i1,j1] in Indices GoB f & [i2,j2] in Indices GoB f &
f/.k = (GoB f)*(i1,j1) & f/.(k+1) = (GoB f)*(i2,j2) holds
i1 = i2 & j1+1 = j2 & P1 = cell(GoB f,i1,j1) or
i1+1 = i2 & j1 = j2 & P1 = cell(GoB f,i1,j1-'1) or
i1 = i2+1 & j1 = j2 & P1 = cell(GoB f,i2,j2) or
i1 = i2 & j1 = j2+1 & P1 = cell(GoB f,i1-'1,j2) and
A40: for i1,j1,i2,j2 being Nat st
[i1,j1] in Indices GoB f & [i2,j2] in Indices GoB f &
f/.k = (GoB f)*(i1,j1) & f/.(k+1) = (GoB f)*(i2,j2) holds
i1 = i2 & j1+1 = j2 & P2 = cell(GoB f,i1,j1) or
i1+1 = i2 & j1 = j2 & P2 = cell(GoB f,i1,j1-'1) or
i1 = i2+1 & j1 = j2 & P2 = cell(GoB f,i2,j2) or
i1 = i2 & j1 = j2+1 & P2 = cell(GoB f,i1-'1,j2);
per cases by A10;
suppose i1 = i2 & j1+1 = j2;
then
A41: j1 < j2 by XREAL_1:29;
A42: j2 <= j2+1 by NAT_1:11;
hence P1 = cell(GoB f,i1,j1) by A4,A5,A7,A8,A39,A41
.= P2 by A4,A5,A7,A8,A40,A41,A42;
end;
suppose i1+1 = i2 & j1 = j2;
then
A43: i1 < i2 by XREAL_1:29;
A44: i2 <= i2+1 by NAT_1:11;
hence P1 = cell(GoB f,i1,j1-'1) by A4,A5,A7,A8,A39,A43
.= P2 by A4,A5,A7,A8,A40,A43,A44;
end;
suppose i1 = i2+1 & j1 = j2;
then
A45: i2 < i1 by XREAL_1:29;
A46: i1 <= i1+1 by NAT_1:11;
hence P1 = cell(GoB f,i2,j2) by A4,A5,A7,A8,A39,A45
.= P2 by A4,A5,A7,A8,A40,A45,A46;
end;
suppose i1 = i2 & j1 = j2+1;
then
A47: j2 < j1 by XREAL_1:29;
A48: j1 <= j1+1 by NAT_1:11;
hence P1 = cell(GoB f,i1-'1,j2) by A4,A5,A7,A8,A39,A47
.= P2 by A4,A5,A7,A8,A40,A47,A48;
end;
end;
func left_cell(f,k) -> Subset of TOP-REAL 2 means
:Def7:
for i1,j1,i2,j2 being Nat st
[i1,j1] in Indices GoB f & [i2,j2] in Indices GoB f &
f/.k = (GoB f)*(i1,j1) & f/.(k+1) = (GoB f)*(i2,j2) holds
i1 = i2 & j1+1 = j2 & it = cell(GoB f,i1-'1,j1) or
i1+1 = i2 & j1 = j2 & it = cell(GoB f,i1,j1) or
i1 = i2+1 & j1 = j2 & it = cell(GoB f,i2,j2-'1) or
i1 = i2 & j1 = j2+1 & it = cell(GoB f,i1,j2);
existence
proof
per cases by A10;
suppose
A49: i1 = i2 & j1+1 = j2;
take cell(GoB f,i1-'1,j1);
let i19,j19,i29,j29 be Nat;
assume that
A50: [i19,j19] in Indices GoB f and
A51: [i29,j29] in Indices GoB f and
A52: f/.k = (GoB f)*(i19,j19) and
A53: f/.(k+1) = (GoB f)*(i29,j29);
A54: i1 = i19 by A4,A5,A50,A52,GOBOARD1:5;
j1 = j19 by A4,A5,A50,A52,GOBOARD1:5;
hence thesis by A7,A8,A49,A51,A53,A54,GOBOARD1:5;
end;
suppose
A55: i1+1 = i2 & j1 = j2;
take cell(GoB f,i1,j1);
let i19,j19,i29,j29 be Nat;
assume that
A56: [i19,j19] in Indices GoB f and
A57: [i29,j29] in Indices GoB f and
A58: f/.k = (GoB f)*(i19,j19) and
A59: f/.(k+1) = (GoB f)*(i29,j29);
A60: i1 = i19 by A4,A5,A56,A58,GOBOARD1:5;
j1 = j19 by A4,A5,A56,A58,GOBOARD1:5;
hence thesis by A7,A8,A55,A57,A59,A60,GOBOARD1:5;
end;
suppose
A61: i1 = i2+1 & j1 = j2;
take cell(GoB f,i2,j2-'1);
let i19,j19,i29,j29 be Nat;
assume that
A62: [i19,j19] in Indices GoB f and
A63: [i29,j29] in Indices GoB f and
A64: f/.k = (GoB f)*(i19,j19) and
A65: f/.(k+1) = (GoB f)*(i29,j29);
A66: i2 = i29 by A7,A8,A63,A65,GOBOARD1:5;
j1 = j19 by A4,A5,A62,A64,GOBOARD1:5;
hence thesis by A4,A5,A7,A8,A61,A62,A63,A64,A65,A66,GOBOARD1:5;
end;
suppose
A67: i1 = i2 & j1 = j2+1;
take cell(GoB f,i1,j2);
let i19,j19,i29,j29 be Nat;
assume that
A68: [i19,j19] in Indices GoB f and
A69: [i29,j29] in Indices GoB f and
A70: f/.k = (GoB f)*(i19,j19) and
A71: f/.(k+1) = (GoB f)*(i29,j29);
A72: i1 = i19 by A4,A5,A68,A70,GOBOARD1:5;
j1 = j19 by A4,A5,A68,A70,GOBOARD1:5;
hence thesis by A7,A8,A67,A69,A71,A72,GOBOARD1:5;
end;
end;
uniqueness
proof
let P1,P2 be Subset of TOP-REAL 2 such that
A73: for i1,j1,i2,j2 being Nat st
[i1,j1] in Indices GoB f & [i2,j2] in Indices GoB f &
f/.k = (GoB f)*(i1,j1) & f/.(k+1) = (GoB f)*(i2,j2) holds
i1 = i2 & j1+1 = j2 & P1 = cell(GoB f,i1-'1,j1) or
i1+1 = i2 & j1 = j2 & P1 = cell(GoB f,i1,j1) or
i1 = i2+1 & j1 = j2 & P1 = cell(GoB f,i2,j2-'1) or
i1 = i2 & j1 = j2+1 & P1 = cell(GoB f,i1,j2) and
A74: for i1,j1,i2,j2 being Nat st
[i1,j1] in Indices GoB f & [i2,j2] in Indices GoB f &
f/.k = (GoB f)*(i1,j1) & f/.(k+1) = (GoB f)*(i2,j2) holds
i1 = i2 & j1+1 = j2 & P2 = cell(GoB f,i1-'1,j1) or
i1+1 = i2 & j1 = j2 & P2 = cell(GoB f,i1,j1) or
i1 = i2+1 & j1 = j2 & P2 = cell(GoB f,i2,j2-'1) or
i1 = i2 & j1 = j2+1 & P2 = cell(GoB f,i1,j2);
per cases by A10;
suppose i1 = i2 & j1+1 = j2;
then
A75: j1 < j2 by XREAL_1:29;
A76: j2 <= j2+1 by NAT_1:11;
hence P1 = cell(GoB f,i1-'1,j1) by A4,A5,A7,A8,A73,A75
.= P2 by A4,A5,A7,A8,A74,A75,A76;
end;
suppose i1+1 = i2 & j1 = j2;
then
A77: i1 < i2 by XREAL_1:29;
A78: i2 <= i2+1 by NAT_1:11;
hence P1 = cell(GoB f,i1,j1) by A4,A5,A7,A8,A73,A77
.= P2 by A4,A5,A7,A8,A74,A77,A78;
end;
suppose i1 = i2+1 & j1 = j2;
then
A79: i2 < i1 by XREAL_1:29;
A80: i1 <= i1+1 by NAT_1:11;
hence P1 = cell(GoB f,i2,j2-'1) by A4,A5,A7,A8,A73,A79
.= P2 by A4,A5,A7,A8,A74,A79,A80;
end;
suppose i1 = i2 & j1 = j2+1;
then
A81: j2 < j1 by XREAL_1:29;
A82: j1 <= j1+1 by NAT_1:11;
hence P1 = cell(GoB f,i1,j2) by A4,A5,A7,A8,A73,A81
.= P2 by A4,A5,A7,A8,A74,A81,A82;
end;
end;
end;
theorem Th13:
G is non empty-yielding X_equal-in-line X_increasing-in-column &
i < len G & 1 <= j & j < width G
implies LSeg(G*(i+1,j),G*(i+1,j+1)) c= v_strip(G,i)
proof
assume that
A1: G is non empty-yielding and
A2: G is X_equal-in-line and
A3: G is X_increasing-in-column and
A4: i < len G and
A5: 1 <= j and
A6: j < width G;
A7: 1 <= j+1 by A5,NAT_1:13;
A8: j+1 <= width G by A6,NAT_1:13;
let x be object;
assume
A9: x in LSeg(G*(i+1,j),G*(i+1,j+1));
then reconsider p = x as Point of TOP-REAL 2;
A10: p = |[p`1, p`2]| by EUCLID:53;
A11: 1 <= i+1 by NAT_1:11;
A12: i+1 <= len G by A4,NAT_1:13;
then
A13: G*(i+1,j)`1 = G*(i+1,1)`1 by A2,A5,A6,A11,Th2
.= G*(i+1,j+1)`1 by A2,A7,A8,A11,A12,Th2;
now per cases;
suppose
A14: i = 0;
then p`1 <= G*(1,j)`1 by A9,A13,TOPREAL1:3;
then p in { |[r,s]| : r <= G*(1,j)`1 } by A10;
hence thesis by A1,A2,A5,A6,A14,Th10;
end;
suppose i > 0;
then
A15: 0+1 <= i by NAT_1:13;
A16: G*(i+1,j)`1 <= p`1 by A9,A13,TOPREAL1:3;
A17: p`1 <= G*(i+1,j)`1 by A9,A13,TOPREAL1:3;
then
A18: p`1 = G*(i+1,j)`1 by A16,XXREAL_0:1;
i < i+1 by XREAL_1:29;
then G*(i,j)`1 < p`1 by A3,A5,A6,A12,A15,A18,Th3;
then p in { |[r,s]| : G*(i,j)`1 <= r & r <= G*(i+1,j)`1 } by A10,A17;
hence thesis by A2,A4,A5,A6,A15,Th8;
end;
end;
hence thesis;
end;
theorem Th14:
G is non empty-yielding X_equal-in-line X_increasing-in-column &
1 <= i & i <= len G & 1 <= j & j < width G
implies LSeg(G*(i,j),G*(i,j+1)) c= v_strip(G,i)
proof
assume that
A1: G is non empty-yielding and
A2: G is X_equal-in-line and
A3: G is X_increasing-in-column and
A4: 1 <= i and
A5: i <= len G and
A6: 1 <= j and
A7: j < width G;
A8: 1 <= j+1 by A6,NAT_1:13;
A9: j+1 <= width G by A7,NAT_1:13;
let x be object;
assume
A10: x in LSeg(G*(i,j),G*(i,j+1));
then reconsider p = x as Point of TOP-REAL 2;
A11: p = |[p`1, p`2]| by EUCLID:53;
A12: G*(i,j)`1 = G*(i,1)`1 by A2,A4,A5,A6,A7,Th2
.= G*(i,j+1)`1 by A2,A4,A5,A8,A9,Th2;
now per cases by A5,XXREAL_0:1;
suppose
A13: i = len G;
then G*(len G,j)`1 <= p`1 by A10,A12,TOPREAL1:3;
then p in { |[r,s]| : G*(len G,j)`1 <= r } by A11;
hence thesis by A1,A2,A6,A7,A13,Th9;
end;
suppose
A14: i < len G;
then
A15: i+1 <= len G by NAT_1:13;
A16: G*(i,j)`1 <= p`1 by A10,A12,TOPREAL1:3;
p`1 <= G*(i,j)`1 by A10,A12,TOPREAL1:3;
then
A17: p`1 = G*(i,j)`1 by A16,XXREAL_0:1;
i < i+1 by XREAL_1:29;
then p`1 < G*(i+1,j)`1 by A3,A4,A6,A7,A15,A17,Th3;
then p in { |[r,s]| : G*(i,j)`1 <= r & r <= G*(i+1,j)`1 } by A11,A16;
hence thesis by A2,A4,A6,A7,A14,Th8;
end;
end;
hence thesis;
end;
theorem Th15:
G is non empty-yielding Y_equal-in-column Y_increasing-in-line &
j < width G & 1 <= i & i < len G
implies LSeg(G*(i,j+1),G*(i+1,j+1)) c= h_strip(G,j)
proof
assume that
A1: G is non empty-yielding and
A2: G is Y_equal-in-column and
A3: G is Y_increasing-in-line and
A4: j < width G and
A5: 1 <= i and
A6: i < len G;
A7: 1 <= i+1 by A5,NAT_1:13;
A8: i+1 <= len G by A6,NAT_1:13;
let x be object;
assume
A9: x in LSeg(G*(i,j+1),G*(i+1,j+1));
then reconsider p = x as Point of TOP-REAL 2;
A10: p = |[p`1, p`2]| by EUCLID:53;
A11: 1 <= j+1 by NAT_1:11;
A12: j+1 <= width G by A4,NAT_1:13;
then
A13: G*(i,j+1)`2 = G*(1,j+1)`2 by A2,A5,A6,A11,Th1
.= G*(i+1,j+1)`2 by A2,A7,A8,A11,A12,Th1;
now per cases;
suppose
A14: j = 0;
then p`2 <= G*(i,1)`2 by A9,A13,TOPREAL1:4;
then p in { |[r,s]| : s <= G*(i,1)`2 } by A10;
hence thesis by A1,A2,A5,A6,A14,Th7;
end;
suppose j > 0;
then
A15: 0+1 <= j by NAT_1:13;
A16: G*(i,j+1)`2 <= p`2 by A9,A13,TOPREAL1:4;
A17: p`2 <= G*(i,j+1)`2 by A9,A13,TOPREAL1:4;
then
A18: p`2 = G*(i,j+1)`2 by A16,XXREAL_0:1;
j < j+1 by XREAL_1:29;
then G*(i,j)`2 < p`2 by A3,A5,A6,A12,A15,A18,Th4;
then p in { |[r,s]| : G*(i,j)`2 <= s & s <= G*(i,j+1)`2 } by A10,A17;
hence thesis by A2,A4,A5,A6,A15,Th5;
end;
end;
hence thesis;
end;
theorem Th16:
G is non empty-yielding Y_equal-in-column Y_increasing-in-line &
1 <= j & j <= width G & 1 <= i & i < len G
implies LSeg(G*(i,j),G*(i+1,j)) c= h_strip(G,j)
proof
assume that
A1: G is non empty-yielding and
A2: G is Y_equal-in-column and
A3: G is Y_increasing-in-line and
A4: 1 <= j and
A5: j <= width G and
A6: 1 <= i and
A7: i < len G;
A8: 1 <= i+1 by A6,NAT_1:13;
A9: i+1 <= len G by A7,NAT_1:13;
let x be object;
assume
A10: x in LSeg(G*(i,j),G*(i+1,j));
then reconsider p = x as Point of TOP-REAL 2;
A11: p = |[p`1, p`2]| by EUCLID:53;
A12: G*(i,j)`2 = G*(1,j)`2 by A2,A4,A5,A6,A7,Th1
.= G*(i+1,j)`2 by A2,A4,A5,A8,A9,Th1;
now per cases by A5,XXREAL_0:1;
suppose
A13: j = width G;
then G*(i,width G)`2 <= p`2 by A10,A12,TOPREAL1:4;
then p in { |[r,s]| : G*(i,width G)`2 <= s } by A11;
hence thesis by A1,A2,A6,A7,A13,Th6;
end;
suppose
A14: j < width G;
then
A15: j+1 <= width G by NAT_1:13;
A16: G*(i,j)`2 <= p`2 by A10,A12,TOPREAL1:4;
p`2 <= G*(i,j)`2 by A10,A12,TOPREAL1:4;
then
A17: p`2 = G*(i,j)`2 by A16,XXREAL_0:1;
j < j+1 by XREAL_1:29;
then p`2 < G*(i,j+1)`2 by A3,A4,A6,A7,A15,A17,Th4;
then p in { |[r,s]| : G*(i,j)`2 <= s & s <= G*(i,j+1)`2 } by A11,A16;
hence thesis by A2,A4,A6,A7,A14,Th5;
end;
end;
hence thesis;
end;
theorem Th17:
G is Y_equal-in-column Y_increasing-in-line &
1 <= i & i <= len G & 1 <= j & j+1 <= width G
implies LSeg(G*(i,j),G*(i,j+1)) c= h_strip(G,j)
proof
assume that
A1: G is Y_equal-in-column and
A2: G is Y_increasing-in-line and
A3: 1 <= i and
A4: i <= len G and
A5: 1 <= j and
A6: j+1 <= width G;
let x be object;
assume
A7: x in LSeg(G*(i,j),G*(i,j+1));
then reconsider p = x as Point of TOP-REAL 2;
A8: p = |[p`1, p`2]| by EUCLID:53;
A9: j < width G by A6,NAT_1:13;
j < j+1 by XREAL_1:29;
then
A10: G*(i,j)`2 < G*(i,j+1)`2 by A2,A3,A4,A5,A6,Th4;
then
A11: G*(i,j)`2 <= p`2 by A7,TOPREAL1:4;
p`2 <= G*(i,j+1)`2 by A7,A10,TOPREAL1:4;
then p in { |[r,s]| : G*(i,j)`2 <= s & s <= G*(i,j+1)`2 } by A8,A11;
hence thesis by A1,A3,A4,A5,A9,Th5;
end;
theorem Th18:
for G being Go-board holds i < len G & 1 <= j & j < width G
implies LSeg(G*(i+1,j),G*(i+1,j+1)) c= cell(G,i,j)
proof
let G be Go-board;
assume that
A1: i < len G and
A2: 1 <= j and
A3: j < width G;
A4: LSeg(G*(i+1,j),G*(i+1,j+1)) c= v_strip(G,i) by A1,A2,A3,Th13;
A5: 1 <= i+1 by NAT_1:11;
A6: i+1 <= len G by A1,NAT_1:13;
j+1 <= width G by A3,NAT_1:13;
then LSeg(G*(i+1,j),G*(i+1,j+1)) c= h_strip(G,j) by A2,A5,A6,Th17;
hence thesis by A4,XBOOLE_1:19;
end;
theorem Th19:
for G being Go-board holds 1 <= i & i <= len G & 1 <= j & j < width G
implies LSeg(G*(i,j),G*(i,j+1)) c= cell(G,i,j)
proof
let G be Go-board;
assume that
A1: 1 <= i and
A2: i <= len G and
A3: 1 <= j and
A4: j < width G;
A5: LSeg(G*(i,j),G*(i,j+1)) c= v_strip(G,i) by A1,A2,A3,A4,Th14;
j+1 <= width G by A4,NAT_1:13;
then LSeg(G*(i,j),G*(i,j+1)) c= h_strip(G,j) by A1,A2,A3,Th17;
hence thesis by A5,XBOOLE_1:19;
end;
theorem Th20:
G is X_equal-in-line X_increasing-in-column &
1 <= j & j <= width G & 1 <= i & i+1 <= len G
implies LSeg(G*(i,j),G*(i+1,j)) c= v_strip(G,i)
proof
assume that
A1: G is X_equal-in-line and
A2: G is X_increasing-in-column and
A3: 1 <= j and
A4: j <= width G and
A5: 1 <= i and
A6: i+1 <= len G;
let x be object;
assume
A7: x in LSeg(G*(i,j),G*(i+1,j));
then reconsider p = x as Point of TOP-REAL 2;
A8: p = |[p`1, p`2]| by EUCLID:53;
A9: i < len G by A6,NAT_1:13;
i < i+1 by XREAL_1:29;
then
A10: G*(i,j)`1 < G*(i+1,j)`1 by A2,A3,A4,A5,A6,Th3;
then
A11: G*(i,j)`1 <= p`1 by A7,TOPREAL1:3;
p`1 <= G*(i+1,j)`1 by A7,A10,TOPREAL1:3;
then p in { |[r,s]| : G*(i,j)`1 <= r & r <= G*(i+1,j)`1 } by A8,A11;
hence thesis by A1,A3,A4,A5,A9,Th8;
end;
theorem Th21:
for G being Go-board holds j < width G & 1 <= i & i < len G
implies LSeg(G*(i,j+1),G*(i+1,j+1)) c= cell(G,i,j)
proof
let G be Go-board;
assume that
A1: j < width G and
A2: 1 <= i and
A3: i < len G;
A4: LSeg(G*(i,j+1),G*(i+1,j+1)) c= h_strip(G,j) by A1,A2,A3,Th15;
A5: 1 <= j+1 by NAT_1:11;
A6: i+1 <= len G by A3,NAT_1:13;
j+1 <= width G by A1,NAT_1:13;
then LSeg(G*(i,j+1),G*(i+1,j+1)) c= v_strip(G,i) by A2,A5,A6,Th20;
hence thesis by A4,XBOOLE_1:19;
end;
theorem Th22:
for G being Go-board holds 1 <= i & i < len G & 1 <= j & j <= width G
implies LSeg(G*(i,j),G*(i+1,j)) c= cell(G,i,j)
proof
let G be Go-board;
assume that
A1: 1 <= i and
A2: i < len G and
A3: 1 <= j and
A4: j <= width G;
A5: LSeg(G*(i,j),G*(i+1,j)) c= h_strip(G,j) by A1,A2,A3,A4,Th16;
i+1 <= len G by A2,NAT_1:13;
then LSeg(G*(i,j),G*(i+1,j)) c= v_strip(G,i) by A1,A3,A4,Th20;
hence thesis by A5,XBOOLE_1:19;
end;
theorem Th23:
G is non empty-yielding X_equal-in-line X_increasing-in-column &
i+1 <= len G implies
v_strip(G,i) /\ v_strip(G,i+1) = { q : q`1 = G*(i+1,1)`1 }
proof
assume that
A1: G is non empty-yielding X_equal-in-line and
A2: G is X_increasing-in-column and
A3: i+1 <= len G;
width G <> 0 by A1,MATRIX_0:def 10;
then
A4: 1 <= width G by NAT_1:14;
A5: i < len G by A3,NAT_1:13;
thus v_strip(G,i) /\ v_strip(G,i+1) c= { q : q`1 = G*(i+1,1)`1 }
proof
let x be object;
assume
A6: x in v_strip(G,i) /\ v_strip(G,i+1);
then
A7: x in v_strip(G,i) by XBOOLE_0:def 4;
A8: x in v_strip(G,i+1) by A6,XBOOLE_0:def 4;
reconsider p = x as Point of TOP-REAL 2 by A6;
per cases;
suppose that
A9: i = 0 and
A10: i+1 = len G;
v_strip(G,i) = { |[r,s]| : r <= G*(0+1,1)`1 } by A1,A4,A9,Th10;
then consider r1,s1 being Real such that
A11: x = |[r1,s1]| and
A12: r1 <= G*(1,1)`1 by A7;
v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 <= r } by A1,A4,Th9;
then consider r2,s2 being Real such that
A13: x = |[r2,s2]| and
A14: G*(i+1,1)`1 <= r2 by A8,A10;
r1 = |[r2,s2]|`1 by A11,A13,EUCLID:52
.= r2 by EUCLID:52;
then G*(i+1,1)`1 = r1 by A9,A12,A14,XXREAL_0:1;
then G*(i+1,1)`1 = p`1 by A11,EUCLID:52;
hence thesis;
end;
suppose that
A15: i = 0 and
A16: i+1 <> len G;
v_strip(G,i) = { |[r,s]| : r <= G*(0+1,1)`1 } by A1,A4,A15,Th10;
then consider r1,s1 being Real such that
A17: x = |[r1,s1]| and
A18: r1 <= G*(1,1)`1 by A7;
i+1 < len G by A3,A16,XXREAL_0:1;
then v_strip(G,i+1) = { |[r,s]| : G*(0+1,1)`1 <= r & r <= G*
(0+1+1,1)`1 } by A1,A4,A15,Th8;
then consider r2,s2 being Real such that
A19: x = |[r2,s2]| and
A20: G*(1,1)`1 <= r2 and r2 <= G*(1+1,1)`1 by A8;
r1 = |[r2,s2]|`1 by A17,A19,EUCLID:52
.= r2 by EUCLID:52;
then G*(1,1)`1 = r1 by A18,A20,XXREAL_0:1;
then G*(1,1)`1 = p`1 by A17,EUCLID:52;
hence thesis by A15;
end;
suppose that
A21: i <> 0 and
A22: i+1 = len G;
A23: 1 <= i by A21,NAT_1:14;
v_strip(G,i) = { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 }
by A1,A4,A23,Th8,A3,NAT_1:13;
then consider r1,s1 being Real such that
A24: x = |[r1,s1]| and
G*(i,1)`1 <= r1 and
A25: r1 <= G*(i+1,1)`1 by A7;
v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 <= r } by A1,A4,Th9;
then consider r2,s2 being Real such that
A26: x = |[r2,s2]| and
A27: G*(i+1,1)`1 <= r2 by A8,A22;
r1 = |[r2,s2]|`1 by A24,A26,EUCLID:52
.= r2 by EUCLID:52;
then G*(i+1,1)`1 = r1 by A25,A27,XXREAL_0:1;
then G*(i+1,1)`1 = p`1 by A24,EUCLID:52;
hence thesis;
end;
suppose that
A28: i <> 0 and
A29: i+1 <> len G;
A30: 1 <= i by A28,NAT_1:14;
v_strip(G,i) = { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 }
by A1,A4,A30,Th8,A3,NAT_1:13;
then consider r1,s1 being Real such that
A31: x = |[r1,s1]| and
G*(i,1)`1 <= r1 and
A32: r1 <= G*(i+1,1)`1 by A7;
A33: 1 <= i+1 by NAT_1:11;
i+1 < len G by A3,A29,XXREAL_0:1;
then v_strip(G,i+1) = { |[r,s]| : G*(i+1,1)`1 <= r & r <= G*
(i+1+1,1)`1 } by A1,A4,A33,Th8;
then consider r2,s2 being Real such that
A34: x = |[r2,s2]| and
A35: G*(i+1,1)`1 <= r2 and r2 <= G*(i+1+1,1)`1 by A8;
r1 = |[r2,s2]|`1 by A31,A34,EUCLID:52
.= r2 by EUCLID:52;
then G*(i+1,1)`1 = r1 by A32,A35,XXREAL_0:1;
then G*(i+1,1)`1 = p`1 by A31,EUCLID:52;
hence thesis;
end;
end;
A36: { q : q`1 = G*(i+1,1)`1 } c= v_strip(G,i)
proof
let x be object;
assume x in { q : q`1 = G*(i+1,1)`1 };
then consider p such that
A37: p = x and
A38: p`1 = G*(i+1,1)`1;
A39: p = |[p`1, p`2]| by EUCLID:53;
per cases by NAT_1:14;
suppose
A40: i = 0;
then v_strip(G,i) = { |[r,s]| : r <= G*(1,1)`1 } by A1,A4,Th10;
hence thesis by A37,A38,A39,A40;
end;
suppose
A41: i >= 1;
then
A42: v_strip(G,i) = { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 }
by A1,A4,A5,Th8;
i < i+1 by XREAL_1:29;
then G*(i,1)`1 < p`1 by A2,A3,A4,A38,A41,Th3;
hence thesis by A37,A38,A39,A42;
end;
end;
{ q : q`1 = G*(i+1,1)`1 } c= v_strip(G,i+1)
proof
let x be object;
assume x in { q : q`1 = G*(i+1,1)`1 };
then consider p such that
A43: p = x and
A44: p`1 = G*(i+1,1)`1;
A45: p = |[p`1, p`2]| by EUCLID:53;
A46: 1 <= i+1 by NAT_1:11;
per cases by A3,XXREAL_0:1;
suppose
A47: i+1 = len G;
then v_strip(G,i+1) = { |[r,s]| : G*(len G,1)`1 <= r } by A1,A4,Th9;
hence thesis by A43,A44,A45,A47;
end;
suppose
A48: i+1 < len G;
then
A49: v_strip
(G,i+1) = { |[r,s]| : G*(i+1,1)`1 <= r & r <= G*(i+1+1, 1)`1 }
by A1,A4,A46,Th8;
A50: i+1 < i+1+1 by NAT_1:13;
i+1+1 <= len G by A48,NAT_1:13;
then p`1 < G*(i+1+1,1)`1 by A2,A4,A44,A46,A50,Th3;
hence thesis by A43,A44,A45,A49;
end;
end;
hence thesis by A36,XBOOLE_1:19;
end;
theorem Th24:
G is non empty-yielding Y_equal-in-column Y_increasing-in-line &
j+1 <= width G implies
h_strip(G,j) /\ h_strip(G,j+1) = { q : q`2 = G*(1,j+1)`2 }
proof
assume that
A1: G is non empty-yielding Y_equal-in-column and
A2: G is Y_increasing-in-line and
A3: j+1 <= width G;
len G <> 0 by A1,MATRIX_0:def 10;
then
A4: 1 <= len G by NAT_1:14;
A5: j < width G by A3,NAT_1:13;
thus h_strip(G,j) /\ h_strip(G,j+1) c= { q : q`2 = G*(1,j+1)`2 }
proof
let x be object;
assume
A6: x in h_strip(G,j) /\ h_strip(G,j+1);
then
A7: x in h_strip(G,j) by XBOOLE_0:def 4;
A8: x in h_strip(G,j+1) by A6,XBOOLE_0:def 4;
reconsider p = x as Point of TOP-REAL 2 by A6;
per cases;
suppose that
A9: j = 0 and
A10: j+1 = width G;
h_strip(G,j) = { |[r,s]| : s <= G*(1,0+1)`2 } by A1,A4,A9,Th7;
then consider r1,s1 being Real such that
A11: x = |[r1,s1]| and
A12: s1 <= G*(1,1)`2 by A7;
h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 <= s } by A1,A4,Th6;
then consider r2,s2 being Real such that
A13: x = |[r2,s2]| and
A14: G*(1,j+1)`2 <= s2 by A8,A10;
s1 = |[r2,s2]|`2 by A11,A13,EUCLID:52
.= s2 by EUCLID:52;
then G*(1,j+1)`2 = s1 by A9,A12,A14,XXREAL_0:1;
then G*(1,j+1)`2 = p`2 by A11,EUCLID:52;
hence thesis;
end;
suppose that
A15: j = 0 and
A16: j+1 <> width G;
h_strip(G,j) = { |[r,s]| : s <= G*(1,0+1)`2 } by A1,A4,A15,Th7;
then consider r1,s1 being Real such that
A17: x = |[r1,s1]| and
A18: s1 <= G*(1,1)`2 by A7;
j+1 < width G by A3,A16,XXREAL_0:1;
then h_strip(G,j+1) = { |[r,s]| : G*(1,0+1)`2 <= s & s <= G*
(1,0+1+1)`2 } by A1,A4,A15,Th5;
then consider r2,s2 being Real such that
A19: x = |[r2,s2]| and
A20: G*(1,1)`2 <= s2 and s2 <= G*(1,1+1)`2 by A8;
s1 = |[r2,s2]|`2 by A17,A19,EUCLID:52
.= s2 by EUCLID:52;
then G*(1,1)`2 = s1 by A18,A20,XXREAL_0:1;
then G*(1,1)`2 = p`2 by A17,EUCLID:52;
hence thesis by A15;
end;
suppose that
A21: j <> 0 and
A22: j+1 = width G;
A23: 1 <= j by A21,NAT_1:14;
h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
by A1,A4,A23,Th5,A3,NAT_1:13;
then consider r1,s1 being Real such that
A24: x = |[r1,s1]| and
G*(1,j)`2 <= s1 and
A25: s1 <= G*(1,j+1)`2 by A7;
h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 <= s } by A1,A4,Th6;
then consider r2,s2 being Real such that
A26: x = |[r2,s2]| and
A27: G*(1,j+1)`2 <= s2 by A8,A22;
s1 = |[r2,s2]|`2 by A24,A26,EUCLID:52
.= s2 by EUCLID:52;
then G*(1,j+1)`2 = s1 by A25,A27,XXREAL_0:1;
then G*(1,j+1)`2 = p`2 by A24,EUCLID:52;
hence thesis;
end;
suppose that
A28: j <> 0 and
A29: j+1 <> width G;
A30: 1 <= j by A28,NAT_1:14;
h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
by A1,A4,A30,Th5,A3,NAT_1:13;
then consider r1,s1 being Real such that
A31: x = |[r1,s1]| and
G*(1,j)`2 <= s1 and
A32: s1 <= G*(1,j+1)`2 by A7;
A33: 1 <= j+1 by NAT_1:11;
j+1 < width G by A3,A29,XXREAL_0:1;
then h_strip(G,j+1) = { |[r,s]| : G*(1,j+1)`2 <= s & s <= G*
(1,j+1+1)`2 } by A1,A4,A33,Th5;
then consider r2,s2 being Real such that
A34: x = |[r2,s2]| and
A35: G*(1,j+1)`2 <= s2 and s2 <= G*(1,j+1+1)`2 by A8;
s1 = |[r2,s2]|`2 by A31,A34,EUCLID:52
.= s2 by EUCLID:52;
then G*(1,j+1)`2 = s1 by A32,A35,XXREAL_0:1;
then G*(1,j+1)`2 = p`2 by A31,EUCLID:52;
hence thesis;
end;
end;
A36: { q : q`2 = G*(1,j+1)`2 } c= h_strip(G,j)
proof
let x be object;
assume x in { q : q`2 = G*(1,j+1)`2 };
then consider p such that
A37: p = x and
A38: p`2 = G*(1,j+1)`2;
A39: p = |[p`1, p`2]| by EUCLID:53;
per cases by NAT_1:14;
suppose
A40: j = 0;
then h_strip(G,j) = { |[r,s]| : s <= G*(1,1)`2 } by A1,A4,Th7;
hence thesis by A37,A38,A39,A40;
end;
suppose
A41: j >= 1;
then
A42: h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
by A1,A4,A5,Th5;
j < j+1 by XREAL_1:29;
then G*(1,j)`2 < p`2 by A2,A3,A4,A38,A41,Th4;
hence thesis by A37,A38,A39,A42;
end;
end;
{ q : q`2 = G*(1,j+1)`2 } c= h_strip(G,j+1)
proof
let x be object;
assume x in { q : q`2 = G*(1,j+1)`2 };
then consider p such that
A43: p = x and
A44: p`2 = G*(1,j+1)`2;
A45: p = |[p`1, p`2]| by EUCLID:53;
A46: 1 <= j+1 by NAT_1:11;
per cases by A3,XXREAL_0:1;
suppose
A47: j+1 = width G;
then h_strip(G,j+1) = { |[r,s]| : G*(1,width G)`2 <= s } by A1,A4,Th6;
hence thesis by A43,A44,A45,A47;
end;
suppose
A48: j+1 < width G;
then
A49: h_strip
(G,j+1) = { |[r,s]| : G*(1,j+1)`2 <= s & s <= G*(1,j+1+ 1)`2 }
by A1,A4,A46,Th5;
A50: j+1 < j+1+1 by NAT_1:13;
j+1+1 <= width G by A48,NAT_1:13;
then p`2 < G*(1,j+1+1)`2 by A2,A4,A44,A46,A50,Th4;
hence thesis by A43,A44,A45,A49;
end;
end;
hence thesis by A36,XBOOLE_1:19;
end;
theorem Th25:
for G being Go-board holds i < len G & 1 <= j & j < width G
implies cell(G,i,j) /\ cell(G,i+1,j) = LSeg(G*(i+1,j),G*(i+1,j+1))
proof
let G be Go-board;
assume that
A1: i < len G and
A2: 1 <= j and
A3: j < width G;
A4: 0+1 <= i+1 by XREAL_1:6;
A5: i+1 <= len G by A1,NAT_1:13;
thus cell(G,i,j) /\ cell(G,i+1,j) c= LSeg(G*(i+1,j),G*(i+1,j+1))
proof
let x be object;
A6: cell(G,i,j) /\ cell(G,i+1,j)
= v_strip(G,i) /\ (v_strip(G,i+1) /\ h_strip(G,j) /\
h_strip(G,j)) by XBOOLE_1:16
.= v_strip(G,i) /\ (v_strip(G,i+1) /\ (h_strip(G,j) /\ h_strip(G,j)))
by XBOOLE_1:16
.= v_strip(G,i) /\ v_strip(G,i+1) /\ h_strip(G,j) by XBOOLE_1:16;
assume
A7: x in cell(G,i,j) /\ cell(G,i+1,j);
then
A8: x in v_strip(G,i) /\ v_strip(G,i+1) by A6,XBOOLE_0:def 4;
A9: x in h_strip(G,j) by A6,A7,XBOOLE_0:def 4;
A10: j < j+1 by NAT_1:13;
A11: j+1 <= width G by A3,NAT_1:13;
then
A12: G*(i+1,j)`2 < G*(i+1,j+1)`2 by A2,A4,A5,A10,Th4;
A13: G*(i+1,j) = |[G*(i+1,j)`1,G*(i+1,j)`2]| by EUCLID:53;
A14: j+1 >= 1 by NAT_1:11;
G*(i+1,j)`1 = G*(i+1,1)`1 by A2,A3,A4,A5,Th2
.= G*(i+1,j+1)`1 by A4,A5,A11,A14,Th2;
then
A15: G*(i+1,j+1) = |[G*(i+1,j)`1,G*(i+1,j+1)`2]| by EUCLID:53;
reconsider p = x as Point of TOP-REAL 2 by A7;
i+1 <= len G by A1,NAT_1:13;
then p in { q : q`1 = G*(i+1,1)`1 } by A8,Th23;
then ex q st q = p & q`1 = G*(i+1,1)`1;
then
A16: p`1 = G*(i+1,j)`1 by A2,A3,A4,A5,Th2;
p in { |[r,s]| : G*(i+1,j)`2 <= s & s <= G*(i+1,j+1)`2 } by A2,A3,A4,A5,A9
,Th5;
then
A17: ex r,s st ( p = |[r,s]|)&( G*(i+1,j)`2 <= s)&( s <= G*(i+1, j+1)`2);
then
A18: G*(i+1,j)`2 <= p`2 by EUCLID:52;
p`2 <= G*(i+1,j+1)`2 by A17,EUCLID:52;
then p in
{ q : q`1 = G*(i+1,j)`1 & G*(i+1,j)`2 <= q`2 & q`2 <= G*(i+1,j+1)`2 }
by A16,A18;
hence thesis by A12,A13,A15,TOPREAL3:9;
end;
A19: LSeg(G*(i+1,j),G*(i+1,j+1)) c= cell(G,i,j) by A1,A2,A3,Th18;
LSeg(G*(i+1,j),G*(i+1,j+1)) c= cell(G,i+1,j) by A2,A3,A4,A5,Th19;
hence thesis by A19,XBOOLE_1:19;
end;
theorem Th26:
for G being Go-board holds j < width G & 1 <= i & i < len G
implies cell(G,i,j) /\ cell(G,i,j+1) = LSeg(G*(i,j+1),G*(i+1,j+1))
proof
let G be Go-board;
assume that
A1: j < width G and
A2: 1 <= i and
A3: i < len G;
A4: 0+1 <= j+1 by XREAL_1:6;
A5: j+1 <= width G by A1,NAT_1:13;
thus cell(G,i,j) /\ cell(G,i,j+1) c= LSeg(G*(i,j+1),G*(i+1,j+1))
proof
let x be object;
A6: cell(G,i,j) /\ cell(G,i,j+1)
= h_strip(G,j) /\ (h_strip(G,j+1) /\ v_strip(G,i) /\
v_strip(G,i)) by XBOOLE_1:16
.= h_strip(G,j) /\ (h_strip(G,j+1) /\ (v_strip(G,i) /\ v_strip(G,i)))
by XBOOLE_1:16
.= h_strip(G,j) /\ h_strip(G,j+1) /\ v_strip(G,i) by XBOOLE_1:16;
assume
A7: x in cell(G,i,j) /\ cell(G,i,j+1);
then
A8: x in h_strip(G,j) /\ h_strip(G,j+1) by A6,XBOOLE_0:def 4;
A9: x in v_strip(G,i) by A6,A7,XBOOLE_0:def 4;
A10: i < i+1 by NAT_1:13;
A11: i+1 <= len G by A3,NAT_1:13;
then
A12: G*(i,j+1)`1 < G*(i+1,j+1)`1 by A2,A4,A5,A10,Th3;
A13: G*(i,j+1) = |[G*(i,j+1)`1,G*(i,j+1)`2]| by EUCLID:53;
A14: i+1 >= 1 by NAT_1:11;
G*(i,j+1)`2 = G*(1,j+1)`2 by A2,A3,A4,A5,Th1
.= G*(i+1,j+1)`2 by A4,A5,A11,A14,Th1;
then
A15: G*(i+1,j+1) = |[G*(i+1,j+1)`1,G*(i,j+1)`2]| by EUCLID:53;
reconsider p = x as Point of TOP-REAL 2 by A7;
j+1 <= width G by A1,NAT_1:13;
then p in { q : q`2 = G*(1,j+1)`2 } by A8,Th24;
then ex q st q = p & q`2 = G*(1,j+1)`2;
then
A16: p`2 = G*(i,j+1)`2 by A2,A3,A4,A5,Th1;
p in { |[r,s]| : G*(i,j+1)`1 <= r & r <= G*(i+1,j+1)`1 } by A2,A3,A4,A5,A9
,Th8;
then
A17: ex r,s st ( p = |[r,s]|)&( G*(i,j+1)`1 <= r)&( r <= G*(i+1, j+1)`1);
then
A18: G*(i,j+1)`1 <= p`1 by EUCLID:52;
p`1 <= G*(i+1,j+1)`1 by A17,EUCLID:52;
then p in
{ q : q`2 = G*(i,j+1)`2 & G*(i,j+1)`1 <= q`1 & q`1 <= G*(i+1,j+1)`1 }
by A16,A18;
hence thesis by A12,A13,A15,TOPREAL3:10;
end;
A19: LSeg(G*(i,j+1),G*(i+1,j+1)) c= cell(G,i,j) by A1,A2,A3,Th21;
LSeg(G*(i,j+1),G*(i+1,j+1)) c= cell(G,i,j+1) by A2,A3,A4,A5,Th22;
hence thesis by A19,XBOOLE_1:19;
end;
theorem Th27:
1 <= k & k+1 <= len f & [i+1,j] in Indices GoB f & [i+1,j+1] in
Indices GoB f &
f/.k = (GoB f)*(i+1,j) & f/.(k+1) = (GoB f)*(i+1,j+1) implies
left_cell(f,k) = cell(GoB f,i,j) & right_cell(f,k) = cell(GoB f,i+1,j)
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f and
A3: [i+1,j] in Indices GoB f and
A4: [i+1,j+1] in Indices GoB f and
A5: f/.k = (GoB f)*(i+1,j) and
A6: f/.(k+1) = (GoB f)*(i+1,j+1);
A7: j < j+1 by XREAL_1:29;
A8: j+1 <= j+1+1 by NAT_1:11;
hence left_cell(f,k) = cell(GoB f,i+1-'1,j) by A1,A2,A3,A4,A5,A6,A7,Def7
.= cell(GoB f,i,j) by NAT_D:34;
thus thesis by A1,A2,A3,A4,A5,A6,A7,A8,Def6;
end;
theorem Th28:
1 <= k & k+1 <= len f & [i,j+1] in Indices GoB f & [i+1,j+1] in
Indices GoB f &
f/.k = (GoB f)*(i,j+1) & f/.(k+1) = (GoB f)*(i+1,j+1) implies
left_cell(f,k) = cell(GoB f,i,j+1) & right_cell(f,k) = cell(GoB f,i,j)
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f and
A3: [i,j+1] in Indices GoB f and
A4: [i+1,j+1] in Indices GoB f and
A5: f/.k = (GoB f)*(i,j+1) and
A6: f/.(k+1) = (GoB f)*(i+1,j+1);
A7: i < i+1 by XREAL_1:29;
A8: i+1 <= i+1+1 by NAT_1:11;
hence left_cell(f,k) = cell(GoB f,i,j+1) by A1,A2,A3,A4,A5,A6,A7,Def7;
thus right_cell(f,k) = cell(GoB f,i,j+1-'1) by A1,A2,A3,A4,A5,A6,A7,A8,Def6
.= cell(GoB f,i,j) by NAT_D:34;
end;
theorem Th29:
1 <= k & k+1 <= len f & [i,j+1] in Indices GoB f & [i+1,j+1] in
Indices GoB f &
f/.k = (GoB f)*(i+1,j+1) & f/.(k+1) = (GoB f)*(i,j+1) implies
left_cell(f,k) = cell(GoB f,i,j) & right_cell(f,k) = cell(GoB f,i,j+1)
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f and
A3: [i,j+1] in Indices GoB f and
A4: [i+1,j+1] in Indices GoB f and
A5: f/.k = (GoB f)*(i+1,j+1) and
A6: f/.(k+1) = (GoB f)*(i,j+1);
A7: i < i+1 by XREAL_1:29;
A8: i+1 <= i+1+1 by NAT_1:11;
hence left_cell(f,k) = cell(GoB f,i,j+1-'1) by A1,A2,A3,A4,A5,A6,A7,Def7
.= cell(GoB f,i,j) by NAT_D:34;
thus thesis by A1,A2,A3,A4,A5,A6,A7,A8,Def6;
end;
theorem Th30:
1 <= k & k+1 <= len f & [i+1,j+1] in Indices GoB f & [i+1,j] in
Indices GoB f &
f/.k = (GoB f)*(i+1,j+1) & f/.(k+1) = (GoB f)*(i+1,j) implies
left_cell(f,k) = cell(GoB f,i+1,j) & right_cell(f,k) = cell(GoB f,i,j)
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f and
A3: [i+1,j+1] in Indices GoB f and
A4: [i+1,j] in Indices GoB f and
A5: f/.k = (GoB f)*(i+1,j+1) and
A6: f/.(k+1) = (GoB f)*(i+1,j);
A7: j < j+1 by XREAL_1:29;
A8: j+1 <= j+1+1 by NAT_1:11;
hence left_cell(f,k) = cell(GoB f,i+1,j) by A1,A2,A3,A4,A5,A6,A7,Def7;
thus right_cell(f,k) = cell(GoB f,i+1-'1,j) by A1,A2,A3,A4,A5,A6,A7,A8,Def6
.= cell(GoB f,i,j) by NAT_D:34;
end;
theorem
1 <= k & k+1 <= len f implies left_cell(f,k) /\ right_cell(f,k) = LSeg(f, k )
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f;
k <= k+1 by NAT_1:11;
then k <= len f by A2,XXREAL_0:2;
then
A3: k in dom f by A1,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A4: [i1,j1] in Indices GoB f and
A5: f/.k = (GoB f)*(i1,j1) by Th11;
A6: k+1 in dom f by A2,FINSEQ_3:25,NAT_1:11;
then consider i2,j2 being Nat such that
A7: [i2,j2] in Indices GoB f and
A8: f/.(k+1) = (GoB f)*(i2,j2) by Th11;
A9: |.i1-i2.|+|.j1-j2.| = 1 by A3,A4,A5,A6,A7,A8,Th12;
A10: now per cases by A9,SEQM_3:42;
case that
A11: |.i1-i2.| = 1 and
A12: j1 = j2;
i1-i2 = 1 or -(i1-i2) = 1 by A11,ABSVALUE:def 1;
hence i1 = i2+1 or i1+1 = i2;
thus j1 = j2 by A12;
end;
case that
A13: i1 = i2 and
A14: |.j1-j2.| = 1;
j1-j2 = 1 or -(j1-j2) = 1 by A14,ABSVALUE:def 1;
hence j1 = j2+1 or j1+1 = j2;
thus i1 = i2 by A13;
end;
end;
A15: 0+1 <= j1 by A4,MATRIX_0:32;
A16: j1 <= width GoB f by A4,MATRIX_0:32;
A17: 1 <= j2 by A7,MATRIX_0:32;
A18: j2 <= width GoB f by A7,MATRIX_0:32;
A19: 0+1 <= i1 by A4,MATRIX_0:32;
A20: i1 <= len GoB f by A4,MATRIX_0:32;
A21: 1 <= i2 by A7,MATRIX_0:32;
A22: i2 <= len GoB f by A7,MATRIX_0:32;
i1 > 0 by A19;
then consider i being Nat such that
A23: i+1 = i1 by NAT_1:6;
reconsider i as Nat;
A24: i+1 = i1 by A23;
A25: i < len GoB f by A20,A23,NAT_1:13;
j1 > 0 by A15;
then consider j being Nat such that
A26: j+1 = j1 by NAT_1:6;
reconsider j as Nat;
A27: j+1 = j1 by A26;
A28: j < width GoB f by A16,A26,NAT_1:13;
per cases by A10;
suppose
A29: i1 = i2 & j1+1 = j2;
then
A30: j1 < width GoB f by A18,NAT_1:13;
A31: left_cell(f,k) = cell(GoB f,i,j1) by A1,A2,A4,A5,A7,A8,A23,A29,Th27;
right_cell(f,k) = cell(GoB f,i1, j1 ) by A1,A2,A4,A5,A7,A8,A24,A29,Th27;
hence left_cell(f,k) /\ right_cell(f,k)
= LSeg((GoB f)*(i1,j1),(GoB f)*(i1,j1+1)) by A15,A23,A25,A30,A31,Th25
.= LSeg(f,k) by A1,A2,A5,A8,A29,TOPREAL1:def 3;
end;
suppose
A32: i1+1 = i2 & j1 = j2;
then
A33: i1 < len GoB f by A22,NAT_1:13;
A34: left_cell(f,k) = cell(GoB f,i1,j1) by A1,A2,A4,A5,A7,A8,A27,A32,Th28;
right_cell(f,k) = cell(GoB f,i1, j ) by A1,A2,A4,A5,A7,A8,A26,A32,Th28;
hence left_cell(f,k) /\ right_cell(f,k)
= LSeg((GoB f)*(i1,j1),(GoB f)*(i1+1,j1)) by A19,A26,A28,A33,A34,Th26
.= LSeg(f,k) by A1,A2,A5,A8,A32,TOPREAL1:def 3;
end;
suppose
A35: i1 = i2+1 & j1 = j2;
then
A36: i2 < len GoB f by A20,NAT_1:13;
A37: left_cell(f,k) = cell(GoB f,i2,j) by A1,A2,A4,A5,A7,A8,A26,A35,Th29;
right_cell(f,k) = cell(GoB f,i2, j1 ) by A1,A2,A4,A5,A7,A8,A27,A35,Th29;
hence left_cell(f,k) /\ right_cell(f,k)
= LSeg((GoB f)*(i2+1,j1),(GoB f)*(i2,j1)) by A21,A26,A28,A36,A37,Th26
.= LSeg(f,k) by A1,A2,A5,A8,A35,TOPREAL1:def 3;
end;
suppose
A38: i1 = i2 & j1 = j2+1;
then
A39: j2 < width GoB f by A16,NAT_1:13;
A40: left_cell(f,k) = cell(GoB f,i1,j2) by A1,A2,A4,A5,A7,A8,A24,A38,Th30;
right_cell(f,k) = cell(GoB f,i, j2 ) by A1,A2,A4,A5,A7,A8,A23,A38,Th30;
hence left_cell(f,k) /\ right_cell(f,k)
= LSeg((GoB f)*(i1,j2+1),(GoB f)*(i1,j2)) by A17,A23,A25,A39,A40,Th25
.= LSeg(f,k) by A1,A2,A5,A8,A38,TOPREAL1:def 3;
end;
end;