per cases ( 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;
suppose A1: 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;
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 )
A6: len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50;
per cases ( i < len (f :- p) or i >= len (f :- p) ) ;
suppose A7: 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 )
A8: ((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 A7, NAT_1:13;
then A9: (Rotate (f,p)) /. (i + 1) = f /. (((i -' 1) + (p .. f)) + 1) by A1, A8, Th9, NAT_1:11;
( 0 <= i -' 1 & 1 <= p .. f ) by A1, FINSEQ_4:21;
then A10: 1 + 0 <= (i -' 1) + (p .. f) by XREAL_1:7;
i < ((len f) + 1) - (p .. f) by A6, A7;
then i + (p .. f) < (len f) + 1 by XREAL_1:20;
then i + (p .. f) <= len f by NAT_1:13;
then A11: ((i -' 1) + 1) + (p .. f) <= len f by A3, XREAL_1:235;
(Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) by A1, A3, A7, 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 A9, A10, A11, TOPREAL1:def 5; :: thesis: verum
end;
suppose A12: 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 A13: (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) by A1, A12, Th17;
i - ((len f) - (p .. f)) >= 1 by A6, A12, XREAL_1:19;
then (i + (p .. f)) - (len f) >= 1 ;
then A14: 1 <= (i + (p .. f)) -' (len f) by NAT_D:39;
A15: i + 1 >= len (f :- p) by A5, A12, XXREAL_0:2;
then i >= (len f) - (p .. f) by A6, XREAL_1:6;
then A16: 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 A16, NAT_D:38 ;
then A17: (Rotate (f,p)) /. (i + 1) = f /. (((i + (p .. f)) -' (len f)) + 1) by A1, A4, A2, A15, 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 A16, 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 A13, A17, A14, 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;