:: More on Segments on a Go Board
:: by Andrzej Trybulec
::
:: Received October 17, 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, SUBSET_1, PRE_TOPC, EUCLID, FUNCT_1, GOBOARD5, XXREAL_0,
ARYTM_3, FINSEQ_1, GOBOARD2, TREES_1, PARTFUN1, RELAT_1, RLTOPSP1,
XBOOLE_0, TOPREAL1, TARSKI, TOPS_1, ARYTM_1, CARD_1, MCART_1, GOBOARD1,
MATRIX_1, NAT_1, COMPLEX1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1,
NAT_1, NAT_D, PARTFUN1, FINSEQ_1, MATRIX_0, SEQM_3, STRUCT_0, PRE_TOPC,
TOPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2,
GOBOARD5, XXREAL_0;
constructors REAL_1, NAT_D, TOPS_1, GOBOARD2, GOBOARD5, GOBOARD1, RELSET_1;
registrations RELSET_1, XREAL_0, STRUCT_0, EUCLID, GOBOARD2, GOBOARD5,
ORDINAL1, NAT_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems GOBOARD5, EUCLID, GOBOARD1, TOPREAL3, TOPREAL1, GOBOARD2, FINSEQ_3,
NAT_1, GOBOARD6, GOBOARD7, SPPOL_2, XBOOLE_0, XBOOLE_1, ZFMISC_1,
XREAL_1, XXREAL_0, XREAL_0, MATRIX_0, SEQM_3;
begin
reserve i,j,k,i1,j1 for Nat,
p for Point of TOP-REAL 2,
x for set;
reserve f for non constant standard special_circular_sequence;
theorem
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+1 <= len GoB f &
1 <= j & j+2 <= width GoB 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+2) = (GoB f)*(i+1,j) & f/.k = (
GoB f)*(i+1,j+2)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f
)*(i,j+1)+(GoB f)*(i+1,j+2))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let i,j such that
A6: 1 <= i and
A7: i+1 <= len GoB f and
A8: 1 <= j and
A9: j+2 <= width GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j+1) and
A11: f/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.(k+2) =
(GoB f)*(i+1,j) & f/.k = (GoB f)*(i+1,j+2);
A12: i < len GoB f by A7,NAT_1:13;
j < j+2 by XREAL_1:29;
then j <= width GoB f by A9,XXREAL_0:2;
then
A13: L~f misses Int cell(GoB f,i,j) by A12,GOBOARD7:12;
j+1 <= j+2 by XREAL_1:6;
then
A14: j+1 <= width GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i,j+1) by A12,GOBOARD7:12;
then
A15: L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1) by A13,XBOOLE_1:70
;
j+1+1 = j+(1+1);
then
A16: j+1 < width GoB f by A9,NAT_1:13;
assume LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i,j+1)+(
GoB f)*(i+1,j+2))) meets L~f;
then
L~f meets Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1) \/ { 1/2*((GoB f
)*(i,j+1)+(GoB f)*(i+1,j+1)) } by A6,A8,A16,A12,GOBOARD6:64,XBOOLE_1:63;
then 1 <= j+1 & L~f meets { 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) } by A15,
NAT_1:11,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A17: LSeg(f/.(k+1),(GoB f)*(i,j+1)) = LSeg(f,k0) by A6,A7,A10,A14,GOBOARD7:40
,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A10,A11,A16,A12,A17,A4,A5,GOBOARD7:60;
end;
theorem
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f &
1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+2,j+1) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.(k+2) = (GoB f)*(i+2,j+1) & f/.k =
(GoB f)*(i+1,j+2)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB
f)*(i,j+1)+(GoB f)*(i+1,j+2))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let i,j such that
A6: 1 <= i and
A7: i+2 <= len GoB f and
A8: 1 <= j and
A9: j+2 <= width GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j+1) and
A11: f/.k = (GoB f)*(i+2,j+1) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.(k+2)
= (GoB f)*(i+2,j+1) & f/.k = (GoB f)*(i+1,j+2);
i+1+1 = i+(1+1);
then
A12: i+1 < len GoB f by A7,NAT_1:13;
then
A13: i < len GoB f by NAT_1:13;
j < j+2 by XREAL_1:29;
then j < width GoB f by A9,XXREAL_0:2;
then
A14: L~f misses Int cell(GoB f,i,j) by A13,GOBOARD7:12;
j+1 <= j+2 by XREAL_1:6;
then
A15: j+1 <= width GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i,j+1) by A13,GOBOARD7:12;
then
A16: L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1) by A14,XBOOLE_1:70
;
A17: 1 <= j+1 by NAT_1:11;
A18: j+1+1 = j+(1+1);
then
A19: j+1 < width GoB f by A9,NAT_1:13;
assume LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i,j+1)+(
GoB f)*(i+1,j+2))) meets L~f;
then
L~f meets Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1) \/ { 1/2*((GoB f
)*(i,j+1)+(GoB f)*(i+1,j+1)) } by A6,A8,A19,A13,GOBOARD6:64,XBOOLE_1:63;
then L~f meets { 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) } by A16,XBOOLE_1:70
;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A20: LSeg( f/.(k+1),(GoB f)*(i,j+1)) = LSeg(f,k0) by A6,A10,A17,A15,A12,
GOBOARD7:40,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A10,A11,A17,A12,A18,A19,A20,A4,A5,GOBOARD7:61;
end;
theorem
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f &
1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+2,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or f/.(k+2) = (GoB f)*(i+2,j+1) & f/.k = (
GoB f)*(i+1,j)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*
(i,j+1)+(GoB f)*(i+1,j+2))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let i,j such that
A6: 1 <= i and
A7: i+2 <= len GoB f and
A8: 1 <= j and
A9: j+2 <= width GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j+1) and
A11: f/.k = (GoB f)*(i+2,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or f/.(k+2) =
(GoB f)*(i+2,j+1) & f/.k = (GoB f)*(i+1,j);
i+1+1 = i+(1+1);
then
A12: i+1 < len GoB f by A7,NAT_1:13;
then
A13: i < len GoB f by NAT_1:13;
j+1 <= j+2 by XREAL_1:6;
then
A14: j+1 <= width GoB f by A9,XXREAL_0:2;
then
A15: L~f misses Int cell(GoB f,i,j+1) by A13,GOBOARD7:12;
j+1+1 = j+(1+1);
then
A16: j+1 < width GoB f by A9,NAT_1:13;
assume LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i,j+1)+(
GoB f)*(i+1,j+2))) meets L~f;
then
A17: L~f meets Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1) \/ { 1/2*((GoB f
)*(i,j+1)+(GoB f)*(i+1,j+1)) } by A6,A8,A16,A13,GOBOARD6:64,XBOOLE_1:63;
j < j+2 by XREAL_1:29;
then
A18: j < width GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i,j) by A13,GOBOARD7:12;
then L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1) by A15,
XBOOLE_1:70;
then
1 <= j+1 & L~f meets { 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) } by A17,
NAT_1:11,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A19: LSeg( f/.(k+1),(GoB f)*(i,j+1)) = LSeg(f,k0) by A6,A10,A14,A12,GOBOARD7:40
,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A10,A11,A18,A12,A19,A4,A5,GOBOARD7:62;
end;
theorem
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+1 <= len GoB f &
1 <= j & j+2 <= width GoB 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+2) = (GoB f)*(i,j) & f/.k = (GoB f)*(i,
j+2)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i,j+1)+(
GoB f)*(i+1,j+2))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let i,j such that
A6: 1 <= i and
A7: i+1 <= len GoB f and
A8: 1 <= j and
A9: j+2 <= width GoB f and
A10: f/.(k+1) = (GoB f)*(i,j+1) and
A11: f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i,j+2) or f/.(k+2) = (
GoB f)*(i,j) & f/.k = (GoB f)*(i,j+2);
A12: i < len GoB f by A7,NAT_1:13;
j < j+2 by XREAL_1:29;
then j <= width GoB f by A9,XXREAL_0:2;
then
A13: L~f misses Int cell(GoB f,i,j) by A12,GOBOARD7:12;
j+1 <= j+2 by XREAL_1:6;
then
A14: j+1 <= width GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i,j+1) by A12,GOBOARD7:12;
then
A15: L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1) by A13,XBOOLE_1:70
;
j+1+1 = j+(1+1);
then
A16: j+1 < width GoB f by A9,NAT_1:13;
assume LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i,j+1)+(
GoB f)*(i+1,j+2))) meets L~f;
then
L~f meets Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1) \/ { 1/2*((GoB f
)*(i,j+1)+(GoB f)*(i+1,j+1)) } by A6,A8,A16,A12,GOBOARD6:64,XBOOLE_1:63;
then 1 <= j+1 & L~f meets { 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) } by A15,
NAT_1:11,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A17: LSeg(f/.(k+1),(GoB f)*(i+1,j+1)) = LSeg(f,k0) by A6,A7,A10,A14,GOBOARD7:40
,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A10,A11,A16,A12,A17,A4,A5,GOBOARD7:59;
end;
theorem
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f &
1 <= j & j+2 <= width GoB 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+2) or f/.(k+2) = (GoB f)*(i,j+1) & f/.k = (
GoB f)*(i+1,j+2)) holds LSeg(1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1)), 1/2*((GoB
f)*(i+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let i,j such that
A6: 1 <= i and
A7: i+2 <= len GoB f and
A8: 1 <= j and
A9: j+2 <= width GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j+1) and
A11: f/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.(k+2) =
(GoB f)*(i,j+1) & f/.k = (GoB f)*(i+1,j+2);
A12: i+1+1 = i+(1+1);
then
A13: i+1 < len GoB f by A7,NAT_1:13;
j < j+2 by XREAL_1:29;
then j < width GoB f by A9,XXREAL_0:2;
then
A14: L~f misses Int cell(GoB f,i+1,j) by A13,GOBOARD7:12;
j+1 <= j+2 by XREAL_1:6;
then
A15: j+1 <= width GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i+1,j+1) by A13,GOBOARD7:12;
then
A16: L~f misses Int cell(GoB f,i+1,j) \/ Int cell(GoB f,i+1,j+1) by A14,
XBOOLE_1:70;
A17: 1 <= j+1 by NAT_1:11;
A18: j+1+1 = j+(1+1);
then
A19: j+1 < width GoB f by A9,NAT_1:13;
A20: 1 <= i+1 by NAT_1:11;
assume LSeg(1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1)), 1/2*((GoB f)*(i+1,j+1
)+(GoB f)*(i+2,j+2))) meets L~f;
then L~f meets Int cell(GoB f,i+1,j) \/ Int cell(GoB f,i+1,j+1) \/ { 1/2*((
GoB f)*(i+1,j+1)+(GoB f)* (i+2,j+1)) } by A8,A12,A13,A19,A20,GOBOARD6:64
,XBOOLE_1:63;
then L~f meets { 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+2,j+1)) } by A16,
XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A21: LSeg(f/.(k+1),(GoB f)*(i+2,j+1)) = LSeg(f,k0) by A7,A10,A17,A15,A12,A20,
GOBOARD7:40,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A10,A11,A17,A13,A18,A19,A21,A4,A5,GOBOARD7:61;
end;
theorem
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f &
1 <= j & j+2 <= width GoB 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+2) = (GoB f)*(i,j+1) & f/.k = (GoB
f)*(i+1,j)) holds LSeg(1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1)), 1/2*((GoB f)*(i
+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let i,j such that
A6: 1 <= i and
A7: i+2 <= len GoB f and
A8: 1 <= j and
A9: j+2 <= width GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j+1) and
A11: f/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or f/.(k+2) = (
GoB f)*(i,j+1) & f/.k = (GoB f)*(i+1,j);
A12: i+1+1 = i+(1+1);
then
A13: i+1 < len GoB f by A7,NAT_1:13;
j+1 <= j+2 by XREAL_1:6;
then
A14: j+1 <= width GoB f by A9,XXREAL_0:2;
then
A15: L~f misses Int cell(GoB f,i+1,j+1) by A13,GOBOARD7:12;
j+1+1 = j+(1+1);
then
A16: j+1 < width GoB f by A9,NAT_1:13;
A17: 1 <= i+1 by NAT_1:11;
j < j+2 by XREAL_1:29;
then
A18: j < width GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i+1,j) by A13,GOBOARD7:12;
then
A19: L~f misses Int cell(GoB f,i+1,j) \/ Int cell(GoB f,i+1,j+1) by A15,
XBOOLE_1:70;
assume LSeg(1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1)), 1/2*((GoB f)*(i+1,j+1
)+(GoB f)*(i+2,j+2))) meets L~f;
then L~f meets Int cell(GoB f,i+1,j) \/ Int cell(GoB f,i+1,j+1) \/ { 1/2*((
GoB f)*(i+1,j+1)+(GoB f)* (i+2,j+1)) } by A8,A12,A13,A16,A17,GOBOARD6:64
,XBOOLE_1:63;
then 1 <= j+1 & L~f meets { 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+2,j+1)) } by
A19,NAT_1:11,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A20: LSeg(f/.(k+1),(GoB f)*(i+2,j+1)) = LSeg(f,k0) by A7,A10,A14,A12,A17,
GOBOARD7:40,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A10,A11,A18,A13,A20,A4,A5,GOBOARD7:62;
end;
theorem
for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f
/.(k+1) = (GoB f)*(i+1,1) & (f/.k = (GoB f)*(i+2,1) & f/.(k+2) = (GoB f)*(i+1,2
) or f/.(k+2) = (GoB f)*(i+2,1) & f/.k = (GoB f)*(i+1,2)) holds LSeg(1/2*((GoB
f)*(i,1)+(GoB f)*(i+1,1))- |[0,1]|, 1/2*((GoB f)*(i,1)+(GoB f)*(i+1,2))) misses
L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
A6: 1 < width GoB f by GOBOARD7:33;
let i such that
A7: 1 <= i and
A8: i+2 <= len GoB f and
A9: f/.(k+1) = (GoB f)*(i+1,1) and
A10: f/.k = (GoB f)*(i+2,1) & f/.(k+2) = (GoB f)*(i+1,2) or f/.(k+2) = (
GoB f)*(i+2,1) & f/.k = (GoB f)*(i+1,2);
i+1+1 = i+(1+1);
then
A11: i+1 < len GoB f by A8,NAT_1:13;
then
A12: i < len GoB f by NAT_1:13;
width GoB f <> 0 by MATRIX_0:def 10;
then
A13: 0+1 <= width GoB f by NAT_1:14;
then
A14: L~f misses Int cell(GoB f,i,1) by A12,GOBOARD7:12;
0 < width GoB f by A13;
then L~f misses Int cell(GoB f,i,0) by A12,GOBOARD7:12;
then
A15: L~f misses Int cell(GoB f,i,0) \/ Int cell(GoB f,i,1) by A14,XBOOLE_1:70;
assume LSeg(1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1))- |[0,1]|, 1/2*((GoB f)*(i,
1)+(GoB f)*(i+1,2))) meets L~f;
then
L~f meets Int cell(GoB f,i,0) \/ Int cell(GoB f,i,1) \/ { 1/2*((GoB f)*
(i,1)+(GoB f)*(i+1,1)) } by A7,A6,A12,GOBOARD6:66,XBOOLE_1:63;
then L~f meets { 1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1)) } by A15,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A16: LSeg(f/.(k+1),(GoB f)*(i,1)) = LSeg(f,k0) by A7,A9,A13,A11,GOBOARD7:40
,ZFMISC_1:50;
A17: LSeg(f,k+1) c= L~f & 1+1 = 2 by TOPREAL3:19;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A7,A9,A10,A11,A6,A16,A17,A4,A5,GOBOARD7:61;
end;
theorem
for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f
/.(k+1) = (GoB f)*(i+1,1) & (f/.k = (GoB f)*(i,1) & f/.(k+2) = (GoB f)*(i+1,2)
or f/.(k+2) = (GoB f)*(i,1) & f/.k = (GoB f)*(i+1,2)) holds LSeg(1/2*((GoB f)*(
i+1,1)+(GoB f)*(i+2,1))- |[0,1]|, 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,2))) misses
L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
A6: 1 < width GoB f by GOBOARD7:33;
let i such that
A7: 1 <= i and
A8: i+2 <= len GoB f and
A9: f/.(k+1) = (GoB f)*(i+1,1) and
A10: f/.k = (GoB f)*(i,1) & f/.(k+2) = (GoB f)*(i+1,2) or f/.(k+2) = (GoB
f)*(i,1) & f/.k = (GoB f)*(i+1,2);
A11: i+1+1 = i+(1+1);
then
A12: i+1 < len GoB f by A8,NAT_1:13;
width GoB f <> 0 by MATRIX_0:def 10;
then
A13: 0+1 <= width GoB f by NAT_1:14;
then
A14: L~f misses Int cell(GoB f,i+1,1) by A12,GOBOARD7:12;
0 < width GoB f by A13;
then L~f misses Int cell(GoB f,i+1,0) by A12,GOBOARD7:12;
then
A15: L~f misses Int cell(GoB f,i+1,0) \/ Int cell(GoB f,i+1,1) by A14,
XBOOLE_1:70;
A16: 1 <= i+1 by NAT_1:11;
assume LSeg(1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1))- |[0,1]|, 1/2*((GoB f)*(
i+1,1)+(GoB f)*(i+2,2))) meets L~f;
then
L~f meets Int cell(GoB f,i+1,0) \/ Int cell(GoB f,i+1,1) \/ { 1/2*((GoB
f)*(i+1,1)+(GoB f)*(i+2,1)) } by A11,A12,A6,A16,GOBOARD6:66,XBOOLE_1:63;
then L~f meets { 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1)) } by A15,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A17: LSeg(f/.(k+1),(GoB f)*(i+2,1)) = LSeg(f,k0) by A8,A9,A13,A11,A16,
GOBOARD7:40,ZFMISC_1:50;
A18: LSeg(f,k+1) c= L~f & 1+1 = 2 by TOPREAL3:19;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A7,A9,A10,A12,A6,A17,A4,A18,A5,GOBOARD7:61;
end;
theorem
for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f
/.(k+1) = (GoB f)*(i+1,width GoB f) & (f/.k = (GoB f)*(i+2,width GoB f) & f/.(k
+2) = (GoB f)*(i+1,width GoB f -' 1) or f/.(k+2) = (GoB f)*(i+2,width GoB f) &
f/.k = (GoB f)*(i+1,width GoB f -' 1)) holds LSeg(1/2*((GoB f)*(i,width GoB f
-' 1)+(GoB f)*(i+1,width GoB f)), 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,
width GoB f))+|[0,1]|) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let i such that
A6: 1 <= i and
A7: i+2 <= len GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,width GoB f) and
A9: f/.k = (GoB f)*(i+2,width GoB f) & f/.(k+2) = (GoB f)*(i+1,width GoB
f -' 1) or f/.(k+2) = (GoB f)*(i+2,width GoB f) & f/.k = (GoB f)*(i+1,width GoB
f -' 1);
i+1+1 = i+(1+1);
then
A10: i+1 < len GoB f by A7,NAT_1:13;
then
A11: i < len GoB f by NAT_1:13;
then
A12: L~f misses Int cell(GoB f,i,width GoB f) by GOBOARD7:12;
assume
A13: LSeg(1/2*((GoB f)*(i,width GoB f -' 1)+(GoB f)*(i+1,width GoB f)),
1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f))+|[0,1]|) meets L~f;
A14: 1 < width GoB f by GOBOARD7:33;
then
A15: width GoB f -'1 +1 = width GoB f by XREAL_1:235;
then
A16: width GoB f -' 1 < width GoB f by NAT_1:13;
then L~f misses Int cell(GoB f,i,width GoB f -' 1) by A11,GOBOARD7:12;
then
A17: L~f misses Int cell(GoB f,i,width GoB f -' 1) \/ Int cell(GoB f,i,width
GoB f) by A12,XBOOLE_1:70;
A18: 1 <= width GoB f -' 1 by A14,A15,NAT_1:13;
then 1/2*((GoB f)*(i,width GoB f -' 1)+(GoB f)*(i+1,width GoB f)) = 1/2*((
GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f -' 1)) by A6,A15,A10,
GOBOARD7:9;
then L~f meets Int cell(GoB f,i,width GoB f -' 1) \/ Int cell(GoB f,i,width
GoB f) \/ { 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f)) } by A6,A14
,A11,A13,GOBOARD6:67,XBOOLE_1:63;
then L~f meets { 1/2*((GoB f)*(i,width GoB f)+(GoB f)* (i+1,width GoB f)) }
by A17,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A19: LSeg(f/.(k+1),(GoB f)*(i,width GoB f)) = LSeg(f,k0) by A6,A8,A14,A10,
GOBOARD7:40,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A9,A15,A18,A16,A10,A19,A4,A5,GOBOARD7:62;
end;
theorem
for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f
/.(k+1) = (GoB f)*(i+1,width GoB f) & (f/.k = (GoB f)*(i,width GoB f) & f/.(k+2
) = (GoB f)*(i+1,width GoB f -' 1) or f/.(k+2) = (GoB f)*(i,width GoB f) & f/.k
= (GoB f)*(i+1,width GoB f -' 1)) holds LSeg(1/2*((GoB f)*(i+1,width GoB f -' 1
)+(GoB f)*(i+2,width GoB f)), 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width
GoB f))+|[0,1]|) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let i such that
A6: 1 <= i and
A7: i+2 <= len GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,width GoB f) and
A9: f/.k = (GoB f)*(i,width GoB f) & f/.(k+2) = (GoB f)*(i+1,width GoB f
-' 1) or f/.(k+2) = (GoB f)*(i,width GoB f) & f/.k = (GoB f)*(i+1,width GoB f
-' 1);
A10: i+1+1 = i+(1+1);
then
A11: i+1 < len GoB f by A7,NAT_1:13;
then
A12: L~f misses Int cell(GoB f,i+1,width GoB f) by GOBOARD7:12;
A13: 1 <= width GoB f by GOBOARD7:33;
then
A14: width GoB f -'1 +1 = width GoB f by XREAL_1:235;
then
A15: width GoB f -' 1 < width GoB f by NAT_1:13;
then L~f misses Int cell(GoB f,i+1,width GoB f -' 1) by A11,GOBOARD7:12;
then
A16: L~f misses Int cell(GoB f,i+1,width GoB f -' 1) \/ Int cell(GoB f,i+1,
width GoB f) by A12,XBOOLE_1:70;
assume
A17: LSeg(1/2*((GoB f)*(i+1,width GoB f -' 1)+(GoB f)*(i+2,width GoB f))
, 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width GoB f))+|[0,1]|) meets L~f;
A18: 1 <= i+1 by NAT_1:11;
A19: 1 < width GoB f by GOBOARD7:33;
then
A20: 1 <= width GoB f -' 1 by A14,NAT_1:13;
then
1/2*((GoB f)*(i+1,width GoB f -' 1)+(GoB f)*(i+2,width GoB f)) = 1/2*((
GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width GoB f -' 1)) by A7,A14,A10,A18,
GOBOARD7:9;
then L~f meets Int cell(GoB f,i+1,width GoB f -' 1) \/ Int cell(GoB f,i+1,
width GoB f) \/ { 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width GoB f)) }
by A19,A10,A11,A18,A17,GOBOARD6:67,XBOOLE_1:63;
then L~f meets {1/2*((GoB f)*(i+1,width GoB f)+(GoB f)* (i+2,width GoB f))}
by A16,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A21: LSeg(f/.(k+1),(GoB f)*(i+2,width GoB f)) = LSeg(f,k0) by A7,A8,A13,A10,A18
,GOBOARD7:40,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A9,A14,A20,A15,A11,A21,A4,A5,GOBOARD7:62;
end;
theorem
for k st 1 <= k & k+2 <= len f for i,j st 1 <= j & j+1 <= width GoB f
& 1 <= i & i+2 <= len GoB 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+2) = (GoB f)*(i,j+1) & f/.k = (
GoB f)*(i+2,j+1)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f
)*(i+1,j)+(GoB f)*(i+2,j+1))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let i,j such that
A6: 1 <= j and
A7: j+1 <= width GoB f and
A8: 1 <= i and
A9: i+2 <= len GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j+1) and
A11: f/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2) =
(GoB f)*(i,j+1) & f/.k = (GoB f)*(i+2,j+1);
A12: j < width GoB f by A7,NAT_1:13;
i < i+2 by XREAL_1:29;
then i <= len GoB f by A9,XXREAL_0:2;
then
A13: L~f misses Int cell(GoB f,i,j) by A12,GOBOARD7:12;
i+1 <= i+2 by XREAL_1:6;
then
A14: i+1 <= len GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i+1,j) by A12,GOBOARD7:12;
then
A15: L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j) by A13,XBOOLE_1:70
;
i+1+1 = i+(1+1);
then
A16: i+1 < len GoB f by A9,NAT_1:13;
assume LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i+1,j)+(
GoB f)*(i+2,j+1))) meets L~f;
then
L~f meets Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j) \/ { 1/2*((GoB f
)*(i+1,j)+(GoB f)*(i+1,j+1)) } by A6,A8,A16,A12,GOBOARD6:65,XBOOLE_1:63;
then 1 <= i+1 & L~f meets { 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) } by A15,
NAT_1:11,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A17: LSeg(f/.(k+1),(GoB f)*(i+1,j)) = LSeg(f,k0) by A6,A7,A10,A14,GOBOARD7:39
,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A10,A11,A16,A12,A17,A4,A5,GOBOARD7:62;
end;
theorem
for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f
& 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+1,j+2) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2) = (GoB f)*(i+1,j+2) & f/.k =
(GoB f)*(i+2,j+1)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB
f)*(i+1,j)+(GoB f)*(i+2,j+1))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let j,i such that
A6: 1 <= j and
A7: j+2 <= width GoB f and
A8: 1 <= i and
A9: i+2 <= len GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j+1) and
A11: f/.k = (GoB f)*(i+1,j+2) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2)
= (GoB f)*(i+1,j+2) & f/.k = (GoB f)*(i+2,j+1);
j+1+1 = j+(1+1);
then
A12: j+1 < width GoB f by A7,NAT_1:13;
then
A13: j < width GoB f by NAT_1:13;
i < i+2 by XREAL_1:29;
then i < len GoB f by A9,XXREAL_0:2;
then
A14: L~f misses Int cell(GoB f,i,j) by A13,GOBOARD7:12;
i+1 <= i+2 by XREAL_1:6;
then
A15: i+1 <= len GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i+1,j) by A13,GOBOARD7:12;
then
A16: L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j) by A14,XBOOLE_1:70
;
A17: 1 <= i+1 by NAT_1:11;
A18: i+1+1 = i+(1+1);
then
A19: i+1 < len GoB f by A9,NAT_1:13;
assume LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i+1,j)+(
GoB f)*(i+2,j+1))) meets L~f;
then
L~f meets Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j) \/ { 1/2*((GoB f
)*(i+1,j)+(GoB f)*(i+1,j+1)) } by A6,A8,A19,A13,GOBOARD6:65,XBOOLE_1:63;
then L~f meets { 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) } by A16,XBOOLE_1:70
;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A20: LSeg( f/.(k+1),(GoB f)*(i+1,j)) = LSeg(f,k0) by A6,A10,A17,A15,A12,
GOBOARD7:39,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A10,A11,A17,A12,A18,A19,A20,A4,A5,GOBOARD7:59;
end;
theorem
for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f
& 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+1,j+2) & f/.(k+2) = (GoB f)*(i,j+1) or f/.(k+2) = (GoB f)*(i+1,j+2) & f/.k = (
GoB f)*(i,j+1)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*
(i+1,j)+(GoB f)*(i+2,j+1))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let j,i such that
A6: 1 <= j and
A7: j+2 <= width GoB f and
A8: 1 <= i and
A9: i+2 <= len GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j+1) and
A11: f/.k = (GoB f)*(i+1,j+2) & f/.(k+2) = (GoB f)*(i,j+1) or f/.(k+2) =
(GoB f)*(i+1,j+2) & f/.k = (GoB f)*(i,j+1);
j+1+1 = j+(1+1);
then
A12: j+1 < width GoB f by A7,NAT_1:13;
then
A13: j < width GoB f by NAT_1:13;
i+1 <= i+2 by XREAL_1:6;
then
A14: i+1 <= len GoB f by A9,XXREAL_0:2;
then
A15: L~f misses Int cell(GoB f,i+1,j) by A13,GOBOARD7:12;
i+1+1 = i+(1+1);
then
A16: i+1 < len GoB f by A9,NAT_1:13;
assume LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i+1,j)+(
GoB f)*(i+2,j+1))) meets L~f;
then
A17: L~f meets Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j) \/ { 1/2*((GoB f
)*(i+1,j)+(GoB f)*(i+1,j+1)) } by A6,A8,A16,A13,GOBOARD6:65,XBOOLE_1:63;
i < i+2 by XREAL_1:29;
then
A18: i < len GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i,j) by A13,GOBOARD7:12;
then L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j) by A15,
XBOOLE_1:70;
then
1 <= i+1 & L~f meets { 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) } by A17,
NAT_1:11,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A19: LSeg( f/.(k+1),(GoB f)*(i+1,j)) = LSeg(f,k0) by A6,A10,A14,A12,GOBOARD7:39
,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A10,A11,A18,A12,A19,A4,A5,GOBOARD7:60;
end;
theorem
for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+1 <= width GoB f
& 1 <= i & i+2 <= len GoB 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+2) = (GoB f)*(i,j) & f/.k = (GoB f)*(i+
2,j)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i+1,j)+(
GoB f)*(i+2,j+1))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let j,i such that
A6: 1 <= j and
A7: j+1 <= width GoB f and
A8: 1 <= i and
A9: i+2 <= len GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j) and
A11: f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+2,j) or f/.(k+2) = (
GoB f)*(i,j) & f/.k = (GoB f)*(i+2,j);
A12: j < width GoB f by A7,NAT_1:13;
i < i+2 by XREAL_1:29;
then i <= len GoB f by A9,XXREAL_0:2;
then
A13: L~f misses Int cell(GoB f,i,j) by A12,GOBOARD7:12;
i+1 <= i+2 by XREAL_1:6;
then
A14: i+1 <= len GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i+1,j) by A12,GOBOARD7:12;
then
A15: L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j) by A13,XBOOLE_1:70
;
i+1+1 = i+(1+1);
then
A16: i+1 < len GoB f by A9,NAT_1:13;
assume LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i+1,j)+(
GoB f)*(i+2,j+1))) meets L~f;
then
L~f meets Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j) \/ { 1/2*((GoB f
)*(i+1,j)+(GoB f)*(i+1,j+1)) } by A6,A8,A16,A12,GOBOARD6:65,XBOOLE_1:63;
then 1 <= i+1 & L~f meets { 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) } by A15,
NAT_1:11,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A17: LSeg(f/.(k+1),(GoB f)*(i+1,j+1)) = LSeg(f,k0) by A6,A7,A10,A14,GOBOARD7:39
,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A10,A11,A16,A12,A17,A4,A5,GOBOARD7:61;
end;
theorem
for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f
& 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+1,j) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2) = (GoB f)*(i+1,j) & f/.k = (
GoB f)*(i+2,j+1)) holds LSeg(1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2)), 1/2*((GoB
f)*(i+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let j,i such that
A6: 1 <= j and
A7: j+2 <= width GoB f and
A8: 1 <= i and
A9: i+2 <= len GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j+1) and
A11: f/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2) =
(GoB f)*(i+1,j) & f/.k = (GoB f)*(i+2,j+1);
A12: j+1+1 = j+(1+1);
then
A13: j+1 < width GoB f by A7,NAT_1:13;
i < i+2 by XREAL_1:29;
then i < len GoB f by A9,XXREAL_0:2;
then
A14: L~f misses Int cell(GoB f,i,j+1) by A13,GOBOARD7:12;
i+1 <= i+2 by XREAL_1:6;
then
A15: i+1 <= len GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i+1,j+1) by A13,GOBOARD7:12;
then
A16: L~f misses Int cell(GoB f,i,j+1) \/ Int cell(GoB f,i+1,j+1) by A14,
XBOOLE_1:70;
A17: 1 <= i+1 by NAT_1:11;
A18: i+1+1 = i+(1+1);
then
A19: i+1 < len GoB f by A9,NAT_1:13;
A20: 1 <= j+1 by NAT_1:11;
assume LSeg(1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2)), 1/2*((GoB f)*(i+1,j+1
)+(GoB f)*(i+2,j+2))) meets L~f;
then L~f meets Int cell(GoB f,i,j+1) \/ Int cell(GoB f,i+1,j+1) \/ { 1/2*((
GoB f)*(i+1,j+1)+(GoB f)* (i+1,j+2)) } by A8,A12,A13,A19,A20,GOBOARD6:65
,XBOOLE_1:63;
then L~f meets { 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+1,j+2)) } by A16,
XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A21: LSeg(f/.(k+1),(GoB f)*(i+1,j+2)) = LSeg(f,k0) by A7,A10,A17,A15,A12,A20,
GOBOARD7:39,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A10,A11,A17,A13,A18,A19,A21,A4,A5,GOBOARD7:59;
end;
theorem
for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f
& 1 <= i & i+2 <= len GoB 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+2) = (GoB f)*(i+1,j) & f/.k = (GoB
f)*(i,j+1)) holds LSeg(1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2)), 1/2*((GoB f)*(i
+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let j,i such that
A6: 1 <= j and
A7: j+2 <= width GoB f and
A8: 1 <= i and
A9: i+2 <= len GoB f and
A10: f/.(k+1) = (GoB f)*(i+1,j+1) and
A11: f/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j+1) or f/.(k+2) = (
GoB f)*(i+1,j) & f/.k = (GoB f)*(i,j+1);
A12: j+1+1 = j+(1+1);
then
A13: j+1 < width GoB f by A7,NAT_1:13;
i+1 <= i+2 by XREAL_1:6;
then
A14: i+1 <= len GoB f by A9,XXREAL_0:2;
then
A15: L~f misses Int cell(GoB f,i+1,j+1) by A13,GOBOARD7:12;
i+1+1 = i+(1+1);
then
A16: i+1 < len GoB f by A9,NAT_1:13;
A17: 1 <= j+1 by NAT_1:11;
i < i+2 by XREAL_1:29;
then
A18: i < len GoB f by A9,XXREAL_0:2;
then L~f misses Int cell(GoB f,i,j+1) by A13,GOBOARD7:12;
then
A19: L~f misses Int cell(GoB f,i,j+1) \/ Int cell(GoB f,i+1,j+1) by A15,
XBOOLE_1:70;
assume LSeg(1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2)), 1/2*((GoB f)*(i+1,j+1
)+(GoB f)*(i+2,j+2))) meets L~f;
then L~f meets Int cell(GoB f,i,j+1) \/ Int cell(GoB f,i+1,j+1) \/ { 1/2*((
GoB f)*(i+1,j+1)+(GoB f)* (i+1,j+2)) } by A8,A12,A13,A16,A17,GOBOARD6:65
,XBOOLE_1:63;
then 1 <= i+1 & L~f meets { 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+1,j+2)) } by
A19,NAT_1:11,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A20: LSeg(f/.(k+1),(GoB f)*(i+1,j+2)) = LSeg(f,k0) by A7,A10,A14,A12,A17,
GOBOARD7:39,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A10,A11,A18,A13,A20,A4,A5,GOBOARD7:60;
end;
theorem
for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f &
f/.(k+1) = (GoB f)*(1,j+1) & (f/.k = (GoB f)*(1,j+2) & f/.(k+2) = (GoB f)*(2,j+
1) or f/.(k+2) = (GoB f)*(1,j+2) & f/.k = (GoB f)*(2,j+1)) holds LSeg(1/2*((GoB
f)*(1,j)+(GoB f)*(1,j+1))- |[1,0]|, 1/2*((GoB f)*(1,j)+(GoB f)*(2,j+1))) misses
L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
A6: 1 < len GoB f by GOBOARD7:32;
let j such that
A7: 1 <= j and
A8: j+2 <= width GoB f and
A9: f/.(k+1) = (GoB f)*(1,j+1) and
A10: f/.k = (GoB f)*(1,j+2) & f/.(k+2) = (GoB f)*(2,j+1) or f/.(k+2) = (
GoB f)*(1,j+2) & f/.k = (GoB f)*(2,j+1);
j+1+1 = j+(1+1);
then
A11: j+1 < width GoB f by A8,NAT_1:13;
then
A12: j < width GoB f by NAT_1:13;
len GoB f <> 0 by MATRIX_0:def 10;
then
A13: 0+1 <= len GoB f by NAT_1:14;
then
A14: L~f misses Int cell(GoB f,1,j) by A12,GOBOARD7:12;
0 < len GoB f by A13;
then L~f misses Int cell(GoB f,0,j) by A12,GOBOARD7:12;
then
A15: L~f misses Int cell(GoB f,0,j) \/ Int cell(GoB f,1,j) by A14,XBOOLE_1:70;
assume LSeg(1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1))- |[1,0]|, 1/2*((GoB f)*(1,
j)+(GoB f)*(2,j+1))) meets L~f;
then
L~f meets Int cell(GoB f,0,j) \/ Int cell(GoB f,1,j) \/ { 1/2*((GoB f)*
(1,j)+(GoB f)*(1,j+1)) } by A7,A6,A12,GOBOARD6:68,XBOOLE_1:63;
then L~f meets { 1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1)) } by A15,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A16: LSeg(f/.(k+1),(GoB f)*(1,j)) = LSeg(f,k0) by A7,A9,A13,A11,GOBOARD7:39
,ZFMISC_1:50;
A17: LSeg(f,k+1) c= L~f & 1+1 = 2 by TOPREAL3:19;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A7,A9,A10,A11,A6,A16,A17,A4,A5,GOBOARD7:59;
end;
theorem
for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f &
f/.(k+1) = (GoB f)*(1,j+1) & (f/.k = (GoB f)*(1,j) & f/.(k+2) = (GoB f)*(2,j+1)
or f/.(k+2) = (GoB f)*(1,j) & f/.k = (GoB f)*(2,j+1)) holds LSeg(1/2*((GoB f)*(
1,j+1)+(GoB f)*(1,j+2))- |[1,0]|, 1/2*((GoB f)*(1,j+1)+(GoB f)*(2,j+2))) misses
L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
A6: 1 < len GoB f by GOBOARD7:32;
let j such that
A7: 1 <= j and
A8: j+2 <= width GoB f and
A9: f/.(k+1) = (GoB f)*(1,j+1) and
A10: f/.k = (GoB f)*(1,j) & f/.(k+2) = (GoB f)*(2,j+1) or f/.(k+2) = (GoB
f)*(1,j) & f/.k = (GoB f)*(2,j+1);
A11: j+1+1 = j+(1+1);
then
A12: j+1 < width GoB f by A8,NAT_1:13;
len GoB f <> 0 by MATRIX_0:def 10;
then
A13: 0+1 <= len GoB f by NAT_1:14;
then
A14: L~f misses Int cell(GoB f,1,j+1) by A12,GOBOARD7:12;
0 < len GoB f by A13;
then L~f misses Int cell(GoB f,0,j+1) by A12,GOBOARD7:12;
then
A15: L~f misses Int cell(GoB f,0,j+1) \/ Int cell(GoB f,1,j+1) by A14,
XBOOLE_1:70;
A16: 1 <= j+1 by NAT_1:11;
assume LSeg(1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2))- |[1,0]|, 1/2*((GoB f)*(
1,j+1)+(GoB f)*(2,j+2))) meets L~f;
then
L~f meets Int cell(GoB f,0,j+1) \/ Int cell(GoB f,1,j+1) \/ { 1/2*((GoB
f)*(1,j+1)+(GoB f)*(1,j+2)) } by A11,A12,A6,A16,GOBOARD6:68,XBOOLE_1:63;
then L~f meets { 1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2)) } by A15,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A17: LSeg(f/.(k+1),(GoB f)*(1,j+2)) = LSeg(f,k0) by A8,A9,A13,A11,A16,
GOBOARD7:39,ZFMISC_1:50;
A18: LSeg(f,k+1) c= L~f & 1+1 = 2 by TOPREAL3:19;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A7,A9,A10,A12,A6,A17,A4,A18,A5,GOBOARD7:59;
end;
theorem
for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f &
f/.(k+1) = (GoB f)*(len GoB f,j+1) & (f/.k = (GoB f)*(len GoB f,j+2) & f/.(k+2)
= (GoB f)*(len GoB f -' 1,j+1) or f/.(k+2) = (GoB f)*(len GoB f,j+2) & f/.k = (
GoB f)*(len GoB f -' 1,j+1)) holds LSeg(1/2*((GoB f)*(len GoB f -' 1,j)+(GoB f)
*(len GoB f,j+1)), 1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1))+|[1,0]|)
misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let j such that
A6: 1 <= j and
A7: j+2 <= width GoB f and
A8: f/.(k+1) = (GoB f)*(len GoB f,j+1) and
A9: f/.k = (GoB f)*(len GoB f,j+2) & f/.(k+2) = (GoB f)*(len GoB f -' 1,
j+1) or f/.(k+2) = (GoB f)*(len GoB f,j+2) & f/.k = (GoB f)*(len GoB f -' 1,j+1
);
j+1+1 = j+(1+1);
then
A10: j+1 < width GoB f by A7,NAT_1:13;
then
A11: j < width GoB f by NAT_1:13;
then
A12: L~f misses Int cell(GoB f,len GoB f,j) by GOBOARD7:12;
assume
A13: LSeg(1/2*((GoB f)*(len GoB f -' 1,j)+(GoB f)*(len GoB f,j+1)), 1/2*
((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1))+|[1,0]|) meets L~f;
A14: 1 < len GoB f by GOBOARD7:32;
then
A15: len GoB f -'1 +1 = len GoB f by XREAL_1:235;
then
A16: len GoB f -' 1 < len GoB f by NAT_1:13;
then L~f misses Int cell(GoB f,len GoB f -' 1,j) by A11,GOBOARD7:12;
then
A17: L~f misses Int cell(GoB f,len GoB f -' 1,j) \/ Int cell(GoB f,len GoB f
,j) by A12,XBOOLE_1:70;
A18: 1 <= len GoB f -' 1 by A14,A15,NAT_1:13;
then
1/2*((GoB f)*(len GoB f -' 1,j)+(GoB f)*(len GoB f,j+1)) = 1/2*((GoB f)
*(len GoB f -' 1,j+1)+(GoB f)*(len GoB f,j)) by A6,A15,A10,GOBOARD7:9;
then
L~f meets Int cell(GoB f,len GoB f -' 1,j) \/ Int cell(GoB f,len GoB f,
j) \/ { 1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1)) } by A6,A14,A11,A13
,GOBOARD6:69,XBOOLE_1:63;
then L~f meets { 1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1)) } by A17
,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A19: LSeg(f/.(k+1),(GoB f)*(len GoB f,j)) = LSeg(f,k0) by A6,A8,A14,A10,
GOBOARD7:39,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A9,A15,A18,A16,A10,A19,A4,A5,GOBOARD7:60;
end;
theorem
for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f &
f/.(k+1) = (GoB f)*(len GoB f,j+1) & (f/.k = (GoB f)*(len GoB f,j) & f/.(k+2) =
(GoB f)*(len GoB f -' 1,j+1) or f/.(k+2) = (GoB f)*(len GoB f,j) & f/.k = (GoB
f)*(len GoB f -' 1,j+1)) holds LSeg(1/2*((GoB f)*(len GoB f -' 1,j+1)+(GoB f)*(
len GoB f,j+2)), 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))+|[1,0]|)
misses L~f
proof
let k such that
A1: k >= 1 and
A2: k+2 <= len f;
A3: k+1+1 = k+(1+1);
then k+1 < len f by A2,NAT_1:13;
then
A4: LSeg(f,k+1) c= L~f & LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,TOPREAL1:def 3
,TOPREAL3:19;
1 <= k+1 by NAT_1:11;
then
A5: LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,TOPREAL1:def 3;
let j such that
A6: 1 <= j and
A7: j+2 <= width GoB f and
A8: f/.(k+1) = (GoB f)*(len GoB f,j+1) and
A9: f/.k = (GoB f)*(len GoB f,j) & f/.(k+2) = (GoB f)*(len GoB f -' 1,j+
1) or f/.(k+2) = (GoB f)*(len GoB f,j) & f/.k = (GoB f)*(len GoB f -' 1,j+1);
A10: j+1+1 = j+(1+1);
then
A11: j+1 < width GoB f by A7,NAT_1:13;
then
A12: L~f misses Int cell(GoB f,len GoB f,j+1) by GOBOARD7:12;
A13: 1 <= len GoB f by GOBOARD7:32;
then
A14: len GoB f -'1 +1 = len GoB f by XREAL_1:235;
then
A15: len GoB f -' 1 < len GoB f by NAT_1:13;
then L~f misses Int cell(GoB f,len GoB f -' 1,j+1) by A11,GOBOARD7:12;
then
A16: L~f misses Int cell(GoB f,len GoB f -' 1,j+1) \/ Int cell(GoB f,len GoB
f,j+1) by A12,XBOOLE_1:70;
assume
A17: LSeg(1/2*((GoB f)*(len GoB f -' 1,j+1)+(GoB f)*(len GoB f,j+2)), 1/
2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))+|[1,0]|) meets L~f;
A18: 1 <= j+1 by NAT_1:11;
A19: 1 < len GoB f by GOBOARD7:32;
then
A20: 1 <= len GoB f -' 1 by A14,NAT_1:13;
then 1/2*((GoB f)*(len GoB f -' 1,j+1)+(GoB f)*(len GoB f,j+2)) = 1/2*((GoB
f)*(len GoB f,j+1)+(GoB f)*(len GoB f -' 1,j+2)) by A7,A14,A10,A18,GOBOARD7:9
;
then L~f meets Int cell(GoB f,len GoB f -' 1,j+1) \/ Int cell(GoB f,len GoB
f,j+1) \/ { 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2)) } by A19,A10
,A11,A18,A17,GOBOARD6:69,XBOOLE_1:63;
then L~f meets {1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))} by A16
,XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0+1 <= len f and
A21: LSeg(f/.(k+1),(GoB f)*(len GoB f,j+2)) = LSeg(f,k0) by A7,A8,A13,A10,A18,
GOBOARD7:39,ZFMISC_1:50;
LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f by TOPREAL3:19;
hence contradiction by A6,A8,A9,A14,A20,A15,A11,A21,A4,A5,GOBOARD7:60;
end;
reserve P for Subset of TOP-REAL 2;
theorem Th21:
(for p st p in P holds p`1 < (GoB f)*(1,1)`1) implies P misses L~f
proof
assume
A1: for p st p in P holds p`1 < (GoB f)*(1,1)`1;
assume P meets L~f;
then consider x being object such that
A2: x in P and
A3: x in L~f by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A2;
A4: x`1 < (GoB f)*(1,1)`1 by A1,A2;
A5: 1 < width GoB f by GOBOARD7:33;
A6: f is_sequence_on GoB f by GOBOARD5:def 5;
consider i such that
A7: 1 <= i and
A8: i+1 <= len f and
A9: x in LSeg(f/.i,f/.(i+1)) by A3,SPPOL_2:14;
per cases;
suppose
(f/.i)`1 <= (f/.(i+1))`1;
then
A10: (f/.i)`1 <= x `1 by A9,TOPREAL1:3;
i <= len f by A8,NAT_1:13;
then i in dom f by A7,FINSEQ_3:25;
then consider i1,j1 such that
A11: [i1,j1] in Indices GoB f and
A12: f/.i = (GoB f)*(i1,j1) by A6,GOBOARD1:def 9;
A13: 1 <= i1 by A11,MATRIX_0:32;
A14: i1 <= len GoB f by A11,MATRIX_0:32;
1 <= j1 & j1 <= width GoB f by A11,MATRIX_0:32;
then
A15: (f/.i)`1 = (GoB f)*(i1,1)`1 by A12,A13,A14,GOBOARD5:2;
then 1 < i1 by A4,A10,A13,XXREAL_0:1;
then (GoB f)*(1,1)`1 < (f/.i)`1 by A5,A14,A15,GOBOARD5:3;
hence contradiction by A1,A2,A10,XXREAL_0:2;
end;
suppose
(f/.i)`1 >= (f/.(i+1))`1;
then
A16: (f/.(i+1))`1 <= x `1 by A9,TOPREAL1:3;
1 <= i+1 by NAT_1:11;
then i+1 in dom f by A8,FINSEQ_3:25;
then consider i1,j1 such that
A17: [i1,j1] in Indices GoB f and
A18: f/.(i+1) = (GoB f)*(i1,j1) by A6,GOBOARD1:def 9;
A19: 1 <= i1 by A17,MATRIX_0:32;
A20: i1 <= len GoB f by A17,MATRIX_0:32;
1 <= j1 & j1 <= width GoB f by A17,MATRIX_0:32;
then
A21: (f/.(i+1))`1 = (GoB f)*(i1,1)`1 by A18,A19,A20,GOBOARD5:2;
then 1 < i1 by A4,A16,A19,XXREAL_0:1;
then (GoB f)*(1,1)`1 < (f/.(i+1))`1 by A5,A20,A21,GOBOARD5:3;
hence contradiction by A1,A2,A16,XXREAL_0:2;
end;
end;
theorem Th22:
(for p st p in P holds p`1 > (GoB f)*(len GoB f,1)`1) implies P misses L~f
proof
assume
A1: for p st p in P holds p`1 > (GoB f)*(len GoB f,1)`1;
assume P meets L~f;
then consider x being object such that
A2: x in P and
A3: x in L~f by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A2;
A4: x`1 > (GoB f)*(len GoB f,1)`1 by A1,A2;
A5: 1 < width GoB f by GOBOARD7:33;
A6: f is_sequence_on GoB f by GOBOARD5:def 5;
consider i such that
A7: 1 <= i and
A8: i+1 <= len f and
A9: x in LSeg(f/.i,f/.(i+1)) by A3,SPPOL_2:14;
per cases;
suppose
(f/.i)`1 >= (f/.(i+1))`1;
then
A10: (f/.i)`1 >= x `1 by A9,TOPREAL1:3;
i <= len f by A8,NAT_1:13;
then i in dom f by A7,FINSEQ_3:25;
then consider i1,j1 such that
A11: [i1,j1] in Indices GoB f and
A12: f/.i = (GoB f)*(i1,j1) by A6,GOBOARD1:def 9;
A13: 1 <= i1 by A11,MATRIX_0:32;
A14: i1 <= len GoB f by A11,MATRIX_0:32;
1 <= j1 & j1 <= width GoB f by A11,MATRIX_0:32;
then
A15: (f/.i)`1 = (GoB f)*(i1,1)`1 by A12,A13,A14,GOBOARD5:2;
then i1 < len GoB f by A4,A10,A14,XXREAL_0:1;
then (GoB f)*(len GoB f,1)`1 > (f/.i)`1 by A5,A13,A15,GOBOARD5:3;
hence contradiction by A1,A2,A10,XXREAL_0:2;
end;
suppose
(f/.i)`1 <= (f/.(i+1))`1;
then
A16: (f/.(i+1))`1 >= x `1 by A9,TOPREAL1:3;
1 <= i+1 by NAT_1:11;
then i+1 in dom f by A8,FINSEQ_3:25;
then consider i1,j1 such that
A17: [i1,j1] in Indices GoB f and
A18: f/.(i+1) = (GoB f)*(i1,j1) by A6,GOBOARD1:def 9;
A19: 1 <= i1 by A17,MATRIX_0:32;
A20: i1 <= len GoB f by A17,MATRIX_0:32;
1 <= j1 & j1 <= width GoB f by A17,MATRIX_0:32;
then
A21: (f/.(i+1))`1 = (GoB f)*(i1,1)`1 by A18,A19,A20,GOBOARD5:2;
then i1 < len GoB f by A4,A16,A20,XXREAL_0:1;
then (GoB f)*(len GoB f,1)`1 > (f/.(i+1))`1 by A5,A19,A21,GOBOARD5:3;
hence contradiction by A1,A2,A16,XXREAL_0:2;
end;
end;
theorem Th23:
(for p st p in P holds p`2 < (GoB f)*(1,1)`2) implies P misses L~f
proof
assume
A1: for p st p in P holds p`2 < (GoB f)*(1,1)`2;
assume P meets L~f;
then consider x being object such that
A2: x in P and
A3: x in L~f by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A2;
A4: x`2 < (GoB f)*(1,1)`2 by A1,A2;
A5: 1 < len GoB f by GOBOARD7:32;
A6: f is_sequence_on GoB f by GOBOARD5:def 5;
consider j such that
A7: 1 <= j and
A8: j+1 <= len f and
A9: x in LSeg(f/.j,f/.(j+1)) by A3,SPPOL_2:14;
per cases;
suppose
(f/.j)`2 <= (f/.(j+1))`2;
then
A10: (f/.j)`2 <= x `2 by A9,TOPREAL1:4;
j <= len f by A8,NAT_1:13;
then j in dom f by A7,FINSEQ_3:25;
then consider i1,j1 such that
A11: [i1,j1] in Indices GoB f and
A12: f/.j = (GoB f)*(i1,j1) by A6,GOBOARD1:def 9;
A13: 1 <= j1 by A11,MATRIX_0:32;
A14: j1 <= width GoB f by A11,MATRIX_0:32;
1 <= i1 & i1 <= len GoB f by A11,MATRIX_0:32;
then
A15: (f/.j)`2 = (GoB f)*(1,j1)`2 by A12,A13,A14,GOBOARD5:1;
then 1 < j1 by A4,A10,A13,XXREAL_0:1;
then (GoB f)*(1,1)`2 < (f/.j)`2 by A5,A14,A15,GOBOARD5:4;
hence contradiction by A1,A2,A10,XXREAL_0:2;
end;
suppose
(f/.j)`2 >= (f/.(j+1))`2;
then
A16: (f/.(j+1))`2 <= x `2 by A9,TOPREAL1:4;
1 <= j+1 by NAT_1:11;
then j+1 in dom f by A8,FINSEQ_3:25;
then consider i1,j1 such that
A17: [i1,j1] in Indices GoB f and
A18: f/.(j+1) = (GoB f)*(i1,j1) by A6,GOBOARD1:def 9;
A19: 1 <= j1 by A17,MATRIX_0:32;
A20: j1 <= width GoB f by A17,MATRIX_0:32;
1 <= i1 & i1 <= len GoB f by A17,MATRIX_0:32;
then
A21: (f/.(j+1))`2 = (GoB f)*(1,j1)`2 by A18,A19,A20,GOBOARD5:1;
then 1 < j1 by A4,A16,A19,XXREAL_0:1;
then (GoB f)*(1,1)`2 < (f/.(j+1))`2 by A5,A20,A21,GOBOARD5:4;
hence contradiction by A1,A2,A16,XXREAL_0:2;
end;
end;
theorem Th24:
(for p st p in P holds p`2 > (GoB f)*(1,width GoB f)`2) implies P misses L~f
proof
assume
A1: for p st p in P holds p`2 > (GoB f)*(1,width GoB f)`2;
assume P meets L~f;
then consider x being object such that
A2: x in P and
A3: x in L~f by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A2;
A4: x`2 > (GoB f)*(1,width GoB f)`2 by A1,A2;
A5: 1 < len GoB f by GOBOARD7:32;
A6: f is_sequence_on GoB f by GOBOARD5:def 5;
consider j such that
A7: 1 <= j and
A8: j+1 <= len f and
A9: x in LSeg(f/.j,f/.(j+1)) by A3,SPPOL_2:14;
per cases;
suppose
(f/.j)`2 >= (f/.(j+1))`2;
then
A10: (f/.j)`2 >= x `2 by A9,TOPREAL1:4;
j <= len f by A8,NAT_1:13;
then j in dom f by A7,FINSEQ_3:25;
then consider i1,j1 such that
A11: [i1,j1] in Indices GoB f and
A12: f/.j = (GoB f)*(i1,j1) by A6,GOBOARD1:def 9;
A13: 1 <= j1 by A11,MATRIX_0:32;
A14: j1 <= width GoB f by A11,MATRIX_0:32;
1 <= i1 & i1 <= len GoB f by A11,MATRIX_0:32;
then
A15: (f/.j)`2 = (GoB f)*(1,j1)`2 by A12,A13,A14,GOBOARD5:1;
then j1 < width GoB f by A4,A10,A14,XXREAL_0:1;
then (GoB f)*(1,width GoB f)`2 > (f/.j)`2 by A5,A13,A15,GOBOARD5:4;
hence contradiction by A1,A2,A10,XXREAL_0:2;
end;
suppose
(f/.j)`2 <= (f/.(j+1))`2;
then
A16: (f/.(j+1))`2 >= x `2 by A9,TOPREAL1:4;
1 <= j+1 by NAT_1:11;
then j+1 in dom f by A8,FINSEQ_3:25;
then consider i1,j1 such that
A17: [i1,j1] in Indices GoB f and
A18: f/.(j+1) = (GoB f)*(i1,j1) by A6,GOBOARD1:def 9;
A19: 1 <= j1 by A17,MATRIX_0:32;
A20: j1 <= width GoB f by A17,MATRIX_0:32;
1 <= i1 & i1 <= len GoB f by A17,MATRIX_0:32;
then
A21: (f/.(j+1))`2 = (GoB f)*(1,j1)`2 by A18,A19,A20,GOBOARD5:1;
then j1 < width GoB f by A4,A16,A20,XXREAL_0:1;
then (GoB f)*(1,width GoB f)`2 > (f/.(j+1))`2 by A5,A19,A21,GOBOARD5:4;
hence contradiction by A1,A2,A16,XXREAL_0:2;
end;
end;
theorem
for i st 1 <= i & i+2 <= len GoB f holds LSeg(1/2*((GoB f)*(i,1)+(GoB
f)*(i+1,1))- |[0,1]|, 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1))- |[0,1]|) misses L~
f
proof
let i such that
A1: 1 <= i and
A2: i+2 <= len GoB f;
A3: 1 <= width GoB f by GOBOARD7:33;
now
A4: i <= i+2 by NAT_1:11;
then i <= len GoB f by A2,XXREAL_0:2;
then
A5: (GoB f)*(i,1)`2 = (GoB f)*(1,1)`2 by A1,A3,GOBOARD5:1;
i+1 <= i+2 by XREAL_1:6;
then 1 <= i+1 & i+1 <= len GoB f by A2,NAT_1:11,XXREAL_0:2;
then
A6: (GoB f)*(i+1,1)`2 = (GoB f)*(1,1)`2 by A3,GOBOARD5:1;
1 <= i+2 by A1,A4,XXREAL_0:2;
then
A7: (GoB f)*(i+2,1)`2 = (GoB f)*(1,1)`2 by A2,A3,GOBOARD5:1;
(1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1))- |[0,1]|)`2 = (1/2*((GoB f)*(i
+1,1)+(GoB f)*(i+2,1)))`2- |[0,1]|`2 by TOPREAL3:3
.= 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1))`2- |[0,1]|`2 by TOPREAL3:4
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)- |[0,1]|`2 by A6,A7,TOPREAL3:2
.= 1*((GoB f)*(1,1))`2-1 by EUCLID:52;
then
A8: 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1))- |[0,1]| = |[(1/2*((GoB f)*(i+1
,1)+(GoB f)*(i+2,1))- |[0,1]|)`1, (GoB f)*(1,1)`2-1]| by EUCLID:53;
(1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1))- |[0,1]|)`2 = (1/2*((GoB f)*(i,1
)+(GoB f)*(i+1,1)))`2- |[0,1]|`2 by TOPREAL3:3
.= 1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1))`2- |[0,1]|`2 by TOPREAL3:4
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)- |[0,1]|`2 by A5,A6,TOPREAL3:2
.= 1*((GoB f)*(1,1))`2-1 by EUCLID:52;
then
A9: 1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1))- |[0,1]| = |[(1/2*((GoB f)*(i,1)+
(GoB f)*(i+1,1))- |[0,1]|)`1, ((GoB f)*(1,1))`2-1]| by EUCLID:53;
let p;
assume p in LSeg(1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1))- |[0,1]|, 1/2*((GoB
f)*(i+1,1)+(GoB f)*(i+2,1))- |[0,1]|);
then p`2 = (GoB f)*(1,1)`2 - 1 by A9,A8,TOPREAL3:12;
hence p`2 < (GoB f)*(1,1)`2 by XREAL_1:44;
end;
hence thesis by Th23;
end;
theorem
LSeg((GoB f)*(1,1)- |[1,1]|,1/2*((GoB f)*(1,1)+(GoB f)*(2,1))- |[0,1]|
) misses L~f
proof
A1: 1 <= width GoB f by GOBOARD7:33;
now
1 < len GoB f by GOBOARD7:32;
then 1+1 <= len GoB f by NAT_1:13;
then
A2: (GoB f)*(2,1)`2 = (GoB f)*(1,1)`2 by A1,GOBOARD5:1;
(1/2*((GoB f)*(1,1)+(GoB f)*(2,1))- |[0,1]|)`2 = (1/2*((GoB f)*(1,1)+(
GoB f)*(2,1)))`2- |[0,1]|`2 by TOPREAL3:3
.= 1/2*((GoB f)*(1,1)+(GoB f)*(2,1))`2- |[0,1]|`2 by TOPREAL3:4
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)- |[0,1]|`2 by A2,TOPREAL3:2
.= 1*((GoB f)*(1,1))`2-1 by EUCLID:52;
then
A3: 1/2*((GoB f)*(1,1)+(GoB f)*(2,1))- |[0,1]| = |[(1/2*((GoB f)*(1,1)+(
GoB f)*(2,1))- |[0,1]|)`1, (GoB f)*(1,1)`2-1]| by EUCLID:53;
((GoB f)*(1,1)- |[1,1]|)`2 = ((GoB f)*(1,1))`2- |[1,1]|`2 by TOPREAL3:3
.= (GoB f)*(1,1)`2-1 by EUCLID:52;
then
A4: (GoB f)*(1,1)- |[1,1]| = |[((GoB f)*(1,1)- |[1,1]|)`1,(GoB f)*(1,1)`2-
1]| by EUCLID:53;
let p;
assume p in LSeg((GoB f)*(1,1)- |[1,1]|, 1/2*((GoB f)*(1,1)+(GoB f)*(2,1)
)- |[0,1]|);
then p`2 = (GoB f)*(1,1)`2 - 1 by A4,A3,TOPREAL3:12;
hence p`2 < (GoB f)*(1,1)`2 by XREAL_1:44;
end;
hence thesis by Th23;
end;
theorem
LSeg(1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))- |[0,1]|,
(GoB f)*(len GoB f,1)+|[1,-1]|) misses L~f
proof
A1: 1 <= width GoB f by GOBOARD7:33;
now
A2: 1 < len GoB f by GOBOARD7:32;
then
A3: len GoB f -' 1 +1 = len GoB f by XREAL_1:235;
then
A4: len GoB f -' 1 <= len GoB f by NAT_1:11;
A5: (GoB f)*(len GoB f,1)`2 = (GoB f)*(1,1)`2 by A1,A2,GOBOARD5:1;
then
((GoB f)*(len GoB f,1)+|[1,-1]|)`2 = (GoB f)*(1,1)`2+|[1,-1]|`2 by TOPREAL3:2
.= (GoB f)*(1,1)`2+-1 by EUCLID:52
.= (GoB f)*(1,1)`2-1;
then
A6: (GoB f)*(len GoB f,1)+|[1,-1]| = |[((GoB f)*(len GoB f,1)+|[1,-1]|)`1
,(GoB f)* (1,1)`2-1]| by EUCLID:53;
1 <= len GoB f -' 1 by A2,A3,NAT_1:13;
then
A7: (GoB f)*(len GoB f -' 1,1)`2 = (GoB f)*(1,1)`2 by A1,A4,GOBOARD5:1;
(1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))- |[0,1]|)`2 =
(1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1)))`2- |[0,1]|`2 by
TOPREAL3:3
.= 1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))`2- |[0,1]|`2
by TOPREAL3:4
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)- |[0,1]|`2 by A7,A5,TOPREAL3:2
.= 1*((GoB f)*(1,1))`2-1 by EUCLID:52;
then
A8: 1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))- |[0,1]| = |[(
1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))- |[0,1]|)`1, (GoB f)*(1,
1)`2-1]| by EUCLID:53;
let p;
assume p in LSeg(1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))-
|[0,1]|, (GoB f)*(len GoB f,1)+|[1,-1]|);
then p`2 = (GoB f)*(1,1)`2 - 1 by A8,A6,TOPREAL3:12;
hence p`2 < (GoB f)*(1,1)`2 by XREAL_1:44;
end;
hence thesis by Th23;
end;
theorem
for i st 1 <= i & i+2 <= len GoB f holds LSeg(1/2*((GoB f)*(i,width
GoB f)+(GoB f)*(i+1,width GoB f))+|[0,1]|, 1/2*((GoB f)*(i+1,width GoB f)+(GoB
f)*(i+2,width GoB f))+|[0,1]|) misses L~f
proof
let i such that
A1: 1 <= i and
A2: i+2 <= len GoB f;
A3: 1 <= width GoB f by GOBOARD7:33;
now
A4: i <= i+2 by NAT_1:11;
then i <= len GoB f by A2,XXREAL_0:2;
then
A5: (GoB f)*(i,width GoB f)`2 = (GoB f)* (1,width GoB f)`2 by A1,A3,GOBOARD5:1;
i+1 <= i+2 by XREAL_1:6;
then 1 <= i+1 & i+1 <= len GoB f by A2,NAT_1:11,XXREAL_0:2;
then
A6: (GoB f)*(i+1,width GoB f)`2 = (GoB f)* (1,width GoB f)`2 by A3,GOBOARD5:1;
1 <= i+2 by A1,A4,XXREAL_0:2;
then
A7: (GoB f)*(i+2,width GoB f)`2 = (GoB f)*(1,width GoB f)`2 by A2,A3,GOBOARD5:1
;
(1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width GoB f))+|[0,1]|)`2
= (1/2*((GoB f)*(i+1,width GoB f)+(GoB f)* (i+2,width GoB f)))`2+|[0,1]|`2 by
TOPREAL3:2
.= 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)* (i+2,width GoB f))`2+|[0,1
]|`2 by TOPREAL3:4
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+|[0,1]|`2
by A6,A7,TOPREAL3:2
.= 1*((GoB f)*(1,width GoB f))`2+1 by EUCLID:52;
then
A8: 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width GoB f))+|[0,1]| =
|[(1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width GoB f))+|[0,1]|)`1, (GoB f
)*(1,width GoB f)`2+1]| by EUCLID:53;
(1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f))+|[0,1]|)`2 =
(1/2*((GoB f)*(i,width GoB f)+(GoB f)* (i+1,width GoB f)))`2+|[0,1]|`2 by
TOPREAL3:2
.= 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f))`2+|[0,1]|`2
by TOPREAL3:4
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+|[0,1]|`2
by A5,A6,TOPREAL3:2
.= 1*((GoB f)*(1,width GoB f))`2+1 by EUCLID:52;
then
A9: 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f))+|[0,1]| = |[(
1/2*((GoB f)*(i,width GoB f)+(GoB f)* (i+1,width GoB f))+|[0,1]|)`1, (GoB f)*(1
,width GoB f)`2+1]| by EUCLID:53;
let p;
assume p in LSeg(1/2*((GoB f)*(i,width GoB f)+(GoB f)* (i+1,width GoB f))
+|[0,1]|, 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width GoB f))+|[0,1]|);
then p`2 = (GoB f)*(1,width GoB f)`2 + 1 by A9,A8,TOPREAL3:12;
hence p`2 > (GoB f)*(1,width GoB f)`2 by XREAL_1:29;
end;
hence thesis by Th24;
end;
theorem
LSeg((GoB f)*(1,width GoB f)+|[-1,1]|, 1/2*((GoB f)*(1,width GoB f)+(
GoB f)*(2,width GoB f))+|[0,1]|) misses L~f
proof
A1: 1 <= width GoB f by GOBOARD7:33;
now
1 < len GoB f by GOBOARD7:32;
then 1+1 <= len GoB f by NAT_1:13;
then
A2: (GoB f)*(2,width GoB f)`2 = (GoB f)*(1,width GoB f)`2 by A1,GOBOARD5:1;
(1/2*((GoB f)*(1,width GoB f)+(GoB f)*(2,width GoB f))+|[0,1]|)`2 = (1
/2*((GoB f)*(1,width GoB f)+(GoB f)*(2,width GoB f)))`2+|[0,1]|`2 by TOPREAL3:2
.= 1/2*((GoB f)*(1,width GoB f)+(GoB f)*(2,width GoB f))`2+|[0,1]|`2
by TOPREAL3:4
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+|[0,1]|`2
by A2,TOPREAL3:2
.= 1*((GoB f)*(1,width GoB f))`2+1 by EUCLID:52;
then
A3: 1/2*((GoB f)*(1,width GoB f)+(GoB f)*(2,width GoB f))+|[0,1]| = |[(1/
2*((GoB f)*(1,width GoB f)+(GoB f)*(2,width GoB f))+|[0,1]|)`1, (GoB f)*(1,
width GoB f)`2+1]| by EUCLID:53;
((GoB f)*(1,width GoB f)+|[-1,1]|)`2 = ((GoB f)*(1,width GoB f))`2+|[-
1,1]|`2 by TOPREAL3:2
.= (GoB f)*(1,width GoB f)`2+1 by EUCLID:52;
then
A4: (GoB f)*(1,width GoB f)+|[-1,1]| = |[((GoB f)*(1,width GoB f)+|[-1,1]|
)`1,(GoB f)*(1,width GoB f)`2+1]| by EUCLID:53;
let p;
assume p in LSeg((GoB f)*(1,width GoB f)+|[-1,1]|, 1/2*((GoB f)*(1,width
GoB f)+(GoB f)*(2,width GoB f))+|[0,1]|);
then p`2 = (GoB f)*(1,width GoB f)`2 + 1 by A4,A3,TOPREAL3:12;
hence p`2 > (GoB f)*(1,width GoB f)`2 by XREAL_1:29;
end;
hence thesis by Th24;
end;
theorem
LSeg(1/2*((GoB f)*(len GoB f -' 1,width GoB f)+ (GoB f)*(len GoB f,
width GoB f))+|[0,1]|, (GoB f)*(len GoB f,width GoB f)+|[1,1]|) misses L~f
proof
A1: 1 <= width GoB f by GOBOARD7:33;
now
A2: 1 < len GoB f by GOBOARD7:32;
then
A3: len GoB f -' 1 +1 = len GoB f by XREAL_1:235;
then
A4: len GoB f -' 1 <= len GoB f by NAT_1:11;
A5: (GoB f)*(len GoB f,width GoB f)`2 = (GoB f)*(1,width GoB f)`2 by A1,A2,
GOBOARD5:1;
then
((GoB f)*(len GoB f,width GoB f)+|[1,1]|)`2 = (GoB f)*(1,width GoB f)
`2+|[1,1]|`2 by TOPREAL3:2
.= (GoB f)*(1,width GoB f)`2+1 by EUCLID:52;
then
A6: (GoB f)*(len GoB f,width GoB f)+|[1,1]| = |[((GoB f)*(len GoB f,width
GoB f)+|[1,1]|)`1, (GoB f)*(1,width GoB f)`2+1]| by EUCLID:53;
1 <= len GoB f -' 1 by A2,A3,NAT_1:13;
then
A7: (GoB f)*(len GoB f -' 1,width GoB f)`2 = (GoB f)*(1,width GoB f)`2 by A1,A4
,GOBOARD5:1;
(1/2*((GoB f)*(len GoB f -' 1,width GoB f) +(GoB f)*(len GoB f,width
GoB f))+|[0,1]|)`2 = (1/2*((GoB f)*(len GoB f -' 1,width GoB f) +(GoB f)*(len
GoB f,width GoB f)))`2+|[0,1]|`2 by TOPREAL3:2
.= 1/2*((GoB f)*(len GoB f -' 1,width GoB f) +(GoB f)*(len GoB f,width
GoB f))`2+|[0,1]|`2 by TOPREAL3:4
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+|[0,1]|`2
by A7,A5,TOPREAL3:2
.= 1*((GoB f)*(1,width GoB f))`2+1 by EUCLID:52;
then
A8: 1/2*((GoB f)*(len GoB f -' 1,width GoB f) +(GoB f)*(len GoB f,width
GoB f))+|[0,1]| = |[(1/2*((GoB f)*(len GoB f -' 1,width GoB f) +(GoB f)*(len
GoB f,width GoB f))+|[0,1]|)`1, (GoB f)*(1,width GoB f)`2+1]| by EUCLID:53;
let p;
assume p in LSeg(1/2*((GoB f)*(len GoB f -' 1,width GoB f)+ (GoB f)*(len
GoB f,width GoB f))+|[0,1]|, (GoB f)*(len GoB f,width GoB f)+|[1,1]|);
then p`2 = (GoB f)*(1,width GoB f)`2 + 1 by A8,A6,TOPREAL3:12;
hence p`2 > (GoB f)*(1,width GoB f)`2 by XREAL_1:29;
end;
hence thesis by Th24;
end;
theorem
for j st 1 <= j & j+2 <= width GoB f holds LSeg(1/2*((GoB f)*(1,j)+(
GoB f)*(1,j+1))- |[1,0]|, 1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2))- |[1,0]|)
misses L~f
proof
let j such that
A1: 1 <= j and
A2: j+2 <= width GoB f;
A3: 1 <= len GoB f by GOBOARD7:32;
now
A4: j <= j+2 by NAT_1:11;
then j <= width GoB f by A2,XXREAL_0:2;
then
A5: (GoB f)*(1,j)`1 = (GoB f)*(1,1)`1 by A1,A3,GOBOARD5:2;
j+1 <= j+2 by XREAL_1:6;
then 1 <= j+1 & j+1 <= width GoB f by A2,NAT_1:11,XXREAL_0:2;
then
A6: (GoB f)*(1,j+1)`1 = (GoB f)*(1,1)`1 by A3,GOBOARD5:2;
1 <= j+2 by A1,A4,XXREAL_0:2;
then
A7: (GoB f)*(1,j+2)`1 = (GoB f)*(1,1)`1 by A2,A3,GOBOARD5:2;
(1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2))- |[1,0]|)`1 = (1/2*((GoB f)*(1
,j+1)+(GoB f)*(1,j+2)))`1- |[1,0]|`1 by TOPREAL3:3
.= 1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2))`1- |[1,0]|`1 by TOPREAL3:4
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)- |[1,0]|`1 by A6,A7,TOPREAL3:2
.= 1*((GoB f)*(1,1))`1-1 by EUCLID:52;
then
A8: 1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2))- |[1,0]| = |[(GoB f)*(1,1)`1-1,
(1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2))- |[1,0]|)`2]| by EUCLID:53;
(1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1))- |[1,0]|)`1 = (1/2*((GoB f)*(1,j
)+(GoB f)*(1,j+1)))`1- |[1,0]|`1 by TOPREAL3:3
.= 1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1))`1- |[1,0]|`1 by TOPREAL3:4
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)- |[1,0]|`1 by A5,A6,TOPREAL3:2
.= 1*((GoB f)*(1,1))`1-1 by EUCLID:52;
then
A9: 1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1))- |[1,0]| = |[(GoB f)*(1,1)`1-1 ,
(1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1))- |[1,0]|)`2]| by EUCLID:53;
let p;
assume p in LSeg(1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1))- |[1,0]|, 1/2*((GoB
f)*(1,j+1)+(GoB f)*(1,j+2))- |[1,0]|);
then p`1 = (GoB f)*(1,1)`1 - 1 by A9,A8,TOPREAL3:11;
hence p`1 < (GoB f)*(1,1)`1 by XREAL_1:44;
end;
hence thesis by Th21;
end;
theorem
LSeg((GoB f)*(1,1)- |[1,1]|,1/2*((GoB f)*(1,1)+(GoB f)*(1,2))- |[1,0]|
) misses L~f
proof
A1: 1 <= len GoB f by GOBOARD7:32;
now
1 < width GoB f by GOBOARD7:33;
then 1+1 <= width GoB f by NAT_1:13;
then
A2: (GoB f)*(1,2)`1 = (GoB f)*(1,1)`1 by A1,GOBOARD5:2;
(1/2*((GoB f)*(1,1)+(GoB f)*(1,2))- |[1,0]|)`1 = (1/2*((GoB f)*(1,1)+(
GoB f)*(1,2)))`1- |[1,0]|`1 by TOPREAL3:3
.= 1/2*((GoB f)*(1,1)+(GoB f)*(1,2))`1- |[1,0]|`1 by TOPREAL3:4
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)- |[1,0]|`1 by A2,TOPREAL3:2
.= 1*((GoB f)*(1,1))`1-1 by EUCLID:52;
then
A3: 1/2*((GoB f)*(1,1)+(GoB f)*(1,2))- |[1,0]| = |[(GoB f)*(1,1)`1-1, (1/
2*((GoB f)*(1,1)+(GoB f)*(1,2))- |[1,0]|)`2]| by EUCLID:53;
((GoB f)*(1,1)- |[1,1]|)`1 = ((GoB f)*(1,1))`1- |[1,1]|`1 by TOPREAL3:3
.= (GoB f)*(1,1)`1-1 by EUCLID:52;
then
A4: (GoB f)*(1,1)- |[1,1]| = |[(GoB f)*(1,1)`1-1,((GoB f)*(1,1)- |[1,1]|)
`2]| by EUCLID:53;
let p;
assume p in LSeg((GoB f)*(1,1)- |[1,1]|, 1/2*((GoB f)*(1,1)+(GoB f)*(1,2)
)- |[1,0]|);
then p`1 = (GoB f)*(1,1)`1 - 1 by A4,A3,TOPREAL3:11;
hence p`1 < (GoB f)*(1,1)`1 by XREAL_1:44;
end;
hence thesis by Th21;
end;
theorem
LSeg(1/2*((GoB f)*(1,width GoB f -' 1)+(GoB f)*(1,width GoB f))- |[1,0
]| , (GoB f)*(1,width GoB f)+|[-1,1]|) misses L~f
proof
A1: 1 <= len GoB f by GOBOARD7:32;
now
A2: 1 < width GoB f by GOBOARD7:33;
then
A3: width GoB f -' 1 +1 = width GoB f by XREAL_1:235;
then
A4: width GoB f -' 1 <= width GoB f by NAT_1:11;
A5: (GoB f)*(1,width GoB f)`1 = (GoB f)*(1,1)`1 by A1,A2,GOBOARD5:2;
then ((GoB f)*(1,width GoB f)+|[-1,1]|)`1 = (GoB f)*(1,1)`1+|[-1,1]|`1 by
TOPREAL3:2
.= (GoB f)*(1,1)`1+-1 by EUCLID:52
.= (GoB f)*(1,1)`1-1;
then
A6: (GoB f)*(1,width GoB f)+|[-1,1]| = |[(GoB f)*(1,1)`1-1,((GoB f)* (1,
width GoB f)+|[-1,1]|)`2]| by EUCLID:53;
1 <= width GoB f -' 1 by A2,A3,NAT_1:13;
then
A7: (GoB f)*(1,width GoB f -' 1)`1 = (GoB f)*(1,1)`1 by A1,A4,GOBOARD5:2;
(1/2*((GoB f)*(1,width GoB f -' 1)+(GoB f)*(1,width GoB f))- |[1,0]|)
`1 = (1/2*((GoB f)*(1,width GoB f -' 1) +(GoB f)*(1,width GoB f)))`1- |[1,0]|`1
by TOPREAL3:3
.= 1/2*((GoB f)*(1,width GoB f -' 1)+(GoB f)* (1,width GoB f))`1- |[1,
0]|`1 by TOPREAL3:4
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)- |[1,0]|`1 by A7,A5,TOPREAL3:2
.= 1*((GoB f)*(1,1))`1-1 by EUCLID:52;
then
A8: 1/2*((GoB f)*(1,width GoB f -' 1)+(GoB f)*(1,width GoB f))- |[1 ,0 ]|
= |[(GoB f)*(1,1)`1-1,(1/2*((GoB f)*(1,width GoB f -' 1) +(GoB f)*(1,width GoB
f))- |[1,0]|)`2]| by EUCLID:53;
let p;
assume p in LSeg(1/2*((GoB f)*(1,width GoB f -' 1)+(GoB f)* (1,width GoB
f))- |[1,0]|, (GoB f)*(1,width GoB f)+|[-1,1]|);
then p`1 = (GoB f)*(1,1)`1 - 1 by A8,A6,TOPREAL3:11;
hence p`1 < (GoB f)*(1,1)`1 by XREAL_1:44;
end;
hence thesis by Th21;
end;
theorem
for j st 1 <= j & j+2 <= width GoB f holds LSeg(1/2*((GoB f)*(len GoB
f,j)+(GoB f)*(len GoB f,j+1))+|[1,0]|, 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(
len GoB f,j+2))+|[1,0]|) misses L~f
proof
let j such that
A1: 1 <= j and
A2: j+2 <= width GoB f;
A3: 1 <= len GoB f by GOBOARD7:32;
now
A4: j <= j+2 by NAT_1:11;
then j <= width GoB f by A2,XXREAL_0:2;
then
A5: (GoB f)*(len GoB f,j)`1 = (GoB f)*(len GoB f,1)`1 by A1,A3,GOBOARD5:2;
j+1 <= j+2 by XREAL_1:6;
then 1 <= j+1 & j+1 <= width GoB f by A2,NAT_1:11,XXREAL_0:2;
then
A6: (GoB f)*(len GoB f,j+1)`1 = (GoB f)*(len GoB f,1)`1 by A3,GOBOARD5:2;
1 <= j+2 by A1,A4,XXREAL_0:2;
then
A7: (GoB f)*(len GoB f,j+2)`1 = (GoB f)*(len GoB f,1)`1 by A2,A3,GOBOARD5:2;
(1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))+|[1,0]|)`1 = (
1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2)))`1+|[1,0]|`1 by
TOPREAL3:2
.= 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))`1+|[1,0]|`1
by TOPREAL3:4
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+|[1,0]|`1 by A6
,A7,TOPREAL3:2
.= 1*((GoB f)*(len GoB f,1))`1+1 by EUCLID:52;
then
A8: 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))+|[1,0]| = |[(
GoB f)*(len GoB f,1)`1+1,(1/2*((GoB f)*(len GoB f,j+1) +(GoB f)*(len GoB f,j+2)
)+|[1,0]|)`2]| by EUCLID:53;
(1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1))+|[1,0]|)`1 = (1/
2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1)))`1+|[1,0]|`1 by TOPREAL3:2
.= 1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1))`1+|[1,0]|`1 by
TOPREAL3:4
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+|[1,0]|`1 by A5
,A6,TOPREAL3:2
.= 1*((GoB f)*(len GoB f,1))`1+1 by EUCLID:52;
then
A9: 1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1))+|[1,0]| = |[(GoB
f)*(len GoB f,1)`1+1,(1/2*((GoB f)*(len GoB f,j) +(GoB f)*(len GoB f,j+1))+|[1,
0]|)`2]| by EUCLID:53;
let p;
assume p in LSeg(1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1))+|[1,
0]|, 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))+|[1,0]|);
then p`1 = (GoB f)*(len GoB f,1)`1 + 1 by A9,A8,TOPREAL3:11;
hence p`1 > (GoB f)*(len GoB f,1)`1 by XREAL_1:29;
end;
hence thesis by Th22;
end;
theorem
LSeg((GoB f)*(len GoB f,1)+|[1,-1]|, 1/2*((GoB f)*(len GoB f,1)+(GoB f
)*(len GoB f,2))+|[1,0]|) misses L~f
proof
A1: 1 <= len GoB f by GOBOARD7:32;
now
1 < width GoB f by GOBOARD7:33;
then 1+1 <= width GoB f by NAT_1:13;
then
A2: (GoB f)*(len GoB f,2)`1 = (GoB f)*(len GoB f,1)`1 by A1,GOBOARD5:2;
(1/2*((GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2))+|[1,0]|)`1 = (1/2*(
(GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2)))`1+|[1,0]|`1 by TOPREAL3:2
.= 1/2*((GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2))`1+|[1,0]|`1 by
TOPREAL3:4
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+|[1,0]|`1 by A2,
TOPREAL3:2
.= 1*((GoB f)*(len GoB f,1))`1+1 by EUCLID:52;
then
A3: 1/2*((GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2))+|[1,0]| = |[(GoB f)
*(len GoB f,1)`1+1, (1/2*((GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2))+|[1,0]|)
`2]| by EUCLID:53;
((GoB f)*(len GoB f,1)+|[1,-1]|)`1 = ((GoB f)*(len GoB f,1))`1+|[1,-1
]|`1 by TOPREAL3:2
.= (GoB f)*(len GoB f,1)`1+1 by EUCLID:52;
then
A4: (GoB f)*(len GoB f,1)+|[1,-1]| = |[(GoB f)*(len GoB f,1)`1+1,((GoB f)*
(len GoB f,1)+|[1,-1]|)`2]| by EUCLID:53;
let p;
assume p in LSeg((GoB f)*(len GoB f,1)+|[1,-1]|, 1/2*((GoB f)*(len GoB f,
1)+(GoB f)*(len GoB f,2))+|[1,0]|);
then p`1 = (GoB f)*(len GoB f,1)`1 + 1 by A4,A3,TOPREAL3:11;
hence p`1 > (GoB f)*(len GoB f,1)`1 by XREAL_1:29;
end;
hence thesis by Th22;
end;
theorem
LSeg(1/2*((GoB f)*(len GoB f,width GoB f -' 1)+ (GoB f)*(len GoB f,
width GoB f))+|[1,0]|, (GoB f)*(len GoB f,width GoB f)+|[1,1]|) misses L~f
proof
A1: 1 <= len GoB f by GOBOARD7:32;
now
A2: 1 < width GoB f by GOBOARD7:33;
then
A3: width GoB f -' 1 +1 = width GoB f by XREAL_1:235;
then
A4: width GoB f -' 1 <= width GoB f by NAT_1:11;
A5: (GoB f)*(len GoB f,width GoB f)`1 = (GoB f)*(len GoB f,1)`1 by A1,A2,
GOBOARD5:2;
then
((GoB f)*(len GoB f,width GoB f)+|[1,1]|)`1 = (GoB f)*(len GoB f,1)`1
+|[1,1]|`1 by TOPREAL3:2
.= (GoB f)*(len GoB f,1)`1+1 by EUCLID:52;
then
A6: (GoB f)*(len GoB f,width GoB f)+|[1,1]| = |[(GoB f)*(len GoB f,1)`1+1
, ((GoB f)*(len GoB f,width GoB f)+|[1,1]|)`2 ]| by EUCLID:53;
1 <= width GoB f -' 1 by A2,A3,NAT_1:13;
then
A7: (GoB f)*(len GoB f,width GoB f -' 1)`1 = (GoB f)*(len GoB f,1)`1 by A1,A4,
GOBOARD5:2;
(1/2*((GoB f)*(len GoB f,width GoB f -' 1) +(GoB f)*(len GoB f,width
GoB f))+|[1,0]|)`1 = (1/2*((GoB f)*(len GoB f,width GoB f -' 1) +(GoB f)*(len
GoB f,width GoB f)))`1+|[1,0]|`1 by TOPREAL3:2
.= 1/2*((GoB f)*(len GoB f,width GoB f -' 1) +(GoB f)*(len GoB f,width
GoB f))`1+|[1,0]|`1 by TOPREAL3:4
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+|[1,0]|`1 by A7
,A5,TOPREAL3:2
.= 1*((GoB f)*(len GoB f,1))`1+1 by EUCLID:52;
then
A8: 1/2*((GoB f)*(len GoB f,width GoB f -' 1) +(GoB f)*(len GoB f,width
GoB f))+|[1,0]| = |[(GoB f)*(len GoB f,1)`1+1,(1/2*((GoB f)* (len GoB f,width
GoB f -' 1) +(GoB f)*(len GoB f,width GoB f))+|[1,0]|)`2 ]| by EUCLID:53;
let p;
assume p in LSeg(1/2*((GoB f)*(len GoB f,width GoB f -' 1)+ (GoB f)*(len
GoB f,width GoB f))+|[1,0]|, (GoB f)*(len GoB f,width GoB f)+|[1,1]|);
then p`1 = (GoB f)*(len GoB f,1)`1 + 1 by A8,A6,TOPREAL3:11;
hence p`1 > (GoB f)*(len GoB f,1)`1 by XREAL_1:29;
end;
hence thesis by Th22;
end;
theorem
1 <= k & k+1 <= len f implies Int left_cell(f,k) misses L~f
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f;
k <= k+1 by NAT_1:11;
then k <= len f by A2,XXREAL_0:2;
then
A3: k in dom f by A1,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A4: [i1,j1] in Indices GoB f and
A5: f/.k = (GoB f)*(i1,j1) by GOBOARD2:14;
A6: i1 <= len GoB f by A4,MATRIX_0:32;
j1 <> 0 by A4,MATRIX_0:32;
then consider j being Nat such that
A7: j1 = j+1 by NAT_1:6;
i1 <> 0 by A4,MATRIX_0:32;
then consider i being Nat such that
A8: i1 = i+1 by NAT_1:6;
i <= i1 by A8,NAT_1:11;
then
A9: i <= len GoB f by A6,XXREAL_0:2;
A10: j1 <= width GoB f by A4,MATRIX_0:32;
k+1 >= 1 by NAT_1:11;
then
A11: k+1 in dom f by A2,FINSEQ_3:25;
then consider i2,j2 being Nat such that
A12: [i2,j2] in Indices GoB f and
A13: f/.(k+1) = (GoB f)*(i2,j2) by GOBOARD2:14;
reconsider i19=i1, i29=i2, j19=j1, j29=j2 as Element of REAL by XREAL_0:def 1
;
|.i1-i2.|+|.j1-j2.| = 1 by A3,A4,A5,A11,A12,A13,GOBOARD5:12;
then
A14: |.i19-i29.| = 1 & j1 = j2 or |.j19-j29.|=1 & i1 = i2 by SEQM_3:42;
reconsider i,j as Nat;
A15: i1 = i+1 by A8;
A16: j1 = j+1 by A7;
A17: j2 <= width GoB f by A12,MATRIX_0:32;
A18: i2 <= len GoB f by A12,MATRIX_0:32;
j <= j1 by A7,NAT_1:11;
then
A19: j <= width GoB f by A10,XXREAL_0:2;
per cases by A14,SEQM_3:41;
suppose
i1 = i2 & j1+1 = j2;
then left_cell(f,k) = cell(GoB f,i,j1) by A1,A2,A4,A5,A8,A12,A13,
GOBOARD5:27;
hence thesis by A10,A9,GOBOARD7:12;
end;
suppose
i1+1 = i2 & j1 = j2;
then left_cell(f,k) = cell(GoB f,i1,j1) by A1,A2,A4,A5,A16,A12,A13,
GOBOARD5:28;
hence thesis by A6,A10,GOBOARD7:12;
end;
suppose
i1 = i2+1 & j1 = j2;
then left_cell(f,k) = cell(GoB f,i2,j) by A1,A2,A4,A5,A7,A12,A13,
GOBOARD5:29;
hence thesis by A19,A18,GOBOARD7:12;
end;
suppose
i1 = i2 & j1 = j2+1;
then left_cell(f,k) = cell(GoB f,i1,j2) by A1,A2,A4,A5,A15,A12,A13,
GOBOARD5:30;
hence thesis by A6,A17,GOBOARD7:12;
end;
end;
theorem
1 <= k & k+1 <= len f implies Int right_cell(f,k) misses L~f
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f;
k <= k+1 by NAT_1:11;
then k <= len f by A2,XXREAL_0:2;
then
A3: k in dom f by A1,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A4: [i1,j1] in Indices GoB f and
A5: f/.k = (GoB f)*(i1,j1) by GOBOARD2:14;
A6: i1 <= len GoB f by A4,MATRIX_0:32;
j1 <> 0 by A4,MATRIX_0:32;
then consider j being Nat such that
A7: j1 = j+1 by NAT_1:6;
i1 <> 0 by A4,MATRIX_0:32;
then consider i being Nat such that
A8: i1 = i+1 by NAT_1:6;
i <= i1 by A8,NAT_1:11;
then
A9: i <= len GoB f by A6,XXREAL_0:2;
A10: j1 <= width GoB f by A4,MATRIX_0:32;
k+1 >= 1 by NAT_1:11;
then
A11: k+1 in dom f by A2,FINSEQ_3:25;
then consider i2,j2 being Nat such that
A12: [i2,j2] in Indices GoB f and
A13: f/.(k+1) = (GoB f)*(i2,j2) by GOBOARD2:14;
reconsider i19=i1, i29=i2, j19=j1, j29=j2 as Element of REAL by XREAL_0:def 1
;
|.i1-i2.|+|.j1-j2.| = 1 by A3,A4,A5,A11,A12,A13,GOBOARD5:12;
then
A14: |.i19-i29.| = 1 & j1 = j2 or |.j19-j29.|=1 & i1 = i2 by SEQM_3:42;
reconsider i,j as Nat;
A15: i1 = i+1 by A8;
A16: j1 = j+1 by A7;
A17: j2 <= width GoB f by A12,MATRIX_0:32;
A18: i2 <= len GoB f by A12,MATRIX_0:32;
j <= j1 by A7,NAT_1:11;
then
A19: j <= width GoB f by A10,XXREAL_0:2;
per cases by A14,SEQM_3:41;
suppose
i1 = i2 & j1+1 = j2;
then right_cell(f,k) = cell(GoB f,i1,j1) by A1,A2,A4,A5,A15,A12,A13,
GOBOARD5:27;
hence thesis by A6,A10,GOBOARD7:12;
end;
suppose
i1+1 = i2 & j1 = j2;
then right_cell(f,k) = cell(GoB f,i1,j) by A1,A2,A4,A5,A7,A12,A13,
GOBOARD5:28;
hence thesis by A6,A19,GOBOARD7:12;
end;
suppose
i1 = i2+1 & j1 = j2;
then right_cell(f,k) = cell(GoB f,i2,j1) by A1,A2,A4,A5,A16,A12,A13,
GOBOARD5:29;
hence thesis by A10,A18,GOBOARD7:12;
end;
suppose
i1 = i2 & j1 = j2+1;
then right_cell(f,k) = cell(GoB f,i,j2) by A1,A2,A4,A5,A8,A12,A13,
GOBOARD5:30;
hence thesis by A9,A17,GOBOARD7:12;
end;
end;