Copyright (c) 1995 Association of Mizar Users
environ
vocabulary PRE_TOPC, EUCLID, SEQM_3, GOBOARD5, FINSEQ_1, GOBOARD2, TREES_1,
TOPREAL1, ARYTM_3, BOOLE, TOPS_1, ARYTM_1, MCART_1, GOBOARD1, RELAT_1,
MATRIX_1, ABSVALUE, FINSEQ_4;
notation TARSKI, XBOOLE_0, XREAL_0, REAL_1, NAT_1, ABSVALUE, BINARITH,
FINSEQ_1, FINSEQ_4, MATRIX_1, STRUCT_0, PRE_TOPC, TOPS_1, EUCLID,
TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5;
constructors TOPS_1, GROUP_1, GOBOARD5, GOBOARD2, SEQM_3, REAL_1, BINARITH,
FINSEQ_4, MEMBERED;
clusters STRUCT_0, GOBOARD5, RELSET_1, GOBOARD2, EUCLID, ARYTM_3, MEMBERED;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems GOBOARD5, EUCLID, GOBOARD1, RLVECT_1, REAL_1, AXIOMS, TOPREAL3,
REAL_2, TOPREAL1, GOBOARD2, FINSEQ_3, NAT_1, AMI_5, GOBOARD6, GOBOARD7,
SPPOL_2, XBOOLE_0, XBOOLE_1, ZFMISC_1, XCMPLX_0, XCMPLX_1;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i,j such that
A6: 1 <= i & i+1 <= len GoB f and
A7: 1 <= j & j+2 <= width GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j+1) and
A9: (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));
j < j+2 by REAL_1:69;
then A10: j <= width GoB f by A7,AXIOMS:22;
j+1 <= j+2 by AXIOMS:24;
then A11: 1 <= j+1 & j+1 <= width GoB f by A7,AXIOMS:22,NAT_1:29;
A12: j+1+1 = j+(1+1) by XCMPLX_1:1;
then A13: j+1 < width GoB f by A7,NAT_1:38;
A14: i < len GoB f by A6,NAT_1:38;
assume
A15: 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;
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+1+1)))
c= 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,A7,A12,A13,A14,GOBOARD6:67;
then A16: 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 A12,A15,XBOOLE_1:63
;
A17: L~f misses Int cell(GoB f,i,j) by A10,A14,GOBOARD7:14;
L~f misses Int cell(GoB f,i,j+1) by A11,A14,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1)
by A17,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) }
by A16,XBOOLE_1:70;
then 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A18: LSeg(f/.(k+1),(GoB f)*(i,j+1)) = LSeg(f,k0)
by A6,A8,A11,GOBOARD7:42;
A19: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A20: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A9,A13,A14,A18,A19,A20,GOBOARD7:62;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i,j such that
A6: 1 <= i & i+2 <= len GoB f and
A7: 1 <= j & j+2 <= width GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j+1) and
A9: (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));
j < j+2 by REAL_1:69;
then A10: j < width GoB f by A7,AXIOMS:22;
j+1 <= j+2 by AXIOMS:24;
then A11: 1 <= j+1 & j+1 <= width GoB f by A7,AXIOMS:22,NAT_1:29;
i+1+1 = i+(1+1) by XCMPLX_1:1;
then A12: i+1 < len GoB f by A6,NAT_1:38;
A13: j+1+1 = j+(1+1) by XCMPLX_1:1;
then A14: j+1 < width GoB f by A7,NAT_1:38;
A15: i < len GoB f by A12,NAT_1:38;
assume
A16: 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;
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+1+1)))
c= 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,A7,A13,A14,A15,GOBOARD6:67;
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 A13,A16,XBOOLE_1:63
;
A18: L~f misses Int cell(GoB f,i,j) by A10,A15,GOBOARD7:14;
L~f misses Int cell(GoB f,i,j+1) by A11,A15,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1)
by A18,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) }
by A17,XBOOLE_1:70;
then 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A19: LSeg(
f/.(k+1),(GoB f)*(i,j+1)) = LSeg(f,k0) by A6,A8,A11,A12,GOBOARD7:42;
A20: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A21: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A8,A9,A11,A12,A13,A14,A19,A20,A21,GOBOARD7:63;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i,j such that
A6: 1 <= i & i+2 <= len GoB f and
A7: 1 <= j & j+2 <= width GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j+1) and
A9: (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));
j < j+2 by REAL_1:69;
then A10: j < width GoB f by A7,AXIOMS:22;
j+1 <= j+2 by AXIOMS:24;
then A11: 1 <= j+1 & j+1 <= width GoB f by A7,AXIOMS:22,NAT_1:29;
i+1+1 = i+(1+1) by XCMPLX_1:1;
then A12: i+1 < len GoB f by A6,NAT_1:38;
j+1+1 = j+(1+1) by XCMPLX_1:1;
then A13: j+1 < width GoB f by A7,NAT_1:38;
A14: i < len GoB f by A12,NAT_1:38;
assume
A15: 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;
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)))
c= 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,A7,A13,A14,GOBOARD6:67;
then A16: 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 A15,XBOOLE_1:63;
A17: L~f misses Int cell(GoB f,i,j) by A10,A14,GOBOARD7:14;
L~f misses Int cell(GoB f,i,j+1) by A11,A14,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1)
by A17,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) }
by A16,XBOOLE_1:70;
then 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A18: LSeg(
f/.(k+1),(GoB f)*(i,j+1)) = LSeg(f,k0) by A6,A8,A11,A12,GOBOARD7:42;
A19: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A20: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A9,A10,A12,A18,A19,A20,GOBOARD7:64;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i,j such that
A6: 1 <= i & i+1 <= len GoB f and
A7: 1 <= j & j+2 <= width GoB f and
A8: f/.(k+1) = (GoB f)*(i,j+1) and
A9: (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));
j < j+2 by REAL_1:69;
then A10: j <= width GoB f by A7,AXIOMS:22;
j+1 <= j+2 by AXIOMS:24;
then A11: 1 <= j+1 & j+1 <= width GoB f by A7,AXIOMS:22,NAT_1:29;
j+1+1 = j+(1+1) by XCMPLX_1:1;
then A12: j+1 < width GoB f by A7,NAT_1:38;
A13: i < len GoB f by A6,NAT_1:38;
assume
A14: 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;
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)))
c= 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,A7,A12,A13,GOBOARD6:67;
then A15: 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 A14,XBOOLE_1:63;
A16: L~f misses Int cell(GoB f,i,j) by A10,A13,GOBOARD7:14;
L~f misses Int cell(GoB f,i,j+1) by A11,A13,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i,j+1)
by A16,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) }
by A15,XBOOLE_1:70;
then 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A17: LSeg(f/.(k+1),(GoB f)*(i+1,j+1)) = LSeg(f,k0)
by A6,A8,A11,GOBOARD7:42;
A18: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A19: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A9,A12,A13,A17,A18,A19,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+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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i,j such that
A6: 1 <= i & i+2 <= len GoB f and
A7: 1 <= j & j+2 <= width GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j+1) and
A9: (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));
j < j+2 by REAL_1:69;
then A10: j < width GoB f by A7,AXIOMS:22;
j+1 <= j+2 by AXIOMS:24;
then A11: 1 <= j+1 & j+1 <= width GoB f by A7,AXIOMS:22,NAT_1:29;
A12: i+1+1 = i+(1+1) by XCMPLX_1:1;
then A13: i+1 < len GoB f by A6,NAT_1:38;
A14: j+1+1 = j+(1+1) by XCMPLX_1:1;
then A15: j+1 < width GoB f by A7,NAT_1:38;
A16: 1 <= i+1 by NAT_1:29;
assume
A17: 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;
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)))
c= 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 A7,A12,A13,A15,A16,GOBOARD6:67;
then A18: 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 A17,XBOOLE_1:63;
A19: L~f misses Int cell(GoB f,i+1,j) by A10,A13,GOBOARD7:14;
L~f misses Int cell(GoB f,i+1,j+1) by A11,A13,GOBOARD7:14;
then L~f misses Int cell(GoB f,i+1,j) \/ Int cell(GoB f,i+1,j+1)
by A19,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+2,j+1)) }
by A18,XBOOLE_1:70;
then 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+2,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A20: LSeg(f/.(k+1),(GoB f)*(i+2,j+1)) = LSeg(f,k0)
by A6,A8,A11,A12,A16,GOBOARD7:42;
A21: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A22: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A8,A9,A11,A13,A14,A15,A20,A21,A22,GOBOARD7:63;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i,j such that
A6: 1 <= i & i+2 <= len GoB f and
A7: 1 <= j & j+2 <= width GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j+1) and
A9: (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));
j < j+2 by REAL_1:69;
then A10: j < width GoB f by A7,AXIOMS:22;
j+1 <= j+2 by AXIOMS:24;
then A11: 1 <= j+1 & j+1 <= width GoB f by A7,AXIOMS:22,NAT_1:29;
A12: i+1+1 = i+(1+1) by XCMPLX_1:1;
then A13: i+1 < len GoB f by A6,NAT_1:38;
j+1+1 = j+(1+1) by XCMPLX_1:1;
then A14: j+1 < width GoB f by A7,NAT_1:38;
A15: 1 <= i+1 by NAT_1:29;
assume
A16: 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;
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)))
c= 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 A7,A12,A13,A14,A15,GOBOARD6:67;
then A17: 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 A16,XBOOLE_1:63;
A18: L~f misses Int cell(GoB f,i+1,j) by A10,A13,GOBOARD7:14;
L~f misses Int cell(GoB f,i+1,j+1) by A11,A13,GOBOARD7:14;
then L~f misses Int cell(GoB f,i+1,j) \/ Int cell(GoB f,i+1,j+1)
by A18,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+2,j+1)) }
by A17,XBOOLE_1:70;
then 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+2,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A19: LSeg(f/.(k+1),(GoB f)*(i+2,j+1)) = LSeg(f,k0)
by A6,A8,A11,A12,A15,GOBOARD7:42;
A20: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A21: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A9,A10,A13,A19,A20,A21,GOBOARD7:64;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i such that
A6: 1 <= i & i+2 <= len GoB f and
A7: f/.(k+1) = (GoB f)*(i+1,1) and
A8: (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));
width GoB f <> 0 by GOBOARD1:def 5;
then A9: 0+1 <= width GoB f by RLVECT_1:99;
i+1+1 = i+(1+1) by XCMPLX_1:1;
then A10: i+1 < len GoB f by A6,NAT_1:38;
A11: 1 < width GoB f by GOBOARD7:35;
A12: 0 < width GoB f by A9,NAT_1:38;
A13: i < len GoB f by A10,NAT_1:38;
assume
A14: 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;
LSeg(1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1))- |[0,1]|,
1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1+1)))
c= Int cell(GoB f,i,0) \/ Int cell(GoB f,i,1)
\/ { 1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1)) }
by A6,A11,A13,GOBOARD6:69;
then A15: 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 A14,XBOOLE_1:63;
A16: L~f misses Int cell(GoB f,i,0) by A12,A13,GOBOARD7:14;
L~f misses Int cell(GoB f,i,1) by A9,A13,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,0) \/ Int cell(GoB f,i,1)
by A16,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1)) }
by A15,XBOOLE_1:70;
then 1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A17: LSeg(f/.(k+1),(GoB f)*(i,1)) = LSeg(f,k0) by A6,A7,A9,A10,GOBOARD7:42;
A18: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A19: 1+1 = 2;
A20: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A10,A11,A17,A18,A19,A20,GOBOARD7:63;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i such that
A6: 1 <= i & i+2 <= len GoB f and
A7: f/.(k+1) = (GoB f)*(i+1,1) and
A8: (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));
width GoB f <> 0 by GOBOARD1:def 5;
then A9: 0+1 <= width GoB f by RLVECT_1:99;
A10: i+1+1 = i+(1+1) by XCMPLX_1:1;
then A11: i+1 < len GoB f by A6,NAT_1:38;
A12: 1 < width GoB f by GOBOARD7:35;
A13: 0 < width GoB f by A9,NAT_1:38;
A14: 1 <= i+1 by NAT_1:29;
assume
A15: 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;
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)))
c= 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 A10,A11,A12,A14,GOBOARD6:69;
then A16: 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 A15,XBOOLE_1:63;
A17: L~f misses Int cell(GoB f,i+1,0) by A11,A13,GOBOARD7:14;
L~f misses Int cell(GoB f,i+1,1) by A9,A11,GOBOARD7:14;
then L~f misses Int cell(GoB f,i+1,0) \/ Int cell(GoB f,i+1,1)
by A17,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1)) }
by A16,XBOOLE_1:70;
then 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A18: LSeg(f/.(k+1),(GoB f)*(i+2,1)) = LSeg(f,k0)
by A6,A7,A9,A10,A14,GOBOARD7:42;
A19: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A20: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
A21: 1+1 = 2;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A11,A12,A18,A19,A20,A21,GOBOARD7:63;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i such that
A6: 1 <= i & i+2 <= len GoB f and
A7: f/.(k+1) = (GoB f)*(i+1,width GoB f) and
A8: (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));
A9: 1 < width GoB f by GOBOARD7:35;
then A10: width GoB f -'1 +1 = width GoB f by AMI_5:4;
then A11: 1 <= width GoB f -' 1 by A9,NAT_1:38;
A12: width GoB f -' 1 < width GoB f by A10,NAT_1:38;
i+1+1 = i+(1+1) by XCMPLX_1:1;
then A13: i+1 < len GoB f by A6,NAT_1:38;
then A14: i < len GoB f by NAT_1:38;
assume
A15: 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;
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,A10,A11,A13,GOBOARD7:11;
then 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]|)
c= 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,A9,A14,GOBOARD6:70;
then A16: 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 A15,XBOOLE_1:63;
A17: L~f misses Int cell(GoB f,i,width GoB f -' 1) by A12,A14,GOBOARD7:14;
L~f misses Int cell(GoB f,i,width GoB f) by A14,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,width GoB f -' 1)
\/ Int cell(GoB f,i,width GoB f)
by A17,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i,width GoB f)+(GoB f)*
(i+1,width GoB f)) }
by A16,XBOOLE_1:70;
then 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f)) in L~f
by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A18: LSeg(f/.(k+1),(GoB f)*(i,width GoB f)) = LSeg(f,k0)
by A6,A7,A9,A13,GOBOARD7:42;
A19: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A20: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A10,A11,A12,A13,A18,A19,A20,GOBOARD7:64;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i such that
A6: 1 <= i & i+2 <= len GoB f and
A7: f/.(k+1) = (GoB f)*(i+1,width GoB f) and
A8: (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));
A9: 1 < width GoB f by GOBOARD7:35;
A10: 1 <= width GoB f by GOBOARD7:35;
then A11: width GoB f -'1 +1 = width GoB f by AMI_5:4;
then A12: 1 <= width GoB f -' 1 by A9,NAT_1:38;
A13: width GoB f -' 1 < width GoB f by A11,NAT_1:38;
A14: i+1+1 = i+(1+1) by XCMPLX_1:1;
then A15: i+1 < len GoB f by A6,NAT_1:38;
A16: 1 <= i+1 by NAT_1:29;
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;
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 A6,A11,A12,A14,A16,GOBOARD7:11;
then 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]|)
c= 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 A9,A14,A15,A16,GOBOARD6:70;
then A18: 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 A17,XBOOLE_1:63;
A19: L~f misses Int cell(GoB f,i+1,width GoB f -' 1) by A13,A15,GOBOARD7:14;
L~f misses Int cell(GoB f,i+1,width GoB f) by A15,GOBOARD7:14;
then L~f misses Int cell(GoB f,i+1,width GoB f -' 1)
\/ Int cell(GoB f,i+1,width GoB f) by A19,XBOOLE_1:70;
then L~f meets {1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*
(i+2,width GoB f))}
by A18,XBOOLE_1:70;
then 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width GoB f)) in L~f
by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A20: LSeg(f/.(k+1),(GoB f)*(i+2,width GoB f)) = LSeg(f,k0)
by A6,A7,A10,A14,A16,GOBOARD7:42;
A21: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A22: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A11,A12,A13,A15,A20,A21,A22,GOBOARD7:64;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let i,j such that
A6: 1 <= j & j+1 <= width GoB f and
A7: 1 <= i & i+2 <= len GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j+1) and
A9: (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));
i < i+2 by REAL_1:69;
then A10: i <= len GoB f by A7,AXIOMS:22;
i+1 <= i+2 by AXIOMS:24;
then A11: 1 <= i+1 & i+1 <= len GoB f by A7,AXIOMS:22,NAT_1:29;
A12: i+1+1 = i+(1+1) by XCMPLX_1:1;
then A13: i+1 < len GoB f by A7,NAT_1:38;
A14: j < width GoB f by A6,NAT_1:38;
assume
A15: 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;
LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)),
1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1+1,j+1)))
c= 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,A7,A12,A13,A14,GOBOARD6:68;
then A16: 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 A12,A15,XBOOLE_1:63
;
A17: L~f misses Int cell(GoB f,i,j) by A10,A14,GOBOARD7:14;
L~f misses Int cell(GoB f,i+1,j) by A11,A14,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j)
by A17,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) }
by A16,XBOOLE_1:70;
then 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A18: LSeg(f/.(k+1),(GoB f)*(i+1,j)) = LSeg(f,k0)
by A6,A8,A11,GOBOARD7:41;
A19: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A20: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A9,A13,A14,A18,A19,A20,GOBOARD7:64;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let j,i such that
A6: 1 <= j & j+2 <= width GoB f and
A7: 1 <= i & i+2 <= len GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j+1) and
A9: (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));
i < i+2 by REAL_1:69;
then A10: i < len GoB f by A7,AXIOMS:22;
i+1 <= i+2 by AXIOMS:24;
then A11: 1 <= i+1 & i+1 <= len GoB f by A7,AXIOMS:22,NAT_1:29;
j+1+1 = j+(1+1) by XCMPLX_1:1;
then A12: j+1 < width GoB f by A6,NAT_1:38;
A13: i+1+1 = i+(1+1) by XCMPLX_1:1;
then A14: i+1 < len GoB f by A7,NAT_1:38;
A15: j < width GoB f by A12,NAT_1:38;
assume
A16: 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;
LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)),
1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1+1,j+1)))
c= 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,A7,A13,A14,A15,GOBOARD6:68;
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 A13,A16,XBOOLE_1:63
;
A18: L~f misses Int cell(GoB f,i,j) by A10,A15,GOBOARD7:14;
L~f misses Int cell(GoB f,i+1,j) by A11,A15,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j)
by A18,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) }
by A17,XBOOLE_1:70;
then 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A19: LSeg(
f/.(k+1),(GoB f)*(i+1,j)) = LSeg(f,k0) by A6,A8,A11,A12,GOBOARD7:41;
A20: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A21: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A8,A9,A11,A12,A13,A14,A19,A20,A21,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+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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let j,i such that
A6: 1 <= j & j+2 <= width GoB f and
A7: 1 <= i & i+2 <= len GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j+1) and
A9: (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));
i < i+2 by REAL_1:69;
then A10: i < len GoB f by A7,AXIOMS:22;
i+1 <= i+2 by AXIOMS:24;
then A11: 1 <= i+1 & i+1 <= len GoB f by A7,AXIOMS:22,NAT_1:29;
j+1+1 = j+(1+1) by XCMPLX_1:1;
then A12: j+1 < width GoB f by A6,NAT_1:38;
i+1+1 = i+(1+1) by XCMPLX_1:1;
then A13: i+1 < len GoB f by A7,NAT_1:38;
A14: j < width GoB f by A12,NAT_1:38;
assume
A15: 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;
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)))
c= 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,A7,A13,A14,GOBOARD6:68;
then A16: 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 A15,XBOOLE_1:63;
A17: L~f misses Int cell(GoB f,i,j) by A10,A14,GOBOARD7:14;
L~f misses Int cell(GoB f,i+1,j) by A11,A14,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j)
by A17,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) }
by A16,XBOOLE_1:70;
then 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A18: LSeg(
f/.(k+1),(GoB f)*(i+1,j)) = LSeg(f,k0) by A6,A8,A11,A12,GOBOARD7:41;
A19: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A20: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A9,A10,A12,A18,A19,A20,GOBOARD7:62;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let j,i such that
A6: 1 <= j & j+1 <= width GoB f and
A7: 1 <= i & i+2 <= len GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j) and
A9: (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));
i < i+2 by REAL_1:69;
then A10: i <= len GoB f by A7,AXIOMS:22;
i+1 <= i+2 by AXIOMS:24;
then A11: 1 <= i+1 & i+1 <= len GoB f by A7,AXIOMS:22,NAT_1:29;
i+1+1 = i+(1+1) by XCMPLX_1:1;
then A12: i+1 < len GoB f by A7,NAT_1:38;
A13: j < width GoB f by A6,NAT_1:38;
assume
A14: 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;
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)))
c= 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,A7,A12,A13,GOBOARD6:68;
then A15: 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 A14,XBOOLE_1:63;
A16: L~f misses Int cell(GoB f,i,j) by A10,A13,GOBOARD7:14;
L~f misses Int cell(GoB f,i+1,j) by A11,A13,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,j) \/ Int cell(GoB f,i+1,j)
by A16,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) }
by A15,XBOOLE_1:70;
then 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+1,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A17: LSeg(f/.(k+1),(GoB f)*(i+1,j+1)) = LSeg(f,k0)
by A6,A8,A11,GOBOARD7:41;
A18: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A19: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A9,A12,A13,A17,A18,A19,GOBOARD7:63;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let j,i such that
A6: 1 <= j & j+2 <= width GoB f and
A7: 1 <= i & i+2 <= len GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j+1) and
A9: (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));
i < i+2 by REAL_1:69;
then A10: i < len GoB f by A7,AXIOMS:22;
i+1 <= i+2 by AXIOMS:24;
then A11: 1 <= i+1 & i+1 <= len GoB f by A7,AXIOMS:22,NAT_1:29;
A12: j+1+1 = j+(1+1) by XCMPLX_1:1;
then A13: j+1 < width GoB f by A6,NAT_1:38;
A14: i+1+1 = i+(1+1) by XCMPLX_1:1;
then A15: i+1 < len GoB f by A7,NAT_1:38;
A16: 1 <= j+1 by NAT_1:29;
assume
A17: 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;
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)))
c= 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 A7,A12,A13,A15,A16,GOBOARD6:68;
then A18: 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 A17,XBOOLE_1:63;
A19: L~f misses Int cell(GoB f,i,j+1) by A10,A13,GOBOARD7:14;
L~f misses Int cell(GoB f,i+1,j+1) by A11,A13,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,j+1) \/ Int cell(GoB f,i+1,j+1)
by A19,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+1,j+2)) }
by A18,XBOOLE_1:70;
then 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+1,j+2)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A20: LSeg(f/.(k+1),(GoB f)*(i+1,j+2)) = LSeg(f,k0)
by A6,A8,A11,A12,A16,GOBOARD7:41;
A21: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A22: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A8,A9,A11,A13,A14,A15,A20,A21,A22,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,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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let j,i such that
A6: 1 <= j & j+2 <= width GoB f and
A7: 1 <= i & i+2 <= len GoB f and
A8: f/.(k+1) = (GoB f)*(i+1,j+1) and
A9: (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));
i < i+2 by REAL_1:69;
then A10: i < len GoB f by A7,AXIOMS:22;
i+1 <= i+2 by AXIOMS:24;
then A11: 1 <= i+1 & i+1 <= len GoB f by A7,AXIOMS:22,NAT_1:29;
A12: j+1+1 = j+(1+1) by XCMPLX_1:1;
then A13: j+1 < width GoB f by A6,NAT_1:38;
i+1+1 = i+(1+1) by XCMPLX_1:1;
then A14: i+1 < len GoB f by A7,NAT_1:38;
A15: 1 <= j+1 by NAT_1:29;
assume
A16: 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;
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)))
c= 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 A7,A12,A13,A14,A15,GOBOARD6:68;
then A17: 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 A16,XBOOLE_1:63;
A18: L~f misses Int cell(GoB f,i,j+1) by A10,A13,GOBOARD7:14;
L~f misses Int cell(GoB f,i+1,j+1) by A11,A13,GOBOARD7:14;
then L~f misses Int cell(GoB f,i,j+1) \/ Int cell(GoB f,i+1,j+1)
by A18,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+1,j+2)) }
by A17,XBOOLE_1:70;
then 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+1,j+2)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A19: LSeg(f/.(k+1),(GoB f)*(i+1,j+2)) = LSeg(f,k0)
by A6,A8,A11,A12,A15,GOBOARD7:41;
A20: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A21: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A9,A10,A13,A19,A20,A21,GOBOARD7:62;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let j such that
A6: 1 <= j & j+2 <= width GoB f and
A7: f/.(k+1) = (GoB f)*(1,j+1) and
A8: (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));
len GoB f <> 0 by GOBOARD1:def 5;
then A9: 0+1 <= len GoB f by RLVECT_1:99;
j+1+1 = j+(1+1) by XCMPLX_1:1;
then A10: j+1 < width GoB f by A6,NAT_1:38;
A11: 1 < len GoB f by GOBOARD7:34;
A12: 0 < len GoB f by A9,NAT_1:38;
A13: j < width GoB f by A10,NAT_1:38;
assume
A14: 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;
LSeg(1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1))- |[1,0]|,
1/2*((GoB f)*(1,j)+(GoB f)*(1+1,j+1)))
c= Int cell(GoB f,0,j) \/ Int cell(GoB f,1,j)
\/ { 1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1)) }
by A6,A11,A13,GOBOARD6:71;
then A15: 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 A14,XBOOLE_1:63;
A16: L~f misses Int cell(GoB f,0,j) by A12,A13,GOBOARD7:14;
L~f misses Int cell(GoB f,1,j) by A9,A13,GOBOARD7:14;
then L~f misses Int cell(GoB f,0,j) \/ Int cell(GoB f,1,j)
by A16,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1)) }
by A15,XBOOLE_1:70;
then 1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A17: LSeg(f/.(k+1),(GoB f)*(1,j)) = LSeg(f,k0) by A6,A7,A9,A10,GOBOARD7:41;
A18: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A19: 1+1 = 2;
A20: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A10,A11,A17,A18,A19,A20,GOBOARD7:61;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let j such that
A6: 1 <= j & j+2 <= width GoB f and
A7: f/.(k+1) = (GoB f)*(1,j+1) and
A8: (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));
len GoB f <> 0 by GOBOARD1:def 5;
then A9: 0+1 <= len GoB f by RLVECT_1:99;
A10: j+1+1 = j+(1+1) by XCMPLX_1:1;
then A11: j+1 < width GoB f by A6,NAT_1:38;
A12: 1 < len GoB f by GOBOARD7:34;
A13: 0 < len GoB f by A9,NAT_1:38;
A14: 1 <= j+1 by NAT_1:29;
assume
A15: 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;
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)))
c= 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 A10,A11,A12,A14,GOBOARD6:71;
then A16: 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 A15,XBOOLE_1:63;
A17: L~f misses Int cell(GoB f,0,j+1) by A11,A13,GOBOARD7:14;
L~f misses Int cell(GoB f,1,j+1) by A9,A11,GOBOARD7:14;
then L~f misses Int cell(GoB f,0,j+1) \/ Int cell(GoB f,1,j+1)
by A17,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2)) }
by A16,XBOOLE_1:70;
then 1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2)) in L~f by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A18: LSeg(f/.(k+1),(GoB f)*(1,j+2)) = LSeg(f,k0)
by A6,A7,A9,A10,A14,GOBOARD7:41;
A19: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A20: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
A21: 1+1 = 2;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A11,A12,A18,A19,A20,A21,GOBOARD7:61;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let j such that
A6: 1 <= j & j+2 <= width GoB f and
A7: f/.(k+1) = (GoB f)*(len GoB f,j+1) and
A8: (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));
A9: 1 < len GoB f by GOBOARD7:34;
then A10: len GoB f -'1 +1 = len GoB f by AMI_5:4;
then A11: 1 <= len GoB f -' 1 by A9,NAT_1:38;
A12: len GoB f -' 1 < len GoB f by A10,NAT_1:38;
j+1+1 = j+(1+1) by XCMPLX_1:1;
then A13: j+1 < width GoB f by A6,NAT_1:38;
then A14: j < width GoB f by NAT_1:38;
assume
A15: 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;
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,A10,A11,A13,GOBOARD7:11;
then 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]|)
c= 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,A9,A14,GOBOARD6:72;
then A16: 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 A15,XBOOLE_1:63;
A17: L~f misses Int cell(GoB f,len GoB f -' 1,j) by A12,A14,GOBOARD7:14;
L~f misses Int cell(GoB f,len GoB f,j) by A14,GOBOARD7:14;
then L~f misses Int cell(GoB f,len GoB f -' 1,j)
\/ Int cell(GoB f,len GoB f,j)
by A17,XBOOLE_1:70;
then L~f meets { 1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1)) }
by A16,XBOOLE_1:70;
then 1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1)) in L~f
by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A18: LSeg(f/.(k+1),(GoB f)*(len GoB f,j)) = LSeg(f,k0)
by A6,A7,A9,A13,GOBOARD7:41;
A19: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A20: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A10,A11,A12,A13,A18,A19,A20,GOBOARD7:62;
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: 1 <= k+1 by NAT_1:29;
A4: k+1+1 = k+(1+1) by XCMPLX_1:1;
then A5: k+1 < len f by A2,NAT_1:38;
let j such that
A6: 1 <= j & j+2 <= width GoB f and
A7: f/.(k+1) = (GoB f)*(len GoB f,j+1) and
A8: (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));
A9: 1 < len GoB f by GOBOARD7:34;
A10: 1 <= len GoB f by GOBOARD7:34;
then A11: len GoB f -'1 +1 = len GoB f by AMI_5:4;
then A12: 1 <= len GoB f -' 1 by A9,NAT_1:38;
A13: len GoB f -' 1 < len GoB f by A11,NAT_1:38;
A14: j+1+1 = j+(1+1) by XCMPLX_1:1;
then A15: j+1 < width GoB f by A6,NAT_1:38;
A16: 1 <= j+1 by NAT_1:29;
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;
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 A6,A11,A12,A14,A16,GOBOARD7:11;
then 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]|)
c= 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 A9,A14,A15,A16,GOBOARD6:72;
then A18: 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 A17,XBOOLE_1:63;
A19: L~f misses Int cell(GoB f,len GoB f -' 1,j+1) by A13,A15,GOBOARD7:14;
L~f misses Int cell(GoB f,len GoB f,j+1) by A15,GOBOARD7:14;
then L~f misses Int cell(GoB f,len GoB f -' 1,j+1)
\/ Int cell(GoB f,len GoB f,j+1) by A19,XBOOLE_1:70;
then L~f meets {1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))}
by A18,XBOOLE_1:70;
then 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2)) in L~f
by ZFMISC_1:56;
then consider k0 being Nat such that
1 <= k0 & k0+1 <= len f and
A20: LSeg(f/.(k+1),(GoB f)*(len GoB f,j+2)) = LSeg(f,k0)
by A6,A7,A10,A14,A16,GOBOARD7:41;
A21: LSeg(f,k0) c= L~f & LSeg(f,k) c= L~f & LSeg(f,k+1) c= L~f by TOPREAL3:26;
A22: LSeg(f,k) = LSeg(f/.k,f/.(k+1)) by A1,A5,TOPREAL1:def 5;
LSeg(f,k+1) = LSeg(f/.(k+1),f/.(k+2)) by A2,A3,A4,TOPREAL1:def 5;
hence contradiction by A6,A7,A8,A11,A12,A13,A15,A20,A21,A22,GOBOARD7:62;
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;
A2: f is_sequence_on GoB f by GOBOARD5:def 5;
assume P meets L~f;
then consider x such that
A3: x in P and
A4: x in L~f by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A3;
A5: x`1 < (GoB f)*(1,1)`1 by A1,A3;
consider i such that
A6: 1 <= i and
A7: i+1 <= len f and
A8: x in LSeg(f/.i,f/.(i+1)) by A4,SPPOL_2:14;
A9: 1 < width GoB f by GOBOARD7:35;
per cases;
suppose (f/.i)`1 <= (f/.(i+1))`1;
then A10: (f/.i)`1 <= x `1 by A8,TOPREAL1:9;
i <= len f by A7,NAT_1:38;
then i in dom f by A6,FINSEQ_3:27;
then consider i1,j1 such that
A11: [i1,j1] in Indices GoB f and
A12: f/.i = (GoB f)*(i1,j1) by A2,GOBOARD1:def 11;
A13: 1 <= j1 & j1 <= width GoB f & 1 <= i1 & i1 <= len GoB f by A11,GOBOARD5:1;
then A14: (f/.i)`1 = (GoB f)*(i1,1)`1 by A12,GOBOARD5:3;
then 1 < i1 by A5,A10,A13,AXIOMS:21;
then (GoB f)*(1,1)`1 < (f/.i)`1 by A9,A13,A14,GOBOARD5:4;
hence contradiction by A5,A10,AXIOMS:22;
suppose (f/.i)`1 >= (f/.(i+1))`1;
then A15: (f/.(i+1))`1 <= x `1 by A8,TOPREAL1:9;
1 <= i+1 by NAT_1:29;
then i+1 in dom f by A7,FINSEQ_3:27;
then consider i1,j1 such that
A16: [i1,j1] in Indices GoB f and
A17: f/.(i+1) = (GoB f)*(i1,j1) by A2,GOBOARD1:def 11;
A18: 1 <= j1 & j1 <= width GoB f & 1 <= i1 & i1 <= len GoB f by A16,GOBOARD5:1;
then A19: (f/.(i+1))`1 = (GoB f)*(i1,1)`1 by A17,GOBOARD5:3;
then 1 < i1 by A5,A15,A18,AXIOMS:21;
then (GoB f)*(1,1)`1 < (f/.(i+1))`1 by A9,A18,A19,GOBOARD5:4;
hence contradiction by A5,A15,AXIOMS:22;
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;
A2: f is_sequence_on GoB f by GOBOARD5:def 5;
assume P meets L~f;
then consider x such that
A3: x in P and
A4: x in L~f by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A3;
A5: x`1 > (GoB f)*(len GoB f,1)`1 by A1,A3;
consider i such that
A6: 1 <= i and
A7: i+1 <= len f and
A8: x in LSeg(f/.i,f/.(i+1)) by A4,SPPOL_2:14;
A9: 1 < width GoB f by GOBOARD7:35;
per cases;
suppose (f/.i)`1 >= (f/.(i+1))`1;
then A10: (f/.i)`1 >= x `1 by A8,TOPREAL1:9;
i <= len f by A7,NAT_1:38;
then i in dom f by A6,FINSEQ_3:27;
then consider i1,j1 such that
A11: [i1,j1] in Indices GoB f and
A12: f/.i = (GoB f)*(i1,j1) by A2,GOBOARD1:def 11;
A13: 1 <= j1 & j1 <= width GoB f & 1 <= i1 & i1 <= len GoB f by A11,GOBOARD5:1;
then A14: (f/.i)`1 = (GoB f)*(i1,1)`1 by A12,GOBOARD5:3;
then i1 < len GoB f by A5,A10,A13,AXIOMS:21;
then (GoB f)*(len GoB f,1)`1 > (f/.i)`1 by A9,A13,A14,GOBOARD5:4;
hence contradiction by A5,A10,AXIOMS:22;
suppose (f/.i)`1 <= (f/.(i+1))`1;
then A15: (f/.(i+1))`1 >= x `1 by A8,TOPREAL1:9;
1 <= i+1 by NAT_1:29;
then i+1 in dom f by A7,FINSEQ_3:27;
then consider i1,j1 such that
A16: [i1,j1] in Indices GoB f and
A17: f/.(i+1) = (GoB f)*(i1,j1) by A2,GOBOARD1:def 11;
A18: 1 <= j1 & j1 <= width GoB f & 1 <= i1 & i1 <= len GoB f by A16,GOBOARD5:1;
then A19: (f/.(i+1))`1 = (GoB f)*(i1,1)`1 by A17,GOBOARD5:3;
then i1 < len GoB f by A5,A15,A18,AXIOMS:21;
then (GoB f)*(len GoB f,1)`1 > (f/.(i+1))`1 by A9,A18,A19,GOBOARD5:4;
hence contradiction by A5,A15,AXIOMS:22;
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;
A2: f is_sequence_on GoB f by GOBOARD5:def 5;
assume P meets L~f;
then consider x such that
A3: x in P and
A4: x in L~f by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A3;
A5: x`2 < (GoB f)*(1,1)`2 by A1,A3;
consider j such that
A6: 1 <= j and
A7: j+1 <= len f and
A8: x in LSeg(f/.j,f/.(j+1)) by A4,SPPOL_2:14;
A9: 1 < len GoB f by GOBOARD7:34;
per cases;
suppose (f/.j)`2 <= (f/.(j+1))`2;
then A10: (f/.j)`2 <= x `2 by A8,TOPREAL1:10;
j <= len f by A7,NAT_1:38;
then j in dom f by A6,FINSEQ_3:27;
then consider i1,j1 such that
A11: [i1,j1] in Indices GoB f and
A12: f/.j = (GoB f)*(i1,j1) by A2,GOBOARD1:def 11;
A13: 1 <= i1 & i1 <= len GoB f & 1 <= j1 & j1 <= width GoB f by A11,GOBOARD5:1;
then A14: (f/.j)`2 = (GoB f)*(1,j1)`2 by A12,GOBOARD5:2;
then 1 < j1 by A5,A10,A13,AXIOMS:21;
then (GoB f)*(1,1)`2 < (f/.j)`2 by A9,A13,A14,GOBOARD5:5;
hence contradiction by A5,A10,AXIOMS:22;
suppose (f/.j)`2 >= (f/.(j+1))`2;
then A15: (f/.(j+1))`2 <= x `2 by A8,TOPREAL1:10;
1 <= j+1 by NAT_1:29;
then j+1 in dom f by A7,FINSEQ_3:27;
then consider i1,j1 such that
A16: [i1,j1] in Indices GoB f and
A17: f/.(j+1) = (GoB f)*(i1,j1) by A2,GOBOARD1:def 11;
A18: 1 <= i1 & i1 <= len GoB f & 1 <= j1 & j1 <= width GoB f by A16,GOBOARD5:1;
then A19: (f/.(j+1))`2 = (GoB f)*(1,j1)`2 by A17,GOBOARD5:2;
then 1 < j1 by A5,A15,A18,AXIOMS:21;
then (GoB f)*(1,1)`2 < (f/.(j+1))`2 by A9,A18,A19,GOBOARD5:5;
hence contradiction by A5,A15,AXIOMS:22;
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;
A2: f is_sequence_on GoB f by GOBOARD5:def 5;
assume P meets L~f;
then consider x such that
A3: x in P and
A4: x in L~f by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A3;
A5: x`2 > (GoB f)*(1,width GoB f)`2 by A1,A3;
consider j such that
A6: 1 <= j and
A7: j+1 <= len f and
A8: x in LSeg(f/.j,f/.(j+1)) by A4,SPPOL_2:14;
A9: 1 < len GoB f by GOBOARD7:34;
per cases;
suppose (f/.j)`2 >= (f/.(j+1))`2;
then A10: (f/.j)`2 >= x `2 by A8,TOPREAL1:10;
j <= len f by A7,NAT_1:38;
then j in dom f by A6,FINSEQ_3:27;
then consider i1,j1 such that
A11: [i1,j1] in Indices GoB f and
A12: f/.j = (GoB f)*(i1,j1) by A2,GOBOARD1:def 11;
A13: 1 <= i1 & i1 <= len GoB f & 1 <= j1 & j1 <= width GoB f by A11,GOBOARD5:1;
then A14: (f/.j)`2 = (GoB f)*(1,j1)`2 by A12,GOBOARD5:2;
then j1 < width GoB f by A5,A10,A13,AXIOMS:21;
then (GoB f)*(1,width GoB f)`2 > (f/.j)`2 by A9,A13,A14,GOBOARD5:5;
hence contradiction by A5,A10,AXIOMS:22;
suppose (f/.j)`2 <= (f/.(j+1))`2;
then A15: (f/.(j+1))`2 >= x `2 by A8,TOPREAL1:10;
1 <= j+1 by NAT_1:29;
then j+1 in dom f by A7,FINSEQ_3:27;
then consider i1,j1 such that
A16: [i1,j1] in Indices GoB f and
A17: f/.(j+1) = (GoB f)*(i1,j1) by A2,GOBOARD1:def 11;
A18: 1 <= i1 & i1 <= len GoB f & 1 <= j1 & j1 <= width GoB f by A16,GOBOARD5:1;
then A19: (f/.(j+1))`2 = (GoB f)*(1,j1)`2 by A17,GOBOARD5:2;
then j1 < width GoB f by A5,A15,A18,AXIOMS:21;
then (GoB f)*(1,width GoB f)`2 > (f/.(j+1))`2 by A9,A18,A19,GOBOARD5:5;
hence contradiction by A5,A15,AXIOMS:22;
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 & i+2 <= len GoB f;
A2: 1 <= width GoB f by GOBOARD7:35;
now let p such that
A3: 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]|);
A4: i <= i+2 by NAT_1:29;
then i <= len GoB f by A1,AXIOMS:22;
then A5: (GoB f)*(i,1)`2 = (GoB f)*(1,1)`2 by A1,A2,GOBOARD5:2;
i+1 <= i+2 by AXIOMS:24;
then 1 <= i+1 & i+1 <= len GoB f by A1,AXIOMS:22,NAT_1:29;
then A6: (GoB f)*(i+1,1)`2 = (GoB f)*(1,1)`2 by A2,GOBOARD5:2;
1 <= i+2 by A1,A4,AXIOMS:22;
then A7: (GoB f)*(i+2,1)`2 = (GoB f)*(1,1)`2 by A1,A2,GOBOARD5:2;
(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:8
.= 1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1))`2- |[0,1]|`2 by TOPREAL3:9
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)- |[0,1]|`2 by A5,A6,TOPREAL3:7
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)-1 by EUCLID:56
.= 1/2*(2*((GoB f)*(1,1))`2)-1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,1))`2-1 by XCMPLX_1:4
.= 1*((GoB f)*(1,1))`2-1;
then A8: 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:57;
(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:8
.= 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1))`2- |[0,1]|`2 by TOPREAL3:9
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)- |[0,1]|`2 by A6,A7,TOPREAL3:7
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)-1 by EUCLID:56
.= 1/2*(2*((GoB f)*(1,1))`2)-1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,1))`2-1 by XCMPLX_1:4
.= 1*((GoB f)*(1,1))`2-1;
then 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:57;
then p`2 = (GoB f)*(1,1)`2 - 1 by A3,A8,TOPREAL3:18;
hence p`2 < (GoB f)*(1,1)`2 by REAL_2:174;
end;
hence 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 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:35;
now let p such that
A2: p in LSeg((GoB f)*(1,1)- |[1,1]|,
1/2*((GoB f)*(1,1)+(GoB f)*(2,1))- |[0,1]|);
1 < len GoB f by GOBOARD7:34;
then 1+1 <= len GoB f by NAT_1:38;
then A3: (GoB f)*(2,1)`2 = (GoB f)*(1,1)`2 by A1,GOBOARD5:2;
((GoB f)*(1,1)- |[1,1]|)`2 = ((GoB f)*(1,1))`2- |[1,1]|`2 by TOPREAL3:8
.= (GoB f)*(1,1)`2-1 by EUCLID:56;
then A4: (GoB f)*(1,1)- |[1,1]|
= |[((GoB f)*(1,1)- |[1,1]|)`1,(GoB f)*(1,1)`2-1]| by EUCLID:57;
(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:8
.= 1/2*((GoB f)*(1,1)+(GoB f)*(2,1))`2- |[0,1]|`2 by TOPREAL3:9
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)- |[0,1]|`2 by A3,TOPREAL3:7
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)-1 by EUCLID:56
.= 1/2*(2*((GoB f)*(1,1))`2)-1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,1))`2-1 by XCMPLX_1:4
.= 1*((GoB f)*(1,1))`2-1;
then 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:57;
then p`2 = (GoB f)*(1,1)`2 - 1 by A2,A4,TOPREAL3:18;
hence p`2 < (GoB f)*(1,1)`2 by REAL_2:174;
end;
hence LSeg((GoB f)*(1,1)- |[1,1]|,
1/2*((GoB f)*(1,1)+(GoB f)*(2,1))- |[0,1]|) misses L~f 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:35;
now let p such that
A2: 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]|);
A3: 1 < len GoB f by GOBOARD7:34;
then A4: len GoB f -' 1 +1 = len GoB f by AMI_5:4;
then A5: 1 <= len GoB f -' 1 by A3,NAT_1:38;
len GoB f -' 1 <= len GoB f by A4,NAT_1:29;
then A6: (GoB f)*(len GoB f -' 1,1)`2 = (GoB f)*(1,1)`2 by A1,A5,GOBOARD5:2;
A7: (GoB f)*(len GoB f,1)`2 = (GoB f)*(1,1)`2 by A1,A3,GOBOARD5:2;
(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:8
.= 1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))`2- |[0,1]|`2
by TOPREAL3:9
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)- |[0,1]|`2 by A6,A7,TOPREAL3:7
.= 1/2*((GoB f)*(1,1)`2+(GoB f)*(1,1)`2)-1 by EUCLID:56
.= 1/2*(2*((GoB f)*(1,1))`2)-1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,1))`2-1 by XCMPLX_1:4
.= 1*((GoB f)*(1,1))`2-1;
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:57;
((GoB f)*(len GoB f,1)+|[1,-1]|)`2
= (GoB f)*(1,1)`2+|[1,-1]|`2 by A7,TOPREAL3:7
.= (GoB f)*(1,1)`2+-1 by EUCLID:56
.= (GoB f)*(1,1)`2-1 by XCMPLX_0:def 8;
then (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:57;
then p`2 = (GoB f)*(1,1)`2 - 1 by A2,A8,TOPREAL3:18;
hence p`2 < (GoB f)*(1,1)`2 by REAL_2:174;
end;
hence 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 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 & i+2 <= len GoB f;
A2: 1 <= width GoB f by GOBOARD7:35;
now let p such that
A3: 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]|);
A4: i <= i+2 by NAT_1:29;
then i <= len GoB f by A1,AXIOMS:22;
then A5: (GoB f)*(i,width GoB f)`2 = (GoB f)*
(1,width GoB f)`2 by A1,A2,GOBOARD5:2;
i+1 <= i+2 by AXIOMS:24;
then 1 <= i+1 & i+1 <= len GoB f by A1,AXIOMS:22,NAT_1:29;
then A6: (GoB f)*(i+1,width GoB f)`2 = (GoB f)*
(1,width GoB f)`2 by A2,GOBOARD5:2;
1 <= i+2 by A1,A4,AXIOMS:22;
then A7: (GoB f)*(i+2,width GoB f)`2 = (GoB f)*(1,width GoB f)`2
by A1,A2,GOBOARD5:2;
(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:7
.= 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f))`2+|[0,1]|`2
by TOPREAL3:9
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+|[0,1]|`2
by A5,A6,TOPREAL3:7
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+1
by EUCLID:56
.= 1/2*(2*((GoB f)*(1,width GoB f))`2)+1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,width GoB f))`2+1 by XCMPLX_1:4
.= 1*((GoB f)*(1,width GoB f))`2+1;
then A8: 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:57;
(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:7
.= 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*
(i+2,width GoB f))`2+|[0,1]|`2
by TOPREAL3:9
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+|[0,1]|`2
by A6,A7,TOPREAL3:7
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+1
by EUCLID:56
.= 1/2*(2*((GoB f)*(1,width GoB f))`2)+1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,width GoB f))`2+1 by XCMPLX_1:4
.= 1*((GoB f)*(1,width GoB f))`2+1;
then 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:57;
then p`2 = (GoB f)*(1,width GoB f)`2 + 1 by A3,A8,TOPREAL3:18;
hence p`2 > (GoB f)*(1,width GoB f)`2 by REAL_1:69;
end;
hence 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 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:35;
now let p such that
A2: 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]|);
1 < len GoB f by GOBOARD7:34;
then 1+1 <= len GoB f by NAT_1:38;
then A3: (GoB f)*(2,width GoB f)`2 = (GoB f)*(1,width GoB f)`2 by A1,GOBOARD5:
2;
((GoB f)*(1,width GoB f)+|[-1,1]|)`2
= ((GoB f)*(1,width GoB f))`2+|[-1,1]|`2 by TOPREAL3:7
.= (GoB f)*(1,width GoB f)`2+1 by EUCLID:56;
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:57;
(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:7
.= 1/2*((GoB f)*(1,width GoB f)+(GoB f)*(2,width GoB f))`2+|[0,1]|`2
by TOPREAL3:9
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+|[0,1]|`2
by A3,TOPREAL3:7
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+1
by EUCLID:56
.= 1/2*(2*((GoB f)*(1,width GoB f))`2)+1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,width GoB f))`2+1 by XCMPLX_1:4
.= 1*((GoB f)*(1,width GoB f))`2+1;
then 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:57;
then p`2 = (GoB f)*(1,width GoB f)`2 + 1 by A2,A4,TOPREAL3:18;
hence p`2 > (GoB f)*(1,width GoB f)`2 by REAL_1:69;
end;
hence 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 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:35;
now let p such that
A2: 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]|);
A3: 1 < len GoB f by GOBOARD7:34;
then A4: len GoB f -' 1 +1 = len GoB f by AMI_5:4;
then A5: 1 <= len GoB f -' 1 by A3,NAT_1:38;
len GoB f -' 1 <= len GoB f by A4,NAT_1:29;
then A6: (GoB f)*(len GoB f -' 1,width GoB f)`2 = (GoB f)*(1,width GoB f)`2
by A1,A5,GOBOARD5:2;
A7: (GoB f)*(len GoB f,width GoB f)`2 = (GoB f)*(1,width GoB f)`2
by A1,A3,GOBOARD5:2;
(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:7
.= 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:9
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+|[0,1]|`2
by A6,A7,TOPREAL3:7
.= 1/2*((GoB f)*(1,width GoB f)`2+(GoB f)*(1,width GoB f)`2)+1
by EUCLID:56
.= 1/2*(2*((GoB f)*(1,width GoB f))`2)+1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,width GoB f))`2+1 by XCMPLX_1:4
.= 1*((GoB f)*(1,width GoB f))`2+1;
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:57;
((GoB f)*(len GoB f,width GoB f)+|[1,1]|)`2
= (GoB f)*(1,width GoB f)`2+|[1,1]|`2 by A7,TOPREAL3:7
.= (GoB f)*(1,width GoB f)`2+1 by EUCLID:56;
then (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:57;
then p`2 = (GoB f)*(1,width GoB f)`2 + 1 by A2,A8,TOPREAL3:18;
hence p`2 > (GoB f)*(1,width GoB f)`2 by REAL_1:69;
end;
hence 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 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 & j+2 <= width GoB f;
A2: 1 <= len GoB f by GOBOARD7:34;
now let p such that
A3: 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]|);
A4: j <= j+2 by NAT_1:29;
then j <= width GoB f by A1,AXIOMS:22;
then A5: (GoB f)*(1,j)`1 = (GoB f)*(1,1)`1 by A1,A2,GOBOARD5:3;
j+1 <= j+2 by AXIOMS:24;
then 1 <= j+1 & j+1 <= width GoB f by A1,AXIOMS:22,NAT_1:29;
then A6: (GoB f)*(1,j+1)`1 = (GoB f)*(1,1)`1 by A2,GOBOARD5:3;
1 <= j+2 by A1,A4,AXIOMS:22;
then A7: (GoB f)*(1,j+2)`1 = (GoB f)*(1,1)`1 by A1,A2,GOBOARD5:3;
(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:8
.= 1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1))`1- |[1,0]|`1 by TOPREAL3:9
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)- |[1,0]|`1 by A5,A6,TOPREAL3:7
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)-1 by EUCLID:56
.= 1/2*(2*((GoB f)*(1,1))`1)-1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,1))`1-1 by XCMPLX_1:4
.= 1*((GoB f)*(1,1))`1-1;
then A8: 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:57;
(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:8
.= 1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2))`1- |[1,0]|`1 by TOPREAL3:9
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)- |[1,0]|`1 by A6,A7,TOPREAL3:7
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)-1 by EUCLID:56
.= 1/2*(2*((GoB f)*(1,1))`1)-1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,1))`1-1 by XCMPLX_1:4
.= 1*((GoB f)*(1,1))`1-1;
then 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:57;
then p`1 = (GoB f)*(1,1)`1 - 1 by A3,A8,TOPREAL3:17;
hence p`1 < (GoB f)*(1,1)`1 by REAL_2:174;
end;
hence 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 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:34;
now let p such that
A2: p in LSeg((GoB f)*(1,1)- |[1,1]|,
1/2*((GoB f)*(1,1)+(GoB f)*(1,2))- |[1,0]|);
1 < width GoB f by GOBOARD7:35;
then 1+1 <= width GoB f by NAT_1:38;
then A3: (GoB f)*(1,2)`1 = (GoB f)*(1,1)`1 by A1,GOBOARD5:3;
((GoB f)*(1,1)- |[1,1]|)`1 = ((GoB f)*(1,1))`1- |[1,1]|`1 by TOPREAL3:8
.= (GoB f)*(1,1)`1-1 by EUCLID:56;
then A4: (GoB f)*(1,1)- |[1,1]|
= |[(GoB f)*(1,1)`1-1,((GoB f)*(1,1)- |[1,1]|)`2]| by EUCLID:57;
(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:8
.= 1/2*((GoB f)*(1,1)+(GoB f)*(1,2))`1- |[1,0]|`1 by TOPREAL3:9
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)- |[1,0]|`1 by A3,TOPREAL3:7
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)-1 by EUCLID:56
.= 1/2*(2*((GoB f)*(1,1))`1)-1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,1))`1-1 by XCMPLX_1:4
.= 1*((GoB f)*(1,1))`1-1;
then 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:57;
then p`1 = (GoB f)*(1,1)`1 - 1 by A2,A4,TOPREAL3:17;
hence p`1 < (GoB f)*(1,1)`1 by REAL_2:174;
end;
hence LSeg((GoB f)*(1,1)- |[1,1]|,
1/2*((GoB f)*(1,1)+(GoB f)*(1,2))- |[1,0]|) misses L~f 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:34;
now let p such that
A2: 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]|);
A3: 1 < width GoB f by GOBOARD7:35;
then A4: width GoB f -' 1 +1 = width GoB f by AMI_5:4;
then A5: 1 <= width GoB f -' 1 by A3,NAT_1:38;
width GoB f -' 1 <= width GoB f by A4,NAT_1:29;
then A6: (GoB f)*(1,width GoB f -' 1)`1 = (GoB f)*(1,1)`1 by A1,A5,GOBOARD5:3;
A7: (GoB f)*(1,width GoB f)`1 = (GoB f)*(1,1)`1 by A1,A3,GOBOARD5:3;
(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:8
.= 1/2*((GoB f)*(1,width GoB f -' 1)+(GoB f)*
(1,width GoB f))`1- |[1,0]|`1 by TOPREAL3:9
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)- |[1,0]|`1 by A6,A7,TOPREAL3:7
.= 1/2*((GoB f)*(1,1)`1+(GoB f)*(1,1)`1)-1 by EUCLID:56
.= 1/2*(2*((GoB f)*(1,1))`1)-1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(1,1))`1-1 by XCMPLX_1:4
.= 1*((GoB f)*(1,1))`1-1;
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:57;
((GoB f)*(1,width GoB f)+|[-1,1]|)`1
= (GoB f)*(1,1)`1+|[-1,1]|`1 by A7,TOPREAL3:7
.= (GoB f)*(1,1)`1+-1 by EUCLID:56
.= (GoB f)*(1,1)`1-1 by XCMPLX_0:def 8;
then (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:57;
then p`1 = (GoB f)*(1,1)`1 - 1 by A2,A8,TOPREAL3:17;
hence p`1 < (GoB f)*(1,1)`1 by REAL_2:174;
end;
hence 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 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 & j+2 <= width GoB f;
A2: 1 <= len GoB f by GOBOARD7:34;
now let p such that
A3: 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]|);
A4: j <= j+2 by NAT_1:29;
then j <= width GoB f by A1,AXIOMS:22;
then A5: (GoB f)*(len GoB f,j)`1 = (GoB f)*(len GoB f,1)`1 by A1,A2,GOBOARD5:3
;
j+1 <= j+2 by AXIOMS:24;
then 1 <= j+1 & j+1 <= width GoB f by A1,AXIOMS:22,NAT_1:29;
then A6: (GoB f)*(len GoB f,j+1)`1 = (GoB f)*(len GoB f,1)`1 by A2,GOBOARD5:3;
1 <= j+2 by A1,A4,AXIOMS:22;
then A7: (GoB f)*(len GoB f,j+2)`1 = (GoB f)*(len GoB f,1)`1
by A1,A2,GOBOARD5:3;
(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:7
.= 1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1))`1+|[1,0]|`1
by TOPREAL3:9
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+|[1,0]|`1
by A5,A6,TOPREAL3:7
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+1
by EUCLID:56
.= 1/2*(2*((GoB f)*(len GoB f,1))`1)+1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(len GoB f,1))`1+1 by XCMPLX_1:4
.= 1*((GoB f)*(len GoB f,1))`1+1;
then A8: 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:57;
(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:7
.= 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))`1+|[1,0]|`1
by TOPREAL3:9
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+|[1,0]|`1
by A6,A7,TOPREAL3:7
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+1
by EUCLID:56
.= 1/2*(2*((GoB f)*(len GoB f,1))`1)+1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(len GoB f,1))`1+1 by XCMPLX_1:4
.= 1*((GoB f)*(len GoB f,1))`1+1;
then 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:57;
then p`1 = (GoB f)*(len GoB f,1)`1 + 1 by A3,A8,TOPREAL3:17;
hence p`1 > (GoB f)*(len GoB f,1)`1 by REAL_1:69;
end;
hence 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 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:34;
now let p such that
A2: 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]|);
1 < width GoB f by GOBOARD7:35;
then 1+1 <= width GoB f by NAT_1:38;
then A3: (GoB f)*(len GoB f,2)`1 = (GoB f)*(len GoB f,1)`1 by A1,GOBOARD5:3;
((GoB f)*(len GoB f,1)+|[1,-1]|)`1
= ((GoB f)*(len GoB f,1))`1+|[1,-1]|`1 by TOPREAL3:7
.= (GoB f)*(len GoB f,1)`1+1 by EUCLID:56;
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:57;
(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:7
.= 1/2*((GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2))`1+|[1,0]|`1
by TOPREAL3:9
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+|[1,0]|`1
by A3,TOPREAL3:7
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+1
by EUCLID:56
.= 1/2*(2*((GoB f)*(len GoB f,1))`1)+1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(len GoB f,1))`1+1 by XCMPLX_1:4
.= 1*((GoB f)*(len GoB f,1))`1+1;
then 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:57;
then p`1 = (GoB f)*(len GoB f,1)`1 + 1 by A2,A4,TOPREAL3:17;
hence p`1 > (GoB f)*(len GoB f,1)`1 by REAL_1:69;
end;
hence 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 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:34;
now let p such that
A2: 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]|);
A3: 1 < width GoB f by GOBOARD7:35;
then A4: width GoB f -' 1 +1 = width GoB f by AMI_5:4;
then A5: 1 <= width GoB f -' 1 by A3,NAT_1:38;
width GoB f -' 1 <= width GoB f by A4,NAT_1:29;
then A6: (GoB f)*(len GoB f,width GoB f -' 1)`1 = (GoB f)*(len GoB f,1)`1
by A1,A5,GOBOARD5:3;
A7: (GoB f)*(len GoB f,width GoB f)`1 = (GoB f)*(len GoB f,1)`1
by A1,A3,GOBOARD5:3;
(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:7
.= 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:9
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+|[1,0]|`1
by A6,A7,TOPREAL3:7
.= 1/2*((GoB f)*(len GoB f,1)`1+(GoB f)*(len GoB f,1)`1)+1
by EUCLID:56
.= 1/2*(2*((GoB f)*(len GoB f,1))`1)+1 by XCMPLX_1:11
.= 1/2*2*((GoB f)*(len GoB f,1))`1+1 by XCMPLX_1:4
.= 1*((GoB f)*(len GoB f,1))`1+1;
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:57;
((GoB f)*(len GoB f,width GoB f)+|[1,1]|)`1
= (GoB f)*(len GoB f,1)`1+|[1,1]|`1 by A7,TOPREAL3:7
.= (GoB f)*(len GoB f,1)`1+1 by EUCLID:56;
then (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:57;
then p`1 = (GoB f)*(len GoB f,1)`1 + 1 by A2,A8,TOPREAL3:17;
hence p`1 > (GoB f)*(len GoB f,1)`1 by REAL_1:69;
end;
hence 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 by Th22;
end;
theorem
1 <= k & k+1 <= len f implies Int left_cell(f,k) misses L~f
proof assume
A1: 1 <= k & k+1 <= len f;
k <= k+1 by NAT_1:29;
then k <= len f by A1,AXIOMS:22;
then A2: k in dom f by A1,FINSEQ_3:27;
then consider i1,j1 being Nat such that
A3: [i1,j1] in Indices GoB f and
A4: f/.k = (GoB f)*(i1,j1) by GOBOARD2:25;
A5: i1 <= len GoB f by A3,GOBOARD5:1;
A6: j1 <= width GoB f by A3,GOBOARD5:1;
i1 <> 0 by A3,GOBOARD5:1;
then consider i such that
A7: i1 = i+1 by NAT_1:22;
i <= i1 by A7,NAT_1:29;
then A8: i <= len GoB f by A5,AXIOMS:22;
j1 <> 0 by A3,GOBOARD5:1;
then consider j such that
A9: j1 = j+1 by NAT_1:22;
j <= j1 by A9,NAT_1:29;
then A10: j <= width GoB f by A6,AXIOMS:22;
k+1 >= 1 by NAT_1:29;
then A11: k+1 in dom f by A1,FINSEQ_3:27;
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:25;
A14: i2 <= len GoB f by A12,GOBOARD5:1;
A15: j2 <= width GoB f by A12,GOBOARD5:1;
abs(i1-i2)+abs(j1-j2) = 1 by A2,A3,A4,A11,A12,A13,GOBOARD5:13;
then A16: abs(i1-i2) = 1 & j1 = j2 or abs(j1-j2)=1 & i1 = i2 by GOBOARD1:2;
per cases by A16,GOBOARD1:1;
suppose i1 = i2 & j1+1 = j2;
then left_cell(f,k) = cell(GoB f,i,j1) by A1,A3,A4,A7,A12,A13,GOBOARD5:28;
hence thesis by A6,A8,GOBOARD7:14;
suppose i1+1 = i2 & j1 = j2;
then left_cell(f,k) = cell(GoB f,i1,j1) by A1,A3,A4,A9,A12,A13,GOBOARD5:29;
hence thesis by A5,A6,GOBOARD7:14;
suppose i1 = i2+1 & j1 = j2;
then left_cell(f,k) = cell(GoB f,i2,j) by A1,A3,A4,A9,A12,A13,GOBOARD5:30;
hence thesis by A10,A14,GOBOARD7:14;
suppose i1 = i2 & j1 = j2+1;
then left_cell(f,k) = cell(GoB f,i1,j2) by A1,A3,A4,A7,A12,A13,GOBOARD5:31;
hence thesis by A5,A15,GOBOARD7:14;
end;
theorem
1 <= k & k+1 <= len f implies Int right_cell(f,k) misses L~f
proof assume
A1: 1 <= k & k+1 <= len f;
k <= k+1 by NAT_1:29;
then k <= len f by A1,AXIOMS:22;
then A2: k in dom f by A1,FINSEQ_3:27;
then consider i1,j1 being Nat such that
A3: [i1,j1] in Indices GoB f and
A4: f/.k = (GoB f)*(i1,j1) by GOBOARD2:25;
A5: i1 <= len GoB f by A3,GOBOARD5:1;
A6: j1 <= width GoB f by A3,GOBOARD5:1;
i1 <> 0 by A3,GOBOARD5:1;
then consider i such that
A7: i1 = i+1 by NAT_1:22;
i <= i1 by A7,NAT_1:29;
then A8: i <= len GoB f by A5,AXIOMS:22;
j1 <> 0 by A3,GOBOARD5:1;
then consider j such that
A9: j1 = j+1 by NAT_1:22;
j <= j1 by A9,NAT_1:29;
then A10: j <= width GoB f by A6,AXIOMS:22;
k+1 >= 1 by NAT_1:29;
then A11: k+1 in dom f by A1,FINSEQ_3:27;
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:25;
A14: i2 <= len GoB f by A12,GOBOARD5:1;
A15: j2 <= width GoB f by A12,GOBOARD5:1;
abs(i1-i2)+abs(j1-j2) = 1 by A2,A3,A4,A11,A12,A13,GOBOARD5:13;
then A16: abs(i1-i2) = 1 & j1 = j2 or abs(j1-j2)=1 & i1 = i2 by GOBOARD1:2;
per cases by A16,GOBOARD1:1;
suppose i1 = i2 & j1+1 = j2;
then right_cell(f,k) = cell(GoB f,i1,j1) by A1,A3,A4,A7,A12,A13,GOBOARD5:28
;
hence thesis by A5,A6,GOBOARD7:14;
suppose i1+1 = i2 & j1 = j2;
then right_cell(f,k) = cell(GoB f,i1,j) by A1,A3,A4,A9,A12,A13,GOBOARD5:29;
hence thesis by A5,A10,GOBOARD7:14;
suppose i1 = i2+1 & j1 = j2;
then right_cell(f,k) = cell(GoB f,i2,j1) by A1,A3,A4,A9,A12,A13,GOBOARD5:30
;
hence thesis by A6,A14,GOBOARD7:14;
suppose i1 = i2 & j1 = j2+1;
then right_cell(f,k) = cell(GoB f,i,j2) by A1,A3,A4,A7,A12,A13,GOBOARD5:31;
hence thesis by A8,A15,GOBOARD7:14;
end;