:: On the Go Board of a Standard Special Circular Sequence
:: by Andrzej Trybulec
::
:: Received October 15, 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, XBOOLE_0, FINSEQ_1, EUCLID, REAL_1, PRE_TOPC, GOBOARD1,
COMPLEX1, ARYTM_1, XXREAL_0, ARYTM_3, CARD_1, SUPINF_2, RLTOPSP1,
MCART_1, RELAT_1, TREES_1, SPPOL_1, GOBOARD2, MATRIX_1, PARTFUN1,
TOPREAL1, TOPS_1, GOBOARD5, TARSKI, FUNCT_1, FINSET_1, FINSEQ_6, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0,
XCMPLX_0, COMPLEX1, REAL_1, XREAL_0, NAT_1, INT_2, NAT_D, FUNCT_1,
PARTFUN1, FINSEQ_1, FINSET_1, STRUCT_0, MATRIX_0, MATRIX_1, PRE_TOPC,
TOPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2,
SPPOL_1, FINSEQ_6, GOBOARD5;
constructors PARTFUN1, XXREAL_0, REAL_1, NAT_1, INT_2, NAT_D, TOPS_1,
GOBOARD2, SPPOL_1, GOBOARD5, GOBOARD1, DOMAIN_1, BINOP_2, RELSET_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, INT_1, FINSEQ_1, STRUCT_0, EUCLID,
GOBOARD2, GOBOARD5, FINSET_1, CARD_1, XREAL_0, NAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities RLTOPSP1, RLVECT_1;
theorems GOBOARD5, TOPS_1, EUCLID, GOBOARD1, TOPREAL3, ABSVALUE, TARSKI,
SPPOL_1, TOPREAL1, GOBOARD2, FINSEQ_3, NAT_1, FINSEQ_6, GOBOARD6,
MATRIX_0, FINSEQ_1, CARD_2, FINSEQ_5, XBOOLE_0, XREAL_1, FUNCT_1,
XXREAL_0, RLTOPSP1, SEQM_3, RLVECT_1;
schemes NAT_1;
begin
reserve f for non empty FinSequence of TOP-REAL 2,
i,j,k,k1,k2,n,i1,i2,j1,j2 for Nat,
r,s,r1,r2 for Real,
p,q,p1,q1 for Point of TOP-REAL 2,
G for Go-board;
theorem Th1:
|.r1-r2.| > s implies r1+s < r2 or r2+s < r1
proof
assume
A1: |.r1-r2.| > s;
now
per cases;
case
r1 < r2;
then r1 - r2 < 0 by XREAL_1:49;
then |.r1-r2.| = -(r1-r2) by ABSVALUE:def 1
.= r2 - r1;
hence r1+s < r2 by A1,XREAL_1:20;
end;
case
r2 <= r1;
then r1 - r2 >= 0 by XREAL_1:48;
then |.r1-r2.| = r1 - r2 by ABSVALUE:def 1;
hence r2+s < r1 by A1,XREAL_1:20;
end;
end;
hence thesis;
end;
theorem Th2:
|.r-s.| = 0 iff r = s
proof
hereby
assume |.r-s.| = 0;
then r - s = 0 by ABSVALUE:2;
hence r = s;
end;
assume r = s;
hence thesis by ABSVALUE:2;
end;
theorem Th3:
for p,p1,q being Point of TOP-REAL n st p + p1 = q + p1 holds p = q
proof
let p,p1,q be Point of TOP-REAL n such that
A1: p + p1 = q + p1;
thus p = p + 0.TOP-REAL n by RLVECT_1:4
.= p + (p1 - p1) by RLVECT_1:5
.= p + p1 - p1 by RLVECT_1:def 3
.= q + (p1 - p1) by A1,RLVECT_1:def 3
.= q + 0.TOP-REAL n by RLVECT_1:5
.= q by RLVECT_1:4;
end;
theorem
for p,p1,q being Point of TOP-REAL n st p1 + p = p1 + q holds p = q by Th3;
theorem Th5:
p1 in LSeg(p,q) & p`1 = q`1 implies p1`1 = q`1
proof
assume p1 in LSeg(p,q);
then consider r such that
A1: p1 = (1-r)*p+r*q and
0<=r and
r<=1;
assume
A2: p`1 = q`1;
p1`1 = ((1-r)*p)`1+(r*q)`1 by A1,TOPREAL3:2
.= ((1-r)*p)`1+r*q`1 by TOPREAL3:4
.= (1-r)*p`1+r*q`1 by TOPREAL3:4;
hence thesis by A2;
end;
theorem Th6:
p1 in LSeg(p,q) & p`2 = q`2 implies p1`2 = q`2
proof
assume p1 in LSeg(p,q);
then consider r such that
A1: p1 = (1-r)*p+r*q and
0<=r and
r<=1;
assume
A2: p`2 = q`2;
p1`2 = ((1-r)*p)`2+(r*q)`2 by A1,TOPREAL3:2
.= ((1-r)*p)`2+r*q`2 by TOPREAL3:4
.= (1-r)*p`2+r*q`2 by TOPREAL3:4;
hence thesis by A2;
end;
theorem Th7:
p`1 = q`1 & q`1 = p1`1 & p`2 <= q`2 & q`2 <= p1`2 implies q in LSeg(p,p1)
proof
assume that
A1: p`1 = q`1 and
A2: q`1 = p1`1 and
A3: p`2 <= q`2 & q`2 <= p1`2;
A4: p`2 <= p1`2 by A3,XXREAL_0:2;
per cases by A4,XXREAL_0:1;
suppose
A5: p`2 = p1`2;
then p`2 = q`2 by A3,XXREAL_0:1;
then
A6: q = |[p`1,p`2]| by A1,EUCLID:53
.= p by EUCLID:53;
p = |[p1`1,p1`2]| by A1,A2,A5,EUCLID:53
.= p1 by EUCLID:53;
then LSeg(p,p1) = {p} by RLTOPSP1:70;
hence thesis by A6,TARSKI:def 1;
end;
suppose
A7: p`2 < p1`2;
A8: q in {q1: q1`1 = q`1 & p`2 <= q1`2 & q1`2 <= p1`2} by A3;
p = |[q`1,p`2]| & p1 = |[q`1,p1`2]| by A1,A2,EUCLID:53;
hence thesis by A7,A8,TOPREAL3:9;
end;
end;
theorem Th8:
p`1 <= q`1 & q`1 <= p1`1 & p`2 = q`2 & q`2 = p1`2 implies q in LSeg(p,p1)
proof
assume that
A1: p`1 <= q`1 & q`1 <= p1`1 and
A2: p`2 = q`2 and
A3: q`2 = p1`2;
A4: p`1 <= p1`1 by A1,XXREAL_0:2;
per cases by A4,XXREAL_0:1;
suppose
A5: p`1 = p1`1;
then p`1 = q`1 by A1,XXREAL_0:1;
then
A6: q = |[p`1,p`2]| by A2,EUCLID:53
.= p by EUCLID:53;
p = |[p1`1,p1`2]| by A2,A3,A5,EUCLID:53
.= p1 by EUCLID:53;
then LSeg(p,p1) = {p} by RLTOPSP1:70;
hence thesis by A6,TARSKI:def 1;
end;
suppose
A7: p`1 < p1`1;
A8: q in {q1: q1`2 = q`2 & p`1 <= q1`1 & q1`1 <= p1`1} by A1;
p = |[p`1,q`2]| & p1 = |[p1`1,q`2]| by A2,A3,EUCLID:53;
hence thesis by A7,A8,TOPREAL3:10;
end;
end;
theorem
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies 1/2*(G*(i,j)+G
*(i+1,j+1)) = 1/2*(G*(i,j+1)+G*(i+1,j))
proof
assume that
A1: 1 <= i and
A2: i+1 <= len G and
A3: 1 <= j and
A4: j+1 <= width G;
A5: j < width G by A4,NAT_1:13;
A6: 1 <= j+1 by NAT_1:11;
A7: 1 <= i+1 by NAT_1:11;
then
A8: G*(i+1,j)`1 = G*(i+1,1)`1 by A2,A3,A5,GOBOARD5:2
.= G*(i+1,j+1)`1 by A2,A4,A7,A6,GOBOARD5:2;
A9: i < len G by A2,NAT_1:13;
then
A10: G*(i,j)`1 = G*(i,1)`1 by A1,A3,A5,GOBOARD5:2
.= G*(i,j+1)`1 by A1,A4,A9,A6,GOBOARD5:2;
A11: G*(i+1,j+1)`2 = G*(1,j+1)`2 by A2,A4,A7,A6,GOBOARD5:1
.= G*(i,j+1)`2 by A1,A4,A9,A6,GOBOARD5:1;
A12: G*(i,j)`2 = G*(1,j)`2 by A1,A3,A9,A5,GOBOARD5:1
.= G*(i+1,j)`2 by A2,A3,A7,A5,GOBOARD5:1;
A13: (1/2*(G*(i,j)+G*(i+1,j+1)))`2 = 1/2*(G*(i,j)+G*(i+1,j+1))`2 by TOPREAL3:4
.= 1/2*(G*(i,j)`2+G*(i+1,j+1)`2) by TOPREAL3:2
.= 1/2*(G*(i,j+1)+G*(i+1,j))`2 by A12,A11,TOPREAL3:2
.= (1/2*(G*(i,j+1)+G*(i+1,j)))`2 by TOPREAL3:4;
(1/2*(G*(i,j)+G*(i+1,j+1)))`1 = 1/2*(G*(i,j)+G*(i+1,j+1))`1 by TOPREAL3:4
.= 1/2*(G*(i,j)`1+G*(i+1,j+1)`1) by TOPREAL3:2
.= 1/2*(G*(i,j+1)+G*(i+1,j))`1 by A10,A8,TOPREAL3:2
.= (1/2*(G*(i,j+1)+G*(i+1,j)))`1 by TOPREAL3:4;
hence
1/2*(G*(i,j)+G*(i+1,j+1)) = |[(1/2*(G*(i,j+1)+G*(i+1,j)))`1,(1/2*(G*(i,
j+1)+G*(i+1,j)))`2]| by A13,EUCLID:53
.= 1/2*(G*(i,j+1)+G*(i+1,j)) by EUCLID:53;
end;
theorem Th10:
LSeg(f,k) is horizontal implies ex j st 1 <= j & j <= width GoB
f & for p st p in LSeg(f,k) holds p`2 = (GoB f)*(1,j)`2
proof
assume
A1: LSeg(f,k) is horizontal;
per cases;
suppose
A2: 1 <= k & k+1 <= len f;
k <= k+1 by NAT_1:11;
then k <= len f by A2,XXREAL_0:2;
then k in dom f by A2,FINSEQ_3:25;
then consider i,j such that
A3: [i,j] in Indices GoB f and
A4: f/.k = (GoB f)*(i,j) by GOBOARD2:14;
take j;
thus
A5: 1 <= j & j <= width GoB f by A3,MATRIX_0:32;
A6: f/.k in LSeg(f,k) by A2,TOPREAL1:21;
let p;
A7: 1 <= i & i <= len GoB f by A3,MATRIX_0:32;
assume p in LSeg(f,k);
hence p`2 = (f/.k)`2 by A1,A6,SPPOL_1:def 2
.= (GoB f)*(1,j)`2 by A4,A5,A7,GOBOARD5:1;
end;
suppose
A8: not(1 <= k & k+1 <= len f);
take 1;
width GoB f <> 0 by MATRIX_0:def 10;
hence 1 <= 1 & 1 <= width GoB f by NAT_1:14;
thus thesis by A8,TOPREAL1:def 3;
end;
end;
theorem Th11:
LSeg(f,k) is vertical implies ex i st 1 <= i & i <= len GoB f &
for p st p in LSeg(f,k) holds p`1 = (GoB f)*(i,1)`1
proof
assume
A1: LSeg(f,k) is vertical;
per cases;
suppose
A2: 1 <= k & k+1 <= len f;
k <= k+1 by NAT_1:11;
then k <= len f by A2,XXREAL_0:2;
then k in dom f by A2,FINSEQ_3:25;
then consider i,j such that
A3: [i,j] in Indices GoB f and
A4: f/.k = (GoB f)*(i,j) by GOBOARD2:14;
take i;
thus
A5: 1 <= i & i <= len GoB f by A3,MATRIX_0:32;
A6: f/.k in LSeg(f,k) by A2,TOPREAL1:21;
let p;
A7: 1 <= j & j <= width GoB f by A3,MATRIX_0:32;
assume p in LSeg(f,k);
hence p`1 = (f/.k)`1 by A1,A6,SPPOL_1:def 3
.= (GoB f)*(i,1)`1 by A4,A5,A7,GOBOARD5:2;
end;
suppose
A8: not(1 <= k & k+1 <= len f);
take 1;
0 <> len GoB f by MATRIX_0:def 10;
hence 1 <= 1 & 1 <= len GoB f by NAT_1:14;
thus thesis by A8,TOPREAL1:def 3;
end;
end;
theorem
f is special & i <= len GoB f & j <= width GoB f implies Int cell(GoB
f,i,j) misses L~f
proof
assume that
A1: f is special and
A2: i <= len GoB f and
A3: j <= width GoB f;
A4: Int cell(GoB f,i,j) = Int(v_strip(GoB f,i) /\ h_strip(GoB f,j)) by
GOBOARD5:def 3
.= Int v_strip(GoB f,i) /\ Int h_strip(GoB f,j) by TOPS_1:17;
assume Int cell(GoB f,i,j) meets L~f;
then consider x be object such that
A5: x in Int cell(GoB f,i,j) and
A6: x in L~f by XBOOLE_0:3;
L~f = union { LSeg(f,k) : 1 <= k & k+1 <= len f } by TOPREAL1:def 4;
then consider X being set such that
A7: x in X and
A8: X in { LSeg(f,k) : 1 <= k & k+1 <= len f } by A6,TARSKI:def 4;
consider k such that
A9: X = LSeg(f,k) and
1 <= k and
k+1 <= len f by A8;
reconsider p = x as Point of TOP-REAL 2 by A7,A9;
per cases by A1,SPPOL_1:19;
suppose
LSeg(f,k) is horizontal;
then consider j0 being Nat such that
A10: 1 <= j0 and
A11: j0 <= width GoB f and
A12: for p st p in LSeg(f,k) holds p`2 = (GoB f)*(1,j0)`2 by Th10;
now
A13: j0 > j implies j0 >= j+1 by NAT_1:13;
assume
A14: p in Int h_strip(GoB f,j);
per cases by A13,XXREAL_0:1;
suppose
A15: j0 < j;
0 <> len GoB f by MATRIX_0:def 10;
then 1 <= len GoB f by NAT_1:14;
then
A16: (GoB f)*(1,j)`2 > (GoB f)*(1,j0)`2 by A3,A10,A15,GOBOARD5:4;
j >= 1 by A10,A15,XXREAL_0:2;
then p`2 > (GoB f)*(1,j)`2 by A3,A14,GOBOARD6:27;
hence contradiction by A7,A9,A12,A16;
end;
suppose
j0 = j;
then p`2 > (GoB f)*(1,j0)`2 by A10,A11,A14,GOBOARD6:27;
hence contradiction by A7,A9,A12;
end;
suppose
A17: j0 > j+1;
then j + 1 <= width GoB f by A11,XXREAL_0:2;
then j < width GoB f by NAT_1:13;
then
A18: p`2 < (GoB f)*(1,j+1)`2 by A14,GOBOARD6:28;
0 <> len GoB f by MATRIX_0:def 10;
then
A19: 1 <= len GoB f by NAT_1:14;
j+1 >= 1 by NAT_1:11;
then (GoB f)*(1,j+1)`2 < (GoB f)*(1,j0)`2 by A11,A17,A19,GOBOARD5:4;
hence contradiction by A7,A9,A12,A18;
end;
suppose
A20: j0 = j+1;
then j < width GoB f by A11,NAT_1:13;
then p`2 < (GoB f)*(1,j0)`2 by A14,A20,GOBOARD6:28;
hence contradiction by A7,A9,A12;
end;
end;
hence contradiction by A5,A4,XBOOLE_0:def 4;
end;
suppose
LSeg(f,k) is vertical;
then consider i0 being Nat such that
A21: 1 <= i0 and
A22: i0 <= len GoB f and
A23: for p st p in LSeg(f,k) holds p`1 = (GoB f)*(i0,1)`1 by Th11;
now
A24: i0 > i implies i0 >= i+1 by NAT_1:13;
assume
A25: p in Int v_strip(GoB f,i);
per cases by A24,XXREAL_0:1;
suppose
A26: i0 < i;
0 <> width GoB f by MATRIX_0:def 10;
then 1 <= width GoB f by NAT_1:14;
then
A27: (GoB f)*(i,1)`1 > (GoB f)*(i0,1)`1 by A2,A21,A26,GOBOARD5:3;
i >= 1 by A21,A26,XXREAL_0:2;
then p`1 > (GoB f)*(i,1)`1 by A2,A25,GOBOARD6:29;
hence contradiction by A7,A9,A23,A27;
end;
suppose
i0 = i;
then p`1 > (GoB f)*(i0,1)`1 by A21,A22,A25,GOBOARD6:29;
hence contradiction by A7,A9,A23;
end;
suppose
A28: i0 > i+1;
then i + 1 <= len GoB f by A22,XXREAL_0:2;
then i < len GoB f by NAT_1:13;
then
A29: p`1 < (GoB f)*(i+1,1)`1 by A25,GOBOARD6:30;
0 <> width GoB f by MATRIX_0:def 10;
then
A30: 1 <= width GoB f by NAT_1:14;
i+1 >= 1 by NAT_1:11;
then (GoB f)*(i+1,1)`1 < (GoB f)*(i0,1)`1 by A22,A28,A30,GOBOARD5:3;
hence contradiction by A7,A9,A23,A29;
end;
suppose
A31: i0 = i+1;
then i < len GoB f by A22,NAT_1:13;
then p`1 < (GoB f)*(i0,1)`1 by A25,A31,GOBOARD6:30;
hence contradiction by A7,A9,A23;
end;
end;
hence contradiction by A5,A4,XBOOLE_0:def 4;
end;
end;
begin :: Segments on a Go Board
theorem Th13:
1 <= i & i <= len G & 1 <= j & j+2 <= width G implies LSeg(G*(i,
j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i,j+2)) = { G*(i,j+1) }
proof
assume that
A1: 1 <= i & i <= len G and
A2: 1 <= j and
A3: j+2 <= width G;
now
let x be object;
hereby
assume
A4: x in LSeg(G*(i,j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i,j+2));
then reconsider p = x as Point of TOP-REAL 2;
A5: x in LSeg(G*(i,j),G*(i,j+1)) by A4,XBOOLE_0:def 4;
A6: p in LSeg(G*(i,j+1),G*(i,j+2)) by A4,XBOOLE_0:def 4;
j <= j+2 by NAT_1:11;
then
A7: j <= width G by A3,XXREAL_0:2;
A8: j+1 < j+2 by XREAL_1:6;
then
A9: j+1 <= width G by A3,XXREAL_0:2;
A10: 1 <= j+1 by NAT_1:11;
then G*(i,j+1)`1 = G*(i,1)`1 by A1,A9,GOBOARD5:2
.= G*(i,j)`1 by A1,A2,A7,GOBOARD5:2;
then
A11: p`1 = G*(i,j+1)`1 by A5,Th5;
j < j+1 by XREAL_1:29;
then G*(i,j)`2 < G*(i,j+1)`2 by A1,A2,A9,GOBOARD5:4;
then
A12: p`2 <= G*(i,j+1)`2 by A5,TOPREAL1:4;
G*(i,j+1)`2 < G*(i,j+2)`2 by A1,A3,A8,A10,GOBOARD5:4;
then p`2 >= G*(i,j+1)`2 by A6,TOPREAL1:4;
then p`2 = G*(i,j+1)`2 by A12,XXREAL_0:1;
hence x = G*(i,j+1) by A11,TOPREAL3:6;
end;
assume x = G*(i,j+1);
then x in LSeg(G*(i,j),G*(i,j+1)) & x in LSeg(G*(i,j+1),G*(i,j+2)) by
RLTOPSP1:68;
hence x in LSeg(G*(i,j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i,j+2)) by
XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th14:
1 <= i & i+2 <= len G & 1 <= j & j <= width G implies LSeg(G*(i,
j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+2,j)) = { G*(i+1,j) }
proof
assume that
A1: 1 <= i and
A2: i+2 <= len G and
A3: 1 <= j & j <= width G;
now
let x be object;
hereby
assume
A4: x in LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+2,j));
then reconsider p = x as Point of TOP-REAL 2;
A5: x in LSeg(G*(i,j),G*(i+1,j)) by A4,XBOOLE_0:def 4;
A6: p in LSeg(G*(i+1,j),G*(i+2,j)) by A4,XBOOLE_0:def 4;
i <= i+2 by NAT_1:11;
then
A7: i <= len G by A2,XXREAL_0:2;
A8: i+1 < i+2 by XREAL_1:6;
then
A9: i+1 <= len G by A2,XXREAL_0:2;
A10: 1 <= i+1 by NAT_1:11;
then G*(i+1,j)`2 = G*(1,j)`2 by A3,A9,GOBOARD5:1
.= G*(i,j)`2 by A1,A3,A7,GOBOARD5:1;
then
A11: p`2 = G*(i+1,j)`2 by A5,Th6;
i < i+1 by XREAL_1:29;
then G*(i,j)`1 < G*(i+1,j)`1 by A1,A3,A9,GOBOARD5:3;
then
A12: p`1 <= G*(i+1,j)`1 by A5,TOPREAL1:3;
G*(i+1,j)`1 < G*(i+2,j)`1 by A2,A3,A8,A10,GOBOARD5:3;
then p`1 >= G*(i+1,j)`1 by A6,TOPREAL1:3;
then p`1 = G*(i+1,j)`1 by A12,XXREAL_0:1;
hence x = G*(i+1,j) by A11,TOPREAL3:6;
end;
assume x = G*(i+1,j);
then x in LSeg(G*(i,j),G*(i+1,j)) & x in LSeg(G*(i+1,j),G*(i+2,j)) by
RLTOPSP1:68;
hence x in LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+2,j)) by
XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th15:
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies LSeg(G*(
i,j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i+1,j+1)) = { G*(i,j+1) }
proof
assume that
A1: 1 <= i and
A2: i+1 <= len G and
A3: 1 <= j and
A4: j+1 <= width G;
now
let x be object;
hereby
assume
A5: x in LSeg(G*(i,j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i+1,j+1));
then reconsider p = x as Point of TOP-REAL 2;
A6: x in LSeg(G*(i,j),G*(i,j+1)) by A5,XBOOLE_0:def 4;
A7: p in LSeg(G*(i,j+1),G*(i+1,j+1)) by A5,XBOOLE_0:def 4;
A8: 1 <= i+1 by NAT_1:11;
i <= i+1 by NAT_1:11;
then
A9: i <= len G by A2,XXREAL_0:2;
A10: 1 <= j+1 by NAT_1:11;
then G*(i,j+1)`2 = G*(1,j+1)`2 by A1,A4,A9,GOBOARD5:1
.= G*(i+1,j+1)`2 by A2,A4,A10,A8,GOBOARD5:1;
then
A11: p`2 = G*(i,j+1)`2 by A7,Th6;
j < j+1 by XREAL_1:29;
then j <= width G by A4,XXREAL_0:2;
then G*(i,j)`1 = G*(i,1)`1 by A1,A3,A9,GOBOARD5:2
.= G*(i,j+1)`1 by A1,A4,A9,A10,GOBOARD5:2;
then p`1 = G*(i,j+1)`1 by A6,Th5;
hence x = G*(i,j+1) by A11,TOPREAL3:6;
end;
assume x = G*(i,j+1);
then x in LSeg(G*(i,j),G*(i,j+1)) & x in LSeg(G*(i,j+1),G*(i+1,j+1)) by
RLTOPSP1:68;
hence x in LSeg(G*(i,j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i+1,j+1)) by
XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th16:
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies LSeg(G*(
i,j+1),G*(i+1,j+1)) /\ LSeg(G*(i+1,j),G*(i+1,j+1)) = { G* (i+1,j+1) }
proof
assume that
A1: 1 <= i and
A2: i+1 <= len G and
A3: 1 <= j and
A4: j+1 <= width G;
now
let x be object;
hereby
assume
A5: x in LSeg(G*(i,j+1),G*(i+1,j+1)) /\ LSeg(G*(i+1,j),G*(i+1,j+1));
then reconsider p = x as Point of TOP-REAL 2;
A6: x in LSeg(G*(i,j+1),G*(i+1,j+1)) by A5,XBOOLE_0:def 4;
A7: p in LSeg(G*(i+1,j),G*(i+1,j+1)) by A5,XBOOLE_0:def 4;
A8: 1 <= i+1 by NAT_1:11;
A9: 1 <= i+1 by NAT_1:11;
A10: 1 <= j+1 by NAT_1:11;
j < j+1 by XREAL_1:29;
then j <= width G by A4,XXREAL_0:2;
then G*(i+1,j)`1 = G*(i+1,1)`1 by A2,A3,A8,GOBOARD5:2
.= G*(i+1,j+1)`1 by A2,A4,A10,A9,GOBOARD5:2;
then
A11: p`1 = G*(i+1,j+1)`1 by A7,Th5;
i <= i+1 by NAT_1:11;
then i <= len G by A2,XXREAL_0:2;
then G*(i,j+1)`2 = G*(1,j+1)`2 by A1,A4,A10,GOBOARD5:1
.= G*(i+1,j+1)`2 by A2,A4,A10,A8,GOBOARD5:1;
then p`2 = G*(i+1,j+1)`2 by A6,Th6;
hence x = G*(i+1,j+1) by A11,TOPREAL3:6;
end;
assume x = G*(i+1,j+1);
then x in LSeg(G*(i,j+1),G*(i+1,j+1)) & x in LSeg(G*(i+1,j),G*(i+1,j+1))
by RLTOPSP1:68;
hence x in LSeg(G*(i,j+1),G*(i+1,j+1)) /\ LSeg(G*(i+1,j),G*(i+1,j+1)) by
XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th17:
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies LSeg(G*(
i,j),G*(i+1,j)) /\ LSeg(G*(i,j),G*(i,j+1)) = { G*(i,j) }
proof
assume that
A1: 1 <= i and
A2: i+1 <= len G and
A3: 1 <= j and
A4: j+1 <= width G;
now
let x be object;
hereby
assume
A5: x in LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i,j),G*(i,j+1));
then reconsider p = x as Point of TOP-REAL 2;
A6: x in LSeg(G*(i,j),G*(i+1,j)) by A5,XBOOLE_0:def 4;
A7: p in LSeg(G*(i,j),G*(i,j+1)) by A5,XBOOLE_0:def 4;
A8: 1 <= i+1 by NAT_1:11;
A9: 1 <= j+1 by NAT_1:11;
j < j+1 by XREAL_1:29;
then
A10: j <= width G by A4,XXREAL_0:2;
i <= i+1 by NAT_1:11;
then
A11: i <= len G by A2,XXREAL_0:2;
then G*(i,j)`1 = G*(i,1)`1 by A1,A3,A10,GOBOARD5:2
.= G*(i,j+1)`1 by A1,A4,A11,A9,GOBOARD5:2;
then
A12: p`1 = G*(i,j)`1 by A7,Th5;
G*(i,j)`2 = G*(1,j)`2 by A1,A3,A11,A10,GOBOARD5:1
.= G*(i+1,j)`2 by A2,A3,A8,A10,GOBOARD5:1;
then p`2 = G*(i,j)`2 by A6,Th6;
hence x = G*(i,j) by A12,TOPREAL3:6;
end;
assume x = G*(i,j);
then x in LSeg(G*(i,j),G*(i+1,j)) & x in LSeg(G*(i,j),G*(i,j+1)) by
RLTOPSP1:68;
hence x in LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i,j),G* (i,j+1)) by
XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th18:
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies LSeg(G*(
i,j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+1,j+1)) = { G*(i+1,j) }
proof
assume that
A1: 1 <= i and
A2: i+1 <= len G and
A3: 1 <= j and
A4: j+1 <= width G;
now
let x be object;
hereby
assume
A5: x in LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+1,j+1));
then reconsider p = x as Point of TOP-REAL 2;
A6: x in LSeg(G*(i,j),G*(i+1,j)) by A5,XBOOLE_0:def 4;
A7: p in LSeg(G*(i+1,j),G*(i+1,j+1)) by A5,XBOOLE_0:def 4;
A8: 1 <= j+1 & 1 <= i+1 by NAT_1:11;
j < j+1 by XREAL_1:29;
then
A9: j <= width G by A4,XXREAL_0:2;
A10: 1 <= i+1 by NAT_1:11;
then G*(i+1,j)`1 = G*(i+1,1)`1 by A2,A3,A9,GOBOARD5:2
.= G*(i+1,j+1)`1 by A2,A4,A8,GOBOARD5:2;
then
A11: p`1 = G*(i+1,j)`1 by A7,Th5;
i <= i+1 by NAT_1:11;
then i <= len G by A2,XXREAL_0:2;
then G*(i,j)`2 = G*(1,j)`2 by A1,A3,A9,GOBOARD5:1
.= G*(i+1,j)`2 by A2,A3,A10,A9,GOBOARD5:1;
then p`2 = G*(i+1,j)`2 by A6,Th6;
hence x = G*(i+1,j) by A11,TOPREAL3:6;
end;
assume x = G*(i+1,j);
then x in LSeg(G*(i,j),G*(i+1,j)) & x in LSeg(G*(i+1,j),G*(i+1,j+1)) by
RLTOPSP1:68;
hence x in LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+1,j+1)) by
XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th19:
for i1,j1,i2,j2 being Nat st 1 <= i1 & i1 <= len G &
1 <= j1 & j1+1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G &
LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1)) holds i1 = i2 &
|.j1-j2.| <= 1
proof
let i1,j1,i2,j2 be Nat such that
A1: 1 <= i1 & i1 <= len G and
A2: 1 <= j1 and
A3: j1+1 <= width G and
A4: 1 <= i2 & i2 <= len G and
A5: 1 <= j2 and
A6: j2+1 <= width G;
A7: 1 <= j1+1 by A2,NAT_1:13;
A8: j1 < width G by A3,NAT_1:13;
assume LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1));
then consider x being object such that
A9: x in LSeg(G*(i1,j1),G*(i1,j1+1)) and
A10: x in LSeg(G*(i2,j2),G*(i2,j2+1)) by XBOOLE_0:3;
reconsider p = x as Point of TOP-REAL 2 by A9;
consider r1 such that
A11: p = (1-r1)*(G*(i1,j1))+r1*(G*(i1,j1+1)) and
A12: r1 >= 0 and
A13: r1 <= 1 by A9;
consider r2 such that
A14: p = (1-r2)*(G*(i2,j2))+r2*(G*(i2,j2+1)) and
A15: r2 >= 0 and
A16: r2 <= 1 by A10;
A17: 1 <= j2+1 by A5,NAT_1:13;
A18: j2 < width G by A6,NAT_1:13;
assume
A19: not thesis;
per cases by A19;
suppose
i1 <> i2;
then
A20: i1 < i2 or i2 < i1 by XXREAL_0:1;
A21: G*(i2,j2)`1 = G*(i2,1)`1 by A4,A5,A18,GOBOARD5:2
.= G*(i2,j2+1)`1 by A4,A6,A17,GOBOARD5:2;
G*(i1,j1)`1 = G*(i1,1)`1 by A1,A2,A8,GOBOARD5:2
.= G*(i1,j1+1)`1 by A1,A3,A7,GOBOARD5:2;
then 1*(G*(i1,j1))`1 = (1-r1)*(G*(i1,j1))`1+r1*(G*(i1,j1+1))`1
.= ((1-r1)*(G*(i1,j1)))`1+r1*(G*(i1,j1+1))`1 by TOPREAL3:4
.= ((1-r1)*(G*(i1,j1)))`1+(r1*(G*(i1,j1+1)))`1 by TOPREAL3:4
.= p`1 by A11,TOPREAL3:2
.= ((1-r2)*(G*(i2,j2)))`1+(r2*(G*(i2,j2+1)))`1 by A14,TOPREAL3:2
.= (1-r2)*(G*(i2,j2))`1+(r2*(G*(i2,j2+1)))`1 by TOPREAL3:4
.= (1-r2)*(G*(i2,j2))`1+r2*(G*(i2,j2+1))`1 by TOPREAL3:4
.= G*(i2,1)`1 by A4,A6,A17,A21,GOBOARD5:2
.= G*(i2,j1)`1 by A2,A4,A8,GOBOARD5:2;
hence contradiction by A1,A2,A4,A8,A20,GOBOARD5:3;
end;
suppose
A22: |.j1-j2.| > 1;
A23: G*(i2,j2+1)`2 = G*(1,j2+1)`2 by A4,A6,A17,GOBOARD5:1
.= G*(i1,j2+1)`2 by A1,A6,A17,GOBOARD5:1;
A24: G*(i2,j2)`2 = G*(1,j2)`2 by A4,A5,A18,GOBOARD5:1
.= G*(i1,j2)`2 by A1,A5,A18,GOBOARD5:1;
A25: (1-r1)*(G*(i1,j1))`2+r1*(G*(i1,j1+1))`2 = ((1-r1)*(G*(i1,j1)))`2+r1*(
G*(i1,j1+1))`2 by TOPREAL3:4
.= ((1-r1)*(G*(i1,j1)))`2+(r1*(G*(i1,j1+1)))`2 by TOPREAL3:4
.= p`2 by A11,TOPREAL3:2
.= ((1-r2)*(G*(i2,j2)))`2+(r2*(G*(i2,j2+1)))`2 by A14,TOPREAL3:2
.= (1-r2)*(G*(i2,j2))`2+(r2*(G*(i2,j2+1)))`2 by TOPREAL3:4
.= (1-r2)*(G*(i1,j2))`2+r2*(G*(i1,j2+1))`2 by A23,A24,TOPREAL3:4;
now
per cases by A22,Th1;
suppose
A26: j1+1 < j2;
j2 < j2+1 by XREAL_1:29;
then G*(i1,j2)`2 < G*(i1,j2+1)`2 by A1,A5,A6,GOBOARD5:4;
then
(1-r2)*(G*(i1,j2))`2+r2*(G*(i1,j2))`2 = 1*(G*(i1,j2))`2 & r2*(G*(
i1,j2))`2 <= r2*(G*(i1,j2+1))`2 by A15,XREAL_1:64;
then
A27: G*(i1,j2)`2 <= (1-r2)*(G*(i1,j2))`2+r2*(G*(i1,j2+1))`2 by XREAL_1:6;
j1 < j1 + 1 by XREAL_1:29;
then
A28: G*(i1,j1)`2 <= G*(i1,j1+1)`2 by A1,A2,A3,GOBOARD5:4;
1-r1 >= 0 by A13,XREAL_1:48;
then
(1-r1)*(G*(i1,j1+1))`2+r1*(G*(i1,j1+1))`2 = 1*(G*(i1,j1+1))`2 & (
1-r1)*(G*( i1,j1))`2 <= (1-r1)*(G*(i1,j1+1))`2 by A28,XREAL_1:64;
then
A29: (1-r1)*(G*(i1,j1))`2+r1*(G*(i1,j1+1))`2 <= G*(i1,j1+1)`2 by XREAL_1:6;
G*(i1,j1+1)`2 < G*(i1,j2)`2 by A1,A7,A18,A26,GOBOARD5:4;
hence contradiction by A25,A29,A27,XXREAL_0:2;
end;
suppose
A30: j2+1 < j1;
j1 < j1+1 by XREAL_1:29;
then G*(i1,j1)`2 < G*(i1,j1+1)`2 by A1,A2,A3,GOBOARD5:4;
then
(1-r1)*(G*(i1,j1))`2+r1*(G*(i1,j1))`2 = 1*(G*(i1,j1))`2 & r1*(G*(
i1,j1))`2 <= r1*(G*(i1,j1+1))`2 by A12,XREAL_1:64;
then
A31: G*(i1,j1)`2 <= (1-r1)*(G*(i1,j1))`2+r1*(G* (i1,j1+1))`2 by XREAL_1:6;
j2 < j2 + 1 by XREAL_1:29;
then
A32: G*(i1,j2)`2 <= G*(i1,j2+1)`2 by A1,A5,A6,GOBOARD5:4;
1-r2 >= 0 by A16,XREAL_1:48;
then
(1-r2)*(G*(i1,j2+1))`2+r2*(G*(i1,j2+1))`2 = 1*(G*(i1,j2+1))`2 & (
1-r2)*(G*( i1,j2))`2 <= (1-r2)*(G*(i1,j2+1))`2 by A32,XREAL_1:64;
then
A33: (1-r2)*(G*(i1,j2))`2+r2*(G*(i1,j2+1))`2 <= G*(i1,j2+1)`2 by XREAL_1:6;
G*(i1,j2+1)`2 < G*(i1,j1)`2 by A1,A8,A17,A30,GOBOARD5:4;
hence contradiction by A25,A33,A31,XXREAL_0:2;
end;
end;
hence contradiction;
end;
end;
theorem Th20:
for i1,j1,i2,j2 being Nat st 1 <= i1 & i1+1 <= len G
& 1 <= j1 & j1 <= width G & 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
LSeg(G*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2+1,j2)) holds j1 = j2 &
|.i1-i2.| <= 1
proof
let i1,j1,i2,j2 be Nat such that
A1: 1 <= i1 and
A2: i1+1 <= len G and
A3: 1 <= j1 & j1 <= width G and
A4: 1 <= i2 and
A5: i2+1 <= len G and
A6: 1 <= j2 & j2 <= width G;
A7: 1 <= i1+1 by A1,NAT_1:13;
A8: i1 < len G by A2,NAT_1:13;
assume LSeg(G*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2+1,j2));
then consider x being object such that
A9: x in LSeg(G*(i1,j1),G*(i1+1,j1)) and
A10: x in LSeg(G*(i2,j2),G*(i2+1,j2)) by XBOOLE_0:3;
reconsider p = x as Point of TOP-REAL 2 by A9;
consider r1 such that
A11: p = (1-r1)*(G*(i1,j1))+r1*(G*(i1+1,j1)) and
A12: r1 >= 0 and
A13: r1 <= 1 by A9;
consider r2 such that
A14: p = (1-r2)*(G*(i2,j2))+r2*(G*(i2+1,j2)) and
A15: r2 >= 0 and
A16: r2 <= 1 by A10;
A17: 1 <= i2+1 by A4,NAT_1:13;
A18: i2 < len G by A5,NAT_1:13;
assume
A19: not thesis;
per cases by A19;
suppose
j1 <> j2;
then
A20: j1 < j2 or j2 < j1 by XXREAL_0:1;
A21: G*(i2,j2)`2 = G*(1,j2)`2 by A4,A6,A18,GOBOARD5:1
.= G*(i2+1,j2)`2 by A5,A6,A17,GOBOARD5:1;
G*(i1,j1)`2 = G*(1,j1)`2 by A1,A3,A8,GOBOARD5:1
.= G*(i1+1,j1)`2 by A2,A3,A7,GOBOARD5:1;
then 1*(G*(i1,j1))`2 = (1-r1)*(G*(i1,j1))`2+r1*(G*(i1+1,j1))`2
.= ((1-r1)*(G*(i1,j1)))`2+r1*(G*(i1+1,j1))`2 by TOPREAL3:4
.= ((1-r1)*(G*(i1,j1)))`2+(r1*(G*(i1+1,j1)))`2 by TOPREAL3:4
.= p`2 by A11,TOPREAL3:2
.= ((1-r2)*(G*(i2,j2)))`2+(r2*(G*(i2+1,j2)))`2 by A14,TOPREAL3:2
.= (1-r2)*(G*(i2,j2))`2+(r2*(G*(i2+1,j2)))`2 by TOPREAL3:4
.= (1-r2)*(G*(i2,j2))`2+r2*(G*(i2+1,j2))`2 by TOPREAL3:4
.= G*(1,j2)`2 by A5,A6,A17,A21,GOBOARD5:1
.= G*(i1,j2)`2 by A1,A6,A8,GOBOARD5:1;
hence contradiction by A1,A3,A6,A8,A20,GOBOARD5:4;
end;
suppose
A22: |.i1-i2.| > 1;
A23: G*(i2+1,j2)`1 = G*(i2+1,1)`1 by A5,A6,A17,GOBOARD5:2
.= G*(i2+1,j1)`1 by A3,A5,A17,GOBOARD5:2;
A24: G*(i2,j2)`1 = G*(i2,1)`1 by A4,A6,A18,GOBOARD5:2
.= G*(i2,j1)`1 by A3,A4,A18,GOBOARD5:2;
A25: (1-r1)*(G*(i1,j1))`1+r1*(G*(i1+1,j1))`1 = ((1-r1)*(G*(i1,j1)))`1+r1*(
G*(i1+1,j1))`1 by TOPREAL3:4
.= ((1-r1)*(G*(i1,j1)))`1+(r1*(G*(i1+1,j1)))`1 by TOPREAL3:4
.= p`1 by A11,TOPREAL3:2
.= ((1-r2)*(G*(i2,j2)))`1+(r2*(G*(i2+1,j2)))`1 by A14,TOPREAL3:2
.= (1-r2)*(G*(i2,j2))`1+(r2*(G*(i2+1,j2)))`1 by TOPREAL3:4
.= (1-r2)*(G*(i2,j1))`1+r2*(G*(i2+1,j1))`1 by A23,A24,TOPREAL3:4;
now
per cases by A22,Th1;
suppose
A26: i1+1 < i2;
i2 < i2+1 by XREAL_1:29;
then G*(i2,j1)`1 < G*(i2+1,j1)`1 by A3,A4,A5,GOBOARD5:3;
then
(1-r2)*(G*(i2,j1))`1+r2*(G*(i2,j1))`1 = 1*(G*(i2,j1))`1 & r2*(G*(
i2,j1))`1 <= r2*(G*(i2+1,j1))`1 by A15,XREAL_1:64;
then
A27: G*(i2,j1)`1 <= (1-r2)*(G*(i2,j1))`1+r2*(G* (i2+1,j1))`1 by XREAL_1:6;
i1 < i1 + 1 by XREAL_1:29;
then
A28: G*(i1,j1)`1 <= G*(i1+1,j1)`1 by A1,A2,A3,GOBOARD5:3;
1-r1 >= 0 by A13,XREAL_1:48;
then
(1-r1)*(G*(i1+1,j1))`1+r1*(G*(i1+1,j1))`1 = 1*(G*(i1+1,j1))`1 & (
1-r1)*(G*( i1,j1))`1 <= (1-r1)*(G*(i1+1,j1))`1 by A28,XREAL_1:64;
then
A29: (1-r1)*(G*(i1,j1))`1+r1*(G*(i1+1,j1))`1 <= G*(i1+1,j1)`1 by XREAL_1:6;
G*(i1+1,j1)`1 < G*(i2,j1)`1 by A3,A7,A18,A26,GOBOARD5:3;
hence contradiction by A25,A29,A27,XXREAL_0:2;
end;
suppose
A30: i2+1 < i1;
i1 < i1+1 by XREAL_1:29;
then G*(i1,j1)`1 < G*(i1+1,j1)`1 by A1,A2,A3,GOBOARD5:3;
then
(1-r1)*(G*(i1,j1))`1+r1*(G*(i1,j1))`1 = 1*(G*(i1,j1))`1 & r1*(G*(
i1,j1))`1 <= r1*(G*(i1+1,j1))`1 by A12,XREAL_1:64;
then
A31: G*(i1,j1)`1 <= (1-r1)*(G*(i1,j1))`1+r1*(G* (i1+1,j1))`1 by XREAL_1:6;
i2 < i2 + 1 by XREAL_1:29;
then
A32: G*(i2,j1)`1 <= G*(i2+1,j1)`1 by A3,A4,A5,GOBOARD5:3;
1-r2 >= 0 by A16,XREAL_1:48;
then
(1-r2)*(G*(i2+1,j1))`1+r2*(G*(i2+1,j1))`1 = 1*(G*(i2+1,j1))`1 & (
1-r2)*(G*( i2,j1))`1 <= (1-r2)*(G*(i2+1,j1))`1 by A32,XREAL_1:64;
then
A33: (1-r2)*(G*(i2,j1))`1+r2*(G*(i2+1,j1))`1 <= G*(i2+1,j1)`1 by XREAL_1:6;
G*(i2+1,j1)`1 < G*(i1,j1)`1 by A3,A8,A17,A30,GOBOARD5:3;
hence contradiction by A25,A33,A31,XXREAL_0:2;
end;
end;
hence contradiction;
end;
end;
theorem Th21:
for i1,j1,i2,j2 being Nat st 1 <= i1 & i1 <= len G &
1 <= j1 & j1+1 <= width G & 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2+1,j2)) holds (i1 = i2 or
i1 = i2+1) & (j1 = j2 or j1+1 = j2)
proof
let i1,j1,i2,j2 be Nat such that
A1: 1 <= i1 and
A2: i1 <= len G and
A3: 1 <= j1 and
A4: j1+1 <= width G and
A5: 1 <= i2 and
A6: i2+1 <= len G and
A7: 1 <= j2 and
A8: j2 <= width G;
assume LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2+1,j2));
then consider x being object such that
A9: x in LSeg(G*(i1,j1),G*(i1,j1+1)) and
A10: x in LSeg(G*(i2,j2),G*(i2+1,j2)) by XBOOLE_0:3;
reconsider p = x as Point of TOP-REAL 2 by A9;
consider r1 such that
A11: p = (1-r1)*(G*(i1,j1))+r1*(G*(i1,j1+1)) and
A12: r1 >= 0 and
A13: r1 <= 1 by A9;
consider r2 such that
A14: p = (1-r2)*(G*(i2,j2))+r2*(G*(i2+1,j2)) and
A15: r2 >= 0 and
A16: r2 <= 1 by A10;
A17: i2 < len G by A6,NAT_1:13;
A18: 1 <= j1+1 by A3,NAT_1:13;
then
A19: G*(i1,j1+1)`2 = G*(1,j1+1)`2 by A1,A2,A4,GOBOARD5:1
.= G*(i2,j1+1)`2 by A4,A5,A18,A17,GOBOARD5:1;
A20: j1 < width G by A4,NAT_1:13;
then
A21: G*(i1,j1)`2 = G*(1,j1)`2 by A1,A2,A3,GOBOARD5:1
.= G*(i2,j1)`2 by A3,A5,A20,A17,GOBOARD5:1;
A22: (1-r2)*(G*(i2,j2))`2+r2*(G*(i2+1,j2))`2 = ((1-r2)*(G*(i2,j2)))`2+r2*(G*
(i2+1,j2))`2 by TOPREAL3:4
.= ((1-r2)*(G*(i2,j2)))`2+(r2*(G*(i2+1,j2)))`2 by TOPREAL3:4
.= p`2 by A14,TOPREAL3:2
.= ((1-r1)*(G*(i1,j1)))`2+(r1*(G*(i1,j1+1)))`2 by A11,TOPREAL3:2
.= (1-r1)*(G*(i1,j1))`2+(r1*(G*(i1,j1+1)))`2 by TOPREAL3:4
.= (1-r1)*(G*(i2,j1))`2+r1*(G*(i2,j1+1))`2 by A19,A21,TOPREAL3:4;
A23: 1 <= i2+1 by A5,NAT_1:13;
thus i1 = i2 or i1 = i2+1
proof
A24: G*(i2,j2)`1 = G*(i2,1)`1 by A5,A7,A8,A17,GOBOARD5:2
.= G*(i2,j1)`1 by A3,A5,A20,A17,GOBOARD5:2;
A25: G*(i2+1,j2)`1 = G*(i2+1,1)`1 by A6,A7,A8,A23,GOBOARD5:2
.= G*(i2+1,j1)`1 by A3,A6,A20,A23,GOBOARD5:2;
A26: (1-r1)*(G*(i1,j1))`1+r1*(G*(i1,j1+1))`1 = ((1-r1)*(G*(i1,j1)))`1+r1*(
G*(i1,j1+1))`1 by TOPREAL3:4
.= ((1-r1)*(G*(i1,j1)))`1+(r1*(G*(i1,j1+1)))`1 by TOPREAL3:4
.= p`1 by A11,TOPREAL3:2
.= ((1-r2)*(G*(i2,j2)))`1+(r2*(G*(i2+1,j2)))`1 by A14,TOPREAL3:2
.= (1-r2)*(G*(i2,j2))`1+(r2*(G*(i2+1,j2)))`1 by TOPREAL3:4
.= (1-r2)*(G*(i2,j1))`1+r2*(G*(i2+1,j1))`1 by A25,A24,TOPREAL3:4;
A27: G*(i1,j1)`1 = G*(i1,1)`1 by A1,A2,A3,A20,GOBOARD5:2
.= G*(i1,j1+1)`1 by A1,A2,A4,A18,GOBOARD5:2;
assume
A28: not thesis;
per cases by A28,XXREAL_0:1;
suppose
A29: i1 < i2 & i1 < i2+1;
i2 < i2+1 by XREAL_1:29;
then G*(i2,j1)`1 < G*(i2+1,j1)`1 by A3,A5,A6,A20,GOBOARD5:3;
then
A30: (1-r2)*(G*(i2,j1))`1+r2*(G*(i2,j1))`1 = 1*(G*(i2,j1))`1 & r2*(G*(i2
,j1))`1 <= r2*(G*(i2+1,j1))`1 by A15,XREAL_1:64;
G*(i1,j1)`1 < G*(i2,j1)`1 by A1,A3,A20,A17,A29,GOBOARD5:3;
hence contradiction by A26,A27,A30,XREAL_1:6;
end;
suppose
i1 < i2 & i2+1 < i1;
hence thesis by NAT_1:13;
end;
suppose
i2 < i1 & i1 < i2+1;
hence thesis by NAT_1:13;
end;
suppose
A31: i2+1 < i1;
i2 < i2 + 1 by XREAL_1:29;
then
A32: G*(i2,j1)`1 <= G*(i2+1,j1)`1 by A3,A5,A6,A20,GOBOARD5:3;
1-r2 >= 0 by A16,XREAL_1:48;
then
(1-r2)*(G*(i2+1,j1))`1+r2*(G*(i2+1,j1))`1 = 1*(G*(i2+1,j1))`1 & (1-
r2)*(G*( i2,j1))`1 <= (1-r2)*(G*(i2+1,j1))`1 by A32,XREAL_1:64;
then (1-r2)*(G*(i2,j1))`1+r2*(G*(i2+1,j1))`1 <= G*(i2+1,j1)`1 by
XREAL_1:6;
hence contradiction by A2,A3,A20,A23,A26,A27,A31,GOBOARD5:3;
end;
end;
A33: G*(i2,j2)`2 = G*(1,j2)`2 by A5,A7,A8,A17,GOBOARD5:1
.= G*(i2+1,j2)`2 by A6,A7,A8,A23,GOBOARD5:1;
assume
A34: not thesis;
per cases by A34,XXREAL_0:1;
suppose
A35: j2 < j1 & j2 < j1+1;
j1 < j1+1 by XREAL_1:29;
then G*(i2,j1)`2 < G*(i2,j1+1)`2 by A3,A4,A5,A17,GOBOARD5:4;
then
A36: (1-r1)*(G*(i2,j1))`2+r1*(G*(i2,j1))`2 = 1*(G*(i2,j1))`2 & r1*(G*(i2,
j1))`2 <= r1*(G*(i2,j1+1))`2 by A12,XREAL_1:64;
G*(i2,j2)`2 < G*(i2,j1)`2 by A5,A7,A20,A17,A35,GOBOARD5:4;
hence contradiction by A22,A33,A36,XREAL_1:6;
end;
suppose
j2 < j1 & j1+1 < j2;
hence thesis by NAT_1:13;
end;
suppose
j1 < j2 & j2 < j1+1;
hence thesis by NAT_1:13;
end;
suppose
A37: j1+1 < j2;
j1 < j1 + 1 by XREAL_1:29;
then
A38: G*(i2,j1)`2 <= G*(i2,j1+1)`2 by A3,A4,A5,A17,GOBOARD5:4;
1-r1 >= 0 by A13,XREAL_1:48;
then
(1-r1)*(G*(i2,j1+1))`2+r1*(G*(i2,j1+1))`2 = 1*(G*(i2,j1+1))`2 & (1-r1
)*(G*( i2,j1))`2 <= (1-r1)*(G*(i2,j1+1))`2 by A38,XREAL_1:64;
then (1-r1)*(G*(i2,j1))`2+r1*(G*(i2,j1+1))`2 <= G* (i2,j1+1)`2 by XREAL_1:6
;
hence contradiction by A5,A8,A18,A17,A22,A33,A37,GOBOARD5:4;
end;
end;
theorem
for i1,j1,i2,j2 being Nat st 1 <= i1 & i1 <= len G & 1 <=
j1 & j1+1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G & LSeg
(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1)) holds j1 = j2 & LSeg(
G*(i1,j1),G*(i1,j1+1)) = LSeg(G*(i2,j2),G*(i2,j2+1)) or j1 = j2+1 & LSeg(G*(i1,
j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2,j2+1)) = { G* (i1,j1) } or j1+1 = j2 &
LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2,j2+1)) = { G* (i2,j2) }
proof
let i1,j1,i2,j2 be Nat such that
A1: 1 <= i1 & i1 <= len G and
A2: 1 <= j1 and
A3: j1+1 <= width G and
A4: 1 <= i2 & i2 <= len G and
A5: 1 <= j2 and
A6: j2+1 <= width G and
A7: LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1));
A8: i1 = i2 by A1,A2,A3,A4,A5,A6,A7,Th19;
A9: j1+1+1 = j1+(1+1);
A10: j2+1+1 = j2+(1+1);
A11: |.j1-j2.| = 0 or |.j1-j2.| = 1 by A1,A2,A3,A4,A5,A6,A7,Th19,NAT_1:25;
per cases by A11,Th2,SEQM_3:41;
case
j1 = j2;
hence thesis by A8;
end;
case
j1 = j2+1;
hence thesis by A1,A3,A5,A8,A10,Th13;
end;
case
j1+1 = j2;
hence thesis by A1,A2,A6,A8,A9,Th13;
end;
end;
theorem
for i1,j1,i2,j2 being Nat st 1 <= i1 & i1+1 <= len G & 1 <=
j1 & j1 <= width G & 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G & LSeg(G
*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2+1,j2)) holds i1 = i2 & LSeg(G*
(i1,j1),G*(i1+1,j1)) = LSeg(G*(i2,j2),G*(i2+1,j2)) or i1 = i2+1 & LSeg(G*(i1,j1
),G*(i1+1,j1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G* (i1,j1) } or i1+1 = i2 &
LSeg(G*(i1,j1),G*(i1+1,j1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G* (i2,j2) }
proof
let i1,j1,i2,j2 be Nat such that
A1: 1 <= i1 and
A2: i1+1 <= len G and
A3: 1 <= j1 & j1 <= width G and
A4: 1 <= i2 and
A5: i2+1 <= len G and
A6: 1 <= j2 & j2 <= width G & LSeg(G*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(
i2, j2),G*(i2+1,j2));
A7: j1 = j2 by A1,A2,A3,A4,A5,A6,Th20;
A8: i1+1+1 = i1+(1+1);
A9: i2+1+1 = i2+(1+1);
A10: |.i1-i2.| = 0 or |.i1-i2.| = 1 by A1,A2,A3,A4,A5,A6,Th20,NAT_1:25;
per cases by A10,Th2,SEQM_3:41;
case
i1 = i2;
hence thesis by A7;
end;
case
i1 = i2+1;
hence thesis by A2,A3,A4,A7,A9,Th14;
end;
case
i1+1 = i2;
hence thesis by A1,A3,A5,A7,A8,Th14;
end;
end;
theorem
for i1,j1,i2,j2 being Nat st 1 <= i1 & i1 <= len G & 1 <=
j1 & j1+1 <= width G & 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G & LSeg
(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2+1,j2)) holds j1 = j2 & LSeg(
G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G* (i1,j1) } or j1+1
= j2 & LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G* (i1,j1
+1) }
proof
let i1,j1,i2,j2 be Nat such that
A1: 1 <= i1 & i1 <= len G and
A2: 1 <= j1 & j1+1 <= width G & 1 <= i2 & i2+1 <= len G and
A3: 1 <= j2 & j2 <= width G & LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(
i2, j2),G*(i2+1,j2));
per cases by A1,A2,A3,Th21;
case
A4: j1 = j2;
now
per cases by A1,A2,A3,Th21;
suppose
i1 = i2;
hence thesis by A2,A4,Th17;
end;
suppose
i1 = i2+1;
hence thesis by A2,A4,Th18;
end;
end;
hence thesis;
end;
case
A5: j1+1 = j2;
now
per cases by A1,A2,A3,Th21;
suppose
i1 = i2;
hence thesis by A2,A5,Th15;
end;
suppose
i1 = i2+1;
hence thesis by A2,A5,Th16;
end;
end;
hence thesis;
end;
end;
Lm1: 1 - 1/2 = 1/2;
theorem Th25:
1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G & 1 <= i2 & i2
<= len G & 1 <= j2 & j2+1 <= width G & 1/2*(G*(i1,j1)+G*(i1,j1+1)) in LSeg(G*(
i2,j2),G*(i2,j2+1)) implies i1 = i2 & j1 = j2
proof
assume that
A1: 1 <= i1 & i1 <= len G and
A2: 1 <= j1 and
A3: j1+1 <= width G and
A4: 1 <= i2 & i2 <= len G and
A5: 1 <= j2 and
A6: j2+1 <= width G;
set mi = 1/2*(G*(i1,j1)+G*(i1,j1+1));
A7: 1/2*(G*(i1,j1))+1/2*(G*(i1,j1+1)) = 1/2*(G*(i1,j1)+G*(i1,j1+1)) by
RLVECT_1:def 5;
then
A8: mi in LSeg(G*(i1,j1),G*(i1,j1+1)) by Lm1;
assume
A9: mi in LSeg(G*(i2,j2),G*(i2,j2+1));
then
A10: LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1)) by A8,
XBOOLE_0:3;
hence
A11: i1 = i2 by A1,A2,A3,A4,A5,A6,Th19;
now
j1 < j1+1 by XREAL_1:29;
then
A12: G*(i1,j1+1)`2 > G*(i1,j1)`2 by A1,A2,A3,GOBOARD5:4;
assume
A13: |.j1-j2.| = 1;
per cases by A13,SEQM_3:41;
suppose
A14: j1 = j2+1;
then
LSeg(G*(i2,j2),G*(i2,j2+1)) /\ LSeg(G*(i2,j2+1),G*(i2,j2+2)) = { G*
(i2,j2+1) } by A3,A4,A5,Th13;
then mi in { G*(i1,j1) } by A9,A8,A11,A14,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1,j1+1)) = G*(i1,j1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1,j1)) by RLVECT_1:def 8
.= 1/2*(G*(i1,j1))+1/2*(G*(i1,j1)) by RLVECT_1:def 6;
then 1/2*(G*(i1,j1)) = 1/2*(G*(i1,j1+1)) by Th3;
hence contradiction by A12,RLVECT_1:36;
end;
suppose
A15: j1+1 = j2;
then
LSeg(G*(i2,j1),G*(i2,j1+1)) /\ LSeg(G*(i2,j1+1),G*(i2,j1+2)) = { G*
(i2,j1+1) } by A2,A4,A6,Th13;
then mi in { G*(i1,j2) } by A9,A8,A11,A15,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1,j1+1)) = G*(i1,j2) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1,j2)) by RLVECT_1:def 8
.= 1/2*(G*(i1,j2))+1/2*(G*(i1,j2)) by RLVECT_1:def 6;
then 1/2*(G*(i1,j1)) = 1/2*(G*(i1,j1+1)) by A15,Th3;
hence contradiction by A12,RLVECT_1:36;
end;
end;
then |.j1-j2.| = 0 by A1,A2,A3,A4,A5,A6,A10,Th19,NAT_1:25;
hence thesis by Th2;
end;
theorem Th26:
1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2
+1 <= len G & 1 <= j2 & j2 <= width G & 1/2*(G*(i1,j1)+G*(i1+1,j1)) in LSeg(G*(
i2,j2),G*(i2+1,j2)) implies i1 = i2 & j1 = j2
proof
assume that
A1: 1 <= i1 and
A2: i1+1 <= len G and
A3: 1 <= j1 & j1 <= width G and
A4: 1 <= i2 and
A5: i2+1 <= len G and
A6: 1 <= j2 & j2 <= width G;
set mi = 1/2*(G*(i1,j1)+G*(i1+1,j1));
A7: 1/2*(G*(i1,j1))+1/2*(G*(i1+1,j1)) = 1/2*(G*(i1,j1)+G*(i1+1,j1)) by
RLVECT_1:def 5;
then
A8: mi in LSeg(G*(i1,j1),G*(i1+1,j1)) by Lm1;
assume
A9: mi in LSeg(G*(i2,j2),G*(i2+1,j2));
then
A10: LSeg(G*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2+1,j2)) by A8,
XBOOLE_0:3;
then
A11: j1 = j2 by A1,A2,A3,A4,A5,A6,Th20;
now
i1 < i1+1 by XREAL_1:29;
then
A12: G*(i1+1,j1)`1 > G*(i1,j1)`1 by A1,A2,A3,GOBOARD5:3;
assume
A13: |.i1-i2.| = 1;
per cases by A13,SEQM_3:41;
suppose
A14: i1 = i2+1;
then
LSeg(G*(i2,j2),G*(i2+1,j2)) /\ LSeg(G*(i2+1,j2),G*(i2+2,j2)) = { G*
(i2+1,j2) } by A2,A4,A6,Th14;
then mi in { G*(i1,j1) } by A9,A8,A11,A14,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1+1,j1)) = G*(i1,j1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1,j1)) by RLVECT_1:def 8
.= 1/2*(G*(i1,j1))+1/2*(G*(i1,j1)) by RLVECT_1:def 6;
then 1/2*(G*(i1,j1)) = 1/2*(G*(i1+1,j1)) by Th3;
hence contradiction by A12,RLVECT_1:36;
end;
suppose
A15: i1+1 = i2;
then
LSeg(G*(i1,j2),G*(i1+1,j2)) /\ LSeg(G*(i1+1,j2),G*(i1+2,j2)) = { G*
(i1+1,j2) } by A1,A5,A6,Th14;
then mi in { G*(i2,j1) } by A9,A8,A11,A15,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1+1,j1)) = G*(i2,j1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i2,j1)) by RLVECT_1:def 8
.= 1/2*(G*(i2,j1))+1/2*(G*(i2,j1)) by RLVECT_1:def 6;
then 1/2*(G*(i1,j1)) = 1/2*(G*(i1+1,j1)) by A15,Th3;
hence contradiction by A12,RLVECT_1:36;
end;
end;
then |.i1-i2.| = 0 by A1,A2,A3,A4,A5,A6,A10,Th20,NAT_1:25;
hence i1 = i2 by Th2;
thus thesis by A1,A2,A3,A4,A5,A6,A10,Th20;
end;
theorem Th27:
1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G implies not ex
i2,j2 st 1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G & 1/2*(G*(i1,j1)+G*(
i1+1,j1)) in LSeg(G*(i2,j2),G*(i2,j2+1))
proof
assume that
A1: 1 <= i1 & i1+1 <= len G and
A2: 1 <= j1 & j1 <= width G;
A3: i1 < i1+1 by XREAL_1:29;
set mi = 1/2*(G*(i1,j1)+G*(i1+1,j1));
given i2,j2 such that
A4: 1 <= i2 & i2 <= len G and
A5: 1 <= j2 & j2+1 <= width G and
A6: mi in LSeg(G*(i2,j2),G*(i2,j2+1));
A7: 1/2*(G*(i1,j1))+1/2*(G*(i1+1,j1)) = 1/2*(G*(i1,j1)+G*(i1+1,j1)) by
RLVECT_1:def 5;
then
A8: mi in LSeg(G*(i1,j1),G*(i1+1,j1)) by Lm1;
then
A9: LSeg(G*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2,j2+1)) by A6,
XBOOLE_0:3;
per cases by A1,A2,A4,A5,A9,Th21;
suppose
A10: j1 = j2 & i1 = i2;
then
LSeg(G*(i1,j1),G*(i1+1,j1)) /\ LSeg(G*(i1,j1+1),G*(i1,j1)) = { G*(i1,
j1) } by A1,A5,Th17;
then mi in { G*(i1,j1) } by A6,A8,A10,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1+1,j1)) = G*(i1,j1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1,j1)) by RLVECT_1:def 8
.= 1/2*(G*(i1,j1))+1/2*(G*(i1,j1)) by RLVECT_1:def 6;
then
A11: 1/2*(G*(i1+1,j1)) = 1/2*(G*(i1,j1)) by Th3;
G*(i1+1,j1)`1 > G*(i1,j1)`1 by A1,A2,A3,GOBOARD5:3;
hence contradiction by A11,RLVECT_1:36;
end;
suppose
A12: j1 = j2 & i1+1 = i2;
then
LSeg(G*(i1,j1),G*(i1+1,j1)) /\ LSeg(G*(i1+1,j1+1),G*(i1+1,j1)) = { G*
(i1+1,j1) } by A1,A5,Th18;
then mi in { G*(i1+1,j1) } by A6,A8,A12,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1+1,j1)) = G*(i1+1,j1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1+1,j1)) by RLVECT_1:def 8
.= 1/2*(G*(i1+1,j1))+1/2*(G*(i1+1,j1)) by RLVECT_1:def 6;
then
A13: 1/2*(G*(i1+1,j1)) = 1/2*(G*(i1,j1)) by Th3;
G*(i1+1,j1)`1 > G*(i1,j1)`1 by A1,A2,A3,GOBOARD5:3;
hence contradiction by A13,RLVECT_1:36;
end;
suppose
A14: j1 = j2+1 & i1 = i2;
then
LSeg(G*(i1,j1),G*(i1+1,j1)) /\ LSeg(G*(i1,j1),G*(i1,j2)) = { G*(i1,j1
) } by A1,A5,Th15;
then mi in { G*(i1,j1) } by A6,A8,A14,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1+1,j1)) = G*(i1,j1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1,j1)) by RLVECT_1:def 8
.= 1/2*(G*(i1,j1))+1/2*(G*(i1,j1)) by RLVECT_1:def 6;
then
A15: 1/2*(G*(i1+1,j1)) = 1/2*(G*(i1,j1)) by Th3;
G*(i1+1,j1)`1 > G*(i1,j1)`1 by A1,A2,A3,GOBOARD5:3;
hence contradiction by A15,RLVECT_1:36;
end;
suppose
A16: j1 = j2+1 & i1+1 = i2;
then LSeg(G*(i1,j1),G*(i1+1,j1)) /\ LSeg(G*(i1+1,j1),G*(i1+1,j2)) = { G*(
i1+1,j1) } by A1,A5,Th16;
then mi in { G*(i1+1,j1) } by A6,A8,A16,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1+1,j1)) = G*(i1+1,j1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1+1,j1)) by RLVECT_1:def 8
.= 1/2*(G*(i1+1,j1))+1/2*(G*(i1+1,j1)) by RLVECT_1:def 6;
then
A17: 1/2*(G*(i1+1,j1)) = 1/2*(G*(i1,j1)) by Th3;
G*(i1+1,j1)`1 > G*(i1,j1)`1 by A1,A2,A3,GOBOARD5:3;
hence contradiction by A17,RLVECT_1:36;
end;
end;
theorem Th28:
1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G implies not ex
i2,j2 st 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G & 1/2*(G*(i1,j1)+G*(
i1,j1+1)) in LSeg(G*(i2,j2),G*(i2+1,j2))
proof
assume that
A1: 1 <= i1 & i1 <= len G and
A2: 1 <= j1 & j1+1 <= width G;
A3: j1 < j1+1 by XREAL_1:29;
set mi = 1/2*(G*(i1,j1)+G*(i1,j1+1));
given i2,j2 such that
A4: 1 <= i2 & i2+1 <= len G and
A5: 1 <= j2 & j2 <= width G and
A6: mi in LSeg(G*(i2,j2),G*(i2+1,j2));
A7: 1/2*(G*(i1,j1))+1/2*(G*(i1,j1+1)) = 1/2*(G*(i1,j1)+G*(i1,j1+1)) by
RLVECT_1:def 5;
then
A8: mi in LSeg(G*(i1,j1),G*(i1,j1+1)) by Lm1;
then
A9: LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2+1,j2)) by A6,
XBOOLE_0:3;
per cases by A1,A2,A4,A5,A9,Th21;
suppose
A10: i1 = i2 & j1 = j2;
then
LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i1+1,j1),G*(i1,j1)) = { G*(i1,
j1) } by A2,A4,Th17;
then mi in { G*(i1,j1) } by A6,A8,A10,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1,j1+1)) = G*(i1,j1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1,j1)) by RLVECT_1:def 8
.= 1/2*(G*(i1,j1))+1/2*(G*(i1,j1)) by RLVECT_1:def 6;
then
A11: 1/2*(G*(i1,j1+1)) = 1/2*(G*(i1,j1)) by Th3;
G*(i1,j1+1)`2 > G*(i1,j1)`2 by A1,A2,A3,GOBOARD5:4;
hence contradiction by A11,RLVECT_1:36;
end;
suppose
A12: i1 = i2 & j1+1 = j2;
then
LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i1+1,j1+1),G*(i1,j1+1)) = { G*
(i1,j1+1) } by A2,A4,Th15;
then mi in { G*(i1,j1+1) } by A6,A8,A12,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1,j1+1)) = G*(i1,j1+1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1,j1+1)) by RLVECT_1:def 8
.= 1/2*(G*(i1,j1+1))+1/2*(G*(i1,j1+1)) by RLVECT_1:def 6;
then
A13: 1/2*(G*(i1,j1+1)) = 1/2*(G*(i1,j1)) by Th3;
G*(i1,j1+1)`2 > G*(i1,j1)`2 by A1,A2,A3,GOBOARD5:4;
hence contradiction by A13,RLVECT_1:36;
end;
suppose
A14: i1 = i2+1 & j1 = j2;
then
LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i1,j1),G*(i2,j1)) = { G*(i1,j1
) } by A2,A4,Th18;
then mi in { G*(i1,j1) } by A6,A8,A14,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1,j1+1)) = G*(i1,j1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1,j1)) by RLVECT_1:def 8
.= 1/2*(G*(i1,j1))+1/2*(G*(i1,j1)) by RLVECT_1:def 6;
then
A15: 1/2*(G*(i1,j1+1)) = 1/2*(G*(i1,j1)) by Th3;
G*(i1,j1+1)`2 > G*(i1,j1)`2 by A1,A2,A3,GOBOARD5:4;
hence contradiction by A15,RLVECT_1:36;
end;
suppose
A16: i1 = i2+1 & j1+1 = j2;
then LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i1,j1+1),G*(i2,j1+1)) = { G*(
i1,j1+1) } by A2,A4,Th16;
then mi in { G*(i1,j1+1) } by A6,A8,A16,XBOOLE_0:def 4;
then 1/2*(G*(i1,j1))+1/2*(G*(i1,j1+1)) = G*(i1,j1+1) by A7,TARSKI:def 1
.= (1/2+1/2)*(G*(i1,j1+1)) by RLVECT_1:def 8
.= 1/2*(G*(i1,j1+1))+1/2*(G*(i1,j1+1)) by RLVECT_1:def 6;
then
A17: 1/2*(G*(i1,j1+1)) = 1/2*(G*(i1,j1)) by Th3;
G*(i1,j1+1)`2 > G*(i1,j1)`2 by A1,A2,A3,GOBOARD5:4;
hence contradiction by A17,RLVECT_1:36;
end;
end;
begin :: Standard special circular sequences
reserve f for non constant standard special_circular_sequence;
Lm2: len f > 1
proof
consider n1,n2 being object such that
A1: n1 in dom f and
A2: n2 in dom f & f.n1 <> f.n2 by FUNCT_1:def 10;
reconsider df = dom f as finite set;
A3: now
assume
A4: card df <= 1;
per cases by A4,NAT_1:25;
suppose
card df = 0;
hence contradiction by A1;
end;
suppose
card df = 1;
then consider x being object such that
A5: dom f = {x} by CARD_2:42;
n1 = x by A1,A5,TARSKI:def 1;
hence contradiction by A2,A5,TARSKI:def 1;
end;
end;
dom f = Seg len f by FINSEQ_1:def 3;
hence thesis by A3,FINSEQ_1:57;
end;
theorem Th29:
for f being standard non empty FinSequence of TOP-REAL 2 st i
in dom f & i+1 in dom f holds f/.i <> f/.(i+1)
proof
A1: |.0 .| = 0 by ABSVALUE:2;
let f be standard non empty FinSequence of TOP-REAL 2 such that
A2: i in dom f and
A3: i+1 in dom f;
A4: f is_sequence_on GoB f by GOBOARD5:def 5;
then consider i1,j1 such that
A5: [i1,j1] in Indices GoB f & f/.i = (GoB f)*(i1,j1) by A2,GOBOARD1:def 9;
consider i2,j2 such that
A6: [i2,j2] in Indices GoB f and
A7: f/.(i+1) = (GoB f)*(i2,j2) by A3,A4,GOBOARD1:def 9;
assume
A8: f/.i = f/.(i+1);
then j1 = j2 by A5,A6,A7,GOBOARD1:5;
then
A9: j1-j2 = 0;
i1 = i2 by A5,A6,A7,A8,GOBOARD1:5;
then i1-i2 = 0;
then |.0 .|+|.0 .| = 1 by A2,A3,A4,A5,A7,A9,GOBOARD1:def 9;
hence contradiction by A1;
end;
theorem Th30:
ex i st i in dom f & (f/.i)`1 <> (f/.1)`1
proof
assume
A1: for i st i in dom f holds (f/.i)`1 = (f/.1)`1;
A2: len f > 1 by Lm2;
then
A3: len f >= 1+1 by NAT_1:13;
then
A4: 1+1 in dom f by FINSEQ_3:25;
A5: now
assume
A6: (f/.2)`2 = (f/.1)`2;
(f/.2)`1 = (f/.1)`1 by A1,A4;
then f/.2 = |[(f/.1)`1,(f/.1)`2]| by A6,EUCLID:53
.= f/.1 by EUCLID:53;
hence contradiction by A4,Th29,FINSEQ_5:6;
end;
len f = 2 implies f/.2 = f/.1 by FINSEQ_6:def 1;
then
A7: 2 < len f by A3,A5,XXREAL_0:1;
per cases by A5,XXREAL_0:1;
suppose
A8: (f/.2)`2 < (f/.1)`2;
defpred P[Nat] means
2 <= $1 & $1 < len f implies (f/.$1)`2 <=
(f/.2)`2 & (f/.($1+1))`2 < (f/.$1)`2;
A9: for j st P[j] holds P[j+1]
proof
let j such that
A10: 2 <= j & j < len f implies (f/.j)`2 <= (f/.2)`2 & (f/.(j+1))`2
< (f/.j)`2 and
A11: 2 <= j+1 and
A12: j+1 < len f;
1+1 <= j+1 by A11;
then
A13: 1 <= j by XREAL_1:6;
thus (f/.(j+1))`2 <= (f/.2)`2
proof
per cases by A11,XXREAL_0:1;
suppose
2 = j+1;
hence thesis;
end;
suppose
2 < j+1;
hence thesis by A10,A12,NAT_1:13,XXREAL_0:2;
end;
end;
A14: j+1+1 <= len f by A12,NAT_1:13;
A15: now
per cases by A11,XXREAL_0:1;
suppose
1+1 = j+1;
hence (f/.(j+1))`2 < (f/.j)`2 by A8;
end;
suppose
2 < j+1;
hence (f/.(j+1))`2 < (f/.j)`2 by A10,A12,NAT_1:13;
end;
end;
A16: 1 <= j+1 by NAT_1:11;
then
A17: j+1 in dom f by A12,FINSEQ_3:25;
then
A18: (f/.(j+1))`1 = (f/.1)`1 by A1;
j < len f by A12,NAT_1:13;
then
A19: j in dom f by A13,FINSEQ_3:25;
then
A20: (f/.j)`1 = (f/.1)`1 by A1;
1 <= j+1+1 by NAT_1:11;
then
A21: j+1+1 in dom f by A14,FINSEQ_3:25;
then
A22: (f/.(j+1+1))`1 = (f/.1)`1 by A1;
assume
A23: (f/.(j+1+1))`2 >= (f/.(j+1))`2;
per cases by A23,XXREAL_0:1;
suppose
A24: (f/.(j+1+1))`2 > (f/.(j+1))`2;
now
per cases;
suppose
(f/.j)`2 <= (f/.(j+1+1))`2;
then f/.j in LSeg(f/.(j+1),f/.(j+1+1)) by A15,A20,A18,A22,Th7;
then
A25: f/.j in LSeg(f,j+1) by A14,A16,TOPREAL1:def 3;
j+1+1 = j+(1+1);
then
A26: LSeg(f,j) /\ LSeg(f,j+1) = {f/.(j+1)} by A14,A13,TOPREAL1:def 6;
f/.j in LSeg(f,j) by A12,A13,TOPREAL1:21;
then f/.j in LSeg(f,j) /\ LSeg(f,j+1) by A25,XBOOLE_0:def 4;
then f/.j = f/.(j+1) by A26,TARSKI:def 1;
hence contradiction by A19,A17,Th29;
end;
suppose
(f/.j)`2 >= (f/.(j+1+1))`2;
then f/.(j+1+1) in LSeg(f/.j,f/.(j+1)) by A20,A18,A22,A24,Th7;
then
A27: f/.(j+1+1) in LSeg(f,j) by A12,A13,TOPREAL1:def 3;
j+1+1 = j+(1+1);
then
A28: LSeg(f,j) /\ LSeg(f,j+1) = {f/.(j+1)} by A14,A13,TOPREAL1:def 6;
f/.(j+1+1) in LSeg(f,j+1) by A14,A16,TOPREAL1:21;
then f/.(j+1+1) in LSeg(f,j) /\ LSeg(f,j+1) by A27,XBOOLE_0:def 4;
then f/.(j+1+1) = f/.(j+1) by A28,TARSKI:def 1;
hence contradiction by A17,A21,Th29;
end;
end;
hence contradiction;
end;
suppose
A29: (f/.(j+1+1))`2 = (f/.(j+1))`2;
(f/.(j+1+1))`1 = (f/.1)`1 by A1,A21
.= (f/.(j+1))`1 by A1,A17;
then f/.(j+1+1) = |[(f/.(j+1))`1,(f/.(j+1))`2]| by A29,EUCLID:53
.= f/.(j+1) by EUCLID:53;
hence contradiction by A17,A21,Th29;
end;
end;
A30: len f -'1+1 = len f by A2,XREAL_1:235;
then
A31: 2 <= len f -'1 & len f-'1 < len f by A7,NAT_1:13;
A32: P[0];
A33: for j holds P[j] from NAT_1:sch 2(A32,A9);
then
A34: (f/.(len f-'1))`2 <= (f/.2)`2 by A31;
(f/.len f)`2 < (f/.(len f -'1))`2 by A33,A30,A31;
then (f/.len f)`2 < (f/.2)`2 by A34,XXREAL_0:2;
hence contradiction by A8,FINSEQ_6:def 1;
end;
suppose
A35: (f/.2)`2 > (f/.1)`2;
defpred P[Nat] means
2 <= $1 & $1 < len f implies (f/.$1)`2 >=
(f/.2)`2 & (f/.($1+1))`2 > (f/.$1)`2;
A36: for j st P[j] holds P[j+1]
proof
let j such that
A37: 2 <= j & j < len f implies (f/.j)`2 >= (f/.2)`2 & (f/.(j+1))`2
> (f/.j)`2 and
A38: 2 <= j+1 and
A39: j+1 < len f;
1+1 <= j+1 by A38;
then
A40: 1 <= j by XREAL_1:6;
thus (f/.(j+1))`2 >= (f/.2)`2
proof
per cases by A38,XXREAL_0:1;
suppose
2 = j+1;
hence thesis;
end;
suppose
2 < j+1;
hence thesis by A37,A39,NAT_1:13,XXREAL_0:2;
end;
end;
A41: j+1+1 <= len f by A39,NAT_1:13;
A42: now
per cases by A38,XXREAL_0:1;
suppose
1+1 = j+1;
hence (f/.(j+1))`2 > (f/.j)`2 by A35;
end;
suppose
2 < j+1;
hence (f/.(j+1))`2 > (f/.j)`2 by A37,A39,NAT_1:13;
end;
end;
A43: 1 <= j+1 by NAT_1:11;
then
A44: j+1 in dom f by A39,FINSEQ_3:25;
then
A45: (f/.(j+1))`1 = (f/.1)`1 by A1;
j < len f by A39,NAT_1:13;
then
A46: j in dom f by A40,FINSEQ_3:25;
then
A47: (f/.j)`1 = (f/.1)`1 by A1;
1 <= j+1+1 by NAT_1:11;
then
A48: j+1+1 in dom f by A41,FINSEQ_3:25;
then
A49: (f/.(j+1+1))`1 = (f/.1)`1 by A1;
assume
A50: (f/.(j+1+1))`2 <= (f/.(j+1))`2;
per cases by A50,XXREAL_0:1;
suppose
A51: (f/.(j+1+1))`2 < (f/.(j+1))`2;
now
per cases;
suppose
(f/.j)`2 >= (f/.(j+1+1))`2;
then f/.j in LSeg(f/.(j+1),f/.(j+1+1)) by A42,A47,A45,A49,Th7;
then
A52: f/.j in LSeg(f,j+1) by A41,A43,TOPREAL1:def 3;
j+1+1 = j+(1+1);
then
A53: LSeg(f,j) /\ LSeg(f,j+1) = {f/.(j+1)} by A41,A40,TOPREAL1:def 6;
f/.j in LSeg(f,j) by A39,A40,TOPREAL1:21;
then f/.j in LSeg(f,j) /\ LSeg(f,j+1) by A52,XBOOLE_0:def 4;
then f/.j = f/.(j+1) by A53,TARSKI:def 1;
hence contradiction by A46,A44,Th29;
end;
suppose
(f/.j)`2 <= (f/.(j+1+1))`2;
then f/.(j+1+1) in LSeg(f/.j,f/.(j+1)) by A47,A45,A49,A51,Th7;
then
A54: f/.(j+1+1) in LSeg(f,j) by A39,A40,TOPREAL1:def 3;
j+1+1 = j+(1+1);
then
A55: LSeg(f,j) /\ LSeg(f,j+1) = {f/.(j+1)} by A41,A40,TOPREAL1:def 6;
f/.(j+1+1) in LSeg(f,j+1) by A41,A43,TOPREAL1:21;
then f/.(j+1+1) in LSeg(f,j) /\ LSeg(f,j+1) by A54,XBOOLE_0:def 4;
then f/.(j+1+1) = f/.(j+1) by A55,TARSKI:def 1;
hence contradiction by A44,A48,Th29;
end;
end;
hence contradiction;
end;
suppose
A56: (f/.(j+1+1))`2 = (f/.(j+1))`2;
(f/.(j+1+1))`1 = (f/.1)`1 by A1,A48
.= (f/.(j+1))`1 by A1,A44;
then f/.(j+1+1) = |[(f/.(j+1))`1,(f/.(j+1))`2]| by A56,EUCLID:53
.= f/.(j+1) by EUCLID:53;
hence contradiction by A44,A48,Th29;
end;
end;
A57: len f -'1+1 = len f by A2,XREAL_1:235;
then
A58: 2 <= len f -'1 & len f-'1 < len f by A7,NAT_1:13;
A59: P[0];
A60: for j holds P[j] from NAT_1:sch 2(A59,A36);
then
A61: (f/.(len f-'1))`2 >= (f/.2)`2 by A58;
(f/.len f)`2 > (f/.(len f -'1))`2 by A60,A57,A58;
then (f/.len f)`2 > (f/.2)`2 by A61,XXREAL_0:2;
hence contradiction by A35,FINSEQ_6:def 1;
end;
end;
theorem Th31:
ex i st i in dom f & (f/.i)`2 <> (f/.1)`2
proof
assume
A1: for i st i in dom f holds (f/.i)`2 = (f/.1)`2;
A2: len f > 1 by Lm2;
then
A3: len f >= 1+1 by NAT_1:13;
then
A4: 1+1 in dom f by FINSEQ_3:25;
A5: now
assume
A6: (f/.2)`1 = (f/.1)`1;
(f/.2)`2 = (f/.1)`2 by A1,A4;
then f/.2 = |[(f/.1)`1,(f/.1)`2]| by A6,EUCLID:53
.= f/.1 by EUCLID:53;
hence contradiction by A4,Th29,FINSEQ_5:6;
end;
len f = 2 implies f/.2 = f/.1 by FINSEQ_6:def 1;
then
A7: 2 < len f by A3,A5,XXREAL_0:1;
per cases by A5,XXREAL_0:1;
suppose
A8: (f/.2)`1 < (f/.1)`1;
defpred P[Nat] means
2 <= $1 & $1 < len f implies (f/.$1)`1 <=
(f/.2)`1 & (f/.($1+1))`1 < (f/.$1)`1;
A9: for j st P[j] holds P[j+1]
proof
let j such that
A10: 2 <= j & j < len f implies (f/.j)`1 <= (f/.2)`1 & (f/.(j+1))`1
< (f/.j)`1 and
A11: 2 <= j+1 and
A12: j+1 < len f;
1+1 <= j+1 by A11;
then
A13: 1 <= j by XREAL_1:6;
thus (f/.(j+1))`1 <= (f/.2)`1
proof
per cases by A11,XXREAL_0:1;
suppose
2 = j+1;
hence thesis;
end;
suppose
2 < j+1;
hence thesis by A10,A12,NAT_1:13,XXREAL_0:2;
end;
end;
A14: j+1+1 <= len f by A12,NAT_1:13;
A15: now
per cases by A11,XXREAL_0:1;
suppose
1+1 = j+1;
hence (f/.(j+1))`1 < (f/.j)`1 by A8;
end;
suppose
2 < j+1;
hence (f/.(j+1))`1 < (f/.j)`1 by A10,A12,NAT_1:13;
end;
end;
A16: 1 <= j+1 by NAT_1:11;
then
A17: j+1 in dom f by A12,FINSEQ_3:25;
then
A18: (f/.(j+1))`2 = (f/.1)`2 by A1;
j < len f by A12,NAT_1:13;
then
A19: j in dom f by A13,FINSEQ_3:25;
then
A20: (f/.j)`2 = (f/.1)`2 by A1;
1 <= j+1+1 by NAT_1:11;
then
A21: j+1+1 in dom f by A14,FINSEQ_3:25;
then
A22: (f/.(j+1+1))`2 = (f/.1)`2 by A1;
assume
A23: (f/.(j+1+1))`1 >= (f/.(j+1))`1;
per cases by A23,XXREAL_0:1;
suppose
A24: (f/.(j+1+1))`1 > (f/.(j+1))`1;
now
per cases;
suppose
(f/.j)`1 <= (f/.(j+1+1))`1;
then f/.j in LSeg(f/.(j+1),f/.(j+1+1)) by A15,A20,A18,A22,Th8;
then
A25: f/.j in LSeg(f,j+1) by A14,A16,TOPREAL1:def 3;
j+1+1 = j+(1+1);
then
A26: LSeg(f,j) /\ LSeg(f,j+1) = {f/.(j+1)} by A14,A13,TOPREAL1:def 6;
f/.j in LSeg(f,j) by A12,A13,TOPREAL1:21;
then f/.j in LSeg(f,j) /\ LSeg(f,j+1) by A25,XBOOLE_0:def 4;
then f/.j = f/.(j+1) by A26,TARSKI:def 1;
hence contradiction by A19,A17,Th29;
end;
suppose
(f/.j)`1 >= (f/.(j+1+1))`1;
then f/.(j+1+1) in LSeg(f/.j,f/.(j+1)) by A20,A18,A22,A24,Th8;
then
A27: f/.(j+1+1) in LSeg(f,j) by A12,A13,TOPREAL1:def 3;
j+1+1 = j+(1+1);
then
A28: LSeg(f,j) /\ LSeg(f,j+1) = {f/.(j+1)} by A14,A13,TOPREAL1:def 6;
f/.(j+1+1) in LSeg(f,j+1) by A14,A16,TOPREAL1:21;
then f/.(j+1+1) in LSeg(f,j) /\ LSeg(f,j+1) by A27,XBOOLE_0:def 4;
then f/.(j+1+1) = f/.(j+1) by A28,TARSKI:def 1;
hence contradiction by A17,A21,Th29;
end;
end;
hence contradiction;
end;
suppose
A29: (f/.(j+1+1))`1 = (f/.(j+1))`1;
(f/.(j+1+1))`2 = (f/.1)`2 by A1,A21
.= (f/.(j+1))`2 by A1,A17;
then f/.(j+1+1) = |[(f/.(j+1))`1,(f/.(j+1))`2]| by A29,EUCLID:53
.= f/.(j+1) by EUCLID:53;
hence contradiction by A17,A21,Th29;
end;
end;
A30: len f -'1+1 = len f by A2,XREAL_1:235;
then
A31: 2 <= len f -'1 & len f-'1 < len f by A7,NAT_1:13;
A32: P[0];
A33: for j holds P[j] from NAT_1:sch 2(A32,A9);
then
A34: (f/.(len f-'1))`1 <= (f/.2)`1 by A31;
(f/.len f)`1 < (f/.(len f-'1))`1 by A33,A30,A31;
then (f/.len f)`1 < (f/.2)`1 by A34,XXREAL_0:2;
hence contradiction by A8,FINSEQ_6:def 1;
end;
suppose
A35: (f/.2)`1 > (f/.1)`1;
defpred P[Nat] means
2 <= $1 & $1 < len f implies (f/.$1)`1 >=
(f/.2)`1 & (f/.($1+1))`1 > (f/.$1)`1;
A36: for j st P[j] holds P[j+1]
proof
let j such that
A37: 2 <= j & j < len f implies (f/.j)`1 >= (f/.2)`1 & (f/.(j+1))`1
> (f/.j)`1 and
A38: 2 <= j+1 and
A39: j+1 < len f;
1+1 <= j+1 by A38;
then
A40: 1 <= j by XREAL_1:6;
thus (f/.(j+1))`1 >= (f/.2)`1
proof
per cases by A38,XXREAL_0:1;
suppose
2 = j+1;
hence thesis;
end;
suppose
2 < j+1;
hence thesis by A37,A39,NAT_1:13,XXREAL_0:2;
end;
end;
A41: j+1+1 <= len f by A39,NAT_1:13;
A42: now
per cases by A38,XXREAL_0:1;
suppose
1+1 = j+1;
hence (f/.(j+1))`1 > (f/.j)`1 by A35;
end;
suppose
2 < j+1;
hence (f/.(j+1))`1 > (f/.j)`1 by A37,A39,NAT_1:13;
end;
end;
A43: 1 <= j+1 by NAT_1:11;
then
A44: j+1 in dom f by A39,FINSEQ_3:25;
then
A45: (f/.(j+1))`2 = (f/.1)`2 by A1;
j < len f by A39,NAT_1:13;
then
A46: j in dom f by A40,FINSEQ_3:25;
then
A47: (f/.j)`2 = (f/.1)`2 by A1;
1 <= j+1+1 by NAT_1:11;
then
A48: j+1+1 in dom f by A41,FINSEQ_3:25;
then
A49: (f/.(j+1+1))`2 = (f/.1)`2 by A1;
assume
A50: (f/.(j+1+1))`1 <= (f/.(j+1))`1;
per cases by A50,XXREAL_0:1;
suppose
A51: (f/.(j+1+1))`1 < (f/.(j+1))`1;
now
per cases;
suppose
(f/.j)`1 >= (f/.(j+1+1))`1;
then f/.j in LSeg(f/.(j+1),f/.(j+1+1)) by A42,A47,A45,A49,Th8;
then
A52: f/.j in LSeg(f,j+1) by A41,A43,TOPREAL1:def 3;
j+1+1 = j+(1+1);
then
A53: LSeg(f,j) /\ LSeg(f,j+1) = {f/.(j+1)} by A41,A40,TOPREAL1:def 6;
f/.j in LSeg(f,j) by A39,A40,TOPREAL1:21;
then f/.j in LSeg(f,j) /\ LSeg(f,j+1) by A52,XBOOLE_0:def 4;
then f/.j = f/.(j+1) by A53,TARSKI:def 1;
hence contradiction by A46,A44,Th29;
end;
suppose
(f/.j)`1 <= (f/.(j+1+1))`1;
then f/.(j+1+1) in LSeg(f/.j,f/.(j+1)) by A47,A45,A49,A51,Th8;
then
A54: f/.(j+1+1) in LSeg(f,j) by A39,A40,TOPREAL1:def 3;
j+1+1 = j+(1+1);
then
A55: LSeg(f,j) /\ LSeg(f,j+1) = {f/.(j+1)} by A41,A40,TOPREAL1:def 6;
f/.(j+1+1) in LSeg(f,j+1) by A41,A43,TOPREAL1:21;
then f/.(j+1+1) in LSeg(f,j) /\ LSeg(f,j+1) by A54,XBOOLE_0:def 4;
then f/.(j+1+1) = f/.(j+1) by A55,TARSKI:def 1;
hence contradiction by A44,A48,Th29;
end;
end;
hence contradiction;
end;
suppose
A56: (f/.(j+1+1))`1 = (f/.(j+1))`1;
(f/.(j+1+1))`2 = (f/.1)`2 by A1,A48
.= (f/.(j+1))`2 by A1,A44;
then f/.(j+1+1) = |[(f/.(j+1))`1,(f/.(j+1))`2]| by A56,EUCLID:53
.= f/.(j+1) by EUCLID:53;
hence contradiction by A44,A48,Th29;
end;
end;
A57: len f -'1+1 = len f by A2,XREAL_1:235;
then
A58: 2 <= len f -'1 & len f-'1 < len f by A7,NAT_1:13;
A59: P[0];
A60: for j holds P[j] from NAT_1:sch 2(A59,A36);
then
A61: (f/.(len f-'1))`1 >= (f/.2)`1 by A58;
(f/.len f)`1 > (f/.(len f-'1))`1 by A60,A57,A58;
then (f/.len f)`1 > (f/.2)`1 by A61,XXREAL_0:2;
hence contradiction by A35,FINSEQ_6:def 1;
end;
end;
theorem
len GoB f > 1
proof
A1: len GoB f <> 0 by MATRIX_0:def 10;
1 in dom f by FINSEQ_5:6;
then consider i2,j2 such that
A2: [i2,j2] in Indices GoB f and
A3: f/.1 = (GoB f)*(i2,j2) by GOBOARD2:14;
A4: 1 <= i2 by A2,MATRIX_0:32;
assume len GoB f <= 1;
then
A5: len GoB f = 1 by A1,NAT_1:25;
then i2 <= 1 by A2,MATRIX_0:32;
then
A6: i2 = 1 by A4,XXREAL_0:1;
consider i such that
A7: i in dom f and
A8: (f/.i)`1 <> (f/.1)`1 by Th30;
consider i1,j1 such that
A9: [i1,j1] in Indices GoB f and
A10: f/.i = (GoB f)*(i1,j1) by A7,GOBOARD2:14;
A11: 1 <= j1 & j1 <= width GoB f by A9,MATRIX_0:32;
A12: 1 <= i1 by A9,MATRIX_0:32;
i1 <= 1 by A5,A9,MATRIX_0:32;
then i1 = 1 by A12,XXREAL_0:1;
then
A13: (GoB f)*(i1,j1)`1 = (GoB f)*(1,1)`1 by A5,A11,GOBOARD5:2;
1 <= j2 & j2 <= width GoB f by A2,MATRIX_0:32;
hence contradiction by A5,A8,A10,A3,A13,A6,GOBOARD5:2;
end;
theorem
width GoB f > 1
proof
A1: width GoB f <> 0 by MATRIX_0:def 10;
1 in dom f by FINSEQ_5:6;
then consider i2,j2 such that
A2: [i2,j2] in Indices GoB f and
A3: f/.1 = (GoB f)*(i2,j2) by GOBOARD2:14;
A4: 1 <= j2 by A2,MATRIX_0:32;
assume width GoB f <= 1;
then
A5: width GoB f = 1 by A1,NAT_1:25;
then j2 <= 1 by A2,MATRIX_0:32;
then
A6: j2 = 1 by A4,XXREAL_0:1;
consider i such that
A7: i in dom f and
A8: (f/.i)`2 <> (f/.1)`2 by Th31;
consider i1,j1 such that
A9: [i1,j1] in Indices GoB f and
A10: f/.i = (GoB f)*(i1,j1) by A7,GOBOARD2:14;
A11: 1 <= i1 & i1 <= len GoB f by A9,MATRIX_0:32;
A12: 1 <= j1 by A9,MATRIX_0:32;
j1 <= 1 by A5,A9,MATRIX_0:32;
then j1 = 1 by A12,XXREAL_0:1;
then
A13: (GoB f)*(i1,j1)`2 = (GoB f)*(1,1)`2 by A5,A11,GOBOARD5:1;
1 <= i2 & i2 <= len GoB f by A2,MATRIX_0:32;
hence contradiction by A5,A8,A10,A3,A13,A6,GOBOARD5:1;
end;
theorem Th34:
len f > 4
proof
assume
A1: len f <= 4;
A2: len f > 1 by Lm2;
then
A3: 1 in dom f by FINSEQ_3:25;
A4: len f >= 1+1 by A2,NAT_1:13;
then
A5: 2 in dom f by FINSEQ_3:25;
consider i2 such that
A6: i2 in dom f and
A7: (f/.i2)`2 <> (f/.1)`2 by Th31;
consider i1 such that
A8: i1 in dom f and
A9: (f/.i1)`1 <> (f/.1)`1 by Th30;
per cases by A4,TOPREAL1:def 5;
suppose
A10: (f/.(1+1))`1 = (f/.1)`1;
A11: i1 <= len f by A8,FINSEQ_3:25;
A12: f/.len f = f/.1 by FINSEQ_6:def 1;
A13: i1 <> 0 by A8,FINSEQ_3:25;
now
i1 <= 4 by A1,A11,XXREAL_0:2;
then i1 = 0 or ... or i1 = 4;
then per cases by A9,A10,A13;
suppose
A14: i1 = 3;
A15: now
assume (f/.(1+1))`2 = (f/.1)`2;
then f/.(1+1) = |[(f/.1)`1,(f/.1)`2]| by A10,EUCLID:53
.= f/.1 by EUCLID:53;
hence contradiction by A3,A5,Th29;
end;
A16: len f >= 3 by A8,A14,FINSEQ_3:25;
then len f > 3 by A9,A12,A14,XXREAL_0:1;
then
A17: len f >= 3+1 by NAT_1:13;
then
A18: (f/.3)`1 = (f/.(3+1))`1 or (f/.3)`2 = (f/.(3+1))`2 by TOPREAL1:def 5;
A19: len f = 4 by A1,A17,XXREAL_0:1;
(f/.2)`2 = (f/.(2+1))`2 by A9,A10,A14,A16,TOPREAL1:def 5;
hence contradiction by A9,A14,A19,A15,A18,FINSEQ_6:def 1;
end;
suppose
i1 = 4;
hence contradiction by A1,A9,A11,A12,XXREAL_0:1;
end;
end;
hence contradiction;
end;
suppose
A20: (f/.(1+1))`2 = (f/.1)`2;
A21: i2 <= len f by A6,FINSEQ_3:25;
A22: f/.len f = f/.1 by FINSEQ_6:def 1;
A23: i2 <> 0 by A6,FINSEQ_3:25;
now
i2 <= 4 by A1,A21,XXREAL_0:2;
then i2 = 0 or ... or i2 = 4;
then per cases by A7,A20,A23;
suppose
A24: i2 = 3;
A25: now
assume (f/.(1+1))`1 = (f/.1)`1;
then f/.(1+1) = |[(f/.1)`1,(f/.1)`2]| by A20,EUCLID:53
.= f/.1 by EUCLID:53;
hence contradiction by A3,A5,Th29;
end;
A26: len f >= 3 by A6,A24,FINSEQ_3:25;
then len f > 3 by A7,A22,A24,XXREAL_0:1;
then
A27: len f >= 3+1 by NAT_1:13;
then
A28: (f/.3)`2 = (f/.(3+1))`2 or (f/.3)`1 = (f/.(3+1))`1 by TOPREAL1:def 5;
A29: len f = 4 by A1,A27,XXREAL_0:1;
(f/.2)`1 = (f/.(2+1))`1 by A7,A20,A24,A26,TOPREAL1:def 5;
hence contradiction by A7,A24,A29,A25,A28,FINSEQ_6:def 1;
end;
suppose
i2 = 4;
hence contradiction by A1,A7,A21,A22,XXREAL_0:1;
end;
end;
hence contradiction;
end;
end;
theorem Th35:
for f being circular s.c.c. FinSequence of TOP-REAL 2 st len f >
4 for i,j being Nat st 1 <= i & i < j & j < len f holds f/.i <> f/.j
proof
let f be circular s.c.c. FinSequence of TOP-REAL 2 such that
A1: len f > 4;
let i,j be Nat such that
A2: 1 <= i and
A3: i < j and
A4: j < len f and
A5: f/.i = f/.j;
A6: j+1 <= len f by A4,NAT_1:13;
A7: i+1 <= j & i <> 0 by A2,A3,NAT_1:13;
1 <= j by A2,A3,XXREAL_0:2;
then
A8: f/.j in LSeg(f,j) by A6,TOPREAL1:21;
A9: i < len f by A3,A4,XXREAL_0:2;
then i+1 <= len f by NAT_1:13;
then
A10: f/.i in LSeg(f,i) by A2,TOPREAL1:21;
i <= 2 implies i = 0 or ... or i = 2;
then per cases by A7,XXREAL_0:1;
suppose that
A11: i+1 = j and
A12: i = 1;
A13: len f -' 1 + 1 = len f by A1,XREAL_1:235,XXREAL_0:2;
j+1+1 < len f by A1,A11,A12;
then
A14: j+1 < len f -' 1 by A13,XREAL_1:6;
len f -' 1 < len f by A13,XREAL_1:29;
then LSeg(f,j) misses LSeg(f,len f -' 1) by A11,A12,A14,GOBOARD5:def 4;
then
A15: LSeg(f,j) /\ LSeg(f,len f -' 1) = {} by XBOOLE_0:def 7;
A16: f/.i = f/.len f by A12,FINSEQ_6:def 1;
1+1 <= len f by A1,XXREAL_0:2;
then 1 <= len f -' 1 by A13,XREAL_1:6;
then f/.i in LSeg(f,len f -' 1) by A13,A16,TOPREAL1:21;
hence contradiction by A5,A8,A15,XBOOLE_0:def 4;
end;
suppose that
A17: i+1 = j and
A18: i = 1+1;
A19: i -' 1 + 1 = i by A2,XREAL_1:235;
j+1 < len f by A1,A17,A18;
then LSeg(f,i -' 1) misses LSeg(f,j) by A3,A19,GOBOARD5:def 4;
then
A20: LSeg(f,i -' 1) /\ LSeg(f,j) = {} by XBOOLE_0:def 7;
f/.i in LSeg(f,i -' 1) by A9,A18,A19,TOPREAL1:21;
hence contradiction by A5,A8,A20,XBOOLE_0:def 4;
end;
suppose that
A21: i > 1+1;
A22: i -' 1 + 1 = i by A2,XREAL_1:235;
then
A23: 1 < i -' 1 by A21,XREAL_1:6;
then LSeg(f,i-'1) misses LSeg(f,j) by A3,A4,A22,GOBOARD5:def 4;
then
A24: LSeg(f,i-'1) /\ LSeg(f,j) = {} by XBOOLE_0:def 7;
f/.i in LSeg(f,i-' 1) by A9,A22,A23,TOPREAL1:21;
hence contradiction by A5,A8,A24,XBOOLE_0:def 4;
end;
suppose that
A25: i+1 < j and
A26: i <> 1;
1 < i by A2,A26,XXREAL_0:1;
then LSeg(f,i) misses LSeg(f,j) by A4,A25,GOBOARD5:def 4;
then LSeg(f,i) /\ LSeg(f,j) = {} by XBOOLE_0:def 7;
hence contradiction by A5,A8,A10,XBOOLE_0:def 4;
end;
suppose that
A27: i+1 < j and
A28: j+1 <> len f;
j+1 < len f by A6,A28,XXREAL_0:1;
then LSeg(f,i) misses LSeg(f,j) by A27,GOBOARD5:def 4;
then LSeg(f,i) /\ LSeg(f,j) = {} by XBOOLE_0:def 7;
hence contradiction by A5,A8,A10,XBOOLE_0:def 4;
end;
suppose that
A29: i+1 < j and
A30: i = 1 and
A31: j+1 = len f;
A32: j < len f by A31,NAT_1:13;
A33: j-'1+1 = j by A2,A3,XREAL_1:235,XXREAL_0:2;
then
A34: i+1 <= j-'1 by A29,NAT_1:13;
i+1 <> j-'1 by A1,A30,A31,A33;
then i+1 < j-'1 by A34,XXREAL_0:1;
then LSeg(f,1) misses LSeg(f,j-'1) by A30,A33,A32,GOBOARD5:def 4;
then
A35: LSeg(f,1) /\ LSeg(f,j-'1) = {} by XBOOLE_0:def 7;
1 <= j-'1 by A30,A34,XXREAL_0:2;
then f/.j in LSeg(f,j-'1) by A4,A33,TOPREAL1:21;
hence contradiction by A5,A10,A30,A35,XBOOLE_0:def 4;
end;
end;
theorem Th36:
for i,j being Nat st 1 <= i & i < j & j < len f holds f/.i <> f/.j
proof
len f > 4 by Th34;
hence thesis by Th35;
end;
theorem Th37:
for i,j being Nat st 1 < i & i < j & j <= len f holds f/.i <> f/.j
proof
let i,j be Nat such that
A1: 1 < i and
A2: i < j and
A3: j <= len f;
per cases by A3,XXREAL_0:1;
suppose
j < len f;
hence thesis by A1,A2,Th36;
end;
suppose
j = len f;
then
A4: f/.j = f/.1 by FINSEQ_6:def 1;
i < len f by A2,A3,XXREAL_0:2;
hence thesis by A1,A4,Th36;
end;
end;
theorem Th38:
for i being Nat st 1 < i & i <= len f & f/.i = f/.1
holds i = len f
proof
let i be Nat such that
A1: 1 < i and
A2: i <= len f and
A3: f/.i = f/.1;
assume i <> len f;
then i < len f by A2,XXREAL_0:1;
hence contradiction by A1,A3,Th36;
end;
theorem Th39:
1 <= i & i <= len GoB f & 1 <= j & j+1 <= width GoB f & 1/2*((
GoB f)*(i,j)+(GoB f)*(i,j+1)) in L~f implies ex k st 1 <= k & k+1 <= len f &
LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k)
proof
set mi = 1/2*((GoB f)*(i,j)+(GoB f)*(i,j+1));
assume that
A1: 1 <= i & i <= len GoB f & 1 <= j & j+1 <= width GoB f and
A2: 1/2*((GoB f)*(i,j)+(GoB f)*(i,j+1)) in L~f;
L~f = union { LSeg(f,k) : 1 <= k & k+1 <= len f } by TOPREAL1:def 4;
then consider x be set such that
A3: 1/2*((GoB f)*(i,j)+(GoB f)*(i,j+1)) in x and
A4: x in { LSeg(f,k) : 1 <= k & k+1 <= len f } by A2,TARSKI:def 4;
consider k such that
A5: x = LSeg(f,k) and
A6: 1 <= k and
A7: k+1 <= len f by A4;
A8: f is_sequence_on GoB f by GOBOARD5:def 5;
A9: mi in LSeg(f/.k,f/.(k+1)) by A3,A5,A6,A7,TOPREAL1:def 3;
k <= k+1 by NAT_1:11;
then k <= len f by A7,XXREAL_0:2;
then
A10: k in dom f by A6,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A11: [i1,j1] in Indices GoB f and
A12: f/.k = (GoB f)*(i1,j1) by A8,GOBOARD1:def 9;
A13: 1 <= i1 by A11,MATRIX_0:32;
take k;
thus 1 <= k & k+1 <= len f by A6,A7;
1 <= k+1 by NAT_1:11;
then
A14: k+1 in dom f by A7,FINSEQ_3:25;
then consider i2,j2 being Nat such that
A15: [i2,j2] in Indices GoB f and
A16: f/.(k+1) = (GoB f)*(i2,j2) by A8,GOBOARD1:def 9;
A17: 1 <= i2 by A15,MATRIX_0:32;
A18: j2 <= width GoB f by A15,MATRIX_0:32;
|.i1-i2.|+|.j1-j2.| = 1 by A8,A10,A11,A12,A14,A15,A16,GOBOARD1:def 9;
then
A19: |.i1-i2.| = 1 & j1 = j2 or |.j1-j2.| = 1 & i1 = i2 by SEQM_3:42;
A20: i1 <= len GoB f by A11,MATRIX_0:32;
A21: j1 <= width GoB f by A11,MATRIX_0:32;
A22: 1 <= j1 by A11,MATRIX_0:32;
A23: i2 <= len GoB f by A15,MATRIX_0:32;
A24: 1 <= j2 by A15,MATRIX_0:32;
per cases by A19,SEQM_3:41;
suppose
A25: j1 = j2 & i1 = i2+1;
then
mi in LSeg((GoB f)*(i2,j2),(GoB f)*(i2+1,j2)) by A3,A5,A6,A7,A12,A16,
TOPREAL1:def 3;
hence thesis by A1,A20,A17,A24,A18,A25,Th28;
end;
suppose
A26: j1 = j2 & i1+1 = i2;
then
mi in LSeg((GoB f)*(i1,j1),(GoB f)*(i1+1,j1)) by A3,A5,A6,A7,A12,A16,
TOPREAL1:def 3;
hence thesis by A1,A13,A22,A21,A23,A26,Th28;
end;
suppose
A27: j1 = j2+1 & i1 = i2;
then i = i2 & j = j2 by A1,A12,A16,A13,A20,A21,A24,A9,Th25;
hence thesis by A6,A7,A12,A16,A27,TOPREAL1:def 3;
end;
suppose
A28: j1+1 = j2 & i1 = i2;
then i = i1 & j = j1 by A1,A12,A16,A13,A20,A22,A18,A9,Th25;
hence thesis by A6,A7,A12,A16,A28,TOPREAL1:def 3;
end;
end;
theorem Th40:
1 <= i & i+1 <= len GoB f & 1 <= j & j <= width GoB f & 1/2*((
GoB f)*(i,j)+(GoB f)*(i+1,j)) in L~f implies ex k st 1 <= k & k+1 <= len f &
LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k)
proof
set mi = 1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j));
assume that
A1: 1 <= i & i+1 <= len GoB f & 1 <= j & j <= width GoB f and
A2: 1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j)) in L~f;
L~f = union { LSeg(f,k) : 1 <= k & k+1 <= len f } by TOPREAL1:def 4;
then consider x be set such that
A3: 1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j)) in x and
A4: x in { LSeg(f,k) : 1 <= k & k+1 <= len f } by A2,TARSKI:def 4;
consider k such that
A5: x = LSeg(f,k) and
A6: 1 <= k and
A7: k+1 <= len f by A4;
A8: f is_sequence_on GoB f by GOBOARD5:def 5;
A9: mi in LSeg(f/.k,f/.(k+1)) by A3,A5,A6,A7,TOPREAL1:def 3;
k <= k+1 by NAT_1:11;
then k <= len f by A7,XXREAL_0:2;
then
A10: k in dom f by A6,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A11: [i1,j1] in Indices GoB f and
A12: f/.k = (GoB f)*(i1,j1) by A8,GOBOARD1:def 9;
A13: 1 <= j1 by A11,MATRIX_0:32;
take k;
thus 1 <= k & k+1 <= len f by A6,A7;
1 <= k+1 by NAT_1:11;
then
A14: k+1 in dom f by A7,FINSEQ_3:25;
then consider i2,j2 being Nat such that
A15: [i2,j2] in Indices GoB f and
A16: f/.(k+1) = (GoB f)*(i2,j2) by A8,GOBOARD1:def 9;
A17: 1 <= j2 by A15,MATRIX_0:32;
A18: i2 <= len GoB f by A15,MATRIX_0:32;
|.j1-j2.|+|.i1-i2.| = 1 by A8,A10,A11,A12,A14,A15,A16,GOBOARD1:def 9;
then
A19: |.j1-j2.| = 1 & i1 = i2 or |.i1-i2.| = 1 & j1 = j2 by SEQM_3:42;
A20: j1 <= width GoB f by A11,MATRIX_0:32;
A21: i1 <= len GoB f by A11,MATRIX_0:32;
A22: 1 <= i1 by A11,MATRIX_0:32;
A23: j2 <= width GoB f by A15,MATRIX_0:32;
A24: 1 <= i2 by A15,MATRIX_0:32;
per cases by A19,SEQM_3:41;
suppose
A25: i1 = i2 & j1 = j2+1;
then
mi in LSeg((GoB f)*(i2,j2),(GoB f)*(i2,j2+1)) by A3,A5,A6,A7,A12,A16,
TOPREAL1:def 3;
hence thesis by A1,A20,A17,A24,A18,A25,Th27;
end;
suppose
A26: i1 = i2 & j1+1 = j2;
then
mi in LSeg((GoB f)*(i1,j1),(GoB f)*(i1,j1+1)) by A3,A5,A6,A7,A12,A16,
TOPREAL1:def 3;
hence thesis by A1,A13,A22,A21,A23,A26,Th27;
end;
suppose
A27: i1 = i2+1 & j1 = j2;
then j = j2 & i = i2 by A1,A12,A16,A13,A20,A21,A24,A9,Th26;
hence thesis by A6,A7,A12,A16,A27,TOPREAL1:def 3;
end;
suppose
A28: i1+1 = i2 & j1 = j2;
then j = j1 & i = i1 by A1,A12,A16,A13,A20,A22,A18,A9,Th26;
hence thesis by A6,A7,A12,A16,A28,TOPREAL1:def 3;
end;
end;
theorem
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1
< len f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i
+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j+1) & f/.(k+1
) = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i+1,j)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: 1 <= k and
A6: k+1 < len f and
A7: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) and
A8: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1);
A9: 1 <= j+1 by NAT_1:11;
A10: i < i+1 by NAT_1:13;
A11: 1 <= i+1 by NAT_1:11;
j < width GoB f by A4,NAT_1:13;
then (GoB f)*(i+1,j)`1 = (GoB f)*(i+1,1)`1 by A2,A3,A11,GOBOARD5:2
.= (GoB f)*(i+1,j+1)`1 by A2,A4,A9,A11,GOBOARD5:2;
then
A12: (GoB f)*(i,j+1) <> (GoB f)*(i+1,j) by A1,A2,A4,A9,A10,GOBOARD5:3;
A13: 1 <= k+1 by NAT_1:11;
A14: k+(1+1) = k+1+1;
then k+2 <= len f by A6,NAT_1:13;
then
A15: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f/.(k+1),f/.(k+2)) by A8
,A14,A13,TOPREAL1:def 3;
then
A16: (GoB f)*(i+1,j) = f/.(k+2) & (GoB f)*(i+1,j+1) = f/.(k+1) or (GoB f)*(i
+1,j) = f/.(k+1) & (GoB f)*(i+1,j+1) = f/.(k+2) by SPPOL_1:8;
A17: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f/.k,f/.(k+1)) by A5,A6,A7,
TOPREAL1:def 3;
then
(GoB f)*(i+1,j+1) = f/.(k+1) & (GoB f)*(i,j+1) = f/.k or (GoB f)*(i+1,j
+1) = f/.k & (GoB f)* (i,j+1) = f/.(k+1) by SPPOL_1:8;
hence f/.k = (GoB f)*(i,j+1) by A15,A12,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i+1,j+1) by A17,A16,A12,SPPOL_1:8;
thus thesis by A17,A16,A12,SPPOL_1:8;
end;
theorem
1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f & 1 <= k & k+1 <
len f & LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f,k) & LSeg((GoB f)*(i,j),
(GoB f)*(i,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j+2) & f/.(k+1) = (GoB
f)*(i,j+1) & f/.(k+2) = (GoB f)*(i,j)
proof
assume that
A1: 1 <= i & i <= len GoB f & 1 <= j and
A2: j+1 < width GoB f and
A3: 1 <= k and
A4: k+1 < len f and
A5: LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f,k) and
A6: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k+1);
A7: 1 <= k+1 by NAT_1:11;
A8: k+(1+1) = k+1+1;
then k+2 <= len f by A4,NAT_1:13;
then
A9: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f/.(k+1),f/.(k+2)) by A6,A8,A7,
TOPREAL1:def 3;
then
A10: (GoB f)*(i,j) = f/.(k+2) & (GoB f)*(i,j+1) = f/.(k+1) or (GoB f)*(i,j)
= f/.(k+1) & (GoB f)*(i,j+1) = f/.(k+2) by SPPOL_1:8;
A11: j < j+2 by XREAL_1:29;
j+(1+1) = j+1+1;
then j+2 <= width GoB f by A2,NAT_1:13;
then
A12: (GoB f)*(i,j)`2 < (GoB f)*(i,j+2)`2 by A1,A11,GOBOARD5:4;
A13: LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f/.k,f/.(k+1)) by A3,A4,A5,
TOPREAL1:def 3;
then
(GoB f)*(i,j+1) = f/.(k+1) & (GoB f)*(i,j+2) = f/.k or (GoB f)*(i,j+1) =
f/.k & (GoB f)*(i,j+2) = f/.(k+1) by SPPOL_1:8;
hence f/.k = (GoB f)*(i,j+2) by A9,A12,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i,j+1) by A13,A10,A12,SPPOL_1:8;
thus thesis by A13,A10,A12,SPPOL_1:8;
end;
theorem
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1
< len f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i
,j),(GoB f)*(i,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i+1,j+1) & f/.(k+1)
= (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i,j)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: 1 <= k and
A6: k+1 < len f and
A7: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) and
A8: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k+1);
A9: j < width GoB f by A4,NAT_1:13;
A10: j < j+1 by NAT_1:13;
A11: 1 <= i+1 by NAT_1:11;
i < len GoB f by A2,NAT_1:13;
then (GoB f)*(i,j)`2 = (GoB f)*(1,j)`2 by A1,A3,A9,GOBOARD5:1
.= (GoB f)*(i+1,j)`2 by A2,A3,A11,A9,GOBOARD5:1;
then
A12: (GoB f)*(i,j) <> (GoB f)*(i+1,j+1) by A2,A3,A4,A11,A10,GOBOARD5:4;
A13: 1 <= k+1 by NAT_1:11;
A14: k+(1+1) = k+1+1;
then k+2 <= len f by A6,NAT_1:13;
then
A15: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f/.(k+1),f/.(k+2)) by A8,A14
,A13,TOPREAL1:def 3;
then
A16: (GoB f)*(i,j) = f/.(k+2) & (GoB f)*(i,j+1) = f/.(k+1) or (GoB f)*(i,j)
= f/.(k+1) & (GoB f)*(i,j+1) = f/.(k+2) by SPPOL_1:8;
A17: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f/.k,f/.(k+1)) by A5,A6,A7,
TOPREAL1:def 3;
then
(GoB f)*(i+1,j+1) = f/.(k+1) & (GoB f)*(i,j+1) = f/.k or (GoB f)*(i+1,j
+1) = f/.k & (GoB f)* (i,j+1) = f/.(k+1) by SPPOL_1:8;
hence f/.k = (GoB f)*(i+1,j+1) by A15,A12,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i,j+1) by A17,A16,A12,SPPOL_1:8;
thus thesis by A17,A16,A12,SPPOL_1:8;
end;
theorem
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1
< len f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i
,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i+1,j) & f/.(k+1
) = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i,j+1)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: 1 <= k and
A6: k+1 < len f and
A7: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) and
A8: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1);
A9: 1 <= i+1 by NAT_1:11;
A10: j < j+1 by NAT_1:13;
A11: 1 <= j+1 by NAT_1:11;
i < len GoB f by A2,NAT_1:13;
then (GoB f)*(i,j+1)`2 = (GoB f)*(1,j+1)`2 by A1,A4,A11,GOBOARD5:1
.= (GoB f)*(i+1,j+1)`2 by A2,A4,A9,A11,GOBOARD5:1;
then
A12: (GoB f)*(i+1,j) <> (GoB f)*(i,j+1) by A2,A3,A4,A9,A10,GOBOARD5:4;
A13: 1 <= k+1 by NAT_1:11;
A14: k+(1+1) = k+1+1;
then k+2 <= len f by A6,NAT_1:13;
then
A15: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f/.(k+1),f/.(k+2)) by A8
,A14,A13,TOPREAL1:def 3;
then
A16: (GoB f)*(i,j+1) = f/.(k+2) & (GoB f)*(i+1,j+1) = f/.(k+1) or (GoB f)*(i
,j+1) = f/.(k+1) & (GoB f)*(i+1,j+1) = f/.(k+2) by SPPOL_1:8;
A17: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f/.k,f/.(k+1)) by A5,A6,A7,
TOPREAL1:def 3;
then
(GoB f)*(i+1,j+1) = f/.(k+1) & (GoB f)*(i+1,j) = f/.k or (GoB f)*(i+1,j
+1) = f/.k & (GoB f)* (i+1,j) = f/.(k+1) by SPPOL_1:8;
hence f/.k = (GoB f)*(i+1,j) by A15,A12,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i+1,j+1) by A17,A16,A12,SPPOL_1:8;
thus thesis by A17,A16,A12,SPPOL_1:8;
end;
theorem
1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f & 1 <= k & k+1 <
len f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f,k) & LSeg((GoB f)*(i,j),
(GoB f)*(i+1,j)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i+2,j) & f/.(k+1) = (GoB
f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j)
proof
assume that
A1: 1 <= i and
A2: i+1 < len GoB f and
A3: 1 <= j & j <= width GoB f and
A4: 1 <= k and
A5: k+1 < len f and
A6: LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f,k) and
A7: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k+1);
A8: i < i+2 by XREAL_1:29;
i+(1+1) = i+1+1;
then i+2 <= len GoB f by A2,NAT_1:13;
then
A9: (GoB f)*(i,j)`1 < (GoB f)*(i+2,j)`1 by A1,A3,A8,GOBOARD5:3;
A10: 1 <= k+1 by NAT_1:11;
A11: k+(1+1) = k+1+1;
then k+2 <= len f by A5,NAT_1:13;
then
A12: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f/.(k+1),f/.(k+2)) by A7,A11
,A10,TOPREAL1:def 3;
then
A13: (GoB f)*(i,j) = f/.(k+2) & (GoB f)*(i+1,j) = f/.(k+1) or (GoB f)*(i,j)
= f/.(k+1) & (GoB f)*(i+1,j) = f/.(k+2) by SPPOL_1:8;
A14: LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f/.k,f/.(k+1)) by A4,A5,A6,
TOPREAL1:def 3;
then
(GoB f)*(i+1,j) = f/.(k+1) & (GoB f)*(i+2,j) = f/.k or (GoB f)*(i+1,j) =
f/.k & (GoB f)*(i+2,j) = f/.(k+1) by SPPOL_1:8;
hence f/.k = (GoB f)*(i+2,j) by A12,A9,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i+1,j) by A14,A13,A9,SPPOL_1:8;
thus thesis by A14,A13,A9,SPPOL_1:8;
end;
theorem
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1
< len f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i
,j),(GoB f)*(i+1,j)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i+1,j+1) & f/.(k+1)
= (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: 1 <= k and
A6: k+1 < len f and
A7: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) and
A8: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k+1);
A9: i < len GoB f by A2,NAT_1:13;
A10: i < i+1 by NAT_1:13;
A11: 1 <= j+1 by NAT_1:11;
j < width GoB f by A4,NAT_1:13;
then (GoB f)*(i,j)`1 = (GoB f)*(i,1)`1 by A1,A3,A9,GOBOARD5:2
.= (GoB f)*(i,j+1)`1 by A1,A4,A11,A9,GOBOARD5:2;
then
A12: (GoB f)*(i,j) <> (GoB f)*(i+1,j+1) by A1,A2,A4,A11,A10,GOBOARD5:3;
A13: 1 <= k+1 by NAT_1:11;
A14: k+(1+1) = k+1+1;
then k+2 <= len f by A6,NAT_1:13;
then
A15: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f/.(k+1),f/.(k+2)) by A8,A14
,A13,TOPREAL1:def 3;
then
A16: (GoB f)*(i,j) = f/.(k+2) & (GoB f)*(i+1,j) = f/.(k+1) or (GoB f)*(i,j)
= f/.(k+1) & (GoB f)*(i+1,j) = f/.(k+2) by SPPOL_1:8;
A17: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f/.k,f/.(k+1)) by A5,A6,A7,
TOPREAL1:def 3;
then
(GoB f)*(i+1,j+1) = f/.(k+1) & (GoB f)*(i+1,j) = f/.k or (GoB f)*(i+1,j
+1) = f/.k & (GoB f)* (i+1,j) = f/.(k+1) by SPPOL_1:8;
hence f/.k = (GoB f)*(i+1,j+1) by A15,A12,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i+1,j) by A17,A16,A12,SPPOL_1:8;
thus thesis by A17,A16,A12,SPPOL_1:8;
end;
theorem
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1
< len f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i
,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i+1,j) & f/.(k+1
) = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i,j+1)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: 1 <= k and
A6: k+1 < len f and
A7: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) and
A8: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1);
A9: 1 <= j+1 by NAT_1:11;
A10: i < i+1 by NAT_1:13;
A11: 1 <= i+1 by NAT_1:11;
j < width GoB f by A4,NAT_1:13;
then (GoB f)*(i+1,j)`1 = (GoB f)*(i+1,1)`1 by A2,A3,A11,GOBOARD5:2
.= (GoB f)*(i+1,j+1)`1 by A2,A4,A9,A11,GOBOARD5:2;
then
A12: (GoB f)*(i,j+1) <> (GoB f)*(i+1,j) by A1,A2,A4,A9,A10,GOBOARD5:3;
A13: 1 <= k+1 by NAT_1:11;
A14: k+(1+1) = k+1+1;
then k+2 <= len f by A6,NAT_1:13;
then
A15: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f/.(k+1),f/.(k+2)) by A8
,A14,A13,TOPREAL1:def 3;
then
A16: (GoB f)*(i+1,j+1) = f/.(k+1) & (GoB f)*(i,j+1) = f/.(k+2) or (GoB f)*(i
+1,j+1) = f/.(k+2) & (GoB f)*(i,j+1) = f/.(k+1) by SPPOL_1:8;
A17: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f/.k,f/.(k+1)) by A5,A6,A7,
TOPREAL1:def 3;
then
(GoB f)*(i+1,j) = f/.k & (GoB f)*(i+1,j+1) = f/.(k+1) or (GoB f)*(i+1,j
) = f/.(k+1) & (GoB f)* (i+1,j+1) = f/.k by SPPOL_1:8;
hence f/.k = (GoB f)*(i+1,j) by A15,A12,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i+1,j+1) by A17,A16,A12,SPPOL_1:8;
thus thesis by A17,A16,A12,SPPOL_1:8;
end;
theorem
1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f & 1 <= k & k+1 <
len f & LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i,j+1),
(GoB f)*(i,j+2)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f
)*(i,j+1) & f/.(k+2) = (GoB f)*(i,j+2)
proof
assume that
A1: 1 <= i & i <= len GoB f & 1 <= j and
A2: j+1 < width GoB f and
A3: 1 <= k and
A4: k+1 < len f and
A5: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k) and
A6: LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f,k+1);
A7: 1 <= k+1 by NAT_1:11;
A8: k+(1+1) = k+1+1;
then k+2 <= len f by A4,NAT_1:13;
then
A9: LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f/.(k+1),f/.(k+2)) by A6,A8,A7
,TOPREAL1:def 3;
then
A10: (GoB f)*(i,j+1) = f/.(k+1) & (GoB f)*(i,j+2) = f/.(k+2) or (GoB f)*(i,j
+1) = f/.(k+2) & (GoB f)* (i,j+2) = f/.(k+1) by SPPOL_1:8;
A11: j < j+2 by XREAL_1:29;
j+(1+1) = j+1+1;
then j+2 <= width GoB f by A2,NAT_1:13;
then
A12: (GoB f)*(i,j)`2 < (GoB f)*(i,j+2)`2 by A1,A11,GOBOARD5:4;
A13: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f/.k,f/.(k+1)) by A3,A4,A5,
TOPREAL1:def 3;
then
(GoB f)*(i,j) = f/.k & (GoB f)*(i,j+1) = f/.(k+1) or (GoB f)*(i,j) = f/.
(k+1) & (GoB f)*(i,j+1) = f/.k by SPPOL_1:8;
hence f/.k = (GoB f)*(i,j) by A9,A12,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i,j+1) by A13,A10,A12,SPPOL_1:8;
thus thesis by A13,A10,A12,SPPOL_1:8;
end;
theorem
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1
< len f & LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i,j+1
),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j) & f/.(k+1) = (
GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j+1)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: 1 <= k and
A6: k+1 < len f and
A7: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k) and
A8: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1);
A9: j < width GoB f by A4,NAT_1:13;
A10: j < j+1 by NAT_1:13;
A11: 1 <= i+1 by NAT_1:11;
i < len GoB f by A2,NAT_1:13;
then (GoB f)*(i,j)`2 = (GoB f)*(1,j)`2 by A1,A3,A9,GOBOARD5:1
.= (GoB f)*(i+1,j)`2 by A2,A3,A11,A9,GOBOARD5:1;
then
A12: (GoB f)*(i,j) <> (GoB f)*(i+1,j+1) by A2,A3,A4,A11,A10,GOBOARD5:4;
A13: 1 <= k+1 by NAT_1:11;
A14: k+(1+1) = k+1+1;
then k+2 <= len f by A6,NAT_1:13;
then
A15: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f/.(k+1),f/.(k+2)) by A8
,A14,A13,TOPREAL1:def 3;
then
A16: (GoB f)*(i+1,j+1) = f/.(k+1) & (GoB f)*(i,j+1) = f/.(k+2) or (GoB f)*(i
+1,j+1) = f/.(k+2) & (GoB f)*(i,j+1) = f/.(k+1) by SPPOL_1:8;
A17: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f/.k,f/.(k+1)) by A5,A6,A7,
TOPREAL1:def 3;
then (GoB f)*(i,j) = f/.k & (GoB f)*(i,j+1) = f/.(k+1) or (GoB f)*(i,j) = f
/.(k+1) & (GoB f)*(i,j+1) = f/.k by SPPOL_1:8;
hence f/.k = (GoB f)*(i,j) by A15,A12,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i,j+1) by A17,A16,A12,SPPOL_1:8;
thus thesis by A17,A16,A12,SPPOL_1:8;
end;
theorem
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1
< len f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i
+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j+1) & f/.(k+1
) = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i+1,j)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: 1 <= k and
A6: k+1 < len f and
A7: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) and
A8: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1);
A9: 1 <= i+1 by NAT_1:11;
A10: j < j+1 by NAT_1:13;
A11: 1 <= j+1 by NAT_1:11;
i < len GoB f by A2,NAT_1:13;
then (GoB f)*(i,j+1)`2 = (GoB f)*(1,j+1)`2 by A1,A4,A11,GOBOARD5:1
.= (GoB f)*(i+1,j+1)`2 by A2,A4,A9,A11,GOBOARD5:1;
then
A12: (GoB f)*(i+1,j) <> (GoB f)*(i,j+1) by A2,A3,A4,A9,A10,GOBOARD5:4;
A13: 1 <= k+1 by NAT_1:11;
A14: k+(1+1) = k+1+1;
then k+2 <= len f by A6,NAT_1:13;
then
A15: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f/.(k+1),f/.(k+2)) by A8
,A14,A13,TOPREAL1:def 3;
then
A16: (GoB f)*(i+1,j+1) = f/.(k+1) & (GoB f)*(i+1,j) = f/.(k+2) or (GoB f)*(i
+1,j+1) = f/.(k+2) & (GoB f)*(i+1,j) = f/.(k+1) by SPPOL_1:8;
A17: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f/.k,f/.(k+1)) by A5,A6,A7,
TOPREAL1:def 3;
then
(GoB f)*(i,j+1) = f/.k & (GoB f)*(i+1,j+1) = f/.(k+1) or (GoB f)*(i,j+1
) = f/.(k+1) & (GoB f)* (i+1,j+1) = f/.k by SPPOL_1:8;
hence f/.k = (GoB f)*(i,j+1) by A15,A12,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i+1,j+1) by A17,A16,A12,SPPOL_1:8;
thus thesis by A17,A16,A12,SPPOL_1:8;
end;
theorem
1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f & 1 <= k & k+1 <
len f & LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k) & LSeg((GoB f)*(i+1,j),
(GoB f)*(i+2,j)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f
)*(i+1,j) & f/.(k+2) = (GoB f)*(i+2,j)
proof
assume that
A1: 1 <= i and
A2: i+1 < len GoB f and
A3: 1 <= j & j <= width GoB f and
A4: 1 <= k and
A5: k+1 < len f and
A6: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k) and
A7: LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f,k+1);
A8: i < i+2 by XREAL_1:29;
i+(1+1) = i+1+1;
then i+2 <= len GoB f by A2,NAT_1:13;
then
A9: (GoB f)*(i,j)`1 < (GoB f)*(i+2,j)`1 by A1,A3,A8,GOBOARD5:3;
A10: 1 <= k+1 by NAT_1:11;
A11: k+(1+1) = k+1+1;
then k+2 <= len f by A5,NAT_1:13;
then
A12: LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f/.(k+1),f/.(k+2)) by A7,A11
,A10,TOPREAL1:def 3;
then
A13: (GoB f)*(i+1,j) = f/.(k+1) & (GoB f)*(i+2,j) = f/.(k+2) or (GoB f)*(i+1
,j) = f/.(k+2) & (GoB f)* (i+2,j) = f/.(k+1) by SPPOL_1:8;
A14: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f/.k,f/.(k+1)) by A4,A5,A6,
TOPREAL1:def 3;
then
(GoB f)*(i,j) = f/.k & (GoB f)*(i+1,j) = f/.(k+1) or (GoB f)*(i,j) = f/.
(k+1) & (GoB f)*(i+1,j) = f/.k by SPPOL_1:8;
hence f/.k = (GoB f)*(i,j) by A12,A9,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i+1,j) by A14,A13,A9,SPPOL_1:8;
thus thesis by A14,A13,A9,SPPOL_1:8;
end;
theorem
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1
< len f & LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k) & LSeg((GoB f)*(i+1,j
),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j) & f/.(k+1) = (
GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i+1,j+1)
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: 1 <= k and
A6: k+1 < len f and
A7: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k) and
A8: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1);
A9: i < len GoB f by A2,NAT_1:13;
A10: i < i+1 by NAT_1:13;
A11: 1 <= j+1 by NAT_1:11;
j < width GoB f by A4,NAT_1:13;
then (GoB f)*(i,j)`1 = (GoB f)*(i,1)`1 by A1,A3,A9,GOBOARD5:2
.= (GoB f)*(i,j+1)`1 by A1,A4,A11,A9,GOBOARD5:2;
then
A12: (GoB f)*(i,j) <> (GoB f)*(i+1,j+1) by A1,A2,A4,A11,A10,GOBOARD5:3;
A13: 1 <= k+1 by NAT_1:11;
A14: k+(1+1) = k+1+1;
then k+2 <= len f by A6,NAT_1:13;
then
A15: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f/.(k+1),f/.(k+2)) by A8
,A14,A13,TOPREAL1:def 3;
then
A16: (GoB f)*(i+1,j+1) = f/.(k+1) & (GoB f)*(i+1,j) = f/.(k+2) or (GoB f)*(i
+1,j+1) = f/.(k+2) & (GoB f)*(i+1,j) = f/.(k+1) by SPPOL_1:8;
A17: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f/.k,f/.(k+1)) by A5,A6,A7,
TOPREAL1:def 3;
then (GoB f)*(i,j) = f/.k & (GoB f)*(i+1,j) = f/.(k+1) or (GoB f)*(i,j) = f
/.(k+1) & (GoB f)*(i+1,j) = f/.k by SPPOL_1:8;
hence f/.k = (GoB f)*(i,j) by A15,A12,SPPOL_1:8;
thus f/.(k+1) = (GoB f)*(i+1,j) by A17,A16,A12,SPPOL_1:8;
thus thesis by A17,A16,A12,SPPOL_1:8;
end;
theorem Th53:
1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f & LSeg((GoB
f)*(i,j),(GoB f)*(i,j+1)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) c= L~f
implies f/.1 = (GoB f)*(i,j+1) & (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f
)*(i,j+2) or f/.2 = (GoB f)*(i,j+2) & f/.(len f-'1) = (GoB f)*(i,j)) or ex k st
1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) & (f/.k = (GoB f)*(i,j) & f/.
(k+2) = (GoB f)*(i,j+2) or f/.k = (GoB f)*(i,j+2) & f/.(k+2) = (GoB f)*(i,j))
proof
assume that
A1: 1 <= i & i <= len GoB f and
A2: 1 <= j and
A3: j+1 < width GoB f and
A4: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f and
A5: LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) c= L~f;
A6: 1 <= j+1 by NAT_1:11;
1/2*((GoB f)*(i,j)+(GoB f)*(i,j+1)) in LSeg((GoB f)*(i,j),(GoB f)* (i,j
+1)) by RLTOPSP1:69;
then consider k1 such that
A7: 1 <= k1 and
A8: k1+1 <= len f and
A9: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k1) by A1,A2,A3,A4,Th39;
A10: k1 < len f by A8,NAT_1:13;
A11: now
assume k1 > 1;
then k1 >= 1+1 by NAT_1:13;
hence k1 = 2 or k1 > 2 by XXREAL_0:1;
end;
A12: j < width GoB f by A3,NAT_1:13;
A13: j+(1+1) = j+1+1;
then
A14: 1 <= j+2 by NAT_1:11;
A15: j+2 <= width GoB f by A3,A13,NAT_1:13;
1/2*((GoB f)*(i,j+1)+(GoB f)*(i,j+2)) in LSeg((GoB f)*(i,j+1),(GoB f)*(
i,j+2)) by RLTOPSP1:69;
then consider k2 such that
A16: 1 <= k2 and
A17: k2+1 <= len f and
A18: LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f,k2) by A1,A5,A6,A13,A15
,Th39;
A19: k2 < len f by A17,NAT_1:13;
A20: now
assume k2 > 1;
then k2 >= 1+1 by NAT_1:13;
hence k2 = 2 or k2 > 2 by XXREAL_0:1;
end;
A21: k1 = 1 or k1 > 1 by A7,XXREAL_0:1;
now
per cases by A16,A11,A20,A21,XXREAL_0:1;
case that
A22: k1 = 1 and
A23: k2 = 2;
A24: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A17,A23,TOPREAL1:def 3;
then
A25: (GoB f)*(i,j+1) = f/.2 & (GoB f)*(i,j+2) = f/.(2+1) or (GoB f)*(i,j
+1) = f/.(2+1) & (GoB f)*(i,j+2) = (f/.2) by A18,A23,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A17,A23,NAT_1:13;
A26: 3 < len f by Th34,XXREAL_0:2;
then
A27: f/.1 <> f/.3 by Th36;
A28: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A8,A22,TOPREAL1:def 3;
then
A29: (GoB f)*(i,j) = f/.1 & (GoB f)*(i,j+1) = (f/.2) or (GoB f)*(i,j) =
f/.2 & (GoB f)*(i,j+1) = f/.1 by A9,A22,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i,j+1) by A25,A26,Th36;
thus f/.1 = (GoB f)*(i,j) by A18,A23,A29,A24,A27,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i,j+2) by A9,A22,A28,A25,A27,SPPOL_1:8;
end;
case that
A30: k1 = 1 and
A31: k2 > 2;
A32: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A8,A30,TOPREAL1:def 3;
then
A33: (GoB f)*(i,j) = f/.1 & (GoB f)*(i,j+1) = f/.2 or (GoB f)*(i,j) = f
/.2 & (GoB f)*(i,j+1) = f/.1 by A9,A30,SPPOL_1:8;
A34: 2 < k2+1 by A31,NAT_1:13;
then
A35: f/.(k2+1) <> f/.2 by A17,Th37;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
A36: (GoB f)*(i,j+1) = f/.k2 & (GoB f)*(i,j+2) = f/.(k2+1) or (GoB f)*(i
,j+1) = f/.(k2+1) & (GoB f)*(i,j+2) = f/.k2 by A18,SPPOL_1:8;
A37: f/.k2 <> f/.2 by A19,A31,Th36;
hence f/.1 = (GoB f)*(i,j+1) by A9,A30,A32,A36,A35,SPPOL_1:8;
thus f/.2 = (GoB f)*(i,j) by A9,A30,A32,A36,A37,A35,SPPOL_1:8;
A38: k2 > 1 by A31,XXREAL_0:2;
then
A39: k2+1 > 1 by NAT_1:13;
then k2+1 = len f by A17,A19,A31,A33,A36,A38,A34,Th37,Th38;
then k2 + 1 = len f -'1 + 1 by A39,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i,j+2) by A19,A31,A33,A36,A38,Th36;
end;
case that
A40: k2 = 1 and
A41: k1 = 2;
A42: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A8,A41,TOPREAL1:def 3;
then
A43: (GoB f)*(i,j+1) = f/.2 & (GoB f)*(i,j) = f/.(2+1) or (GoB f)*(i,j+1
) = f/.(2+1) & (GoB f)*(i,j) = (f/.2) by A9,A41,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A8,A41,NAT_1:13;
A44: 3 < len f by Th34,XXREAL_0:2;
then
A45: f/.1 <> f/.3 by Th36;
A46: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A17,A40,TOPREAL1:def 3;
then
A47: (GoB f)*(i,j+2) = f/.1 & (GoB f)*(i,j+1) = f/.2 or (GoB f)*(i,j+2)
= f/.2 & (GoB f)*(i,j+1) = f/.1 by A18,A40,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i,j+1) by A43,A44,Th36;
thus f/.1 = (GoB f)*(i,j+2) by A9,A41,A47,A42,A45,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i,j) by A18,A40,A46,A43,A45,SPPOL_1:8;
end;
case that
A48: k2 = 1 and
A49: k1 > 2;
A50: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A17,A48,TOPREAL1:def 3;
then
A51: (GoB f)*(i,j+2) = f/.1 & (GoB f)*(i,j+1) = f/.2 or (GoB f)*(i,j+2)
= f/.2 & (GoB f)*(i,j+1) = f/.1 by A18,A48,SPPOL_1:8;
A52: 2 < k1+1 by A49,NAT_1:13;
then
A53: f/.(k1+1) <> f/.2 by A8,Th37;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A7,A8,TOPREAL1:def 3;
then
A54: (GoB f)*(i,j+1) = f/.k1 & (GoB f)*(i,j) = f/.(k1+1) or (GoB f)*(i,j
+1) = f/.(k1+1) & (GoB f)*(i,j) = f/.k1 by A9,SPPOL_1:8;
A55: f/.k1 <> f/.2 by A10,A49,Th36;
hence f/.1 = (GoB f)*(i,j+1) by A18,A48,A50,A54,A53,SPPOL_1:8;
thus f/.2 = (GoB f)*(i,j+2) by A18,A48,A50,A54,A55,A53,SPPOL_1:8;
A56: k1 > 1 by A49,XXREAL_0:2;
then
A57: k1+1 > 1 by NAT_1:13;
then k1+1 = len f by A8,A10,A49,A51,A54,A56,A52,Th37,Th38;
then k1 + 1 = len f -'1 + 1 by A57,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i,j) by A10,A49,A51,A54,A56,Th36;
end;
case
k1 = k2;
then
A58: (GoB f)*(i,j) = (GoB f)*(i,j+2) or (GoB f)*(i,j) = (GoB f)*(i, j+1)
by A9,A18,SPPOL_1:8;
A59: [i,j+2] in Indices GoB f by A1,A15,A14,MATRIX_0:30;
[i,j] in Indices GoB f & [i,j+1] in Indices GoB f by A1,A2,A3,A6,A12,
MATRIX_0:30;
then j = j+1 or j = j+2 by A58,A59,GOBOARD1:5;
hence contradiction;
end;
case that
A60: k1 > 1 and
A61: k2 > k1;
A62: 1 < k1+1 & k1+1 < k2+1 by A60,A61,NAT_1:13,XREAL_1:6;
A63: k1 < k2 + 1 by A61,NAT_1:13;
then
A64: f/.k1 <> f/.(k2+1) by A17,A60,Th37;
A65: k1+1 <= k2 by A61,NAT_1:13;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
A66: (GoB f)*(i,j+1) = f/.k2 & (GoB f)*(i,j+2) = f/.(k2+1) or (GoB f)*(i
,j+1) = f/.(k2+1) & (GoB f)*(i,j+2) = f/.k2 by A18,SPPOL_1:8;
A67: k2 < len f by A17,NAT_1:13;
then
A68: f/.k1 <> f/.k2 by A60,A61,Th37;
A69: LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A7,A8,TOPREAL1:def 3;
then
(GoB f)*(i,j) = f/.k1 & (GoB f)*(i,j+1) = f/.(k1+1) or (GoB f)*(i,j
) = f/.(k1+1) & (GoB f)*(i,j+1) = f/.k1 by A9,SPPOL_1:8;
then k1+1 >= k2 by A17,A60,A61,A66,A63,A67,A62,Th37;
then
A70: k1+1 = k2 by A65,XXREAL_0:1;
hence 1 <= k1 & k1+1 < len f by A17,A60,NAT_1:13;
thus f/.(k1+1) = (GoB f)*(i,j+1) by A9,A69,A66,A64,A68,SPPOL_1:8;
thus f/.k1 = (GoB f)*(i,j) by A9,A69,A66,A64,A68,SPPOL_1:8;
thus f/.(k1+2) = (GoB f)*(i,j+2) by A9,A69,A66,A64,A70,SPPOL_1:8;
end;
case that
A71: k2 > 1 and
A72: k1 > k2;
A73: 1 < k2+1 & k2+1 < k1+1 by A71,A72,NAT_1:13,XREAL_1:6;
A74: k2 < k1 + 1 by A72,NAT_1:13;
then
A75: f/.k2 <> f/.(k1+1) by A8,A71,Th37;
A76: k2+1 <= k1 by A72,NAT_1:13;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A7,A8,TOPREAL1:def 3;
then
A77: (GoB f)*(i,j+1) = f/.k1 & (GoB f)*(i,j) = f/.(k1+1) or (GoB f)*(i,j
+1) = f/.(k1+1) & (GoB f)*(i,j) = f/.k1 by A9,SPPOL_1:8;
A78: k1 < len f by A8,NAT_1:13;
then
A79: f/.k2 <> f/.k1 by A71,A72,Th37;
A80: LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
(GoB f)*(i,j+2) = f/.k2 & (GoB f)*(i,j+1) = f/.(k2+1) or (GoB f)*(i
,j+2) = f/.(k2+1) & (GoB f)*(i,j+1) = f/.k2 by A18,SPPOL_1:8;
then k2+1 >= k1 by A8,A71,A72,A77,A74,A78,A73,Th37;
then
A81: k2+1 = k1 by A76,XXREAL_0:1;
hence 1 <= k2 & k2+1 < len f by A8,A71,NAT_1:13;
thus f/.(k2+1) = (GoB f)*(i,j+1) by A18,A80,A77,A75,A79,SPPOL_1:8;
thus f/.k2 = (GoB f)*(i,j+2) by A18,A80,A77,A75,A79,SPPOL_1:8;
thus f/.(k2+2) = (GoB f)*(i,j) by A18,A80,A77,A75,A81,SPPOL_1:8;
end;
end;
hence thesis;
end;
theorem Th54:
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & LSeg((
GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1))
c= L~f implies f/.1 = (GoB f)*(i,j+1) & (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) =
(GoB f)*(i+1,j+1) or f/.2 = (GoB f)*(i+1,j+1) & f/.(len f-'1) = (GoB f)*(i,j))
or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) & (f/.k = (GoB f)*
(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or f/.k = (GoB f)*(i+1,j+1) & f/.(k+2) = (
GoB f)*(i,j))
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f and
A6: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f;
A7: i < len GoB f by A2,NAT_1:13;
A8: j < width GoB f by A4,NAT_1:13;
A9: 1 <= i+1 by NAT_1:11;
1/2*((GoB f)*(i,j)+(GoB f)*(i,j+1)) in LSeg((GoB f)*(i,j),(GoB f)* (i,j
+1)) by RLTOPSP1:69;
then consider k1 such that
A10: 1 <= k1 and
A11: k1+1 <= len f and
A12: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k1) by A1,A3,A4,A5,A7,Th39;
A13: k1 < len f by A11,NAT_1:13;
A14: now
assume k1 > 1;
then k1 >= 1+1 by NAT_1:13;
hence k1 = 2 or k1 > 2 by XXREAL_0:1;
end;
A15: 1 <= j+1 by NAT_1:11;
1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) in LSeg((GoB f)*(i,j+1),(GoB f)
*(i+1,j+1)) by RLTOPSP1:69;
then consider k2 such that
A16: 1 <= k2 and
A17: k2+1 <= len f and
A18: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k2) by A1,A2,A4,A6,A15
,Th40;
A19: k2 < len f by A17,NAT_1:13;
A20: now
assume k2 > 1;
then k2 >= 1+1 by NAT_1:13;
hence k2 = 2 or k2 > 2 by XXREAL_0:1;
end;
A21: k1 = 1 or k1 > 1 by A10,XXREAL_0:1;
now
per cases by A16,A14,A20,A21,XXREAL_0:1;
case that
A22: k1 = 1 and
A23: k2 = 2;
A24: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A17,A23,TOPREAL1:def 3;
then
A25: (GoB f)*(i,j+1) = f/.2 & (GoB f)*(i+1,j+1) = f/.(2+1) or (GoB f)*(i
,j+1) = f/.(2+1) & (GoB f)*(i+1,j+1) = (f/.2) by A18,A23,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A17,A23,NAT_1:13;
A26: 3 < len f by Th34,XXREAL_0:2;
then
A27: f/.1 <> f/.3 by Th36;
A28: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A11,A22,TOPREAL1:def 3;
then
A29: (GoB f)*(i,j) = f/.1 & (GoB f)*(i,j+1) = f/.2 or (GoB f)*(i,j) = f
/.2 & (GoB f)*(i,j+1) = f/.1 by A12,A22,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i,j+1) by A25,A26,Th36;
thus f/.1 = (GoB f)*(i,j) by A18,A23,A29,A24,A27,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i+1,j+1) by A12,A22,A28,A25,A27,SPPOL_1:8;
end;
case that
A30: k1 = 1 and
A31: k2 > 2;
A32: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A11,A30,TOPREAL1:def 3;
then
A33: (GoB f)*(i,j) = f/.1 & (GoB f)*(i,j+1) = f/.2 or (GoB f)*(i,j) = f
/.2 & (GoB f)*(i,j+1) = f/.1 by A12,A30,SPPOL_1:8;
A34: 2 < k2+1 by A31,NAT_1:13;
then
A35: f/.(k2+1) <> f/.2 by A17,Th37;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
A36: (GoB f)*(i,j+1) = f/.k2 & (GoB f)*(i+1,j+1) = f/.(k2+1) or (GoB f)*
(i,j+1) = f/.(k2+1) & (GoB f)*(i+1,j+1) = f/.k2 by A18,SPPOL_1:8;
A37: f/.k2 <> f/.2 by A19,A31,Th36;
hence f/.1 = (GoB f)*(i,j+1) by A12,A30,A32,A36,A35,SPPOL_1:8;
thus f/.2 = (GoB f)*(i,j) by A12,A30,A32,A36,A37,A35,SPPOL_1:8;
A38: k2 > 1 by A31,XXREAL_0:2;
then
A39: k2+1 > 1 by NAT_1:13;
then k2+1 = len f by A17,A19,A31,A33,A36,A38,A34,Th37,Th38;
then k2 + 1 = len f -'1 + 1 by A39,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i+1,j+1) by A19,A31,A33,A36,A38,Th36;
end;
case that
A40: k2 = 1 and
A41: k1 = 2;
A42: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A11,A41,TOPREAL1:def 3;
then
A43: (GoB f)*(i,j+1) = f/.2 & (GoB f)*(i,j) = f/.(2+1) or (GoB f)*(i,j+1
) = f/.(2+1) & (GoB f)*(i,j) = (f/.2) by A12,A41,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A11,A41,NAT_1:13;
A44: 3 < len f by Th34,XXREAL_0:2;
then
A45: f/.1 <> f/.3 by Th36;
A46: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A17,A40,TOPREAL1:def 3;
then
A47: (GoB f)*(i+1,j+1) = f/.1 & (GoB f)*(i,j+1) = f/.2 or (GoB f)*(i+1,j
+1) = f/.2 & (GoB f)*(i,j+1) = f/.1 by A18,A40,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i,j+1) by A43,A44,Th36;
thus f/.1 = (GoB f)*(i+1,j+1) by A12,A41,A47,A42,A45,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i,j) by A18,A40,A46,A43,A45,SPPOL_1:8;
end;
case that
A48: k2 = 1 and
A49: k1 > 2;
A50: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A17,A48,TOPREAL1:def 3;
then
A51: (GoB f)*(i+1,j+1) = f/.1 & (GoB f)*(i,j+1) = f/.2 or (GoB f)*(i+1,j
+1) = f/.2 & (GoB f)*(i,j+1) = f/.1 by A18,A48,SPPOL_1:8;
A52: 2 < k1+1 by A49,NAT_1:13;
then
A53: f/.(k1+1) <> f/.2 by A11,Th37;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A10,A11,TOPREAL1:def 3;
then
A54: (GoB f)*(i,j+1) = f/.k1 & (GoB f)*(i,j) = f/.(k1+1) or (GoB f)*(i,j
+1) = f/.(k1+1) & (GoB f)*(i,j) = f/.k1 by A12,SPPOL_1:8;
A55: f/.k1 <> f/.2 by A13,A49,Th36;
hence f/.1 = (GoB f)*(i,j+1) by A18,A48,A50,A54,A53,SPPOL_1:8;
thus f/.2 = (GoB f)*(i+1,j+1) by A18,A48,A50,A54,A55,A53,SPPOL_1:8;
A56: k1 > 1 by A49,XXREAL_0:2;
then
A57: k1+1 > 1 by NAT_1:13;
then k1+1 = len f by A11,A13,A49,A51,A54,A56,A52,Th37,Th38;
then k1 + 1 = len f -'1 + 1 by A57,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i,j) by A13,A49,A51,A54,A56,Th36;
end;
case
k1 = k2;
then
A58: (GoB f)*(i,j) = (GoB f)*(i+1,j+1) or (GoB f)*(i,j) = (GoB f)*( i,j+
1) by A12,A18,SPPOL_1:8;
A59: [i+1,j+1] in Indices GoB f by A2,A4,A15,A9,MATRIX_0:30;
[i,j] in Indices GoB f & [i,j+1] in Indices GoB f by A1,A3,A4,A15,A8,A7,
MATRIX_0:30;
then j = j+1 by A58,A59,GOBOARD1:5;
hence contradiction;
end;
case that
A60: k1 > 1 and
A61: k2 > k1;
A62: 1 < k1+1 & k1+1 < k2+1 by A60,A61,NAT_1:13,XREAL_1:6;
A63: k1 < k2 + 1 by A61,NAT_1:13;
then
A64: f/.k1 <> f/.(k2+1) by A17,A60,Th37;
A65: k1+1 <= k2 by A61,NAT_1:13;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
A66: (GoB f)*(i,j+1) = f/.k2 & (GoB f)*(i+1,j+1) = f/.(k2+1) or (GoB f)*
(i,j+1) = f/.(k2+1) & (GoB f)*(i+1,j+1) = f/.k2 by A18,SPPOL_1:8;
A67: k2 < len f by A17,NAT_1:13;
then
A68: f/.k1 <> f/.k2 by A60,A61,Th37;
A69: LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A10,A11,TOPREAL1:def 3;
then
(GoB f)*(i,j) = f/.k1 & (GoB f)*(i,j+1) = f/.(k1+1) or (GoB f)*(i,j
) = f/.(k1+1) & (GoB f)*(i,j+1) = f/.k1 by A12,SPPOL_1:8;
then k1+1 >= k2 by A17,A60,A61,A66,A63,A67,A62,Th37;
then
A70: k1+1 = k2 by A65,XXREAL_0:1;
hence 1 <= k1 & k1+1 < len f by A17,A60,NAT_1:13;
thus f/.(k1+1) = (GoB f)*(i,j+1) by A12,A69,A66,A64,A68,SPPOL_1:8;
thus f/.k1 = (GoB f)*(i,j) by A12,A69,A66,A64,A68,SPPOL_1:8;
thus f/.(k1+2) = (GoB f)*(i+1,j+1) by A12,A69,A66,A64,A70,SPPOL_1:8;
end;
case that
A71: k2 > 1 and
A72: k1 > k2;
A73: 1 < k2+1 & k2+1 < k1+1 by A71,A72,NAT_1:13,XREAL_1:6;
A74: k2 < k1 + 1 by A72,NAT_1:13;
then
A75: f/.k2 <> f/.(k1+1) by A11,A71,Th37;
A76: k2+1 <= k1 by A72,NAT_1:13;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A10,A11,TOPREAL1:def 3;
then
A77: (GoB f)*(i,j+1) = f/.k1 & (GoB f)*(i,j) = f/.(k1+1) or (GoB f)*(i,j
+1) = f/.(k1+1) & (GoB f)*(i,j) = f/.k1 by A12,SPPOL_1:8;
A78: k1 < len f by A11,NAT_1:13;
then
A79: f/.k2 <> f/.k1 by A71,A72,Th37;
A80: LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
(GoB f)*(i+1,j+1) = f/.k2 & (GoB f)*(i,j+1) = f/.(k2+1) or (GoB f)*
(i+1,j+1) = f/.(k2+1) & (GoB f)*(i,j+1) = f/.k2 by A18,SPPOL_1:8;
then k2+1 >= k1 by A11,A71,A72,A77,A74,A78,A73,Th37;
then
A81: k2+1 = k1 by A76,XXREAL_0:1;
hence 1 <= k2 & k2+1 < len f by A11,A71,NAT_1:13;
thus f/.(k2+1) = (GoB f)*(i,j+1) by A18,A80,A77,A75,A79,SPPOL_1:8;
thus f/.k2 = (GoB f)*(i+1,j+1) by A18,A80,A77,A75,A79,SPPOL_1:8;
thus f/.(k2+2) = (GoB f)*(i,j) by A18,A80,A77,A75,A81,SPPOL_1:8;
end;
end;
hence thesis;
end;
theorem Th55:
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & LSeg((
GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f & LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+1,
j)) c= L~f implies f/.1 = (GoB f)*(i+1,j+1) & (f/.2 = (GoB f)*(i,j+1) & f/.(len
f-'1) = (GoB f)*(i+1,j) or f/.2 = (GoB f)*(i+1,j) & f/.(len f-'1) = (GoB f)*(i,
j+1)) or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k =
(GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or f/.k = (GoB f)*(i+1,j) & f/.(k+
2) = (GoB f)*(i,j+1))
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f and
A6: LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+1,j)) c= L~f;
A7: 1 <= j+1 by NAT_1:11;
1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) in LSeg((GoB f)*(i,j+1),(GoB f)
*(i+1,j+1)) by RLTOPSP1:69;
then consider k1 such that
A8: 1 <= k1 and
A9: k1+1 <= len f and
A10: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k1) by A1,A2,A4,A5,A7
,Th40;
A11: k1 < len f by A9,NAT_1:13;
A12: now
assume k1 > 1;
then k1 >= 1+1 by NAT_1:13;
hence k1 = 2 or k1 > 2 by XXREAL_0:1;
end;
A13: j < width GoB f & i < len GoB f by A2,A4,NAT_1:13;
A14: 1 <= i+1 by NAT_1:11;
1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) in LSeg((GoB f)*(i+1,j+1),(GoB
f)*(i+1,j)) by RLTOPSP1:69;
then consider k2 such that
A15: 1 <= k2 and
A16: k2+1 <= len f and
A17: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k2) by A2,A3,A4,A6,A14
,Th39;
A18: k2 < len f by A16,NAT_1:13;
A19: now
assume k2 > 1;
then k2 >= 1+1 by NAT_1:13;
hence k2 = 2 or k2 > 2 by XXREAL_0:1;
end;
A20: k1 = 1 or k1 > 1 by A8,XXREAL_0:1;
now
per cases by A15,A12,A19,A20,XXREAL_0:1;
case that
A21: k1 = 1 and
A22: k2 = 2;
A23: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A16,A22,TOPREAL1:def 3;
then
A24: (GoB f)*(i+1,j+1) = f/.2 & (GoB f)*(i+1,j) = f/.(2+1) or (GoB f)*(i
+1,j+1) = f/.(2+1) & (GoB f)*(i+1,j) = (f/.2) by A17,A22,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A16,A22,NAT_1:13;
A25: 3 < len f by Th34,XXREAL_0:2;
then
A26: f/.1 <> f/.3 by Th36;
A27: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A9,A21,TOPREAL1:def 3;
then
A28: (GoB f)*(i,j+1) = f/.1 & (GoB f)*(i+1,j+1) = f/.2 or (GoB f)*(i,j+1
) = f/.2 & (GoB f)*(i+1,j+1) = f/.1 by A10,A21,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i+1,j+1) by A24,A25,Th36;
thus f/.1 = (GoB f)*(i,j+1) by A17,A22,A28,A23,A26,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i+1,j) by A10,A21,A27,A24,A26,SPPOL_1:8;
end;
case that
A29: k1 = 1 and
A30: k2 > 2;
A31: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A9,A29,TOPREAL1:def 3;
then
A32: (GoB f)*(i,j+1) = f/.1 & (GoB f)*(i+1,j+1) = f/.2 or (GoB f)*(i,j+1
) = f/.2 & (GoB f)*(i+1,j+1) = f/.1 by A10,A29,SPPOL_1:8;
A33: 2 < k2+1 by A30,NAT_1:13;
then
A34: f/.(k2+1) <> f/.2 by A16,Th37;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A15,A16,TOPREAL1:def 3;
then
A35: (GoB f)*(i+1,j+1) = f/.k2 & (GoB f)*(i+1,j) = f/.(k2+1) or (GoB f)*
(i+1,j+1) = f/.(k2+1) & (GoB f)*(i+1,j) = f/.k2 by A17,SPPOL_1:8;
A36: f/.k2 <> f/.2 by A18,A30,Th36;
hence f/.1 = (GoB f)*(i+1,j+1) by A10,A29,A31,A35,A34,SPPOL_1:8;
thus f/.2 = (GoB f)*(i,j+1) by A10,A29,A31,A35,A36,A34,SPPOL_1:8;
A37: k2 > 1 by A30,XXREAL_0:2;
then
A38: k2+1 > 1 by NAT_1:13;
then k2+1 = len f by A16,A18,A30,A32,A35,A37,A33,Th37,Th38;
then k2 + 1 = len f -'1 + 1 by A38,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i+1,j) by A18,A30,A32,A35,A37,Th36;
end;
case that
A39: k2 = 1 and
A40: k1 = 2;
A41: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A9,A40,TOPREAL1:def 3;
then
A42: (GoB f)*(i+1,j+1) = f/.2 & (GoB f)*(i,j+1) = f/.(2+1) or (GoB f)*(i
+1,j+1) = f/.(2+1) & (GoB f)*(i,j+1) = (f/.2) by A10,A40,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A9,A40,NAT_1:13;
A43: 3 < len f by Th34,XXREAL_0:2;
then
A44: f/.1 <> f/.3 by Th36;
A45: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A16,A39,TOPREAL1:def 3;
then
A46: (GoB f)*(i+1,j) = f/.1 & (GoB f)*(i+1,j+1) = f/.2 or (GoB f)*(i+1,j
) = f/.2 & (GoB f)*(i+1,j+1) = f/.1 by A17,A39,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i+1,j+1) by A42,A43,Th36;
thus f/.1 = (GoB f)*(i+1,j) by A10,A40,A46,A41,A44,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i,j+1) by A17,A39,A45,A42,A44,SPPOL_1:8;
end;
case that
A47: k2 = 1 and
A48: k1 > 2;
A49: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A16,A47,TOPREAL1:def 3;
then
A50: (GoB f)*(i+1,j) = f/.1 & (GoB f)*(i+1,j+1) = f/.2 or (GoB f)*(i+1,j
) = f/.2 & (GoB f)*(i+1,j+1) = f/.1 by A17,A47,SPPOL_1:8;
A51: 2 < k1+1 by A48,NAT_1:13;
then
A52: f/.(k1+1) <> f/.2 by A9,Th37;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A8,A9,TOPREAL1:def 3;
then
A53: (GoB f)*(i+1,j+1) = f/.k1 & (GoB f)*(i,j+1) = f/.(k1+1) or (GoB f)*
(i+1,j+1) = f/.(k1+1) & (GoB f)*(i,j+1) = f/.k1 by A10,SPPOL_1:8;
A54: f/.k1 <> f/.2 by A11,A48,Th36;
hence f/.1 = (GoB f)*(i+1,j+1) by A17,A47,A49,A53,A52,SPPOL_1:8;
thus f/.2 = (GoB f)*(i+1,j) by A17,A47,A49,A53,A54,A52,SPPOL_1:8;
A55: k1 > 1 by A48,XXREAL_0:2;
then
A56: k1+1 > 1 by NAT_1:13;
then k1+1 = len f by A9,A11,A48,A50,A53,A55,A51,Th37,Th38;
then k1 + 1 = len f -'1 + 1 by A56,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i,j+1) by A11,A48,A50,A53,A55,Th36;
end;
case
k1 = k2;
then
A57: (GoB f)*(i,j+1) = (GoB f)*(i+1,j) or (GoB f)*(i,j+1) = (GoB f) * (i
+1,j+1) by A10,A17,SPPOL_1:8;
A58: [i+1,j+1] in Indices GoB f by A2,A4,A7,A14,MATRIX_0:30;
[i+1,j] in Indices GoB f & [i,j+1] in Indices GoB f by A1,A2,A3,A4,A7,A14
,A13,MATRIX_0:30;
then i = i+1 or j = j+1 by A57,A58,GOBOARD1:5;
hence contradiction;
end;
case that
A59: k1 > 1 and
A60: k2 > k1;
A61: 1 < k1+1 & k1+1 < k2+1 by A59,A60,NAT_1:13,XREAL_1:6;
A62: k1 < k2 + 1 by A60,NAT_1:13;
then
A63: f/.k1 <> f/.(k2+1) by A16,A59,Th37;
A64: k1+1 <= k2 by A60,NAT_1:13;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A15,A16,TOPREAL1:def 3;
then
A65: (GoB f)*(i+1,j+1) = f/.k2 & (GoB f)*(i+1,j) = f/.(k2+1) or (GoB f)*
(i+1,j+1) = f/.(k2+1) & (GoB f)*(i+1,j) = f/.k2 by A17,SPPOL_1:8;
A66: k2 < len f by A16,NAT_1:13;
then
A67: f/.k1 <> f/.k2 by A59,A60,Th37;
A68: LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A8,A9,TOPREAL1:def 3;
then
(GoB f)*(i,j+1) = f/.k1 & (GoB f)*(i+1,j+1) = f/.(k1+1) or (GoB f)*
(i,j+1) = f/.(k1+1) & (GoB f)*(i+1,j+1) = f/.k1 by A10,SPPOL_1:8;
then k1+1 >= k2 by A16,A59,A60,A65,A62,A66,A61,Th37;
then
A69: k1+1 = k2 by A64,XXREAL_0:1;
hence 1 <= k1 & k1+1 < len f by A16,A59,NAT_1:13;
thus f/.(k1+1) = (GoB f)*(i+1,j+1) by A10,A68,A65,A63,A67,SPPOL_1:8;
thus f/.k1 = (GoB f)*(i,j+1) by A10,A68,A65,A63,A67,SPPOL_1:8;
thus f/.(k1+2) = (GoB f)*(i+1,j) by A10,A68,A65,A63,A69,SPPOL_1:8;
end;
case that
A70: k2 > 1 and
A71: k1 > k2;
A72: 1 < k2+1 & k2+1 < k1+1 by A70,A71,NAT_1:13,XREAL_1:6;
A73: k2 < k1 + 1 by A71,NAT_1:13;
then
A74: f/.k2 <> f/.(k1+1) by A9,A70,Th37;
A75: k2+1 <= k1 by A71,NAT_1:13;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A8,A9,TOPREAL1:def 3;
then
A76: (GoB f)*(i+1,j+1) = f/.k1 & (GoB f)*(i,j+1) = f/.(k1+1) or (GoB f)*
(i+1,j+1) = f/.(k1+1) & (GoB f)*(i,j+1) = f/.k1 by A10,SPPOL_1:8;
A77: k1 < len f by A9,NAT_1:13;
then
A78: f/.k2 <> f/.k1 by A70,A71,Th37;
A79: LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A15,A16,TOPREAL1:def 3;
then
(GoB f)*(i+1,j) = f/.k2 & (GoB f)*(i+1,j+1) = f/.(k2+1) or (GoB f)*
(i+1,j) = f/.(k2+1) & (GoB f)*(i+1,j+1) = f/.k2 by A17,SPPOL_1:8;
then k2+1 >= k1 by A9,A70,A71,A76,A73,A77,A72,Th37;
then
A80: k2+1 = k1 by A75,XXREAL_0:1;
hence 1 <= k2 & k2+1 < len f by A9,A70,NAT_1:13;
thus f/.(k2+1) = (GoB f)*(i+1,j+1) by A17,A79,A76,A74,A78,SPPOL_1:8;
thus f/.k2 = (GoB f)*(i+1,j) by A17,A79,A76,A74,A78,SPPOL_1:8;
thus f/.(k2+2) = (GoB f)*(i,j+1) by A17,A79,A76,A74,A80,SPPOL_1:8;
end;
end;
hence thesis;
end;
theorem Th56:
1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f & LSeg((GoB
f)*(i,j),(GoB f)*(i+1,j)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) c= L~f
implies f/.1 = (GoB f)*(i+1,j) & (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f
)*(i+2,j) or f/.2 = (GoB f)*(i+2,j) & f/.(len f-'1) = (GoB f)*(i,j)) or ex k st
1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) & (f/.k = (GoB f)*(i,j) & f/.
(k+2) = (GoB f)*(i+2,j) or f/.k = (GoB f)*(i+2,j) & f/.(k+2) = (GoB f)*(i,j))
proof
assume that
A1: 1 <= i and
A2: i+1 < len GoB f and
A3: 1 <= j & j <= width GoB f and
A4: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f and
A5: LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) c= L~f;
A6: 1 <= i+1 by NAT_1:11;
1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j)) in LSeg((GoB f)*(i,j),(GoB f)* (i+1
,j)) by RLTOPSP1:69;
then consider k1 such that
A7: 1 <= k1 and
A8: k1+1 <= len f and
A9: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k1) by A1,A2,A3,A4,Th40;
A10: k1 < len f by A8,NAT_1:13;
A11: now
assume k1 > 1;
then k1 >= 1+1 by NAT_1:13;
hence k1 = 2 or k1 > 2 by XXREAL_0:1;
end;
A12: i < len GoB f by A2,NAT_1:13;
A13: i+(1+1) = i+1+1;
then
A14: 1 <= i+2 by NAT_1:11;
A15: i+2 <= len GoB f by A2,A13,NAT_1:13;
1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j)) in LSeg((GoB f)*(i+1,j),(GoB f)*(
i+2,j)) by RLTOPSP1:69;
then consider k2 such that
A16: 1 <= k2 and
A17: k2+1 <= len f and
A18: LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f,k2) by A3,A5,A6,A13,A15
,Th40;
A19: k2 < len f by A17,NAT_1:13;
A20: now
assume k2 > 1;
then k2 >= 1+1 by NAT_1:13;
hence k2 = 2 or k2 > 2 by XXREAL_0:1;
end;
A21: k1 = 1 or k1 > 1 by A7,XXREAL_0:1;
now
per cases by A16,A11,A20,A21,XXREAL_0:1;
case that
A22: k1 = 1 and
A23: k2 = 2;
A24: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A17,A23,TOPREAL1:def 3;
then
A25: (GoB f)*(i+1,j) = f/.2 & (GoB f)*(i+2,j) = f/.(2+1) or (GoB f)*(i+1
,j) = f/.(2+1) & (GoB f)*(i+2,j) = (f/.2) by A18,A23,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A17,A23,NAT_1:13;
A26: 3 < len f by Th34,XXREAL_0:2;
then
A27: f/.1 <> f/.3 by Th36;
A28: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A8,A22,TOPREAL1:def 3;
then
A29: (GoB f)*(i,j) = f/.1 & (GoB f)*(i+1,j) = f/.2 or (GoB f)*(i,j) = f
/.2 & (GoB f)*(i+1,j) = f/.1 by A9,A22,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i+1,j) by A25,A26,Th36;
thus f/.1 = (GoB f)*(i,j) by A18,A23,A29,A24,A27,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i+2,j) by A9,A22,A28,A25,A27,SPPOL_1:8;
end;
case that
A30: k1 = 1 and
A31: k2 > 2;
A32: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A8,A30,TOPREAL1:def 3;
then
A33: (GoB f)*(i,j) = f/.1 & (GoB f)*(i+1,j) = f/.2 or (GoB f)*(i,j) = f
/.2 & (GoB f)*(i+1,j) = f/.1 by A9,A30,SPPOL_1:8;
A34: 2 < k2+1 by A31,NAT_1:13;
then
A35: f/.(k2+1) <> f/.2 by A17,Th37;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
A36: (GoB f)*(i+1,j) = f/.k2 & (GoB f)*(i+2,j) = f/.(k2+1) or (GoB f)*(i
+1,j) = f/.(k2+1) & (GoB f)*(i+2,j) = f/.k2 by A18,SPPOL_1:8;
A37: f/.k2 <> f/.2 by A19,A31,Th36;
hence f/.1 = (GoB f)*(i+1,j) by A9,A30,A32,A36,A35,SPPOL_1:8;
thus f/.2 = (GoB f)*(i,j) by A9,A30,A32,A36,A37,A35,SPPOL_1:8;
A38: k2 > 1 by A31,XXREAL_0:2;
then
A39: k2+1 > 1 by NAT_1:13;
then k2+1 = len f by A17,A19,A31,A33,A36,A38,A34,Th37,Th38;
then k2 + 1 = len f -'1 + 1 by A39,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i+2,j) by A19,A31,A33,A36,A38,Th36;
end;
case that
A40: k2 = 1 and
A41: k1 = 2;
A42: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A8,A41,TOPREAL1:def 3;
then
A43: (GoB f)*(i+1,j) = f/.2 & (GoB f)*(i,j) = f/.(2+1) or (GoB f)*(i+1,j
) = f/.(2+1) & (GoB f)*(i,j) = (f/.2) by A9,A41,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A8,A41,NAT_1:13;
A44: 3 < len f by Th34,XXREAL_0:2;
then
A45: f/.1 <> f/.3 by Th36;
A46: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A17,A40,TOPREAL1:def 3;
then
A47: (GoB f)*(i+2,j) = f/.1 & (GoB f)*(i+1,j) = f/.2 or (GoB f)*(i+2,j)
= f/.2 & (GoB f)*(i+1,j) = f/.1 by A18,A40,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i+1,j) by A43,A44,Th36;
thus f/.1 = (GoB f)*(i+2,j) by A9,A41,A47,A42,A45,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i,j) by A18,A40,A46,A43,A45,SPPOL_1:8;
end;
case that
A48: k2 = 1 and
A49: k1 > 2;
A50: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A17,A48,TOPREAL1:def 3;
then
A51: (GoB f)*(i+2,j) = f/.1 & (GoB f)*(i+1,j) = f/.2 or (GoB f)*(i+2,j)
= f/.2 & (GoB f)*(i+1,j) = f/.1 by A18,A48,SPPOL_1:8;
A52: 2 < k1+1 by A49,NAT_1:13;
then
A53: f/.(k1+1) <> f/.2 by A8,Th37;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A7,A8,TOPREAL1:def 3;
then
A54: (GoB f)*(i+1,j) = f/.k1 & (GoB f)*(i,j) = f/.(k1+1) or (GoB f)*(i+1
,j) = f/.(k1+1) & (GoB f)*(i,j) = f/.k1 by A9,SPPOL_1:8;
A55: f/.k1 <> f/.2 by A10,A49,Th36;
hence f/.1 = (GoB f)*(i+1,j) by A18,A48,A50,A54,A53,SPPOL_1:8;
thus f/.2 = (GoB f)*(i+2,j) by A18,A48,A50,A54,A55,A53,SPPOL_1:8;
A56: k1 > 1 by A49,XXREAL_0:2;
then
A57: k1+1 > 1 by NAT_1:13;
then k1+1 = len f by A8,A10,A49,A51,A54,A56,A52,Th37,Th38;
then k1 + 1 = len f -'1 + 1 by A57,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i,j) by A10,A49,A51,A54,A56,Th36;
end;
case
k1 = k2;
then
A58: (GoB f)*(i,j) = (GoB f)*(i+2,j) or (GoB f)*(i,j) = (GoB f)*(i+ 1,j)
by A9,A18,SPPOL_1:8;
A59: [i+2,j] in Indices GoB f by A3,A15,A14,MATRIX_0:30;
[i,j] in Indices GoB f & [i+1,j] in Indices GoB f by A1,A2,A3,A6,A12,
MATRIX_0:30;
then i = i+1 or i = i+2 by A58,A59,GOBOARD1:5;
hence contradiction;
end;
case that
A60: k1 > 1 and
A61: k2 > k1;
A62: 1 < k1+1 & k1+1 < k2+1 by A60,A61,NAT_1:13,XREAL_1:6;
A63: k1 < k2 + 1 by A61,NAT_1:13;
then
A64: f/.k1 <> f/.(k2+1) by A17,A60,Th37;
A65: k1+1 <= k2 by A61,NAT_1:13;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
A66: (GoB f)*(i+1,j) = f/.k2 & (GoB f)*(i+2,j) = f/.(k2+1) or (GoB f)*(i
+1,j) = f/.(k2+1) & (GoB f)*(i+2,j) = f/.k2 by A18,SPPOL_1:8;
A67: k2 < len f by A17,NAT_1:13;
then
A68: f/.k1 <> f/.k2 by A60,A61,Th37;
A69: LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A7,A8,TOPREAL1:def 3;
then
(GoB f)*(i,j) = f/.k1 & (GoB f)*(i+1,j) = f/.(k1+1) or (GoB f)*(i,j
) = f/.(k1+1) & (GoB f)*(i+1,j) = f/.k1 by A9,SPPOL_1:8;
then k1+1 >= k2 by A17,A60,A61,A66,A63,A67,A62,Th37;
then
A70: k1+1 = k2 by A65,XXREAL_0:1;
hence 1 <= k1 & k1+1 < len f by A17,A60,NAT_1:13;
thus f/.(k1+1) = (GoB f)*(i+1,j) by A9,A69,A66,A64,A68,SPPOL_1:8;
thus f/.k1 = (GoB f)*(i,j) by A9,A69,A66,A64,A68,SPPOL_1:8;
thus f/.(k1+2) = (GoB f)*(i+2,j) by A9,A69,A66,A64,A70,SPPOL_1:8;
end;
case that
A71: k2 > 1 and
A72: k1 > k2;
A73: 1 < k2+1 & k2+1 < k1+1 by A71,A72,NAT_1:13,XREAL_1:6;
A74: k2 < k1 + 1 by A72,NAT_1:13;
then
A75: f/.k2 <> f/.(k1+1) by A8,A71,Th37;
A76: k2+1 <= k1 by A72,NAT_1:13;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A7,A8,TOPREAL1:def 3;
then
A77: (GoB f)*(i+1,j) = f/.k1 & (GoB f)*(i,j) = f/.(k1+1) or (GoB f)*(i+1
,j) = f/.(k1+1) & (GoB f)*(i,j) = f/.k1 by A9,SPPOL_1:8;
A78: k1 < len f by A8,NAT_1:13;
then
A79: f/.k2 <> f/.k1 by A71,A72,Th37;
A80: LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
(GoB f)*(i+2,j) = f/.k2 & (GoB f)*(i+1,j) = f/.(k2+1) or (GoB f)*(i
+2,j) = f/.(k2+1) & (GoB f)*(i+1,j) = f/.k2 by A18,SPPOL_1:8;
then k2+1 >= k1 by A8,A71,A72,A77,A74,A78,A73,Th37;
then
A81: k2+1 = k1 by A76,XXREAL_0:1;
hence 1 <= k2 & k2+1 < len f by A8,A71,NAT_1:13;
thus f/.(k2+1) = (GoB f)*(i+1,j) by A18,A80,A77,A75,A79,SPPOL_1:8;
thus f/.k2 = (GoB f)*(i+2,j) by A18,A80,A77,A75,A79,SPPOL_1:8;
thus f/.(k2+2) = (GoB f)*(i,j) by A18,A80,A77,A75,A81,SPPOL_1:8;
end;
end;
hence thesis;
end;
theorem Th57:
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & LSeg((
GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1))
c= L~f implies f/.1 = (GoB f)*(i+1,j) & (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) =
(GoB f)*(i+1,j+1) or f/.2 = (GoB f)*(i+1,j+1) & f/.(len f-'1) = (GoB f)*(i,j))
or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) & (f/.k = (GoB f)*
(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or f/.k = (GoB f)*(i+1,j+1) & f/.(k+2) = (
GoB f)*(i,j))
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f and
A6: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f;
A7: j < width GoB f by A4,NAT_1:13;
A8: i < len GoB f by A2,NAT_1:13;
A9: 1 <= j+1 by NAT_1:11;
1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j)) in LSeg((GoB f)*(i,j),(GoB f)* (i+1
,j)) by RLTOPSP1:69;
then consider k1 such that
A10: 1 <= k1 and
A11: k1+1 <= len f and
A12: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k1) by A1,A2,A3,A5,A7,Th40;
A13: k1 < len f by A11,NAT_1:13;
A14: now
assume k1 > 1;
then k1 >= 1+1 by NAT_1:13;
hence k1 = 2 or k1 > 2 by XXREAL_0:1;
end;
A15: 1 <= i+1 by NAT_1:11;
1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) in LSeg((GoB f)*(i+1,j),(GoB f)
*(i+1,j+1)) by RLTOPSP1:69;
then consider k2 such that
A16: 1 <= k2 and
A17: k2+1 <= len f and
A18: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k2) by A2,A3,A4,A6,A15
,Th39;
A19: k2 < len f by A17,NAT_1:13;
A20: now
assume k2 > 1;
then k2 >= 1+1 by NAT_1:13;
hence k2 = 2 or k2 > 2 by XXREAL_0:1;
end;
A21: k1 = 1 or k1 > 1 by A10,XXREAL_0:1;
now
per cases by A16,A14,A20,A21,XXREAL_0:1;
case that
A22: k1 = 1 and
A23: k2 = 2;
A24: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A17,A23,TOPREAL1:def 3;
then
A25: (GoB f)*(i+1,j) = f/.2 & (GoB f)*(i+1,j+1) = f/.(2+1) or (GoB f)*(i
+1,j) = f/.(2+1) & (GoB f)*(i+1,j+1) = (f/.2) by A18,A23,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A17,A23,NAT_1:13;
A26: 3 < len f by Th34,XXREAL_0:2;
then
A27: f/.1 <> f/.3 by Th36;
A28: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A11,A22,TOPREAL1:def 3;
then
A29: (GoB f)*(i,j) = f/.1 & (GoB f)*(i+1,j) = f/.2 or (GoB f)*(i,j) = f
/.2 & (GoB f)*(i+1,j) = f/.1 by A12,A22,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i+1,j) by A25,A26,Th36;
thus f/.1 = (GoB f)*(i,j) by A18,A23,A29,A24,A27,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i+1,j+1) by A12,A22,A28,A25,A27,SPPOL_1:8;
end;
case that
A30: k1 = 1 and
A31: k2 > 2;
A32: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A11,A30,TOPREAL1:def 3;
then
A33: (GoB f)*(i,j) = f/.1 & (GoB f)*(i+1,j) = f/.2 or (GoB f)*(i,j) = f
/.2 & (GoB f)*(i+1,j) = f/.1 by A12,A30,SPPOL_1:8;
A34: 2 < k2+1 by A31,NAT_1:13;
then
A35: f/.(k2+1) <> f/.2 by A17,Th37;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
A36: (GoB f)*(i+1,j) = f/.k2 & (GoB f)*(i+1,j+1) = f/.(k2+1) or (GoB f)*
(i+1,j) = f/.(k2+1) & (GoB f)*(i+1,j+1) = f/.k2 by A18,SPPOL_1:8;
A37: f/.k2 <> f/.2 by A19,A31,Th36;
hence f/.1 = (GoB f)*(i+1,j) by A12,A30,A32,A36,A35,SPPOL_1:8;
thus f/.2 = (GoB f)*(i,j) by A12,A30,A32,A36,A37,A35,SPPOL_1:8;
A38: k2 > 1 by A31,XXREAL_0:2;
then
A39: k2+1 > 1 by NAT_1:13;
then k2+1 = len f by A17,A19,A31,A33,A36,A38,A34,Th37,Th38;
then k2 + 1 = len f -'1 + 1 by A39,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i+1,j+1) by A19,A31,A33,A36,A38,Th36;
end;
case that
A40: k2 = 1 and
A41: k1 = 2;
A42: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A11,A41,TOPREAL1:def 3;
then
A43: (GoB f)*(i+1,j) = f/.2 & (GoB f)*(i,j) = f/.(2+1) or (GoB f)*(i+1,j
) = f/.(2+1) & (GoB f)*(i,j) = (f/.2) by A12,A41,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A11,A41,NAT_1:13;
A44: 3 < len f by Th34,XXREAL_0:2;
then
A45: f/.1 <> f/.3 by Th36;
A46: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A17,A40,TOPREAL1:def 3;
then
A47: (GoB f)*(i+1,j+1) = f/.1 & (GoB f)*(i+1,j) = f/.2 or (GoB f)*(i+1,j
+1) = f/.2 & (GoB f)*(i+1,j) = f/.1 by A18,A40,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i+1,j) by A43,A44,Th36;
thus f/.1 = (GoB f)*(i+1,j+1) by A12,A41,A47,A42,A45,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i,j) by A18,A40,A46,A43,A45,SPPOL_1:8;
end;
case that
A48: k2 = 1 and
A49: k1 > 2;
A50: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A17,A48,TOPREAL1:def 3;
then
A51: (GoB f)*(i+1,j+1) = f/.1 & (GoB f)*(i+1,j) = f/.2 or (GoB f)*(i+1,j
+1) = f/.2 & (GoB f)*(i+1,j) = f/.1 by A18,A48,SPPOL_1:8;
A52: 2 < k1+1 by A49,NAT_1:13;
then
A53: f/.(k1+1) <> f/.2 by A11,Th37;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A10,A11,TOPREAL1:def 3;
then
A54: (GoB f)*(i+1,j) = f/.k1 & (GoB f)*(i,j) = f/.(k1+1) or (GoB f)*(i+1
,j) = f/.(k1+1) & (GoB f)*(i,j) = f/.k1 by A12,SPPOL_1:8;
A55: f/.k1 <> f/.2 by A13,A49,Th36;
hence f/.1 = (GoB f)*(i+1,j) by A18,A48,A50,A54,A53,SPPOL_1:8;
thus f/.2 = (GoB f)*(i+1,j+1) by A18,A48,A50,A54,A55,A53,SPPOL_1:8;
A56: k1 > 1 by A49,XXREAL_0:2;
then
A57: k1+1 > 1 by NAT_1:13;
then k1+1 = len f by A11,A13,A49,A51,A54,A56,A52,Th37,Th38;
then k1 + 1 = len f -'1 + 1 by A57,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i,j) by A13,A49,A51,A54,A56,Th36;
end;
case
k1 = k2;
then
A58: (GoB f)*(i,j) = (GoB f)*(i+1,j+1) or (GoB f)*(i,j) = (GoB f)*( i+1,
j) by A12,A18,SPPOL_1:8;
A59: [i+1,j+1] in Indices GoB f by A2,A4,A15,A9,MATRIX_0:30;
[i,j] in Indices GoB f & [i+1,j] in Indices GoB f by A1,A2,A3,A15,A8,A7,
MATRIX_0:30;
then i = i+1 by A58,A59,GOBOARD1:5;
hence contradiction;
end;
case that
A60: k1 > 1 and
A61: k2 > k1;
A62: 1 < k1+1 & k1+1 < k2+1 by A60,A61,NAT_1:13,XREAL_1:6;
A63: k1 < k2 + 1 by A61,NAT_1:13;
then
A64: f/.k1 <> f/.(k2+1) by A17,A60,Th37;
A65: k1+1 <= k2 by A61,NAT_1:13;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
A66: (GoB f)*(i+1,j) = f/.k2 & (GoB f)*(i+1,j+1) = f/.(k2+1) or (GoB f)*
(i+1,j) = f/.(k2+1) & (GoB f)*(i+1,j+1) = f/.k2 by A18,SPPOL_1:8;
A67: k2 < len f by A17,NAT_1:13;
then
A68: f/.k1 <> f/.k2 by A60,A61,Th37;
A69: LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A10,A11,TOPREAL1:def 3;
then
(GoB f)*(i,j) = f/.k1 & (GoB f)*(i+1,j) = f/.(k1+1) or (GoB f)*(i,j
) = f/.(k1+1) & (GoB f)*(i+1,j) = f/.k1 by A12,SPPOL_1:8;
then k1+1 >= k2 by A17,A60,A61,A66,A63,A67,A62,Th37;
then
A70: k1+1 = k2 by A65,XXREAL_0:1;
hence 1 <= k1 & k1+1 < len f by A17,A60,NAT_1:13;
thus f/.(k1+1) = (GoB f)*(i+1,j) by A12,A69,A66,A64,A68,SPPOL_1:8;
thus f/.k1 = (GoB f)*(i,j) by A12,A69,A66,A64,A68,SPPOL_1:8;
thus f/.(k1+2) = (GoB f)*(i+1,j+1) by A12,A69,A66,A64,A70,SPPOL_1:8;
end;
case that
A71: k2 > 1 and
A72: k1 > k2;
A73: 1 < k2+1 & k2+1 < k1+1 by A71,A72,NAT_1:13,XREAL_1:6;
A74: k2 < k1 + 1 by A72,NAT_1:13;
then
A75: f/.k2 <> f/.(k1+1) by A11,A71,Th37;
A76: k2+1 <= k1 by A72,NAT_1:13;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A10,A11,TOPREAL1:def 3;
then
A77: (GoB f)*(i+1,j) = f/.k1 & (GoB f)*(i,j) = f/.(k1+1) or (GoB f)*(i+1
,j) = f/.(k1+1) & (GoB f)*(i,j) = f/.k1 by A12,SPPOL_1:8;
A78: k1 < len f by A11,NAT_1:13;
then
A79: f/.k2 <> f/.k1 by A71,A72,Th37;
A80: LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A16,A17,TOPREAL1:def 3;
then
(GoB f)*(i+1,j+1) = f/.k2 & (GoB f)*(i+1,j) = f/.(k2+1) or (GoB f)*
(i+1,j+1) = f/.(k2+1) & (GoB f)*(i+1,j) = f/.k2 by A18,SPPOL_1:8;
then k2+1 >= k1 by A11,A71,A72,A77,A74,A78,A73,Th37;
then
A81: k2+1 = k1 by A76,XXREAL_0:1;
hence 1 <= k2 & k2+1 < len f by A11,A71,NAT_1:13;
thus f/.(k2+1) = (GoB f)*(i+1,j) by A18,A80,A77,A75,A79,SPPOL_1:8;
thus f/.k2 = (GoB f)*(i+1,j+1) by A18,A80,A77,A75,A79,SPPOL_1:8;
thus f/.(k2+2) = (GoB f)*(i,j) by A18,A80,A77,A75,A81,SPPOL_1:8;
end;
end;
hence thesis;
end;
theorem Th58:
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & LSeg((
GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f & LSeg((GoB f)*(i+1,j+1),(GoB f)*(i,j+
1)) c= L~f implies f/.1 = (GoB f)*(i+1,j+1) & (f/.2 = (GoB f)*(i+1,j) & f/.(len
f-'1) = (GoB f)*(i,j+1) or f/.2 = (GoB f)*(i,j+1) & f/.(len f-'1) = (GoB f)*(i+
1,j)) or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k =
(GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j+1) or f/.k = (GoB f)*(i,j+1) & f/.(k+
2) = (GoB f)*(i+1,j))
proof
assume that
A1: 1 <= i and
A2: i+1 <= len GoB f and
A3: 1 <= j and
A4: j+1 <= width GoB f and
A5: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f and
A6: LSeg((GoB f)*(i+1,j+1),(GoB f)*(i,j+1)) c= L~f;
A7: 1 <= i+1 by NAT_1:11;
1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) in LSeg((GoB f)*(i+1,j),(GoB f)
*(i+1,j+1)) by RLTOPSP1:69;
then consider k1 such that
A8: 1 <= k1 and
A9: k1+1 <= len f and
A10: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k1) by A2,A3,A4,A5,A7
,Th39;
A11: k1 < len f by A9,NAT_1:13;
A12: now
assume k1 > 1;
then k1 >= 1+1 by NAT_1:13;
hence k1 = 2 or k1 > 2 by XXREAL_0:1;
end;
A13: i < len GoB f & j < width GoB f by A2,A4,NAT_1:13;
A14: 1 <= j+1 by NAT_1:11;
1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) in LSeg((GoB f)*(i+1,j+1),(GoB
f)*(i,j+1)) by RLTOPSP1:69;
then consider k2 such that
A15: 1 <= k2 and
A16: k2+1 <= len f and
A17: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k2) by A1,A2,A4,A6,A14
,Th40;
A18: k2 < len f by A16,NAT_1:13;
A19: now
assume k2 > 1;
then k2 >= 1+1 by NAT_1:13;
hence k2 = 2 or k2 > 2 by XXREAL_0:1;
end;
A20: k1 = 1 or k1 > 1 by A8,XXREAL_0:1;
now
per cases by A15,A12,A19,A20,XXREAL_0:1;
case that
A21: k1 = 1 and
A22: k2 = 2;
A23: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A16,A22,TOPREAL1:def 3;
then
A24: (GoB f)*(i+1,j+1) = f/.2 & (GoB f)*(i,j+1) = f/.(2+1) or (GoB f)*(i
+1,j+1) = f/.(2+1) & (GoB f)*(i,j+1) = (f/.2) by A17,A22,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A16,A22,NAT_1:13;
A25: 3 < len f by Th34,XXREAL_0:2;
then
A26: f/.1 <> f/.3 by Th36;
A27: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A9,A21,TOPREAL1:def 3;
then
A28: (GoB f)*(i+1,j) = f/.1 & (GoB f)*(i+1,j+1) = f/.2 or (GoB f)*(i+1,j
) = f/.2 & (GoB f)*(i+1,j+1) = f/.1 by A10,A21,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i+1,j+1) by A24,A25,Th36;
thus f/.1 = (GoB f)*(i+1,j) by A17,A22,A28,A23,A26,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i,j+1) by A10,A21,A27,A24,A26,SPPOL_1:8;
end;
case that
A29: k1 = 1 and
A30: k2 > 2;
A31: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A9,A29,TOPREAL1:def 3;
then
A32: (GoB f)*(i+1,j) = f/.1 & (GoB f)*(i+1,j+1) = f/.2 or (GoB f)*(i+1,j
) = f/.2 & (GoB f)*(i+1,j+1) = f/.1 by A10,A29,SPPOL_1:8;
A33: 2 < k2+1 by A30,NAT_1:13;
then
A34: f/.(k2+1) <> f/.2 by A16,Th37;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A15,A16,TOPREAL1:def 3;
then
A35: (GoB f)*(i+1,j+1) = f/.k2 & (GoB f)*(i,j+1) = f/.(k2+1) or (GoB f)*
(i+1,j+1) = f/.(k2+1) & (GoB f)*(i,j+1) = f/.k2 by A17,SPPOL_1:8;
A36: f/.k2 <> f/.2 by A18,A30,Th36;
hence f/.1 = (GoB f)*(i+1,j+1) by A10,A29,A31,A35,A34,SPPOL_1:8;
thus f/.2 = (GoB f)*(i+1,j) by A10,A29,A31,A35,A36,A34,SPPOL_1:8;
A37: k2 > 1 by A30,XXREAL_0:2;
then
A38: k2+1 > 1 by NAT_1:13;
then k2+1 = len f by A16,A18,A30,A32,A35,A37,A33,Th37,Th38;
then k2 + 1 = len f -'1 + 1 by A38,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i,j+1) by A18,A30,A32,A35,A37,Th36;
end;
case that
A39: k2 = 1 and
A40: k1 = 2;
A41: LSeg(f,2) = LSeg((f/.2),f/.(2+1)) by A9,A40,TOPREAL1:def 3;
then
A42: (GoB f)*(i+1,j+1) = f/.2 & (GoB f)*(i+1,j) = f/.(2+1) or (GoB f)*(i
+1,j+1) = f/.(2+1) & (GoB f)*(i+1,j) = (f/.2) by A10,A40,SPPOL_1:8;
thus 1 <= 1 & 1+1 < len f by A9,A40,NAT_1:13;
A43: 3 < len f by Th34,XXREAL_0:2;
then
A44: f/.1 <> f/.3 by Th36;
A45: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A16,A39,TOPREAL1:def 3;
then
A46: (GoB f)*(i,j+1) = f/.1 & (GoB f)*(i+1,j+1) = f/.2 or (GoB f)*(i,j+1
) = f/.2 & (GoB f)*(i+1,j+1) = f/.1 by A17,A39,SPPOL_1:8;
hence f/.(1+1) = (GoB f)*(i+1,j+1) by A42,A43,Th36;
thus f/.1 = (GoB f)*(i,j+1) by A10,A40,A46,A41,A44,SPPOL_1:8;
thus f/.(1+2) = (GoB f)*(i+1,j) by A17,A39,A45,A42,A44,SPPOL_1:8;
end;
case that
A47: k2 = 1 and
A48: k1 > 2;
A49: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A16,A47,TOPREAL1:def 3;
then
A50: (GoB f)*(i,j+1) = f/.1 & (GoB f)*(i+1,j+1) = f/.2 or (GoB f)*(i,j+1
) = f/.2 & (GoB f)*(i+1,j+1) = f/.1 by A17,A47,SPPOL_1:8;
A51: 2 < k1+1 by A48,NAT_1:13;
then
A52: f/.(k1+1) <> f/.2 by A9,Th37;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A8,A9,TOPREAL1:def 3;
then
A53: (GoB f)*(i+1,j+1) = f/.k1 & (GoB f)*(i+1,j) = f/.(k1+1) or (GoB f)*
(i+1,j+1) = f/.(k1+1) & (GoB f)*(i+1,j) = f/.k1 by A10,SPPOL_1:8;
A54: f/.k1 <> f/.2 by A11,A48,Th36;
hence f/.1 = (GoB f)*(i+1,j+1) by A17,A47,A49,A53,A52,SPPOL_1:8;
thus f/.2 = (GoB f)*(i,j+1) by A17,A47,A49,A53,A54,A52,SPPOL_1:8;
A55: k1 > 1 by A48,XXREAL_0:2;
then
A56: k1+1 > 1 by NAT_1:13;
then k1+1 = len f by A9,A11,A48,A50,A53,A55,A51,Th37,Th38;
then k1 + 1 = len f -'1 + 1 by A56,XREAL_1:235;
hence f/.(len f-'1) = (GoB f)*(i+1,j) by A11,A48,A50,A53,A55,Th36;
end;
case
k1 = k2;
then
A57: (GoB f)*(i+1,j) = (GoB f)*(i,j+1) or (GoB f)*(i+1,j) = (GoB f) * (i
+1,j+1) by A10,A17,SPPOL_1:8;
A58: [i+1,j+1] in Indices GoB f by A2,A4,A7,A14,MATRIX_0:30;
[i,j+1] in Indices GoB f & [i+1,j] in Indices GoB f by A1,A2,A3,A4,A7,A14
,A13,MATRIX_0:30;
then j = j+1 or i = i+1 by A57,A58,GOBOARD1:5;
hence contradiction;
end;
case that
A59: k1 > 1 and
A60: k2 > k1;
A61: 1 < k1+1 & k1+1 < k2+1 by A59,A60,NAT_1:13,XREAL_1:6;
A62: k1 < k2 + 1 by A60,NAT_1:13;
then
A63: f/.k1 <> f/.(k2+1) by A16,A59,Th37;
A64: k1+1 <= k2 by A60,NAT_1:13;
LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A15,A16,TOPREAL1:def 3;
then
A65: (GoB f)*(i+1,j+1) = f/.k2 & (GoB f)*(i,j+1) = f/.(k2+1) or (GoB f)*
(i+1,j+1) = f/.(k2+1) & (GoB f)*(i,j+1) = f/.k2 by A17,SPPOL_1:8;
A66: k2 < len f by A16,NAT_1:13;
then
A67: f/.k1 <> f/.k2 by A59,A60,Th37;
A68: LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A8,A9,TOPREAL1:def 3;
then
(GoB f)*(i+1,j) = f/.k1 & (GoB f)*(i+1,j+1) = f/.(k1+1) or (GoB f)*
(i+1,j) = f/.(k1+1) & (GoB f)*(i+1,j+1) = f/.k1 by A10,SPPOL_1:8;
then k1+1 >= k2 by A16,A59,A60,A65,A62,A66,A61,Th37;
then
A69: k1+1 = k2 by A64,XXREAL_0:1;
hence 1 <= k1 & k1+1 < len f by A16,A59,NAT_1:13;
thus f/.(k1+1) = (GoB f)*(i+1,j+1) by A10,A68,A65,A63,A67,SPPOL_1:8;
thus f/.k1 = (GoB f)*(i+1,j) by A10,A68,A65,A63,A67,SPPOL_1:8;
thus f/.(k1+2) = (GoB f)*(i,j+1) by A10,A68,A65,A63,A69,SPPOL_1:8;
end;
case that
A70: k2 > 1 and
A71: k1 > k2;
A72: 1 < k2+1 & k2+1 < k1+1 by A70,A71,NAT_1:13,XREAL_1:6;
A73: k2 < k1 + 1 by A71,NAT_1:13;
then
A74: f/.k2 <> f/.(k1+1) by A9,A70,Th37;
A75: k2+1 <= k1 by A71,NAT_1:13;
LSeg(f,k1) = LSeg(f/.k1,f/.(k1+1)) by A8,A9,TOPREAL1:def 3;
then
A76: (GoB f)*(i+1,j+1) = f/.k1 & (GoB f)*(i+1,j) = f/.(k1+1) or (GoB f)*
(i+1,j+1) = f/.(k1+1) & (GoB f)*(i+1,j) = f/.k1 by A10,SPPOL_1:8;
A77: k1 < len f by A9,NAT_1:13;
then
A78: f/.k2 <> f/.k1 by A70,A71,Th37;
A79: LSeg(f,k2) = LSeg(f/.k2,f/.(k2+1)) by A15,A16,TOPREAL1:def 3;
then
(GoB f)*(i,j+1) = f/.k2 & (GoB f)*(i+1,j+1) = f/.(k2+1) or (GoB f)*
(i,j+1) = f/.(k2+1) & (GoB f)*(i+1,j+1) = f/.k2 by A17,SPPOL_1:8;
then k2+1 >= k1 by A9,A70,A71,A76,A73,A77,A72,Th37;
then
A80: k2+1 = k1 by A75,XXREAL_0:1;
hence 1 <= k2 & k2+1 < len f by A9,A70,NAT_1:13;
thus f/.(k2+1) = (GoB f)*(i+1,j+1) by A17,A79,A76,A74,A78,SPPOL_1:8;
thus f/.k2 = (GoB f)*(i,j+1) by A17,A79,A76,A74,A78,SPPOL_1:8;
thus f/.(k2+2) = (GoB f)*(i+1,j) by A17,A79,A76,A74,A80,SPPOL_1:8;
end;
end;
hence thesis;
end;
theorem
1 <= i & i < len GoB f & 1 <= j & j+1 < width GoB f implies not ( LSeg
((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2))
c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f)
proof
assume that
A1: 1 <= i and
A2: i < len GoB f and
A3: 1 <= j and
A4: j+1 < width GoB f and
A5: LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f & LSeg((GoB f)*(i,j+1),(
GoB f)* (i,j+2)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f;
A6: i+1 <= len GoB f by A2,NAT_1:13;
j+(1+1) = j+1+1;
then
A7: j+2 <= width GoB f by A4,NAT_1:13;
A8: 1 <= j+1 by NAT_1:11;
A9: j < width GoB f by A4,NAT_1:13;
A10: 1 <= i+1 by NAT_1:11;
j+1 <= j+2 by XREAL_1:6;
then
A11: 1 <= j+2 by A8,XXREAL_0:2;
per cases by A1,A2,A3,A4,A5,A6,Th53,Th54;
suppose
A12: f/.(len f-'1) = (GoB f)*(i,j+2) & f/.(len f-'1) = (GoB f)* (i+1,j +1);
[i,j+2] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A4,A6,A10,A8
,A7,A11,MATRIX_0:30;
then i = i+1 by A12,GOBOARD1:5;
hence contradiction;
end;
suppose
A13: f/.2 = (GoB f)*(i,j) & f/.2 = (GoB f)*(i+1,j+1);
[i,j] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A3,A4,A6,A10
,A9,A8,MATRIX_0:30;
then i = i+1 by A13,GOBOARD1:5;
hence contradiction;
end;
suppose
A14: f/.2 = (GoB f)*(i,j+2) & f/.2 = (GoB f)*(i,j);
[i,j+2] in Indices GoB f & [i,j] in Indices GoB f by A1,A2,A3,A9,A7,A11,
MATRIX_0:30;
then j = j+2 by A14,GOBOARD1:5;
hence contradiction;
end;
suppose
A15: f/.2 = (GoB f)*(i,j+2) & f/.2 = (GoB f)*(i+1,j+1);
[i,j+2] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A4,A6,A10,A8
,A7,A11,MATRIX_0:30;
then i = i+1 by A15,GOBOARD1:5;
hence contradiction;
end;
suppose that
A16: f/.1 = (GoB f)*(i,j+1) and
A17: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) & (f/.k
= (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or f/.k = (GoB f)*(i+1,j+1) & f
/.(k+2) = (GoB f)*(i,j));
consider k such that
A18: 1 <= k and
A19: k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) and
f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or f/.k = (GoB f)*
(i+1,j+1) & f/.(k+2) = (GoB f)*(i,j) by A17;
1 < k+1 by A18,NAT_1:13;
hence contradiction by A16,A19,Th36;
end;
suppose that
A20: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) & (f/.k
= (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i,j+2) or f/.k = (GoB f)*(i,j+2) & f/.(k+
2) = (GoB f)*(i,j)) and
A21: f/.1 = (GoB f)*(i,j+1);
consider k such that
A22: 1 <= k and
A23: k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) and
f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i,j+2) or f/.k = (GoB f)*(i
,j+2) & f/.(k+2) = (GoB f)*(i,j) by A20;
1 < k+1 by A22,NAT_1:13;
hence contradiction by A21,A23,Th36;
end;
suppose that
A24: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) & (f/.k
= (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i,j+2) or f/.k = (GoB f)*(i,j+2) & f/.(k+
2) = (GoB f)*(i,j)) and
A25: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) & (f/.k
= (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or f/.k = (GoB f)*(i+1,j+1) & f
/.(k+2) = (GoB f)*(i,j));
consider k1 such that
1 <= k1 and
A26: k1+1 < len f and
A27: f/.(k1+1) = (GoB f)*(i,j+1) and
A28: f/.k1 = (GoB f)*(i,j) & f/.(k1+2) = (GoB f)*(i,j+2) or f/.k1 = (
GoB f)*(i,j+2) & f/.(k1+2) = (GoB f)*(i,j) by A24;
consider k2 such that
1 <= k2 and
A29: k2+1 < len f and
A30: f/.(k2+1) = (GoB f)*(i,j+1) and
A31: f/.k2 = (GoB f)*(i,j) & f/.(k2+2) = (GoB f)*(i+1,j+1) or f/.k2 =
(GoB f)*(i+1,j+1) & f/.(k2+2) = (GoB f)*(i,j) by A25;
A32: now
assume
A33: k1 <> k2;
per cases by A33,XXREAL_0:1;
suppose
k1 < k2;
then k1+1 < k2+1 by XREAL_1:6;
hence contradiction by A27,A29,A30,Th36,NAT_1:11;
end;
suppose
k2 < k1;
then k2+1 < k1+1 by XREAL_1:6;
hence contradiction by A26,A27,A30,Th36,NAT_1:11;
end;
end;
now
per cases by A28,A31;
suppose
A34: f/.(k1+2) = (GoB f)*(i,j+2) & f/.(k2+2) = (GoB f)*(i+1,j+1);
[i,j+2] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A4,A6
,A10,A8,A7,A11,MATRIX_0:30;
then i = i+1 by A32,A34,GOBOARD1:5;
hence contradiction;
end;
suppose
A35: f/.k1 = (GoB f)*(i,j) & f/.k2 = (GoB f)*(i+1,j+1);
[i,j] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A3,A4,A6
,A10,A9,A8,MATRIX_0:30;
then i = i+1 by A32,A35,GOBOARD1:5;
hence contradiction;
end;
suppose
A36: f/.k1 = (GoB f)*(i,j+2) & f/.k2 = (GoB f)*(i,j);
[i,j+2] in Indices GoB f & [i,j] in Indices GoB f by A1,A2,A3,A9,A7,A11
,MATRIX_0:30;
then j = j+2 by A32,A36,GOBOARD1:5;
hence contradiction;
end;
suppose
A37: f/.k1 = (GoB f)*(i,j+2) & f/.k2 = (GoB f)*(i+1,j+1);
[i,j+2] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A4,A6
,A10,A8,A7,A11,MATRIX_0:30;
then i = i+1 by A32,A37,GOBOARD1:5;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
theorem
1 <= i & i < len GoB f & 1 <= j & j+1 < width GoB f implies not ( LSeg
((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f & LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+
1,j+2)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f)
proof
assume that
A1: 1 <= i and
A2: i < len GoB f and
A3: 1 <= j and
A4: j+1 < width GoB f and
A5: LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f & LSeg((GoB f)*(i+1,j
+1),( GoB f)*(i+1,j+2)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f
;
A6: i+1 <= len GoB f by A2,NAT_1:13;
j+(1+1) = j+1+1;
then
A7: j+2 <= width GoB f by A4,NAT_1:13;
A8: 1 <= j+1 by NAT_1:11;
A9: j < width GoB f by A4,NAT_1:13;
A10: 1 <= i+1 by NAT_1:11;
j+1 <= j+2 by XREAL_1:6;
then
A11: 1 <= j+2 by A8,XXREAL_0:2;
per cases by A1,A3,A4,A5,A6,A10,Th53,Th55;
suppose
A12: f/.2 = (GoB f)*(i+1,j) & f/.2 = (GoB f)*(i,j+1);
[i+1,j] in Indices GoB f & [i,j+1] in Indices GoB f by A1,A2,A3,A4,A6,A10
,A9,A8,MATRIX_0:30;
then i = i+1 by A12,GOBOARD1:5;
hence contradiction;
end;
suppose
A13: f/.(len f-'1) = (GoB f)*(i+1,j+2) & f/.(len f-'1) = (GoB f)* (i,j +1);
[i+1,j+2] in Indices GoB f & [i,j+1] in Indices GoB f by A1,A2,A4,A6,A10,A8
,A7,A11,MATRIX_0:30;
then i = i+1 by A13,GOBOARD1:5;
hence contradiction;
end;
suppose
A14: f/.2 = (GoB f)*(i+1,j+2) & f/.2 = (GoB f)*(i,j+1);
[i+1,j+2] in Indices GoB f & [i,j+1] in Indices GoB f by A1,A2,A4,A6,A10,A8
,A7,A11,MATRIX_0:30;
then i = i+1 by A14,GOBOARD1:5;
hence contradiction;
end;
suppose
A15: f/.2 = (GoB f)*(i+1,j+2) & f/.2 = (GoB f)*(i+1,j);
[i+1,j+2] in Indices GoB f & [i+1,j] in Indices GoB f by A3,A6,A10,A9,A7
,A11,MATRIX_0:30;
then j = j+2 by A15,GOBOARD1:5;
hence contradiction;
end;
suppose that
A16: f/.1 = (GoB f)*(i+1,j+1) and
A17: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f
/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or f/.k = (GoB f)*(i+1,j) &
f/.(k+2) = (GoB f)*(i,j+1));
consider k such that
A18: 1 <= k and
A19: k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) and
f/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or f/.k = (GoB f)*
(i+1,j) & f/.(k+2) = (GoB f)*(i,j+1) by A17;
1 < k+1 by A18,NAT_1:13;
hence contradiction by A16,A19,Th36;
end;
suppose that
A20: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f
/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.k = (GoB f)*(i+1,j+2
) & f/.(k+2) = (GoB f)*(i+1,j)) and
A21: f/.1 = (GoB f)*(i+1,j+1);
consider k such that
A22: 1 <= k and
A23: k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) and
f/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.k = (GoB f
)*(i+1,j+2) & f/.(k+2) = (GoB f)*(i+1,j) by A20;
1 < k+1 by A22,NAT_1:13;
hence contradiction by A21,A23,Th36;
end;
suppose that
A24: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f
/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.k = (GoB f)*(i+1,j+2
) & f/.(k+2) = (GoB f)*(i+1,j)) and
A25: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f
/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or f/.k = (GoB f)*(i+1,j) &
f/.(k+2) = (GoB f)*(i,j+1));
consider k1 such that
1 <= k1 and
A26: k1+1 < len f and
A27: f/.(k1+1) = (GoB f)*(i+1,j+1) and
A28: f/.k1 = (GoB f)*(i+1,j) & f/.(k1+2) = (GoB f)*(i+1,j+2) or f/.k1
= (GoB f)*(i+1,j+2) & f/.(k1+2) = (GoB f)*(i+1,j) by A24;
consider k2 such that
1 <= k2 and
A29: k2+1 < len f and
A30: f/.(k2+1) = (GoB f)*(i+1,j+1) and
A31: f/.k2 = (GoB f)*(i,j+1) & f/.(k2+2) = (GoB f)*(i+1,j) or f/.k2 =
(GoB f)*(i+1,j) & f/.(k2+2) = (GoB f)*(i,j+1) by A25;
A32: now
assume
A33: k1 <> k2;
per cases by A33,XXREAL_0:1;
suppose
k1 < k2;
then k1+1 < k2+1 by XREAL_1:6;
hence contradiction by A27,A29,A30,Th36,NAT_1:11;
end;
suppose
k2 < k1;
then k2+1 < k1+1 by XREAL_1:6;
hence contradiction by A26,A27,A30,Th36,NAT_1:11;
end;
end;
now
per cases by A28,A31;
suppose
A34: f/.k1 = (GoB f)*(i+1,j) & f/.k2 = (GoB f)*(i,j+1);
[i+1,j] in Indices GoB f & [i,j+1] in Indices GoB f by A1,A2,A3,A4,A6
,A10,A9,A8,MATRIX_0:30;
then i = i+1 by A32,A34,GOBOARD1:5;
hence contradiction;
end;
suppose
A35: f/.(k1+2) = (GoB f)*(i+1,j+2) & f/.(k2+2) = (GoB f)*(i,j+1);
[i+1,j+2] in Indices GoB f & [i,j+1] in Indices GoB f by A1,A2,A4,A6
,A10,A8,A7,A11,MATRIX_0:30;
then i = i+1 by A32,A35,GOBOARD1:5;
hence contradiction;
end;
suppose
A36: f/.k1 = (GoB f)*(i+1,j+2) & f/.k2 = (GoB f)*(i,j+1);
[i+1,j+2] in Indices GoB f & [i,j+1] in Indices GoB f by A1,A2,A4,A6
,A10,A8,A7,A11,MATRIX_0:30;
then i = i+1 by A32,A36,GOBOARD1:5;
hence contradiction;
end;
suppose
A37: f/.k1 = (GoB f)*(i+1,j+2) & f/.k2 = (GoB f)*(i+1,j);
[i+1,j+2] in Indices GoB f & [i+1,j] in Indices GoB f by A3,A6,A10,A9
,A7,A11,MATRIX_0:30;
then j = j+2 by A32,A37,GOBOARD1:5;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
theorem
1 <= j & j < width GoB f & 1 <= i & i+1 < len GoB f implies not ( LSeg
((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j))
c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f)
proof
assume that
A1: 1 <= j and
A2: j < width GoB f and
A3: 1 <= i and
A4: i+1 < len GoB f and
A5: LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f & LSeg((GoB f)*(i+1,j),(
GoB f)* (i +2,j)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f;
A6: j+1 <= width GoB f by A2,NAT_1:13;
i+(1+1) = i+1+1;
then
A7: i+2 <= len GoB f by A4,NAT_1:13;
A8: 1 <= i+1 by NAT_1:11;
A9: i < len GoB f by A4,NAT_1:13;
A10: 1 <= j+1 by NAT_1:11;
i+1 <= i+2 by XREAL_1:6;
then
A11: 1 <= i+2 by A8,XXREAL_0:2;
per cases by A1,A2,A3,A4,A5,A6,Th56,Th57;
suppose
A12: f/.(len f-'1) = (GoB f)*(i+2,j) & f/.(len f-'1) = (GoB f)*(i+1,j+ 1);
[i+2,j] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A4,A6,A10,A8
,A7,A11,MATRIX_0:30;
then j = j+1 by A12,GOBOARD1:5;
hence contradiction;
end;
suppose
A13: f/.2 = (GoB f)*(i,j) & f/.2 = (GoB f)*(i+1,j+1);
[i,j] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A3,A4,A6,A10
,A9,A8,MATRIX_0:30;
then j = j+1 by A13,GOBOARD1:5;
hence contradiction;
end;
suppose
A14: f/.2 = (GoB f)*(i+2,j) & f/.2 = (GoB f)*(i,j);
[i+2,j] in Indices GoB f & [i,j] in Indices GoB f by A1,A2,A3,A9,A7,A11,
MATRIX_0:30;
then i = i+2 by A14,GOBOARD1:5;
hence contradiction;
end;
suppose
A15: f/.2 = (GoB f)*(i+2,j) & f/.2 = (GoB f)*(i+1,j+1);
[i+2,j] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A4,A6,A10,A8
,A7,A11,MATRIX_0:30;
then j = j+1 by A15,GOBOARD1:5;
hence contradiction;
end;
suppose that
A16: f/.1 = (GoB f)*(i+1,j) and
A17: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) & (f/.k
= (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or f/.k = (GoB f)*(i+1,j+1) & f
/.(k+2) = (GoB f)*(i,j));
consider k such that
A18: 1 <= k and
A19: k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) and
f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or f/.k = (GoB f)*
(i+1,j+1) & f/.(k+2) = (GoB f)*(i,j) by A17;
1 < k+1 by A18,NAT_1:13;
hence contradiction by A16,A19,Th36;
end;
suppose that
A20: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) & (f/.k
= (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+2,j) or f/.k = (GoB f)*(i+2,j) & f/.(k+
2) = (GoB f)*(i,j)) and
A21: f/.1 = (GoB f)*(i+1,j);
consider k such that
A22: 1 <= k and
A23: k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) and
f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+2,j) or f/.k = (GoB f)*(i
+2,j) & f/.(k+2) = (GoB f)*(i,j) by A20;
1 < k+1 by A22,NAT_1:13;
hence contradiction by A21,A23,Th36;
end;
suppose that
A24: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) & (f/.k
= (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+2,j) or f/.k = (GoB f)*(i+2,j) & f/.(k+
2) = (GoB f)*(i,j)) and
A25: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) & (f/.k
= (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or f/.k = (GoB f)*(i+1,j+1) & f
/.(k+2) = (GoB f)*(i,j));
consider k1 such that
1 <= k1 and
A26: k1+1 < len f and
A27: f/.(k1+1) = (GoB f)*(i+1,j) and
A28: f/.k1 = (GoB f)*(i,j) & f/.(k1+2) = (GoB f)*(i+2,j) or f/.k1 = (
GoB f)*(i+2,j) & f/.(k1+2) = (GoB f)*(i,j) by A24;
consider k2 such that
1 <= k2 and
A29: k2+1 < len f and
A30: f/.(k2+1) = (GoB f)*(i+1,j) and
A31: f/.k2 = (GoB f)*(i,j) & f/.(k2+2) = (GoB f)*(i+1,j+1) or f/.k2 =
(GoB f)*(i+1,j+1) & f/.(k2+2) = (GoB f)*(i,j) by A25;
A32: now
assume
A33: k1 <> k2;
per cases by A33,XXREAL_0:1;
suppose
k1 < k2;
then k1+1 < k2+1 by XREAL_1:6;
hence contradiction by A27,A29,A30,Th36,NAT_1:11;
end;
suppose
k2 < k1;
then k2+1 < k1+1 by XREAL_1:6;
hence contradiction by A26,A27,A30,Th36,NAT_1:11;
end;
end;
now
per cases by A28,A31;
suppose
A34: f/.(k1+2) = (GoB f)*(i+2,j) & f/.(k2+2) = (GoB f)*(i+1,j+1);
[i+2,j] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A4,A6
,A10,A8,A7,A11,MATRIX_0:30;
then j = j+1 by A32,A34,GOBOARD1:5;
hence contradiction;
end;
suppose
A35: f/.k1 = (GoB f)*(i,j) & f/.k2 = (GoB f)*(i+1,j+1);
[i,j] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A3,A4,A6
,A10,A9,A8,MATRIX_0:30;
then j = j+1 by A32,A35,GOBOARD1:5;
hence contradiction;
end;
suppose
A36: f/.k1 = (GoB f)*(i+2,j) & f/.k2 = (GoB f)*(i,j);
[i+2,j] in Indices GoB f & [i,j] in Indices GoB f by A1,A2,A3,A9,A7,A11
,MATRIX_0:30;
then i = i+2 by A32,A36,GOBOARD1:5;
hence contradiction;
end;
suppose
A37: f/.k1 = (GoB f)*(i+2,j) & f/.k2 = (GoB f)*(i+1,j+1);
[i+2,j] in Indices GoB f & [i+1,j+1] in Indices GoB f by A1,A2,A4,A6
,A10,A8,A7,A11,MATRIX_0:30;
then j = j+1 by A32,A37,GOBOARD1:5;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
theorem
1 <= j & j < width GoB f & 1 <= i & i+1 < len GoB f implies not ( LSeg
((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f & LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+
2,j+1)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f)
proof
assume that
A1: 1 <= j and
A2: j < width GoB f and
A3: 1 <= i and
A4: i+1 < len GoB f and
A5: LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f & LSeg((GoB f)*(i+1,j
+1),( GoB f)*(i+2,j+1)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f
;
A6: j+1 <= width GoB f by A2,NAT_1:13;
i+(1+1) = i+1+1;
then
A7: i+2 <= len GoB f by A4,NAT_1:13;
A8: 1 <= i+1 by NAT_1:11;
A9: i < len GoB f by A4,NAT_1:13;
A10: 1 <= j+1 by NAT_1:11;
i+1 <= i+2 by XREAL_1:6;
then
A11: 1 <= i+2 by A8,XXREAL_0:2;
per cases by A1,A3,A4,A5,A6,A10,Th56,Th58;
suppose
A12: f/.2 = (GoB f)*(i,j+1) & f/.2 = (GoB f)*(i+1,j);
[i,j+1] in Indices GoB f & [i+1,j] in Indices GoB f by A1,A2,A3,A4,A6,A10
,A9,A8,MATRIX_0:30;
then j = j+1 by A12,GOBOARD1:5;
hence contradiction;
end;
suppose
A13: f/.(len f -' 1) = (GoB f)*(i+2,j+1) & f/.(len f -' 1) = (GoB f)*( i+1,j);
[i+2,j+1] in Indices GoB f & [i+1,j] in Indices GoB f by A1,A2,A4,A6,A10,A8
,A7,A11,MATRIX_0:30;
then j = j+1 by A13,GOBOARD1:5;
hence contradiction;
end;
suppose
A14: f/.2 = (GoB f)*(i+2,j+1) & f/.2 = (GoB f)*(i+1,j);
[i+2,j+1] in Indices GoB f & [i+1,j] in Indices GoB f by A1,A2,A4,A6,A10,A8
,A7,A11,MATRIX_0:30;
then j = j+1 by A14,GOBOARD1:5;
hence contradiction;
end;
suppose
A15: f/.2 = (GoB f)*(i+2,j+1) & f/.2 = (GoB f)*(i,j+1);
[i+2,j+1] in Indices GoB f & [i,j+1] in Indices GoB f by A3,A6,A10,A9,A7
,A11,MATRIX_0:30;
then i = i+2 by A15,GOBOARD1:5;
hence contradiction;
end;
suppose that
A16: f/.1 = (GoB f)*(i+1,j+1) and
A17: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f
/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j+1) or f/.k = (GoB f)*(i,j+1) &
f/.(k+2) = (GoB f)*(i+1,j));
consider k such that
A18: 1 <= k and
A19: k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) and
f/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j+1) or f/.k = (GoB f)*
(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j) by A17;
1 < k+1 by A18,NAT_1:13;
hence contradiction by A16,A19,Th36;
end;
suppose that
A20: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f
/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.k = (GoB f)*(i+2,j+1
) & f/.(k+2) = (GoB f)*(i,j+1)) and
A21: f/.1 = (GoB f)*(i+1,j+1);
consider k such that
A22: 1 <= k and
A23: k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) and
f/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.k = (GoB f
)*(i+2,j+1) & f/.(k+2) = (GoB f)*(i,j+1) by A20;
1 < k+1 by A22,NAT_1:13;
hence contradiction by A21,A23,Th36;
end;
suppose that
A24: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f
/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.k = (GoB f)*(i+2,j+1
) & f/.(k+2) = (GoB f)*(i,j+1)) and
A25: ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f
/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j+1) or f/.k = (GoB f)*(i,j+1) &
f/.(k+2) = (GoB f)*(i+1,j));
consider k1 such that
1 <= k1 and
A26: k1+1 < len f and
A27: f/.(k1+1) = (GoB f)*(i+1,j+1) and
A28: f/.k1 = (GoB f)*(i,j+1) & f/.(k1+2) = (GoB f)*(i+2,j+1) or f/.k1
= (GoB f)*(i+2,j+1) & f/.(k1+2) = (GoB f)*(i,j+1) by A24;
consider k2 such that
1 <= k2 and
A29: k2+1 < len f and
A30: f/.(k2+1) = (GoB f)*(i+1,j+1) and
A31: f/.k2 = (GoB f)*(i+1,j) & f/.(k2+2) = (GoB f)*(i,j+1) or f/.k2 =
(GoB f)*(i,j+1) & f/.(k2+2) = (GoB f)*(i+1,j) by A25;
A32: now
assume
A33: k1 <> k2;
per cases by A33,XXREAL_0:1;
suppose
k1 < k2;
then k1+1 < k2+1 by XREAL_1:6;
hence contradiction by A27,A29,A30,Th36,NAT_1:11;
end;
suppose
k2 < k1;
then k2+1 < k1+1 by XREAL_1:6;
hence contradiction by A26,A27,A30,Th36,NAT_1:11;
end;
end;
now
per cases by A28,A31;
suppose
A34: f/.k1 = (GoB f)*(i,j+1) & f/.k2 = (GoB f)*(i+1,j);
[i,j+1] in Indices GoB f & [i+1,j] in Indices GoB f by A1,A2,A3,A4,A6
,A10,A9,A8,MATRIX_0:30;
then j = j+1 by A32,A34,GOBOARD1:5;
hence contradiction;
end;
suppose
A35: f/.(k1+2) = (GoB f)*(i+2,j+1) & f/.(k2+2) = (GoB f)*(i+1,j);
[i+2,j+1] in Indices GoB f & [i+1,j] in Indices GoB f by A1,A2,A4,A6
,A10,A8,A7,A11,MATRIX_0:30;
then j = j+1 by A32,A35,GOBOARD1:5;
hence contradiction;
end;
suppose
A36: f/.k1 = (GoB f)*(i+2,j+1) & f/.k2 = (GoB f)*(i+1,j);
[i+2,j+1] in Indices GoB f & [i+1,j] in Indices GoB f by A1,A2,A4,A6
,A10,A8,A7,A11,MATRIX_0:30;
then j = j+1 by A32,A36,GOBOARD1:5;
hence contradiction;
end;
suppose
A37: f/.k1 = (GoB f)*(i+2,j+1) & f/.k2 = (GoB f)*(i,j+1);
[i+2,j+1] in Indices GoB f & [i,j+1] in Indices GoB f by A3,A6,A10,A9
,A7,A11,MATRIX_0:30;
then i = i+2 by A32,A37,GOBOARD1:5;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
:: Moved from JORDAN15, AK, 22.02.2006
theorem
for p,q,p1,q1 be Point of TOP-REAL 2 st LSeg(p,q) is vertical & LSeg(
p1,q1) is vertical & p`1 = p1`1 & p`2 <= p1`2 & p1`2 <= q1`2 & q1`2 <= q`2
holds LSeg(p1,q1) c= LSeg(p,q)
proof
let p,q,p1,q1 be Point of TOP-REAL 2;
assume that
A1: LSeg(p,q) is vertical and
A2: LSeg(p1,q1) is vertical and
A3: p`1 = p1`1 and
A4: p`2 <= p1`2 and
A5: p1`2 <= q1`2 and
A6: q1`2 <= q`2;
A7: p`1 = q`1 by A1,SPPOL_1:16;
let x be object;
assume
A8: x in LSeg(p1,q1);
then reconsider r=x as Point of TOP-REAL 2;
p1`2 <= r`2 by A5,A8,TOPREAL1:4;
then
A9: p`2 <= r`2 by A4,XXREAL_0:2;
r`2 <= q1`2 by A5,A8,TOPREAL1:4;
then
A10: r`2 <= q`2 by A6,XXREAL_0:2;
p1`1 = r`1 by A2,A8,SPPOL_1:41;
hence thesis by A3,A7,A9,A10,Th7;
end;
theorem
for p,q,p1,q1 be Point of TOP-REAL 2 st LSeg(p,q) is horizontal & LSeg
(p1,q1) is horizontal & p`2 = p1`2 & p`1 <= p1`1 & p1`1 <= q1`1 & q1`1 <= q`1
holds LSeg(p1,q1) c= LSeg(p,q)
proof
let p,q,p1,q1 be Point of TOP-REAL 2;
assume that
A1: LSeg(p,q) is horizontal and
A2: LSeg(p1,q1) is horizontal and
A3: p`2 = p1`2 and
A4: p`1 <= p1`1 and
A5: p1`1 <= q1`1 and
A6: q1`1 <= q`1;
A7: p`2 = q`2 by A1,SPPOL_1:15;
let x be object;
assume
A8: x in LSeg(p1,q1);
then reconsider r=x as Point of TOP-REAL 2;
p1`1 <= r`1 by A5,A8,TOPREAL1:3;
then
A9: p`1 <= r`1 by A4,XXREAL_0:2;
r`1 <= q1`1 by A5,A8,TOPREAL1:3;
then
A10: r`1 <= q`1 by A6,XXREAL_0:2;
p1`2 = r`2 by A2,A8,SPPOL_1:40;
hence thesis by A3,A7,A9,A10,Th8;
end;