### The Mizar article:

### Gauges

**by****Czeslaw Bylinski**

- Received January 22, 1999
Copyright (c) 1999 Association of Mizar Users

- MML identifier: JORDAN8
- [ MML identifier index ]

environ vocabulary FINSEQ_1, MATRIX_1, RELAT_1, FINSEQ_4, BOOLE, FUNCT_1, GOBOARD1, ABSVALUE, ARYTM_1, RFINSEQ, PRE_TOPC, EUCLID, GOBOARD5, TOPREAL1, GOBOARD2, TREES_1, MCART_1, SEQM_3, COMPTS_1, SPPOL_1, PSCOMP_1, ARYTM_3, GROUP_1, INCSP_1, JORDAN8; notation TARSKI, XBOOLE_0, ZFMISC_1, XREAL_0, REAL_1, NAT_1, STRUCT_0, BINARITH, ABSVALUE, RELAT_1, FUNCT_1, CARD_4, FINSEQ_1, FINSEQ_4, RFINSEQ, MATRIX_1, PRE_TOPC, COMPTS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD5; constructors REAL_1, ABSVALUE, FINSEQ_4, CARD_4, RFINSEQ, SEQM_3, BINARITH, COMPTS_1, GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD5; clusters STRUCT_0, RELAT_1, RELSET_1, EUCLID, GOBOARD2, FINSEQ_5, SPRECT_1, NAT_1, MEMBERED; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions GOBOARD1, GOBOARD5, TOPREAL1, XBOOLE_0; theorems ZFMISC_1, NAT_1, FINSEQ_1, MATRIX_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, AXIOMS, REAL_1, REAL_2, HEINE, JORDAN3, SQUARE_1, PSCOMP_1, SPRECT_1, FINSEQ_5, GOBOARD7, TOPREAL1, GOBOARD5, SPRECT_2, ABSVALUE, GROUP_5, GOBOARD9, UNIFORM1, SUBSET_1, GOBRD11, GOBOARD2, SPRECT_3, JORDAN5D, SCMFSA_7, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes MATRIX_1; begin reserve i,i1,i2,i',i1',j,j1,j2,j',j1',k,l,m,n for Nat; reserve r,s,r',s' for Real; reserve D for set, f for FinSequence of D, G for Matrix of D; theorem len f >= 2 implies f|2 = <*f/.1,f/.2*> proof assume A1: len f >= 2; then A2: len(f|2) = 2 by TOPREAL1:3; set d1 = f/.1, d2 = f/.2; now A3: rng f c= D by FINSEQ_1:def 4; assume D is empty; then rng f = {} by A3,XBOOLE_1:3; then f = {} by RELAT_1:64; then len f = 0 by FINSEQ_1:25; hence contradiction by A1; end; then reconsider D as non empty set; reconsider f as FinSequence of D; 1 in dom(f|2) by A2,FINSEQ_3:27; then A4: d1 = (f|2)/.1 by TOPREAL1:1 .= (f|2).1 by A2,FINSEQ_4:24; 2 in dom(f|2) by A2,FINSEQ_3:27; then d2 = (f|2)/.2 by TOPREAL1:1 .= (f|2).2 by A2,FINSEQ_4:24; hence thesis by A2,A4,FINSEQ_1:61; end; theorem k+1 <= len f implies f|(k+1) = (f|k)^<*f/.(k+1)*> proof assume A1: k+1 <= len f; 1 <= k+1 by NAT_1:37; then A2: k+1 in dom f by A1,FINSEQ_3:27; f|k = f|Seg k by TOPREAL1:def 1; then f|Seg(k+1) = (f|k)^<*f.(k+1)*> by A2,FINSEQ_5:11; hence f|(k+1) = (f|k)^<*f.(k+1)*> by TOPREAL1:def 1 .= (f|k)^<*f/.(k+1)*> by A2,FINSEQ_4:def 4; end; theorem <*>D is_sequence_on G proof set f = <*>D; thus (for n st n in dom f ex i,j st [i,j] in Indices G & f/.n = G*(i,j)) & for n st n in dom f & n+1 in dom f holds for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & f/.n = G*(m,k) & f/.(n+1) = G*(i,j) holds abs(m-i)+abs(k-j) = 1; end; canceled; theorem for D being non empty set, f being FinSequence of D, G being Matrix of D st f is_sequence_on G holds f/^m is_sequence_on G proof let D be non empty set, f be FinSequence of D, G be Matrix of D such that A1: for n st n in dom f ex i,j st [i,j] in Indices G & f/.n = G*(i,j) and A2: for n st n in dom f & n+1 in dom f for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & f/.n=G*(m,k) & f/.(n+1)=G*(i,j) holds abs(m-i)+abs(k-j) = 1; set g = f/^m; hereby let n; assume A3: n in dom g; then n+m in dom f by FINSEQ_5:29; then consider i,j such that A4: [i,j] in Indices G and A5: f/.(n+m) = G*(i,j) by A1; take i,j; thus [i,j] in Indices G by A4; thus g/.n = G*(i,j) by A3,A5,FINSEQ_5:30; end; let n such that A6: n in dom g and A7: n+1 in dom g; let i1,j1,i2,j2 such that A8: [i1,j1] in Indices G & [i2,j2] in Indices G and A9: g/.n = G*(i1,j1) & g/.(n+1) = G*(i2,j2); A10: n+m in dom f by A6,FINSEQ_5:29; A11: n+1+m = n+m+1 by XCMPLX_1:1; then A12: n+m+1 in dom f by A7,FINSEQ_5:29; f/.(n+m) = g/.n & f/.(n+m+1) = g/.(n+1) by A6,A7,A11,FINSEQ_5:30; hence abs(i1-i2)+abs(j1-j2) = 1 by A2,A8,A9,A10,A12; end; theorem Th6: 1 <= k & k+1 <= len f & f is_sequence_on G implies ex i1,j1,i2,j2 being Nat st [i1,j1] in Indices G & f/.k = G*(i1,j1) & [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) & (i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1) proof assume that A1: 1 <= k & k+1 <= len f and A2: f is_sequence_on G; k <= k+1 by NAT_1:29; then k <= len f by A1,AXIOMS:22; then A3: k in dom f by A1,FINSEQ_3:27; then consider i1,j1 being Nat such that A4: [i1,j1] in Indices G & f/.k = G*(i1,j1) by A2,GOBOARD1:def 11; k+1 >= 1 by NAT_1:29; then A5: k+1 in dom f by A1,FINSEQ_3:27; then consider i2,j2 being Nat such that A6: [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) by A2,GOBOARD1:def 11; A7: abs(i1-i2)+abs(j1-j2) = 1 by A2,A3,A4,A5,A6,GOBOARD1:def 11; now per cases by A7,GOBOARD1:2; case that A8: abs(i1-i2) = 1 and A9: j1 = j2; A10: -(i1-i2) = i2-i1 by XCMPLX_1:143; i1-i2 >= 0 or i1-i2 < 0; then i1-i2 = 1 or -(i1-i2) = 1 by A8,ABSVALUE:def 1; hence i1 = i2+1 or i1+1 = i2 by A10,XCMPLX_1:27; thus j1 = j2 by A9; case that A11: i1 = i2 and A12: abs(j1-j2) = 1; A13: -(j1-j2) = j2-j1 by XCMPLX_1:143; j1-j2 >= 0 or j1-j2 < 0; then j1-j2 = 1 or -(j1-j2) = 1 by A12,ABSVALUE:def 1; hence j1 = j2+1 or j1+1 = j2 by A13,XCMPLX_1:27; thus i1 = i2 by A11; end; hence thesis by A4,A6; end; reserve G for Go-board, p for Point of TOP-REAL 2; theorem for f being non empty FinSequence of TOP-REAL 2 st f is_sequence_on G holds f is standard special proof let f be non empty FinSequence of TOP-REAL 2 such that A1: f is_sequence_on G; thus f is_sequence_on GoB f proof set F = GoB f; thus for n st n in dom f ex i,j st [i,j] in Indices GoB f & f/.n = (GoB f)* (i,j) by GOBOARD2:25; let n such that A2: n in dom f & n+1 in dom f; let m,k,i,j such that A3: [m,k] in Indices GoB f and A4: [i,j] in Indices GoB f and A5: f/.n = (GoB f)*(m,k) and A6: f/.(n+1) = (GoB f)*(i,j); A7: 1 <= m & m <= len F & 1 <= k & k <= width F by A3,GOBOARD5:1; A8: 1 <= i & i <= len F & 1 <= j & j <= width F by A4,GOBOARD5:1; then A9: F*(i,j)`1 = F*(i,1)`1 & F*(i,k)`1 = F*(i,1)`1 by A7,GOBOARD5:3; A10: F*(i,j)`2 = F*(1,j)`2 & F*(m,j)`2 = F*(1,j)`2 by A7,A8,GOBOARD5:2; 1 <= n & n+1 <= len f by A2,FINSEQ_3:27; then consider i1,j1,i2,j2 such that A11: [i1,j1] in Indices G and A12: f/.n = G*(i1,j1) and A13: [i2,j2] in Indices G and A14: f/.(n+1) = G*(i2,j2) and A15: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,Th6; A16: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A11,GOBOARD5:1; A17: 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A13,GOBOARD5:1; then A18: G*(i1,j1)`1 = G*(i1,1)`1 & G*(i2,j2)`1 = G*(i2,1)`1 by A16,GOBOARD5:3; A19: G*(i1,j1)`2 = G*(1,j1)`2 & G*(i2,j1)`2 = G*(1,j1)`2 by A16,A17,GOBOARD5:2; A20: k+1 >= 1 & j+1 >= 1 & m+1 >= 1 & i+1 >= 1 by NAT_1:37; A21: k+1 > k & j+1 > j & m+1 > m & i+1 > i by NAT_1:38; per cases by A15; suppose A22: i1 = i2 & j1+1 = j2; now assume m <> i; then m < i or m > i by REAL_1:def 5; hence contradiction by A5,A6,A7,A8,A9,A12,A14,A18,A22,GOBOARD5:4; end; then m-i = 0 by XCMPLX_1:14; then A23: abs(m-i) = 0 by ABSVALUE:7; now assume j <= k; then A24: F*(i,j)`2 <= F*(m,k)`2 by A7,A8,A10,SPRECT_3:24; j1 < j2 by A22,NAT_1:38; hence contradiction by A5,A6,A12,A14,A16,A17,A19,A24,GOBOARD5:5; end; then A25: k+1 <= j by NAT_1:38; now assume A26: k+1 < j; then A27: k+1 < width F by A8,AXIOMS:22; then consider l,i' such that A28: l in dom f and A29: [i',k+1] in Indices F and A30: f/.l = F*(i',k+1) by A20,JORDAN5D:10; 1 <= i' & i' <= len F by A29,GOBOARD5:1; then A31: F*(i',k+1)`2 = F*(1,k+1)`2 & F*(m,k+1)`2 = F*(1,k+1)`2 by A7,A20,A27,GOBOARD5:2; consider i1',j1' such that A32: [i1',j1'] in Indices G and A33: f/.l = G*(i1',j1') by A1,A28,GOBOARD1:def 11; A34: 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G by A32,GOBOARD5:1; then A35: G*(i1',j1')`2 = G*(1,j1')`2 & G*(i1',j1)`2 = G*(1,j1)`2 by A16,GOBOARD5:2; A36: G*(i2,j2)`2 = G*(1,j2)`2 & G*(i1',j2)`2 = G*(1,j2)`2 by A17,A34,GOBOARD5:2; A37: now assume j1 >= j1'; then G*(i1',j1')`2 <= G*(i1,j1)`2 by A16,A19,A34,A35,SPRECT_3:24; hence contradiction by A5,A7,A12,A21,A27,A30,A31,A33,GOBOARD5:5; end; now assume j2 <= j1'; then G*(i2,j2)`2 <= G*(i1',j1')`2 by A17,A34,A36,SPRECT_3:24; hence contradiction by A6,A7,A8,A10,A14,A20,A26,A30,A31,A33,GOBOARD5:5; end; hence contradiction by A22,A37,NAT_1:38; end; then k+1 = j by A25,AXIOMS:21; then j-k = 1 by XCMPLX_1:26; then abs(j-k) = 1 by ABSVALUE:def 1; hence thesis by A23,UNIFORM1:13; suppose A38: i1+1 = i2 & j1 = j2; now assume k <> j; then k < j or k > j by REAL_1:def 5; hence contradiction by A5,A6,A7,A8,A10,A12,A14,A19,A38,GOBOARD5:5; end; then k-j = 0 by XCMPLX_1:14; then A39: abs(k-j) = 0 by ABSVALUE:7; now assume i <= m; then A40: F*(i,j)`1 <= F*(m,k)`1 by A7,A8,A9,SPRECT_3:25; i1 < i2 by A38,NAT_1:38; hence contradiction by A5,A6,A12,A14,A16,A17,A38,A40,GOBOARD5:4; end; then A41: m+1 <= i by NAT_1:38; now assume A42: m+1 < i; then A43: m+1 < len F by A8,AXIOMS:22; then consider l,j' such that A44: l in dom f and A45: [m+1,j'] in Indices F and A46: f/.l = F*(m+1,j') by A20,JORDAN5D:9; 1 <= j' & j' <= width F by A45,GOBOARD5:1; then A47: F*(m+1,j')`1 = F*(m+1,1)`1 & F*(m+1,k)`1 = F*(m+1,1)`1 by A7,A20,A43,GOBOARD5:3; consider i1',j1' such that A48: [i1',j1'] in Indices G and A49: f/.l = G*(i1',j1') by A1,A44,GOBOARD1:def 11; A50: 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G by A48,GOBOARD5:1; then A51: G*(i1',j1')`1 = G*(i1',1)`1 & G*(i1,j1')`1 = G*(i1,1)`1 by A16,GOBOARD5:3; A52: G*(i2,j2)`1 = G*(i2,1)`1 & G*(i2,j1')`1 = G*(i2,1)`1 by A17,A50,GOBOARD5:3; A53: now assume i1 >= i1'; then G*(i1',j1')`1 <= G*(i1,j1)`1 by A16,A18,A50,A51,SPRECT_3:25; hence contradiction by A5,A7,A12,A21,A43,A46,A47,A49,GOBOARD5:4; end; now assume i2 <= i1'; then G*(i2,j2)`1 <= G*(i1',j1')`1 by A17,A50,A52,SPRECT_3:25; hence contradiction by A6,A7,A8,A9,A14,A20,A42,A46,A47,A49,GOBOARD5:4 ; end; hence contradiction by A38,A53,NAT_1:38; end; then m+1 = i by A41,AXIOMS:21; then i-m = 1 by XCMPLX_1:26; then abs(i-m) = 1 by ABSVALUE:def 1; hence thesis by A39,UNIFORM1:13; suppose A54: i1 = i2+1 & j1 = j2; now assume k <> j; then k < j or k > j by REAL_1:def 5; hence contradiction by A5,A6,A7,A8,A10,A12,A14,A19,A54,GOBOARD5:5; end; then k-j = 0 by XCMPLX_1:14; then A55: abs(k-j) = 0 by ABSVALUE:7; now assume m <= i; then A56: F*(i,j)`1 >= F*(m,k)`1 by A7,A8,A9,SPRECT_3:25; i1 > i2 by A54,NAT_1:38; hence contradiction by A5,A6,A12,A14,A16,A17,A54,A56,GOBOARD5:4; end; then A57: i+1 <= m by NAT_1:38; now assume A58: i+1 < m; then A59: i+1 < len F by A7,AXIOMS:22; then consider l,j' such that A60: l in dom f and A61: [i+1,j'] in Indices F and A62: f/.l = F*(i+1,j') by A20,JORDAN5D:9; 1 <= j' & j' <= width F by A61,GOBOARD5:1; then A63: F*(i+1,j')`1 = F*(i+1,1)`1 & F*(i+1,j)`1 = F*(i+1,j)`1 by A20,A59,GOBOARD5:3; A64: F*(i+1,k)`1 = F*(i+1,1)`1 & F*(i+1,j)`1 = F*(i+1,1)`1 by A7,A8,A20,A59,GOBOARD5:3; consider i1',j1' such that A65: [i1',j1'] in Indices G and A66: f/.l = G*(i1',j1') by A1,A60,GOBOARD1:def 11; A67: 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G by A65,GOBOARD5:1; then A68: G*(i1',j1')`1 = G*(i1',1)`1 & G*(i1,j1')`1 = G*(i1,1)`1 by A16,GOBOARD5:3; A69: G*(i2,j2)`1 = G*(i2,1)`1 & G*(i2,j1')`1 = G*(i2,1)`1 by A17,A67,GOBOARD5:3; A70: now assume i2 >= i1'; then G*(i1',j1')`1 <= G*(i2,j2)`1 by A17,A67,A69,SPRECT_3:25; hence contradiction by A6,A8,A14,A21,A59,A62,A63,A64,A66,GOBOARD5:4; end; now assume i1 <= i1'; then G*(i1,j1)`1 <= G*(i1',j1')`1 by A16,A18,A67,A68,SPRECT_3:25; hence contradiction by A5,A7,A12,A20,A58,A62,A63,A64,A66,GOBOARD5:4; end; hence contradiction by A54,A70,NAT_1:38; end; then i+1 = m by A57,AXIOMS:21; then m-i = 1 by XCMPLX_1:26; hence thesis by A55,ABSVALUE:def 1; suppose A71: i1 = i2 & j1 = j2+1; now assume m <> i; then m < i or m > i by REAL_1:def 5; hence contradiction by A5,A6,A7,A8,A9,A12,A14,A18,A71,GOBOARD5:4; end; then m-i = 0 by XCMPLX_1:14; then A72: abs(m-i) = 0 by ABSVALUE:7; now assume j >= k; then A73: F*(i,j)`2 >= F*(m,k)`2 by A7,A8,A10,SPRECT_3:24; j1 > j2 by A71,NAT_1:38; hence contradiction by A5,A6,A12,A14,A16,A17,A19,A73,GOBOARD5:5; end; then A74: j+1 <= k by NAT_1:38; now assume A75: j+1 < k; then A76: j+1 < width F by A7,AXIOMS:22; then consider l,i' such that A77: l in dom f and A78: [i',j+1] in Indices F and A79: f/.l = F*(i',j+1) by A20,JORDAN5D:10; 1 <= i' & i' <= len F by A78,GOBOARD5:1; then A80: F*(i',j+1)`2 = F*(1,j+1)`2 & F*(i,j+1)`2 = F*(1,j+1)`2 by A8,A20,A76,GOBOARD5:2; A81: F*(m,j+1)`2 = F*(1,j+1)`2 & F*(i,j+1)`2 = F*(1,j+1)`2 by A7,A8,A20,A76,GOBOARD5:2; consider i1',j1' such that A82: [i1',j1'] in Indices G and A83: f/.l = G*(i1',j1') by A1,A77,GOBOARD1:def 11; A84: 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G by A82,GOBOARD5:1; then A85: G*(i1',j1')`2 = G*(1,j1')`2 & G*(i1',j1)`2 = G*(1,j1)`2 by A16,GOBOARD5:2; A86: G*(i2,j2)`2 = G*(1,j2)`2 & G*(i1',j2)`2 = G*(1,j2)`2 by A17,A84,GOBOARD5:2; A87: now assume j2 >= j1'; then G*(i1',j1')`2 <= G*(i2,j2)`2 by A17,A84,A86,SPRECT_3:24; hence contradiction by A6,A8,A14,A21,A76,A79,A80,A83,GOBOARD5:5; end; now assume j1 <= j1'; then G*(i1,j1)`2 <= G*(i1',j1')`2 by A16,A19,A84,A85,SPRECT_3:24; hence contradiction by A5,A7,A12,A20,A75,A79,A80,A81,A83,GOBOARD5:5; end; hence contradiction by A71,A87,NAT_1:38; end; then j+1 = k by A74,AXIOMS:21; then k-j = 1 by XCMPLX_1:26; hence thesis by A72,ABSVALUE:def 1; end; thus f is special proof let i; assume 1 <= i & i+1 <= len f; then consider i1,j1,i2,j2 such that A88: [i1,j1] in Indices G and A89: f/.i = G*(i1,j1) and A90: [i2,j2] in Indices G and A91: f/.(i+1) = G*(i2,j2) and A92: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,Th6; 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A88,A90,GOBOARD5:1; then G*(i1,j1)`2 = G*(1,j1)`2 & G*(i2,j1)`2 = G*(1,j1)`2 & G*(i1,j2)`2 = G*(1,j2)`2 & G*(i2,j2)`2 = G*(1,j2)`2 & G*(i1,j1)`1 = G*(i1,1)`1 & G*(i1,j2)`1 = G*(i1,1)`1 & G*(i2,j1)`1 = G*(i2,1)`1 & G*(i2,j2)`1 = G*(i2,1)`1 by GOBOARD5:2,3; hence (f/.i)`1 = (f/.(i+1))`1 or (f/.i)`2 = (f/.(i+1))`2 by A89,A91,A92; end; end; theorem for f being non empty FinSequence of TOP-REAL 2 st len f >= 2 & f is_sequence_on G holds f is non constant proof let f be non empty FinSequence of TOP-REAL 2 such that A1: len f >= 2 and A2: f is_sequence_on G; assume A3: for n,m st n in dom f & m in dom f holds f.n = f.m; 1 <= len f by A1,AXIOMS:22; then A4: 1 in dom f by FINSEQ_3:27; then consider i1,j1 such that A5: [i1,j1] in Indices G and A6: f/.1 = G*(i1,j1) by A2,GOBOARD1:def 11; A7: 1+1 in dom f by A1,FINSEQ_3:27; then consider i2,j2 such that A8: [i2,j2] in Indices G and A9: f/.2 = G*(i2,j2) by A2,GOBOARD1:def 11; f/.1 = f.1 by A4,FINSEQ_4:def 4 .= f.2 by A3,A4,A7 .= f/.2 by A7,FINSEQ_4:def 4; then i1 = i2 & j1 = j2 by A5,A6,A8,A9,GOBOARD1:21; then i1-i2 = 0 & j1-j2 = 0 by XCMPLX_1:14; then A10: abs(i1-i2) = 0 & abs(j1-j2) = 0 by ABSVALUE:7; abs(i1-i2) + abs(j1-j2) = 1 by A2,A4,A5,A6,A7,A8,A9,GOBOARD1:def 11; hence contradiction by A10; end; theorem for f being non empty FinSequence of TOP-REAL 2 st f is_sequence_on G & (ex i,j st [i,j] in Indices G & p = G*(i,j)) & (for i1,j1,i2,j2 st [i1,j1] in Indices G & [i2,j2] in Indices G & f/.len f = G*(i1,j1) & p = G*(i2,j2) holds abs(i2-i1)+abs(j2-j1) = 1) holds f^<*p*> is_sequence_on G proof let f be non empty FinSequence of TOP-REAL 2 such that A1: f is_sequence_on G and A2: ex i,j st [i,j] in Indices G & p = G*(i,j) and A3: for i1,j1,i2,j2 st [i1,j1] in Indices G & [i2,j2] in Indices G & f/.len f = G*(i1,j1) & p = G*(i2,j2) holds abs(i2-i1)+abs(j2-j1) = 1; A4: for n st n in dom f & n+1 in dom f holds for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & f/.n=G*(m,k) & f/.(n+1)=G*(i,j) holds abs(m-i)+abs(k-j)=1 by A1,GOBOARD1:def 11; A5: now let n; assume n in dom <*p*> & n+1 in dom <*p*>; then 1 <= n & n+1 <= len <*p*> by FINSEQ_3:27; then 1+1 <= n+1 & n+1 <= 1 by AXIOMS:24,FINSEQ_1:56; hence for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & <*p*>/.n=G*(m,k) & <*p*>/.(n+1)=G*(i,j) holds abs(m-i)+abs(k-j)=1 by AXIOMS:22; end; now let m,k,i,j such that A6: [m,k] in Indices G & [i,j] in Indices G & f/.len f=G*(m,k) & <*p*>/.1=G*(i,j) and len f in dom f & 1 in dom <*p*>; <*p*>/.1 = p by FINSEQ_4:25; then abs(i-m)+abs(j-k)=1 by A3,A6; hence 1 = abs(m-i)+abs(j-k) by UNIFORM1:13 .= abs(m-i)+abs(k-j) by UNIFORM1:13; end; then A7: for n st n in dom(f^<*p*>) & n+1 in dom(f^<*p*>) holds for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & (f^<*p*>)/.n =G*(m,k) & (f^<*p*>)/.(n+1)=G*(i,j) holds abs(m-i)+abs(k-j)=1 by A4,A5,GOBOARD1:40; now let n such that A8: n in dom(f^<*p*>); per cases by A8,FINSEQ_1:38; suppose A9: n in dom f; then consider i,j such that A10: [i,j] in Indices G and A11: f/.n = G*(i,j) by A1,GOBOARD1:def 11; take i,j; thus [i,j] in Indices G by A10; thus (f^<*p*>)/.n = G*(i,j) by A9,A11,GROUP_5:95; suppose ex l st l in dom <*p*> & n = (len f) + l; then consider l such that A12: l in dom <*p*> and A13: n = (len f) + l; consider i,j such that A14: [i,j] in Indices G and A15: p = G*(i,j) by A2; take i,j; thus [i,j] in Indices G by A14; 1 <= l & l <= len <*p*> by A12,FINSEQ_3:27; then 1 <= l & l <= 1 by FINSEQ_1:56; then l = 1 by AXIOMS:21; then <*p*>/.l = p by FINSEQ_4:25; hence (f^<*p*>)/.n = G*(i,j) by A12,A13,A15,GROUP_5:96; end; hence f^<*p*> is_sequence_on G by A7,GOBOARD1:def 11; end; theorem i+k < len G & 1 <= j & j < width G & cell(G,i,j) meets cell(G,i+k,j) implies k <= 1 proof assume that A1: i+k < len G and A2: 1 <= j & j < width G and A3: cell(G,i,j) meets cell(G,i+k,j) and A4: k > 1; cell(G,i,j) /\ cell(G,i+k,j) <> {} by A3,XBOOLE_0:def 7; then consider p such that A5: p in cell(G,i,j) /\ cell(G,i+k,j) by SUBSET_1:10; A6: p in cell(G,i,j) & p in cell(G,i+k,j) by A5,XBOOLE_0:def 3; i+k >= 1 by A4,NAT_1:37; then cell(G,i+k,j) = { |[r',s']| : G*(i+k,1)`1 <= r' & r' <= G*(i+k+1,1)`1 & G*(1,j)`2 <= s' & s' <= G*(1,j+1)`2 } by A1,A2,GOBRD11:32; then consider r',s' such that A7: p = |[r',s']| and A8: G*(i+k,1)`1 <= r' and r' <= G*(i+k+1,1)`1 & G*(1,j)`2 <= s' & s' <= G*(1,j+1)`2 by A6; A9: 1 < width G by A2,AXIOMS:22; i = 0 or i > 0 by NAT_1:19; then A10: i = 0 or i >= 1+0 by NAT_1:27; per cases by A10; suppose A11: i = 0; then cell(G,i,j) = {|[r,s]| : r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G* (1,j+1)`2} by A2,GOBRD11:26; then consider r,s such that A12: p = |[r,s]| and A13: r <= G*(1,1)`1 and G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A6; A14: k <= len G by A1,NAT_1:37; p`1 = r & p`1 = r' by A7,A12,EUCLID:56; then G*(k,1)`1 <= G*(1,1)`1 by A8,A11,A13,AXIOMS:22; hence contradiction by A4,A9,A14,GOBOARD5:4; suppose A15: i >= 1; i < len G by A1,NAT_1:37; then cell(G,i,j) = {|[r,s]|: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2} by A2,A15,GOBRD11:32; then consider r,s such that A16: p = |[r,s]| and G*(i,1)`1 <= r and A17: r <= G*(i+1,1)`1 and G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A6; A18: 1 <= i+1 & i+1 < k+i by A4,NAT_1:37,REAL_1:53; p`1 = r & p`1 = r' by A7,A16,EUCLID:56; then G*(i+k,1)`1 <= G*(i+1,1)`1 by A8,A17,AXIOMS:22; hence contradiction by A1,A9,A18,GOBOARD5:4; end; theorem Th11: for C being non empty compact Subset of TOP-REAL 2 holds C is vertical iff E-bound C <= W-bound C proof let C be non empty compact Subset of TOP-REAL 2; A1: E-bound C >= W-bound C by SPRECT_1:23; C is vertical iff W-bound C = E-bound C by SPRECT_1:17; hence thesis by A1,REAL_1:def 5; end; theorem Th12: for C being non empty compact Subset of TOP-REAL 2 holds C is horizontal iff N-bound C <= S-bound C proof let C be non empty compact Subset of TOP-REAL 2; A1: N-bound C >= S-bound C by SPRECT_1:24; C is horizontal iff N-bound C = S-bound C by SPRECT_1:18; hence thesis by A1,REAL_1:def 5; end; definition let C be Subset of TOP-REAL 2, n be Nat; deffunc f(Nat,Nat) = |[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*($1-2), (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*($2-2)]|; A1: 2|^n + 3 > 0 by NAT_1:19; func Gauge (C,n) -> Matrix of TOP-REAL 2 means :Def1: len it = 2|^n + 3 & len it = width it & for i,j st [i,j] in Indices it holds it*(i,j) = |[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i-2), (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2)]|; existence proof consider M being Matrix of (2|^n + 3) ,(2|^n + 3), the carrier of TOP-REAL 2 such that A2: for i,j st [i,j] in Indices M holds M*(i,j) = f(i,j) from MatrixLambda; take M; thus len M = 2|^n + 3 by MATRIX_1:def 3; hence len M = width M by A1,MATRIX_1:24; thus thesis by A2; end; uniqueness proof let M1,M2 be Matrix of TOP-REAL 2 such that A3: len M1 = 2|^n + 3 & len M1 = width M1 and A4: for i,j st [i,j] in Indices M1 holds M1*(i,j) = f(i,j) and A5: len M2 = 2|^n + 3 & len M2 = width M2 and A6: for i,j st [i,j] in Indices M2 holds M2*(i,j) = f(i,j); now let i,j; assume A7: [i,j] in Indices M1; M1 is Matrix of (2|^n + 3) ,(2|^n + 3), the carrier of TOP-REAL 2 & M2 is Matrix of (2|^n + 3) ,(2|^n + 3), the carrier of TOP-REAL 2 by A1,A3,A5,MATRIX_1:20; then A8: [i,j] in Indices M2 by A7,MATRIX_1:27; thus M1*(i,j) = f(i,j) by A4,A7 .= M2*(i,j) by A6,A8; end; hence thesis by A3,A5,MATRIX_1:21; end; end; definition let C be non empty Subset of TOP-REAL 2, n be Nat; cluster Gauge (C,n) -> non empty-yielding X_equal-in-line Y_equal-in-column; coherence proof set M = Gauge (C,n); len M = 2|^n + 3 & len M = width M by Def1; hence M is non empty-yielding by GOBOARD1:def 5; A1: Indices M = [:dom M,Seg width M:] by MATRIX_1:def 5; thus M is X_equal-in-line proof let i; assume A2: i in dom M; set l= Line(M,i), f = X_axis(l); let j1,j2 such that A3: j1 in dom f and A4: j2 in dom f; len l = width M by MATRIX_1:def 8; then A5: dom l = Seg width M by FINSEQ_1:def 3; A6: dom f = dom l by SPRECT_2:19; then A7: l/.j1 = l.j1 by A3,FINSEQ_4:def 4 .= M*(i,j1) by A3,A5,A6,MATRIX_1:def 8; A8: [i,j1] in Indices M by A1,A2,A3,A5,A6,ZFMISC_1:106; A9: l/.j2 = l.j2 by A4,A6,FINSEQ_4:def 4 .= M*(i,j2) by A4,A5,A6,MATRIX_1:def 8; A10: [i,j2] in Indices M by A1,A2,A4,A5,A6,ZFMISC_1:106; set x = (W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i-2); set d = ((N-bound C)-(S-bound C))/(2|^n); thus f.j1 = (l/.j1)`1 by A3,GOBOARD1:def 3 .= |[x,(S-bound C)+d*(j1-2)]|`1 by A7,A8,Def1 .= x by EUCLID:56 .= |[x,(S-bound C)+d*(j2-2)]|`1 by EUCLID:56 .= (l/.j2)`1 by A9,A10,Def1 .= f.j2 by A4,GOBOARD1:def 3; end; thus M is Y_equal-in-column proof let j; assume A11: j in Seg width M; set c = Col(M,j), f = Y_axis(c); let i1,i2 such that A12: i1 in dom f and A13: i2 in dom f; len c = len M by MATRIX_1:def 9; then A14: dom c = dom M by FINSEQ_3:31; A15: dom f = dom c by SPRECT_2:20; then A16: c/.i1 = c.i1 by A12,FINSEQ_4:def 4 .= M*(i1,j) by A12,A14,A15,MATRIX_1:def 9; A17: [i1,j] in Indices M by A1,A11,A12,A14,A15,ZFMISC_1:106; A18: c/.i2 = c.i2 by A13,A15,FINSEQ_4:def 4 .= M*(i2,j) by A13,A14,A15,MATRIX_1:def 9; A19: [i2,j] in Indices M by A1,A11,A13,A14,A15,ZFMISC_1:106; set y = (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2); set d = ((E-bound C)-(W-bound C))/(2|^n); thus f.i1 = (c/.i1)`2 by A12,GOBOARD1:def 4 .= |[(W-bound C)+d*(i1-2),y]|`2 by A16,A17,Def1 .= y by EUCLID:56 .= |[(W-bound C)+d*(i2-2),y]|`2 by EUCLID:56 .= (c/.i2)`2 by A18,A19,Def1 .= f.i2 by A13,GOBOARD1:def 4; end; end; end; definition let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2, n; cluster Gauge (C,n) -> Y_increasing-in-line X_increasing-in-column; coherence proof set M = Gauge (C,n); A1: Indices M = [:dom M,Seg width M:] by MATRIX_1:def 5; thus M is Y_increasing-in-line proof let i; assume A2: i in dom M; set l = Line(M,i), f = Y_axis(l); let j1,j2 such that A3: j1 in dom f and A4: j2 in dom f and A5: j1 < j2; len l = width M by MATRIX_1:def 8; then A6: dom l = Seg width M by FINSEQ_1:def 3; A7: dom f = dom l by SPRECT_2:20; then A8: l/.j1 = l.j1 by A3,FINSEQ_4:def 4 .= M*(i,j1) by A3,A6,A7,MATRIX_1:def 8; A9: [i,j1] in Indices M by A1,A2,A3,A6,A7,ZFMISC_1:106; A10: l/.j2 = l.j2 by A4,A7,FINSEQ_4:def 4 .= M*(i,j2) by A4,A6,A7,MATRIX_1:def 8; A11: [i,j2] in Indices M by A1,A2,A4,A6,A7,ZFMISC_1:106; set x = (W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i-2); set d = ((N-bound C)-(S-bound C))/(2|^n); A12: f.j1 = (l/.j1)`2 by A3,GOBOARD1:def 4 .= |[x,(S-bound C)+d*(j1-2)]|`2 by A8,A9,Def1 .= (S-bound C)+d*(j1-2) by EUCLID:56; A13: f.j2 = (l/.j2)`2 by A4,GOBOARD1:def 4 .= |[x,(S-bound C)+d*(j2-2)]|`2 by A10,A11,Def1 .= (S-bound C)+d*(j2-2) by EUCLID:56; N-bound C > S-bound C by Th12; then (N-bound C)-(S-bound C) > 0 & (2|^n) > 0 by HEINE:5,SQUARE_1:11; then A14: d > 0 by REAL_2:127; j1-2 < j2 -2 by A5,REAL_1:54; then d*(j1-2) < d*(j2-2) by A14,REAL_1:70; hence f.j1 < f.j2 by A12,A13,REAL_1:67; end; let j; assume A15: j in Seg width M; set c = Col(M,j), f = X_axis(c); let i1,i2 such that A16: i1 in dom f and A17: i2 in dom f and A18: i1 < i2; len c = len M by MATRIX_1:def 9; then A19: dom c = dom M by FINSEQ_3:31; A20: dom f = dom c by SPRECT_2:19; then A21: c/.i1 = c.i1 by A16,FINSEQ_4:def 4 .= M*(i1,j) by A16,A19,A20,MATRIX_1:def 9; A22: [i1,j] in Indices M by A1,A15,A16,A19,A20,ZFMISC_1:106; A23: c/.i2 = c.i2 by A17,A20,FINSEQ_4:def 4 .= M*(i2,j) by A17,A19,A20,MATRIX_1:def 9; A24: [i2,j] in Indices M by A1,A15,A17,A19,A20,ZFMISC_1:106; set y = (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2); set d = ((E-bound C)-(W-bound C))/(2|^n); A25: f.i1 = (c/.i1)`1 by A16,GOBOARD1:def 3 .= |[(W-bound C)+d*(i1-2),y]|`1 by A21,A22,Def1 .= (W-bound C)+d*(i1-2) by EUCLID:56; A26: f.i2 = (c/.i2)`1 by A17,GOBOARD1:def 3 .= |[(W-bound C)+d*(i2-2),y]|`1 by A23,A24,Def1 .= (W-bound C)+d*(i2-2) by EUCLID:56; E-bound C > W-bound C by Th11; then (E-bound C)-(W-bound C) > 0 & (2|^n) > 0 by HEINE:5,SQUARE_1:11; then A27: d > 0 by REAL_2:127; i1-2 < i2 -2 by A18,REAL_1:54; then d*(i1-2) < d*(i2-2) by A27,REAL_1:70; hence f.i1 < f.i2 by A25,A26,REAL_1:67; end; end; reserve T for non empty Subset of TOP-REAL 2; theorem Th13: len Gauge(T,n) >= 4 proof set G = Gauge(T,n); A1: len G = 2|^n + 3 by Def1; 2|^n >= n + 1 by HEINE:7; then len G >= n + 1 + 3 by A1,AXIOMS:24; then len G >= n + (3 + 1) & n+4 >= 4 by NAT_1:37,XCMPLX_1:1; hence len G >= 4 by AXIOMS:22; end; theorem 1 <= j & j <= len Gauge(T,n) implies Gauge(T,n)*(2,j)`1 = W-bound T proof set G = Gauge(T,n); set W = W-bound T, S = S-bound T, E = E-bound T, N = N-bound T; assume A1: 1 <= j & j <= len Gauge(T,n); A2: len G = 2|^n + 3 & len G = width G by Def1; len G >= 4 by Th13; then 2 <= len G by AXIOMS:22; then [2,j] in Indices G by A1,A2,GOBOARD7:10; then G*(2,j) = |[W+((E-W)/(2|^n))*(2-2), S+(N-S)/(2|^n)*(j-2)]| by Def1; hence G*(2,j)`1 = W-bound T by EUCLID:56; end; theorem 1 <= j & j <= len Gauge(T,n) implies Gauge(T,n)*(len Gauge(T,n)-'1,j)`1 = E-bound T proof set G = Gauge(T,n); set W = W-bound T, S = S-bound T, E = E-bound T, N = N-bound T; assume A1: 1 <= j & j <= len Gauge(T,n); A2: len G = 2|^n + 3 & len G = width G by Def1; len G >= 4 by Th13; then A3: 1 < len G by AXIOMS:22; then A4: 1 <= (len G)-'1 by JORDAN3:12; A5: (len G)-'1-2 = (len G)-1-2 by A3,SCMFSA_7:3 .= (len G)-(1+2) by XCMPLX_1:36 .= 2|^n by A2,XCMPLX_1:26; A6: 2|^n > 0 by HEINE:5; (len G)-'1 <= len G by GOBOARD9:2; then [(len G)-'1,j] in Indices G by A1,A2,A4,GOBOARD7:10; then G*((len G)-'1,j) = |[W+((E-W)/(2|^n))*((len G)-'1-2), S+((N-S)/(2|^n))*(j-2)]| by Def1; hence G*((len G)-'1,j)`1 = W+((E-W)/(2|^n))*(2|^n) by A5,EUCLID:56 .= W+(E-W) by A6,XCMPLX_1:88 .= E-bound T by XCMPLX_1:27; end; theorem 1 <= i & i <= len Gauge(T,n) implies Gauge(T,n)*(i,2)`2 = S-bound T proof set G = Gauge(T,n); set W = W-bound T, S = S-bound T, E = E-bound T, N = N-bound T; assume A1: 1 <= i & i <= len Gauge(T,n); A2: len G = 2|^n + 3 & len G = width G by Def1; len G >= 4 by Th13; then 2 <= len G by AXIOMS:22; then [i,2] in Indices G by A1,A2,GOBOARD7:10; then G*(i,2) = |[W+((E-W)/(2|^n))*(i-2), S+((N-S)/(2|^n))*(2-2)]| by Def1; hence G*(i,2)`2 = S-bound T by EUCLID:56; end; theorem 1 <= i & i <= len Gauge(T,n) implies Gauge(T,n)*(i,len Gauge(T,n)-'1)`2 = N-bound T proof set G = Gauge(T,n); set W = W-bound T, S = S-bound T, E = E-bound T, N = N-bound T; assume A1: 1 <= i & i <= len Gauge(T,n); A2: len G = 2|^n + 3 & len G = width G by Def1; len G >= 4 by Th13; then A3: 1 < len G by AXIOMS:22; then A4: 1 <= (len G)-'1 by JORDAN3:12; A5: (len G)-'1-2 = (len G)-1-2 by A3,SCMFSA_7:3 .= (len G)-(1+2) by XCMPLX_1:36 .= 2|^n by A2,XCMPLX_1:26; A6: 2|^n > 0 by HEINE:5; (len G)-'1 <= len G by GOBOARD9:2; then [i,(len G)-'1] in Indices G by A1,A2,A4,GOBOARD7:10; then G*(i,(len G)-'1) = |[W+((E-W)/(2|^n))*(i-2), S+((N-S)/(2|^n))*((len G)-'1-2)]| by Def1; hence G*(i,(len G)-'1)`2 = S+((N-S)/(2|^n))*(2|^n) by A5,EUCLID:56 .= S+(N-S) by A6,XCMPLX_1:88 .= N-bound T by XCMPLX_1:27; end; reserve C for compact non vertical non horizontal non empty Subset of TOP-REAL 2; theorem i <= len Gauge(C,n) implies cell(Gauge(C,n),i,len Gauge(C,n)) misses C proof set G = Gauge(C,n); assume A1: i <= len G; A2: len G = 2|^n + (1+2) & len G = width G by Def1; assume cell(G,i,len G) /\ C <> {}; then consider p such that A3: p in cell(G,i,len G) /\ C by SUBSET_1:10; A4: p in cell(G,i,len G) & p in C by A3,XBOOLE_0:def 3; 4 <= len G by Th13; then A5: 1 <= len G by AXIOMS:22; set W = W-bound C, S = S-bound C, E = E-bound C, N = N-bound C; set NS = (N-S)/(2|^n); [1,width G] in Indices G by A2,A5,GOBOARD7:10; then G*(1,width G) = |[W+((E-W)/(2|^n))*(1-2), S+NS*((width G)-2)]| by Def1; then A6: G*(1,width G)`2 = S+NS*((width G)-2) by EUCLID:56; A7: 2|^n > 0 by HEINE:5; N > S by Th12; then N-S > 0 by SQUARE_1:11; then A8: NS > 0 by A7,REAL_2:127; (width G)-2 = 2|^n + 1 + 2 - 2 by A2,XCMPLX_1:1 .= 2|^n + 1 by XCMPLX_1:26; then NS*((width G)-2) = NS*(2|^n) + NS*1 by XCMPLX_1:8 .= N-S+NS by A7,XCMPLX_1:88; then G*(1,width G)`2 = S+(N-S)+NS by A6,XCMPLX_1:1 .= N + NS by XCMPLX_1:27; then A9: G*(1,width G)`2 > N by A8,REAL_1:69; i = 0 or i > 0 by NAT_1:19; then A10: i = 0 or i >= 1+0 by NAT_1:27; per cases by A1,A10,REAL_1:def 5; suppose i = 0; then cell(G,i,width G) = { |[r,s]| : r <= G*(1,1)`1 & G*(1,width G)`2 <= s } by GOBRD11:25; then consider r,s such that A11: p = |[r,s]| and A12: r <= G*(1,1)`1 & G*(1,width G)`2 <= s by A2,A4; p`2 = s by A11,EUCLID:56; then N < p`2 & p`2 <= N by A4,A9,A12,AXIOMS:22,PSCOMP_1:71; hence contradiction; suppose i = len G; then cell(G,i,width G)={|[r,s]| : G*(len G,1)`1 <= r & G*(1,width G)`2 <= s } by GOBRD11:28; then consider r,s such that A13: p = |[r,s]| and A14: G*(len G,1)`1 <= r & G*(1,width G)`2 <= s by A2,A4; p`2 = s by A13,EUCLID:56; then N < p`2 & p`2 <= N by A4,A9,A14,AXIOMS:22,PSCOMP_1:71; hence contradiction; suppose 1 <= i & i < len G; then cell(G,i,width G) = {|[r,s]|: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G* (1,width G)`2 <= s} by GOBRD11:31; then consider r,s such that A15: p = |[r,s]| and A16: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,width G)`2 <= s by A2,A4; p`2 = s by A15,EUCLID:56; then N < p`2 & p`2 <= N by A4,A9,A16,AXIOMS:22,PSCOMP_1:71; hence contradiction; end; theorem j <= len Gauge(C,n) implies cell(Gauge(C,n),len Gauge(C,n),j) misses C proof set G = Gauge(C,n); assume A1: j <= len G; A2: len G = 2|^n + (1+2) & len G = width G by Def1; assume cell(G,len G,j) /\ C <> {}; then consider p such that A3: p in cell(G,len G,j) /\ C by SUBSET_1:10; A4: p in cell(G,len G,j) & p in C by A3,XBOOLE_0:def 3; 4 <= len G by Th13; then A5: 1 <= len G by AXIOMS:22; set W = W-bound C, S = S-bound C, E = E-bound C, N = N-bound C; set EW = (E-W)/(2|^n); [len G,1] in Indices G by A2,A5,GOBOARD7:10; then G*(len G,1) = |[W+EW*((len G)-2), S+((N-S)/(2|^n))*(1-2)]| by Def1; then A6: G*(len G,1)`1 = W+EW*((len G)-2) by EUCLID:56; A7: 2|^n > 0 by HEINE:5; E > W by Th11; then E-W > 0 by SQUARE_1:11; then A8: EW > 0 by A7,REAL_2:127; (len G)-2 = 2|^n + 1 + 2 - 2 by A2,XCMPLX_1:1 .= 2|^n + 1 by XCMPLX_1:26; then EW*((len G)-2) = EW*(2|^n) + EW*1 by XCMPLX_1:8 .= E-W+EW by A7,XCMPLX_1:88; then G*(len G,1)`1 = W+(E-W)+EW by A6,XCMPLX_1:1 .= E + EW by XCMPLX_1:27; then A9: G*(len G,1)`1 > E by A8,REAL_1:69; j = 0 or j > 0 by NAT_1:19; then A10: j = 0 or j >= 1+0 by NAT_1:27; per cases by A1,A10,REAL_1:def 5; suppose j = 0; then cell(G,len G,j) = {|[r,s]| : G*(len G,1)`1 <= r & s <= G*(1,1)`2} by GOBRD11:27; then consider r,s such that A11: p = |[r,s]| and A12: G*(len G,1)`1 <= r & s <= G*(1,1)`2 by A4; p`1 = r by A11,EUCLID:56; then E < p`1 & p`1 <= E by A4,A9,A12,AXIOMS:22,PSCOMP_1:71; hence contradiction; suppose j = len G; then cell(G,len G,j)={|[r,s]| : G*(len G,1)`1 <= r & G*(1,width G)`2 <= s} by A2,GOBRD11:28; then consider r,s such that A13: p = |[r,s]| and A14: G*(len G,1)`1 <= r & G*(1,width G)`2 <= s by A4; p`1 = r by A13,EUCLID:56; then E < p`1 & p`1 <= E by A4,A9,A14,AXIOMS:22,PSCOMP_1:71; hence contradiction; suppose 1 <= j & j < len G; then cell(G,len G,j) = { |[r,s]| : G*(len G,1)`1 <= r & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by A2,GOBRD11:29; then consider r,s such that A15: p = |[r,s]| and A16: G*(len G,1)`1 <= r & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A4; p`1 = r by A15,EUCLID:56; then E < p`1 & p`1 <= E by A4,A9,A16,AXIOMS:22,PSCOMP_1:71; hence contradiction; end; theorem i <= len Gauge(C,n) implies cell(Gauge(C,n),i,0) misses C proof set G = Gauge(C,n); assume A1: i <= len G; A2: len G = 2|^n + (1+2) & len G = width G by Def1; assume cell(G,i,0) /\ C <> {}; then consider p such that A3: p in cell(G,i,0) /\ C by SUBSET_1:10; A4: p in cell(G,i,0) & p in C by A3,XBOOLE_0:def 3; 4 <= len G by Th13; then A5: 1 <= len G by AXIOMS:22; set W = W-bound C, S = S-bound C, E = E-bound C, N = N-bound C; set NS = (N-S)/(2|^n); [1,1] in Indices G by A2,A5,GOBOARD7:10; then G*(1,1) = |[W+((E-W)/(2|^n))*(1-2), S+NS*(1-2)]| by Def1; then A6: G*(1,1)`2 = S+NS*(-1) by EUCLID:56; A7: 2|^n > 0 by HEINE:5; N > S by Th12; then N-S > 0 by SQUARE_1:11; then NS > 0 by A7,REAL_2:127; then NS*(-1) < 0 * (-1) by REAL_1:71; then A8: G*(1,1)`2 < S+0 by A6,REAL_1:53; i = 0 or i > 0 by NAT_1:19; then A9: i = 0 or i >= 1+0 by NAT_1:27; per cases by A1,A9,REAL_1:def 5; suppose i = 0; then cell(G,i,0) ={ |[r,s]| : r <= G*(1,1)`1 & s <= G*(1,1)`2 } by GOBRD11:24; then consider r,s such that A10: p = |[r,s]| and A11: r <= G*(1,1)`1 & s <= G*(1,1)`2 by A4; p`2 = s by A10,EUCLID:56; then S > p`2 & p`2 >= S by A4,A8,A11,AXIOMS:22,PSCOMP_1:71; hence contradiction; suppose i = len G; then cell(G,i,0)={ |[r,s]| : G*(len G,1)`1 <= r & s <= G*(1,1)`2 } by GOBRD11:27; then consider r,s such that A12: p = |[r,s]| and A13: G*(len G,1)`1 <= r & s <= G*(1,1)`2 by A4; p`2 = s by A12,EUCLID:56; then S > p`2 & p`2 >= S by A4,A8,A13,AXIOMS:22,PSCOMP_1:71; hence contradiction; suppose 1 <= i & i < len G; then cell(G,i,0) = { |[r,s]|: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & s <= G* (1,1)`2 } by GOBRD11:30; then consider r,s such that A14: p = |[r,s]| and A15: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & s <= G*(1,1)`2 by A4; p`2 = s by A14,EUCLID:56; then S > p`2 & p`2 >= S by A4,A8,A15,AXIOMS:22,PSCOMP_1:71; hence contradiction; end; theorem j <= len Gauge(C,n) implies cell(Gauge(C,n),0,j) misses C proof set G = Gauge(C,n); assume A1: j <= len G; A2: len G = 2|^n + (1+2) & len G = width G by Def1; assume cell(G,0,j) /\ C <> {}; then consider p such that A3: p in cell(G,0,j) /\ C by SUBSET_1:10; A4: p in cell(G,0,j) & p in C by A3,XBOOLE_0:def 3; 4 <= len G by Th13; then A5: 1 <= len G by AXIOMS:22; set W = W-bound C, S = S-bound C, E = E-bound C, N = N-bound C; set EW = (E-W)/(2|^n); [1,1] in Indices G by A2,A5,GOBOARD7:10; then G*(1,1) = |[W+EW*(1-2), S+((N-S)/(2|^n))*(1-2)]| by Def1; then A6: G*(1,1)`1 = W+EW*(-1) by EUCLID:56; A7: 2|^n > 0 by HEINE:5; E > W by Th11; then E-W > 0 by SQUARE_1:11; then EW > 0 by A7,REAL_2:127; then EW*(-1) < 0 * (-1) by REAL_1:71; then A8: G*(1,1)`1 < W+0 by A6,REAL_1:53; j = 0 or j > 0 by NAT_1:19; then A9: j = 0 or j >= 1+0 by NAT_1:27; per cases by A1,A9,REAL_1:def 5; suppose j = 0; then cell(G,0,j) = { |[r,s]| : r <= G*(1,1)`1 & s <= G*(1,1)`2 } by GOBRD11:24; then consider r,s such that A10: p = |[r,s]| and A11: r <= G*(1,1)`1 & s <= G*(1,1)`2 by A4; p`1 = r by A10,EUCLID:56; then W > p`1 & p`1 >= W by A4,A8,A11,AXIOMS:22,PSCOMP_1:71; hence contradiction; suppose j = len G; then cell(G,0,j)={ |[r,s]| : r <= G*(1,1)`1 & G*(1,width G)`2 <= s } by A2,GOBRD11:25; then consider r,s such that A12: p = |[r,s]| and A13: r <= G*(1,1)`1 & G*(1,width G)`2 <= s by A4; p`1 = r by A12,EUCLID:56; then W > p`1 & p`1 >= W by A4,A8,A13,AXIOMS:22,PSCOMP_1:71; hence contradiction; suppose 1 <= j & j < len G; then cell(G,0,j) = { |[r,s]| : r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by A2,GOBRD11:26; then consider r,s such that A14: p = |[r,s]| and A15: r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A4; p`1 = r by A14,EUCLID:56; then W > p`1 & p`1 >= W by A4,A8,A15,AXIOMS:22,PSCOMP_1:71; hence contradiction; end;

Back to top