Copyright (c) 1999 Association of Mizar Users
environ vocabulary FINSEQ_1, REALSET1, SEQM_3, RELAT_1, FINSEQ_4, FUNCT_1, FINSEQ_5, RFINSEQ, BOOLE, ARYTM_1, FINSEQ_6, EUCLID, JORDAN2C, FINSEQ_2, GOBOARD1, MCART_1, PRE_TOPC, TOPREAL1, GOBOARD2, CARD_1, GOBOARD5, TARSKI, MATRIX_1, ABSVALUE, GOBOARD9, CONNSP_1, SUBSET_1, TOPS_1, PSCOMP_1, SPRECT_2, COMPTS_1, JORDAN5D, TREES_1; notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, ABSVALUE, BINARITH, CARD_1, REALSET1, FUNCT_1, FINSEQ_1, FINSEQ_2, MATRIX_1, FINSEQ_4, RFINSEQ, FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1, COMPTS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, PSCOMP_1, JORDAN5D, SPRECT_2, JORDAN2C; constructors TOPS_1, GOBOARD9, SPRECT_2, PSCOMP_1, RFINSEQ, BINARITH, REAL_1, CONNSP_1, GOBOARD2, FINSEQ_4, INT_1, ABSVALUE, JORDAN5D, JORDAN2C, REALSET1, COMPTS_1, FINSEQOP; clusters RELSET_1, SPRECT_1, SPRECT_2, EUCLID, FINSEQ_6, FINSEQ_5, GOBOARD9, GOBOARD2, PSCOMP_1, INT_1, FINSEQ_1, TEX_1, REALSET1, BINARITH, MEMBERED; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TOPREAL1, GOBOARD5, SPRECT_2, TARSKI, FINSEQ_6, REALSET1, GOBOARD1, XBOOLE_0; theorems FINSEQ_6, GROUP_5, NAT_1, FINSEQ_5, FINSEQ_3, FINSEQ_4, AXIOMS, AMI_5, JORDAN3, NAT_2, REAL_1, REAL_2, FINSEQ_1, SPRECT_3, BINARITH, RFINSEQ, RLVECT_1, SQUARE_1, TOPREAL1, JORDAN4, GOBOARD5, SPPOL_2, TARSKI, SPRECT_2, GOBOARD9, INT_1, SUBSET_1, JGRAPH_1, GOBOARD7, GOBOARD1, GOBOARD2, FUNCT_1, PARTFUN2, RELAT_1, FINSEQ_2, JORDAN5D, PSCOMP_1, REALSET1, JORDAN2C, EUCLID, YELLOW_8, TOPREAL3, SCMFSA_7, XBOOLE_0, XBOOLE_1, XCMPLX_1; begin ::Preliminaries reserve i,j,k,m,n for Nat, D for non empty set, p for Element of D, f for FinSequence of D; definition let S be non trivial 1-sorted; cluster the carrier of S -> non trivial; coherence by REALSET1:def 13; end; definition let D be non empty set; let f be FinSequence of D; redefine attr f is constant means :: GOBOARD1:def 2 :Def1: for n,m st n in dom f & m in dom f holds f/.n=f/.m; compatibility proof hereby assume A1: f is constant; let n,m such that A2: n in dom f and A3: m in dom f; thus f/.n= f.n by A2,FINSEQ_4:def 4 .= f.m by A1,A2,A3,GOBOARD1:def 2 .= f/.m by A3,FINSEQ_4:def 4; end; assume A4: for n,m st n in dom f & m in dom f holds f/.n=f/.m; let n,m such that A5: n in dom f and A6: m in dom f; thus f.n = f/.n by A5,FINSEQ_4:def 4 .= f/.m by A4,A5,A6 .= f.m by A6,FINSEQ_4:def 4; end; end; theorem Th1: for D being non empty set, f being FinSequence of D st f just_once_values f/.len f holds f/.len f..f = len f proof let D be non empty set, f be FinSequence of D; assume A1: f just_once_values f/.len f; then reconsider f' = f as non empty FinSequence of D by FINSEQ_4:7,RELAT_1:60; f/.len f..f + 1 = f/.len f..f + ((Rev f')/.1)..Rev f' by FINSEQ_6:47 .= f/.len f..f + f/.len f..Rev f by FINSEQ_5:68 .= len f + 1 by A1,FINSEQ_6:41; hence f/.len f..f = len f by XCMPLX_1:2; end; theorem Th2: for D being non empty set, f being FinSequence of D holds f /^ len f = {} proof let D be non empty set, f be FinSequence of D; len (f /^ len f) = len f - len f by RFINSEQ:def 2 .= 0 by XCMPLX_1:14; hence thesis by FINSEQ_1:25; end; theorem Th3: for D being non empty set, f being non empty FinSequence of D holds f/.len f in rng f proof let D be non empty set, f be non empty FinSequence of D; len f in dom f by FINSEQ_5:6; hence thesis by PARTFUN2:4; end; definition let D be non empty set, f be FinSequence of D, y be set; redefine pred f just_once_values y means ex x being set st x in dom f & y = f/.x & for z being set st z in dom f & z <> x holds f/.z <> y; compatibility proof hereby assume f just_once_values y; then consider x being set such that A1: x in dom f and A2: y = f.x and A3: for z being set st z in dom f & z <> x holds f.z <> y by FINSEQ_4:9; take x; thus x in dom f by A1; thus y = f/.x by A1,A2,FINSEQ_4:def 4; let z be set; assume A4: z in dom f & z <> x; then f.z <> y by A3; hence f/.z <> y by A4,FINSEQ_4:def 4; end; given x being set such that A5: x in dom f and A6: y = f/.x and A7: for z being set st z in dom f & z <> x holds f/.z <> y; A8: y = f.x by A5,A6,FINSEQ_4:def 4; for z being set st z in dom f & z <> x holds f.z <> y proof let z be set; assume A9: z in dom f & z <> x; then f/.z <> y by A7; hence thesis by A9,FINSEQ_4:def 4; end; hence f just_once_values y by A5,A8,FINSEQ_4:9; end; end; theorem Th4: for D being non empty set, f being FinSequence of D st f just_once_values f/.len f holds f-:f/.len f = f proof let D be non empty set, f be FinSequence of D; assume A1: f just_once_values f/.len f; thus f-:f/.len f = f|(f/.len f..f) by FINSEQ_5:def 1 .= f|len f by A1,Th1 .= f by TOPREAL1:2; end; theorem Th5: for D being non empty set, f being FinSequence of D st f just_once_values f/.len f holds f:-f/.len f = <*f/.len f*> proof let D be non empty set, f be FinSequence of D; assume A1: f just_once_values f/.len f; thus f:-f/.len f = <*f/.len f*>^(f/^f/.len f..f) by FINSEQ_5:def 2 .= <*f/.len f*>^(f/^len f) by A1,Th1 .= <*f/.len f*>^{} by Th2 .= <*f/.len f*> by FINSEQ_1:47; end; theorem Th6: 1 <= len (f:-p) proof len(f:-p) = len(<*p*>^(f/^p..f)) by FINSEQ_5:def 2 .= len<*p*> + len(f/^p..f) by FINSEQ_1:35 .= 1 + len(f/^p..f) by FINSEQ_1:56; hence thesis by NAT_1:29; end; theorem for D being non empty set, p being Element of D, f being FinSequence of D st p in rng f holds len(f:-p) <= len f proof let D be non empty set, p be Element of D, f be FinSequence of D; assume A1: p in rng f; then len (f:-p) = len f - p..f + 1 by FINSEQ_5:53; then A2: len (f:-p) - 1 = len f - p..f by XCMPLX_1:26; 1 <= p..f by A1,FINSEQ_4:31; then len f - 1 >= len f - p..f by REAL_2:106; hence len(f:-p) <= len f by A2,REAL_1:54; end; theorem for D being non empty set, f being circular non empty FinSequence of D holds Rev f is circular proof let D be non empty set, f be circular non empty FinSequence of D; thus (Rev f)/.1 = f/.len f by FINSEQ_5:68 .= f/.1 by FINSEQ_6:def 1 .= (Rev f)/.len f by FINSEQ_5:68 .= (Rev f)/.len Rev f by FINSEQ_5:def 3; end; begin :: About Rotation reserve D for non empty set, p for Element of D, f for FinSequence of D; theorem Th9: p in rng f & 1 <= i & i <= len(f:-p) implies (Rotate(f,p))/.i = f/.(i -' 1 + p..f) proof assume that A1: p in rng f and A2: 1 <= i and A3: i <= len(f:-p); A4: i = i -' 1 + 1 by A2,AMI_5:4; A5: i in dom(f:-p) by A2,A3,FINSEQ_3:27; Rotate(f,p) = (f:-p)^((f-:p)/^1) by A1,FINSEQ_6:def 2; hence (Rotate(f,p))/.i = (f:-p)/.i by A5,GROUP_5:95 .= f/.(i -' 1 + p..f) by A1,A4,A5,FINSEQ_5:55; end; theorem Th10: p in rng f & p..f <= i & i <= len f implies f/.i = (Rotate(f,p))/.(i+1 -' p..f) proof assume that A1: p in rng f and A2: p..f <= i and A3: i <= len f; 1 + p..f <= i+1 by A2,AXIOMS:24; then A4: 1 <= i+1 -' p..f by SPRECT_3:8; i <= i+1 by NAT_1:29; then A5: p..f <= i+1 by A2,AXIOMS:22; i+1 <= len f + 1 by A3,AXIOMS:24; then i+1 - p..f <= len f + 1 - p..f by REAL_1:49; then i+1 - p..f <= len f - p..f + 1 by XCMPLX_1:29; then i+1 -' p..f <= len f - p..f + 1 by A5,SCMFSA_7:3; then A6: i+1 -' p..f <= len(f:-p) by A1,FINSEQ_5:53; i+1 -' p..f -' 1 + p..f = i -' p..f+1 -' 1 + p..f by A2,JORDAN4:3 .= i -' p..f + p..f by BINARITH:39 .= i by A2,AMI_5:4; hence thesis by A1,A4,A6,Th9; end; theorem Th11: p in rng f implies (Rotate(f,p))/.len(f:-p) = f/.len f proof A1: 1 <= len (f:-p) by Th6; assume A2: p in rng f; then p..f <= len f by FINSEQ_4:31; then reconsider x = len f - p..f as Nat by INT_1:18; len (f:-p) -' 1 + p..f = x + 1 -' 1 + p..f by A2,FINSEQ_5:53 .= len f - p..f + p..f by BINARITH:39 .= len f by XCMPLX_1:27; hence thesis by A1,A2,Th9; end; theorem Th12: p in rng f & len(f:-p) < i & i <= len f implies (Rotate(f,p))/.i = f/.(i + p..f -' len f) proof assume that A1: p in rng f and A2: len(f:-p) < i and A3: i <= len f; A4: i -' len(f:-p) + len(f:-p) = i by A2,AMI_5:4; A5: p..f <= len f by A1,FINSEQ_4:31; then len f - p..f = len f -' p..f by SCMFSA_7:3; then A6: len(f:-p) = len f -' p..f + 1 by A1,FINSEQ_5:53; then A7: len f -' p..f < i by A2,NAT_1:38; then A8: len f < i + p..f by SPRECT_3:8; then len f + 1 <= i + p..f by NAT_1:38; then A9: 1 <= i + p..f -' len f by SPRECT_3:8; i + p..f <= p..f + len f by A3,AXIOMS:24; then i + p..f -' len f <= p..f by SPRECT_3:6; then A10: i + p..f -' len f in Seg(p..f) by A9,FINSEQ_1:3; f-:p is non empty by A1,FINSEQ_5:50; then len(f-:p) <> 0 by FINSEQ_1:25; then len(f-:p) >= 1 by RLVECT_1:99; then A11: len((f-:p)/^1) = len(f-:p)-1 by RFINSEQ:def 2; A12: len f - p..f = len f -' p..f by A5,SCMFSA_7:3; len f -' p..f + 1 + 1 <= i by A2,A6,NAT_1:38; then A13: 1 <= i -' (len f -' p..f + 1) by SPRECT_3:8; then A14: 1 <= i -' len(f:-p) by A1,A12,FINSEQ_5:53; A15: len(f-:p) = p..f by A1,FINSEQ_5:45; i <= p..f + (len f -' p..f) by A3,A5,AMI_5:4; then i -' (len f -' p..f) <= p..f by SPRECT_3:6; then i -' (len f -' p..f + 1) + 1 <= p..f by A7,NAT_2:9; then A16: i -' len(f:-p) <= len(f-:p)-1 by A6,A15,REAL_1:84; then A17: i -' len(f:-p) in dom((f-:p)/^1) by A11,A14,FINSEQ_3:27; A18: i -' (len f -' p..f + 1) in dom((f-:p)/^1) by A6,A11,A13,A16,FINSEQ_3:27; Rotate(f,p) = (f:-p)^((f-:p)/^1) by A1,FINSEQ_6:def 2; hence (Rotate(f,p))/.i = ((f-:p)/^1)/.(i -' (len f -' p..f + 1)) by A4,A6,A17,GROUP_5:96 .= (f-:p)/.(i -' (len f -' p..f + 1) + 1) by A18,FINSEQ_5:30 .= (f-:p)/.(i -' (len f -' p..f)) by A7,NAT_2:9 .= (f-:p)/.(i - (len f -' p..f)) by A7,SCMFSA_7:3 .= (f-:p)/.(i - (len f - p..f)) by A5,SCMFSA_7:3 .= (f-:p)/.(i - len f + p..f) by XCMPLX_1:37 .= (f-:p)/.(i + p..f - len f) by XCMPLX_1:29 .= (f-:p)/.(i + p..f -' len f) by A8,SCMFSA_7:3 .= f/.(i + p..f -' len f) by A1,A10,FINSEQ_5:46; end; theorem p in rng f & 1 < i & i <= p..f implies f/.i = (Rotate(f,p))/.(i + len f -' p..f) proof assume that A1: p in rng f and A2: 1 < i and A3: i <= p..f; A4: p..f <= len f by A1,FINSEQ_4:31; len f + 1 < i + len f by A2,REAL_1:53; then len f + 1 - p..f < i + len f - p..f by REAL_1:54; then len f - p..f + 1 < i + len f - p..f by XCMPLX_1:29; then len f - p..f + 1 < i + (len f - p..f) by XCMPLX_1:29; then len f - p..f + 1 < i + (len f -' p..f) by A4,SCMFSA_7:3; then len f - p..f + 1 < i + len f -' p..f by A4,JORDAN4:3; then A5: len(f:-p) < i + len f -' p..f by A1,FINSEQ_5:53; A6: i <= len f by A3,A4,AXIOMS:22; len f -' p..f <= len f -' i by A3,JORDAN3:4; then len f -' p..f + i <= len f by A6,SPRECT_3:7; then A7: i + len f -' p..f <= len f by A4,JORDAN4:3; len f <= i + len f by NAT_1:29; then p..f <= i + len f by A4,AXIOMS:22; then i + len f -' p..f + p..f -' len f = i + len f -' len f by AMI_5:4 .= i by BINARITH:39; hence thesis by A1,A5,A7,Th12; end; theorem Th14: len Rotate(f,p) = len f proof per cases; suppose not p in rng f; hence thesis by FINSEQ_6:def 2; suppose A1: p in rng f; then f-:p <> {} by FINSEQ_5:50; then len(f-:p) <> 0 by FINSEQ_1:25; then A2: 1 <= len(f-:p) by RLVECT_1:99; thus len Rotate(f,p) = len((f:-p)^((f-:p)/^1)) by A1,FINSEQ_6:def 2 .= len(f:-p) + len((f-:p)/^1) by FINSEQ_1:35 .= len(f:-p) + (len(f-:p)-1) by A2,RFINSEQ:def 2 .= len(f:-p) + len(f-:p)-1 by XCMPLX_1:29 .= len f - p..f + 1 + len(f-:p)-1 by A1,FINSEQ_5:53 .= len f - p..f + len(f-:p) + 1-1 by XCMPLX_1:1 .= len f - p..f + len(f-:p) by XCMPLX_1:26 .= len f - p..f + p..f by A1,FINSEQ_5:45 .= len f by XCMPLX_1:27; end; theorem Th15: dom Rotate(f,p) = dom f proof len Rotate(f,p) = len f by Th14; hence thesis by FINSEQ_3:31; end; theorem Th16: for D being non empty set, f being circular FinSequence of D, p be Element of D st for i st 1 < i & i < len f holds f/.i <> f/.1 holds Rotate(Rotate(f,p),f/.1) = f proof let D be non empty set, f be circular FinSequence of D, p be Element of D such that A1: for i st 1 < i & i < len f holds f/.i <> f/.1; per cases; suppose not p in rng f; hence Rotate(Rotate(f,p),f/.1) = Rotate(f,f/.1) by FINSEQ_6:def 2 .= f by FINSEQ_6:95; suppose p = f/.1; hence Rotate(Rotate(f,p),f/.1) = Rotate(f,f/.1) by FINSEQ_6:99 .= f by FINSEQ_6:95; suppose that A2: p in rng f and A3: p <> f/.1; A4: Rotate(f,p) = (f:-p)^((f-:p)/^1) by A2,FINSEQ_6:def 2; A5: f/.1 = f/.len f by FINSEQ_6:def 1; A6: f-:p <> {} by A2,FINSEQ_5:50; A7: f/.1 = (f:-p)/.len(f:-p) by A2,A5,FINSEQ_5:57; then A8: f/.1 in rng(f:-p) by Th3; A9: f:-p just_once_values f/.1 proof take len(f:-p); thus len(f:-p) in dom(f:-p) by FINSEQ_5:6; thus f/.1 = (f:-p)/.len(f:-p) by A2,A5,FINSEQ_5:57; let z be set; assume A10: z in dom(f:-p); then reconsider k = z as Nat; k <> 0 by A10,FINSEQ_3:27; then consider i such that A11: k = i+1 by NAT_1:22; A12: (f:-p)/.(i+1) = f/.(i+p..f) by A2,A10,A11,FINSEQ_5:55; A13: p..f <> 1 by A2,A3,FINSEQ_5:41; p..f >= 1 by A2,FINSEQ_4:31; then A14: p..f > 1 by A13,AXIOMS:21; p..f <= i+p..f by NAT_1:29; then A15: 1 < i+p..f by A14,AXIOMS:22; assume A16: z <> len(f:-p); k <= len(f:-p) by A10,FINSEQ_3:27; then k < len(f:-p) by A16,AXIOMS:21; then i + 1 < len f - p..f + 1 by A2,A11,FINSEQ_5:53; then i < len f - p..f by AXIOMS:24; then i + p..f < len f by REAL_1:86; hence (f:-p)/.z <> f/.1 by A1,A11,A12,A15; end; A17: f/.1 = (f-:p)/.1 by A2,FINSEQ_5:47; f/.1 in rng f by A2,FINSEQ_6:46,RELAT_1:60; then f/.1 in rng Rotate(f,p) by A2,FINSEQ_6:96; hence Rotate(Rotate(f,p),f/.1) = ((f:-p)^((f-:p)/^1)):-(f/.1)^ (((f:-p)^((f-:p)/^1)-:(f/.1))/^1) by A4,FINSEQ_6:def 2 .= (f:-p):-(f/.1)^((f-:p)/^1)^ (((f:-p)^((f-:p)/^1)-:(f/.1))/^1) by A8,FINSEQ_6:69 .= (f:-p):-(f/.1)^((f-:p)/^1)^ (((f:-p)-:(f/.1))/^1) by A8,FINSEQ_6:71 .= <* f/.1 *>^((f-:p)/^1)^ (((f:-p)-:(f/.1))/^1) by A7,A9,Th5 .= (f-:p)^(((f:-p)-:(f/.1))/^1) by A6,A17,FINSEQ_5:32 .= (f-:p)^((f:-p)/^1) by A7,A9,Th4 .= f by A2,FINSEQ_6:81; end; begin :: Rotating circular reserve f for circular FinSequence of D; theorem Th17: p in rng f & len(f:-p) <= i & i <= len f implies (Rotate(f,p))/.i = f/.(i + p..f -' len f) proof assume that A1: p in rng f and A2: len(f:-p) <= i and A3: i <= len f; A4: p..f <= len f by A1,FINSEQ_4:31; then A5: len f - p..f = len f -' p..f by SCMFSA_7:3; per cases by A2,AXIOMS:21; suppose A6: i = len(f:-p); then A7: i = len f - p..f + 1 by A1,FINSEQ_5:53; then i >= 1 by A5,NAT_1:29; hence (Rotate(f,p))/.i = f/.(i -' 1 + p..f) by A1,A6,Th9 .= f/.(len f -' p..f + p..f) by A5,A7,BINARITH:39 .= f/.len f by A4,AMI_5:4 .= f/.1 by FINSEQ_6:def 1 .= f/.(len f + 1 -' len f) by BINARITH:39 .= f/.(len f -' p..f + p..f + 1 -' len f) by A4,AMI_5:4 .= f/.(i + p..f -' len f) by A5,A7,XCMPLX_1:1; suppose i > len(f:-p); hence thesis by A1,A3,Th12; end; theorem Th18: p in rng f & 1 <= i & i <= p..f implies f/.i = (Rotate(f,p))/.(i + len f -' p..f) proof assume that A1: p in rng f and A2: 1 <= i and A3: i <= p..f; A4: p..f <= len f by A1,FINSEQ_4:31; len f + 1 <= i + len f by A2,AXIOMS:24; then len f + 1 - p..f <= i + len f - p..f by REAL_1:49; then len f - p..f + 1 <= i + len f - p..f by XCMPLX_1:29; then len f - p..f + 1 <= i + (len f - p..f) by XCMPLX_1:29; then len f - p..f + 1 <= i + (len f -' p..f) by A4,SCMFSA_7:3; then len f - p..f + 1 <= i + len f -' p..f by A4,JORDAN4:3; then A5: len(f:-p) <= i + len f -' p..f by A1,FINSEQ_5:53; A6: i <= len f by A3,A4,AXIOMS:22; len f -' p..f <= len f -' i by A3,JORDAN3:4; then len f -' p..f + i <= len f by A6,SPRECT_3:7; then A7: i + len f -' p..f <= len f by A4,JORDAN4:3; len f <= i + len f by NAT_1:29; then p..f <= i + len f by A4,AXIOMS:22; then i + len f -' p..f + p..f -' len f = i + len f -' len f by AMI_5:4 .= i by BINARITH:39; hence thesis by A1,A5,A7,Th17; end; definition let D be non trivial set; cluster non constant circular FinSequence of D; existence proof consider d1,d2 being Element of D such that A1: d1 <> d2 by YELLOW_8:def 1; take f = <*d1,d2,d1*>; A2: 1 in dom f & 2 in dom f by TOPREAL3:6; f.1 = d1 & f.2 = d2 by FINSEQ_1:62; hence f is not constant by A1,A2,GOBOARD1:def 2; A3: len f = 3 by FINSEQ_1:62; thus f/.1 = d1 by FINSEQ_4:27 .= f/.len f by A3,FINSEQ_4:27; end; end; definition let D be non trivial set, p be Element of D; let f be non constant circular FinSequence of D; cluster Rotate(f,p) -> non constant; coherence proof per cases; suppose not p in rng f; hence thesis by FINSEQ_6:def 2; suppose A1: p in rng f; consider n,m such that A2: n in dom f and A3: m in dom f and A4: f/.n <> f/.m by Def1; A5: dom Rotate(f,p) = dom f by Th15; A6: 1 <= n & n <= len f by A2,FINSEQ_3:27; A7: 1 <= m & m <= len f by A3,FINSEQ_3:27; thus Rotate(f,p) is not constant proof A8: p..f <= len f by A1,FINSEQ_4:31; A9: 1 <= p..f by A1,FINSEQ_4:31; per cases; suppose that A10: n <= p..f and A11: m <= p..f; A12: f/.n = (Rotate(f,p))/.(n + len f -' p..f) by A1,A6,A10,Th18; A13: f/.m = (Rotate(f,p))/.(m + len f -' p..f) by A1,A7,A11,Th18; n <= n + (len f -' p..f) by NAT_1:29; then 1 <= n + (len f -' p..f) by A6,AXIOMS:22; then A14: 1 <= n + len f -' p..f by A8,JORDAN4:3; n + len f <= len f + p..f by A10,AXIOMS:24; then n + len f -' p..f <= len f by SPRECT_3:6; then A15: n + len f -' p..f in dom f by A14,FINSEQ_3:27; m <= m + (len f -' p..f) by NAT_1:29; then 1 <= m + (len f -' p..f) by A7,AXIOMS:22; then A16: 1 <= m + len f -' p..f by A8,JORDAN4:3; m + len f <= len f + p..f by A11,AXIOMS:24; then m + len f -' p..f <= len f by SPRECT_3:6; then m + len f -' p..f in dom f by A16,FINSEQ_3:27; hence thesis by A4,A5,A12,A13,A15,Def1; suppose that A17: n <= p..f and A18: m >= p..f; A19: f/.n = (Rotate(f,p))/.(n + len f -' p..f) by A1,A6,A17,Th18; A20: f/.m = (Rotate(f,p))/.(m + 1 -' p..f) by A1,A7,A18,Th10; n <= n + (len f -' p..f) by NAT_1:29; then 1 <= n + (len f -' p..f) by A6,AXIOMS:22; then A21: 1 <= n + len f -' p..f by A8,JORDAN4:3; n + len f <= len f + p..f by A17,AXIOMS:24; then n + len f -' p..f <= len f by SPRECT_3:6; then A22: n + len f -' p..f in dom f by A21,FINSEQ_3:27; 1 + p..f <= m + 1 by A18,AXIOMS:24; then A23: 1 <= m + 1 -' p..f by SPRECT_3:8; m + 1 <= len f + p..f by A7,A9,REAL_1:55; then m + 1 -' p..f <= len f by SPRECT_3:6; then m + 1 -' p..f in dom f by A23,FINSEQ_3:27; hence thesis by A4,A5,A19,A20,A22,Def1; suppose that A24: m <= p..f and A25: n >= p..f; A26: f/.m = (Rotate(f,p))/.(m + len f -' p..f) by A1,A7,A24,Th18; A27: f/.n = (Rotate(f,p))/.(n + 1 -' p..f) by A1,A6,A25,Th10; m <= m + (len f -' p..f) by NAT_1:29; then 1 <= m + (len f -' p..f) by A7,AXIOMS:22; then A28: 1 <= m + len f -' p..f by A8,JORDAN4:3; m + len f <= len f + p..f by A24,AXIOMS:24; then m + len f -' p..f <= len f by SPRECT_3:6; then A29: m + len f -' p..f in dom f by A28,FINSEQ_3:27; 1 + p..f <= n + 1 by A25,AXIOMS:24; then A30: 1 <= n + 1 -' p..f by SPRECT_3:8; n + 1 <= len f + p..f by A6,A9,REAL_1:55; then n + 1 -' p..f <= len f by SPRECT_3:6; then n + 1 -' p..f in dom f by A30,FINSEQ_3:27; hence thesis by A4,A5,A26,A27,A29,Def1; suppose that A31: m >= p..f and A32: n >= p..f; A33: f/.m = (Rotate(f,p))/.(m + 1 -' p..f) by A1,A7,A31,Th10; A34: f/.n = (Rotate(f,p))/.(n + 1 -' p..f) by A1,A6,A32,Th10; 1 + p..f <= m + 1 by A31,AXIOMS:24; then A35: 1 <= m + 1 -' p..f by SPRECT_3:8; m + 1 <= len f + p..f by A7,A9,REAL_1:55; then m + 1 -' p..f <= len f by SPRECT_3:6; then A36: m + 1 -' p..f in dom f by A35,FINSEQ_3:27; 1 + p..f <= n + 1 by A32,AXIOMS:24; then A37: 1 <= n + 1 -' p..f by SPRECT_3:8; n + 1 <= len f + p..f by A6,A9,REAL_1:55; then n + 1 -' p..f <= len f by SPRECT_3:6; then n + 1 -' p..f in dom f by A37,FINSEQ_3:27; hence thesis by A4,A5,A33,A34,A36,Def1; end; end; end; begin :: Finite sequences on the plane theorem Th19: for n being non empty Nat holds 0.REAL n <> 1.REAL n proof let n be non empty Nat; A1: 0.REAL n = 0*n by EUCLID:def 9 .= n |-> 0 by EUCLID:def 4; A2: 1.REAL n = 1*n by JORDAN2C:def 8 .= n |-> 1 by JORDAN2C:def 7; 1 <= n by RLVECT_1:99; then 1 in Seg n by FINSEQ_1:3; then (n |-> 0).1 = 0 & (n |-> 1).1 = 1 by FINSEQ_2:71; hence 0.REAL n <> 1.REAL n by A1,A2; end; definition let n be non empty Nat; cluster TOP-REAL n -> non trivial; coherence proof take 0.REAL n, 1.REAL n; thus 0.REAL n <> 1.REAL n by Th19; end; end; reserve f,g for FinSequence of TOP-REAL 2; theorem Th20: rng f c= rng g implies rng X_axis f c= rng X_axis g proof assume A1: rng f c= rng g; let x be set; assume x in rng X_axis f; then consider y being set such that A2: y in dom X_axis f and A3: (X_axis f).y = x by FUNCT_1:def 5; A4: dom X_axis f = dom f by SPRECT_2:19; A5: dom X_axis g = dom g by SPRECT_2:19; reconsider y as Nat by A2; A6: (X_axis f).y = (f/.y)`1 by A2,GOBOARD1:def 3; f/.y in rng f by A2,A4,PARTFUN2:4; then consider z being set such that A7: z in dom g and A8: g.z = f/.y by A1,FUNCT_1:def 5; reconsider z as Nat by A7; g/.z = f/.y by A7,A8,FINSEQ_4:def 4; then (X_axis g).z = (f/.y)`1 by A5,A7,GOBOARD1:def 3; hence x in rng X_axis g by A3,A5,A6,A7,FUNCT_1:def 5; end; theorem Th21: rng f = rng g implies rng X_axis f = rng X_axis g proof assume rng f = rng g; hence rng X_axis f c= rng X_axis g & rng X_axis g c= rng X_axis f by Th20; end; theorem Th22: rng f c= rng g implies rng Y_axis f c= rng Y_axis g proof assume A1: rng f c= rng g; let x be set; assume x in rng Y_axis f; then consider y being set such that A2: y in dom Y_axis f and A3: (Y_axis f).y = x by FUNCT_1:def 5; A4: dom Y_axis f = dom f by SPRECT_2:20; A5: dom Y_axis g = dom g by SPRECT_2:20; reconsider y as Nat by A2; A6: (Y_axis f).y = (f/.y)`2 by A2,GOBOARD1:def 4; f/.y in rng f by A2,A4,PARTFUN2:4; then consider z being set such that A7: z in dom g and A8: g.z = f/.y by A1,FUNCT_1:def 5; reconsider z as Nat by A7; g/.z = f/.y by A7,A8,FINSEQ_4:def 4; then (Y_axis g).z = (f/.y)`2 by A5,A7,GOBOARD1:def 4; hence x in rng Y_axis g by A3,A5,A6,A7,FUNCT_1:def 5; end; theorem Th23: rng f = rng g implies rng Y_axis f = rng Y_axis g proof assume rng f = rng g; hence rng Y_axis f c= rng Y_axis g & rng Y_axis g c= rng Y_axis f by Th22; end; begin :: Rotating finite sequences on the plane reserve p for Point of TOP-REAL 2, f for FinSequence of TOP-REAL 2; definition let p be Point of TOP-REAL 2; let f be special circular FinSequence of TOP-REAL 2; cluster Rotate(f,p) -> special; coherence proof per cases; suppose not p in rng f; hence thesis by FINSEQ_6:def 2; suppose A1: p in rng f; let i such that A2: 1 <= i and A3: i+1 <= len Rotate(f,p); A4: i+1 >= 1 by NAT_1:29; A5: i+1 >= i by NAT_1:29; A6: len Rotate(f,p) = len f by Th14; now A7: len (f:-p) = len f - p..f + 1 by A1,FINSEQ_5:53; per cases; suppose A8: i < len(f:-p); then A9: (Rotate(f,p))/.i = f/.(i -' 1 + p..f) by A1,A2,Th9; A10: i+1 <= len(f:-p) by A8,NAT_1:38; i + 1 -' 1 + p..f = i + p..f by BINARITH:39 .= i -' 1 + 1 + p..f by A2,AMI_5:4 .= i -' 1 + p..f + 1 by XCMPLX_1:1; then A11: (Rotate(f,p))/.(i+1) = f/.(i -' 1 + p..f + 1) by A1,A4,A10,Th9; A12: 0 <= i -' 1 by NAT_1:19; 1 <= p..f by A1,FINSEQ_4:31; then A13: 1 + 0 <= i -' 1 + p..f by A12,REAL_1:55; i < len f + 1 - p..f by A7,A8,XCMPLX_1:29; then i + p..f < len f + 1 by REAL_1:86; then i + p..f <= len f by NAT_1:38; then i -' 1 + 1 + p..f <= len f by A2,AMI_5:4; then i -' 1 + p..f + 1 <= len f by XCMPLX_1:1; hence thesis by A9,A11,A13,TOPREAL1:def 7; suppose A14: i >= len(f:-p); i <= len f by A3,A5,A6,AXIOMS:22; then A15: (Rotate(f,p))/.i = f/.(i + p..f -' len f) by A1,A14,Th17; A16: i+1 >= len(f:-p) by A5,A14,AXIOMS:22; then i >= len f - p..f by A7,REAL_1:53; then A17: len f <= i + p..f by REAL_1:86; i+1 + p..f -' len f = i + p..f+1 -' len f by XCMPLX_1:1 .= i + p..f -' len f + 1 by A17,JORDAN4:3; then A18: (Rotate(f,p))/.(i+1) = f/.(i + p..f -' len f + 1) by A1,A3,A6,A16, Th17; i - (len f - p..f) >= 1 by A7,A14,REAL_1:84; then i - len f + p..f >= 1 by XCMPLX_1:37; then i + p..f - len f >= 1 by XCMPLX_1:29; then A19: 1 <= i + p..f -' len f by JORDAN3:1; p..f <= len f by A1,FINSEQ_4:31; then i + 1 + p..f <= len f + len f by A3,A6,REAL_1:55; then i + p..f + 1 <= len f + len f by XCMPLX_1:1; then i + p..f + 1 - len f <= len f by REAL_1:86; then i + p..f - len f + 1 <= len f by XCMPLX_1:29; then i + p..f -' len f + 1 <= len f by A17,SCMFSA_7:3; hence thesis by A15,A18,A19,TOPREAL1:def 7; end; hence thesis; end; end; theorem Th24: p in rng f & 1 <= i & i < len(f:-p) implies LSeg(Rotate(f,p),i) = LSeg(f,i -' 1 + p..f) proof assume that A1: p in rng f and A2: 1 <= i and A3: i < len(f:-p); A4: len Rotate(f,p) = len f by Th14; A5: (Rotate(f,p))/.i = f/.(i -' 1 + p..f) by A1,A2,A3,Th9; A6: len(f:-p) = len f - p..f + 1 by A1,FINSEQ_5:53; A7: i -' 1 >= 0 by NAT_1:18; A8: 1 <= p..f by A1,FINSEQ_4:31; then A9: 0+1 <= i -' 1 + p..f by A7,REAL_1:55; i - 1 < len f - p..f by A3,A6,REAL_1:84; then i -' 1 < len f - p..f by A2,SCMFSA_7:3; then i -' 1 + p..f < len f by REAL_1:86; then A10: i -' 1 + p..f + 1 <= len f by NAT_1:38; A11: 1 <= i+1 by NAT_1:29; A12: i+1 <= len(f:-p) by A3,NAT_1:38; i -' 1 + p..f + 1 = i -' 1 + 1 + p..f by XCMPLX_1:1 .= i + p..f by A2,AMI_5:4 .= i + 1 -' 1 + p..f by BINARITH:39; then A13: (Rotate(f,p))/.(i+1) = f/.(i -' 1 + p..f + 1)by A1,A11,A12,Th9; p..f - 1 >= 0 by A8,SQUARE_1:12; then len f - (p..f - 1) <= len f by REAL_2:173; then len f - p..f + 1 <= len f by XCMPLX_1:37; then i+1 <= len f by A6,A12,AXIOMS:22; hence LSeg(Rotate(f,p),i) = LSeg(f/.(i -' 1 + p..f),f/.(i -' 1 + p..f + 1)) by A2,A4,A5,A13,TOPREAL1:def 5 .= LSeg(f,i -' 1 + p..f) by A9,A10,TOPREAL1:def 5; end; theorem Th25: p in rng f & p..f <= i & i < len f implies LSeg(f,i) = LSeg(Rotate(f,p),i -' p..f+1) proof assume that A1: p in rng f and A2: p..f <= i and A3: i < len f; 1 + p..f <= i + 1 by A2,AXIOMS:24; then 1 <= i + 1 -' p..f by SPRECT_3:8; then A4: 1 <= i -' p..f+1 by A2,JORDAN4:3; i - p..f < len f - p..f by A3,REAL_1:54; then i -' p..f < len f - p..f by A2,SCMFSA_7:3; then i -' p..f+1 < len f - p..f + 1 by REAL_1:53; then A5: i -' p..f+1 < len(f:-p) by A1,FINSEQ_5:53; i -' p..f+1 -' 1 + p..f =i -' p..f + p..f by BINARITH:39 .= i by A2,AMI_5:4; hence LSeg(f,i) = LSeg(Rotate(f,p),i -' p..f+1) by A1,A4,A5,Th24; end; theorem Th26: for f being circular FinSequence of TOP-REAL 2 holds Incr X_axis f = Incr X_axis Rotate(f,p) proof let f be circular FinSequence of TOP-REAL 2; per cases; suppose not p in rng f; hence thesis by FINSEQ_6:def 2; suppose p in rng f; then rng Rotate(f,p) = rng f by FINSEQ_6:96; then rng X_axis Rotate(f,p) = rng X_axis f by Th21; then rng Incr X_axis Rotate(f,p) = rng X_axis f & len Incr X_axis Rotate(f,p) = card rng X_axis f by GOBOARD2:def 2; hence thesis by GOBOARD2:def 2; end; theorem Th27: for f being circular FinSequence of TOP-REAL 2 holds Incr Y_axis f = Incr Y_axis Rotate(f,p) proof let f be circular FinSequence of TOP-REAL 2; per cases; suppose not p in rng f; hence thesis by FINSEQ_6:def 2; suppose p in rng f; then rng Rotate(f,p) = rng f by FINSEQ_6:96; then rng Y_axis Rotate(f,p) = rng Y_axis f by Th23; then rng Incr Y_axis Rotate(f,p) = rng Y_axis f & len Incr Y_axis Rotate(f,p) = card rng Y_axis f by GOBOARD2:def 2; hence thesis by GOBOARD2:def 2; end; theorem Th28: for f being non empty circular FinSequence of TOP-REAL 2 holds GoB Rotate(f,p) = GoB f proof let f be non empty circular FinSequence of TOP-REAL 2; Incr X_axis f = Incr X_axis Rotate(f,p) & Incr Y_axis f = Incr Y_axis Rotate(f,p) by Th26,Th27; hence GoB Rotate(f,p) = GoB(Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 3 .= GoB f by GOBOARD2:def 3; end; theorem Th29: for f being non constant standard special_circular_sequence holds Rev Rotate(f,p) = Rotate(Rev f,p) proof let f be non constant standard special_circular_sequence; per cases; suppose A1: not p in rng f; then A2: Rotate(f,p) = f by FINSEQ_6:def 2; not p in rng Rev f by A1,FINSEQ_5:60; hence thesis by A2,FINSEQ_6:def 2; suppose A3: p = f/.1; then A4: Rotate(f,p) = f by FINSEQ_6:95; p = (Rev f)/.len f by A3,FINSEQ_5:68 .= (Rev f)/.len Rev f by FINSEQ_5:def 3 .= (Rev f)/.1 by FINSEQ_6:def 1; hence thesis by A4,FINSEQ_6:95; suppose that A5: p in rng f and A6: p <> f/.1; f just_once_values p proof take p..f; thus A7: p..f in dom f by A5,FINSEQ_4:30; thus A8: p = f.(p..f) by A5,FINSEQ_4:29 .= f/.(p..f) by A7,FINSEQ_4:def 4; let z be set such that A9: z in dom f and A10: z <> p..f; reconsider k = z as Nat by A9; per cases by A10,AXIOMS:21; suppose A11: k < p..f; A12: p..f <= len f by A5,FINSEQ_4:31; p..f <> len f by A6,A8,FINSEQ_6:def 1; then A13: p..f < len f by A12,AXIOMS:21; 1 <= k by A9,FINSEQ_3:27; hence f/.z <> p by A8,A11,A13,GOBOARD7:38; suppose A14: k > p..f; p..f >= 1 by A5,FINSEQ_4:31; then A15: p..f > 1 by A6,A8,AXIOMS:21; k <= len f by A9,FINSEQ_3:27; hence f/.z <> p by A8,A14,A15,GOBOARD7:39; end; hence Rev Rotate(f,p) = Rotate(Rev f,p) by FINSEQ_6:112; end; begin :: Circular finite sequences of points of the plane reserve f for circular FinSequence of TOP-REAL 2; theorem Th30: for f being circular s.c.c. FinSequence of TOP-REAL 2 st len f > 4 holds LSeg(f,len f -' 1) /\ LSeg(f,1) = {f/.1} proof let f be circular s.c.c. FinSequence of TOP-REAL 2; assume A1: len f > 4; then A2: len f >= 1+1+1 by AXIOMS:22; A3: len f >= 1+1 by A1,AXIOMS:22; A4: len f >= 1 by A1,AXIOMS:22; then A5: len f -' 1 + 1 = len f by AMI_5:4; A6: 1 <= len f -' 1 by A3,SPRECT_3:8; thus LSeg(f,len f -' 1) /\ LSeg(f,1) c= {f/.1} proof assume not LSeg(f,len f -' 1) /\ LSeg(f,1) c= {f/.1}; then consider p being Point of TOP-REAL 2 such that A7: p in LSeg(f,len f -' 1) /\ LSeg(f,1) and A8: not p in {f/.1} by SUBSET_1:7; A9: LSeg(f,len f -' 1) = LSeg(f/.(len f -' 1),f/.len f) by A5,A6,TOPREAL1:def 5; A10: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A3,TOPREAL1:def 5; A11: p <> f/.1 by A8,TARSKI:def 1; A12: f/.len f = f/.1 by FINSEQ_6:def 1; per cases by A7,A9,A10,A11,A12,JGRAPH_1:20; suppose A13: f/.(1+1) in LSeg(f,len f -' 1); A14: f/.(1+1) in LSeg(f,1+1) by A2,TOPREAL1:27; 1+1 = 2 & 2+1 = 3 & 3+1 = 4; then 1+1+1 < len f - 1 by A1,REAL_1:86; then A15: 1+1+1 < len f -' 1 by A4,SCMFSA_7:3; len f -' 1 < len f by A6,JORDAN3:14; then LSeg(f,1+1) misses LSeg(f,len f -' 1) by A15,GOBOARD5:def 4; hence contradiction by A13,A14,XBOOLE_0:3; suppose A16: f/.(len f -' 1) in LSeg(f,1); A17: len f -' 2+1 = len f -' 1 -' 1+1 by JORDAN3:8 .= len f -' 1 by A6,AMI_5:4; then A18: len f -' 2+1 < len f by A6,JORDAN3:14; 1 <= len f - 2 by A2,REAL_1:84; then 1 <= len f -' 2 by JORDAN3:1; then A19: f/.(len f -' 1) in LSeg(f,len f -' 2) by A17,A18,TOPREAL1:27; 2 + 2 < len f by A1; then 1+1 < len f - 2 by REAL_1:86; then 1+1 < len f -' 2 by A3,SCMFSA_7:3; then LSeg(f,1) misses LSeg(f,len f -' 2) by A18,GOBOARD5:def 4; hence contradiction by A16,A19,XBOOLE_0:3; end; let x be set; assume x in {f/.1}; then A20: x = f/.1 by TARSKI:def 1; then x = f/.len f by FINSEQ_6:def 1; then A21: x in LSeg(f,len f -' 1) by A5,A6,TOPREAL1:27; x in LSeg(f,1) by A3,A20,TOPREAL1:27; hence x in LSeg(f,len f -' 1) /\ LSeg(f,1) by A21,XBOOLE_0:def 3; end; theorem Th31: p in rng f & len(f:-p) <= i & i < len f implies LSeg(Rotate(f,p),i) = LSeg(f,i + p..f -' len f) proof assume that A1: p in rng f and A2: len(f:-p) <= i and A3: i < len f; A4: i+1 <= len f by A3,NAT_1:38; A5: len Rotate(f,p) = len f by Th14; A6: len(f:-p) = len f - p..f + 1 by A1,FINSEQ_5:53; A7: (Rotate(f,p))/.i = f/.(i + p..f -' len f) by A1,A2,A3,Th17; A8: len(f:-p) <= i + 1 by A2,NAT_1:37; A9: i + 1 <= len f by A3,NAT_1:38; A10: p..f <= len f by A1,FINSEQ_4:31; then len f -' p..f + 1 <= i by A2,A6,SCMFSA_7:3; then len f + 1 -' p..f <= i by A10,JORDAN4:3; then A11: len f + 1 <= i + p..f by SPRECT_3:5; then A12: 1 <= i + p..f -' len f by SPRECT_3:8; len f <= len f + 1 by NAT_1:29; then A13: len f <= i + p..f by A11,AXIOMS:22; i + 1 + p..f <= len f + len f by A9,A10,REAL_1:55; then i + p..f + 1 <= len f + len f by XCMPLX_1:1; then i + p..f + 1 -' len f <= len f by SPRECT_3:6; then A14: i + p..f -' len f + 1 <= len f by A13,JORDAN4:3; i + 1 + p..f -' len f = i + p..f + 1 -' len f by XCMPLX_1:1 .= i + p..f -' len f+1 by A13,JORDAN4:3; then A15: (Rotate(f,p))/.(i+1) = f/.(i + p..f -' len f+1) by A1,A8,A9,Th17; len f - p..f >= 0 by A10,SQUARE_1:12; then len f - p..f + 1 >= 0 + 1 by AXIOMS:24; then 0 + 1 <= 0 + i by A2,A6,AXIOMS:22; hence LSeg(Rotate(f,p),i) = LSeg(f/.(i + p..f -' len f),f/.(i + p..f -' len f + 1)) by A4,A5,A7,A15, TOPREAL1:def 5 .= LSeg(f,i + p..f -' len f) by A12,A14,TOPREAL1:def 5; end; definition let p be Point of TOP-REAL 2; let f be circular s.c.c. FinSequence of TOP-REAL 2; cluster Rotate(f,p) -> s.c.c.; coherence proof set h = Rotate(f,p); per cases; suppose not p in rng f; hence thesis by FINSEQ_6:def 2; suppose p in rng f & p..f = 1; then p = f/.1 by FINSEQ_5:41; hence thesis by FINSEQ_6:95; suppose p in rng f & p..f = len f; then p = f/.len f by FINSEQ_5:41; then p = f/.1 by FINSEQ_6:def 1; hence thesis by FINSEQ_6:95; suppose that A1: p in rng f and A2: p..f <> 1 and A3: p..f <> len f; A4: len(f:-p) = len f - p..f + 1 by A1,FINSEQ_5:53; A5: 1 <= p..f & p..f <= len f by A1,FINSEQ_4:31; then A6: len f - p..f = len f -' p..f by SCMFSA_7:3; A7: len f = len h by Th14; A8: p..f > 1 by A2,A5,AXIOMS:21; let i,j such that A9: i+1 < j and A10: i > 1 & j < len h or j+1 < len h; j <= j+1 by NAT_1:29; then A11: j < len f by A7,A10,AXIOMS:22; i <= i+1 by NAT_1:29; then A12: i < j by A9,AXIOMS:22; then A13: i < len f by A11,AXIOMS:22; i -' 1 >= 0 by NAT_1:18; then A14: i -' 1 + p..f > 0+1 by A8,REAL_1:67; now per cases by RLVECT_1:99; suppose i = 0; then LSeg(h,i) = {} by TOPREAL1:def 5; hence thesis by XBOOLE_1:65; suppose that A15: i >= 1 and A16: j < len(f:-p); A17: i < len(f:-p) by A12,A16,AXIOMS:22; A18: 1 <= j by A12,A15,AXIOMS:22; A19: LSeg(h,i) = LSeg(f,i -' 1 + p..f) by A1,A15,A17,Th24; A20: LSeg(h,j) = LSeg(f,j -' 1 + p..f) by A1,A16,A18,Th24; A21: i -' 1 + p..f + 1 = i -' 1 + 1 + p..f by XCMPLX_1:1 .= i + p..f by A15,AMI_5:4 .= i + 1 -' 1 + p..f by BINARITH:39; i < j -' 1 by A9,SPRECT_3:5; then i + 1 -' 1 < j -' 1 by BINARITH:39; then A22: i -' 1 + p..f + 1 < j -' 1 + p..f by A21,REAL_1:53; j -' 1 < len f -' p..f by A4,A6,A16,A18,SPRECT_3:7; then j -' 1 + p..f < len f by SPRECT_3:6; hence LSeg(h,i) misses LSeg(h,j) by A14,A19,A20,A22,GOBOARD5:def 4; suppose that A23: i >= 1 and A24: j >= len(f:-p) and A25: i < len(f:-p); A26: LSeg(h,i) = LSeg(f,i -' 1 + p..f) by A1,A23,A25,Th24; A27: LSeg(h,j) = LSeg(f,j + p..f -' len f) by A1,A11,A24,Th31; len f -' p..f <= len f -' p..f + 1 by NAT_1:29; then len f - p..f <= j by A4,A6,A24,AXIOMS:22; then A28: len f <= j + p..f by REAL_1:86; then A29: len f <= j + p..f + 1 by NAT_1:37; now per cases by A10,Th14; suppose i > 1; then i >= 1+1 by NAT_1:38; then i -' 1 >= 1 by SPRECT_3:8; hence j + 1 < i -' 1 + len f by A11,REAL_1:67; suppose A30: j+1 < len f; i -' 1 >= 0 by NAT_1:18; then 0 + len f <= i -' 1 + len f by AXIOMS:24; hence j + 1 < i -' 1 + len f by A30,AXIOMS:22; end; then j + 1 + p..f < i -' 1 + len f + p..f by REAL_1:53; then j + p..f+1 < i -' 1 + len f + p..f by XCMPLX_1:1; then j + p..f+1 < i -' 1 + p..f + len f by XCMPLX_1:1; then j + p..f+1 -' len f < i -' 1 + p..f by A29,SPRECT_3:7; then A31: j + p..f -' len f+1 < i -' 1 + p..f by A28,JORDAN4:3; now per cases by A9,AXIOMS:22; suppose j > len f - p..f + 1; then 1 < j - (len f - p..f) by REAL_1:86; then 1 < j - len f + p..f by XCMPLX_1:37; then 1 < j + p..f - len f by XCMPLX_1:29; then A32: 1 < j + p..f -' len f by JORDAN3:1; i < len f -' p..f + 1 by A4,A5,A25,SCMFSA_7:3; then i -' 1 < len f -' p..f by A23,SPRECT_3:7; then i -' 1 + p..f < len f by SPRECT_3:6; hence LSeg(h,i) misses LSeg(h,j) by A26,A27,A31,A32,GOBOARD5:def 4; suppose i+1 < len f - p..f + 1; then i < len f - p..f by AXIOMS:24; then i + p..f < len f by REAL_1:86; then i -' 1 + 1 + p..f < len f by A23,AMI_5:4; then i -' 1 + p..f + 1 < len f by XCMPLX_1:1; hence LSeg(h,i) misses LSeg(h,j) by A26,A27,A31,GOBOARD5:def 4; end; hence thesis; suppose A33: i >= len(f:-p); then A34: j >= len(f:-p) by A12,AXIOMS:22; A35: LSeg(h,i) = LSeg(f,i + p..f -' len f) by A1,A13,A33,Th31; A36: LSeg(h,j) = LSeg(f,j + p..f -' len f) by A1,A11,A34,Th31; len f - p..f <= len f - p..f +1 by REAL_1:69; then len f - p..f <= i by A4,A33,AXIOMS:22; then A37: len f <= i + p..f by A6,SPRECT_3:5; then A38: i + p..f -' len f + 1 = i + p..f + 1 -' len f by JORDAN4:3 .= i + 1 + p..f -' len f by XCMPLX_1:1; i + p..f < j + p..f by A12,REAL_1:53; then A39: len f < j + p..f by A37,AXIOMS:22; i + 1 + p..f < j + p..f by A9,REAL_1:53; then A40: i + p..f -' len f + 1 < j + p..f -' len f by A38,A39,SPRECT_3:10 ; j + 1 <= len f & p..f < len f by A3,A5,A7,A10,AXIOMS:21,NAT_1:38; then j + 1 + p..f < len f + len f by REAL_1:67; then j + 1 + p..f - len f < len f by REAL_1:84; then j + (1 + p..f) - len f < len f by XCMPLX_1:1; then j + (p..f + 1 - len f) < len f by XCMPLX_1:29; then j + (p..f - len f + 1) < len f by XCMPLX_1:29; then j + (p..f - len f) + 1 < len f by XCMPLX_1:1; then j + p..f - len f + 1 < len f by XCMPLX_1:29; then j + p..f -' len f + 1 < len f by A39,SCMFSA_7:3; hence LSeg(h,i) misses LSeg(h,j) by A35,A36,A40,GOBOARD5:def 4; end; hence thesis; end; end; definition let p be Point of TOP-REAL 2; let f be non constant standard special_circular_sequence; cluster Rotate(f,p) -> unfolded; coherence proof per cases; suppose not p in rng f; hence thesis by FINSEQ_6:def 2; suppose A1: p in rng f; A2: len f > 4 by GOBOARD7:36; let i such that A3: 1 <= i and A4: i + 2 <= len Rotate(f,p); thus LSeg(Rotate(f,p),i) /\ LSeg(Rotate(f,p),i+1) = {(Rotate(f,p))/.(i+1)} proof A5: len f = len Rotate(f,p) by Th14; A6: 1 <= i+1 by NAT_1:29; i+1 < i+2 by REAL_1:53; then A7: i+1 < len f by A4,A5,AXIOMS:22; A8: i+1 -' 1 + p..f = i + p..f by BINARITH:39 .= i -' 1 + 1 + p..f by A3,AMI_5:4 .= i -' 1 + p..f + 1 by XCMPLX_1:1; A9: len (f:-p) = len f - p..f + 1 by A1,FINSEQ_5:53; A10: len f <= len f + 1 by NAT_1:29; A11: len f >= 1 by A2,AXIOMS:22; per cases by AXIOMS:21; suppose A12: i+1 = len(f:-p); A13: i -' 1 + p..f = i - 1 + p..f by A3,SCMFSA_7:3 .= len f - p..f + 1 - 1 - 1 + p..f by A9,A12,XCMPLX_1:26 .= len f - p..f - 1 + p..f by XCMPLX_1:26 .= len f - p..f + p..f - 1 by XCMPLX_1:29 .= len f - 1 by XCMPLX_1:27 .= len f -' 1 by A11,SCMFSA_7:3; i < len(f:-p) by A12,REAL_1:69; then A14: LSeg(Rotate(f,p),i) = LSeg(f,len f -' 1) by A1,A3,A13,Th24 ; len (f:-p) = len f + 1 - p..f by A9,XCMPLX_1:29; then len (f:-p) + p..f = len f + 1 by XCMPLX_1:27; then len(f:-p) + p..f -' len f = len f + 1 - len f by A10,SCMFSA_7:3 .= 1 by XCMPLX_1:26; then LSeg(Rotate(f,p),len(f:-p)) = LSeg(f,1) by A1,A7,A12,Th31; hence LSeg(Rotate(f,p),i) /\ LSeg(Rotate(f,p),i+1) = {f/.1} by A2,A12,A14,Th30 .= {f/.len f} by FINSEQ_6:def 1 .= {(Rotate(f,p))/.(i+1)} by A1,A12,Th11; suppose A15: i+1 < len(f:-p); i+0 < i+1 by REAL_1:53; then i < len(f:-p) by A15,AXIOMS:22; then A16: LSeg(Rotate(f,p),i) = LSeg(f,i -' 1 + p..f) by A1,A3,Th24; 1 <= i+1 by NAT_1:29; then A17: LSeg(Rotate(f,p),i+1) = LSeg(f,i+1 -' 1 + p..f) by A1,A15, Th24; i -' 1 + p..f >= p..f & p..f >= 1 by A1,FINSEQ_4:31,NAT_1:29; then A18: 1 <= i -' 1 + p..f by AXIOMS:22; i + 1 < len f - p..f + 1 by A1,A15,FINSEQ_5:53; then i < len f - p..f by AXIOMS:24; then i + p..f < len f by REAL_1:86; then i -' 1 + 1 + p..f < len f by A3,AMI_5:4; then i -' 1 + p..f + 1 < len f by XCMPLX_1:1; then i -' 1 + p..f + 1 + 1 <= len f by NAT_1:38; then i -' 1 + p..f + (1+1) <= len f by XCMPLX_1:1; hence LSeg(Rotate(f,p),i) /\ LSeg(Rotate(f,p),i+1) = {f/.(i+1 -' 1 + p..f)} by A8,A16,A17,A18,TOPREAL1:def 8 .= {(Rotate(f,p))/.(i+1)} by A1,A6,A15,Th9; suppose A19: len(f:-p) < i+1; i+(1+1) <= len f by A4,Th14; then i+1+1 <= len f by XCMPLX_1:1; then A20: i+1 < len f by NAT_1:38; i+0 < i+1 by REAL_1:53; then A21: i < len f by A20,AXIOMS:22; len(f:-p) <= i by A19,NAT_1:38; then A22: LSeg(Rotate(f,p),i) = LSeg(f,i + p..f -' len f) by A1,A21, Th31; A23: LSeg(Rotate(f,p),i+1) = LSeg(f,i+1 + p..f -' len f) by A1,A19,A20,Th31 ; i + 1 > len f - p..f + 1 by A1,A19,FINSEQ_5:53; then len f - p..f < i by AXIOMS:24; then A24: len f < i + p..f by REAL_1:84; then A25: i + p..f -' len f = i + p..f - len f by SCMFSA_7:3; 0 < i + p..f - len f by A24,SQUARE_1:11; then A26: 0+1 <= i + p..f -' len f by A25,NAT_1:38; A27: i+1 + p..f -' len f = i + p..f + 1 -' len f by XCMPLX_1:1 .= i + p..f -' len f + 1 by A24,JORDAN4:3; p..f <= len f by A1,FINSEQ_4:31; then i + 2 + p..f <= len f + len f by A4,A5,REAL_1:55; then i + p..f + 2 <= len f + len f by XCMPLX_1:1; then i + p..f + 2 - len f <= len f by REAL_1:86; then i + p..f - len f + 2 <= len f by XCMPLX_1:29; hence LSeg(Rotate(f,p),i) /\ LSeg(Rotate(f,p),i+1) = {f/.(i+1 + p..f -' len f)} by A22,A23,A25,A26,A27,TOPREAL1:def 8 .= {(Rotate(f,p))/.(i+1)} by A1,A7,A19,Th17; end; end; end; theorem Th32: p in rng f & 1 <= i & i < p..f implies LSeg(f,i) = LSeg(Rotate(f,p),i + len f -' p..f) proof assume that A1: p in rng f and A2: 1 <= i and A3: i < p..f; A4: p..f <= len f by A1,FINSEQ_4:31; len f <= i + len f by NAT_1:29; then A5: p.. f <= i + len f by A4,AXIOMS:22; len f + 1 <= i + len f by A2,AXIOMS:24; then len f + 1 -' p..f <= i + len f -' p..f by JORDAN3:5; then len f -' p..f + 1 <= i + len f -' p..f by A4,JORDAN4:3; then len f - p..f + 1 <= i + len f -' p..f by A4,SCMFSA_7:3; then A6: len(f:-p) <= i + len f -' p..f by A1,FINSEQ_5:53; i + len f < len f + p..f by A3,REAL_1:53; then A7: i + len f -' p..f < len f by A5,SPRECT_3:7; i + len f -' p..f + p..f -' len f = i + len f -' len f by A5,AMI_5:4 .= i by BINARITH:39; hence LSeg(f,i) = LSeg(Rotate(f,p),i + len f -' p..f) by A1,A6,A7,Th31; end; theorem Th33: L~Rotate(f,p) = L~f proof per cases; suppose not p in rng f; hence thesis by FINSEQ_6:def 2; suppose A1: p in rng f; A2: len Rotate(f,p) = len f by Th14; set A = { LSeg(Rotate(f,p),i) : 1 <= i & i+1 <= len f }; set B = { LSeg(f,i) : 1 <= i & i+1 <= len f }; A = B proof A3: p..f <= len f by A1,FINSEQ_4:31; thus A c= B proof let x be set; assume x in A; then consider i such that A4: x = LSeg(Rotate(f,p),i) and A5: 1 <= i and A6: i+1 <= len f; A7: i < len f by A6,NAT_1:38; A8: 1 <= p..f by A1,FINSEQ_4:31; per cases; suppose A9: i < len(f:-p); then A10: LSeg(Rotate(f,p),i) = LSeg(f,i -' 1 + p..f) by A1,A5,Th24 ; 1 + 1 <= i + p..f by A5,A8,REAL_1:55; then 1 <= i + p..f -' 1 by SPRECT_3:8; then A11: 1 <= i -' 1 + p..f by A5,JORDAN4:3; i < len f - p..f + 1 by A1,A9,FINSEQ_5:53; then i < len f -' p..f + 1 by A3,SCMFSA_7:3; then i -' 1 < len f -' p..f by A5,SPRECT_3:7; then i -' 1 + p..f < len f by SPRECT_3:6; then i -' 1 + p..f + 1 <= len f by NAT_1:38; hence x in B by A4,A10,A11; suppose A12: i >= len(f:-p); then A13: LSeg(Rotate(f,p),i) = LSeg(f,i + p..f -' len f) by A1,A7, Th31; len f - p..f + 1 <= i by A1,A12,FINSEQ_5:53; then len f -' p..f + 1 <= i by A3,SCMFSA_7:3; then 1 + len f -' p..f <= i by A3,JORDAN4:3; then A14: 1 + len f <= i + p..f by SPRECT_3:5; then A15: 1 <= i + p..f -' len f by SPRECT_3:8; len f <= len f + 1 by NAT_1:29; then A16: len f <= i + p..f by A14,AXIOMS:22; i + 1 + p..f <= len f + len f by A3,A6,REAL_1:55; then i + p..f + 1 <= len f + len f by XCMPLX_1:1; then i + p..f + 1 -' len f <= len f by SPRECT_3:6; then i + p..f -' len f + 1 <= len f by A16,JORDAN4:3; hence x in B by A4,A13,A15; end; let x be set; assume x in B; then consider i such that A17: x = LSeg(f,i) and A18: 1 <= i and A19: i+1 <= len f; A20: i < len f by A19,NAT_1:38; per cases; suppose A21: p..f <= i; then A22: LSeg(f,i) = LSeg(Rotate(f,p),i -' p..f+1) by A1,A20,Th25; 1 + p..f <= i+1 by A21,AXIOMS:24; then 1 <= i+1 -' p..f by SPRECT_3:8; then A23: 1 <= i -' p..f+1 by A21,JORDAN4:3; i <= i+1 by NAT_1:29; then A24: p..f <= i+1 by A21,AXIOMS:22; 1 <= p..f by A1,FINSEQ_4:31; then i + 1 < len f + p..f by A20,REAL_1:67; then i + 1 -' p..f < len f by A24,SPRECT_3:7; then i -' p..f+1 < len f by A21,JORDAN4:3; then i -' p..f+1 +1 <= len f by NAT_1:38; hence x in A by A17,A22,A23; suppose A25: i < p..f; then A26: LSeg(f,i) = LSeg(Rotate(f,p),i + len f -' p..f) by A1,A18,Th32; 1 + p..f <= i + len f by A3,A18,REAL_1:55; then A27: 1 <= i + len f -' p..f by SPRECT_3:8; A28: p..f <= len f by A1,FINSEQ_4:31; len f <= i + len f by NAT_1:29; then A29: p..f <= i + len f by A28,AXIOMS:22; i + 1 <= p..f by A25,NAT_1:38; then i + 1 + len f <= len f + p..f by AXIOMS:24; then i + len f + 1 <= len f + p..f by XCMPLX_1:1; then i + len f + 1 -' p..f <= len f by SPRECT_3:6; then i + len f -' p..f + 1 <= len f by A29,JORDAN4:3; hence x in A by A17,A26,A27; end; hence L~Rotate(f,p) = union B by A2,TOPREAL1:def 6 .= L~f by TOPREAL1:def 6; end; theorem Th34: for G being Go-board holds f is_sequence_on G iff Rotate(f,p) is_sequence_on G proof let G be Go-board; A1: dom f = dom Rotate(f,p) by Th15; A2: len f = len Rotate(f,p) by Th14; per cases; suppose not p in rng f; hence thesis by FINSEQ_6:def 2; suppose A3: p in rng f; then A4: p..f <= len f by FINSEQ_4:31; A5: 1 <= p..f by A3,FINSEQ_4:31; thus f is_sequence_on G implies Rotate(f,p) is_sequence_on G proof assume A6: f is_sequence_on G; thus for n st n in dom Rotate(f,p) ex i,j st [i,j] in Indices G & (Rotate(f,p))/.n = G*(i,j) proof let n; assume n in dom Rotate(f,p); then A7: 1 <= n & n <= len Rotate(f,p) by FINSEQ_3:27; per cases; suppose A8: len(f:-p) <= n; then len f - p..f + 1 <= n by A3,FINSEQ_5:53; then len f -' p..f + 1 <= n by A4,SCMFSA_7:3; then len f + 1 -' p..f <= n by A4,JORDAN4:3; then len f + 1 <= n + p..f by SPRECT_3:5; then A9: 1 <= n + p..f -' len f by SPRECT_3:8; n + p..f <= len f + len f by A2,A4,A7,REAL_1:55; then n + p..f -' len f <= len f by SPRECT_3:6; then n + p..f -' len f in dom Rotate(f,p) by A2,A9,FINSEQ_3:27; then consider i,j such that A10: [i,j] in Indices G and A11: f/.(n + p..f -' len f) = G*(i,j) by A1,A6,GOBOARD1:def 11; take i,j; thus [i,j] in Indices G by A10; thus (Rotate(f,p))/.n = G*(i,j) by A2,A3,A7,A8,A11,Th17; suppose A12: len(f:-p) >= n; 1 + 1 <= n + p..f by A5,A7,REAL_1:55; then 1 <= n + p..f -' 1 by SPRECT_3:8; then A13: 1 <= n -' 1 + p..f by A7,JORDAN4:3; len f - p..f + 1 >= n by A3,A12,FINSEQ_5:53; then len f -' p..f + 1 >= n by A4,SCMFSA_7:3; then n -' 1 <= len f -' p..f by SPRECT_3:6; then n -' 1 + p..f <= len f by A4,SPRECT_3:7; then n -' 1 + p..f in dom Rotate(f,p) by A2,A13,FINSEQ_3:27; then consider i,j such that A14: [i,j] in Indices G and A15: f/.(n -' 1 + p..f) = G*(i,j) by A1,A6,GOBOARD1:def 11; take i,j; thus [i,j] in Indices G by A14; thus (Rotate(f,p))/.n = G*(i,j) by A3,A7,A12,A15,Th9; end; let n such that A16: n in dom Rotate(f,p) and A17: n+1 in dom Rotate(f,p); let m,k,i,j such that A18: [m,k] in Indices G & [i,j] in Indices G & (Rotate(f,p))/.n = G*(m,k) & (Rotate(f,p))/.(n+1) = G*(i,j); A19: 1 <= n & n <= len f by A1,A16,FINSEQ_3:27; A20: 1 <= n+1 & n+1 <= len f by A1,A17,FINSEQ_3:27; thus abs(m-i)+abs(k-j) = 1 proof per cases; suppose that A21: len(f:-p) <= n; n <= n+1 by NAT_1:29; then A22: len(f:-p) <= n+1 by A21,AXIOMS:22; A23: (Rotate(f,p))/.n = f/.(n + p..f -' len f) by A3,A19,A21,Th17; A24: (Rotate(f,p))/.(n+1) = f/.(n+1 + p..f -' len f) by A3,A20,A22,Th17; A25: len f - p..f + 1 <= n + 1 by A3,A22,FINSEQ_5:53; then len f - p..f <= n by REAL_1:53; then A26: len f <= n + p..f by REAL_1:86; A27: n+1 + p..f -' len f = n + p..f + 1 -' len f by XCMPLX_1:1 .= n + p..f -' len f + 1 by A26,JORDAN4:3; len f - p..f + 1 <= n by A3,A21,FINSEQ_5:53; then len f -' p..f + 1 <= n by A4,SCMFSA_7:3; then len f + 1 -' p..f <= n by A4,JORDAN4:3; then len f + 1 <= n + p..f by SPRECT_3:5; then A28: 1 <= n + p..f -' len f by SPRECT_3:8; n + p..f <= len f + len f by A4,A19,REAL_1:55; then n + p..f -' len f <= len f by SPRECT_3:6; then A29: n + p..f -' len f in dom f by A28,FINSEQ_3:27; len f -' p..f + 1 <= n+1 by A4,A25,SCMFSA_7:3; then len f + 1 -' p..f <= n+1 by A4,JORDAN4:3; then len f + 1 <= n+1 + p..f by SPRECT_3:5; then A30: 1 <= n+1 + p..f -' len f by SPRECT_3:8; n+1 + p..f <= len f + len f by A4,A20,REAL_1:55; then n+1 + p..f -' len f <= len f by SPRECT_3:6; then n+1 + p..f -' len f in dom f by A30,FINSEQ_3:27; hence abs(m-i)+abs(k-j) = 1 by A6,A18,A23,A24,A27,A29,GOBOARD1:def 11; suppose A31: len(f:-p) > n; then A32: len(f:-p) >= n+1 by NAT_1:38; A33: (Rotate(f,p))/.n = f/.(n -' 1 + p..f) by A3,A19,A31,Th9; A34: (Rotate(f,p))/.(n+1) = f/.(n+1 -' 1 + p..f) by A3,A20,A32,Th9; A35: n+1 -' 1 + p..f = n + p..f by BINARITH:39 .= n -' 1 + 1 + p..f by A19,AMI_5:4 .= n -' 1 + p..f + 1 by XCMPLX_1:1; 1 + 1 <= n + p..f by A5,A19,REAL_1:55; then 1 <= n + p..f -' 1 by SPRECT_3:8; then A36: 1 <= n -' 1 + p..f by A19,JORDAN4:3; n <= len f - p..f + 1 by A3,A31,FINSEQ_5:53; then n <= len f -' p..f + 1 by A4,SCMFSA_7:3; then n -' 1 <= len f -' p..f by SPRECT_3:6; then n -' 1 + p..f <= len f by A4,SPRECT_3:7; then A37: n -' 1 + p..f in dom f by A36,FINSEQ_3:27; 1 + 1 <= n+1 + p..f by A5,A20,REAL_1:55; then 1 <= n+1 + p..f -' 1 by SPRECT_3:8; then A38: 1 <= n+1 -' 1 + p..f by A20,JORDAN4:3; n+1 <= len f - p..f + 1 by A3,A32,FINSEQ_5:53; then n+1 <= len f -' p..f + 1 by A4,SCMFSA_7:3; then n+1 -' 1 <= len f -' p..f by SPRECT_3:6; then n+1 -' 1 + p..f <= len f by A4,SPRECT_3:7; then n+1 -' 1 + p..f in dom f by A38,FINSEQ_3:27; hence abs(m-i)+abs(k-j) = 1 by A6,A18,A33,A34,A35,A37,GOBOARD1:def 11; end; end; assume A39: Rotate(f,p) is_sequence_on G; thus for n st n in dom f ex i,j st [i,j] in Indices G & f/.n = G*(i,j) proof let n; assume n in dom f; then A40: 1 <= n & n <= len f by FINSEQ_3:27; per cases; suppose A41: n <= p..f; n <= n + (len f -' p..f) by NAT_1:29; then 1 <= n + (len f -' p..f) by A40,AXIOMS:22; then A42: 1 <= n + len f -' p..f by A4,JORDAN4:3; n + len f <= len f + p..f by A41,AXIOMS:24; then n + len f -' p..f <= len f by SPRECT_3:6; then n + len f -' p..f in dom f by A42,FINSEQ_3:27; then consider i,j such that A43: [i,j] in Indices G and A44: (Rotate(f,p))/.(n + len f -' p..f) = G*(i,j) by A1,A39,GOBOARD1:def 11; take i,j; thus [i,j] in Indices G by A43; thus f/.n = G*(i,j) by A3,A40,A41,A44,Th18; suppose A45: n >= p..f; then 1 + p..f <= n + 1 by AXIOMS:24; then A46: 1 <= n + 1 -' p..f by SPRECT_3:8; n + 1 <= len f + p..f by A5,A40,REAL_1:55; then n + 1 -' p..f <= len f by SPRECT_3:6; then n + 1 -' p..f in dom f by A46,FINSEQ_3:27; then consider i,j such that A47: [i,j] in Indices G and A48: (Rotate(f,p))/.(n + 1 -' p..f) = G*(i,j) by A1,A39,GOBOARD1:def 11; take i,j; thus [i,j] in Indices G by A47; thus f/.n = G*(i,j) by A3,A40,A45,A48,Th10; end; let n such that A49: n in dom f and A50: n+1 in dom f; A51: 1 <= n & n <= len f by A49,FINSEQ_3:27; A52: 1 <= n+1 & n+1 <= len f by A50,FINSEQ_3:27; let m,k,i,j such that A53: [m,k] in Indices G and A54: [i,j] in Indices G and A55: f/.n = G*(m,k) and A56: f/.(n+1) = G*(i,j); thus abs(m-i)+abs(k-j) = 1 proof per cases; suppose A57: n < p..f; then A58: n+1 <= p..f by NAT_1:38; A59: f/.n = (Rotate(f,p))/.(n + len f -' p..f) by A3,A51,A57,Th18; A60: f/.(n+1) = (Rotate(f,p))/.(n+1 + len f -' p..f) by A3,A52,A58,Th18; A61: n+1 + len f -' p..f = len f -' p..f + (n+1) by A4,JORDAN4:3 .= len f -' p..f + n+1 by XCMPLX_1:1 .= n + len f -' p..f + 1 by A4,JORDAN4:3; n <= n + (len f -' p..f) by NAT_1:29; then 1 <= n + (len f -' p..f) by A51,AXIOMS:22; then A62: 1 <= n + len f -' p..f by A4,JORDAN4:3; n + len f <= len f + p..f by A57,AXIOMS:24; then n + len f -' p..f <= len f by SPRECT_3:6; then A63: n + len f -' p..f in dom f by A62,FINSEQ_3:27; n+1 <= n+1 + (len f -' p..f) by NAT_1:29; then 1 <= n+1 + (len f -' p..f) by A52,AXIOMS:22; then A64: 1 <= n+1 + len f -' p..f by A4,JORDAN4:3; n+1 + len f <= len f + p..f by A58,AXIOMS:24; then n+1 + len f -' p..f <= len f by SPRECT_3:6; then n+1 + len f -' p..f in dom f by A64,FINSEQ_3:27; hence abs(m-i)+abs(k-j) = 1 by A1,A39,A53,A54,A55,A56,A59,A60,A61,A63,GOBOARD1:def 11; suppose A65: n >= p..f; n <= n+1 by NAT_1:29; then A66: n+1 >= p..f by A65,AXIOMS:22; then A67: f/.(n+1) = (Rotate(f,p))/.(n+1 + 1 -' p..f) by A3,A52,Th10; A68: f/.n = (Rotate(f,p))/.(n + 1 -' p..f) by A3,A51,A65,Th10; A69: n+1 + 1 -' p..f = n + 1 -' p..f + 1 by A66,JORDAN4:3; 1 + p..f <= n+1 + 1 by A66,AXIOMS:24; then A70: 1 <= n+1 + 1 -' p..f by SPRECT_3:8; n+1 + 1 <= len f + p..f by A5,A52,REAL_1:55; then n+1 + 1 -' p..f <= len f by SPRECT_3:6; then A71: n+1 + 1 -' p..f in dom f by A70,FINSEQ_3:27; 1 + p..f <= n + 1 by A65,AXIOMS:24; then A72: 1 <= n + 1 -' p..f by SPRECT_3:8; n + 1 <= len f + p..f by A5,A51,REAL_1:55; then n + 1 -' p..f <= len f by SPRECT_3:6; then n + 1 -' p..f in dom f by A72,FINSEQ_3:27; hence abs(m-i)+abs(k-j) = 1 by A1,A39,A53,A54,A55,A56,A67,A68,A69,A71,GOBOARD1:def 11; end; end; definition let p be Point of TOP-REAL 2; let f be standard (non empty circular FinSequence of TOP-REAL 2); cluster Rotate(f,p) -> standard; coherence proof A1: GoB Rotate(f,p) = GoB f by Th28; f is_sequence_on GoB f by GOBOARD5:def 5; hence Rotate(f,p) is_sequence_on GoB Rotate(f,p) by A1,Th34; end; end; theorem Th35: for f being non constant standard special_circular_sequence, p,k st p in rng f & 1 <= k & k < p..f holds left_cell(f,k) = left_cell(Rotate(f,p),k + len f -' p..f) proof let f be non constant standard special_circular_sequence, p,k such that A1: p in rng f and A2: 1 <= k and A3: k < p..f; A4: p..f <= len f by A1,FINSEQ_4:31; then A5: k < len f by A3,AXIOMS:22; 0 < k by A2,AXIOMS:22; then A6: 0+1 < k+1 by REAL_1:53; A7: k+1 <= p..f by A3,NAT_1:38; A8: k+1 <= len f by A5,NAT_1:38; set n = k + len f -' p..f; len f <= k + len f by NAT_1:29; then p..f <= k + len f by A4,AXIOMS:22; then A9: n+1 = k + len f + 1 -' p..f by JORDAN4:3; then A10: n+1 = k + 1 + len f -' p..f by XCMPLX_1:1; 1 + p..f <= k + len f by A2,A4,REAL_1:55; then A11: 1 <= n by SPRECT_3:8; k + 1 + len f <= len f + p..f by A7,AXIOMS:24; then k + len f + 1 <= len f + p..f by XCMPLX_1:1; then n+1 <= len f by A9,SPRECT_3:6; then A12: n+1 <= len Rotate(f,p) by Th14; for i1,j1,i2,j2 being Nat st [i1,j1] in Indices GoB Rotate(f,p) & [i2,j2] in Indices GoB Rotate(f,p) & (Rotate(f,p))/.n = (GoB Rotate(f,p))*(i1,j1) & (Rotate(f,p))/.(n+1) = (GoB Rotate(f,p))*(i2,j2) holds i1 = i2 & j1+1 = j2 & left_cell(f,k) = cell(GoB Rotate(f,p),i1-'1,j1) or i1+1 = i2 & j1 = j2 & left_cell(f,k) = cell(GoB Rotate(f,p),i1,j1) or i1 = i2+1 & j1 = j2 & left_cell(f,k) = cell(GoB Rotate(f,p),i2,j2-'1) or i1 = i2 & j1 = j2+1 & left_cell(f,k) = cell(GoB Rotate(f,p),i1,j2) proof let i1,j1,i2,j2 be Nat such that A13: [i1,j1] in Indices GoB Rotate(f,p) and A14: [i2,j2] in Indices GoB Rotate(f,p) and A15: (Rotate(f,p))/.n = (GoB Rotate(f,p))*(i1,j1) and A16: (Rotate(f,p))/.(n+1) = (GoB Rotate(f,p))*(i2,j2); A17: GoB Rotate(f,p) = GoB f by Th28; then A18: f/.k = (GoB f)*(i1,j1) by A1,A2,A3,A15,Th18; A19: f/.(k+1) = (GoB f)*(i2,j2) by A1,A6,A7,A10,A16,A17,Th18; A20: left_cell(f,k) = left_cell(f,k); then A21: i1 = i2 & j1+1 = j2 & left_cell(f,k) = cell(GoB f,i1-'1,j1) or i1+1 = i2 & j1 = j2 & left_cell(f,k) = cell(GoB f,i1,j1) or i1 = i2+1 & j1 = j2 & left_cell(f,k) = cell(GoB f,i2,j2-'1) or i1 = i2 & j1 = j2+1 & left_cell(f,k) = cell(GoB f,i1,j2) by A2,A8,A13,A14,A17,A18,A19,GOBOARD5:def 7; A22: j1+1+1 = j1+(1+1) by XCMPLX_1:1; A23: i1+1+1 = i1+(1+1) by XCMPLX_1:1; per cases by A2,A8,A13,A14,A17,A18,A19,A20,GOBOARD5:def 7; case i1 = i2 & j1+1 = j2; hence left_cell(f,k) = cell(GoB Rotate(f,p),i1-'1,j1) by A21,A22,Th28,REAL_1 :69; case i1+1 = i2 & j1 = j2; hence left_cell(f,k) = cell(GoB Rotate(f,p),i1,j1) by A21,A23,Th28,REAL_1:69 ; case i1 = i2+1 & j1 = j2; hence left_cell(f,k) = cell(GoB Rotate(f,p),i2,j2-'1) by A21,A23,Th28,REAL_1 :69; case i1 = i2 & j1 = j2+1; hence left_cell(f,k) = cell(GoB Rotate(f,p),i1,j2) by A21,A22,Th28,REAL_1:69 ; end; hence left_cell(f,k) = left_cell(Rotate(f,p),n) by A11,A12,GOBOARD5:def 7; end; theorem Th36: for f being non constant standard special_circular_sequence holds LeftComp Rotate(f,p) = LeftComp f proof let f be non constant standard special_circular_sequence; LeftComp Rotate(f,p) is_a_component_of (L~Rotate(f,p))` by GOBOARD9:def 1; then A1: LeftComp Rotate(f,p) is_a_component_of (L~f)` by Th33; A2: p in rng f implies p..f >= 1 by FINSEQ_4:31; per cases by A2,AXIOMS:21; suppose not p in rng f; hence LeftComp Rotate(f,p) = LeftComp f by FINSEQ_6:def 2; suppose that A3: p in rng f and A4: p..f = 1; A5: 1 in dom f by FINSEQ_5:6; f.1 = p by A3,A4,FINSEQ_4:29; then f/.1 = p by A5,FINSEQ_4:def 4; hence LeftComp Rotate(f,p) = LeftComp f by FINSEQ_6:95; suppose that A6: p in rng f and A7: 1 < p..f; A8: p..f <= len f by A6,FINSEQ_4:31; then 1 + p..f <= 1 + len f by AXIOMS:24; then A9: 1 <= 1 + len f -' p..f by SPRECT_3:8; len f <= len f + 1 by NAT_1:29; then A10: p..f <= len f + 1 by A8,AXIOMS:22; 1 + 1 <= p..f by A7,NAT_1:38; then 1 + 1 + len f <= len f + p..f by AXIOMS:24; then 1 + len f + 1 <= len f + p..f by XCMPLX_1:1; then 1 + len f + 1 -' p..f <= len f by SPRECT_3:6; then 1 + len f -' p..f + 1 <= len f by A10,JORDAN4:3; then A11: 1 + len f -' p..f + 1 <= len Rotate(f,p) by Th14; left_cell(f,1) = left_cell(Rotate(f,p),1 + len f -' p..f) by A6,A7,Th35; then Int left_cell(f,1) c= LeftComp Rotate(f,p) by A9,A11,GOBOARD9:24; hence LeftComp Rotate(f,p) = LeftComp f by A1,GOBOARD9:def 1; end; theorem for f being non constant standard special_circular_sequence holds RightComp Rotate(f,p) = RightComp f proof let f be non constant standard special_circular_sequence; A1: RightComp Rotate(f,p) = LeftComp Rev Rotate(f,p) by GOBOARD9:26 .= LeftComp Rotate(Rev f,p) by Th29; RightComp f = LeftComp Rev f by GOBOARD9:26; hence RightComp Rotate(f,p) = RightComp f by A1,Th36; end; begin :: Clockwise oriented Lm1: for f being non constant standard special_circular_sequence st f/.1 = N-min L~f holds f is clockwise_oriented or Rev f is clockwise_oriented proof let f be non constant standard special_circular_sequence such that A1: f/.1 = N-min L~f; reconsider A = L~Rev f as non empty compact Subset of TOP-REAL 2; A2: (Rev f)/.1 = f/.len f by FINSEQ_5:68 .= N-min L~f by A1,FINSEQ_6:def 1 .= N-min A by SPPOL_2:22; A3:len f > 4 by GOBOARD7:36; then A4: len f > 1+1 by AXIOMS:22; A5: len f > 1 by A3,AXIOMS:22; A6: 1 <= len f -' 1 by A4,SPRECT_3:8; A7: len f -' 1 <= len f by JORDAN3:7; then A8: len f -' 1 in dom f by A6,FINSEQ_3:27; len f -' 1 + (1+1) = len f -' 1 + 1 + 1 by XCMPLX_1:1 .= len f + 1 by A5,AMI_5:4; then A9: (Rev f)/.2 = f/.(len f -' 1) by A8,FINSEQ_5:69; A10: [i_w_n f, width GoB f] in Indices GoB f by JORDAN5D:def 7; A11: (GoB f)*(i_w_n f,width GoB f) = N-min L~f by JORDAN5D:def 7; A12: 1+1 in dom f by A4,FINSEQ_3:27; then consider i1,j1 being Nat such that A13: [i1,j1] in Indices GoB f and A14: f/.2 = (GoB f)*(i1,j1) by GOBOARD5:12; consider i2,j2 being Nat such that A15: [i2,j2] in Indices GoB f and A16: f/.(len f -' 1) = (GoB f)*(i2,j2) by A8,GOBOARD5:12; A17: 1 <= width GoB f by A10,GOBOARD5:1; A18: 1 <= j1 & j1 <= width GoB f by A13,GOBOARD5:1; A19: 1 <= j2 & j2 <= width GoB f by A15,GOBOARD5:1; A20: 1 <= i_w_n f & i_w_n f <= len GoB f by A10,GOBOARD5:1; A21: 1 <= i1 & i1 <= len GoB f by A13,GOBOARD5:1; A22: 1 <= i2 & i2 <= len GoB f by A15,GOBOARD5:1; A23: 1 in dom f by A5,FINSEQ_3:27; A24: (GoB f)*(i1,j1) in L~f by A4,A12,A14,GOBOARD1:16; A25: 1 <= width GoB f by A18,AXIOMS:22; A26: now assume A27: width GoB f = j1; then (GoB f)*(1,j1)`2 = N-bound L~f by JORDAN5D:42; then (GoB f)*(i1,j1)`2 = N-bound L~f by A18,A21,GOBOARD5:2; then (GoB f)*(i1,j1) in N-most L~f by A24,SPRECT_2:14; then (N-min L~f)`1 <= (GoB f)*(i1,j1)`1 by PSCOMP_1:98; hence i_w_n f <= i1 by A11,A18,A20,A21,A27,GOBOARD5:4; end; abs(i_w_n f-i1)+abs(width GoB f-j1) = 1 by A1,A10,A11,A12,A13,A14,A23,GOBOARD5:13; then abs(i_w_n f-i1)=1 & width GoB f=j1 or abs(width GoB f-j1)=1 & i_w_n f= i1 by GOBOARD1:2; then A28: i1 = i_w_n f+1 & width GoB f = j1 or width GoB f = j1+1 & i_w_n f = i1 by A18,A26,GOBOARD1:1; A29: len f in dom f by A5,FINSEQ_3:27; A30: (GoB f)*(i2,j2) in L~f by A4,A8,A16,GOBOARD1:16; A31: now assume A32: width GoB f = j2; then (GoB f)*(1,j2)`2 = N-bound L~f by JORDAN5D:42; then (GoB f)*(i2,j2)`2 = N-bound L~f by A19,A22,GOBOARD5:2; then (GoB f)*(i2,j2) in N-most L~f by A30,SPRECT_2:14; then (N-min L~f)`1 <= (GoB f)*(i2,j2)`1 by PSCOMP_1:98; hence i_w_n f <= i2 by A11,A20,A22,A25,A32,GOBOARD5:4; end; A33: len f -' 1 + 1 = len f by A5,AMI_5:4; then f/.(len f -' 1 + 1) = f/.1 by FINSEQ_6:def 1; then abs(i2-i_w_n f)+abs(j2-width GoB f) = 1 by A1,A8,A10,A11,A15,A16,A29,A33,GOBOARD5:13; then abs(i2-i_w_n f)=1 & j2=width GoB f or abs(j2-width GoB f)=1 & i2=i_w_n f by GOBOARD1:2; then A34: i2 = i_w_n f+1 & j2 = width GoB f or j2+1 = width GoB f & i2 = i_w_n f by A19,A31,GOBOARD1:1; A35: j2 + 1 -' 1 = j2 by BINARITH:39; A36: j1 + 1 -' 1 = j1 by BINARITH:39; A37: A = L~f by SPPOL_2:22; A38: 1 <= i_w_n f +1 by NAT_1:29; A39: i_w_n f < i_e_n f by SPRECT_3:44; i_e_n f <= len GoB f by JORDAN5D:47; then i_w_n f < len GoB f by A39,AXIOMS:22; then A40: i_w_n f +1 <= len GoB f by NAT_1:38; 1+1+1 < len f by A3,AXIOMS:22; then 2 < len f -' 1 by SPRECT_3:5; then (f/.2)`2 = (GoB f)*(1,width GoB f)`2 or (f/.(len f -' 1))`2 = (GoB f)*(1,width GoB f)`2 by A7,A14,A16,A17,A28,A34,A35,A36,A38,A40,GOBOARD5:2,GOBOARD7:39; then (f/.2)`2 = N-bound L~f or (f/.(len f -' 1))`2 = N-bound L~f by JORDAN5D:42; then f/.2 in N-most L~f or f/.(len f -' 1) in N-most L~f by A14,A16,A24,A30,SPRECT_2:14; hence thesis by A1,A2,A9,A37,SPRECT_2:34; end; definition let p be Point of TOP-REAL 2; let f be clockwise_oriented (non constant standard special_circular_sequence); cluster Rotate(f,p) -> clockwise_oriented; coherence proof A1: for i st 1 < i & i < len f holds f/.i <> f/.1 by GOBOARD7:38; A2: L~Rotate(f,p) = L~f by Th33; per cases; suppose A3: N-min L~f = f/.1; then Rotate(Rotate(f,p),N-min L~f) = f by A1,Th16; hence (Rotate(Rotate(f,p),N-min L~Rotate(f,p)))/.2 in N-most L~Rotate(f,p) by A2,A3,SPRECT_2:34; suppose A4: N-min L~f <> f/.1; A5: f just_once_values N-min L~f proof take n_w_n f; A6: 1 <= n_w_n f & n_w_n f + 1 <= len f by JORDAN5D:def 15; then A7: 1 <= n_w_n f & n_w_n f < len f by NAT_1:38; hence A8: n_w_n f in dom f by FINSEQ_3:27; thus A9: N-min L~f = f.n_w_n f by JORDAN5D:def 15 .= f/.n_w_n f by A8,FINSEQ_4:def 4; let z be set; assume A10: z in dom f; then reconsider k = z as Nat; assume A11: z <> n_w_n f; per cases by A11,AXIOMS:21; suppose A12: k < n_w_n f; 1 <= k by A10,FINSEQ_3:27; hence f/.z <> N-min L~f by A7,A9,A12,GOBOARD7:38; suppose A13: k > n_w_n f; A14: 1 < n_w_n f by A4,A6,A9,AXIOMS:21; k <= len f by A10,FINSEQ_3:27; hence f/.z <> N-min L~f by A9,A13,A14,GOBOARD7:39; end; (Rotate(f,N-min L~f))/.2 in N-most L~f by SPRECT_2:def 4; hence (Rotate(Rotate(f,p),N-min L~Rotate(f,p)))/.2 in N-most L~Rotate(f,p) by A2,A5,FINSEQ_6:111; end; end; theorem for f being non constant standard special_circular_sequence holds f is clockwise_oriented or Rev f is clockwise_oriented proof let f be non constant standard special_circular_sequence; per cases; suppose N-min L~f = f/.1; hence thesis by Lm1; suppose A1: N-min L~f <> f/.1; thus thesis proof set g = Rotate(f,N-min L~f); A2: N-min L~f in rng f by SPRECT_2:43; L~f = L~g by Th33; then A3: g/.1 = N-min L~g by A2,FINSEQ_6:98; A4: for i st 1 < i & i < len f holds f/.i <> f/.1 by GOBOARD7:38; per cases by A3,Lm1; suppose g is clockwise_oriented; then reconsider g as clockwise_oriented (non constant standard special_circular_sequence); f = Rotate(g,f/.1) by A4,Th16; hence f is clockwise_oriented or Rev f is clockwise_oriented; suppose Rev g is clockwise_oriented; then reconsider h = Rev g as clockwise_oriented (non constant standard special_circular_sequence); A5: g just_once_values f/.1 proof take (f/.1)..g; A6: N-min L~f in rng f by SPRECT_2:43; f/.1 in rng f by FINSEQ_6:46; then A7: f/.1 in rng g by A6,FINSEQ_6:96; A8: f/.1 <> g/.1 by A1,A6,FINSEQ_6:98; thus A9: (f/.1)..g in dom g by A7,FINSEQ_4:30; thus A10: f/.1 = g.((f/.1)..g) by A7,FINSEQ_4:29 .= g/.((f/.1)..g) by A9,FINSEQ_4:def 4; let z be set such that A11: z in dom g and A12: z <> (f/.1)..g; reconsider k = z as Nat by A11; per cases by A12,AXIOMS:21; suppose A13: k < (f/.1)..g; A14: (f/.1)..g <= len g by A7,FINSEQ_4:31; (f/.1)..g <> len g by A8,A10,FINSEQ_6:def 1; then A15: (f/.1)..g < len g by A14,AXIOMS:21; 1 <= k by A11,FINSEQ_3:27; hence g/.z <> f/.1 by A10,A13,A15,GOBOARD7:38; suppose A16: k > (f/.1)..g; (f/.1)..g >= 1 by A7,FINSEQ_4:31; then A17: (f/.1)..g > 1 by A8,A10,AXIOMS:21; k <= len g by A11,FINSEQ_3:27; hence g/.z <> f/.1 by A10,A16,A17,GOBOARD7:39; end; Rev f = Rev Rotate(g,f/.1) by A4,Th16 .= Rotate(h,f/.1) by A5,FINSEQ_6:112; hence f is clockwise_oriented or Rev f is clockwise_oriented; end; end;