:: REVROT_1 semantic presentation begin definition let D be non empty set ; let f be FinSequence of D; :: original: constant redefine attrf is constant means :Def1: :: REVROT_1:def 1 for n, m being Element of NAT st n in dom f & m in dom f holds f /. n = f /. m; compatibility ( f is constant iff for n, m being Element of NAT st n in dom f & m in dom f holds f /. n = f /. m ) proof hereby ::_thesis: ( ( for n, m being Element of NAT st n in dom f & m in dom f holds f /. n = f /. m ) implies f is constant ) assume A1: f is constant ; ::_thesis: for n, m being Element of NAT st n in dom f & m in dom f holds f /. n = f /. m let n, m be Element of NAT ; ::_thesis: ( n in dom f & m in dom f implies f /. n = f /. m ) assume that A2: n in dom f and A3: m in dom f ; ::_thesis: f /. n = f /. m thus f /. n = f . n by A2, PARTFUN1:def_6 .= f . m by A1, A2, A3, SEQM_3:def_10 .= f /. m by A3, PARTFUN1:def_6 ; ::_thesis: verum end; assume A4: for n, m being Element of NAT st n in dom f & m in dom f holds f /. n = f /. m ; ::_thesis: f is constant let n be Element of NAT ; :: according to SEQM_3:def_10 ::_thesis: for b1 being Element of NAT holds ( not n in dom f or not b1 in dom f or f . n = f . b1 ) let m be Element of NAT ; ::_thesis: ( not n in dom f or not m in dom f or f . n = f . m ) assume that A5: n in dom f and A6: m in dom f ; ::_thesis: f . n = f . m thus f . n = f /. n by A5, PARTFUN1:def_6 .= f /. m by A4, A5, A6 .= f . m by A6, PARTFUN1:def_6 ; ::_thesis: verum end; end; :: deftheorem Def1 defines constant REVROT_1:def_1_:_ for D being non empty set for f being FinSequence of D holds ( f is constant iff for n, m being Element of NAT st n in dom f & m in dom f holds f /. n = f /. m ); theorem Th1: :: REVROT_1:1 for D being non empty set for 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 ; ::_thesis: for f being FinSequence of D st f just_once_values f /. (len f) holds (f /. (len f)) .. f = len f let f be FinSequence of D; ::_thesis: ( f just_once_values f /. (len f) implies (f /. (len f)) .. f = len f ) assume A1: f just_once_values f /. (len f) ; ::_thesis: (f /. (len f)) .. f = len f then reconsider f9 = f as non empty FinSequence of D by FINSEQ_4:5, RELAT_1:38; ((f /. (len f)) .. f) + 1 = ((f /. (len f)) .. f) + (((Rev f9) /. 1) .. (Rev f9)) by FINSEQ_6:43 .= ((f /. (len f)) .. f) + ((f /. (len f)) .. (Rev f)) by FINSEQ_5:65 .= (len f) + 1 by A1, FINSEQ_6:37 ; hence (f /. (len f)) .. f = len f ; ::_thesis: verum end; theorem :: REVROT_1:2 for D being non empty set for f being FinSequence of D holds f /^ (len f) = {} by RFINSEQ:27; theorem Th3: :: REVROT_1:3 for D being non empty set for f being non empty FinSequence of D holds f /. (len f) in rng f proof let D be non empty set ; ::_thesis: for f being non empty FinSequence of D holds f /. (len f) in rng f let f be non empty FinSequence of D; ::_thesis: f /. (len f) in rng f len f in dom f by FINSEQ_5:6; hence f /. (len f) in rng f by PARTFUN2:2; ::_thesis: verum end; definition let D be non empty set ; let f be FinSequence of D; let y be set ; :: original: just_once_values redefine predf just_once_values y means :: REVROT_1:def 2 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 ( f just_once_values y iff 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 ) ) ) proof hereby ::_thesis: ( 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 ) ) implies f just_once_values y ) assume f just_once_values y ; ::_thesis: 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 ) ) 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:7; take x = x; ::_thesis: ( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds f /. z <> y ) ) thus x in dom f by A1; ::_thesis: ( y = f /. x & ( for z being set st z in dom f & z <> x holds f /. z <> y ) ) thus y = f /. x by A1, A2, PARTFUN1:def_6; ::_thesis: for z being set st z in dom f & z <> x holds f /. z <> y let z be set ; ::_thesis: ( z in dom f & z <> x implies f /. z <> y ) assume that A4: z in dom f and A5: z <> x ; ::_thesis: f /. z <> y f . z <> y by A3, A4, A5; hence f /. z <> y by A4, PARTFUN1:def_6; ::_thesis: verum end; given x being set such that A6: x in dom f and A7: y = f /. x and A8: for z being set st z in dom f & z <> x holds f /. z <> y ; ::_thesis: f just_once_values y A9: for z being set st z in dom f & z <> x holds f . z <> y proof let z be set ; ::_thesis: ( z in dom f & z <> x implies f . z <> y ) assume that A10: z in dom f and A11: z <> x ; ::_thesis: f . z <> y f /. z <> y by A8, A10, A11; hence f . z <> y by A10, PARTFUN1:def_6; ::_thesis: verum end; y = f . x by A6, A7, PARTFUN1:def_6; hence f just_once_values y by A6, A9, FINSEQ_4:7; ::_thesis: verum end; end; :: deftheorem defines just_once_values REVROT_1:def_2_:_ for D being non empty set for f being FinSequence of D for y being set holds ( f just_once_values y iff 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 ) ) ); theorem Th4: :: REVROT_1:4 for D being non empty set for 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 ; ::_thesis: for f being FinSequence of D st f just_once_values f /. (len f) holds f -: (f /. (len f)) = f let f be FinSequence of D; ::_thesis: ( f just_once_values f /. (len f) implies f -: (f /. (len f)) = f ) assume A1: f just_once_values f /. (len f) ; ::_thesis: f -: (f /. (len f)) = f thus f -: (f /. (len f)) = f | ((f /. (len f)) .. f) by FINSEQ_5:def_1 .= f | (len f) by A1, Th1 .= f by FINSEQ_1:58 ; ::_thesis: verum end; theorem Th5: :: REVROT_1:5 for D being non empty set for 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 ; ::_thesis: for f being FinSequence of D st f just_once_values f /. (len f) holds f :- (f /. (len f)) = <*(f /. (len f))*> let f be FinSequence of D; ::_thesis: ( f just_once_values f /. (len f) implies f :- (f /. (len f)) = <*(f /. (len f))*> ) assume A1: f just_once_values f /. (len f) ; ::_thesis: f :- (f /. (len f)) = <*(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 RFINSEQ:27 .= <*(f /. (len f))*> by FINSEQ_1:34 ; ::_thesis: verum end; theorem Th6: :: REVROT_1:6 for D being non empty set for p being Element of D for f being FinSequence of D holds 1 <= len (f :- p) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds 1 <= len (f :- p) let p be Element of D; ::_thesis: for f being FinSequence of D holds 1 <= len (f :- p) let f be FinSequence of D; ::_thesis: 1 <= len (f :- p) len (f :- p) = len (<*p*> ^ (f /^ (p .. f))) by FINSEQ_5:def_2 .= (len <*p*>) + (len (f /^ (p .. f))) by FINSEQ_1:22 .= 1 + (len (f /^ (p .. f))) by FINSEQ_1:39 ; hence 1 <= len (f :- p) by NAT_1:11; ::_thesis: verum end; theorem :: REVROT_1:7 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds len (f :- p) <= len f proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds len (f :- p) <= len f let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds len (f :- p) <= len f let f be FinSequence of D; ::_thesis: ( p in rng f implies len (f :- p) <= len f ) assume A1: p in rng f ; ::_thesis: len (f :- p) <= len f then 1 <= p .. f by FINSEQ_4:21; then A2: (len f) - 1 >= (len f) - (p .. f) by XREAL_1:10; len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50; then (len (f :- p)) - 1 = (len f) - (p .. f) ; hence len (f :- p) <= len f by A2, XREAL_1:9; ::_thesis: verum end; theorem :: REVROT_1:8 for D being non empty set for f being non empty circular FinSequence of D holds Rev f is circular proof let D be non empty set ; ::_thesis: for f being non empty circular FinSequence of D holds Rev f is circular let f be non empty circular FinSequence of D; ::_thesis: Rev f is circular thus (Rev f) /. 1 = f /. (len f) by FINSEQ_5:65 .= f /. 1 by FINSEQ_6:def_1 .= (Rev f) /. (len f) by FINSEQ_5:65 .= (Rev f) /. (len (Rev f)) by FINSEQ_5:def_3 ; :: according to FINSEQ_6:def_1 ::_thesis: verum end; begin theorem Th9: :: REVROT_1:9 for i being Element of NAT for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & 1 <= i & i <= len (f :- p) holds (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) proof let i be Element of NAT ; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & 1 <= i & i <= len (f :- p) holds (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & 1 <= i & i <= len (f :- p) holds (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & 1 <= i & i <= len (f :- p) holds (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) let f be FinSequence of D; ::_thesis: ( p in rng f & 1 <= i & i <= len (f :- p) implies (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) ) assume that A1: p in rng f and A2: 1 <= i and A3: i <= len (f :- p) ; ::_thesis: (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) A4: i in dom (f :- p) by A2, A3, FINSEQ_3:25; A5: i = (i -' 1) + 1 by A2, XREAL_1:235; Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A1, FINSEQ_6:def_2; hence (Rotate (f,p)) /. i = (f :- p) /. i by A4, FINSEQ_4:68 .= f /. ((i -' 1) + (p .. f)) by A1, A5, A4, FINSEQ_5:52 ; ::_thesis: verum end; theorem Th10: :: REVROT_1:10 for i being Element of NAT for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f <= i & i <= len f holds f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) proof let i be Element of NAT ; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f <= i & i <= len f holds f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & p .. f <= i & i <= len f holds f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & p .. f <= i & i <= len f holds f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) let f be FinSequence of D; ::_thesis: ( p in rng f & p .. f <= i & i <= len f implies f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) ) assume that A1: p in rng f and A2: p .. f <= i and A3: i <= len f ; ::_thesis: f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) A4: 1 + (p .. f) <= i + 1 by A2, XREAL_1:6; i + 1 <= (len f) + 1 by A3, XREAL_1:6; then ( i <= i + 1 & (i + 1) - (p .. f) <= ((len f) + 1) - (p .. f) ) by NAT_1:11, XREAL_1:9; then (i + 1) -' (p .. f) <= ((len f) - (p .. f)) + 1 by A2, XREAL_1:233, XXREAL_0:2; then A5: (i + 1) -' (p .. f) <= len (f :- p) by A1, FINSEQ_5:50; (((i + 1) -' (p .. f)) -' 1) + (p .. f) = (((i -' (p .. f)) + 1) -' 1) + (p .. f) by A2, NAT_D:38 .= (i -' (p .. f)) + (p .. f) by NAT_D:34 .= i by A2, XREAL_1:235 ; hence f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) by A1, A4, A5, Th9, NAT_D:55; ::_thesis: verum end; theorem Th11: :: REVROT_1:11 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds (Rotate (f,p)) /. (len (f :- p)) = f /. (len f) proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f holds (Rotate (f,p)) /. (len (f :- p)) = f /. (len f) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f holds (Rotate (f,p)) /. (len (f :- p)) = f /. (len f) let f be FinSequence of D; ::_thesis: ( p in rng f implies (Rotate (f,p)) /. (len (f :- p)) = f /. (len f) ) A1: 1 <= len (f :- p) by Th6; assume A2: p in rng f ; ::_thesis: (Rotate (f,p)) /. (len (f :- p)) = f /. (len f) then p .. f <= len f by FINSEQ_4:21; then reconsider x = (len f) - (p .. f) as Element of NAT by INT_1:5; ((len (f :- p)) -' 1) + (p .. f) = ((x + 1) -' 1) + (p .. f) by A2, FINSEQ_5:50 .= ((len f) - (p .. f)) + (p .. f) by NAT_D:34 .= len f ; hence (Rotate (f,p)) /. (len (f :- p)) = f /. (len f) by A1, A2, Th9; ::_thesis: verum end; theorem Th12: :: REVROT_1:12 for i being Element of NAT for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) proof let i be Element of NAT ; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) let f be FinSequence of D; ::_thesis: ( p in rng f & len (f :- p) < i & i <= len f implies (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) ) assume that A1: p in rng f and A2: len (f :- p) < i and A3: i <= len f ; ::_thesis: (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) A4: len (f -: p) = p .. f by A1, FINSEQ_5:42; A5: ( (i -' (len (f :- p))) + (len (f :- p)) = i & Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) ) by A1, A2, FINSEQ_6:def_2, XREAL_1:235; not f -: p is empty by A1, FINSEQ_5:47; then len (f -: p) >= 1 by NAT_1:14; then A6: len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def_1; i + (p .. f) <= (p .. f) + (len f) by A3, XREAL_1:6; then A7: (i + (p .. f)) -' (len f) <= p .. f by NAT_D:53; A8: p .. f <= len f by A1, FINSEQ_4:21; then (len f) - (p .. f) = (len f) -' (p .. f) by XREAL_1:233; then A9: len (f :- p) = ((len f) -' (p .. f)) + 1 by A1, FINSEQ_5:50; then A10: (len f) -' (p .. f) < i by A2, NAT_1:13; then A11: len f < i + (p .. f) by NAT_D:55; then (len f) + 1 <= i + (p .. f) by NAT_1:13; then 1 <= (i + (p .. f)) -' (len f) by NAT_D:55; then A12: (i + (p .. f)) -' (len f) in Seg (p .. f) by A7, FINSEQ_1:1; i <= (p .. f) + ((len f) -' (p .. f)) by A3, A8, XREAL_1:235; then i -' ((len f) -' (p .. f)) <= p .. f by NAT_D:53; then (i -' (((len f) -' (p .. f)) + 1)) + 1 <= p .. f by A10, NAT_2:7; then A13: i -' (len (f :- p)) <= (len (f -: p)) - 1 by A9, A4, XREAL_1:19; (((len f) -' (p .. f)) + 1) + 1 <= i by A2, A9, NAT_1:13; then A14: 1 <= i -' (((len f) -' (p .. f)) + 1) by NAT_D:55; then A15: i -' (((len f) -' (p .. f)) + 1) in dom ((f -: p) /^ 1) by A9, A6, A13, FINSEQ_3:25; (len f) - (p .. f) = (len f) -' (p .. f) by A8, XREAL_1:233; then 1 <= i -' (len (f :- p)) by A1, A14, FINSEQ_5:50; then i -' (len (f :- p)) in dom ((f -: p) /^ 1) by A6, A13, FINSEQ_3:25; hence (Rotate (f,p)) /. i = ((f -: p) /^ 1) /. (i -' (((len f) -' (p .. f)) + 1)) by A9, A5, FINSEQ_4:69 .= (f -: p) /. ((i -' (((len f) -' (p .. f)) + 1)) + 1) by A15, FINSEQ_5:27 .= (f -: p) /. (i -' ((len f) -' (p .. f))) by A10, NAT_2:7 .= (f -: p) /. (i - ((len f) -' (p .. f))) by A10, XREAL_1:233 .= (f -: p) /. (i - ((len f) - (p .. f))) by A8, XREAL_1:233 .= (f -: p) /. ((i + (p .. f)) - (len f)) .= (f -: p) /. ((i + (p .. f)) -' (len f)) by A11, XREAL_1:233 .= f /. ((i + (p .. f)) -' (len f)) by A1, A12, FINSEQ_5:43 ; ::_thesis: verum end; theorem :: REVROT_1:13 for i being Element of NAT for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & 1 < i & i <= p .. f holds f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) proof let i be Element of NAT ; ::_thesis: for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & 1 < i & i <= p .. f holds f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D st p in rng f & 1 < i & i <= p .. f holds f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) let p be Element of D; ::_thesis: for f being FinSequence of D st p in rng f & 1 < i & i <= p .. f holds f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) let f be FinSequence of D; ::_thesis: ( p in rng f & 1 < i & i <= p .. f implies f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) ) assume that A1: p in rng f and A2: 1 < i and A3: i <= p .. f ; ::_thesis: f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) A4: (len f) -' (p .. f) <= (len f) -' i by A3, NAT_D:41; A5: p .. f <= len f by A1, FINSEQ_4:21; then i <= len f by A3, XXREAL_0:2; then ((len f) -' (p .. f)) + i <= len f by A4, NAT_D:54; then A6: (i + (len f)) -' (p .. f) <= len f by A5, NAT_D:38; (len f) + 1 < i + (len f) by A2, XREAL_1:6; then ((len f) + 1) - (p .. f) < (i + (len f)) - (p .. f) by XREAL_1:9; then ((len f) - (p .. f)) + 1 < i + ((len f) - (p .. f)) ; then ((len f) - (p .. f)) + 1 < i + ((len f) -' (p .. f)) by A5, XREAL_1:233; then ((len f) - (p .. f)) + 1 < (i + (len f)) -' (p .. f) by A5, NAT_D:38; then A7: len (f :- p) < (i + (len f)) -' (p .. f) by A1, FINSEQ_5:50; len f <= i + (len f) by NAT_1:11; then (((i + (len f)) -' (p .. f)) + (p .. f)) -' (len f) = (i + (len f)) -' (len f) by A5, XREAL_1:235, XXREAL_0:2 .= i by NAT_D:34 ; hence f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) by A1, A7, A6, Th12; ::_thesis: verum end; theorem Th14: :: REVROT_1:14 for D being non empty set for p being Element of D for f being FinSequence of D holds len (Rotate (f,p)) = len f proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds len (Rotate (f,p)) = len f let p be Element of D; ::_thesis: for f being FinSequence of D holds len (Rotate (f,p)) = len f let f be FinSequence of D; ::_thesis: len (Rotate (f,p)) = len f percases ( not p in rng f or p in rng f ) ; suppose not p in rng f ; ::_thesis: len (Rotate (f,p)) = len f hence len (Rotate (f,p)) = len f by FINSEQ_6:def_2; ::_thesis: verum end; supposeA1: p in rng f ; ::_thesis: len (Rotate (f,p)) = len f then f -: p <> {} by FINSEQ_5:47; then A2: 1 <= len (f -: p) by NAT_1:14; 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:22 .= (len (f :- p)) + ((len (f -: p)) - 1) by A2, RFINSEQ:def_1 .= ((len (f :- p)) + (len (f -: p))) - 1 .= ((((len f) - (p .. f)) + 1) + (len (f -: p))) - 1 by A1, FINSEQ_5:50 .= ((len f) - (p .. f)) + (len (f -: p)) .= ((len f) - (p .. f)) + (p .. f) by A1, FINSEQ_5:42 .= len f ; ::_thesis: verum end; end; end; theorem Th15: :: REVROT_1:15 for D being non empty set for p being Element of D for f being FinSequence of D holds dom (Rotate (f,p)) = dom f proof let D be non empty set ; ::_thesis: for p being Element of D for f being FinSequence of D holds dom (Rotate (f,p)) = dom f let p be Element of D; ::_thesis: for f being FinSequence of D holds dom (Rotate (f,p)) = dom f let f be FinSequence of D; ::_thesis: dom (Rotate (f,p)) = dom f len (Rotate (f,p)) = len f by Th14; hence dom (Rotate (f,p)) = dom f by FINSEQ_3:29; ::_thesis: verum end; theorem Th16: :: REVROT_1:16 for D being non empty set for f being circular FinSequence of D for p being Element of D st ( for i being Element of NAT 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 ; ::_thesis: for f being circular FinSequence of D for p being Element of D st ( for i being Element of NAT st 1 < i & i < len f holds f /. i <> f /. 1 ) holds Rotate ((Rotate (f,p)),(f /. 1)) = f let f be circular FinSequence of D; ::_thesis: for p being Element of D st ( for i being Element of NAT st 1 < i & i < len f holds f /. i <> f /. 1 ) holds Rotate ((Rotate (f,p)),(f /. 1)) = f let p be Element of D; ::_thesis: ( ( for i being Element of NAT st 1 < i & i < len f holds f /. i <> f /. 1 ) implies Rotate ((Rotate (f,p)),(f /. 1)) = f ) assume A1: for i being Element of NAT st 1 < i & i < len f holds f /. i <> f /. 1 ; ::_thesis: Rotate ((Rotate (f,p)),(f /. 1)) = f percases ( not p in rng f or p = f /. 1 or ( p in rng f & p <> f /. 1 ) ) ; suppose not p in rng f ; ::_thesis: Rotate ((Rotate (f,p)),(f /. 1)) = f hence Rotate ((Rotate (f,p)),(f /. 1)) = Rotate (f,(f /. 1)) by FINSEQ_6:def_2 .= f by FINSEQ_6:89 ; ::_thesis: verum end; suppose p = f /. 1 ; ::_thesis: Rotate ((Rotate (f,p)),(f /. 1)) = f hence Rotate ((Rotate (f,p)),(f /. 1)) = Rotate (f,(f /. 1)) by FINSEQ_6:93 .= f by FINSEQ_6:89 ; ::_thesis: verum end; supposethat A2: p in rng f and A3: p <> f /. 1 ; ::_thesis: Rotate ((Rotate (f,p)),(f /. 1)) = f A4: f /. 1 = (f -: p) /. 1 by A2, FINSEQ_5:44; A5: f /. 1 = f /. (len f) by FINSEQ_6:def_1; then A6: f /. 1 = (f :- p) /. (len (f :- p)) by A2, FINSEQ_5:54; then A7: f /. 1 in rng (f :- p) by Th3; A8: f :- p just_once_values f /. 1 proof ( p .. f <> 1 & p .. f >= 1 ) by A2, A3, FINSEQ_4:21, FINSEQ_5:38; then A9: p .. f > 1 by XXREAL_0:1; take len (f :- p) ; :: according to REVROT_1:def_2 ::_thesis: ( len (f :- p) in dom (f :- p) & f /. 1 = (f :- p) /. (len (f :- p)) & ( for z being set st z in dom (f :- p) & z <> len (f :- p) holds (f :- p) /. z <> f /. 1 ) ) thus len (f :- p) in dom (f :- p) by FINSEQ_5:6; ::_thesis: ( f /. 1 = (f :- p) /. (len (f :- p)) & ( for z being set st z in dom (f :- p) & z <> len (f :- p) holds (f :- p) /. z <> f /. 1 ) ) thus f /. 1 = (f :- p) /. (len (f :- p)) by A2, A5, FINSEQ_5:54; ::_thesis: for z being set st z in dom (f :- p) & z <> len (f :- p) holds (f :- p) /. z <> f /. 1 let z be set ; ::_thesis: ( z in dom (f :- p) & z <> len (f :- p) implies (f :- p) /. z <> f /. 1 ) assume A10: z in dom (f :- p) ; ::_thesis: ( not z <> len (f :- p) or (f :- p) /. z <> f /. 1 ) then reconsider k = z as Element of NAT ; k <> 0 by A10, FINSEQ_3:25; then consider i being Nat such that A11: k = i + 1 by NAT_1:6; assume A12: z <> len (f :- p) ; ::_thesis: (f :- p) /. z <> f /. 1 reconsider i = i as Element of NAT by ORDINAL1:def_12; k <= len (f :- p) by A10, FINSEQ_3:25; then k < len (f :- p) by A12, XXREAL_0:1; then i + 1 < ((len f) - (p .. f)) + 1 by A2, A11, FINSEQ_5:50; then i < (len f) - (p .. f) by XREAL_1:6; then A13: i + (p .. f) < len f by XREAL_1:20; p .. f <= i + (p .. f) by NAT_1:11; then A14: 1 < i + (p .. f) by A9, XXREAL_0:2; (f :- p) /. (i + 1) = f /. (i + (p .. f)) by A2, A10, A11, FINSEQ_5:52; hence (f :- p) /. z <> f /. 1 by A1, A11, A14, A13; ::_thesis: verum end; f /. 1 in rng f by A2, FINSEQ_6:42, RELAT_1:38; then A15: f /. 1 in rng (Rotate (f,p)) by A2, FINSEQ_6:90; Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A2, FINSEQ_6:def_2; hence Rotate ((Rotate (f,p)),(f /. 1)) = (((f :- p) ^ ((f -: p) /^ 1)) :- (f /. 1)) ^ ((((f :- p) ^ ((f -: p) /^ 1)) -: (f /. 1)) /^ 1) by A15, FINSEQ_6:def_2 .= (((f :- p) :- (f /. 1)) ^ ((f -: p) /^ 1)) ^ ((((f :- p) ^ ((f -: p) /^ 1)) -: (f /. 1)) /^ 1) by A7, FINSEQ_6:64 .= (((f :- p) :- (f /. 1)) ^ ((f -: p) /^ 1)) ^ (((f :- p) -: (f /. 1)) /^ 1) by A7, FINSEQ_6:66 .= (<*(f /. 1)*> ^ ((f -: p) /^ 1)) ^ (((f :- p) -: (f /. 1)) /^ 1) by A6, A8, Th5 .= (f -: p) ^ (((f :- p) -: (f /. 1)) /^ 1) by A2, A4, FINSEQ_5:29, FINSEQ_5:47 .= (f -: p) ^ ((f :- p) /^ 1) by A6, A8, Th4 .= f by A2, FINSEQ_6:76 ; ::_thesis: verum end; end; end; begin theorem Th17: :: REVROT_1:17 for i being Element of NAT for D being non empty set for p being Element of D for f being circular FinSequence of D st p in rng f & len (f :- p) <= i & i <= len f holds (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) proof let i be Element of NAT ; ::_thesis: for D being non empty set for p being Element of D for f being circular FinSequence of D st p in rng f & len (f :- p) <= i & i <= len f holds (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) let D be non empty set ; ::_thesis: for p being Element of D for f being circular FinSequence of D st p in rng f & len (f :- p) <= i & i <= len f holds (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) let p be Element of D; ::_thesis: for f being circular FinSequence of D st p in rng f & len (f :- p) <= i & i <= len f holds (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) let f be circular FinSequence of D; ::_thesis: ( p in rng f & len (f :- p) <= i & i <= len f implies (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) ) assume that A1: p in rng f and A2: len (f :- p) <= i and A3: i <= len f ; ::_thesis: (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) A4: p .. f <= len f by A1, FINSEQ_4:21; then A5: (len f) - (p .. f) = (len f) -' (p .. f) by XREAL_1:233; percases ( i = len (f :- p) or i > len (f :- p) ) by A2, XXREAL_0:1; supposeA6: i = len (f :- p) ; ::_thesis: (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) then A7: i = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50; then i >= 1 by A5, NAT_1:11; hence (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) by A1, A6, Th9 .= f /. (((len f) -' (p .. f)) + (p .. f)) by A5, A7, NAT_D:34 .= f /. (len f) by A4, XREAL_1:235 .= f /. 1 by FINSEQ_6:def_1 .= f /. (((len f) + 1) -' (len f)) by NAT_D:34 .= f /. ((i + (p .. f)) -' (len f)) by A7 ; ::_thesis: verum end; suppose i > len (f :- p) ; ::_thesis: (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) hence (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) by A1, A3, Th12; ::_thesis: verum end; end; end; theorem Th18: :: REVROT_1:18 for i being Element of NAT for D being non empty set for p being Element of D for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) proof let i be Element of NAT ; ::_thesis: for D being non empty set for p being Element of D for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) let D be non empty set ; ::_thesis: for p being Element of D for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) let p be Element of D; ::_thesis: for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) let f be circular FinSequence of D; ::_thesis: ( p in rng f & 1 <= i & i <= p .. f implies f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) ) assume that A1: p in rng f and A2: 1 <= i and A3: i <= p .. f ; ::_thesis: f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) A4: (len f) -' (p .. f) <= (len f) -' i by A3, NAT_D:41; A5: p .. f <= len f by A1, FINSEQ_4:21; then i <= len f by A3, XXREAL_0:2; then ((len f) -' (p .. f)) + i <= len f by A4, NAT_D:54; then A6: (i + (len f)) -' (p .. f) <= len f by A5, NAT_D:38; (len f) + 1 <= i + (len f) by A2, XREAL_1:6; then ((len f) + 1) - (p .. f) <= (i + (len f)) - (p .. f) by XREAL_1:9; then ((len f) - (p .. f)) + 1 <= i + ((len f) - (p .. f)) ; then ((len f) - (p .. f)) + 1 <= i + ((len f) -' (p .. f)) by A5, XREAL_1:233; then ((len f) - (p .. f)) + 1 <= (i + (len f)) -' (p .. f) by A5, NAT_D:38; then A7: len (f :- p) <= (i + (len f)) -' (p .. f) by A1, FINSEQ_5:50; len f <= i + (len f) by NAT_1:11; then (((i + (len f)) -' (p .. f)) + (p .. f)) -' (len f) = (i + (len f)) -' (len f) by A5, XREAL_1:235, XXREAL_0:2 .= i by NAT_D:34 ; hence f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) by A1, A7, A6, Th17; ::_thesis: verum end; registration let D be non trivial set ; clusterV1() V4( NAT ) V5(D) Function-like V8() V30() FinSequence-like FinSubsequence-like circular for FinSequence of D; existence ex b1 being FinSequence of D st ( b1 is V8() & b1 is circular ) proof consider d1, d2 being Element of D such that A1: d1 <> d2 by SUBSET_1:def_7; take f = <*d1,d2,d1*>; ::_thesis: ( f is V8() & f is circular ) A2: ( f . 1 = d1 & f . 2 = d2 ) by FINSEQ_1:45; ( 1 in dom f & 2 in dom f ) by TOPREAL3:1; hence f is V8() by A1, A2, SEQM_3:def_10; ::_thesis: f is circular A3: len f = 3 by FINSEQ_1:45; thus f /. 1 = d1 by FINSEQ_4:18 .= f /. (len f) by A3, FINSEQ_4:18 ; :: according to FINSEQ_6:def_1 ::_thesis: verum end; end; registration let D be non trivial set ; let p be Element of D; let f be V8() circular FinSequence of D; cluster Rotate (f,p) -> V8() ; coherence not Rotate (f,p) is constant proof percases ( not p in rng f or p in rng f ) ; suppose not p in rng f ; ::_thesis: not Rotate (f,p) is constant hence not Rotate (f,p) is constant by FINSEQ_6:def_2; ::_thesis: verum end; supposeA1: p in rng f ; ::_thesis: not Rotate (f,p) is constant A2: dom (Rotate (f,p)) = dom f by Th15; consider n, m being Element of NAT such that A3: n in dom f and A4: m in dom f and A5: f /. n <> f /. m by Def1; A6: n <= len f by A3, FINSEQ_3:25; A7: m <= len f by A4, FINSEQ_3:25; A8: 1 <= m by A4, FINSEQ_3:25; A9: 1 <= n by A3, FINSEQ_3:25; thus Rotate (f,p) is V8() ::_thesis: verum proof A10: 1 <= p .. f by A1, FINSEQ_4:21; A11: p .. f <= len f by A1, FINSEQ_4:21; percases ( ( n <= p .. f & m <= p .. f ) or ( n <= p .. f & m >= p .. f ) or ( m <= p .. f & n >= p .. f ) or ( m >= p .. f & n >= p .. f ) ) ; supposethat A12: n <= p .. f and A13: m <= p .. f ; ::_thesis: Rotate (f,p) is V8() n <= n + ((len f) -' (p .. f)) by NAT_1:11; then 1 <= n + ((len f) -' (p .. f)) by A9, XXREAL_0:2; then A14: 1 <= (n + (len f)) -' (p .. f) by A11, NAT_D:38; m <= m + ((len f) -' (p .. f)) by NAT_1:11; then 1 <= m + ((len f) -' (p .. f)) by A8, XXREAL_0:2; then A15: 1 <= (m + (len f)) -' (p .. f) by A11, NAT_D:38; m + (len f) <= (len f) + (p .. f) by A13, XREAL_1:6; then (m + (len f)) -' (p .. f) <= len f by NAT_D:53; then A16: (m + (len f)) -' (p .. f) in dom f by A15, FINSEQ_3:25; n + (len f) <= (len f) + (p .. f) by A12, XREAL_1:6; then (n + (len f)) -' (p .. f) <= len f by NAT_D:53; then A17: (n + (len f)) -' (p .. f) in dom f by A14, FINSEQ_3:25; ( f /. n = (Rotate (f,p)) /. ((n + (len f)) -' (p .. f)) & f /. m = (Rotate (f,p)) /. ((m + (len f)) -' (p .. f)) ) by A1, A9, A8, A12, A13, Th18; hence Rotate (f,p) is V8() by A5, A2, A17, A16, Def1; ::_thesis: verum end; supposethat A18: n <= p .. f and A19: m >= p .. f ; ::_thesis: Rotate (f,p) is V8() 1 + (p .. f) <= m + 1 by A19, XREAL_1:6; then A20: 1 <= (m + 1) -' (p .. f) by NAT_D:55; n <= n + ((len f) -' (p .. f)) by NAT_1:11; then 1 <= n + ((len f) -' (p .. f)) by A9, XXREAL_0:2; then A21: 1 <= (n + (len f)) -' (p .. f) by A11, NAT_D:38; n + (len f) <= (len f) + (p .. f) by A18, XREAL_1:6; then (n + (len f)) -' (p .. f) <= len f by NAT_D:53; then A22: (n + (len f)) -' (p .. f) in dom f by A21, FINSEQ_3:25; m + 1 <= (len f) + (p .. f) by A7, A10, XREAL_1:7; then (m + 1) -' (p .. f) <= len f by NAT_D:53; then A23: (m + 1) -' (p .. f) in dom f by A20, FINSEQ_3:25; ( f /. n = (Rotate (f,p)) /. ((n + (len f)) -' (p .. f)) & f /. m = (Rotate (f,p)) /. ((m + 1) -' (p .. f)) ) by A1, A9, A7, A18, A19, Th10, Th18; hence Rotate (f,p) is V8() by A5, A2, A22, A23, Def1; ::_thesis: verum end; supposethat A24: m <= p .. f and A25: n >= p .. f ; ::_thesis: Rotate (f,p) is V8() 1 + (p .. f) <= n + 1 by A25, XREAL_1:6; then A26: 1 <= (n + 1) -' (p .. f) by NAT_D:55; m <= m + ((len f) -' (p .. f)) by NAT_1:11; then 1 <= m + ((len f) -' (p .. f)) by A8, XXREAL_0:2; then A27: 1 <= (m + (len f)) -' (p .. f) by A11, NAT_D:38; m + (len f) <= (len f) + (p .. f) by A24, XREAL_1:6; then (m + (len f)) -' (p .. f) <= len f by NAT_D:53; then A28: (m + (len f)) -' (p .. f) in dom f by A27, FINSEQ_3:25; n + 1 <= (len f) + (p .. f) by A6, A10, XREAL_1:7; then (n + 1) -' (p .. f) <= len f by NAT_D:53; then A29: (n + 1) -' (p .. f) in dom f by A26, FINSEQ_3:25; ( f /. m = (Rotate (f,p)) /. ((m + (len f)) -' (p .. f)) & f /. n = (Rotate (f,p)) /. ((n + 1) -' (p .. f)) ) by A1, A6, A8, A24, A25, Th10, Th18; hence Rotate (f,p) is V8() by A5, A2, A28, A29, Def1; ::_thesis: verum end; supposethat A30: m >= p .. f and A31: n >= p .. f ; ::_thesis: Rotate (f,p) is V8() 1 + (p .. f) <= m + 1 by A30, XREAL_1:6; then A32: 1 <= (m + 1) -' (p .. f) by NAT_D:55; 1 + (p .. f) <= n + 1 by A31, XREAL_1:6; then A33: 1 <= (n + 1) -' (p .. f) by NAT_D:55; n + 1 <= (len f) + (p .. f) by A6, A10, XREAL_1:7; then (n + 1) -' (p .. f) <= len f by NAT_D:53; then A34: (n + 1) -' (p .. f) in dom f by A33, FINSEQ_3:25; m + 1 <= (len f) + (p .. f) by A7, A10, XREAL_1:7; then (m + 1) -' (p .. f) <= len f by NAT_D:53; then A35: (m + 1) -' (p .. f) in dom f by A32, FINSEQ_3:25; ( f /. m = (Rotate (f,p)) /. ((m + 1) -' (p .. f)) & f /. n = (Rotate (f,p)) /. ((n + 1) -' (p .. f)) ) by A1, A6, A7, A30, A31, Th10; hence Rotate (f,p) is V8() by A5, A2, A35, A34, Def1; ::_thesis: verum end; end; end; end; end; end; end; begin theorem Th19: :: REVROT_1:19 for n being non zero Nat holds 0.REAL n <> 1.REAL n proof let n be non zero Nat; ::_thesis: 0.REAL n <> 1.REAL n 1 <= n by NAT_1:14; then 1 in Seg n by FINSEQ_1:1; then A1: ( (n |-> 0) . 1 = 0 & (n |-> 1) . 1 = 1 ) by FINSEQ_2:57; 1.REAL n = 1* n by EUCLID:def_12 .= n |-> 1 by EUCLID:def_11 ; hence 0.REAL n <> 1.REAL n by A1, EUCLID:def_4; ::_thesis: verum end; registration let n be non zero Nat; cluster TOP-REAL n -> non trivial ; coherence not TOP-REAL n is trivial proof reconsider 1R = 1.REAL n as Element of (TOP-REAL n) ; take 1R ; :: according to STRUCT_0:def_18 ::_thesis: not 1R = 0. (TOP-REAL n) 0.REAL n = 0. (TOP-REAL n) by EUCLID:66; hence 1R <> 0. (TOP-REAL n) by Th19; ::_thesis: verum end; end; theorem Th20: :: REVROT_1:20 for f, g being FinSequence of (TOP-REAL 2) st rng f c= rng g holds rng (X_axis f) c= rng (X_axis g) proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( rng f c= rng g implies rng (X_axis f) c= rng (X_axis g) ) assume A1: rng f c= rng g ; ::_thesis: rng (X_axis f) c= rng (X_axis g) A2: dom (X_axis g) = dom g by SPRECT_2:15; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (X_axis f) or x in rng (X_axis g) ) assume x in rng (X_axis f) ; ::_thesis: x in rng (X_axis g) then consider y being set such that A3: y in dom (X_axis f) and A4: (X_axis f) . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A3; A5: (X_axis f) . y = (f /. y) `1 by A3, GOBOARD1:def_1; dom (X_axis f) = dom f by SPRECT_2:15; then f /. y in rng f by A3, PARTFUN2:2; then consider z being set such that A6: z in dom g and A7: g . z = f /. y by A1, FUNCT_1:def_3; reconsider z = z as Element of NAT by A6; g /. z = f /. y by A6, A7, PARTFUN1:def_6; then (X_axis g) . z = (f /. y) `1 by A2, A6, GOBOARD1:def_1; hence x in rng (X_axis g) by A4, A2, A5, A6, FUNCT_1:def_3; ::_thesis: verum end; theorem Th21: :: REVROT_1:21 for f, g being FinSequence of (TOP-REAL 2) st rng f = rng g holds rng (X_axis f) = rng (X_axis g) proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( rng f = rng g implies rng (X_axis f) = rng (X_axis g) ) assume rng f = rng g ; ::_thesis: rng (X_axis f) = rng (X_axis g) hence ( rng (X_axis f) c= rng (X_axis g) & rng (X_axis g) c= rng (X_axis f) ) by Th20; :: according to XBOOLE_0:def_10 ::_thesis: verum end; theorem Th22: :: REVROT_1:22 for f, g being FinSequence of (TOP-REAL 2) st rng f c= rng g holds rng (Y_axis f) c= rng (Y_axis g) proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( rng f c= rng g implies rng (Y_axis f) c= rng (Y_axis g) ) assume A1: rng f c= rng g ; ::_thesis: rng (Y_axis f) c= rng (Y_axis g) A2: dom (Y_axis g) = dom g by SPRECT_2:16; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Y_axis f) or x in rng (Y_axis g) ) assume x in rng (Y_axis f) ; ::_thesis: x in rng (Y_axis g) then consider y being set such that A3: y in dom (Y_axis f) and A4: (Y_axis f) . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A3; A5: (Y_axis f) . y = (f /. y) `2 by A3, GOBOARD1:def_2; dom (Y_axis f) = dom f by SPRECT_2:16; then f /. y in rng f by A3, PARTFUN2:2; then consider z being set such that A6: z in dom g and A7: g . z = f /. y by A1, FUNCT_1:def_3; reconsider z = z as Element of NAT by A6; g /. z = f /. y by A6, A7, PARTFUN1:def_6; then (Y_axis g) . z = (f /. y) `2 by A2, A6, GOBOARD1:def_2; hence x in rng (Y_axis g) by A4, A2, A5, A6, FUNCT_1:def_3; ::_thesis: verum end; theorem Th23: :: REVROT_1:23 for f, g being FinSequence of (TOP-REAL 2) st rng f = rng g holds rng (Y_axis f) = rng (Y_axis g) proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( rng f = rng g implies rng (Y_axis f) = rng (Y_axis g) ) assume rng f = rng g ; ::_thesis: rng (Y_axis f) = rng (Y_axis g) hence ( rng (Y_axis f) c= rng (Y_axis g) & rng (Y_axis g) c= rng (Y_axis f) ) by Th22; :: according to XBOOLE_0:def_10 ::_thesis: verum end; begin registration let p be Point of (TOP-REAL 2); let f be circular special FinSequence of (TOP-REAL 2); cluster Rotate (f,p) -> special ; coherence Rotate (f,p) is special proof percases ( not p in rng f or p in rng f ) ; suppose not p in rng f ; ::_thesis: Rotate (f,p) is special hence Rotate (f,p) is special by FINSEQ_6:def_2; ::_thesis: verum end; supposeA1: p in rng f ; ::_thesis: Rotate (f,p) is special A2: len (Rotate (f,p)) = len f by Th14; let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (Rotate (f,p)) or ((Rotate (f,p)) /. i) `1 = ((Rotate (f,p)) /. (i + 1)) `1 or ((Rotate (f,p)) /. i) `2 = ((Rotate (f,p)) /. (i + 1)) `2 ) assume that A3: 1 <= i and A4: i + 1 <= len (Rotate (f,p)) ; ::_thesis: ( ((Rotate (f,p)) /. i) `1 = ((Rotate (f,p)) /. (i + 1)) `1 or ((Rotate (f,p)) /. i) `2 = ((Rotate (f,p)) /. (i + 1)) `2 ) A5: i + 1 >= i by NAT_1:11; A6: i in NAT by ORDINAL1:def_12; now__::_thesis:_(_((Rotate_(f,p))_/._i)_`1_=_((Rotate_(f,p))_/._(i_+_1))_`1_or_((Rotate_(f,p))_/._i)_`2_=_((Rotate_(f,p))_/._(i_+_1))_`2_) A7: len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50; percases ( i < len (f :- p) or i >= len (f :- p) ) ; supposeA8: i < len (f :- p) ; ::_thesis: ( ((Rotate (f,p)) /. i) `1 = ((Rotate (f,p)) /. (i + 1)) `1 or ((Rotate (f,p)) /. i) `2 = ((Rotate (f,p)) /. (i + 1)) `2 ) A9: ((i + 1) -' 1) + (p .. f) = i + (p .. f) by NAT_D:34 .= ((i -' 1) + 1) + (p .. f) by A3, XREAL_1:235 .= ((i -' 1) + (p .. f)) + 1 ; i + 1 <= len (f :- p) by A8, NAT_1:13; then A10: (Rotate (f,p)) /. (i + 1) = f /. (((i -' 1) + (p .. f)) + 1) by A1, A9, Th9, NAT_1:11; ( 0 <= i -' 1 & 1 <= p .. f ) by A1, FINSEQ_4:21, NAT_1:3; then A11: 1 + 0 <= (i -' 1) + (p .. f) by XREAL_1:7; i < ((len f) + 1) - (p .. f) by A7, A8; then i + (p .. f) < (len f) + 1 by XREAL_1:20; then i + (p .. f) <= len f by NAT_1:13; then A12: ((i -' 1) + 1) + (p .. f) <= len f by A3, XREAL_1:235; (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) by A1, A3, A6, A8, Th9; hence ( ((Rotate (f,p)) /. i) `1 = ((Rotate (f,p)) /. (i + 1)) `1 or ((Rotate (f,p)) /. i) `2 = ((Rotate (f,p)) /. (i + 1)) `2 ) by A10, A11, A12, TOPREAL1:def_5; ::_thesis: verum end; supposeA13: i >= len (f :- p) ; ::_thesis: ( ((Rotate (f,p)) /. i) `1 = ((Rotate (f,p)) /. (i + 1)) `1 or ((Rotate (f,p)) /. i) `2 = ((Rotate (f,p)) /. (i + 1)) `2 ) i <= len f by A4, A5, A2, XXREAL_0:2; then A14: (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) by A1, A6, A13, Th17; i - ((len f) - (p .. f)) >= 1 by A7, A13, XREAL_1:19; then (i + (p .. f)) - (len f) >= 1 ; then A15: 1 <= (i + (p .. f)) -' (len f) by NAT_D:39; A16: i + 1 >= len (f :- p) by A5, A13, XXREAL_0:2; then i >= (len f) - (p .. f) by A7, XREAL_1:6; then A17: len f <= i + (p .. f) by XREAL_1:20; ((i + 1) + (p .. f)) -' (len f) = ((i + (p .. f)) + 1) -' (len f) .= ((i + (p .. f)) -' (len f)) + 1 by A17, NAT_D:38 ; then A18: (Rotate (f,p)) /. (i + 1) = f /. (((i + (p .. f)) -' (len f)) + 1) by A1, A4, A2, A16, Th17; p .. f <= len f by A1, FINSEQ_4:21; then (i + 1) + (p .. f) <= (len f) + (len f) by A4, A2, XREAL_1:7; then ((i + (p .. f)) + 1) - (len f) <= len f by XREAL_1:20; then ((i + (p .. f)) - (len f)) + 1 <= len f ; then ((i + (p .. f)) -' (len f)) + 1 <= len f by A17, XREAL_1:233; hence ( ((Rotate (f,p)) /. i) `1 = ((Rotate (f,p)) /. (i + 1)) `1 or ((Rotate (f,p)) /. i) `2 = ((Rotate (f,p)) /. (i + 1)) `2 ) by A14, A18, A15, TOPREAL1:def_5; ::_thesis: verum end; end; end; hence ( ((Rotate (f,p)) /. i) `1 = ((Rotate (f,p)) /. (i + 1)) `1 or ((Rotate (f,p)) /. i) `2 = ((Rotate (f,p)) /. (i + 1)) `2 ) ; ::_thesis: verum end; end; end; end; theorem Th24: :: REVROT_1:24 for i being Element of NAT for p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < len (f :- p) holds LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f))) proof let i be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < len (f :- p) holds LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f))) let p be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < len (f :- p) holds LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f))) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( p in rng f & 1 <= i & i < len (f :- p) implies LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f))) ) assume that A1: p in rng f and A2: 1 <= i and A3: i < len (f :- p) ; ::_thesis: LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f))) A4: i + 1 <= len (f :- p) by A3, NAT_1:13; A5: len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50; then i - 1 < (len f) - (p .. f) by A3, XREAL_1:19; then i -' 1 < (len f) - (p .. f) by A2, XREAL_1:233; then (i -' 1) + (p .. f) < len f by XREAL_1:20; then A6: ((i -' 1) + (p .. f)) + 1 <= len f by NAT_1:13; (p .. f) - 1 >= 0 by A1, FINSEQ_4:21, XREAL_1:48; then (len f) - ((p .. f) - 1) <= len f by XREAL_1:43; then A7: i + 1 <= len f by A5, A4, XXREAL_0:2; ( i -' 1 >= 0 & 1 <= p .. f ) by A1, FINSEQ_4:21, NAT_1:2; then A8: 0 + 1 <= (i -' 1) + (p .. f) by XREAL_1:7; ((i -' 1) + (p .. f)) + 1 = ((i -' 1) + 1) + (p .. f) .= i + (p .. f) by A2, XREAL_1:235 .= ((i + 1) -' 1) + (p .. f) by NAT_D:34 ; then A9: (Rotate (f,p)) /. (i + 1) = f /. (((i -' 1) + (p .. f)) + 1) by A1, A4, Th9, NAT_1:11; A10: len (Rotate (f,p)) = len f by Th14; (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) by A1, A2, A3, Th9; hence LSeg ((Rotate (f,p)),i) = LSeg ((f /. ((i -' 1) + (p .. f))),(f /. (((i -' 1) + (p .. f)) + 1))) by A2, A10, A9, A7, TOPREAL1:def_3 .= LSeg (f,((i -' 1) + (p .. f))) by A8, A6, TOPREAL1:def_3 ; ::_thesis: verum end; theorem Th25: :: REVROT_1:25 for i being Element of NAT for p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st p in rng f & p .. f <= i & i < len f holds LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1)) proof let i be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st p in rng f & p .. f <= i & i < len f holds LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1)) let p be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st p in rng f & p .. f <= i & i < len f holds LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1)) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( p in rng f & p .. f <= i & i < len f implies LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1)) ) assume that A1: p in rng f and A2: p .. f <= i and A3: i < len f ; ::_thesis: LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1)) i - (p .. f) < (len f) - (p .. f) by A3, XREAL_1:9; then i -' (p .. f) < (len f) - (p .. f) by A2, XREAL_1:233; then (i -' (p .. f)) + 1 < ((len f) - (p .. f)) + 1 by XREAL_1:6; then A4: (i -' (p .. f)) + 1 < len (f :- p) by A1, FINSEQ_5:50; 1 + (p .. f) <= i + 1 by A2, XREAL_1:6; then 1 <= (i + 1) -' (p .. f) by NAT_D:55; then A5: 1 <= (i -' (p .. f)) + 1 by A2, NAT_D:38; (((i -' (p .. f)) + 1) -' 1) + (p .. f) = (i -' (p .. f)) + (p .. f) by NAT_D:34 .= i by A2, XREAL_1:235 ; hence LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1)) by A1, A5, A4, Th24; ::_thesis: verum end; theorem Th26: :: REVROT_1:26 for p being Point of (TOP-REAL 2) for f being circular FinSequence of (TOP-REAL 2) holds Incr (X_axis f) = Incr (X_axis (Rotate (f,p))) proof let p be Point of (TOP-REAL 2); ::_thesis: for f being circular FinSequence of (TOP-REAL 2) holds Incr (X_axis f) = Incr (X_axis (Rotate (f,p))) let f be circular FinSequence of (TOP-REAL 2); ::_thesis: Incr (X_axis f) = Incr (X_axis (Rotate (f,p))) percases ( not p in rng f or p in rng f ) ; suppose not p in rng f ; ::_thesis: Incr (X_axis f) = Incr (X_axis (Rotate (f,p))) hence Incr (X_axis f) = Incr (X_axis (Rotate (f,p))) by FINSEQ_6:def_2; ::_thesis: verum end; suppose p in rng f ; ::_thesis: Incr (X_axis f) = Incr (X_axis (Rotate (f,p))) then rng (Rotate (f,p)) = rng f by FINSEQ_6:90; 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 SEQ_4:def_21; hence Incr (X_axis f) = Incr (X_axis (Rotate (f,p))) by SEQ_4:def_21; ::_thesis: verum end; end; end; theorem Th27: :: REVROT_1:27 for p being Point of (TOP-REAL 2) for f being circular FinSequence of (TOP-REAL 2) holds Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p))) proof let p be Point of (TOP-REAL 2); ::_thesis: for f being circular FinSequence of (TOP-REAL 2) holds Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p))) let f be circular FinSequence of (TOP-REAL 2); ::_thesis: Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p))) percases ( not p in rng f or p in rng f ) ; suppose not p in rng f ; ::_thesis: Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p))) hence Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p))) by FINSEQ_6:def_2; ::_thesis: verum end; suppose p in rng f ; ::_thesis: Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p))) then rng (Rotate (f,p)) = rng f by FINSEQ_6:90; 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 SEQ_4:def_21; hence Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p))) by SEQ_4:def_21; ::_thesis: verum end; end; end; theorem Th28: :: REVROT_1:28 for p being Point of (TOP-REAL 2) for f being non empty circular FinSequence of (TOP-REAL 2) holds GoB (Rotate (f,p)) = GoB f proof let p be Point of (TOP-REAL 2); ::_thesis: for f being non empty circular FinSequence of (TOP-REAL 2) holds GoB (Rotate (f,p)) = GoB f let f be non empty circular FinSequence of (TOP-REAL 2); ::_thesis: GoB (Rotate (f,p)) = GoB f ( 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_2 .= GoB f by GOBOARD2:def_2 ; ::_thesis: verum end; theorem Th29: :: REVROT_1:29 for p being Point of (TOP-REAL 2) for f being V8() standard special_circular_sequence holds Rev (Rotate (f,p)) = Rotate ((Rev f),p) proof let p be Point of (TOP-REAL 2); ::_thesis: for f being V8() standard special_circular_sequence holds Rev (Rotate (f,p)) = Rotate ((Rev f),p) let f be V8() standard special_circular_sequence; ::_thesis: Rev (Rotate (f,p)) = Rotate ((Rev f),p) percases ( not p in rng f or p = f /. 1 or ( p in rng f & p <> f /. 1 ) ) ; suppose not p in rng f ; ::_thesis: Rev (Rotate (f,p)) = Rotate ((Rev f),p) then ( Rotate (f,p) = f & not p in rng (Rev f) ) by FINSEQ_5:57, FINSEQ_6:def_2; hence Rev (Rotate (f,p)) = Rotate ((Rev f),p) by FINSEQ_6:def_2; ::_thesis: verum end; supposeA1: p = f /. 1 ; ::_thesis: Rev (Rotate (f,p)) = Rotate ((Rev f),p) then A2: p = (Rev f) /. (len f) by FINSEQ_5:65 .= (Rev f) /. (len (Rev f)) by FINSEQ_5:def_3 .= (Rev f) /. 1 by FINSEQ_6:def_1 ; Rotate (f,p) = f by A1, FINSEQ_6:89; hence Rev (Rotate (f,p)) = Rotate ((Rev f),p) by A2, FINSEQ_6:89; ::_thesis: verum end; supposethat A3: p in rng f and A4: p <> f /. 1 ; ::_thesis: Rev (Rotate (f,p)) = Rotate ((Rev f),p) f just_once_values p proof take p .. f ; :: according to REVROT_1:def_2 ::_thesis: ( p .. f in dom f & p = f /. (p .. f) & ( for z being set st z in dom f & z <> p .. f holds f /. z <> p ) ) thus A5: p .. f in dom f by A3, FINSEQ_4:20; ::_thesis: ( p = f /. (p .. f) & ( for z being set st z in dom f & z <> p .. f holds f /. z <> p ) ) thus A6: p = f . (p .. f) by A3, FINSEQ_4:19 .= f /. (p .. f) by A5, PARTFUN1:def_6 ; ::_thesis: for z being set st z in dom f & z <> p .. f holds f /. z <> p let z be set ; ::_thesis: ( z in dom f & z <> p .. f implies f /. z <> p ) assume that A7: z in dom f and A8: z <> p .. f ; ::_thesis: f /. z <> p reconsider k = z as Element of NAT by A7; percases ( k < p .. f or k > p .. f ) by A8, XXREAL_0:1; supposeA9: k < p .. f ; ::_thesis: f /. z <> p ( p .. f <= len f & p .. f <> len f ) by A3, A4, A6, FINSEQ_4:21, FINSEQ_6:def_1; then A10: p .. f < len f by XXREAL_0:1; 1 <= k by A7, FINSEQ_3:25; hence f /. z <> p by A6, A9, A10, GOBOARD7:36; ::_thesis: verum end; supposeA11: k > p .. f ; ::_thesis: f /. z <> p p .. f >= 1 by A3, FINSEQ_4:21; then A12: p .. f > 1 by A4, A6, XXREAL_0:1; k <= len f by A7, FINSEQ_3:25; hence f /. z <> p by A6, A11, A12, GOBOARD7:37; ::_thesis: verum end; end; end; hence Rev (Rotate (f,p)) = Rotate ((Rev f),p) by FINSEQ_6:106; ::_thesis: verum end; end; end; begin theorem Th30: :: REVROT_1:30 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); ::_thesis: ( len f > 4 implies (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) = {(f /. 1)} ) assume A1: len f > 4 ; ::_thesis: (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) = {(f /. 1)} then A2: ((len f) -' 1) + 1 = len f by XREAL_1:235, XXREAL_0:2; A3: len f >= 1 + 1 by A1, XXREAL_0:2; then A4: 1 <= (len f) -' 1 by NAT_D:55; A5: len f >= (1 + 1) + 1 by A1, XXREAL_0:2; thus (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) c= {(f /. 1)} :: according to XBOOLE_0:def_10 ::_thesis: {(f /. 1)} c= (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) proof assume not (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) c= {(f /. 1)} ; ::_thesis: contradiction then consider p being Point of (TOP-REAL 2) such that A6: p in (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) and A7: not p in {(f /. 1)} by SUBSET_1:2; A8: p <> f /. 1 by A7, TARSKI:def_1; A9: ( LSeg (f,((len f) -' 1)) = LSeg ((f /. ((len f) -' 1)),(f /. (len f))) & LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) ) by A3, A2, A4, TOPREAL1:def_3; A10: f /. (len f) = f /. 1 by FINSEQ_6:def_1; percases ( f /. (1 + 1) in LSeg (f,((len f) -' 1)) or f /. ((len f) -' 1) in LSeg (f,1) ) by A6, A9, A8, A10, JGRAPH_1:16; supposeA11: f /. (1 + 1) in LSeg (f,((len f) -' 1)) ; ::_thesis: contradiction A12: f /. (1 + 1) in LSeg (f,(1 + 1)) by A5, TOPREAL1:21; 3 + 1 = 4 ; then (1 + 1) + 1 < (len f) - 1 by A1, XREAL_1:20; then A13: (1 + 1) + 1 < (len f) -' 1 by A1, XREAL_1:233, XXREAL_0:2; (len f) -' 1 < len f by A4, NAT_D:51; then LSeg (f,(1 + 1)) misses LSeg (f,((len f) -' 1)) by A13, GOBOARD5:def_4; hence contradiction by A11, A12, XBOOLE_0:3; ::_thesis: verum end; supposeA14: f /. ((len f) -' 1) in LSeg (f,1) ; ::_thesis: contradiction A15: ((len f) -' 2) + 1 = (((len f) -' 1) -' 1) + 1 by NAT_D:45 .= (len f) -' 1 by A3, NAT_D:55, XREAL_1:235 ; then A16: ((len f) -' 2) + 1 < len f by A4, NAT_D:51; 2 + 2 < len f by A1; then 1 + 1 < (len f) - 2 by XREAL_1:20; then 1 + 1 < (len f) -' 2 by A1, XREAL_1:233, XXREAL_0:2; then A17: LSeg (f,1) misses LSeg (f,((len f) -' 2)) by A16, GOBOARD5:def_4; 1 <= (len f) - 2 by A5, XREAL_1:19; then 1 <= (len f) -' 2 by NAT_D:39; then f /. ((len f) -' 1) in LSeg (f,((len f) -' 2)) by A15, A16, TOPREAL1:21; hence contradiction by A14, A17, XBOOLE_0:3; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(f /. 1)} or x in (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) ) assume x in {(f /. 1)} ; ::_thesis: x in (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) then A18: x = f /. 1 by TARSKI:def_1; then x = f /. (len f) by FINSEQ_6:def_1; then A19: x in LSeg (f,((len f) -' 1)) by A2, A4, TOPREAL1:21; x in LSeg (f,1) by A3, A18, TOPREAL1:21; hence x in (LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) by A19, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th31: :: REVROT_1:31 for i being Element of NAT for p being Point of (TOP-REAL 2) for f being circular FinSequence of (TOP-REAL 2) st p in rng f & len (f :- p) <= i & i < len f holds LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f))) proof let i be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2) for f being circular FinSequence of (TOP-REAL 2) st p in rng f & len (f :- p) <= i & i < len f holds LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f))) let p be Point of (TOP-REAL 2); ::_thesis: for f being circular FinSequence of (TOP-REAL 2) st p in rng f & len (f :- p) <= i & i < len f holds LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f))) let f be circular FinSequence of (TOP-REAL 2); ::_thesis: ( p in rng f & len (f :- p) <= i & i < len f implies LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f))) ) assume that A1: p in rng f and A2: len (f :- p) <= i and A3: i < len f ; ::_thesis: LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f))) A4: p .. f <= len f by A1, FINSEQ_4:21; A5: len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50; then ((len f) -' (p .. f)) + 1 <= i by A2, A4, XREAL_1:233; then ((len f) + 1) -' (p .. f) <= i by A4, NAT_D:38; then A6: (len f) + 1 <= i + (p .. f) by NAT_D:52; then A7: 1 <= (i + (p .. f)) -' (len f) by NAT_D:55; (len f) - (p .. f) >= 0 by A4, XREAL_1:48; then ((len f) - (p .. f)) + 1 >= 0 + 1 by XREAL_1:6; then A8: 0 + 1 <= 0 + i by A2, A5, XXREAL_0:2; A9: len (Rotate (f,p)) = len f by Th14; A10: len f <= (len f) + 1 by NAT_1:11; A11: i + 1 <= len f by A3, NAT_1:13; then (i + 1) + (p .. f) <= (len f) + (len f) by A4, XREAL_1:7; then ((i + (p .. f)) + 1) -' (len f) <= len f by NAT_D:53; then A12: ((i + (p .. f)) -' (len f)) + 1 <= len f by A6, A10, NAT_D:38, XXREAL_0:2; ((i + 1) + (p .. f)) -' (len f) = ((i + (p .. f)) + 1) -' (len f) .= ((i + (p .. f)) -' (len f)) + 1 by A6, A10, NAT_D:38, XXREAL_0:2 ; then A13: (Rotate (f,p)) /. (i + 1) = f /. (((i + (p .. f)) -' (len f)) + 1) by A1, A2, A11, Th17, NAT_1:12; ( i + 1 <= len f & (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) ) by A1, A2, A3, Th17, NAT_1:13; hence LSeg ((Rotate (f,p)),i) = LSeg ((f /. ((i + (p .. f)) -' (len f))),(f /. (((i + (p .. f)) -' (len f)) + 1))) by A9, A13, A8, TOPREAL1:def_3 .= LSeg (f,((i + (p .. f)) -' (len f))) by A7, A12, TOPREAL1:def_3 ; ::_thesis: verum end; registration 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 Rotate (f,p) is s.c.c. proof set h = Rotate (f,p); percases ( not p in rng f or ( p in rng f & p .. f = 1 ) or ( p in rng f & p .. f = len f ) or ( p in rng f & p .. f <> 1 & p .. f <> len f ) ) ; suppose not p in rng f ; ::_thesis: Rotate (f,p) is s.c.c. hence Rotate (f,p) is s.c.c. by FINSEQ_6:def_2; ::_thesis: verum end; suppose ( p in rng f & p .. f = 1 ) ; ::_thesis: Rotate (f,p) is s.c.c. then p = f /. 1 by FINSEQ_5:38; hence Rotate (f,p) is s.c.c. by FINSEQ_6:89; ::_thesis: verum end; suppose ( p in rng f & p .. f = len f ) ; ::_thesis: Rotate (f,p) is s.c.c. then p = f /. (len f) by FINSEQ_5:38; then p = f /. 1 by FINSEQ_6:def_1; hence Rotate (f,p) is s.c.c. by FINSEQ_6:89; ::_thesis: verum end; supposethat A1: p in rng f and A2: p .. f <> 1 and A3: p .. f <> len f ; ::_thesis: Rotate (f,p) is s.c.c. A4: len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50; let i be Element of NAT ; :: according to GOBOARD5:def_4 ::_thesis: for b1 being Element of NAT holds ( b1 <= i + 1 or ( ( i <= 1 or len (Rotate (f,p)) <= b1 ) & len (Rotate (f,p)) <= b1 + 1 ) or LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),b1) ) let j be Element of NAT ; ::_thesis: ( j <= i + 1 or ( ( i <= 1 or len (Rotate (f,p)) <= j ) & len (Rotate (f,p)) <= j + 1 ) or LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) ) assume that A5: i + 1 < j and A6: ( ( i > 1 & j < len (Rotate (f,p)) ) or j + 1 < len (Rotate (f,p)) ) ; ::_thesis: LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) 1 <= p .. f by A1, FINSEQ_4:21; then p .. f > 1 by A2, XXREAL_0:1; then A7: (i -' 1) + (p .. f) > 0 + 1 by NAT_1:2, XREAL_1:8; i <= i + 1 by NAT_1:11; then A8: i < j by A5, XXREAL_0:2; A9: len f = len (Rotate (f,p)) by Th14; A10: p .. f <= len f by A1, FINSEQ_4:21; then A11: (len f) - (p .. f) = (len f) -' (p .. f) by XREAL_1:233; j <= j + 1 by NAT_1:11; then A12: j < len f by A9, A6, XXREAL_0:2; then A13: i < len f by A8, XXREAL_0:2; now__::_thesis:_LSeg_((Rotate_(f,p)),i)_misses_LSeg_((Rotate_(f,p)),j) percases ( i = 0 or ( i >= 1 & j < len (f :- p) ) or ( i >= 1 & j >= len (f :- p) & i < len (f :- p) ) or i >= len (f :- p) ) by NAT_1:14; suppose i = 0 ; ::_thesis: LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) then LSeg ((Rotate (f,p)),i) = {} by TOPREAL1:def_3; hence LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) by XBOOLE_1:65; ::_thesis: verum end; supposethat A14: i >= 1 and A15: j < len (f :- p) ; ::_thesis: LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) i < len (f :- p) by A8, A15, XXREAL_0:2; then A16: LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f))) by A1, A14, Th24; A17: 1 <= j by A8, A14, XXREAL_0:2; then j -' 1 < (len f) -' (p .. f) by A4, A11, A15, NAT_D:54; then A18: (j -' 1) + (p .. f) < len f by NAT_D:53; i < j -' 1 by A5, NAT_D:52; then A19: (i + 1) -' 1 < j -' 1 by NAT_D:34; ((i -' 1) + (p .. f)) + 1 = ((i -' 1) + 1) + (p .. f) .= i + (p .. f) by A14, XREAL_1:235 .= ((i + 1) -' 1) + (p .. f) by NAT_D:34 ; then A20: ((i -' 1) + (p .. f)) + 1 < (j -' 1) + (p .. f) by A19, XREAL_1:6; LSeg ((Rotate (f,p)),j) = LSeg (f,((j -' 1) + (p .. f))) by A1, A15, A17, Th24; hence LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) by A7, A16, A20, A18, GOBOARD5:def_4; ::_thesis: verum end; supposethat A21: i >= 1 and A22: j >= len (f :- p) and A23: i < len (f :- p) ; ::_thesis: LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) now__::_thesis:_j_+_1_<_(i_-'_1)_+_(len_f) percases ( i > 1 or j + 1 < len f ) by A6, Th14; suppose i > 1 ; ::_thesis: j + 1 < (i -' 1) + (len f) then i >= 1 + 1 by NAT_1:13; then i -' 1 >= 1 by NAT_D:55; hence j + 1 < (i -' 1) + (len f) by A12, XREAL_1:8; ::_thesis: verum end; supposeA24: j + 1 < len f ; ::_thesis: j + 1 < (i -' 1) + (len f) i -' 1 >= 0 by NAT_1:2; then 0 + (len f) <= (i -' 1) + (len f) by XREAL_1:6; hence j + 1 < (i -' 1) + (len f) by A24, XXREAL_0:2; ::_thesis: verum end; end; end; then (j + 1) + (p .. f) < ((i -' 1) + (len f)) + (p .. f) by XREAL_1:6; then A25: (j + (p .. f)) + 1 < ((i -' 1) + (p .. f)) + (len f) ; (len f) -' (p .. f) <= ((len f) -' (p .. f)) + 1 by NAT_1:11; then (len f) - (p .. f) <= j by A4, A11, A22, XXREAL_0:2; then A26: len f <= j + (p .. f) by XREAL_1:20; then len f <= (j + (p .. f)) + 1 by NAT_1:12; then ((j + (p .. f)) + 1) -' (len f) < (i -' 1) + (p .. f) by A25, NAT_D:54; then A27: ((j + (p .. f)) -' (len f)) + 1 < (i -' 1) + (p .. f) by A26, NAT_D:38; A28: ( LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f))) & LSeg ((Rotate (f,p)),j) = LSeg (f,((j + (p .. f)) -' (len f))) ) by A1, A12, A21, A22, A23, Th24, Th31; now__::_thesis:_LSeg_((Rotate_(f,p)),i)_misses_LSeg_((Rotate_(f,p)),j) percases ( j > ((len f) - (p .. f)) + 1 or i + 1 < ((len f) - (p .. f)) + 1 ) by A5, XXREAL_0:2; suppose j > ((len f) - (p .. f)) + 1 ; ::_thesis: LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) then 1 < j - ((len f) - (p .. f)) by XREAL_1:20; then 1 < (j + (p .. f)) - (len f) ; then A29: 1 < (j + (p .. f)) -' (len f) by NAT_D:39; i < ((len f) -' (p .. f)) + 1 by A4, A10, A23, XREAL_1:233; then i -' 1 < (len f) -' (p .. f) by A21, NAT_D:54; then (i -' 1) + (p .. f) < len f by NAT_D:53; hence LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) by A28, A27, A29, GOBOARD5:def_4; ::_thesis: verum end; suppose i + 1 < ((len f) - (p .. f)) + 1 ; ::_thesis: LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) then i < (len f) - (p .. f) by XREAL_1:6; then i + (p .. f) < len f by XREAL_1:20; then ((i -' 1) + 1) + (p .. f) < len f by A21, XREAL_1:235; then ((i -' 1) + (p .. f)) + 1 < len f ; hence LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) by A28, A27, GOBOARD5:def_4; ::_thesis: verum end; end; end; hence LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) ; ::_thesis: verum end; supposeA30: i >= len (f :- p) ; ::_thesis: LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) then j >= len (f :- p) by A8, XXREAL_0:2; then A31: LSeg ((Rotate (f,p)),j) = LSeg (f,((j + (p .. f)) -' (len f))) by A1, A12, Th31; (len f) - (p .. f) <= ((len f) - (p .. f)) + 1 by XREAL_1:29; then A32: (len f) - (p .. f) <= i by A4, A30, XXREAL_0:2; then A33: len f <= i + (p .. f) by A11, NAT_D:52; A34: i + (p .. f) < j + (p .. f) by A8, XREAL_1:6; then A35: len f < j + (p .. f) by A33, XXREAL_0:2; ( j + 1 <= len f & p .. f < len f ) by A3, A10, A9, A6, NAT_1:13, XXREAL_0:1; then (j + 1) + (p .. f) < (len f) + (len f) by XREAL_1:8; then (j + (1 + (p .. f))) - (len f) < len f by XREAL_1:19; then ((j + (p .. f)) - (len f)) + 1 < len f ; then A36: ((j + (p .. f)) -' (len f)) + 1 < len f by A33, A34, XREAL_1:233, XXREAL_0:2; A37: (i + 1) + (p .. f) < j + (p .. f) by A5, XREAL_1:6; ((i + (p .. f)) -' (len f)) + 1 = ((i + (p .. f)) + 1) -' (len f) by A11, A32, NAT_D:38, NAT_D:52 .= ((i + 1) + (p .. f)) -' (len f) ; then A38: ((i + (p .. f)) -' (len f)) + 1 < (j + (p .. f)) -' (len f) by A35, A37, NAT_D:57; LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f))) by A1, A13, A30, Th31; hence LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) by A31, A38, A36, GOBOARD5:def_4; ::_thesis: verum end; end; end; hence LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j) ; ::_thesis: verum end; end; end; end; registration let p be Point of (TOP-REAL 2); let f be V8() standard special_circular_sequence; cluster Rotate (f,p) -> unfolded ; coherence Rotate (f,p) is unfolded proof percases ( not p in rng f or p in rng f ) ; suppose not p in rng f ; ::_thesis: Rotate (f,p) is unfolded hence Rotate (f,p) is unfolded by FINSEQ_6:def_2; ::_thesis: verum end; supposeA1: p in rng f ; ::_thesis: Rotate (f,p) is unfolded let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (Rotate (f,p)) or (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {((Rotate (f,p)) /. (i + 1))} ) assume that A2: 1 <= i and A3: i + 2 <= len (Rotate (f,p)) ; ::_thesis: (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {((Rotate (f,p)) /. (i + 1))} A4: i in NAT by ORDINAL1:def_12; A5: len f > 4 by GOBOARD7:34; thus (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {((Rotate (f,p)) /. (i + 1))} ::_thesis: verum proof A6: ((i + 1) -' 1) + (p .. f) = i + (p .. f) by NAT_D:34 .= ((i -' 1) + 1) + (p .. f) by A2, XREAL_1:235 .= ((i -' 1) + (p .. f)) + 1 ; A7: len f = len (Rotate (f,p)) by Th14; i + 1 < i + 2 by XREAL_1:6; then A8: i + 1 < len f by A3, A7, XXREAL_0:2; A9: len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50; percases ( i + 1 = len (f :- p) or i + 1 < len (f :- p) or len (f :- p) < i + 1 ) by XXREAL_0:1; supposeA10: i + 1 = len (f :- p) ; ::_thesis: (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {((Rotate (f,p)) /. (i + 1))} ((len (f :- p)) + (p .. f)) -' (len f) = ((len f) + 1) - (len f) by A9, NAT_1:11, XREAL_1:233 .= 1 ; then A11: LSeg ((Rotate (f,p)),(len (f :- p))) = LSeg (f,1) by A1, A8, A10, Th31; A12: i < len (f :- p) by A10, XREAL_1:29; (i -' 1) + (p .. f) = (((((len f) - (p .. f)) + 1) - 1) - 1) + (p .. f) by A2, A9, A10, XREAL_1:233 .= (((len f) - (p .. f)) + (p .. f)) - 1 .= (len f) -' 1 by A5, XREAL_1:233, XXREAL_0:2 ; then LSeg ((Rotate (f,p)),i) = LSeg (f,((len f) -' 1)) by A1, A2, A4, A12, Th24; hence (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {(f /. 1)} by A10, A11, Th30, GOBOARD7:34 .= {(f /. (len f))} by FINSEQ_6:def_1 .= {((Rotate (f,p)) /. (i + 1))} by A1, A10, Th11 ; ::_thesis: verum end; supposeA13: i + 1 < len (f :- p) ; ::_thesis: (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {((Rotate (f,p)) /. (i + 1))} then i + 1 < ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50; then i < (len f) - (p .. f) by XREAL_1:6; then i + (p .. f) < len f by XREAL_1:20; then ((i -' 1) + 1) + (p .. f) < len f by A2, XREAL_1:235; then (((i -' 1) + (p .. f)) + 1) + 1 <= len f by NAT_1:13; then A14: ((i -' 1) + (p .. f)) + (1 + 1) <= len f ; ( (i -' 1) + (p .. f) >= p .. f & p .. f >= 1 ) by A1, FINSEQ_4:21, NAT_1:11; then A15: 1 <= (i -' 1) + (p .. f) by XXREAL_0:2; i + 0 < i + 1 by XREAL_1:6; then i < len (f :- p) by A13, XXREAL_0:2; then A16: LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f))) by A1, A2, A4, Th24; LSeg ((Rotate (f,p)),(i + 1)) = LSeg (f,(((i + 1) -' 1) + (p .. f))) by A1, A13, Th24, NAT_1:11; hence (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {(f /. (((i + 1) -' 1) + (p .. f)))} by A6, A16, A15, A14, TOPREAL1:def_6 .= {((Rotate (f,p)) /. (i + 1))} by A1, A13, Th9, NAT_1:11 ; ::_thesis: verum end; supposeA17: len (f :- p) < i + 1 ; ::_thesis: (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {((Rotate (f,p)) /. (i + 1))} p .. f <= len f by A1, FINSEQ_4:21; then (i + 2) + (p .. f) <= (len f) + (len f) by A3, A7, XREAL_1:7; then ((i + (p .. f)) + 2) - (len f) <= len f by XREAL_1:20; then A18: ((i + (p .. f)) - (len f)) + 2 <= len f ; (i + 1) + 1 <= len f by A3, Th14; then A19: i + 1 < len f by NAT_1:13; i + 1 > ((len f) - (p .. f)) + 1 by A1, A17, FINSEQ_5:50; then (len f) - (p .. f) < i by XREAL_1:6; then A20: len f < i + (p .. f) by XREAL_1:19; then A21: (i + (p .. f)) -' (len f) = (i + (p .. f)) - (len f) by XREAL_1:233; 0 < (i + (p .. f)) - (len f) by A20, XREAL_1:50; then A22: 0 + 1 <= (i + (p .. f)) -' (len f) by A21, NAT_1:13; A23: ((i + 1) + (p .. f)) -' (len f) = ((i + (p .. f)) + 1) -' (len f) .= ((i + (p .. f)) -' (len f)) + 1 by A20, NAT_D:38 ; A24: len (f :- p) <= i by A17, NAT_1:13; i + 0 < i + 1 by XREAL_1:6; then i < len f by A19, XXREAL_0:2; then A25: LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f))) by A1, A4, A24, Th31; LSeg ((Rotate (f,p)),(i + 1)) = LSeg (f,(((i + 1) + (p .. f)) -' (len f))) by A1, A17, A19, Th31; hence (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {(f /. (((i + 1) + (p .. f)) -' (len f)))} by A25, A21, A22, A23, A18, TOPREAL1:def_6 .= {((Rotate (f,p)) /. (i + 1))} by A1, A8, A17, Th17 ; ::_thesis: verum end; end; end; end; end; end; end; theorem Th32: :: REVROT_1:32 for i being Element of NAT for p being Point of (TOP-REAL 2) for f being circular FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < p .. f holds LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f))) proof let i be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2) for f being circular FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < p .. f holds LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f))) let p be Point of (TOP-REAL 2); ::_thesis: for f being circular FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < p .. f holds LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f))) let f be circular FinSequence of (TOP-REAL 2); ::_thesis: ( p in rng f & 1 <= i & i < p .. f implies LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f))) ) assume that A1: p in rng f and A2: 1 <= i and A3: i < p .. f ; ::_thesis: LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f))) A4: p .. f <= len f by A1, FINSEQ_4:21; A5: i + (len f) < (len f) + (p .. f) by A3, XREAL_1:6; A6: len f <= i + (len f) by NAT_1:11; then p .. f <= i + (len f) by A4, XXREAL_0:2; then A7: (i + (len f)) -' (p .. f) < len f by A5, NAT_D:54; (len f) + 1 <= i + (len f) by A2, XREAL_1:6; then ((len f) + 1) -' (p .. f) <= (i + (len f)) -' (p .. f) by NAT_D:42; then ((len f) -' (p .. f)) + 1 <= (i + (len f)) -' (p .. f) by A4, NAT_D:38; then ((len f) - (p .. f)) + 1 <= (i + (len f)) -' (p .. f) by A4, XREAL_1:233; then A8: len (f :- p) <= (i + (len f)) -' (p .. f) by A1, FINSEQ_5:50; (((i + (len f)) -' (p .. f)) + (p .. f)) -' (len f) = (i + (len f)) -' (len f) by A4, A6, XREAL_1:235, XXREAL_0:2 .= i by NAT_D:34 ; hence LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f))) by A1, A8, A7, Th31; ::_thesis: verum end; theorem Th33: :: REVROT_1:33 for p being Point of (TOP-REAL 2) for f being circular FinSequence of (TOP-REAL 2) holds L~ (Rotate (f,p)) = L~ f proof let p be Point of (TOP-REAL 2); ::_thesis: for f being circular FinSequence of (TOP-REAL 2) holds L~ (Rotate (f,p)) = L~ f let f be circular FinSequence of (TOP-REAL 2); ::_thesis: L~ (Rotate (f,p)) = L~ f percases ( not p in rng f or p in rng f ) ; suppose not p in rng f ; ::_thesis: L~ (Rotate (f,p)) = L~ f hence L~ (Rotate (f,p)) = L~ f by FINSEQ_6:def_2; ::_thesis: verum end; supposeA1: p in rng f ; ::_thesis: L~ (Rotate (f,p)) = L~ f set B = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; set A = { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; A2: { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } proof A3: p .. f <= len f by A1, FINSEQ_4:21; thus { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } c= { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } :: according to XBOOLE_0:def_10 ::_thesis: { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } c= { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } proof A4: 1 <= p .. f by A1, FINSEQ_4:21; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } or x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ) assume x in { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; ::_thesis: x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } then consider i being Element of NAT such that A5: x = LSeg ((Rotate (f,p)),i) and A6: 1 <= i and A7: i + 1 <= len f ; A8: i < len f by A7, NAT_1:13; percases ( i < len (f :- p) or i >= len (f :- p) ) ; supposeA9: i < len (f :- p) ; ::_thesis: x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } then i < ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50; then i < ((len f) -' (p .. f)) + 1 by A3, XREAL_1:233; then i -' 1 < (len f) -' (p .. f) by A6, NAT_D:54; then (i -' 1) + (p .. f) < len f by NAT_D:53; then A10: ((i -' 1) + (p .. f)) + 1 <= len f by NAT_1:13; 1 + 1 <= i + (p .. f) by A6, A4, XREAL_1:7; then 1 <= (i + (p .. f)) -' 1 by NAT_D:55; then A11: 1 <= (i -' 1) + (p .. f) by A6, NAT_D:38; LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f))) by A1, A6, A9, Th24; hence x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A5, A11, A10; ::_thesis: verum end; supposeA12: i >= len (f :- p) ; ::_thesis: x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } then ((len f) - (p .. f)) + 1 <= i by A1, FINSEQ_5:50; then ((len f) -' (p .. f)) + 1 <= i by A3, XREAL_1:233; then (1 + (len f)) -' (p .. f) <= i by A3, NAT_D:38; then A13: 1 + (len f) <= i + (p .. f) by NAT_D:52; then A14: 1 <= (i + (p .. f)) -' (len f) by NAT_D:55; (i + 1) + (p .. f) <= (len f) + (len f) by A3, A7, XREAL_1:7; then ( len f <= (len f) + 1 & ((i + (p .. f)) + 1) -' (len f) <= len f ) by NAT_1:11, NAT_D:53; then A15: ((i + (p .. f)) -' (len f)) + 1 <= len f by A13, NAT_D:38, XXREAL_0:2; LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f))) by A1, A8, A12, Th31; hence x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A5, A14, A15; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } or x in { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ) assume x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; ::_thesis: x in { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } then consider i being Element of NAT such that A16: x = LSeg (f,i) and A17: 1 <= i and A18: i + 1 <= len f ; A19: i < len f by A18, NAT_1:13; percases ( p .. f <= i or i < p .. f ) ; supposeA20: p .. f <= i ; ::_thesis: x in { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } i <= i + 1 by NAT_1:11; then A21: p .. f <= i + 1 by A20, XXREAL_0:2; 1 <= p .. f by A1, FINSEQ_4:21; then i + 1 < (len f) + (p .. f) by A19, XREAL_1:8; then (i + 1) -' (p .. f) < len f by A21, NAT_D:54; then (i -' (p .. f)) + 1 < len f by A20, NAT_D:38; then A22: ((i -' (p .. f)) + 1) + 1 <= len f by NAT_1:13; 1 + (p .. f) <= i + 1 by A20, XREAL_1:6; then 1 <= (i + 1) -' (p .. f) by NAT_D:55; then A23: 1 <= (i -' (p .. f)) + 1 by A20, NAT_D:38; LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1)) by A1, A19, A20, Th25; hence x in { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A16, A23, A22; ::_thesis: verum end; supposeA24: i < p .. f ; ::_thesis: x in { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } then i + 1 <= p .. f by NAT_1:13; then (i + 1) + (len f) <= (len f) + (p .. f) by XREAL_1:6; then A25: ((i + (len f)) + 1) -' (p .. f) <= len f by NAT_D:53; ( p .. f <= len f & len f <= i + (len f) ) by A1, FINSEQ_4:21, NAT_1:11; then A26: ((i + (len f)) -' (p .. f)) + 1 <= len f by A25, NAT_D:38, XXREAL_0:2; 1 + (p .. f) <= i + (len f) by A3, A17, XREAL_1:7; then A27: 1 <= (i + (len f)) -' (p .. f) by NAT_D:55; LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f))) by A1, A17, A24, Th32; hence x in { (LSeg ((Rotate (f,p)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A16, A27, A26; ::_thesis: verum end; end; end; len (Rotate (f,p)) = len f by Th14; hence L~ (Rotate (f,p)) = L~ f by A2; ::_thesis: verum end; end; end; theorem Th34: :: REVROT_1:34 for p being Point of (TOP-REAL 2) for f being circular FinSequence of (TOP-REAL 2) for G being Go-board holds ( f is_sequence_on G iff Rotate (f,p) is_sequence_on G ) proof let p be Point of (TOP-REAL 2); ::_thesis: for f being circular FinSequence of (TOP-REAL 2) for G being Go-board holds ( f is_sequence_on G iff Rotate (f,p) is_sequence_on G ) let f be circular FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board holds ( f is_sequence_on G iff Rotate (f,p) is_sequence_on G ) let G be Go-board; ::_thesis: ( f is_sequence_on G iff Rotate (f,p) is_sequence_on G ) A1: dom f = dom (Rotate (f,p)) by Th15; A2: len f = len (Rotate (f,p)) by Th14; percases ( not p in rng f or p in rng f ) ; suppose not p in rng f ; ::_thesis: ( f is_sequence_on G iff Rotate (f,p) is_sequence_on G ) hence ( f is_sequence_on G iff Rotate (f,p) is_sequence_on G ) by FINSEQ_6:def_2; ::_thesis: verum end; supposeA3: p in rng f ; ::_thesis: ( f is_sequence_on G iff Rotate (f,p) is_sequence_on G ) then A4: p .. f <= len f by FINSEQ_4:21; A5: 1 <= p .. f by A3, FINSEQ_4:21; thus ( f is_sequence_on G implies Rotate (f,p) is_sequence_on G ) ::_thesis: ( Rotate (f,p) is_sequence_on G implies f is_sequence_on G ) proof assume A6: f is_sequence_on G ; ::_thesis: Rotate (f,p) is_sequence_on G thus for n being Element of NAT st n in dom (Rotate (f,p)) holds ex i, j being Element of NAT st ( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) :: according to GOBOARD1:def_9 ::_thesis: for b1 being Element of NAT holds ( not b1 in dom (Rotate (f,p)) or not b1 + 1 in dom (Rotate (f,p)) or for b2, b3, b4, b5 being Element of NAT holds ( not [b2,b3] in Indices G or not [b4,b5] in Indices G or not (Rotate (f,p)) /. b1 = G * (b2,b3) or not (Rotate (f,p)) /. (b1 + 1) = G * (b4,b5) or (abs (b2 - b4)) + (abs (b3 - b5)) = 1 ) ) proof let n be Element of NAT ; ::_thesis: ( n in dom (Rotate (f,p)) implies ex i, j being Element of NAT st ( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) ) assume A7: n in dom (Rotate (f,p)) ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) then A8: 1 <= n by FINSEQ_3:25; A9: n <= len (Rotate (f,p)) by A7, FINSEQ_3:25; percases ( len (f :- p) <= n or len (f :- p) >= n ) ; supposeA10: len (f :- p) <= n ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) then ((len f) - (p .. f)) + 1 <= n by A3, FINSEQ_5:50; then ((len f) -' (p .. f)) + 1 <= n by A4, XREAL_1:233; then ((len f) + 1) -' (p .. f) <= n by A4, NAT_D:38; then (len f) + 1 <= n + (p .. f) by NAT_D:52; then A11: 1 <= (n + (p .. f)) -' (len f) by NAT_D:55; n + (p .. f) <= (len f) + (len f) by A2, A4, A9, XREAL_1:7; then (n + (p .. f)) -' (len f) <= len f by NAT_D:53; then (n + (p .. f)) -' (len f) in dom (Rotate (f,p)) by A2, A11, FINSEQ_3:25; then consider i, j being Element of NAT such that A12: [i,j] in Indices G and A13: f /. ((n + (p .. f)) -' (len f)) = G * (i,j) by A1, A6, GOBOARD1:def_9; take i ; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) take j ; ::_thesis: ( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) thus [i,j] in Indices G by A12; ::_thesis: (Rotate (f,p)) /. n = G * (i,j) thus (Rotate (f,p)) /. n = G * (i,j) by A2, A3, A9, A10, A13, Th17; ::_thesis: verum end; supposeA14: len (f :- p) >= n ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) then ((len f) - (p .. f)) + 1 >= n by A3, FINSEQ_5:50; then ((len f) -' (p .. f)) + 1 >= n by A4, XREAL_1:233; then n -' 1 <= (len f) -' (p .. f) by NAT_D:53; then A15: (n -' 1) + (p .. f) <= len f by A4, NAT_D:54; 1 + 1 <= n + (p .. f) by A5, A8, XREAL_1:7; then 1 <= (n + (p .. f)) -' 1 by NAT_D:55; then 1 <= (n -' 1) + (p .. f) by A8, NAT_D:38; then (n -' 1) + (p .. f) in dom (Rotate (f,p)) by A2, A15, FINSEQ_3:25; then consider i, j being Element of NAT such that A16: [i,j] in Indices G and A17: f /. ((n -' 1) + (p .. f)) = G * (i,j) by A1, A6, GOBOARD1:def_9; take i ; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) take j ; ::_thesis: ( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) thus [i,j] in Indices G by A16; ::_thesis: (Rotate (f,p)) /. n = G * (i,j) thus (Rotate (f,p)) /. n = G * (i,j) by A3, A8, A14, A17, Th9; ::_thesis: verum end; end; end; let n be Element of NAT ; ::_thesis: ( not n in dom (Rotate (f,p)) or not n + 1 in dom (Rotate (f,p)) or for b1, b2, b3, b4 being Element of NAT holds ( not [b1,b2] in Indices G or not [b3,b4] in Indices G or not (Rotate (f,p)) /. n = G * (b1,b2) or not (Rotate (f,p)) /. (n + 1) = G * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 ) ) assume that A18: n in dom (Rotate (f,p)) and A19: n + 1 in dom (Rotate (f,p)) ; ::_thesis: for b1, b2, b3, b4 being Element of NAT holds ( not [b1,b2] in Indices G or not [b3,b4] in Indices G or not (Rotate (f,p)) /. n = G * (b1,b2) or not (Rotate (f,p)) /. (n + 1) = G * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 ) A20: 1 <= n by A18, FINSEQ_3:25; A21: n <= len f by A1, A18, FINSEQ_3:25; A22: 1 <= n + 1 by A19, FINSEQ_3:25; A23: n + 1 <= len f by A1, A19, FINSEQ_3:25; let m, k, i, j be Element of NAT ; ::_thesis: ( not [m,k] in Indices G or not [i,j] in Indices G or not (Rotate (f,p)) /. n = G * (m,k) or not (Rotate (f,p)) /. (n + 1) = G * (i,j) or (abs (m - i)) + (abs (k - j)) = 1 ) assume A24: ( [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) ) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 thus (abs (m - i)) + (abs (k - j)) = 1 ::_thesis: verum proof percases ( len (f :- p) <= n or len (f :- p) > n ) ; supposeA25: len (f :- p) <= n ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 ((len f) - (p .. f)) + 1 <= n by A3, A25, FINSEQ_5:50; then ((len f) -' (p .. f)) + 1 <= n by A4, XREAL_1:233; then ((len f) + 1) -' (p .. f) <= n by A4, NAT_D:38; then (len f) + 1 <= n + (p .. f) by NAT_D:52; then A26: 1 <= (n + (p .. f)) -' (len f) by NAT_D:55; n + (p .. f) <= (len f) + (len f) by A4, A21, XREAL_1:7; then (n + (p .. f)) -' (len f) <= len f by NAT_D:53; then A27: (n + (p .. f)) -' (len f) in dom f by A26, FINSEQ_3:25; n <= n + 1 by NAT_1:11; then A28: len (f :- p) <= n + 1 by A25, XXREAL_0:2; then A29: ((len f) - (p .. f)) + 1 <= n + 1 by A3, FINSEQ_5:50; then (len f) - (p .. f) <= n by XREAL_1:6; then A30: len f <= n + (p .. f) by XREAL_1:20; A31: (Rotate (f,p)) /. (n + 1) = f /. (((n + 1) + (p .. f)) -' (len f)) by A3, A23, A28, Th17; A32: ((n + 1) + (p .. f)) -' (len f) = ((n + (p .. f)) + 1) -' (len f) .= ((n + (p .. f)) -' (len f)) + 1 by A30, NAT_D:38 ; ((len f) -' (p .. f)) + 1 <= n + 1 by A4, A29, XREAL_1:233; then ((len f) + 1) -' (p .. f) <= n + 1 by A4, NAT_D:38; then (len f) + 1 <= (n + 1) + (p .. f) by NAT_D:52; then A33: 1 <= ((n + 1) + (p .. f)) -' (len f) by NAT_D:55; (n + 1) + (p .. f) <= (len f) + (len f) by A4, A23, XREAL_1:7; then ((n + 1) + (p .. f)) -' (len f) <= len f by NAT_D:53; then A34: ((n + 1) + (p .. f)) -' (len f) in dom f by A33, FINSEQ_3:25; (Rotate (f,p)) /. n = f /. ((n + (p .. f)) -' (len f)) by A3, A21, A25, Th17; hence (abs (m - i)) + (abs (k - j)) = 1 by A6, A24, A31, A32, A27, A34, GOBOARD1:def_9; ::_thesis: verum end; supposeA35: len (f :- p) > n ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 then n <= ((len f) - (p .. f)) + 1 by A3, FINSEQ_5:50; then n <= ((len f) -' (p .. f)) + 1 by A4, XREAL_1:233; then n -' 1 <= (len f) -' (p .. f) by NAT_D:53; then A36: (n -' 1) + (p .. f) <= len f by A4, NAT_D:54; 1 + 1 <= n + (p .. f) by A5, A20, XREAL_1:7; then 1 <= (n + (p .. f)) -' 1 by NAT_D:55; then 1 <= (n -' 1) + (p .. f) by A20, NAT_D:38; then A37: (n -' 1) + (p .. f) in dom f by A36, FINSEQ_3:25; A38: ((n + 1) -' 1) + (p .. f) = n + (p .. f) by NAT_D:34 .= ((n -' 1) + 1) + (p .. f) by A20, XREAL_1:235 .= ((n -' 1) + (p .. f)) + 1 ; A39: len (f :- p) >= n + 1 by A35, NAT_1:13; then A40: (Rotate (f,p)) /. (n + 1) = f /. (((n + 1) -' 1) + (p .. f)) by A3, A22, Th9; n + 1 <= ((len f) - (p .. f)) + 1 by A3, A39, FINSEQ_5:50; then n + 1 <= ((len f) -' (p .. f)) + 1 by A4, XREAL_1:233; then (n + 1) -' 1 <= (len f) -' (p .. f) by NAT_D:53; then A41: ((n + 1) -' 1) + (p .. f) <= len f by A4, NAT_D:54; 1 + 1 <= (n + 1) + (p .. f) by A5, A22, XREAL_1:7; then 1 <= ((n + 1) + (p .. f)) -' 1 by NAT_D:55; then 1 <= ((n + 1) -' 1) + (p .. f) by A22, NAT_D:38; then A42: ((n + 1) -' 1) + (p .. f) in dom f by A41, FINSEQ_3:25; (Rotate (f,p)) /. n = f /. ((n -' 1) + (p .. f)) by A3, A20, A35, Th9; hence (abs (m - i)) + (abs (k - j)) = 1 by A6, A24, A40, A38, A37, A42, GOBOARD1:def_9; ::_thesis: verum end; end; end; end; assume A43: Rotate (f,p) is_sequence_on G ; ::_thesis: f is_sequence_on G thus for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) :: according to GOBOARD1:def_9 ::_thesis: for b1 being Element of NAT holds ( not b1 in dom f or not b1 + 1 in dom f or for b2, b3, b4, b5 being Element of NAT holds ( not [b2,b3] in Indices G or not [b4,b5] in Indices G or not f /. b1 = G * (b2,b3) or not f /. (b1 + 1) = G * (b4,b5) or (abs (b2 - b4)) + (abs (b3 - b5)) = 1 ) ) proof let n be Element of NAT ; ::_thesis: ( n in dom f implies ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) assume A44: n in dom f ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) then A45: 1 <= n by FINSEQ_3:25; A46: n <= len f by A44, FINSEQ_3:25; percases ( n <= p .. f or n >= p .. f ) ; supposeA47: n <= p .. f ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) n <= n + ((len f) -' (p .. f)) by NAT_1:11; then 1 <= n + ((len f) -' (p .. f)) by A45, XXREAL_0:2; then A48: 1 <= (n + (len f)) -' (p .. f) by A4, NAT_D:38; n + (len f) <= (len f) + (p .. f) by A47, XREAL_1:6; then (n + (len f)) -' (p .. f) <= len f by NAT_D:53; then (n + (len f)) -' (p .. f) in dom f by A48, FINSEQ_3:25; then consider i, j being Element of NAT such that A49: [i,j] in Indices G and A50: (Rotate (f,p)) /. ((n + (len f)) -' (p .. f)) = G * (i,j) by A1, A43, GOBOARD1:def_9; take i ; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) take j ; ::_thesis: ( [i,j] in Indices G & f /. n = G * (i,j) ) thus [i,j] in Indices G by A49; ::_thesis: f /. n = G * (i,j) thus f /. n = G * (i,j) by A3, A45, A47, A50, Th18; ::_thesis: verum end; supposeA51: n >= p .. f ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) then 1 + (p .. f) <= n + 1 by XREAL_1:6; then A52: 1 <= (n + 1) -' (p .. f) by NAT_D:55; n + 1 <= (len f) + (p .. f) by A5, A46, XREAL_1:7; then (n + 1) -' (p .. f) <= len f by NAT_D:53; then (n + 1) -' (p .. f) in dom f by A52, FINSEQ_3:25; then consider i, j being Element of NAT such that A53: [i,j] in Indices G and A54: (Rotate (f,p)) /. ((n + 1) -' (p .. f)) = G * (i,j) by A1, A43, GOBOARD1:def_9; take i ; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) take j ; ::_thesis: ( [i,j] in Indices G & f /. n = G * (i,j) ) thus [i,j] in Indices G by A53; ::_thesis: f /. n = G * (i,j) thus f /. n = G * (i,j) by A3, A46, A51, A54, Th10; ::_thesis: verum end; end; end; let n be Element of NAT ; ::_thesis: ( not n in dom f or not n + 1 in dom f or for b1, b2, b3, b4 being Element of NAT holds ( not [b1,b2] in Indices G or not [b3,b4] in Indices G or not f /. n = G * (b1,b2) or not f /. (n + 1) = G * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 ) ) assume that A55: n in dom f and A56: n + 1 in dom f ; ::_thesis: for b1, b2, b3, b4 being Element of NAT holds ( not [b1,b2] in Indices G or not [b3,b4] in Indices G or not f /. n = G * (b1,b2) or not f /. (n + 1) = G * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 ) A57: 1 <= n by A55, FINSEQ_3:25; A58: 1 <= n + 1 by A56, FINSEQ_3:25; A59: n <= len f by A55, FINSEQ_3:25; A60: n + 1 <= len f by A56, FINSEQ_3:25; let m, k, i, j be Element of NAT ; ::_thesis: ( not [m,k] in Indices G or not [i,j] in Indices G or not f /. n = G * (m,k) or not f /. (n + 1) = G * (i,j) or (abs (m - i)) + (abs (k - j)) = 1 ) assume A61: ( [m,k] in Indices G & [i,j] in Indices G & f /. n = G * (m,k) & f /. (n + 1) = G * (i,j) ) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 thus (abs (m - i)) + (abs (k - j)) = 1 ::_thesis: verum proof percases ( n < p .. f or n >= p .. f ) ; supposeA62: n < p .. f ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 n <= n + ((len f) -' (p .. f)) by NAT_1:11; then 1 <= n + ((len f) -' (p .. f)) by A57, XXREAL_0:2; then A63: 1 <= (n + (len f)) -' (p .. f) by A4, NAT_D:38; n + (len f) <= (len f) + (p .. f) by A62, XREAL_1:6; then (n + (len f)) -' (p .. f) <= len f by NAT_D:53; then A64: (n + (len f)) -' (p .. f) in dom f by A63, FINSEQ_3:25; A65: ((n + 1) + (len f)) -' (p .. f) = ((len f) -' (p .. f)) + (n + 1) by A4, NAT_D:38 .= (((len f) -' (p .. f)) + n) + 1 .= ((n + (len f)) -' (p .. f)) + 1 by A4, NAT_D:38 ; n + 1 <= (n + 1) + ((len f) -' (p .. f)) by NAT_1:11; then 1 <= (n + 1) + ((len f) -' (p .. f)) by A58, XXREAL_0:2; then A66: 1 <= ((n + 1) + (len f)) -' (p .. f) by A4, NAT_D:38; A67: n + 1 <= p .. f by A62, NAT_1:13; then A68: f /. (n + 1) = (Rotate (f,p)) /. (((n + 1) + (len f)) -' (p .. f)) by A3, A58, Th18; (n + 1) + (len f) <= (len f) + (p .. f) by A67, XREAL_1:6; then ((n + 1) + (len f)) -' (p .. f) <= len f by NAT_D:53; then A69: ((n + 1) + (len f)) -' (p .. f) in dom f by A66, FINSEQ_3:25; f /. n = (Rotate (f,p)) /. ((n + (len f)) -' (p .. f)) by A3, A57, A62, Th18; hence (abs (m - i)) + (abs (k - j)) = 1 by A1, A43, A61, A68, A65, A64, A69, GOBOARD1:def_9; ::_thesis: verum end; supposeA70: n >= p .. f ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 then 1 + (p .. f) <= n + 1 by XREAL_1:6; then A71: 1 <= (n + 1) -' (p .. f) by NAT_D:55; n + 1 <= (len f) + (p .. f) by A5, A59, XREAL_1:7; then (n + 1) -' (p .. f) <= len f by NAT_D:53; then A72: (n + 1) -' (p .. f) in dom f by A71, FINSEQ_3:25; A73: f /. n = (Rotate (f,p)) /. ((n + 1) -' (p .. f)) by A3, A59, A70, Th10; A74: n <= n + 1 by NAT_1:11; then A75: ((n + 1) + 1) -' (p .. f) = ((n + 1) -' (p .. f)) + 1 by A70, NAT_D:38, XXREAL_0:2; A76: n + 1 >= p .. f by A70, A74, XXREAL_0:2; then 1 + (p .. f) <= (n + 1) + 1 by XREAL_1:6; then A77: 1 <= ((n + 1) + 1) -' (p .. f) by NAT_D:55; (n + 1) + 1 <= (len f) + (p .. f) by A5, A60, XREAL_1:7; then ((n + 1) + 1) -' (p .. f) <= len f by NAT_D:53; then A78: ((n + 1) + 1) -' (p .. f) in dom f by A77, FINSEQ_3:25; f /. (n + 1) = (Rotate (f,p)) /. (((n + 1) + 1) -' (p .. f)) by A3, A60, A76, Th10; hence (abs (m - i)) + (abs (k - j)) = 1 by A1, A43, A61, A73, A75, A78, A72, GOBOARD1:def_9; ::_thesis: verum end; end; end; end; end; end; registration let p be Point of (TOP-REAL 2); let f be non empty circular standard FinSequence of (TOP-REAL 2); cluster Rotate (f,p) -> standard ; coherence Rotate (f,p) is standard proof ( GoB (Rotate (f,p)) = GoB f & f is_sequence_on GoB f ) by Th28, GOBOARD5:def_5; hence Rotate (f,p) is_sequence_on GoB (Rotate (f,p)) by Th34; :: according to GOBOARD5:def_5 ::_thesis: verum end; end; theorem Th35: :: REVROT_1:35 for f being V8() standard special_circular_sequence for p being Point of (TOP-REAL 2) for k being Element of NAT 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 V8() standard special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) for k being Element of NAT 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))) let p be Point of (TOP-REAL 2); ::_thesis: for k being Element of NAT 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))) let k be Element of NAT ; ::_thesis: ( p in rng f & 1 <= k & k < p .. f implies left_cell (f,k) = left_cell ((Rotate (f,p)),((k + (len f)) -' (p .. f))) ) assume that A1: p in rng f and A2: 1 <= k and A3: k < p .. f ; ::_thesis: left_cell (f,k) = left_cell ((Rotate (f,p)),((k + (len f)) -' (p .. f))) set n = (k + (len f)) -' (p .. f); A4: p .. f <= len f by A1, FINSEQ_4:21; then k < len f by A3, XXREAL_0:2; then A5: k + 1 <= len f by NAT_1:13; 0 < k by A2, XXREAL_0:2; then A6: 0 + 1 < k + 1 by XREAL_1:6; len f <= k + (len f) by NAT_1:11; then A7: ((k + (len f)) -' (p .. f)) + 1 = ((k + (len f)) + 1) -' (p .. f) by A4, NAT_D:38, XXREAL_0:2; A8: k + 1 <= p .. f by A3, NAT_1:13; then (k + 1) + (len f) <= (len f) + (p .. f) by XREAL_1:6; then ((k + (len f)) -' (p .. f)) + 1 <= len f by A7, NAT_D:53; then A9: ((k + (len f)) -' (p .. f)) + 1 <= len (Rotate (f,p)) by Th14; A10: ((k + (len f)) -' (p .. f)) + 1 = ((k + 1) + (len f)) -' (p .. f) by A7; A11: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. ((k + (len f)) -' (p .. f)) = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (((k + (len f)) -' (p .. f)) + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB (Rotate (f,p))),i1,j2) ) proof A12: left_cell (f,k) = left_cell (f,k) ; let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. ((k + (len f)) -' (p .. f)) = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (((k + (len f)) -' (p .. f)) + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) ) implies ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB (Rotate (f,p))),i1,j2) ) ) assume that A13: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) ) and A14: ( (Rotate (f,p)) /. ((k + (len f)) -' (p .. f)) = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (((k + (len f)) -' (p .. f)) + 1) = (GoB (Rotate (f,p))) * (i2,j2) ) ; ::_thesis: ( ( 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) ) ) A15: GoB (Rotate (f,p)) = GoB f by Th28; then A16: ( f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) ) by A1, A2, A3, A6, A8, A10, A14, Th18; then A17: ( ( 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, A5, A13, A15, A12, GOBOARD5:def_7; percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A2, A5, A13, A15, A16, A12, GOBOARD5:def_7; case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: left_cell (f,k) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) hence left_cell (f,k) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) by A17, Th28; ::_thesis: verum end; case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: left_cell (f,k) = cell ((GoB (Rotate (f,p))),i1,j1) hence left_cell (f,k) = cell ((GoB (Rotate (f,p))),i1,j1) by A17, Th28; ::_thesis: verum end; case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: left_cell (f,k) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) hence left_cell (f,k) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) by A17, Th28; ::_thesis: verum end; case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: left_cell (f,k) = cell ((GoB (Rotate (f,p))),i1,j2) hence left_cell (f,k) = cell ((GoB (Rotate (f,p))),i1,j2) by A17, Th28; ::_thesis: verum end; end; end; 1 + (p .. f) <= k + (len f) by A2, A4, XREAL_1:7; then 1 <= (k + (len f)) -' (p .. f) by NAT_D:55; hence left_cell (f,k) = left_cell ((Rotate (f,p)),((k + (len f)) -' (p .. f))) by A9, A11, GOBOARD5:def_7; ::_thesis: verum end; theorem Th36: :: REVROT_1:36 for p being Point of (TOP-REAL 2) for f being V8() standard special_circular_sequence holds LeftComp (Rotate (f,p)) = LeftComp f proof let p be Point of (TOP-REAL 2); ::_thesis: for f being V8() standard special_circular_sequence holds LeftComp (Rotate (f,p)) = LeftComp f let f be V8() standard special_circular_sequence; ::_thesis: LeftComp (Rotate (f,p)) = LeftComp f A1: ( p in rng f implies p .. f >= 1 ) by FINSEQ_4:21; LeftComp (Rotate (f,p)) is_a_component_of (L~ (Rotate (f,p))) ` by GOBOARD9:def_1; then A2: LeftComp (Rotate (f,p)) is_a_component_of (L~ f) ` by Th33; percases ( not p in rng f or ( p in rng f & p .. f = 1 ) or ( p in rng f & 1 < p .. f ) ) by A1, XXREAL_0:1; suppose not p in rng f ; ::_thesis: LeftComp (Rotate (f,p)) = LeftComp f hence LeftComp (Rotate (f,p)) = LeftComp f by FINSEQ_6:def_2; ::_thesis: verum end; suppose ( p in rng f & p .. f = 1 ) ; ::_thesis: LeftComp (Rotate (f,p)) = LeftComp f then ( 1 in dom f & f . 1 = p ) by FINSEQ_4:19, FINSEQ_5:6; then f /. 1 = p by PARTFUN1:def_6; hence LeftComp (Rotate (f,p)) = LeftComp f by FINSEQ_6:89; ::_thesis: verum end; supposethat A3: p in rng f and A4: 1 < p .. f ; ::_thesis: LeftComp (Rotate (f,p)) = LeftComp f A5: p .. f <= len f by A3, FINSEQ_4:21; then A6: 1 + (p .. f) <= 1 + (len f) by XREAL_1:6; 1 + 1 <= p .. f by A4, NAT_1:13; then (1 + 1) + (len f) <= (len f) + (p .. f) by XREAL_1:6; then ( len f <= (len f) + 1 & ((1 + (len f)) + 1) -' (p .. f) <= len f ) by NAT_1:11, NAT_D:53; then ((1 + (len f)) -' (p .. f)) + 1 <= len f by A5, NAT_D:38, XXREAL_0:2; then A7: ((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 A3, A4, Th35; then Int (left_cell (f,1)) c= LeftComp (Rotate (f,p)) by A6, A7, GOBOARD9:21, NAT_D:55; hence LeftComp (Rotate (f,p)) = LeftComp f by A2, GOBOARD9:def_1; ::_thesis: verum end; end; end; theorem :: REVROT_1:37 for p being Point of (TOP-REAL 2) for f being V8() standard special_circular_sequence holds RightComp (Rotate (f,p)) = RightComp f proof let p be Point of (TOP-REAL 2); ::_thesis: for f being V8() standard special_circular_sequence holds RightComp (Rotate (f,p)) = RightComp f let f be V8() standard special_circular_sequence; ::_thesis: RightComp (Rotate (f,p)) = RightComp f A1: RightComp f = LeftComp (Rev f) by GOBOARD9:23; RightComp (Rotate (f,p)) = LeftComp (Rev (Rotate (f,p))) by GOBOARD9:23 .= LeftComp (Rotate ((Rev f),p)) by Th29 ; hence RightComp (Rotate (f,p)) = RightComp f by A1, Th36; ::_thesis: verum end; begin Lm1: for f being V8() standard special_circular_sequence holds ( not f /. 1 = N-min (L~ f) or f is clockwise_oriented or Rev f is clockwise_oriented ) proof let f be V8() standard special_circular_sequence; ::_thesis: ( not f /. 1 = N-min (L~ f) or f is clockwise_oriented or Rev f is clockwise_oriented ) assume A1: f /. 1 = N-min (L~ f) ; ::_thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented ) (1 + 1) + 1 < len f by GOBOARD7:34, XXREAL_0:2; then A2: 2 < (len f) -' 1 by NAT_D:52; A3: width (GoB f) in NAT ; A4: [(i_w_n f),(width (GoB f))] in Indices (GoB f) by JORDAN5D:def_7; then A5: i_w_n f <= len (GoB f) by MATRIX_1:38; A6: 1 <= width (GoB f) by A4, MATRIX_1:38; A7: (GoB f) * ((i_w_n f),(width (GoB f))) = N-min (L~ f) by JORDAN5D:def_7; A8: len f > 1 + 1 by GOBOARD7:34, XXREAL_0:2; then A9: 1 + 1 in dom f by FINSEQ_3:25; then consider i1, j1 being Element of NAT such that A10: [i1,j1] in Indices (GoB f) and A11: f /. 2 = (GoB f) * (i1,j1) by GOBOARD5:11; A12: j1 <= width (GoB f) by A10, MATRIX_1:38; A13: 1 <= j1 by A10, MATRIX_1:38; then A14: 1 <= width (GoB f) by A12, XXREAL_0:2; A15: 1 <= i1 by A10, MATRIX_1:38; A16: i1 <= len (GoB f) by A10, MATRIX_1:38; A17: now__::_thesis:_(_width_(GoB_f)_=_j1_implies_i_w_n_f_<=_i1_) assume A18: width (GoB f) = j1 ; ::_thesis: i_w_n f <= i1 then ((GoB f) * (1,j1)) `2 = N-bound (L~ f) by JORDAN5D:40; then ((GoB f) * (i1,j1)) `2 = N-bound (L~ f) by A13, A12, A15, A16, GOBOARD5:1; then (GoB f) * (i1,j1) in N-most (L~ f) by A8, A9, A11, GOBOARD1:1, SPRECT_2:10; then (N-min (L~ f)) `1 <= ((GoB f) * (i1,j1)) `1 by PSCOMP_1:39; hence i_w_n f <= i1 by A7, A13, A5, A15, A18, GOBOARD5:3; ::_thesis: verum end; A19: len f > 1 by GOBOARD7:34, XXREAL_0:2; then A20: len f in dom f by FINSEQ_3:25; 1 in dom f by A19, FINSEQ_3:25; then (abs ((i_w_n f) - i1)) + (abs ((width (GoB f)) - j1)) = 1 by A1, A4, A7, A9, A10, A11, GOBOARD5:12; 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 SEQM_3:42; then A21: ( ( i1 = (i_w_n f) + 1 & width (GoB f) = j1 ) or ( width (GoB f) = j1 + 1 & i_w_n f = i1 ) ) by A3, A12, A17, SEQM_3:41; i_e_n f <= len (GoB f) by JORDAN5D:45; then i_w_n f < len (GoB f) by SPRECT_3:27, XXREAL_0:2; then A22: ( 1 <= (i_w_n f) + 1 & (i_w_n f) + 1 <= len (GoB f) ) by NAT_1:11, NAT_1:13; A23: (len f) -' 1 <= len f by NAT_D:44; 1 <= (len f) -' 1 by A8, NAT_D:55; then A24: (len f) -' 1 in dom f by A23, FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A25: [i2,j2] in Indices (GoB f) and A26: f /. ((len f) -' 1) = (GoB f) * (i2,j2) by GOBOARD5:11; A27: j2 <= width (GoB f) by A25, MATRIX_1:38; A28: 1 <= i2 by A25, MATRIX_1:38; A29: ( 1 <= j2 & i2 <= len (GoB f) ) by A25, MATRIX_1:38; A30: now__::_thesis:_(_width_(GoB_f)_=_j2_implies_i_w_n_f_<=_i2_) assume A31: width (GoB f) = j2 ; ::_thesis: i_w_n f <= i2 then ((GoB f) * (1,j2)) `2 = N-bound (L~ f) by JORDAN5D:40; then ((GoB f) * (i2,j2)) `2 = N-bound (L~ f) by A27, A28, A29, GOBOARD5:1; then (GoB f) * (i2,j2) in N-most (L~ f) by A8, A24, A26, GOBOARD1:1, SPRECT_2:10; then (N-min (L~ f)) `1 <= ((GoB f) * (i2,j2)) `1 by PSCOMP_1:39; hence i_w_n f <= i2 by A7, A5, A28, A14, A31, GOBOARD5:3; ::_thesis: verum end; A32: len f > 4 by GOBOARD7:34; then A33: (GoB f) * (i2,j2) in L~ f by A24, A26, GOBOARD1:1, XXREAL_0:2; A34: ((len f) -' 1) + 1 = len f by A32, XREAL_1:235, XXREAL_0:2; 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, A24, A4, A7, A25, A26, A20, A34, GOBOARD5:12; 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 SEQM_3:42; then ( ( i2 = (i_w_n f) + 1 & j2 = width (GoB f) ) or ( j2 + 1 = width (GoB f) & i2 = i_w_n f ) ) by A3, A27, A30, SEQM_3:41; 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 A23, A11, A26, A6, A21, A22, A2, GOBOARD5:1, GOBOARD7:37; then ( (f /. 2) `2 = N-bound (L~ f) or (f /. ((len f) -' 1)) `2 = N-bound (L~ f) ) by JORDAN5D:40; then A35: ( f /. 2 in N-most (L~ f) or f /. ((len f) -' 1) in N-most (L~ f) ) by A8, A9, A26, A33, GOBOARD1:1, SPRECT_2:10; reconsider A = L~ (Rev f) as non empty compact Subset of (TOP-REAL 2) ; A36: A = L~ f by SPPOL_2:22; ((len f) -' 1) + (1 + 1) = (((len f) -' 1) + 1) + 1 .= (len f) + 1 by A32, XREAL_1:235, XXREAL_0:2 ; then A37: (Rev f) /. 2 = f /. ((len f) -' 1) by A24, FINSEQ_5:66; (Rev f) /. 1 = f /. (len f) by FINSEQ_5:65 .= N-min (L~ f) by A1, FINSEQ_6:def_1 .= N-min A by SPPOL_2:22 ; hence ( f is clockwise_oriented or Rev f is clockwise_oriented ) by A1, A37, A36, A35, SPRECT_2:30; ::_thesis: verum end; registration let p be Point of (TOP-REAL 2); let f be V8() standard clockwise_oriented special_circular_sequence; cluster Rotate (f,p) -> clockwise_oriented ; coherence Rotate (f,p) is clockwise_oriented proof A1: for i being Element of NAT st 1 < i & i < len f holds f /. i <> f /. 1 by GOBOARD7:36; A2: L~ (Rotate (f,p)) = L~ f by Th33; percases ( N-min (L~ f) = f /. 1 or N-min (L~ f) <> f /. 1 ) ; supposeA3: N-min (L~ f) = f /. 1 ; ::_thesis: Rotate (f,p) is clockwise_oriented 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:30; :: according to SPRECT_2:def_4 ::_thesis: verum end; supposeA4: N-min (L~ f) <> f /. 1 ; ::_thesis: Rotate (f,p) is clockwise_oriented A5: f just_once_values N-min (L~ f) proof take n_w_n f ; :: according to REVROT_1:def_2 ::_thesis: ( n_w_n f in dom f & N-min (L~ f) = f /. (n_w_n f) & ( for z being set st z in dom f & z <> n_w_n f holds f /. z <> N-min (L~ f) ) ) (n_w_n f) + 1 <= len f by JORDAN5D:def_15; then A6: n_w_n f < len f by NAT_1:13; A7: 1 <= n_w_n f by JORDAN5D:def_15; hence A8: n_w_n f in dom f by A6, FINSEQ_3:25; ::_thesis: ( N-min (L~ f) = f /. (n_w_n f) & ( for z being set st z in dom f & z <> n_w_n f holds f /. z <> N-min (L~ f) ) ) thus A9: N-min (L~ f) = f . (n_w_n f) by JORDAN5D:def_15 .= f /. (n_w_n f) by A8, PARTFUN1:def_6 ; ::_thesis: for z being set st z in dom f & z <> n_w_n f holds f /. z <> N-min (L~ f) let z be set ; ::_thesis: ( z in dom f & z <> n_w_n f implies f /. z <> N-min (L~ f) ) assume A10: z in dom f ; ::_thesis: ( not z <> n_w_n f or f /. z <> N-min (L~ f) ) then reconsider k = z as Element of NAT ; assume A11: z <> n_w_n f ; ::_thesis: f /. z <> N-min (L~ f) percases ( k < n_w_n f or k > n_w_n f ) by A11, XXREAL_0:1; supposeA12: k < n_w_n f ; ::_thesis: f /. z <> N-min (L~ f) 1 <= k by A10, FINSEQ_3:25; hence f /. z <> N-min (L~ f) by A6, A9, A12, GOBOARD7:36; ::_thesis: verum end; supposeA13: k > n_w_n f ; ::_thesis: f /. z <> N-min (L~ f) ( 1 < n_w_n f & k <= len f ) by A4, A7, A9, A10, FINSEQ_3:25, XXREAL_0:1; hence f /. z <> N-min (L~ f) by A9, A13, GOBOARD7:37; ::_thesis: verum end; end; 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:105; :: according to SPRECT_2:def_4 ::_thesis: verum end; end; end; end; theorem :: REVROT_1:38 for f being V8() standard special_circular_sequence holds ( f is clockwise_oriented or Rev f is clockwise_oriented ) proof let f be V8() standard special_circular_sequence; ::_thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented ) percases ( N-min (L~ f) = f /. 1 or N-min (L~ f) <> f /. 1 ) ; suppose N-min (L~ f) = f /. 1 ; ::_thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented ) hence ( f is clockwise_oriented or Rev f is clockwise_oriented ) by Lm1; ::_thesis: verum end; supposeA1: N-min (L~ f) <> f /. 1 ; ::_thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented ) thus ( f is clockwise_oriented or Rev f is clockwise_oriented ) ::_thesis: verum proof set g = Rotate (f,(N-min (L~ f))); A2: for i being Element of NAT st 1 < i & i < len f holds f /. i <> f /. 1 by GOBOARD7:36; ( N-min (L~ f) in rng f & L~ f = L~ (Rotate (f,(N-min (L~ f)))) ) by Th33, SPRECT_2:39; then A3: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by FINSEQ_6:92; percases ( Rotate (f,(N-min (L~ f))) is clockwise_oriented or Rev (Rotate (f,(N-min (L~ f)))) is clockwise_oriented ) by A3, Lm1; suppose Rotate (f,(N-min (L~ f))) is clockwise_oriented ; ::_thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented ) then reconsider g = Rotate (f,(N-min (L~ f))) as V8() standard clockwise_oriented special_circular_sequence ; f = Rotate (g,(f /. 1)) by A2, Th16; hence ( f is clockwise_oriented or Rev f is clockwise_oriented ) ; ::_thesis: verum end; suppose Rev (Rotate (f,(N-min (L~ f)))) is clockwise_oriented ; ::_thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented ) then reconsider h = Rev (Rotate (f,(N-min (L~ f)))) as V8() standard clockwise_oriented special_circular_sequence ; A4: Rotate (f,(N-min (L~ f))) just_once_values f /. 1 proof take (f /. 1) .. (Rotate (f,(N-min (L~ f)))) ; :: according to REVROT_1:def_2 ::_thesis: ( (f /. 1) .. (Rotate (f,(N-min (L~ f)))) in dom (Rotate (f,(N-min (L~ f)))) & f /. 1 = (Rotate (f,(N-min (L~ f)))) /. ((f /. 1) .. (Rotate (f,(N-min (L~ f))))) & ( for z being set st z in dom (Rotate (f,(N-min (L~ f)))) & z <> (f /. 1) .. (Rotate (f,(N-min (L~ f)))) holds (Rotate (f,(N-min (L~ f)))) /. z <> f /. 1 ) ) N-min (L~ f) in rng f by SPRECT_2:39; then A5: f /. 1 <> (Rotate (f,(N-min (L~ f)))) /. 1 by A1, FINSEQ_6:92; f /. 1 in rng f by FINSEQ_6:42; then A6: f /. 1 in rng (Rotate (f,(N-min (L~ f)))) by FINSEQ_6:90, SPRECT_2:39; hence A7: (f /. 1) .. (Rotate (f,(N-min (L~ f)))) in dom (Rotate (f,(N-min (L~ f)))) by FINSEQ_4:20; ::_thesis: ( f /. 1 = (Rotate (f,(N-min (L~ f)))) /. ((f /. 1) .. (Rotate (f,(N-min (L~ f))))) & ( for z being set st z in dom (Rotate (f,(N-min (L~ f)))) & z <> (f /. 1) .. (Rotate (f,(N-min (L~ f)))) holds (Rotate (f,(N-min (L~ f)))) /. z <> f /. 1 ) ) thus A8: f /. 1 = (Rotate (f,(N-min (L~ f)))) . ((f /. 1) .. (Rotate (f,(N-min (L~ f))))) by A6, FINSEQ_4:19 .= (Rotate (f,(N-min (L~ f)))) /. ((f /. 1) .. (Rotate (f,(N-min (L~ f))))) by A7, PARTFUN1:def_6 ; ::_thesis: for z being set st z in dom (Rotate (f,(N-min (L~ f)))) & z <> (f /. 1) .. (Rotate (f,(N-min (L~ f)))) holds (Rotate (f,(N-min (L~ f)))) /. z <> f /. 1 let z be set ; ::_thesis: ( z in dom (Rotate (f,(N-min (L~ f)))) & z <> (f /. 1) .. (Rotate (f,(N-min (L~ f)))) implies (Rotate (f,(N-min (L~ f)))) /. z <> f /. 1 ) assume that A9: z in dom (Rotate (f,(N-min (L~ f)))) and A10: z <> (f /. 1) .. (Rotate (f,(N-min (L~ f)))) ; ::_thesis: (Rotate (f,(N-min (L~ f)))) /. z <> f /. 1 reconsider k = z as Element of NAT by A9; percases ( k < (f /. 1) .. (Rotate (f,(N-min (L~ f)))) or k > (f /. 1) .. (Rotate (f,(N-min (L~ f)))) ) by A10, XXREAL_0:1; supposeA11: k < (f /. 1) .. (Rotate (f,(N-min (L~ f)))) ; ::_thesis: (Rotate (f,(N-min (L~ f)))) /. z <> f /. 1 ( (f /. 1) .. (Rotate (f,(N-min (L~ f)))) <= len (Rotate (f,(N-min (L~ f)))) & (f /. 1) .. (Rotate (f,(N-min (L~ f)))) <> len (Rotate (f,(N-min (L~ f)))) ) by A6, A5, A8, FINSEQ_4:21, FINSEQ_6:def_1; then A12: (f /. 1) .. (Rotate (f,(N-min (L~ f)))) < len (Rotate (f,(N-min (L~ f)))) by XXREAL_0:1; 1 <= k by A9, FINSEQ_3:25; hence (Rotate (f,(N-min (L~ f)))) /. z <> f /. 1 by A8, A11, A12, GOBOARD7:36; ::_thesis: verum end; supposeA13: k > (f /. 1) .. (Rotate (f,(N-min (L~ f)))) ; ::_thesis: (Rotate (f,(N-min (L~ f)))) /. z <> f /. 1 (f /. 1) .. (Rotate (f,(N-min (L~ f)))) >= 1 by A6, FINSEQ_4:21; then A14: (f /. 1) .. (Rotate (f,(N-min (L~ f)))) > 1 by A5, A8, XXREAL_0:1; k <= len (Rotate (f,(N-min (L~ f)))) by A9, FINSEQ_3:25; hence (Rotate (f,(N-min (L~ f)))) /. z <> f /. 1 by A8, A13, A14, GOBOARD7:37; ::_thesis: verum end; end; end; Rev f = Rev (Rotate ((Rotate (f,(N-min (L~ f)))),(f /. 1))) by A2, Th16 .= Rotate (h,(f /. 1)) by A4, FINSEQ_6:106 ; hence ( f is clockwise_oriented or Rev f is clockwise_oriented ) ; ::_thesis: verum end; end; end; end; end; end;