per cases ( 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;
suppose A1: 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: 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
A5: ((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 ;
A6: len f = len (Rotate (f,p)) by Th14;
i + 1 < i + 2 by XREAL_1:6;
then A7: i + 1 < len f by A3, A6, XXREAL_0:2;
A8: len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50;
per cases ( i + 1 = len (f :- p) or i + 1 < len (f :- p) or len (f :- p) < i + 1 ) by XXREAL_0:1;
suppose A9: 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 A8, NAT_1:11, XREAL_1:233
.= 1 ;
then A10: LSeg ((Rotate (f,p)),(len (f :- p))) = LSeg (f,1) by A1, A7, A9, Th31;
A11: i < len (f :- p) by A9, XREAL_1:29;
(i -' 1) + (p .. f) = (((((len f) - (p .. f)) + 1) - 1) - 1) + (p .. f) by A2, A8, A9, XREAL_1:233
.= (((len f) - (p .. f)) + (p .. f)) - 1
.= (len f) -' 1 by A4, XREAL_1:233, XXREAL_0:2 ;
then LSeg ((Rotate (f,p)),i) = LSeg (f,((len f) -' 1)) by A1, A2, A11, Th24;
hence (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {(f /. 1)} by A9, A10, Th30, GOBOARD7:34
.= {(f /. (len f))} by FINSEQ_6:def 1
.= {((Rotate (f,p)) /. (i + 1))} by A1, A9, Th11 ;
:: thesis: verum
end;
suppose A12: 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 A13: ((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 A14: 1 <= (i -' 1) + (p .. f) by XXREAL_0:2;
i + 0 < i + 1 by XREAL_1:6;
then i < len (f :- p) by A12, XXREAL_0:2;
then A15: LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f))) by A1, A2, Th24;
LSeg ((Rotate (f,p)),(i + 1)) = LSeg (f,(((i + 1) -' 1) + (p .. f))) by A1, A12, Th24, NAT_1:11;
hence (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {(f /. (((i + 1) -' 1) + (p .. f)))} by A5, A15, A14, A13, TOPREAL1:def 6
.= {((Rotate (f,p)) /. (i + 1))} by A1, A12, Th9, NAT_1:11 ;
:: thesis: verum
end;
suppose A16: 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, A6, XREAL_1:7;
then ((i + (p .. f)) + 2) - (len f) <= len f by XREAL_1:20;
then A17: ((i + (p .. f)) - (len f)) + 2 <= len f ;
(i + 1) + 1 <= len f by A3, Th14;
then A18: i + 1 < len f by NAT_1:13;
i + 1 > ((len f) - (p .. f)) + 1 by A1, A16, FINSEQ_5:50;
then (len f) - (p .. f) < i by XREAL_1:6;
then A19: len f < i + (p .. f) by XREAL_1:19;
then A20: (i + (p .. f)) -' (len f) = (i + (p .. f)) - (len f) by XREAL_1:233;
0 < (i + (p .. f)) - (len f) by A19, XREAL_1:50;
then A21: 0 + 1 <= (i + (p .. f)) -' (len f) by A20, NAT_1:13;
A22: ((i + 1) + (p .. f)) -' (len f) = ((i + (p .. f)) + 1) -' (len f)
.= ((i + (p .. f)) -' (len f)) + 1 by A19, NAT_D:38 ;
A23: len (f :- p) <= i by A16, NAT_1:13;
i + 0 < i + 1 by XREAL_1:6;
then i < len f by A18, XXREAL_0:2;
then A24: LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f))) by A1, A23, Th31;
LSeg ((Rotate (f,p)),(i + 1)) = LSeg (f,(((i + 1) + (p .. f)) -' (len f))) by A1, A16, A18, Th31;
hence (LSeg ((Rotate (f,p)),i)) /\ (LSeg ((Rotate (f,p)),(i + 1))) = {(f /. (((i + 1) + (p .. f)) -' (len f)))} by A24, A20, A21, A22, A17, TOPREAL1:def 6
.= {((Rotate (f,p)) /. (i + 1))} by A1, A7, A16, Th17 ;
:: thesis: verum
end;
end;
end;
end;
end;