:: 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;