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;
per cases
( not p in rng f or p in rng f )
;
suppose A3:
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:31;
A5:
1
<= p .. f
by A3, FINSEQ_4:31;
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 11 :: 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
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 A7:
( 1
<= n &
n <= len (Rotate f,p) )
by FINSEQ_3:27;
per cases
( len (f :- p) <= n or len (f :- p) >= n )
;
suppose A8:
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:53;
then
((len f) -' (p .. f)) + 1
<= n
by A4, XREAL_1:235;
then
((len f) + 1) -' (p .. f) <= n
by A4, NAT_D:38;
then
(len f) + 1
<= n + (p .. f)
by NAT_D:52;
then A9:
1
<= (n + (p .. f)) -' (len f)
by NAT_D:55;
n + (p .. f) <= (len f) + (len f)
by A2, A4, A7, XREAL_1:9;
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, A9, FINSEQ_3:27;
then consider i,
j being
Element of
NAT such that A10:
[i,j] in Indices G
and A11:
f /. ((n + (p .. f)) -' (len f)) = G * i,
j
by A1, A6, GOBOARD1:def 11;
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 A10;
:: thesis: (Rotate f,p) /. n = G * i,jthus
(Rotate f,p) /. n = G * i,
j
by A2, A3, A7, A8, A11, Th17;
:: thesis: verum end; suppose A12:
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 )
1
+ 1
<= n + (p .. f)
by A5, A7, XREAL_1:9;
then
1
<= (n + (p .. f)) -' 1
by NAT_D:55;
then A13:
1
<= (n -' 1) + (p .. f)
by A7, NAT_D:38;
((len f) - (p .. f)) + 1
>= n
by A3, A12, FINSEQ_5:53;
then
((len f) -' (p .. f)) + 1
>= n
by A4, XREAL_1:235;
then
n -' 1
<= (len f) -' (p .. f)
by NAT_D:53;
then
(n -' 1) + (p .. f) <= len f
by A4, NAT_D:54;
then
(n -' 1) + (p .. f) in dom (Rotate f,p)
by A2, A13, FINSEQ_3:27;
then consider i,
j being
Element of
NAT such that A14:
[i,j] in Indices G
and A15:
f /. ((n -' 1) + (p .. f)) = G * i,
j
by A1, A6, GOBOARD1:def 11;
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 A14;
:: thesis: (Rotate f,p) /. n = G * i,jthus
(Rotate f,p) /. n = G * i,
j
by A3, A7, A12, A15, Th9;
:: thesis: verum
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 A16:
n in dom (Rotate f,p)
and A17:
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 )
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 A18:
(
[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
A19:
( 1
<= n &
n <= len f )
by A1, A16, FINSEQ_3:27;
A20:
( 1
<= n + 1 &
n + 1
<= len f )
by A1, A17, FINSEQ_3:27;
thus
(abs (m - i)) + (abs (k - j)) = 1
:: thesis: verumproof
per cases
( len (f :- p) <= n or len (f :- p) > n )
;
suppose A21:
len (f :- p) <= n
;
:: thesis: (abs (m - i)) + (abs (k - j)) = 1
n <= n + 1
by NAT_1:11;
then A22:
len (f :- p) <= n + 1
by A21, XXREAL_0:2;
A23:
(Rotate f,p) /. n = f /. ((n + (p .. f)) -' (len f))
by A3, A19, A21, Th17;
A24:
(Rotate f,p) /. (n + 1) = f /. (((n + 1) + (p .. f)) -' (len f))
by A3, A20, A22, Th17;
A25:
((len f) - (p .. f)) + 1
<= n + 1
by A3, A22, FINSEQ_5:53;
then
(len f) - (p .. f) <= n
by XREAL_1:8;
then A26:
len f <= n + (p .. f)
by XREAL_1:22;
A27:
((n + 1) + (p .. f)) -' (len f) =
((n + (p .. f)) + 1) -' (len f)
.=
((n + (p .. f)) -' (len f)) + 1
by A26, NAT_D:38
;
((len f) - (p .. f)) + 1
<= n
by A3, A21, FINSEQ_5:53;
then
((len f) -' (p .. f)) + 1
<= n
by A4, XREAL_1:235;
then
((len f) + 1) -' (p .. f) <= n
by A4, NAT_D:38;
then
(len f) + 1
<= n + (p .. f)
by NAT_D:52;
then A28:
1
<= (n + (p .. f)) -' (len f)
by NAT_D:55;
n + (p .. f) <= (len f) + (len f)
by A4, A19, XREAL_1:9;
then
(n + (p .. f)) -' (len f) <= len f
by NAT_D:53;
then A29:
(n + (p .. f)) -' (len f) in dom f
by A28, FINSEQ_3:27;
((len f) -' (p .. f)) + 1
<= n + 1
by A4, A25, XREAL_1:235;
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 A30:
1
<= ((n + 1) + (p .. f)) -' (len f)
by NAT_D:55;
(n + 1) + (p .. f) <= (len f) + (len f)
by A4, A20, XREAL_1:9;
then
((n + 1) + (p .. f)) -' (len f) <= len f
by NAT_D:53;
then
((n + 1) + (p .. f)) -' (len f) in dom f
by A30, FINSEQ_3:27;
hence
(abs (m - i)) + (abs (k - j)) = 1
by A6, A18, A23, A24, A27, A29, GOBOARD1:def 11;
:: thesis: verum end; suppose A31:
len (f :- p) > n
;
:: thesis: (abs (m - i)) + (abs (k - j)) = 1then A32:
len (f :- p) >= n + 1
by NAT_1:13;
A33:
(Rotate f,p) /. n = f /. ((n -' 1) + (p .. f))
by A3, A19, A31, Th9;
A34:
(Rotate f,p) /. (n + 1) = f /. (((n + 1) -' 1) + (p .. f))
by A3, A20, A32, Th9;
A35:
((n + 1) -' 1) + (p .. f) =
n + (p .. f)
by NAT_D:34
.=
((n -' 1) + 1) + (p .. f)
by A19, XREAL_1:237
.=
((n -' 1) + (p .. f)) + 1
;
1
+ 1
<= n + (p .. f)
by A5, A19, XREAL_1:9;
then
1
<= (n + (p .. f)) -' 1
by NAT_D:55;
then A36:
1
<= (n -' 1) + (p .. f)
by A19, NAT_D:38;
n <= ((len f) - (p .. f)) + 1
by A3, A31, FINSEQ_5:53;
then
n <= ((len f) -' (p .. f)) + 1
by A4, XREAL_1:235;
then
n -' 1
<= (len f) -' (p .. f)
by NAT_D:53;
then
(n -' 1) + (p .. f) <= len f
by A4, NAT_D:54;
then A37:
(n -' 1) + (p .. f) in dom f
by A36, FINSEQ_3:27;
1
+ 1
<= (n + 1) + (p .. f)
by A5, A20, XREAL_1:9;
then
1
<= ((n + 1) + (p .. f)) -' 1
by NAT_D:55;
then A38:
1
<= ((n + 1) -' 1) + (p .. f)
by A20, NAT_D:38;
n + 1
<= ((len f) - (p .. f)) + 1
by A3, A32, FINSEQ_5:53;
then
n + 1
<= ((len f) -' (p .. f)) + 1
by A4, XREAL_1:235;
then
(n + 1) -' 1
<= (len f) -' (p .. f)
by NAT_D:53;
then
((n + 1) -' 1) + (p .. f) <= len f
by A4, NAT_D:54;
then
((n + 1) -' 1) + (p .. f) in dom f
by A38, FINSEQ_3:27;
hence
(abs (m - i)) + (abs (k - j)) = 1
by A6, A18, A33, A34, A35, A37, GOBOARD1:def 11;
:: thesis: verum end;
end;
end; assume A39:
Rotate f,
p is_sequence_on G
;
:: thesis: f is_sequence_on Gthus
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 11 :: 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
n in dom f
;
:: thesis: ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * i,j )
then A40:
( 1
<= n &
n <= len f )
by FINSEQ_3:27;
per cases
( n <= p .. f or n >= p .. f )
;
suppose A41:
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 A40, XXREAL_0:2;
then A42:
1
<= (n + (len f)) -' (p .. f)
by A4, NAT_D:38;
n + (len f) <= (len f) + (p .. f)
by A41, XREAL_1:8;
then
(n + (len f)) -' (p .. f) <= len f
by NAT_D:53;
then
(n + (len f)) -' (p .. f) in dom f
by A42, FINSEQ_3:27;
then consider i,
j being
Element of
NAT such that A43:
[i,j] in Indices G
and A44:
(Rotate f,p) /. ((n + (len f)) -' (p .. f)) = G * i,
j
by A1, A39, GOBOARD1:def 11;
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 A43;
:: thesis: f /. n = G * i,jthus
f /. n = G * i,
j
by A3, A40, A41, A44, Th18;
:: thesis: verum end; suppose A45:
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:8;
then A46:
1
<= (n + 1) -' (p .. f)
by NAT_D:55;
n + 1
<= (len f) + (p .. f)
by A5, A40, XREAL_1:9;
then
(n + 1) -' (p .. f) <= len f
by NAT_D:53;
then
(n + 1) -' (p .. f) in dom f
by A46, FINSEQ_3:27;
then consider i,
j being
Element of
NAT such that A47:
[i,j] in Indices G
and A48:
(Rotate f,p) /. ((n + 1) -' (p .. f)) = G * i,
j
by A1, A39, GOBOARD1:def 11;
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 A47;
:: thesis: f /. n = G * i,jthus
f /. n = G * i,
j
by A3, A40, A45, A48, Th10;
:: thesis: verum 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 A49:
n in dom f
and A50:
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 )A51:
( 1
<= n &
n <= len f )
by A49, FINSEQ_3:27;
A52:
( 1
<= n + 1 &
n + 1
<= len f )
by A50, FINSEQ_3:27;
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 that A53:
[m,k] in Indices G
and A54:
[i,j] in Indices G
and A55:
f /. n = G * m,
k
and A56:
f /. (n + 1) = G * i,
j
;
:: thesis: (abs (m - i)) + (abs (k - j)) = 1thus
(abs (m - i)) + (abs (k - j)) = 1
:: thesis: verumproof
per cases
( n < p .. f or n >= p .. f )
;
suppose A57:
n < p .. f
;
:: thesis: (abs (m - i)) + (abs (k - j)) = 1then A58:
n + 1
<= p .. f
by NAT_1:13;
A59:
f /. n = (Rotate f,p) /. ((n + (len f)) -' (p .. f))
by A3, A51, A57, Th18;
A60:
f /. (n + 1) = (Rotate f,p) /. (((n + 1) + (len f)) -' (p .. f))
by A3, A52, A58, Th18;
A61:
((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 <= n + ((len f) -' (p .. f))
by NAT_1:11;
then
1
<= n + ((len f) -' (p .. f))
by A51, XXREAL_0:2;
then A62:
1
<= (n + (len f)) -' (p .. f)
by A4, NAT_D:38;
n + (len f) <= (len f) + (p .. f)
by A57, XREAL_1:8;
then
(n + (len f)) -' (p .. f) <= len f
by NAT_D:53;
then A63:
(n + (len f)) -' (p .. f) in dom f
by A62, FINSEQ_3:27;
n + 1
<= (n + 1) + ((len f) -' (p .. f))
by NAT_1:11;
then
1
<= (n + 1) + ((len f) -' (p .. f))
by A52, XXREAL_0:2;
then A64:
1
<= ((n + 1) + (len f)) -' (p .. f)
by A4, NAT_D:38;
(n + 1) + (len f) <= (len f) + (p .. f)
by A58, XREAL_1:8;
then
((n + 1) + (len f)) -' (p .. f) <= len f
by NAT_D:53;
then
((n + 1) + (len f)) -' (p .. f) in dom f
by A64, FINSEQ_3:27;
hence
(abs (m - i)) + (abs (k - j)) = 1
by A1, A39, A53, A54, A55, A56, A59, A60, A61, A63, GOBOARD1:def 11;
:: thesis: verum end; suppose A65:
n >= p .. f
;
:: thesis: (abs (m - i)) + (abs (k - j)) = 1A66:
n <= n + 1
by NAT_1:11;
then A67:
n + 1
>= p .. f
by A65, XXREAL_0:2;
then A68:
f /. (n + 1) = (Rotate f,p) /. (((n + 1) + 1) -' (p .. f))
by A3, A52, Th10;
A69:
f /. n = (Rotate f,p) /. ((n + 1) -' (p .. f))
by A3, A51, A65, Th10;
A70:
((n + 1) + 1) -' (p .. f) = ((n + 1) -' (p .. f)) + 1
by A65, A66, NAT_D:38, XXREAL_0:2;
1
+ (p .. f) <= (n + 1) + 1
by A67, XREAL_1:8;
then A71:
1
<= ((n + 1) + 1) -' (p .. f)
by NAT_D:55;
(n + 1) + 1
<= (len f) + (p .. f)
by A5, A52, XREAL_1:9;
then
((n + 1) + 1) -' (p .. f) <= len f
by NAT_D:53;
then A72:
((n + 1) + 1) -' (p .. f) in dom f
by A71, FINSEQ_3:27;
1
+ (p .. f) <= n + 1
by A65, XREAL_1:8;
then A73:
1
<= (n + 1) -' (p .. f)
by NAT_D:55;
n + 1
<= (len f) + (p .. f)
by A5, A51, XREAL_1:9;
then
(n + 1) -' (p .. f) <= len f
by NAT_D:53;
then
(n + 1) -' (p .. f) in dom f
by A73, FINSEQ_3:27;
hence
(abs (m - i)) + (abs (k - j)) = 1
by A1, A39, A53, A54, A55, A56, A68, A69, A70, A72, GOBOARD1:def 11;
:: thesis: verum end;
end; end;