set h = Rotate (f,p);
per cases ( 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;
suppose that 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 Nat; :: according to GOBOARD5:def 4 :: thesis: for b1 being set 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 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 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)
per cases ( 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) ; :: thesis: verum
end;
suppose that 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;
suppose that 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)
per cases ( 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;
suppose A24: j + 1 < len f ; :: thesis: j + 1 < (i -' 1) + (len f)
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)
per cases ( 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;
suppose A30: 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;