:: Some Properties of Cells on Go Board
:: by Czes{\l}aw Byli\'nski
::
:: Received April 23, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, XBOOLE_0, FINSEQ_1, EUCLID, FUNCT_1,
RELAT_1, TARSKI, NAT_1, MATRIX_1, TREES_1, XXREAL_0, CARD_1, GOBOARD1,
PARTFUN1, ARYTM_3, MCART_1, ARYTM_1, GOBOARD5, GOBOARD2, PRE_TOPC,
RLTOPSP1, COMPLEX1, RCOMP_1, RFINSEQ, ORDINAL4, GOBRD13;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, COMPLEX1, NAT_D, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1,
FINSEQ_2, RFINSEQ, XXREAL_0, SEQ_4, STRUCT_0, MATRIX_0, MATRIX_1,
PRE_TOPC, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5;
constructors RFINSEQ, NAT_D, GOBOARD2, GOBOARD5, REAL_1, GOBOARD1, RELSET_1,
SEQ_4, RVSUM_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0,
EUCLID, GOBOARD2, GOBOARD5, VALUED_0, SEQ_4, NAT_1, MATRIX_0;
requirements NUMERALS, REAL, SUBSET, ARITHM;
definitions TARSKI;
theorems NAT_1, FINSEQ_1, MATRIX_0, GOBOARD1, EUCLID, FINSEQ_3, FINSEQ_5,
TOPREAL1, GOBOARD5, ABSVALUE, FUNCT_1, FINSEQ_2, GOBRD11, GOBOARD2,
SPRECT_3, JORDAN5D, FINSEQ_4, RFINSEQ, JORDAN8, PARTFUN2, XREAL_1,
XXREAL_0, NAT_D, SEQM_3, SEQ_4;
begin
reserve i,i1,i2,i9,i19,j,j1,j2,j9,j19,k,k1,k2,l,m,n for Nat;
reserve r,s,r9,s9 for Real;
reserve D for non empty set, f for FinSequence of D;
reserve f for FinSequence of TOP-REAL 2, G for Go-board;
::$CT 7
theorem
for G being Matrix of TOP-REAL 2 holds f is_sequence_on G implies rng
f c= Values G
proof
let G be Matrix of TOP-REAL 2;
assume
A1: f is_sequence_on G;
let y be object;
assume y in rng f;
then consider n being Element of NAT such that
A2: n in dom f and
A3: f/.n = y by PARTFUN2:2;
ex i,j st [i,j] in Indices G & f/.n = G*(i,j) by A1,A2,GOBOARD1:def 9;
then y in { G*(i,j): [i,j] in Indices G } by A3;
hence thesis by MATRIX_0:39;
end;
theorem Th2:
for G1,G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in
Indices G1 & 1 <= j2 & j2 <= width G2 & G1*(i1,j1) = G2*(1,j2) holds i1 = 1
proof
let G1,G2 be Go-board such that
A1: Values G1 c= Values G2 and
A2: [i1,j1] in Indices G1 and
A3: 1 <= j2 & j2 <= width G2 and
A4: G1*(i1,j1) = G2*(1,j2);
set p = G1*(1,j1);
A5: 1 <= j1 & j1 <= width G1 by A2,MATRIX_0:32;
assume
A6: i1 <> 1;
1 <= i1 by A2,MATRIX_0:32;
then
A7: 1 < i1 by A6,XXREAL_0:1;
i1 <= len G1 by A2,MATRIX_0:32;
then
A8: p`1 < G1*(i1,j1)`1 by A5,A7,GOBOARD5:3;
0 <> len G1 by MATRIX_0:def 10;
then 1 <= len G1 by NAT_1:14;
then [1,j1] in Indices G1 by A5,MATRIX_0:30;
then p in {G1*(i,j): [i,j] in Indices G1};
then p in Values G1 by MATRIX_0:39;
then p in Values G2 by A1;
then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
then consider i,j such that
A9: p = G2*(i,j) and
A10: [i,j] in Indices G2;
A11: 1 <= j & j <= width G2 by A10,MATRIX_0:32;
0 <> len G2 by MATRIX_0:def 10;
then
A12: 1 <= len G2 by NAT_1:14;
then
A13: G2*(1,j)`1 = G2*(1,1)`1 by A11,GOBOARD5:2
.= G2*(1,j2)`1 by A3,A12,GOBOARD5:2;
A14: i <= len G2 by A10,MATRIX_0:32;
1 <= i by A10,MATRIX_0:32;
then 1 < i by A4,A8,A9,A13,XXREAL_0:1;
hence contradiction by A4,A8,A9,A14,A11,A13,GOBOARD5:3;
end;
theorem Th3:
for G1,G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in
Indices G1 & 1 <= j2 & j2 <= width G2 & G1*(i1,j1) = G2*(len G2,j2) holds i1 =
len G1
proof
let G1,G2 be Go-board such that
A1: Values G1 c= Values G2 and
A2: [i1,j1] in Indices G1 and
A3: 1 <= j2 & j2 <= width G2 and
A4: G1*(i1,j1) = G2*(len G2,j2);
set p = G1*(len G1,j1);
A5: 1 <= j1 & j1 <= width G1 by A2,MATRIX_0:32;
assume
A6: i1 <> len G1;
i1 <= len G1 by A2,MATRIX_0:32;
then
A7: i1 < len G1 by A6,XXREAL_0:1;
1 <= i1 by A2,MATRIX_0:32;
then
A8: G1*(i1,j1)`1 < p`1 by A5,A7,GOBOARD5:3;
0 <> len G1 by MATRIX_0:def 10;
then 1 <= len G1 by NAT_1:14;
then [len G1,j1] in Indices G1 by A5,MATRIX_0:30;
then p in {G1*(i,j): [i,j] in Indices G1};
then p in Values G1 by MATRIX_0:39;
then p in Values G2 by A1;
then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
then consider i,j such that
A9: p = G2*(i,j) and
A10: [i,j] in Indices G2;
A11: 1 <= j & j <= width G2 by A10,MATRIX_0:32;
0 <> len G2 by MATRIX_0:def 10;
then
A12: 1 <= len G2 by NAT_1:14;
then
A13: G2*(len G2,j)`1 = G2*(len G2,1)`1 by A11,GOBOARD5:2
.= G2*(len G2,j2)`1 by A3,A12,GOBOARD5:2;
A14: 1 <= i by A10,MATRIX_0:32;
i <= len G2 by A10,MATRIX_0:32;
then i < len G2 by A4,A8,A9,A13,XXREAL_0:1;
hence contradiction by A4,A8,A9,A14,A11,A13,GOBOARD5:3;
end;
theorem Th4:
for G1,G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in
Indices G1 & 1 <= i2 & i2 <= len G2 & G1*(i1,j1) = G2*(i2,1) holds j1 = 1
proof
let G1,G2 be Go-board such that
A1: Values G1 c= Values G2 and
A2: [i1,j1] in Indices G1 and
A3: 1 <= i2 & i2 <= len G2 and
A4: G1*(i1,j1) = G2*(i2,1);
set p = G1*(i1,1);
A5: 1 <= i1 & i1 <= len G1 by A2,MATRIX_0:32;
assume
A6: j1 <> 1;
1 <= j1 by A2,MATRIX_0:32;
then
A7: 1 < j1 by A6,XXREAL_0:1;
j1 <= width G1 by A2,MATRIX_0:32;
then
A8: p`2 < G1*(i1,j1)`2 by A5,A7,GOBOARD5:4;
0 <> width G1 by MATRIX_0:def 10;
then 1 <= width G1 by NAT_1:14;
then [i1,1] in Indices G1 by A5,MATRIX_0:30;
then p in {G1*(i,j): [i,j] in Indices G1};
then p in Values G1 by MATRIX_0:39;
then p in Values G2 by A1;
then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
then consider i,j such that
A9: p = G2*(i,j) and
A10: [i,j] in Indices G2;
A11: 1 <= i & i <= len G2 by A10,MATRIX_0:32;
0 <> width G2 by MATRIX_0:def 10;
then
A12: 1 <= width G2 by NAT_1:14;
then
A13: G2*(i,1)`2 = G2*(1,1)`2 by A11,GOBOARD5:1
.= G2*(i2,1)`2 by A3,A12,GOBOARD5:1;
A14: j <= width G2 by A10,MATRIX_0:32;
1 <= j by A10,MATRIX_0:32;
then 1 < j by A4,A8,A9,A13,XXREAL_0:1;
hence contradiction by A4,A8,A9,A11,A14,A13,GOBOARD5:4;
end;
theorem Th5:
for G1,G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in
Indices G1 & 1 <= i2 & i2 <= len G2 & G1*(i1,j1) = G2*(i2,width G2) holds j1 =
width G1
proof
let G1,G2 be Go-board such that
A1: Values G1 c= Values G2 and
A2: [i1,j1] in Indices G1 and
A3: 1 <= i2 & i2 <= len G2 and
A4: G1*(i1,j1) = G2*(i2,width G2);
set p = G1*(i1,width G1);
A5: 1 <= i1 & i1 <= len G1 by A2,MATRIX_0:32;
assume
A6: j1 <> width G1;
j1 <= width G1 by A2,MATRIX_0:32;
then
A7: j1 < width G1 by A6,XXREAL_0:1;
1 <= j1 by A2,MATRIX_0:32;
then
A8: G1*(i1,j1)`2 < p`2 by A5,A7,GOBOARD5:4;
0 <> width G1 by MATRIX_0:def 10;
then 1 <= width G1 by NAT_1:14;
then [i1,width G1] in Indices G1 by A5,MATRIX_0:30;
then p in {G1*(i,j): [i,j] in Indices G1};
then p in Values G1 by MATRIX_0:39;
then p in Values G2 by A1;
then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
then consider i,j such that
A9: p = G2*(i,j) and
A10: [i,j] in Indices G2;
A11: 1 <= i & i <= len G2 by A10,MATRIX_0:32;
0 <> width G2 by MATRIX_0:def 10;
then
A12: 1 <= width G2 by NAT_1:14;
then
A13: G2*(i,width G2)`2 = G2*(1,width G2)`2 by A11,GOBOARD5:1
.= G2*(i2,width G2)`2 by A3,A12,GOBOARD5:1;
A14: 1 <= j by A10,MATRIX_0:32;
j <= width G2 by A10,MATRIX_0:32;
then j < width G2 by A4,A8,A9,A13,XXREAL_0:1;
hence contradiction by A4,A8,A9,A11,A14,A13,GOBOARD5:4;
end;
theorem Th6:
for G1,G2 being Go-board st Values G1 c= Values G2 & 1 <= i1 &
i1 < len G1 & 1 <= j1 & j1 <= width G1 & 1 <= i2 & i2 < len G2 & 1 <= j2 & j2
<= width G2 & G1*(i1,j1) = G2*(i2,j2) holds G2*(i2+1,j2)`1 <= G1*(i1+1,j1)`1
proof
let G1,G2 be Go-board such that
A1: Values G1 c= Values G2 and
A2: 1 <= i1 and
A3: i1 < len G1 and
A4: 1 <= j1 & j1 <= width G1 and
A5: 1 <= i2 and
A6: i2 < len G2 and
A7: 1 <= j2 & j2 <= width G2 and
A8: G1*(i1,j1) = G2*(i2,j2);
set p = G1*(i1+1,j1);
A9: i1+1 <= len G1 by A3,NAT_1:13;
1 <= i1+1 by A2,NAT_1:13;
then [i1+1,j1] in Indices G1 by A4,A9,MATRIX_0:30;
then p in {G1*(i,j): [i,j] in Indices G1};
then p in Values G1 by MATRIX_0:39;
then p in Values G2 by A1;
then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
then consider i,j such that
A10: p = G2*(i,j) and
A11: [i,j] in Indices G2;
A12: 1 <= i by A11,MATRIX_0:32;
A13: i <= len G2 by A11,MATRIX_0:32;
1 <= j & j <= width G2 by A11,MATRIX_0:32;
then
A14: G2*(i,j)`1 = G2*(i,1)`1 by A12,A13,GOBOARD5:2
.= G2*(i,j2)`1 by A7,A12,A13,GOBOARD5:2;
i1 < i1+1 by NAT_1:13;
then
A15: G2*(i2,j2)`1 < G2*(i,j2)`1 by A2,A4,A8,A9,A10,A14,GOBOARD5:3;
A16: now
assume i <= i2;
then i = i2 or i < i2 by XXREAL_0:1;
hence contradiction by A6,A7,A12,A15,GOBOARD5:3;
end;
assume
A17: p`1 < G2*(i2+1,j2)`1;
A18: 1 <= i2+1 by A5,NAT_1:13;
now
assume i2+1 <= i;
then i2+1 = i or i2+1 < i by XXREAL_0:1;
hence contradiction by A7,A17,A10,A13,A14,A18,GOBOARD5:3;
end;
hence contradiction by A16,NAT_1:13;
end;
theorem Th7:
for G1,G2 being Go-board st G1*(i1-'1,j1) in Values G2 & 1 < i1
& i1 <= len G1 & 1 <= j1 & j1 <= width G1 & 1 < i2 & i2 <= len G2 & 1 <= j2 &
j2 <= width G2 & G1*(i1,j1) = G2*(i2,j2) holds G1*(i1-'1,j1)`1 <= G2*(i2-'1,j2)
`1
proof
let G1,G2 be Go-board such that
A1: G1*(i1-'1,j1) in Values G2 and
A2: 1 < i1 and
A3: i1 <= len G1 & 1 <= j1 & j1 <= width G1 and
A4: 1 < i2 and
A5: i2 <= len G2 and
A6: 1 <= j2 & j2 <= width G2 and
A7: G1*(i1,j1) = G2*(i2,j2);
set p = G1*(i1-'1,j1);
A8: p in {G2*(i,j): [i,j] in Indices G2} by A1,MATRIX_0:39;
1 <= i2-'1 by A4,NAT_D:49;
then i2-'1 < i2 by NAT_D:51;
then
A9: i2-'1 < len G2 by A5,XXREAL_0:2;
consider i,j such that
A10: p = G2*(i,j) and
A11: [i,j] in Indices G2 by A8;
A12: 1 <= i by A11,MATRIX_0:32;
A13: i <= len G2 by A11,MATRIX_0:32;
1 <= j & j <= width G2 by A11,MATRIX_0:32;
then
A14: G2*(i,j)`1 = G2*(i,1)`1 by A12,A13,GOBOARD5:2
.= G2*(i,j2)`1 by A6,A12,A13,GOBOARD5:2;
A15: 1 <= i1-'1 by A2,NAT_D:49;
then i1-'1 < i1 by NAT_D:51;
then
A16: G2*(i,j2)`1 < G2*(i2,j2)`1 by A3,A7,A15,A10,A14,GOBOARD5:3;
A17: now
assume i2 <= i;
then i = i2 or i2 < i by XXREAL_0:1;
hence contradiction by A4,A6,A13,A16,GOBOARD5:3;
end;
assume
A18: G2*(i2-'1,j2)`1 < p`1;
now
assume i <= i2-'1;
then i2-'1 = i or i < i2-'1 by XXREAL_0:1;
hence contradiction by A6,A18,A10,A12,A14,A9,GOBOARD5:3;
end;
hence contradiction by A17,NAT_D:49;
end;
theorem Th8:
for G1,G2 being Go-board st G1*(i1,j1+1) in Values G2 & 1 <= i1
& i1 <= len G1 & 1 <= j1 & j1 < width G1 & 1 <= i2 & i2 <= len G2 & 1 <= j2 &
j2 < width G2 & G1*(i1,j1) = G2*(i2,j2) holds G2*(i2,j2+1)`2 <= G1*(i1,j1+1)`2
proof
let G1,G2 be Go-board such that
A1: G1*(i1,j1+1) in Values G2 and
A2: 1 <= i1 & i1 <= len G1 & 1 <= j1 and
A3: j1 < width G1 and
A4: 1 <= i2 & i2 <= len G2 and
A5: 1 <= j2 and
A6: j2 < width G2 and
A7: G1*(i1,j1) = G2*(i2,j2);
set p = G1*(i1,j1+1);
p in {G2*(i,j): [i,j] in Indices G2} by A1,MATRIX_0:39;
then consider i,j such that
A8: p = G2*(i,j) and
A9: [i,j] in Indices G2;
A10: 1 <= j by A9,MATRIX_0:32;
A11: j <= width G2 by A9,MATRIX_0:32;
1 <= i & i <= len G2 by A9,MATRIX_0:32;
then
A12: G2*(i,j)`2 = G2*(1,j)`2 by A10,A11,GOBOARD5:1
.= G2*(i2,j)`2 by A4,A10,A11,GOBOARD5:1;
j1 < j1+1 & j1+1 <= width G1 by A3,NAT_1:13;
then
A13: G2*(i2,j2)`2 < G2*(i2,j)`2 by A2,A7,A8,A12,GOBOARD5:4;
A14: now
assume j <= j2;
then j = j2 or j < j2 by XXREAL_0:1;
hence contradiction by A4,A6,A10,A13,GOBOARD5:4;
end;
assume
A15: p`2 < G2*(i2,j2+1)`2;
A16: 1 <= j2+1 by A5,NAT_1:13;
now
assume j2+1 <= j;
then j2+1 = j or j2+1 < j by XXREAL_0:1;
hence contradiction by A4,A15,A8,A11,A12,A16,GOBOARD5:4;
end;
hence contradiction by A14,NAT_1:13;
end;
theorem Th9:
for G1,G2 being Go-board st Values G1 c= Values G2 & 1 <= i1 &
i1 <= len G1 & 1 < j1 & j1 <= width G1 & 1 <= i2 & i2 <= len G2 & 1 < j2 & j2
<= width G2 & G1*(i1,j1) = G2*(i2,j2) holds G1*(i1,j1-'1)`2 <= G2*(i2,j2-'1)`2
proof
let G1,G2 be Go-board such that
A1: Values G1 c= Values G2 and
A2: 1 <= i1 & i1 <= len G1 and
A3: 1 < j1 and
A4: j1 <= width G1 and
A5: 1 <= i2 & i2 <= len G2 and
A6: 1 < j2 and
A7: j2 <= width G2 and
A8: G1*(i1,j1) = G2*(i2,j2);
set p = G1*(i1,j1-'1);
A9: 1 <= j1-'1 by A3,NAT_D:49;
then
A10: j1-'1 < j1 by NAT_D:51;
then j1-'1 < width G1 by A4,XXREAL_0:2;
then [i1,j1-'1] in Indices G1 by A2,A9,MATRIX_0:30;
then p in {G1*(i,j): [i,j] in Indices G1};
then p in Values G1 by MATRIX_0:39;
then p in Values G2 by A1;
then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
then consider i,j such that
A11: p = G2*(i,j) and
A12: [i,j] in Indices G2;
A13: 1 <= j by A12,MATRIX_0:32;
A14: j <= width G2 by A12,MATRIX_0:32;
1 <= i & i <= len G2 by A12,MATRIX_0:32;
then
A15: G2*(i,j)`2 = G2*(1,j)`2 by A13,A14,GOBOARD5:1
.= G2*(i2,j)`2 by A5,A13,A14,GOBOARD5:1;
then
A16: G2*(i2,j)`2 < G2*(i2,j2)`2 by A2,A4,A8,A9,A10,A11,GOBOARD5:4;
A17: now
assume j2 <= j;
then j = j2 or j2 < j by XXREAL_0:1;
hence contradiction by A5,A6,A14,A16,GOBOARD5:4;
end;
1 <= j2-'1 by A6,NAT_D:49;
then j2-'1 < j2 by NAT_D:51;
then
A18: j2-'1 < width G2 by A7,XXREAL_0:2;
assume
A19: G2*(i2,j2-'1)`2 < p`2;
now
assume j <= j2-'1;
then j2-'1 = j or j < j2-'1 by XXREAL_0:1;
hence contradiction by A5,A19,A11,A13,A15,A18,GOBOARD5:4;
end;
hence contradiction by A17,NAT_D:49;
end;
theorem Th10:
for G1,G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in
Indices G1 & [i2,j2] in Indices G2 & G1*(i1,j1) = G2*(i2,j2) holds cell(G2,i2,
j2) c= cell(G1,i1,j1)
proof
let G1,G2 be Go-board such that
A1: Values G1 c= Values G2 and
A2: [i1,j1] in Indices G1 and
A3: [i2,j2] in Indices G2 and
A4: G1*(i1,j1) = G2*(i2,j2);
A5: 1 <= i1 by A2,MATRIX_0:32;
A6: j1 <= width G1 by A2,MATRIX_0:32;
let p be object such that
A7: p in cell(G2,i2,j2);
A8: 1 <= i2 by A3,MATRIX_0:32;
A9: j2 <= width G2 by A3,MATRIX_0:32;
A10: 1 <= j2 by A3,MATRIX_0:32;
A11: i2 <= len G2 by A3,MATRIX_0:32;
then
A12: G2*(i2,j2)`1 = G2*(i2,1)`1 & G2*(i2,j2)`2 = G2*(1,j2)`2 by A8,A10,A9,
GOBOARD5:1,2;
A13: 1 <= j1 by A2,MATRIX_0:32;
A14: i1 <= len G1 by A2,MATRIX_0:32;
then
A15: G1*(i1,j1)`1 = G1*(i1,1)`1 & G1*(i1,j1)`2 = G1*(1,j1)`2 by A5,A13,A6,
GOBOARD5:1,2;
per cases by A11,A9,XXREAL_0:1;
suppose
A16: i2 = len G2 & j2 = width G2;
then
A17: p in { |[r,s]| : G2*(i2,j2)`1 <= r & G2*(i2,j2)`2 <= s } by A7,A12,
GOBRD11:28;
i1 = len G1 & j1 = width G1 by A1,A2,A4,A8,A10,A16,Th3,Th5;
hence thesis by A4,A15,A17,GOBRD11:28;
end;
suppose
A18: i2 = len G2 & j2 < width G2;
then p in { |[r,s]| : G2*(i2,j2)`1 <= r & G2*(i2,j2)`2 <= s & s <= G2*(1,
j2+1)`2 } by A7,A10,A12,GOBRD11:29;
then consider r9,s9 such that
A19: p = |[r9,s9]| & G2*(i2,j2)`1 <= r9 & G2*(i2,j2)`2 <= s9 and
A20: s9 <= G2*(1,j2+1)`2;
A21: i1 = len G1 by A1,A2,A4,A10,A18,Th3;
now
per cases by A6,XXREAL_0:1;
suppose
A22: j1 = width G1;
p in { |[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s} by A4,A19;
hence thesis by A15,A21,A22,GOBRD11:28;
end;
suppose
A23: j1 < width G1;
1 <= j2+1 & j2+1 <= width G2 by A18,NAT_1:12,13;
then
A24: G2*(i2,j2+1)`2 = G2*(1,j2+1)`2 by A8,A11,GOBOARD5:1;
1 <= j1+1 & j1+1 <= width G1 by A23,NAT_1:12,13;
then
G1*(i1,j1+1) in Values G1 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 by A5,A14,
GOBOARD5:1,MATRIX_0:41;
then G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A5,A14,A13,A8,A10,A18,A23
,A24,Th8;
then s9 <= G1*(1,j1+1)`2 by A20,XXREAL_0:2;
then
p in {|[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s & s <= G1*(
1,j1+1)`2} by A4,A19;
hence thesis by A13,A15,A21,A23,GOBRD11:29;
end;
end;
hence thesis;
end;
suppose
A25: i2 < len G2 & j2 = width G2;
then p in {|[r,s]|: G2*(i2,j2)`1 <= r & r <= G2*(i2+1,1)`1 & G2*(i2,j2)`2
<= s} by A7,A8,A12,GOBRD11:31;
then consider r9,s9 such that
A26: p = |[r9,s9]| & G2*(i2,j2)`1 <= r9 and
A27: r9 <= G2*(i2+1,1)`1 and
A28: G2*(i2,j2)`2 <= s9;
A29: j1 = width G1 by A1,A2,A4,A8,A25,Th5;
now
per cases by A14,XXREAL_0:1;
suppose
A30: i1 = len G1;
p in { |[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s} by A4,A26,A28;
hence thesis by A15,A29,A30,GOBRD11:28;
end;
suppose
A31: i1 < len G1;
1 <= i2+1 & i2+1 <= len G2 by A25,NAT_1:12,13;
then
A32: G2*(i2+1,j2)`1 = G2*(i2+1,1)`1 by A10,A9,GOBOARD5:2;
1 <= i1+1 & i1+1 <= len G1 by A31,NAT_1:12,13;
then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A13,A6,GOBOARD5:2;
then G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A13,A6,A8,A10,A25,A31
,A32,Th6;
then r9 <= G1*(i1+1,1)`1 by A27,XXREAL_0:2;
then
p in {|[r,s]|: G1*(i1,j1)`1 <= r & r <= G1*(i1+1,1)`1 & G1*(i1,j1
)`2 <= s} by A4,A26,A28;
hence thesis by A5,A15,A29,A31,GOBRD11:31;
end;
end;
hence thesis;
end;
suppose
A33: i2 < len G2 & j2 < width G2;
then 1 <= j2+1 & j2+1 <= width G2 by NAT_1:12,13;
then
A34: G2*(i2,j2+1)`2 = G2*(1,j2+1)`2 by A8,A11,GOBOARD5:1;
1 <= i2+1 & i2+1 <= len G2 by A33,NAT_1:12,13;
then G2*(i2+1,j2)`1 = G2*(i2+1,1)`1 by A10,A9,GOBOARD5:2;
then
p in { |[r,s]| : G2*(i2,j2)`1 <= r & r <= G2*(i2+1,j2)`1 & G2*(i2,j2)
`2 <= s & s <= G2*(i2,j2+1)`2 } by A7,A8,A10,A12,A33,A34,GOBRD11:32;
then consider r9,s9 such that
A35: p = |[r9,s9]| & G2*(i2,j2)`1 <= r9 and
A36: r9 <= G2*(i2+1,j2)`1 and
A37: G2*(i2,j2)`2 <= s9 and
A38: s9 <= G2*(i2,j2+1)`2;
now
per cases by A14,A6,XXREAL_0:1;
suppose
A39: i1 = len G1 & j1 = width G1;
p in { |[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s } by A4,A35,A37;
hence thesis by A15,A39,GOBRD11:28;
end;
suppose
A40: i1 = len G1 & j1 < width G1;
then 1 <= j1+1 & j1+1 <= width G1 by NAT_1:12,13;
then
G1*(i1,j1+1) in Values G1 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 by A5,A14,
GOBOARD5:1,MATRIX_0:41;
then G2*(i2,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A5,A13,A8,A10,A33,A40
,Th8;
then s9 <= G1*(1,j1+1)`2 by A38,XXREAL_0:2;
then p in {|[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s & s <= G1*
(1,j1+1)`2} by A4,A35,A37;
hence thesis by A13,A15,A40,GOBRD11:29;
end;
suppose
A41: i1 < len G1 & j1 = width G1;
then 1 <= i1+1 & i1+1 <= len G1 by NAT_1:12,13;
then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A13,A6,GOBOARD5:2;
then G2*(i2+1,j2)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A13,A8,A10,A33,A41
,Th6;
then r9 <= G1*(i1+1,1)`1 by A36,XXREAL_0:2;
then
p in {|[r,s]|: G1*(i1,j1)`1 <= r & r <= G1*(i1+1,1)`1 & G1*(i1,j1
)`2 <= s} by A4,A35,A37;
hence thesis by A5,A15,A41,GOBRD11:31;
end;
suppose
A42: i1 < len G1 & j1 < width G1;
then 1 <= i1+1 & i1+1 <= len G1 by NAT_1:12,13;
then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A13,A6,GOBOARD5:2;
then G2*(i2+1,j2)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A13,A8,A10,A33,A42
,Th6;
then
A43: r9 <= G1*(i1+1,1)`1 by A36,XXREAL_0:2;
1 <= j1+1 & j1+1 <= width G1 by A42,NAT_1:12,13;
then
G1*(i1,j1+1) in Values G1 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 by A5,A14,
GOBOARD5:1,MATRIX_0:41;
then G2*(i2,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A5,A13,A8,A10,A33,A42
,Th8;
then s9 <= G1*(1,j1+1)`2 by A38,XXREAL_0:2;
then
p in { |[r,s]| : G1*(i1,1)`1 <= r & r <= G1*(i1+1,1)`1 & G1*(1,j1
)`2 <= s & s <= G1*(1,j1+1)`2 } by A4,A15,A35,A37,A43;
hence thesis by A5,A13,A42,GOBRD11:32;
end;
end;
hence thesis;
end;
end;
theorem Th11:
for G1,G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in
Indices G1 & [i2,j2] in Indices G2 & G1*(i1,j1) = G2*(i2,j2) holds cell(G2,i2-'
1,j2) c= cell(G1,i1-'1,j1)
proof
let G1,G2 be Go-board such that
A1: Values G1 c= Values G2 and
A2: [i1,j1] in Indices G1 and
A3: [i2,j2] in Indices G2 and
A4: G1*(i1,j1) = G2*(i2,j2);
A5: i2 <= len G2 by A3,MATRIX_0:32;
A6: j1 <= width G1 by A2,MATRIX_0:32;
A7: 1 <= j1 by A2,MATRIX_0:32;
A8: j2 <= width G2 by A3,MATRIX_0:32;
A9: 1 <= j2 by A3,MATRIX_0:32;
A10: 1 <= i2 by A3,MATRIX_0:32;
then
A11: G2*(i2,j2)`1 = G2*(i2,1)`1 by A5,A9,A8,GOBOARD5:2;
A12: G2*(i2,j2)`2 = G2*(1,j2)`2 by A10,A5,A9,A8,GOBOARD5:1;
let p be object such that
A13: p in cell(G2,i2-'1,j2);
A14: 1 <= i1 by A2,MATRIX_0:32;
A15: i1 <= len G1 by A2,MATRIX_0:32;
per cases by A14,A10,XXREAL_0:1;
suppose
A16: i1 = 1 & i2 = 1;
then
A17: i1-'1 = 0 by XREAL_1:232;
A18: i2-'1 = 0 by A16,XREAL_1:232;
now
per cases by A8,XXREAL_0:1;
suppose
A19: j2 = width G2;
then
A20: j1 = width G1 by A1,A2,A4,A10,A5,Th5;
p in { |[r,s]| : r <= G2*(1,1)`1 & G2*(1,width G2)`2 <= s } by A13,A18
,A19,GOBRD11:25;
then consider r9,s9 such that
A21: p = |[r9,s9]| and
A22: r9 <= G2*(1,1)`1 and
A23: G2*(1,width G2)`2 <= s9;
G2*(1,1)`1 = G2*(i1,j2)`1 by A5,A9,A8,A16,GOBOARD5:2;
then r9 <= G1*(1,1)`1 by A4,A15,A7,A6,A16,A22,GOBOARD5:2;
then
p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,width G1)`2 <= s } by A4,A16
,A19,A21,A23,A20;
hence thesis by A17,A20,GOBRD11:25;
end;
suppose
A24: j2 < width G2;
then
p in {|[r,s]|: r <= G2*(1,1)`1 & G2*(1,j2)`2 <= s & s <= G2*(1,j2
+1)`2} by A13,A9,A18,GOBRD11:26;
then consider r9,s9 such that
A25: p = |[r9,s9]| and
A26: r9 <= G2*(1,1)`1 and
A27: G2*(1,j2)`2 <= s9 and
A28: s9 <= G2*(1,j2+1)`2;
G2*(1,1)`1 = G2*(i1,j2)`1 by A5,A9,A8,A16,GOBOARD5:2;
then
A29: r9 <= G1*(1,1)`1 by A4,A15,A7,A6,A16,A26,GOBOARD5:2;
now
per cases by A6,XXREAL_0:1;
suppose
A30: j1 = width G1;
then p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,width G1)`2 <= s }
by A4,A16,A25,A27,A29;
hence thesis by A17,A30,GOBRD11:25;
end;
suppose
A31: j1 < width G1;
then 1 <= j1 + 1 & j1 + 1 <= width G1 by NAT_1:11,13;
then G1*(i1,j1+1) in Values G1 by A14,A15,MATRIX_0:41;
then
G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A15,A7,A5,A9,A16,A24,A31
,Th8;
then s9 <= G1*(1,j1+1)`2 by A28,XXREAL_0:2;
then
p in {|[r,s]|: r <= G1*(1,1)`1 & G1*(1,j1)`2 <= s & s <= G1*(
1,j1+1)`2} by A4,A16,A25,A27,A29;
hence thesis by A7,A17,A31,GOBRD11:26;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose that
A32: i1 = 1 and
A33: 1 < i2;
A34: i1-'1 = 0 by A32,XREAL_1:232;
A35: 1 <= i2-'1 by A33,NAT_D:49;
then i2-'1 < i2 by NAT_D:51;
then
A36: i2-'1 < len G2 by A5,XXREAL_0:2;
A37: i2-'1+1 = i2 by A33,XREAL_1:235;
now
per cases by A8,XXREAL_0:1;
suppose
A38: j2 = width G2;
then
p in { |[r,s]|: G2*(i2-'1,1)`1 <= r & r <= G2*(i2,1)`1 & G2*(1,j2
)`2 <= s} by A13,A35,A36,A37,GOBRD11:31;
then consider r9,s9 such that
A39: p = |[r9,s9]| and
G2*(i2-'1,1)`1 <= r9 and
A40: r9 <= G2*(i2,1)`1 & G2*(1,j2)`2 <= s9;
r9 <= G1*(1,1)`1 & G1*(1,j1)`2 <= s9 by A4,A15,A7,A6,A11,A12,A32,A40,
GOBOARD5:2;
then
A41: p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,j1)`2 <= s } by A39;
j1 = width G1 by A1,A2,A4,A10,A5,A38,Th5;
hence thesis by A34,A41,GOBRD11:25;
end;
suppose
A42: j2 < width G2;
then p in { |[r,s]| : G2*(i2-'1,1)`1 <= r & r <= G2*(i2,1)`1 & G2*(1,
j2)`2 <= s & s <= G2*(1,j2+1)`2 } by A13,A9,A35,A36,A37,GOBRD11:32;
then consider r9,s9 such that
A43: p = |[r9,s9]| and
G2*(i2-'1,1)`1 <= r9 and
A44: r9 <= G2*(i2,1)`1 & G2*(1,j2)`2 <= s9 and
A45: s9 <= G2*(1,j2+1)`2;
A46: r9 <= G1*(1,1)`1 & G1*(1,j1)`2 <= s9 by A4,A15,A7,A6,A11,A12,A32,A44,
GOBOARD5:2;
now
per cases by A6,XXREAL_0:1;
suppose
A47: j1 = width G1;
then p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,width G1)`2 <= s }
by A43,A46;
hence thesis by A34,A47,GOBRD11:25;
end;
suppose
A48: j1 < width G1;
1 <= j2+1 & j2+1 <= width G2 by A42,NAT_1:12,13;
then
A49: G2*(i2,j2+1)`2 = G2*(1,j2+1)`2 by A10,A5,GOBOARD5:1;
1 <= j1+1 & j1+1 <= width G1 by A48,NAT_1:12,13;
then
G1*(i1,j1+1) in Values G1 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 by A14
,A15,GOBOARD5:1,MATRIX_0:41;
then
G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A14,A15,A7,A10,A5,A9,A42
,A48,A49,Th8;
then s9 <= G1*(1,j1+1)`2 by A45,XXREAL_0:2;
then
p in {|[r,s]|: r <= G1*(1,1)`1 & G1*(1,j1)`2 <= s & s <= G1*(
1,j1+1)`2} by A43,A46;
hence thesis by A7,A34,A48,GOBRD11:26;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
1 < i1 & i2 = 1;
hence thesis by A1,A2,A4,A9,A8,Th2;
end;
suppose
A50: 1 < i1 & 1 < i2;
then
A51: 1 <= i2-'1 by NAT_D:49;
then
A52: i2-'1+1 = i2 by NAT_D:43;
i2-'1 < i2 by A51,NAT_D:51;
then
A53: i2-'1 < len G2 by A5,XXREAL_0:2;
then
A54: G2*(i2-'1,1)`1 = G2*(i2-'1,j2)`1 by A9,A8,A51,GOBOARD5:2;
A55: 1 <= i1-'1 by A50,NAT_D:49;
then
A56: i1-'1+1 = i1 by NAT_D:43;
i1-'1 < i1 by A55,NAT_D:51;
then
A57: i1-'1 < len G1 by A15,XXREAL_0:2;
then G1*(i1-'1,j1) in Values G1 & G1*(i1-'1,1)`1 = G1*(i1-'1,j1)`1 by A7,A6
,A55,GOBOARD5:2,MATRIX_0:41;
then
A58: G1*(i1-'1,1)`1 <= G2*(i2-'1,1)`1 by A1,A4,A15,A7,A6,A5,A9,A8,A50,A54,Th7;
now
per cases by A8,XXREAL_0:1;
suppose
A59: j2 = width G2;
then
p in { |[r,s]|: G2*(i2-'1,1)`1 <= r & r <= G2*(i2,1)`1 & G2*(1,j2
)`2 <= s} by A13,A51,A53,A52,GOBRD11:31;
then consider r9,s9 such that
A60: p = |[r9,s9]| and
A61: G2*(i2-'1,1)`1 <= r9 & r9 <= G2*(i2,1)`1 and
A62: G2*(1,j2)`2 <= s9;
A63: G1*(1,j1)`2 <= s9 by A4,A14,A15,A7,A6,A12,A62,GOBOARD5:1;
G1*(i1-'1,1)`1 <= r9 & r9 <= G1*(i1,1)`1 by A4,A14,A15,A7,A6,A11,A58
,A61,GOBOARD5:2,XXREAL_0:2;
then
A64: p in { |[r,s]|: G1*(i1-'1,1)`1 <= r & r <= G1*(i1,1)`1 & G1*(1,
j1)`2 <= s} by A60,A63;
j1 = width G1 by A1,A2,A4,A10,A5,A59,Th5;
hence thesis by A55,A57,A56,A64,GOBRD11:31;
end;
suppose
A65: j2 < width G2;
then p in { |[r,s]| : G2*(i2-'1,1)`1 <= r & r <= G2*(i2,1)`1 & G2*(1,
j2)`2 <= s & s <= G2*(1,j2+1)`2 } by A13,A9,A51,A53,A52,GOBRD11:32;
then consider r9,s9 such that
A66: p = |[r9,s9]| and
A67: G2*(i2-'1,1)`1 <= r9 & r9 <= G2*(i2,1)`1 and
A68: G2*(1,j2)`2 <= s9 and
A69: s9 <= G2*(1,j2+1)`2;
A70: G1*(1,j1)`2 <= s9 by A4,A14,A15,A7,A6,A12,A68,GOBOARD5:1;
A71: G1*(i1-'1,1)`1 <= r9 & r9 <= G1*(i1,1)`1 by A4,A14,A15,A7,A6,A11,A58
,A67,GOBOARD5:2,XXREAL_0:2;
per cases by A6,XXREAL_0:1;
suppose
A72: j1 = width G1;
p in { |[r,s]|: G1*(i1-'1,1)`1 <= r & r <= G1*(i1,1)`1 & G1*
(1,j1)`2 <= s } by A66,A71,A70;
hence thesis by A55,A57,A56,A72,GOBRD11:31;
end;
suppose
A73: j1 < width G1;
1 <= j2+1 & j2+1 <= width G2 by A65,NAT_1:12,13;
then
A74: G2*(i2,j2+1)`2 = G2*(1,j2+1)`2 by A10,A5,GOBOARD5:1;
1 <= j1+1 & j1+1 <= width G1 by A73,NAT_1:12,13;
then G1*(i1,j1+1) in Values G1 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2
by A14,A15,GOBOARD5:1,MATRIX_0:41;
then G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A14,A15,A7,A10,A5,A9
,A65,A73,A74,Th8;
then s9 <= G1*(1,j1+1)`2 by A69,XXREAL_0:2;
then p in { |[r,s]| : G1*(i1-'1,1)`1 <= r & r <= G1*(i1,1)`1 & G1
*(1,j1)`2 <= s & s <= G1*(1,j1+1)`2 } by A66,A71,A70;
hence thesis by A7,A55,A57,A56,A73,GOBRD11:32;
end;
end;
end;
hence thesis;
end;
end;
theorem Th12:
for G1,G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in
Indices G1 & [i2,j2] in Indices G2 & G1*(i1,j1) = G2*(i2,j2) holds cell(G2,i2,
j2-'1) c= cell(G1,i1,j1-'1)
proof
let G1,G2 be Go-board such that
A1: Values G1 c= Values G2 and
A2: [i1,j1] in Indices G1 and
A3: [i2,j2] in Indices G2 and
A4: G1*(i1,j1) = G2*(i2,j2);
A5: 1 <= i1 by A2,MATRIX_0:32;
A6: 1 <= j2 by A3,MATRIX_0:32;
A7: 1 <= i2 by A3,MATRIX_0:32;
A8: j1 <= width G1 by A2,MATRIX_0:32;
A9: j2 <= width G2 by A3,MATRIX_0:32;
A10: i2 <= len G2 by A3,MATRIX_0:32;
then
A11: G2*(i2,j2)`1 = G2*(i2,1)`1 by A7,A6,A9,GOBOARD5:2;
A12: i1 <= len G1 by A2,MATRIX_0:32;
A13: 1 <= j1 by A2,MATRIX_0:32;
then A14: G1*(i1,j1)`2 = G1*(1,j1)`2 by A5,A12,A8,GOBOARD5:1;
let p be object such that
A15: p in cell(G2,i2,j2-'1);
A16: G2*(i2,j2)`2 = G2*(1,j2)`2 by A7,A10,A6,A9,GOBOARD5:1;
per cases by A13,A6,XXREAL_0:1;
suppose
A17: j1 = 1 & j2 = 1;
then
A18: j1-'1 = 0 by XREAL_1:232;
A19: j2-'1 = 0 by A17,XREAL_1:232;
now
per cases by A10,XXREAL_0:1;
suppose
A20: i2 = len G2;
then p in { |[r,s]| : G2*(len G2,1)`1 <= r & s <= G2*(1,1)`2 } by A15
,A19,GOBRD11:27;
then consider r9,s9 such that
A21: p = |[r9,s9]| & G2*(len G2,1)`1 <= r9 and
A22: s9 <= G2*(1,1)`2;
A23: i1 = len G1 by A1,A2,A4,A6,A9,A20,Th3;
G2*(1,1)`2 = G2*(i2,j2)`2 by A7,A10,A9,A17,GOBOARD5:1;
then s9 <= G1*(1,1)`2 by A4,A5,A12,A8,A17,A22,GOBOARD5:1;
then p in { |[r,s]| : G1*(len G1,1)`1 <= r & s <= G1*(1,1)`2 } by A4
,A17,A20,A21,A23;
hence thesis by A18,A23,GOBRD11:27;
end;
suppose
A24: i2 < len G2;
then
p in {|[r,s]|: G2*(i2,1)`1 <= r & r <= G2*(i2+1,1)`1 & s <= G2*(1
,1)`2 } by A15,A7,A19,GOBRD11:30;
then consider r9,s9 such that
A25: p = |[r9,s9]| & G2*(i2,1)`1 <= r9 and
A26: r9 <= G2*(i2+1,1)`1 and
A27: s9 <= G2*(1,1)`2;
G2*(1,1)`2 = G2*(i2,j1)`2 by A7,A10,A9,A17,GOBOARD5:1;
then
A28: s9 <= G1*(1,1)`2 by A4,A5,A12,A8,A17,A27,GOBOARD5:1;
now
per cases by A12,XXREAL_0:1;
suppose
A29: i1 = len G1;
then p in { |[r,s]| : G1*(len G1,1)`1 <= r & s <= G1*(1,1)`2 } by
A4,A17,A25,A28;
hence thesis by A18,A29,GOBRD11:27;
end;
suppose
A30: i1 < len G1;
then
G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A8,A7,A9,A17,A24,Th6;
then r9 <= G1*(i1+1,1)`1 by A26,XXREAL_0:2;
then p in {|[r,s]|: G1*(i1,1)`1 <= r & r <= G1*(i1+1,1)`1 & s <=
G1*(1,1)`2} by A4,A17,A25,A28;
hence thesis by A5,A18,A30,GOBRD11:30;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose that
A31: j1 = 1 and
A32: 1 < j2;
A33: j1-'1 = 0 by A31,XREAL_1:232;
A34: 1 <= j2-'1 by A32,NAT_D:49;
then j2-'1 < j2 by NAT_D:51;
then
A35: j2-'1 < width G2 by A9,XXREAL_0:2;
A36: j2-'1+1 = j2 by A32,XREAL_1:235;
now
per cases by A10,XXREAL_0:1;
suppose
A37: i2 = len G2;
then
p in { |[r,s]| : G2*(i2,1)`1 <= r & G2*(1,j2-'1)`2 <= s & s <= G2
*(1,j2)`2 } by A15,A34,A35,A36,GOBRD11:29;
then
ex r9,s9 st p = |[r9,s9]| & G2*(i2,1)`1 <= r9 & G2*(1,j2-'1)`2 <=
s9 & s9 <= G2*(1,j2)`2;
then
A38: p in { |[r,s]| : G1*(i1,1)`1 <= r & s <= G1*(1,1)`2 } by A4,A14,A11,A16
,A31;
i1 = len G1 by A1,A2,A4,A6,A9,A37,Th3;
hence thesis by A33,A38,GOBRD11:27;
end;
suppose
A39: i2 < len G2;
then
p in { |[r,s]| : G2*(i2,1)`1 <= r & r <= G2*(i2+1,1)`1 & G2*(1,j2
-'1)`2 <= s & s <= G2*(1,j2)`2 } by A15,A7,A34,A35,A36,GOBRD11:32;
then consider r9,s9 such that
A40: p = |[r9,s9]| and
A41: G2*(i2,1)`1 <= r9 and
A42: r9 <= G2*(i2+1,1)`1 and
G2*(1,j2-'1)`2 <= s9 and
A43: s9 <= G2*(1,j2)`2;
A44: s9 <= G1*(1,1)`2 & G1*(i1,1)`1 <= r9 by A4,A7,A10,A6,A9,A14,A31,A41,A43
,GOBOARD5:1,2;
now
per cases by A12,XXREAL_0:1;
suppose
A45: i1 = len G1;
then p in { |[r,s]| : G1*(len G1,1)`1 <= r & s <= G1*(1,1)`2 } by
A40,A44;
hence thesis by A33,A45,GOBRD11:27;
end;
suppose
A46: i1 < len G1;
1 <= i2+1 & i2+1 <= len G2 by A39,NAT_1:12,13;
then
A47: G2*(i2+1,j2)`1 = G2*(i2+1,1)`1 by A6,A9,GOBOARD5:2;
1 <= i1+1 & i1+1 <= len G1 by A46,NAT_1:12,13;
then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A13,A8,GOBOARD5:2;
then G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A13,A8,A7,A6,A9,A39
,A46,A47,Th6;
then r9 <= G1*(i1+1,1)`1 by A42,XXREAL_0:2;
then p in {|[r,s]|: G1*(i1,1)`1 <= r & r <= G1*(i1+1,1)`1 & s <=
G1*(1,1)`2} by A40,A44;
hence thesis by A5,A33,A46,GOBRD11:30;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
1 < j1 & j2 = 1;
hence thesis by A1,A2,A4,A7,A10,Th4;
end;
suppose
A48: 1 < j1 & 1 < j2;
then
A49: 1 <= j2-'1 by NAT_D:49;
then
A50: j2-'1+1 = j2 by NAT_D:43;
j2-'1 < j2 by A49,NAT_D:51;
then
A51: j2-'1 < width G2 by A9,XXREAL_0:2;
then
A52: G2*(1,j2-'1)`2 = G2*(i2,j2-'1)`2 by A7,A10,A49,GOBOARD5:1;
A53: 1 <= j1-'1 by A48,NAT_D:49;
then
A54: j1-'1+1 = j1 by NAT_D:43;
j1-'1 < j1 by A53,NAT_D:51;
then
A55: j1-'1 < width G1 by A8,XXREAL_0:2;
then G1*(1,j1-'1)`2 = G1*(i1,j1-'1)`2 by A5,A12,A53,GOBOARD5:1;
then
A56: G1*(1,j1-'1)`2 <= G2*(1,j2-'1)`2 by A1,A4,A5,A12,A8,A7,A10,A9,A48,A52,Th9;
now
per cases by A10,XXREAL_0:1;
suppose
A57: i2 = len G2;
then
p in { |[r,s]| : G2*(i2,1)`1 <= r & G2*(1,j2-'1)`2 <= s & s <= G2
* (1,j2)`2} by A15,A49,A51,A50,GOBRD11:29;
then consider r9,s9 such that
A58: p = |[r9,s9]| and
A59: G2*(i2,1)`1 <= r9 and
A60: G2*(1,j2-'1)`2 <= s9 & s9 <= G2*(1,j2)`2;
A61: G1*(i1,1)`1 <= r9 by A4,A5,A12,A13,A8,A11,A59,GOBOARD5:2;
G1*(1,j1-'1)`2 <= s9 & s9 <= G1*(1,j1)`2 by A4,A5,A12,A13,A8,A16,A56
,A60,GOBOARD5:1,XXREAL_0:2;
then
A62: p in {|[r,s]|: G1*(i1,1)`1 <= r & G1*(1,j1-'1)`2 <= s & s <= G1*(
1,j1)`2} by A58,A61;
i1 = len G1 by A1,A2,A4,A6,A9,A57,Th3;
hence thesis by A53,A55,A54,A62,GOBRD11:29;
end;
suppose
A63: i2 < len G2;
then
p in { |[r,s]| : G2*(i2,1)`1 <= r & r <= G2*(i2+1,1)`1 & G2*(1,j2
-'1)`2 <= s & s <= G2*(1,j2)`2 } by A15,A7,A49,A51,A50,GOBRD11:32;
then consider r9,s9 such that
A64: p = |[r9,s9]| and
A65: G2*(i2,1)`1 <= r9 and
A66: r9 <= G2*(i2+1,1)`1 and
A67: G2*(1,j2-'1)`2 <= s9 & s9 <= G2*(1,j2)`2;
A68: G1*(i1,1)`1 <= r9 by A4,A5,A12,A13,A8,A11,A65,GOBOARD5:2;
A69: G1*(1,j1-'1)`2 <= s9 & s9 <= G1*(1,j1)`2 by A4,A5,A12,A13,A8,A16,A56
,A67,GOBOARD5:1,XXREAL_0:2;
now
per cases by A12,XXREAL_0:1;
suppose
A70: i1 = len G1;
p in {|[r,s]|: G1*(i1,1)`1 <= r & G1*(1,j1-'1)`2 <= s & s <=
G1* (1,j1)`2} by A64,A69,A68;
hence thesis by A53,A55,A54,A70,GOBRD11:29;
end;
suppose
A71: i1 < len G1;
1 <= i2+1 & i2+1 <= len G2 by A63,NAT_1:12,13;
then
A72: G2*(i2+1,j2)`1 = G2*(i2+1,1)`1 by A6,A9,GOBOARD5:2;
1 <= i1+1 & i1+1 <= len G1 by A71,NAT_1:12,13;
then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A13,A8,GOBOARD5:2;
then G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A13,A8,A7,A6,A9,A63
,A71,A72,Th6;
then r9 <= G1*(i1+1,1)`1 by A66,XXREAL_0:2;
then p in { |[r,s]| : G1*(i1,1)`1 <= r & r <= G1*(i1+1,1)`1 & G1*
(1,j1-'1)`2 <= s & s <= G1*(1,j1)`2 } by A64,A69,A68;
hence thesis by A5,A53,A55,A54,A71,GOBRD11:32;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
Lm1: for f being non empty FinSequence of TOP-REAL 2 st 1 <= i & i <= len GoB
f & 1 <= j & j <= width GoB f ex k st k in dom f & (f/.k)`1 = (GoB f)*(i,j)`1
proof
let f be non empty FinSequence of TOP-REAL 2;
assume that
A1: 1 <= i & i <= len GoB f and
A2: 1 <= j & j <= width GoB f;
A3: GoB f = GoB (Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 2;
then len Incr X_axis f = len GoB f by GOBOARD2:def 1;
then i in dom Incr X_axis f by A1,FINSEQ_3:25;
then (Incr X_axis f).i in rng Incr X_axis f by FUNCT_1:def 3;
then (Incr X_axis f).i in rng X_axis f by SEQ_4:def 21;
then consider k being Nat such that
A4: k in dom X_axis f and
A5: (X_axis f).k = (Incr X_axis f).i by FINSEQ_2:10;
[i,j] in Indices GoB f by A1,A2,MATRIX_0:30;
then
A6: (GoB f)*(i,j) = |[Incr(X_axis f).i,Incr(Y_axis f).j]| by A3,GOBOARD2:def 1;
reconsider k as Nat;
take k;
len X_axis f = len f by GOBOARD1:def 1;
hence k in dom f by A4,FINSEQ_3:29;
thus (f/.k)`1 = Incr(X_axis f).i by A4,A5,GOBOARD1:def 1
.= (GoB f)*(i,j)`1 by A6,EUCLID:52;
end;
Lm2: for f being non empty FinSequence of TOP-REAL 2 st 1 <= i & i <= len GoB
f & 1 <= j & j <= width GoB f ex k st k in dom f & (f/.k)`2 = (GoB f)*(i,j)`2
proof
let f be non empty FinSequence of TOP-REAL 2;
assume that
A1: 1 <= i & i <= len GoB f and
A2: 1 <= j & j <= width GoB f;
A3: GoB f = GoB (Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 2;
then len Incr Y_axis f = width GoB f by GOBOARD2:def 1;
then j in dom Incr Y_axis f by A2,FINSEQ_3:25;
then (Incr Y_axis f).j in rng Incr Y_axis f by FUNCT_1:def 3;
then (Incr Y_axis f).j in rng Y_axis f by SEQ_4:def 21;
then consider k being Nat such that
A4: k in dom Y_axis f and
A5: (Y_axis f).k = (Incr Y_axis f).j by FINSEQ_2:10;
[i,j] in Indices GoB f by A1,A2,MATRIX_0:30;
then
A6: (GoB f)*(i,j) = |[Incr(X_axis f).i,Incr(Y_axis f).j]| by A3,GOBOARD2:def 1;
reconsider k as Nat;
take k;
len Y_axis f = len f by GOBOARD1:def 2;
hence k in dom f by A4,FINSEQ_3:29;
thus (f/.k)`2 = Incr(Y_axis f).j by A4,A5,GOBOARD1:def 2
.= (GoB f)*(i,j)`2 by A6,EUCLID:52;
end;
theorem Th13:
for f being standard special_circular_sequence st f
is_sequence_on G holds Values GoB f c= Values G
proof
let f be standard special_circular_sequence such that
A1: f is_sequence_on G;
let p be object;
set F = GoB f;
assume p in Values F;
then p in { F*(i,j): [i,j] in Indices F } by MATRIX_0:39;
then consider i,j such that
A2: p = F*(i,j) and
A3: [i,j] in Indices F;
reconsider p as Point of TOP-REAL 2 by A2;
A4: 1 <= j & j <= width F by A3,MATRIX_0:32;
A5: 1 <= i & i <= len F by A3,MATRIX_0:32;
then consider k1 such that
A6: k1 in dom f and
A7: p`1 = (f/.k1)`1 by A2,A4,Lm1;
consider k2 such that
A8: k2 in dom f and
A9: p`2 = (f/.k2)`2 by A2,A5,A4,Lm2;
consider i2,j2 such that
A10: [i2,j2] in Indices G and
A11: f/.k2 = G*(i2,j2) by A1,A8,GOBOARD1:def 9;
A12: 1 <= i2 & i2 <= len G by A10,MATRIX_0:32;
consider i1,j1 such that
A13: [i1,j1] in Indices G and
A14: f/.k1 = G*(i1,j1) by A1,A6,GOBOARD1:def 9;
A15: 1 <= j1 & j1 <= width G by A13,MATRIX_0:32;
A16: p = |[p`1, p`2]| by EUCLID:53;
A17: 1 <= j2 & j2 <= width G by A10,MATRIX_0:32;
A18: 1 <= i1 & i1 <= len G by A13,MATRIX_0:32;
then
A19: [i1,j2] in Indices G by A17,MATRIX_0:30;
A20: G*(i1,j2)`2 = G*(1,j2)`2 by A18,A17,GOBOARD5:1
.= G*(i2,j2)`2 by A12,A17,GOBOARD5:1;
G*(i1,j2)`1 = G*(i1,1)`1 by A18,A17,GOBOARD5:2
.= G*(i1,j1)`1 by A18,A15,GOBOARD5:2;
then p = G*(i1,j2) by A7,A9,A14,A11,A20,A16,EUCLID:53;
then p in { G*(k,l): [k,l] in Indices G } by A19;
hence thesis by MATRIX_0:39;
end;
definition
::$CD
let f, G, k;
assume 1 <= k & k+1 <= len f & f is_sequence_on G;
then consider i1,j1,i2,j2 being Nat such that
A1: [i1,j1] in Indices G & f/.k = G*(i1,j1) and
A2: [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) and
A3: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or
i1 = i2 & j1 = j2+1 by JORDAN8:3;
func right_cell(f,k,G) -> Subset of TOP-REAL 2 means
:Def1:
for i1,j1,i2,j2 being Nat
st [i1,j1] in Indices G & [i2,j2] in Indices G & f/.k = G*
(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 & j1+1 = j2 & it = cell(G,i1,j1)
or i1+1 = i2 & j1 = j2 & it = cell(G,i1,j1-'1) or i1 = i2+1 & j1 = j2 & it =
cell(G,i2,j2) or i1 = i2 & j1 = j2+1 & it = cell(G,i1-'1,j2);
existence
proof
per cases by A3;
suppose
A4: i1 = i2 & j1+1 = j2;
take cell(G,i1,j1);
let i19,j19,i29,j29 be Nat;
assume that
A5: [i19,j19] in Indices G and
A6: [i29,j29] in Indices G and
A7: f/.k = G*(i19,j19) and
A8: f/.(k+1) = G*(i29,j29);
i1 = i19 & j1 = j19 by A1,A5,A7,GOBOARD1:5;
hence thesis by A2,A4,A6,A8,GOBOARD1:5;
end;
suppose
A9: i1+1 = i2 & j1 = j2;
take cell(G,i1,j1-'1);
let i19,j19,i29,j29 be Nat;
assume that
A10: [i19,j19] in Indices G and
A11: [i29,j29] in Indices G and
A12: f/.k = G*(i19,j19) and
A13: f/.(k+1) = G*(i29,j29);
i1 = i19 & j1 = j19 by A1,A10,A12,GOBOARD1:5;
hence thesis by A2,A9,A11,A13,GOBOARD1:5;
end;
suppose
A14: i1 = i2+1 & j1 = j2;
take cell(G,i2,j2);
let i19,j19,i29,j29 be Nat;
assume
A15: [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
,j19) & f/.(k+1) = G*(i29,j29);
then i2 = i29 & j1 = j19 by A1,A2,GOBOARD1:5;
hence thesis by A1,A2,A14,A15,GOBOARD1:5;
end;
suppose
A16: i1 = i2 & j1 = j2+1;
take cell(G,i1-'1,j2);
let i19,j19,i29,j29 be Nat;
assume that
A17: [i19,j19] in Indices G and
A18: [i29,j29] in Indices G and
A19: f/.k = G*(i19,j19) and
A20: f/.(k+1) = G*(i29,j29);
i1 = i19 & j1 = j19 by A1,A17,A19,GOBOARD1:5;
hence thesis by A2,A16,A18,A20,GOBOARD1:5;
end;
end;
uniqueness
proof
let P1,P2 be Subset of TOP-REAL 2 such that
A21: for i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & [
i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 &
j1+1 = j2 & P1 = cell(G,i1,j1) or i1+1 = i2 & j1 = j2 & P1 = cell(G,i1,j1-'1)
or i1 = i2+1 & j1 = j2 & P1 = cell(G,i2,j2) or i1 = i2 & j1 = j2+1 & P1 = cell(
G,i1-'1,j2) and
A22: for i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & [
i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 &
j1+1 = j2 & P2 = cell(G,i1,j1) or i1+1 = i2 & j1 = j2 & P2 = cell(G,i1,j1-'1)
or i1 = i2+1 & j1 = j2 & P2 = cell(G,i2,j2) or i1 = i2 & j1 = j2+1 & P2 = cell(
G,i1-'1,j2);
per cases by A3;
suppose
A23: i1 = i2 & j1+1 = j2;
A24: j2 <= j2+1 by NAT_1:11;
A25: j1 < j2 by A23,XREAL_1:29;
hence P1 = cell(G,i1,j1) by A1,A2,A21,A24
.= P2 by A1,A2,A22,A25,A24;
end;
suppose
A26: i1+1 = i2 & j1 = j2;
A27: i2 <= i2+1 by NAT_1:11;
A28: i1 < i2 by A26,XREAL_1:29;
hence P1 = cell(G,i1,j1-'1) by A1,A2,A21,A27
.= P2 by A1,A2,A22,A28,A27;
end;
suppose
A29: i1 = i2+1 & j1 = j2;
A30: i1 <= i1+1 by NAT_1:11;
A31: i2 < i1 by A29,XREAL_1:29;
hence P1 = cell(G,i2,j2) by A1,A2,A21,A30
.= P2 by A1,A2,A22,A31,A30;
end;
suppose
A32: i1 = i2 & j1 = j2+1;
A33: j1 <= j1+1 by NAT_1:11;
A34: j2 < j1 by A32,XREAL_1:29;
hence P1 = cell(G,i1-'1,j2) by A1,A2,A21,A33
.= P2 by A1,A2,A22,A34,A33;
end;
end;
func left_cell(f,k,G) -> Subset of TOP-REAL 2 means
:Def2:
for i1,j1,i2,j2
being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f/.k = G*
(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 & j1+1 = j2 & it = cell(G,i1-'1,j1
) or i1+1 = i2 & j1 = j2 & it = cell(G,i1,j1) or i1 = i2+1 & j1 = j2 & it =
cell(G,i2,j2-'1) or i1 = i2 & j1 = j2+1 & it = cell(G,i1,j2);
existence
proof
per cases by A3;
suppose
A35: i1 = i2 & j1+1 = j2;
take cell(G,i1-'1,j1);
let i19,j19,i29,j29 be Nat;
assume that
A36: [i19,j19] in Indices G and
A37: [i29,j29] in Indices G and
A38: f/.k = G*(i19,j19) and
A39: f/.(k+1) = G*(i29,j29);
i1 = i19 & j1 = j19 by A1,A36,A38,GOBOARD1:5;
hence thesis by A2,A35,A37,A39,GOBOARD1:5;
end;
suppose
A40: i1+1 = i2 & j1 = j2;
take cell(G,i1,j1);
let i19,j19,i29,j29 be Nat;
assume that
A41: [i19,j19] in Indices G and
A42: [i29,j29] in Indices G and
A43: f/.k = G*(i19,j19) and
A44: f/.(k+1) = G*(i29,j29);
i1 = i19 & j1 = j19 by A1,A41,A43,GOBOARD1:5;
hence thesis by A2,A40,A42,A44,GOBOARD1:5;
end;
suppose
A45: i1 = i2+1 & j1 = j2;
take cell(G,i2,j2-'1);
let i19,j19,i29,j29 be Nat;
assume
A46: [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
,j19) & f/.(k+1) = G*(i29,j29);
then i2 = i29 & j1 = j19 by A1,A2,GOBOARD1:5;
hence thesis by A1,A2,A45,A46,GOBOARD1:5;
end;
suppose
A47: i1 = i2 & j1 = j2+1;
take cell(G,i1,j2);
let i19,j19,i29,j29 be Nat;
assume that
A48: [i19,j19] in Indices G and
A49: [i29,j29] in Indices G and
A50: f/.k = G*(i19,j19) and
A51: f/.(k+1) = G*(i29,j29);
i1 = i19 & j1 = j19 by A1,A48,A50,GOBOARD1:5;
hence thesis by A2,A47,A49,A51,GOBOARD1:5;
end;
end;
uniqueness
proof
let P1,P2 be Subset of TOP-REAL 2 such that
A52: for i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & [
i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 &
j1+1 = j2 & P1 = cell(G,i1-'1,j1) or i1+1 = i2 & j1 = j2 & P1 = cell(G,i1,j1)
or i1 = i2+1 & j1 = j2 & P1 = cell(G,i2,j2-'1) or i1 = i2 & j1 = j2+1 & P1 =
cell(G,i1,j2) and
A53: for i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & [
i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 &
j1+1 = j2 & P2 = cell(G,i1-'1,j1) or i1+1 = i2 & j1 = j2 & P2 = cell(G,i1,j1)
or i1 = i2+1 & j1 = j2 & P2 = cell(G,i2,j2-'1) or i1 = i2 & j1 = j2+1 & P2 =
cell(G,i1,j2);
per cases by A3;
suppose
A54: i1 = i2 & j1+1 = j2;
A55: j2 <= j2+1 by NAT_1:11;
A56: j1 < j2 by A54,XREAL_1:29;
hence P1 = cell(G,i1-'1,j1) by A1,A2,A52,A55
.= P2 by A1,A2,A53,A56,A55;
end;
suppose
A57: i1+1 = i2 & j1 = j2;
A58: i2 <= i2+1 by NAT_1:11;
A59: i1 < i2 by A57,XREAL_1:29;
hence P1 = cell(G,i1,j1) by A1,A2,A52,A58
.= P2 by A1,A2,A53,A59,A58;
end;
suppose
A60: i1 = i2+1 & j1 = j2;
A61: i1 <= i1+1 by NAT_1:11;
A62: i2 < i1 by A60,XREAL_1:29;
hence P1 = cell(G,i2,j2-'1) by A1,A2,A52,A61
.= P2 by A1,A2,A53,A62,A61;
end;
suppose
A63: i1 = i2 & j1 = j2+1;
A64: j1 <= j1+1 by NAT_1:11;
A65: j2 < j1 by A63,XREAL_1:29;
hence P1 = cell(G,i1,j2) by A1,A2,A52,A64
.= P2 by A1,A2,A53,A65,A64;
end;
end;
end;
theorem Th14:
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G
& [i,j+1] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1) implies
left_cell(f,k,G) = cell(G,i-'1,j)
proof
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
,j+1] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1);
hence thesis by A1,Def2;
end;
theorem Th15:
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G
& [i,j+1] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1) implies
right_cell(f,k,G) = cell(G,i,j)
proof
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
,j+1] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1);
hence thesis by A1,Def1;
end;
theorem Th16:
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G
& [i+1,j] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j) implies
left_cell(f,k,G) = cell(G,i,j)
proof
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
+1,j] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j);
hence thesis by A1,Def2;
end;
theorem Th17:
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G
& [i+1,j] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j) implies
right_cell(f,k,G) = cell(G,i,j-'1)
proof
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
+1,j] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j);
hence thesis by A1,Def1;
end;
theorem Th18:
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G
& [i+1,j] in Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j) implies
left_cell(f,k,G) = cell(G,i,j-'1)
proof
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
+1,j] in Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j);
hence thesis by A1,Def2;
end;
theorem Th19:
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G
& [i+1,j] in Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j) implies
right_cell(f,k,G) = cell(G,i,j)
proof
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
+1,j] in Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j);
hence thesis by A1,Def1;
end;
theorem Th20:
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j+1] in Indices
G & [i,j] in Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j) implies
left_cell(f,k,G) = cell(G,i,j)
proof
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j+1] in Indices G &
[i,j] in Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j);
hence thesis by A1,Def2;
end;
theorem Th21:
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j+1] in Indices
G & [i,j] in Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j) implies
right_cell(f,k,G) = cell(G,i-'1,j)
proof
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j+1] in Indices G &
[i,j] in Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j);
hence thesis by A1,Def1;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G implies left_cell(f,k,G) /\
right_cell(f,k,G) = LSeg(f,k)
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f and
A3: f is_sequence_on G;
k+1 >= 1 by NAT_1:11;
then
A4: k+1 in dom f by A2,FINSEQ_3:25;
then consider i2,j2 being Nat such that
A5: [i2,j2] in Indices G and
A6: f/.(k+1) = G*(i2,j2) by A3,GOBOARD1:def 9;
A7: 1 <= j2 by A5,MATRIX_0:32;
A8: i2 <= len G by A5,MATRIX_0:32;
A9: 1 <= i2 by A5,MATRIX_0:32;
A10: j2 <= width G by A5,MATRIX_0:32;
k <= k+1 by NAT_1:11;
then k <= len f by A2,XXREAL_0:2;
then
A11: k in dom f by A1,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A12: [i1,j1] in Indices G and
A13: f/.k = G*(i1,j1) by A3,GOBOARD1:def 9;
A14: 0+1 <= j1 by A12,MATRIX_0:32;
then j1 > 0;
then consider j being Nat such that
A15: j+1 = j1 by NAT_1:6;
A16: |.i1-i2.|+|.j1-j2.| = 1 by A3,A11,A12,A13,A4,A5,A6,GOBOARD1:def 9;
A17: now
per cases by A16,SEQM_3:42;
case that
A18: |.i1-i2.| = 1 and
A19: j1 = j2;
i1-i2 = 1 or -(i1-i2) = 1 by A18,ABSVALUE:def 1;
hence i1 = i2+1 or i1+1 = i2;
thus j1 = j2 by A19;
end;
case that
A20: i1 = i2 and
A21: |.j1-j2.| = 1;
j1-j2 = 1 or -(j1-j2) = 1 by A21,ABSVALUE:def 1;
hence j1 = j2+1 or j1+1 = j2;
thus i1 = i2 by A20;
end;
end;
A22: j1-'1=j by A15,NAT_D:34;
A23: j1 <= width G by A12,MATRIX_0:32;
then
A24: j < width G by A15,NAT_1:13;
A25: 0+1 <= i1 by A12,MATRIX_0:32;
then i1 > 0;
then consider i being Nat such that
A26: i+1 = i1 by NAT_1:6;
A27: i1 <= len G by A12,MATRIX_0:32;
then
A28: i < len G by A26,NAT_1:13;
A29: i1-'1 = i by A26,NAT_D:34;
reconsider i,j as Nat;
per cases by A17;
suppose
A30: i1 = i2 & j1+1 = j2;
then
A31: right_cell(f,k,G) = cell(G,i1,j1) by A1,A2,A3,A12,A13,A5,A6,Th15;
j1 < width G & left_cell(f,k,G) = cell(G,i,j1) by A1,A2,A3,A12,A13,A5,A6
,A10,A29,A30,Th14,NAT_1:13;
hence left_cell(f,k,G) /\ right_cell(f,k,G) = LSeg(G*(i1,j1),G*(i1,j1+1))
by A14,A26,A28,A31,GOBOARD5:25
.= LSeg(f,k) by A1,A2,A13,A6,A30,TOPREAL1:def 3;
end;
suppose
A32: i1+1 = i2 & j1 = j2;
then
A33: right_cell(f,k,G) = cell(G,i1,j) by A1,A2,A3,A12,A13,A5,A6,A22,Th17;
i1 < len G & left_cell(f,k,G) = cell(G,i1,j1) by A1,A2,A3,A12,A13,A5,A6,A8
,A32,Th16,NAT_1:13;
hence left_cell(f,k,G) /\ right_cell(f,k,G) = LSeg(G*(i1,j1),G*(i1+1,j1))
by A25,A15,A24,A33,GOBOARD5:26
.= LSeg(f,k) by A1,A2,A13,A6,A32,TOPREAL1:def 3;
end;
suppose
A34: i1 = i2+1 & j1 = j2;
then
A35: right_cell(f,k,G) = cell(G,i2,j1) by A1,A2,A3,A12,A13,A5,A6,Th19;
i2 < len G & left_cell(f,k,G) = cell(G,i2,j) by A1,A2,A3,A12,A13,A5,A6,A27
,A22,A34,Th18,NAT_1:13;
hence left_cell(f,k,G) /\ right_cell(f,k,G) = LSeg(G*(i2+1,j1),G*(i2,j1))
by A9,A15,A24,A35,GOBOARD5:26
.= LSeg(f,k) by A1,A2,A13,A6,A34,TOPREAL1:def 3;
end;
suppose
A36: i1 = i2 & j1 = j2+1;
then
A37: right_cell(f,k,G) = cell(G,i,j2) by A1,A2,A3,A12,A13,A5,A6,A29,Th21;
j2 < width G & left_cell(f,k,G) = cell(G,i1,j2) by A1,A2,A3,A12,A13,A5,A6
,A23,A36,Th20,NAT_1:13;
hence left_cell(f,k,G) /\ right_cell(f,k,G) = LSeg(G*(i1,j2+1),G*(i1,j2))
by A7,A26,A28,A37,GOBOARD5:25
.= LSeg(f,k) by A1,A2,A13,A6,A36,TOPREAL1:def 3;
end;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G implies right_cell(f,k,G)
is closed
proof
assume
A1: 1 <= k & k+1 <= len f & f is_sequence_on G;
then consider i1,j1,i2,j2 being Nat such that
A2: [i1,j1] in Indices G & f/.k = G*(i1,j1) & [i2,j2] in Indices G & f/.
( k+1 ) = G*(i2,j2) &( i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1
& j1 = j2 or i1 = i2 & j1 = j2+1) by JORDAN8:3;
i1 = i2 & j1+1 = j2 & right_cell(f,k,G) = cell(G,i1,j1) or i1+1 = i2 &
j1 = j2 & right_cell(f,k,G) = cell(G,i1,j1-'1) or i1 = i2+1 & j1 = j2 &
right_cell(f,k,G) = cell(G,i2,j2) or i1 = i2 & j1 = j2+1 & right_cell(f,k,G) =
cell(G,i1-'1,j2) by A1,A2,Def1;
hence thesis by GOBRD11:33;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G & k+1 <= n implies
left_cell(f,k,G) = left_cell(f|n,k,G) & right_cell(f,k,G) = right_cell(f|n,k,G)
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f and
A3: f is_sequence_on G and
A4: k+1 <= n;
per cases;
suppose
len f <= n;
hence thesis by FINSEQ_1:58;
end;
suppose
n < len f;
then
A5: len(f|n) = n by FINSEQ_1:59;
then k in dom(f|n) by A1,A4,SEQ_4:134;
then
A6: (f|n)/.k = f/.k by FINSEQ_4:70;
k+1 in dom(f|n) by A1,A4,A5,SEQ_4:134;
then
A7: (f|n)/.(k+1) = f/.(k+1) by FINSEQ_4:70;
set lf = left_cell(f,k,G), lfn = left_cell(f|n,k,G), rf = right_cell(f,k,G
), rfn = right_cell(f|n,k,G);
A8: f|n is_sequence_on G by A3,GOBOARD1:22;
consider i1,j1,i2,j2 being Nat such that
A9: [i1,j1] in Indices G & f/.k = G*(i1,j1) & [i2,j2] in Indices G & f
/.( k+1) = G*(i2,j2) and
A10: 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:3;
A11: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A12: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
now
per cases by A10;
suppose
A13: i1 = i2 & j1+1 = j2;
hence lf = cell(G,i1-'1,j1) by A1,A2,A3,A9,A11,Def2
.= lfn by A1,A4,A9,A11,A8,A5,A6,A7,A13,Def2;
thus rf = cell(G,i1,j1) by A1,A2,A3,A9,A11,A13,Def1
.= rfn by A1,A4,A9,A11,A8,A5,A6,A7,A13,Def1;
end;
suppose
A14: i1+1 = i2 & j1 = j2;
hence lf = cell(G,i1,j1) by A1,A2,A3,A9,A12,Def2
.= lfn by A1,A4,A9,A12,A8,A5,A6,A7,A14,Def2;
thus rf = cell(G,i1,j1-'1) by A1,A2,A3,A9,A12,A14,Def1
.= rfn by A1,A4,A9,A12,A8,A5,A6,A7,A14,Def1;
end;
suppose
A15: i1 = i2+1 & j1 = j2;
hence lf = cell(G,i2,j2-'1) by A1,A2,A3,A9,A12,Def2
.= lfn by A1,A4,A9,A12,A8,A5,A6,A7,A15,Def2;
thus rf = cell(G,i2,j2) by A1,A2,A3,A9,A12,A15,Def1
.= rfn by A1,A4,A9,A12,A8,A5,A6,A7,A15,Def1;
end;
suppose
A16: i1 = i2 & j1 = j2+1;
hence lf = cell(G,i1,j2) by A1,A2,A3,A9,A11,Def2
.= lfn by A1,A4,A9,A11,A8,A5,A6,A7,A16,Def2;
thus rf = cell(G,i1-'1,j2) by A1,A2,A3,A9,A11,A16,Def1
.= rfn by A1,A4,A9,A11,A8,A5,A6,A7,A16,Def1;
end;
end;
hence thesis;
end;
end;
theorem
1 <= k & k+1 <= len(f/^n) & n <= len f & f is_sequence_on G implies
left_cell(f,k+n,G) = left_cell(f/^n,k,G) & right_cell(f,k+n,G) = right_cell(f/^
n,k,G)
proof
set g = (f/^n);
assume that
A1: 1 <= k and
A2: k+1 <= len g and
A3: n <= len f and
A4: f is_sequence_on G;
A5: len g = len f - n & k+1+n <= (len g)+n by A2,A3,RFINSEQ:def 1,XREAL_1:6;
k in dom g by A1,A2,SEQ_4:134;
then
A6: g/.k = f/.(k+n) by FINSEQ_5:27;
set lf = left_cell(f,k+n,G), lfn = left_cell(g,k,G), rf = right_cell(f,k+n,G
), rfn = right_cell(g,k,G);
A7: k+1+n = k+n+1 & 1 <= k+n by A1,NAT_1:12;
k+1 in dom g by A1,A2,SEQ_4:134;
then
A8: g/.(k+1) = f/.(k+1+n) by FINSEQ_5:27;
A9: g is_sequence_on G by A4,JORDAN8:2;
then consider i1,j1,i2,j2 being Nat such that
A10: [i1,j1] in Indices G & g/.k = G*(i1,j1) & [i2,j2] in Indices G & g/.
( 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 A1,A2,JORDAN8:3;
A12: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A13: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
now
per cases by A11;
suppose
A14: i1 = i2 & j1+1 = j2;
hence lf = cell(G,i1-'1,j1) by A4,A10,A12,A6,A8,A5,A7,Def2
.= lfn by A1,A2,A9,A10,A12,A14,Def2;
thus rf = cell(G,i1,j1) by A4,A10,A12,A6,A8,A5,A7,A14,Def1
.= rfn by A1,A2,A9,A10,A12,A14,Def1;
end;
suppose
A15: i1+1 = i2 & j1 = j2;
hence lf = cell(G,i1,j1) by A4,A10,A13,A6,A8,A5,A7,Def2
.= lfn by A1,A2,A9,A10,A13,A15,Def2;
thus rf = cell(G,i1,j1-'1) by A4,A10,A13,A6,A8,A5,A7,A15,Def1
.= rfn by A1,A2,A9,A10,A13,A15,Def1;
end;
suppose
A16: i1 = i2+1 & j1 = j2;
hence lf = cell(G,i2,j2-'1) by A4,A10,A13,A6,A8,A5,A7,Def2
.= lfn by A1,A2,A9,A10,A13,A16,Def2;
thus rf = cell(G,i2,j2) by A4,A10,A13,A6,A8,A5,A7,A16,Def1
.= rfn by A1,A2,A9,A10,A13,A16,Def1;
end;
suppose
A17: i1 = i2 & j1 = j2+1;
hence lf = cell(G,i1,j2) by A4,A10,A12,A6,A8,A5,A7,Def2
.= lfn by A1,A2,A9,A10,A12,A17,Def2;
thus rf = cell(G,i1-'1,j2) by A4,A10,A12,A6,A8,A5,A7,A17,Def1
.= rfn by A1,A2,A9,A10,A12,A17,Def1;
end;
end;
hence thesis;
end;
theorem
for G being Go-board, f being standard special_circular_sequence st 1
<= n & n+1 <= len f & f is_sequence_on G holds left_cell(f,n,G) c= left_cell(f,
n) & right_cell(f,n,G) c= right_cell(f,n)
proof
let G be Go-board,f be standard special_circular_sequence such that
A1: 1 <= n & n+1 <= len f and
A2: f is_sequence_on G;
consider i1,j1,i2,j2 such that
A3: [i1,j1] in Indices G and
A4: f/.n = G*(i1,j1) and
A5: [i2,j2] in Indices G and
A6: f/.(n+1) = G*(i2,j2) and
A7: 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,JORDAN8:3;
A8: 1 <= j1 by A3,MATRIX_0:32;
A9: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A10: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
A11: j2 <= width G by A5,MATRIX_0:32;
A12: j1 <= width G by A3,MATRIX_0:32;
A13: i2 <= len G by A5,MATRIX_0:32;
A14: 1 <= i2 by A5,MATRIX_0:32;
then
A15: G*(i2,j1)`2 = G*(1,j1)`2 by A8,A12,A13,GOBOARD5:1;
A16: 1 <= j2 by A5,MATRIX_0:32;
then
A17: G*(i2,j2)`1 = G*(i2,1)`1 by A14,A13,A11,GOBOARD5:2;
A18: i1 <= len G by A3,MATRIX_0:32;
set F = GoB f;
A19: Values F c= Values G by A2,Th13;
f is_sequence_on F by GOBOARD5:def 5;
then consider m,k,i,j such that
A20: [m,k] in Indices F and
A21: f/.n = F*(m,k) and
A22: [i,j] in Indices F and
A23: f/.(n+1) = F*(i,j) and
m = i & k+1 = j or m+1 = i & k = j or m = i+1 & k = j or m = i & k = j+1
by A1,JORDAN8:3;
A24: 1 <= m by A20,MATRIX_0:32;
A25: 1 <= i1 by A3,MATRIX_0:32;
then
A26: G*(i1,j1)`1 = G*(i1,1)`1 by A18,A8,A12,GOBOARD5:2;
A27: G*(i1,j1)`2 = G*(1,j1)`2 by A25,A18,A8,A12,GOBOARD5:1;
A28: m <= len F by A20,MATRIX_0:32;
A29: j+1 > j by NAT_1:13;
A30: k+1 > k by NAT_1:13;
A31: k+1 >= 1 by NAT_1:12;
A32: j+1 >= 1 by NAT_1:12;
A33: j <= width F by A22,MATRIX_0:32;
A34: i+1 > i by NAT_1:13;
A35: m+1 > m by NAT_1:13;
A36: i <= len F by A22,MATRIX_0:32;
A37: i+1 >= 1 by NAT_1:12;
A38: m+1 >= 1 by NAT_1:12;
A39: k <= width F by A20,MATRIX_0:32;
A40: 1 <= j by A22,MATRIX_0:32;
then
A41: F*(m,j)`2 = F*(1,j)`2 by A24,A28,A33,GOBOARD5:1;
A42: 1 <= i by A22,MATRIX_0:32;
then
A43: F*(i,j)`1 = F*(i,1)`1 by A36,A40,A33,GOBOARD5:2;
A44: F*(i,j)`2 = F*(1,j)`2 by A42,A36,A40,A33,GOBOARD5:1;
A45: 1 <= k by A20,MATRIX_0:32;
then
A46: F*(i,k)`1 = F*(i,1)`1 by A39,A42,A36,GOBOARD5:2;
per cases by A7;
suppose
A47: i1 = i2 & j1+1 = j2;
A48: now
A49: G*(i2,j2)`2 = G*(1,j2)`2 by A14,A13,A16,A11,GOBOARD5:1;
assume
A50: k+1 < j;
then
A51: k+1 < width F by A33,XXREAL_0:2;
then consider l,i9 such that
A52: l in dom f and
A53: [i9,k+1] in Indices F and
A54: f/.l = F*(i9,k+1) by JORDAN5D:8,NAT_1:12;
A55: F*(m,k+1)`2 = F*(1,k+1)`2 by A24,A28,A31,A51,GOBOARD5:1;
1 <= i9 & i9 <= len F by A53,MATRIX_0:32;
then
A56: F*(i9,k+1)`2 = F*(1,k+1)`2 by A31,A51,GOBOARD5:1;
consider i19,j19 such that
A57: [i19,j19] in Indices G and
A58: f/.l = G*(i19,j19) by A2,A52,GOBOARD1:def 9;
A59: 1 <= j19 by A57,MATRIX_0:32;
A60: 1 <= i19 & i19 <= len G by A57,MATRIX_0:32;
then
A61: G*(i19,j1)`2 = G*(1,j1)`2 by A8,A12,GOBOARD5:1;
A62: now
assume j1 >= j19;
then G*(i19,j19)`2 <= G*(i1,j1)`2 by A12,A27,A60,A59,A61,SPRECT_3:12;
hence contradiction by A21,A24,A28,A45,A4,A30,A51,A54,A56,A55,A58,
GOBOARD5:4;
end;
A63: j19 <= width G by A57,MATRIX_0:32;
A64: G*(i19,j2)`2 = G*(1,j2)`2 by A16,A11,A60,GOBOARD5:1;
now
assume j2 <= j19;
then G*(i2,j2)`2 <= G*(i19,j19)`2 by A16,A60,A63,A49,A64,SPRECT_3:12;
hence contradiction by A23,A24,A28,A33,A44,A41,A6,A31,A50,A54,A56,A55
,A58,GOBOARD5:4;
end;
hence contradiction by A47,A62,NAT_1:13;
end;
now
assume j <= k;
then
A65: F*(i,j)`2 <= F*(m,k)`2 by A24,A28,A39,A40,A44,A41,SPRECT_3:12;
j1 < j2 by A47,NAT_1:13;
hence contradiction by A21,A23,A4,A6,A8,A14,A13,A11,A27,A15,A65,
GOBOARD5:4;
end;
then k+1 <= j by NAT_1:13;
then k+1 = j by A48,XXREAL_0:1;
then
A66: right_cell(f,n) = cell(F,m,k) & left_cell(f,n) = cell(F,m-'1,k) by A1,A20
,A21,A22,A23,A30,A29,GOBOARD5:def 6,def 7;
right_cell(f,n,G) = cell(G,i1,j1) & left_cell(f,n,G) = cell(G,i1-'1,
j1) by A1,A2,A3,A4,A5,A6,A9,A47,Def1,Def2;
hence thesis by A19,A20,A21,A3,A4,A66,Th10,Th11;
end;
suppose
A67: i1+1 = i2 & j1 = j2;
A68: now
assume
A69: m+1 < i;
then
A70: m+1 < len F by A36,XXREAL_0:2;
then consider l,j9 such that
A71: l in dom f and
A72: [m+1,j9] in Indices F and
A73: f/.l = F*(m+1,j9) by JORDAN5D:7,NAT_1:12;
A74: F*(m+1,k)`1 = F*(m+1,1)`1 by A45,A39,A38,A70,GOBOARD5:2;
1 <= j9 & j9 <= width F by A72,MATRIX_0:32;
then
A75: F*(m+1,j9)`1 = F*(m+1,1)`1 by A38,A70,GOBOARD5:2;
A76: 1 <= m+1 & F*(m+1,j)`1 = F*(m+1,1)`1 by A40,A33,A38,A70,GOBOARD5:2;
A77: G*(i2,j2)`1 = G*(i2,1)`1 by A14,A13,A16,A11,GOBOARD5:2;
consider i19,j19 such that
A78: [i19,j19] in Indices G and
A79: f/.l = G*(i19,j19) by A2,A71,GOBOARD1:def 9;
A80: i19 <= len G by A78,MATRIX_0:32;
A81: 1 <= j19 & j19 <= width G by A78,MATRIX_0:32;
A82: 1 <= i19 by A78,MATRIX_0:32;
then
A83: G*(i19,j19)`1 = G*(i19,1)`1 by A80,A81,GOBOARD5:2;
A84: G*(i19,j1)`1 = G*(i19,1)`1 by A8,A12,A82,A80,GOBOARD5:2;
A85: now
assume i1 >= i19;
then G*(i19,j19)`1 <= G*(i1,j1)`1 by A18,A8,A12,A82,A83,A84,SPRECT_3:13
;
hence contradiction by A21,A24,A45,A39,A4,A35,A70,A73,A75,A74,A79,
GOBOARD5:3;
end;
A86: G*(i2,j19)`1 = G*(i2,1)`1 by A14,A13,A81,GOBOARD5:2;
now
assume i2 <= i19;
then G*(i2,j2)`1 <= G*(i19,j19)`1 by A14,A80,A81,A77,A86,SPRECT_3:13;
hence contradiction by A23,A36,A40,A33,A6,A69,A73,A75,A76,A79,
GOBOARD5:3;
end;
hence contradiction by A67,A85,NAT_1:13;
end;
now
assume i <= m;
then
A87: F*(i,j)`1 <= F*(m,k)`1 by A28,A45,A39,A42,A43,A46,SPRECT_3:13;
i1 < i2 by A67,NAT_1:13;
hence contradiction by A21,A23,A4,A6,A25,A8,A12,A13,A67,A87,GOBOARD5:3;
end;
then m+1 <= i by NAT_1:13;
then m+1 = i by A68,XXREAL_0:1;
then
A88: right_cell(f,n) = cell(F,m, k-'1) & left_cell(f,n) = cell(F,m,k) by A1,A20
,A21,A22,A23,A35,A34,GOBOARD5:def 6,def 7;
right_cell(f,n,G) = cell(G,i1,j1-'1) & left_cell(f,n,G) = cell(G,i1,
j1) by A1,A2,A3,A4,A5,A6,A10,A67,Def1,Def2;
hence thesis by A19,A20,A21,A3,A4,A88,Th10,Th12;
end;
suppose
A89: i1 = i2+1 & j1 = j2;
A90: now
assume
A91: m > i+1;
then
A92: i+1 < len F by A28,XXREAL_0:2;
then consider l,j9 such that
A93: l in dom f and
A94: [i+1,j9] in Indices F and
A95: f/.l = F*(i+1,j9) by JORDAN5D:7,NAT_1:12;
A96: 1 <= i+1 & F*(i+1,k)`1 = F*(i+1,1)`1 by A45,A39,A37,A92,GOBOARD5:2;
1 <= j9 & j9 <= width F by A94,MATRIX_0:32;
then
A97: F*(i+1,j9)`1 = F*(i+1,1)`1 by A37,A92,GOBOARD5:2;
A98: F*(i+1,j)`1 = F*(i+1,1)`1 by A40,A33,A37,A92,GOBOARD5:2;
A99: G*(i2,j2)`1 = G*(i2,1)`1 by A14,A13,A16,A11,GOBOARD5:2;
consider i19,j19 such that
A100: [i19,j19] in Indices G and
A101: f/.l = G*(i19,j19) by A2,A93,GOBOARD1:def 9;
A102: 1 <= i19 by A100,MATRIX_0:32;
A103: 1 <= j19 & j19 <= width G by A100,MATRIX_0:32;
A104: i19 <= len G by A100,MATRIX_0:32;
then
A105: G*(i19,j19)`1 = G*(i19,1)`1 by A102,A103,GOBOARD5:2;
A106: G*(i19,j1)`1 = G*(i19,1)`1 by A8,A12,A102,A104,GOBOARD5:2;
A107: now
assume i1 <= i19;
then G*(i19,j19)`1 >= G*(i1,j1)`1 by A25,A8,A12,A104,A105,A106,
SPRECT_3:13;
hence contradiction by A21,A28,A45,A39,A4,A91,A95,A97,A96,A101,
GOBOARD5:3;
end;
A108: G*(i2,j19)`1 = G*(i2,1)`1 by A14,A13,A103,GOBOARD5:2;
now
assume i2 >= i19;
then G*(i2,j2)`1 >= G*(i19,j19)`1 by A13,A102,A103,A99,A108,SPRECT_3:13
;
hence contradiction by A23,A42,A40,A33,A6,A34,A92,A95,A97,A98,A101,
GOBOARD5:3;
end;
hence contradiction by A89,A107,NAT_1:13;
end;
now
assume m <= i;
then
A109: F*(i,j)`1 >= F*(m,k)`1 by A24,A45,A39,A36,A43,A46,SPRECT_3:13;
i1 > i2 by A89,NAT_1:13;
hence contradiction by A21,A23,A4,A6,A18,A8,A12,A14,A89,A109,GOBOARD5:3;
end;
then i+1 <= m by NAT_1:13;
then i+1 = m by A90,XXREAL_0:1;
then
A110: right_cell(f,n) = cell(F,i,j) & left_cell(f,n) = cell(F,i,j-'1) by A1,A20
,A21,A22,A23,A35,A34,GOBOARD5:def 6,def 7;
right_cell(f,n,G) = cell(G,i2,j2) & left_cell(f,n,G) = cell(G,i2,j2
-'1) by A1,A2,A3,A4,A5,A6,A10,A89,Def1,Def2;
hence thesis by A19,A22,A23,A5,A6,A110,Th10,Th12;
end;
suppose
A111: i1 = i2 & j1 = j2+1;
A112: now
A113: G*(i2,j2)`2 = G*(1,j2)`2 by A14,A13,A16,A11,GOBOARD5:1;
assume
A114: j+1 < k;
then
A115: j+1 < width F by A39,XXREAL_0:2;
then consider l,i9 such that
A116: l in dom f and
A117: [i9,j+1] in Indices F and
A118: f/.l = F*(i9,j+1) by JORDAN5D:8,NAT_1:12;
A119: F*(m,j+1)`2 = F*(1,j+1)`2 by A24,A28,A32,A115,GOBOARD5:1;
1 <= i9 & i9 <= len F by A117,MATRIX_0:32;
then
A120: F*(i9,j+1)`2 = F*(1,j+1)`2 by A32,A115,GOBOARD5:1;
consider i19,j19 such that
A121: [i19,j19] in Indices G and
A122: f/.l = G*(i19,j19) by A2,A116,GOBOARD1:def 9;
A123: j19 <= width G by A121,MATRIX_0:32;
A124: 1 <= i19 & i19 <= len G by A121,MATRIX_0:32;
then
A125: G*(i19,j1)`2 = G*(1,j1)`2 by A8,A12,GOBOARD5:1;
A126: now
assume j1 <= j19;
then G*(i19,j19)`2 >= G*(i1,j1)`2 by A8,A27,A124,A123,A125,SPRECT_3:12;
hence
contradiction by A21,A24,A28,A39,A4,A32,A114,A118,A120,A119,A122,
GOBOARD5:4;
end;
A127: F*(i,j+1)`2 = F*(1,j+1)`2 by A42,A36,A32,A115,GOBOARD5:1;
A128: 1 <= j19 by A121,MATRIX_0:32;
A129: G*(i19,j2)`2 = G*(1,j2)`2 by A16,A11,A124,GOBOARD5:1;
now
assume j2 >= j19;
then G*(i2,j2)`2 >= G*(i19,j19)`2 by A11,A124,A128,A113,A129,
SPRECT_3:12;
hence contradiction by A23,A42,A36,A40,A6,A29,A115,A118,A120,A127,A122,
GOBOARD5:4;
end;
hence contradiction by A111,A126,NAT_1:13;
end;
now
assume j >= k;
then
A130: F*(i,j)`2 >= F*(m,k)`2 by A24,A28,A45,A33,A44,A41,SPRECT_3:12;
j1 > j2 by A111,NAT_1:13;
hence contradiction by A21,A23,A4,A6,A12,A14,A13,A16,A27,A15,A130,
GOBOARD5:4;
end;
then j+1 <= k by NAT_1:13;
then j+1 = k by A112,XXREAL_0:1;
then
A131: right_cell(f,n) = cell(F,m -'1,j) & left_cell(f,n) = cell(F,m,j) by A1
,A20,A21,A22,A23,A30,A29,GOBOARD5:def 6,def 7;
A132: now
assume
A133: m <> i;
per cases by A133,XXREAL_0:1;
suppose
m < i;
hence contradiction by A21,A23,A24,A45,A39,A36,A43,A46,A4,A6,A26,A17
,A111,GOBOARD5:3;
end;
suppose
m > i;
hence contradiction by A21,A23,A28,A45,A39,A42,A43,A46,A4,A6,A26,A17
,A111,GOBOARD5:3;
end;
end;
right_cell(f,n,G) = cell(G,i1-'1,j2) & left_cell(f,n,G) = cell(G,i1,
j2) by A1,A2,A3,A4,A5,A6,A9,A111,Def1,Def2;
hence thesis by A19,A22,A23,A5,A6,A111,A132,A131,Th10,Th11;
end;
end;
definition
let f,G,k;
assume 1 <= k & k+1 <= len f & f is_sequence_on G;
then consider i1,j1,i2,j2 being Nat such that
A1: [i1,j1] in Indices G & f/.k = G*(i1,j1) & [i2,j2] in Indices G & f/.
( k+1) = G*(i2,j2) and
A2: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or
i1 = i2 & j1 = j2+1 by JORDAN8:3;
func front_right_cell(f,k,G) -> Subset of TOP-REAL 2 means
:Def3:
for i1,j1,
i2,j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f/.
k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 & j1+1 = j2 & it = cell(G,i2
,j2) or i1+1 = i2 & j1 = j2 & it = cell(G,i2,j2-'1) or i1 = i2+1 & j1 = j2 & it
= cell(G,i2-'1,j2) or i1 = i2 & j1 = j2+1 & it = cell(G,i2-'1,j2-'1);
existence
proof
per cases by A2;
suppose
A3: i1 = i2 & j1+1 = j2;
take cell(G,i2,j2);
let i19,j19,i29,j29 be Nat;
assume
A4: [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19,
j19) & f/.(k+1) = G*(i29,j29);
then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
hence thesis by A1,A3,A4,GOBOARD1:5;
end;
suppose
A5: i1+1 = i2 & j1 = j2;
take cell(G,i2,j2-'1);
let i19,j19,i29,j29 be Nat;
assume
A6: [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19,
j19) & f/.(k+1) = G*(i29,j29);
then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
hence thesis by A1,A5,A6,GOBOARD1:5;
end;
suppose
A7: i1 = i2+1 & j1 = j2;
take cell(G,i2-'1,j2);
let i19,j19,i29,j29 be Nat;
assume
A8: [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
,j19) & f/.(k+1) = G*(i29,j29);
then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
hence thesis by A1,A7,A8,GOBOARD1:5;
end;
suppose
A9: i1 = i2 & j1 = j2+1;
take cell(G,i2-'1,j2-'1);
let i19,j19,i29,j29 be Nat;
assume
A10: [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
,j19) & f/.(k+1) = G*(i29,j29);
then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
hence thesis by A1,A9,A10,GOBOARD1:5;
end;
end;
uniqueness
proof
let P1,P2 be Subset of TOP-REAL 2 such that
A11: for i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & [
i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 &
j1+1 = j2 & P1 = cell(G,i2,j2) or i1+1 = i2 & j1 = j2 & P1 = cell(G,i2,j2-'1)
or i1 = i2+1 & j1 = j2 & P1 = cell(G,i2-'1,j2) or i1 = i2 & j1 = j2+1 & P1 =
cell(G,i2-'1,j2-'1) and
A12: for i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & [
i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 &
j1+1 = j2 & P2 = cell(G,i2,j2) or i1+1 = i2 & j1 = j2 & P2 = cell(G,i2,j2-'1)
or i1 = i2+1 & j1 = j2 & P2 = cell(G,i2-'1,j2) or i1 = i2 & j1 = j2+1 & P2 =
cell(G,i2-'1,j2-'1);
per cases by A2;
suppose
A13: i1 = i2 & j1+1 = j2;
A14: j2 <= j2+1 by NAT_1:11;
A15: j1 < j2 by A13,XREAL_1:29;
hence P1 = cell(G,i2,j2) by A1,A11,A14
.= P2 by A1,A12,A15,A14;
end;
suppose
A16: i1+1 = i2 & j1 = j2;
A17: i2 <= i2+1 by NAT_1:11;
A18: i1 < i2 by A16,XREAL_1:29;
hence P1 = cell(G,i2,j2-'1) by A1,A11,A17
.= P2 by A1,A12,A18,A17;
end;
suppose
A19: i1 = i2+1 & j1 = j2;
A20: i1 <= i1+1 by NAT_1:11;
A21: i2 < i1 by A19,XREAL_1:29;
hence P1 = cell(G,i2-'1,j2) by A1,A11,A20
.= P2 by A1,A12,A21,A20;
end;
suppose
A22: i1 = i2 & j1 = j2+1;
A23: j1 <= j1+1 by NAT_1:11;
A24: j2 < j1 by A22,XREAL_1:29;
hence P1 = cell(G,i2-'1,j2-'1) by A1,A11,A23
.= P2 by A1,A12,A24,A23;
end;
end;
func front_left_cell(f,k,G) -> Subset of TOP-REAL 2 means
:Def4:
for i1,j1,
i2,j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f/.
k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 & j1+1 = j2 & it = cell(G,i2
-'1,j2) or i1+1 = i2 & j1 = j2 & it = cell(G,i2,j2) or i1 = i2+1 & j1 = j2 & it
= cell(G,i2-'1,j2-'1) or i1 = i2 & j1 = j2+1 & it = cell(G,i2,j2-'1);
existence
proof
per cases by A2;
suppose
A25: i1 = i2 & j1+1 = j2;
take cell(G,i2-'1,j2);
let i19,j19,i29,j29 be Nat;
assume
A26: [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
,j19) & f/.(k+1) = G*(i29,j29);
then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
hence thesis by A1,A25,A26,GOBOARD1:5;
end;
suppose
A27: i1+1 = i2 & j1 = j2;
take cell(G,i2,j2);
let i19,j19,i29,j29 be Nat;
assume
A28: [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
,j19) & f/.(k+1) = G*(i29,j29);
then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
hence thesis by A1,A27,A28,GOBOARD1:5;
end;
suppose
A29: i1 = i2+1 & j1 = j2;
take cell(G,i2-'1,j2-'1);
let i19,j19,i29,j29 be Nat;
assume
A30: [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
,j19) & f/.(k+1) = G*(i29,j29);
then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
hence thesis by A1,A29,A30,GOBOARD1:5;
end;
suppose
A31: i1 = i2 & j1 = j2+1;
take cell(G,i2,j2-'1);
let i19,j19,i29,j29 be Nat;
assume
A32: [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
,j19) & f/.(k+1) = G*(i29,j29);
then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
hence thesis by A1,A31,A32,GOBOARD1:5;
end;
end;
uniqueness
proof
let P1,P2 be Subset of TOP-REAL 2 such that
A33: for i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & [
i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 &
j1+1 = j2 & P1 = cell(G,i2-'1,j2) or i1+1 = i2 & j1 = j2 & P1 = cell(G,i2,j2)
or i1 = i2+1 & j1 = j2 & P1 = cell(G,i2-'1,j2-'1) or i1 = i2 & j1 = j2+1 & P1 =
cell(G,i2,j2-'1) and
A34: for i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & [
i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds i1 = i2 &
j1+1 = j2 & P2 = cell(G,i2-'1,j2) or i1+1 = i2 & j1 = j2 & P2 = cell(G,i2,j2)
or i1 = i2+1 & j1 = j2 & P2 = cell(G,i2-'1,j2-'1) or i1 = i2 & j1 = j2+1 & P2 =
cell(G,i2,j2-'1);
per cases by A2;
suppose
A35: i1 = i2 & j1+1 = j2;
A36: j2 <= j2+1 by NAT_1:11;
A37: j1 < j2 by A35,XREAL_1:29;
hence P1 = cell(G,i2-'1,j2) by A1,A33,A36
.= P2 by A1,A34,A37,A36;
end;
suppose
A38: i1+1 = i2 & j1 = j2;
A39: i2 <= i2+1 by NAT_1:11;
A40: i1 < i2 by A38,XREAL_1:29;
hence P1 = cell(G,i2,j2) by A1,A33,A39
.= P2 by A1,A34,A40,A39;
end;
suppose
A41: i1 = i2+1 & j1 = j2;
A42: i1 <= i1+1 by NAT_1:11;
A43: i2 < i1 by A41,XREAL_1:29;
hence P1 = cell(G,i2-'1,j2-'1) by A1,A33,A42
.= P2 by A1,A34,A43,A42;
end;
suppose
A44: i1 = i2 & j1 = j2+1;
A45: j1 <= j1+1 by NAT_1:11;
A46: j2 < j1 by A44,XREAL_1:29;
hence P1 = cell(G,i2,j2-'1) by A1,A33,A45
.= P2 by A1,A34,A46,A45;
end;
end;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,j
+1] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1) implies
front_left_cell(f,k,G) = cell(G,i-'1,j+1)
proof
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
,j+1] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1);
hence thesis by A1,Def4;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,j
+1] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1) implies
front_right_cell(f,k,G) = cell(G,i,j+1)
proof
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
,j+1] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1);
hence thesis by A1,Def3;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i+1
,j] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j) implies
front_left_cell(f,k,G) = cell(G,i+1,j)
proof
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
+1,j] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j);
hence thesis by A1,Def4;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i+1
,j] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j) implies
front_right_cell(f,k,G) = cell(G,i+1,j-'1)
proof
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
+1,j] in Indices G & f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j);
hence thesis by A1,Def3;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i+1
,j] in Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j) implies
front_left_cell(f,k,G) = cell(G,i-'1,j-'1)
proof
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
+1,j] in Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j);
hence thesis by A1,Def4;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i+1
,j] in Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j) implies
front_right_cell(f,k,G) = cell(G,i-'1,j)
proof
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i
+1,j] in Indices G & f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j);
hence thesis by A1,Def3;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j+1] in Indices G & [i
,j] in Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j) implies
front_left_cell(f,k,G) = cell(G,i,j-'1)
proof
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j+1] in Indices G &
[i,j] in Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j);
hence thesis by A1,Def4;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G & [i,j+1] in Indices G & [i
,j] in Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j) implies
front_right_cell(f,k,G) = cell(G,i-'1,j-'1)
proof
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
assume 1 <= k & k+1 <= len f & f is_sequence_on G & [i,j+1] in Indices G &
[i,j] in Indices G & f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j);
hence thesis by A1,Def3;
end;
theorem
1 <= k & k+1 <= len f & f is_sequence_on G & k+1 <= n implies
front_left_cell(f,k,G) = front_left_cell(f|n,k,G) & front_right_cell(f,k,G) =
front_right_cell(f|n,k,G)
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f and
A3: f is_sequence_on G and
A4: k+1 <= n;
per cases;
suppose
len f <= n;
hence thesis by FINSEQ_1:58;
end;
suppose
n < len f;
then
A5: len(f|n) = n by FINSEQ_1:59;
then k in dom(f|n) by A1,A4,SEQ_4:134;
then
A6: (f|n)/.k = f/.k by FINSEQ_4:70;
k+1 in dom(f|n) by A1,A4,A5,SEQ_4:134;
then
A7: (f|n)/.(k+1) = f/.(k+1) by FINSEQ_4:70;
set lf = front_left_cell(f,k,G), lfn = front_left_cell(f|n,k,G), rf =
front_right_cell(f,k,G), rfn = front_right_cell(f|n,k,G);
A8: f|n is_sequence_on G by A3,GOBOARD1:22;
consider i1,j1,i2,j2 being Nat such that
A9: [i1,j1] in Indices G & f/.k = G*(i1,j1) & [i2,j2] in Indices G & f
/.( k+1) = G*(i2,j2) and
A10: 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:3;
A11: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A12: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
now
per cases by A10;
suppose
A13: i1 = i2 & j1+1 = j2;
hence lf = cell(G,i2-'1,j2) by A1,A2,A3,A9,A11,Def4
.= lfn by A1,A4,A9,A11,A8,A5,A6,A7,A13,Def4;
thus rf = cell(G,i2,j2) by A1,A2,A3,A9,A11,A13,Def3
.= rfn by A1,A4,A9,A11,A8,A5,A6,A7,A13,Def3;
end;
suppose
A14: i1+1 = i2 & j1 = j2;
hence lf = cell(G,i2,j2) by A1,A2,A3,A9,A12,Def4
.= lfn by A1,A4,A9,A12,A8,A5,A6,A7,A14,Def4;
thus rf = cell(G,i2,j2-'1) by A1,A2,A3,A9,A12,A14,Def3
.= rfn by A1,A4,A9,A12,A8,A5,A6,A7,A14,Def3;
end;
suppose
A15: i1 = i2+1 & j1 = j2;
hence lf = cell(G,i2-'1,j2-'1) by A1,A2,A3,A9,A12,Def4
.= lfn by A1,A4,A9,A12,A8,A5,A6,A7,A15,Def4;
thus rf = cell(G,i2-'1,j2) by A1,A2,A3,A9,A12,A15,Def3
.= rfn by A1,A4,A9,A12,A8,A5,A6,A7,A15,Def3;
end;
suppose
A16: i1 = i2 & j1 = j2+1;
hence lf = cell(G,i2,j2-'1) by A1,A2,A3,A9,A11,Def4
.= lfn by A1,A4,A9,A11,A8,A5,A6,A7,A16,Def4;
thus rf = cell(G,i2-'1,j2-'1) by A1,A2,A3,A9,A11,A16,Def3
.= rfn by A1,A4,A9,A11,A8,A5,A6,A7,A16,Def3;
end;
end;
hence thesis;
end;
end;
definition
let D be set;
let f be FinSequence of D, G be (Matrix of D), k;
pred f turns_right k,G means
for i1,j1,i2,j2 being Nat st
[i1,j1] in Indices G & [i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(
i2,j2) holds i1 = i2 & j1+1 = j2 & [i2+1,j2] in Indices G & f/.(k+2) = G*(i2+1,
j2) or i1+1 = i2 & j1 = j2 & [i2,j2-'1] in Indices G & f/.(k+2) = G* (i2,j2-'1)
or i1 = i2+1 & j1 = j2 & [i2,j2+1] in Indices G & f/.(k+2) = G*(i2,j2+1) or i1
= i2 & j1 = j2+1 & [i2-'1,j2] in Indices G & f/.(k+2) = G*(i2-'1,j2);
pred f turns_left k,G means
for i1,j1,i2,j2 being Nat st [
i1,j1] in Indices G & [i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) = G*(
i2,j2) holds i1 = i2 & j1+1 = j2 & [i2-'1,j2] in Indices G & f/.(k+2) = G* (i2
-'1,j2) or i1+1 = i2 & j1 = j2 & [i2,j2+1] in Indices G & f/.(k+2) = G*(i2,j2+1
) or i1 = i2+1 & j1 = j2 & [i2,j2-'1] in Indices G & f/.(k+2) = G* (i2,j2-'1)
or i1 = i2 & j1 = j2+1 & [i2+1,j2] in Indices G & f/.(k+2) = G*(i2+1,j2);
pred f goes_straight k,G means
for i1,j1,i2,j2 being Nat
st [i1,j1] in Indices G & [i2,j2] in Indices G & f/.k = G*(i1,j1) & f/.(k+1) =
G*(i2,j2) holds i1 = i2 & j1+1 = j2 & [i2,j2+1] in Indices G & f/.(k+2) = G*(i2
,j2+1) or i1+1 = i2 & j1 = j2 & [i2+1,j2] in Indices G & f/.(k+2) = G*(i2+1,j2)
or i1 = i2+1 & j1 = j2 & [i2-'1,j2] in Indices G & f/.(k+2) = G* (i2-'1,j2) or
i1 = i2 & j1 = j2+1 & [i2,j2-'1] in Indices G & f/.(k+2) = G*(i2,j2-'1);
end;
reserve D for set,
f,f1,f2 for FinSequence of D,
G for Matrix of D;
theorem
1 <= k & k+2 <= n & f|n turns_right k,G implies f turns_right k,G
proof
assume that
A1: 1 <= k & k+2 <= n and
A2: f|n turns_right k,G;
per cases;
suppose
len f <= n;
hence thesis by A2,FINSEQ_1:58;
end;
suppose
A3: n < len f;
let i19,j19,i29,j29 be Nat;
A4: len(f|n) = n by A3,FINSEQ_1:59;
then k+1 in dom(f|n) by A1,SEQ_4:135;
then
A5: (f|n)/.(k+1) = f/.(k+1) by FINSEQ_4:70;
k+2 in dom(f|n) by A1,A4,SEQ_4:135;
then
A6: (f|n)/.(k+2) = f/.(k+2 ) by FINSEQ_4:70;
k in dom(f|n) by A1,A4,SEQ_4:135;
then (f|n)/.k = f/.k by FINSEQ_4:70;
hence thesis by A2,A5,A6;
end;
end;
theorem
1 <= k & k+2 <= n & f|n turns_left k,G implies f turns_left k,G
proof
assume that
A1: 1 <= k & k+2 <= n and
A2: f|n turns_left k,G;
per cases;
suppose
len f <= n;
hence thesis by A2,FINSEQ_1:58;
end;
suppose
A3: n < len f;
let i19,j19,i29,j29 be Nat;
A4: len(f|n) = n by A3,FINSEQ_1:59;
then k+1 in dom(f|n) by A1,SEQ_4:135;
then
A5: (f|n)/.(k+1) = f/.(k+1) by FINSEQ_4:70;
k+2 in dom(f|n) by A1,A4,SEQ_4:135;
then
A6: (f|n)/.(k+2) = f/.(k+2 ) by FINSEQ_4:70;
k in dom(f|n) by A1,A4,SEQ_4:135;
then (f|n)/.k = f/.k by FINSEQ_4:70;
hence thesis by A2,A5,A6;
end;
end;
theorem
1 <= k & k+2 <= n & f|n goes_straight k,G implies f goes_straight k,G
proof
assume that
A1: 1 <= k & k+2 <= n and
A2: f|n goes_straight k,G;
per cases;
suppose
len f <= n;
hence thesis by A2,FINSEQ_1:58;
end;
suppose
A3: n < len f;
let i19,j19,i29,j29 be Nat;
A4: len(f|n) = n by A3,FINSEQ_1:59;
then k+1 in dom(f|n) by A1,SEQ_4:135;
then
A5: (f|n)/.(k+1) = f/.(k+1) by FINSEQ_4:70;
k+2 in dom(f|n) by A1,A4,SEQ_4:135;
then
A6: (f|n)/.(k+2) = f/.(k+2 ) by FINSEQ_4:70;
k in dom(f|n) by A1,A4,SEQ_4:135;
then (f|n)/.k = f/.k by FINSEQ_4:70;
hence thesis by A2,A5,A6;
end;
end;
theorem
1 < k & k+1 <= len f1 & k+1 <= len f2 & f1 is_sequence_on G & f1|k =
f2|k & f1 turns_right k-'1,G & f2 turns_right k-'1,G implies f1|(k+1) = f2|(k+1
)
proof
assume that
A1: 1 < k and
A2: k+1 <= len f1 and
A3: k+1 <= len f2 and
A4: f1 is_sequence_on G and
A5: f1|k = f2|k and
A6: f1 turns_right k-'1,G and
A7: f2 turns_right k-'1,G;
A8: 1 <= k-'1 by A1,NAT_D:49;
A9: k <= k+1 by NAT_1:12;
then k <= len(f1|k) by A2,FINSEQ_1:59,XXREAL_0:2;
then
A10: k in dom(f1|k) by A1,FINSEQ_3:25;
then
A11: f2/.k = (f2|k)/.k by A5,FINSEQ_4:70;
k-'1 <= k by NAT_D:35;
then k-'1 <= len(f1|k) by A2,A9,FINSEQ_1:59,XXREAL_0:2;
then
A12: k-'1 in dom(f1|k) by A8,FINSEQ_3:25;
then
A13: f2/.(k-'1) = (f2|k)/.(k-'1) by A5,FINSEQ_4:70;
A14: f1/.k = (f1|k)/.k by A10,FINSEQ_4:70;
A15: f1/.(k-'1) = (f1|k)/.(k-'1) by A12,FINSEQ_4:70;
A16: k = k-'1+1 by A1,XREAL_1:235;
k <= len f1 by A2,A9,XXREAL_0:2;
then consider i1,j1,i2,j2 being Nat such that
A17: [i1,j1] in Indices G & f1/.(k-'1) = G*(i1,j1) & [i2,j2] in Indices
G & f1/.k = G*(i2,j2) and
A18: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A4,A8,A16,JORDAN8:3;
A19: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A20: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
now
per cases by A18;
suppose
A21: i1 = i2 & j1+1 = j2;
hence f1/.(k+1) = G*(i2+1,j2) by A6,A16,A17,A19
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A21;
end;
suppose
A22: i1+1 = i2 & j1 = j2;
hence f1/.(k+1) = G*(i2,j2-'1) by A6,A16,A17,A20
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A22;
end;
suppose
A23: i1 = i2+1 & j1 = j2;
hence f1/.(k+1) = G*(i2,j2+1) by A6,A16,A17,A20
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A23;
end;
suppose
A24: i1 = i2 & j1 = j2+1;
hence f1/.(k+1) = G*(i2-'1,j2) by A6,A16,A17,A19
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A24;
end;
end;
hence f1|(k+1) = (f2|k)^<*f2/.(k+1)*> by A2,A5,FINSEQ_5:82
.= f2|(k+1) by A3,FINSEQ_5:82;
end;
theorem
1 < k & k+1 <= len f1 & k+1 <= len f2 & f1 is_sequence_on G & f1|k =
f2|k & f1 turns_left k-'1,G & f2 turns_left k-'1,G implies f1|(k+1) = f2|(k+1)
proof
assume that
A1: 1 < k and
A2: k+1 <= len f1 and
A3: k+1 <= len f2 and
A4: f1 is_sequence_on G and
A5: f1|k = f2|k and
A6: f1 turns_left k-'1,G and
A7: f2 turns_left k-'1,G;
A8: 1 <= k-'1 by A1,NAT_D:49;
A9: k <= k+1 by NAT_1:12;
then k <= len(f1|k) by A2,FINSEQ_1:59,XXREAL_0:2;
then
A10: k in dom(f1|k) by A1,FINSEQ_3:25;
then
A11: f2/.k = (f2|k)/.k by A5,FINSEQ_4:70;
k-'1 <= k by NAT_D:35;
then k-'1 <= len(f1|k) by A2,A9,FINSEQ_1:59,XXREAL_0:2;
then
A12: k-'1 in dom(f1|k) by A8,FINSEQ_3:25;
then
A13: f2/.(k-'1) = (f2|k)/.(k-'1) by A5,FINSEQ_4:70;
A14: f1/.k = (f1|k)/.k by A10,FINSEQ_4:70;
A15: f1/.(k-'1) = (f1|k)/.(k-'1) by A12,FINSEQ_4:70;
A16: k = k-'1+1 by A1,XREAL_1:235;
k <= len f1 by A2,A9,XXREAL_0:2;
then consider i1,j1,i2,j2 being Nat such that
A17: [i1,j1] in Indices G & f1/.(k-'1) = G*(i1,j1) & [i2,j2] in Indices
G & f1/.k = G*(i2,j2) and
A18: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A4,A8,A16,JORDAN8:3;
A19: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A20: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
now
per cases by A18;
suppose
A21: i1 = i2 & j1+1 = j2;
hence f1/.(k+1) = G*(i2-'1,j2) by A6,A16,A17,A19
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A21;
end;
suppose
A22: i1+1 = i2 & j1 = j2;
hence f1/.(k+1) = G*(i2,j2+1) by A6,A16,A17,A20
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A22;
end;
suppose
A23: i1 = i2+1 & j1 = j2;
hence f1/.(k+1) = G*(i2,j2-'1) by A6,A16,A17,A20
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A23;
end;
suppose
A24: i1 = i2 & j1 = j2+1;
hence f1/.(k+1) = G*(i2+1,j2) by A6,A16,A17,A19
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A24;
end;
end;
hence f1|(k+1) = (f2|k)^<*f2/.(k+1)*> by A2,A5,FINSEQ_5:82
.= f2|(k+1) by A3,FINSEQ_5:82;
end;
theorem
1 < k & k+1 <= len f1 & k+1 <= len f2 & f1 is_sequence_on G & f1|k =
f2|k & f1 goes_straight k-'1,G & f2 goes_straight k-'1,G implies f1|(k+1) = f2|
(k+1)
proof
assume that
A1: 1 < k and
A2: k+1 <= len f1 and
A3: k+1 <= len f2 and
A4: f1 is_sequence_on G and
A5: f1|k = f2|k and
A6: f1 goes_straight k-'1,G and
A7: f2 goes_straight k-'1,G;
A8: 1 <= k-'1 by A1,NAT_D:49;
A9: k <= k+1 by NAT_1:12;
then k <= len(f1|k) by A2,FINSEQ_1:59,XXREAL_0:2;
then
A10: k in dom(f1|k) by A1,FINSEQ_3:25;
then
A11: f2/.k = (f2|k)/.k by A5,FINSEQ_4:70;
k-'1 <= k by NAT_D:35;
then k-'1 <= len(f1|k) by A2,A9,FINSEQ_1:59,XXREAL_0:2;
then
A12: k-'1 in dom(f1|k) by A8,FINSEQ_3:25;
then
A13: f2/.(k-'1) = (f2|k)/.(k-'1) by A5,FINSEQ_4:70;
A14: f1/.k = (f1|k)/.k by A10,FINSEQ_4:70;
A15: f1/.(k-'1) = (f1|k)/.(k-'1) by A12,FINSEQ_4:70;
A16: k = k-'1+1 by A1,XREAL_1:235;
k <= len f1 by A2,A9,XXREAL_0:2;
then consider i1,j1,i2,j2 being Nat such that
A17: [i1,j1] in Indices G & f1/.(k-'1) = G*(i1,j1) & [i2,j2] in Indices
G & f1/.k = G*(i2,j2) and
A18: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A4,A8,A16,JORDAN8:3;
A19: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A20: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
now
per cases by A18;
suppose
A21: i1 = i2 & j1+1 = j2;
hence f1/.(k+1) = G*(i2,j2+1) by A6,A16,A17,A19
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A21;
end;
suppose
A22: i1+1 = i2 & j1 = j2;
hence f1/.(k+1) = G*(i2+1,j2) by A6,A16,A17,A20
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A22;
end;
suppose
A23: i1 = i2+1 & j1 = j2;
hence f1/.(k+1) = G*(i2-'1,j2) by A6,A16,A17,A20
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A23;
end;
suppose
A24: i1 = i2 & j1 = j2+1;
hence f1/.(k+1) = G*(i2,j2-'1) by A6,A16,A17,A19
.= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A24;
end;
end;
hence f1|(k+1) = (f2|k)^<*f2/.(k+1)*> by A2,A5,FINSEQ_5:82
.= f2|(k+1) by A3,FINSEQ_5:82;
end;