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 that A1:
p in rng f
and A2:
p .. f <> 1
and A3:
p .. f <> len f
;
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;
GOBOARD5:def 4 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;
( 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)) )
;
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 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 that A14:
i >= 1
and A15:
j < len (f :- p)
;
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;
verum end; suppose that A21:
i >= 1
and A22:
j >= len (f :- p)
and A23:
i < len (f :- p)
;
LSeg ((Rotate (f,p)),i) misses LSeg ((Rotate (f,p)),j)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 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
;
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;
verum end; end; end; hence
LSeg (
(Rotate (f,p)),
i)
misses LSeg (
(Rotate (f,p)),
j)
;
verum end; suppose A30:
i >= len (f :- p)
;
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;
verum end; end; end; hence
LSeg (
(Rotate (f,p)),
i)
misses LSeg (
(Rotate (f,p)),
j)
;
verum end; end;