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 not p in rng f ; :: thesis: ( f is_sequence_on G iff Rotate (f,p) is_sequence_on G )
hence ( f is_sequence_on G iff Rotate (f,p) is_sequence_on G ) by FINSEQ_6:def 2; :: thesis: verum
end;
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:21;
A5: 1 <= p .. f by A3, FINSEQ_4:21;
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 Nat st n in dom (Rotate (f,p)) holds
ex i, j being Nat st
( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) :: according to GOBOARD1:def 9 :: thesis: for b1 being set holds
( not b1 in dom (Rotate (f,p)) or not b1 + 1 in dom (Rotate (f,p)) or for b2, b3, b4, b5 being set 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 |.(b2 - b4).| + |.(b3 - b5).| = 1 ) )
proof
let n be Nat; :: thesis: ( n in dom (Rotate (f,p)) implies ex i, j being Nat st
( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) ) )
assume A7: n in dom (Rotate (f,p)) ; :: thesis: ex i, j being Nat st
( [i,j] in Indices G & (Rotate (f,p)) /. n = G * (i,j) )
then A8: 1 <= n by FINSEQ_3:25;
A9: n <= len (Rotate (f,p)) by A7, FINSEQ_3:25;
per cases ( len (f :- p) <= n or len (f :- p) >= n ) ;
suppose A10: len (f :- p) <= n ; :: thesis: ex i, j being 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:50;
then ((len f) -' (p .. f)) + 1 <= n by A4, XREAL_1:233;
then ((len f) + 1) -' (p .. f) <= n by A4, NAT_D:38;
then (len f) + 1 <= n + (p .. f) by NAT_D:52;
then A11: 1 <= (n + (p .. f)) -' (len f) by NAT_D:55;
n + (p .. f) <= (len f) + (len f) by A2, A4, A9, XREAL_1:7;
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, A11, FINSEQ_3:25;
then consider i, j being Nat such that
A12: [i,j] in Indices G and
A13: f /. ((n + (p .. f)) -' (len f)) = G * (i,j) by A1, A6;
take i ; :: thesis: ex j being 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 A12; :: thesis: (Rotate (f,p)) /. n = G * (i,j)
thus (Rotate (f,p)) /. n = G * (i,j) by A2, A3, A9, A10, A13, Th17; :: thesis: verum
end;
suppose A14: len (f :- p) >= n ; :: thesis: ex i, j being 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:50;
then ((len f) -' (p .. f)) + 1 >= n by A4, XREAL_1:233;
then n -' 1 <= (len f) -' (p .. f) by NAT_D:53;
then A15: (n -' 1) + (p .. f) <= len f by A4, NAT_D:54;
1 + 1 <= n + (p .. f) by A5, A8, XREAL_1:7;
then 1 <= (n + (p .. f)) -' 1 by NAT_D:55;
then 1 <= (n -' 1) + (p .. f) by A8, NAT_D:38;
then (n -' 1) + (p .. f) in dom (Rotate (f,p)) by A2, A15, FINSEQ_3:25;
then consider i, j being Nat such that
A16: [i,j] in Indices G and
A17: f /. ((n -' 1) + (p .. f)) = G * (i,j) by A1, A6;
take i ; :: thesis: ex j being 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 A16; :: thesis: (Rotate (f,p)) /. n = G * (i,j)
thus (Rotate (f,p)) /. n = G * (i,j) by A3, A8, A14, A17, Th9; :: thesis: verum
end;
end;
end;
let n be 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 set 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 |.(b1 - b3).| + |.(b2 - b4).| = 1 ) )
assume that
A18: n in dom (Rotate (f,p)) and
A19: n + 1 in dom (Rotate (f,p)) ; :: thesis: for b1, b2, b3, b4 being set 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 |.(b1 - b3).| + |.(b2 - b4).| = 1 )
A20: 1 <= n by A18, FINSEQ_3:25;
A21: n <= len f by A1, A18, FINSEQ_3:25;
A22: 1 <= n + 1 by A19, FINSEQ_3:25;
A23: n + 1 <= len f by A1, A19, FINSEQ_3:25;
let m, k, i, j be 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 |.(m - i).| + |.(k - j).| = 1 )
assume A24: ( [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: |.(m - i).| + |.(k - j).| = 1
thus |.(m - i).| + |.(k - j).| = 1 :: thesis: verum
proof
per cases ( len (f :- p) <= n or len (f :- p) > n ) ;
suppose A25: len (f :- p) <= n ; :: thesis: |.(m - i).| + |.(k - j).| = 1
((len f) - (p .. f)) + 1 <= n by A3, A25, FINSEQ_5:50;
then ((len f) -' (p .. f)) + 1 <= n by A4, XREAL_1:233;
then ((len f) + 1) -' (p .. f) <= n by A4, NAT_D:38;
then (len f) + 1 <= n + (p .. f) by NAT_D:52;
then A26: 1 <= (n + (p .. f)) -' (len f) by NAT_D:55;
n + (p .. f) <= (len f) + (len f) by A4, A21, XREAL_1:7;
then (n + (p .. f)) -' (len f) <= len f by NAT_D:53;
then A27: (n + (p .. f)) -' (len f) in dom f by A26, FINSEQ_3:25;
n <= n + 1 by NAT_1:11;
then A28: len (f :- p) <= n + 1 by A25, XXREAL_0:2;
then A29: ((len f) - (p .. f)) + 1 <= n + 1 by A3, FINSEQ_5:50;
then (len f) - (p .. f) <= n by XREAL_1:6;
then A30: len f <= n + (p .. f) by XREAL_1:20;
A31: (Rotate (f,p)) /. (n + 1) = f /. (((n + 1) + (p .. f)) -' (len f)) by A3, A23, A28, Th17;
A32: ((n + 1) + (p .. f)) -' (len f) = ((n + (p .. f)) + 1) -' (len f)
.= ((n + (p .. f)) -' (len f)) + 1 by A30, NAT_D:38 ;
((len f) -' (p .. f)) + 1 <= n + 1 by A4, A29, XREAL_1:233;
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 A33: 1 <= ((n + 1) + (p .. f)) -' (len f) by NAT_D:55;
(n + 1) + (p .. f) <= (len f) + (len f) by A4, A23, XREAL_1:7;
then ((n + 1) + (p .. f)) -' (len f) <= len f by NAT_D:53;
then A34: ((n + 1) + (p .. f)) -' (len f) in dom f by A33, FINSEQ_3:25;
(Rotate (f,p)) /. n = f /. ((n + (p .. f)) -' (len f)) by A3, A21, A25, Th17;
hence |.(m - i).| + |.(k - j).| = 1 by A6, A24, A31, A32, A27, A34; :: thesis: verum
end;
suppose A35: len (f :- p) > n ; :: thesis: |.(m - i).| + |.(k - j).| = 1
then n <= ((len f) - (p .. f)) + 1 by A3, FINSEQ_5:50;
then n <= ((len f) -' (p .. f)) + 1 by A4, XREAL_1:233;
then n -' 1 <= (len f) -' (p .. f) by NAT_D:53;
then A36: (n -' 1) + (p .. f) <= len f by A4, NAT_D:54;
1 + 1 <= n + (p .. f) by A5, A20, XREAL_1:7;
then 1 <= (n + (p .. f)) -' 1 by NAT_D:55;
then 1 <= (n -' 1) + (p .. f) by A20, NAT_D:38;
then A37: (n -' 1) + (p .. f) in dom f by A36, FINSEQ_3:25;
A38: ((n + 1) -' 1) + (p .. f) = n + (p .. f) by NAT_D:34
.= ((n -' 1) + 1) + (p .. f) by A20, XREAL_1:235
.= ((n -' 1) + (p .. f)) + 1 ;
A39: len (f :- p) >= n + 1 by A35, NAT_1:13;
then A40: (Rotate (f,p)) /. (n + 1) = f /. (((n + 1) -' 1) + (p .. f)) by A3, A22, Th9;
n + 1 <= ((len f) - (p .. f)) + 1 by A3, A39, FINSEQ_5:50;
then n + 1 <= ((len f) -' (p .. f)) + 1 by A4, XREAL_1:233;
then (n + 1) -' 1 <= (len f) -' (p .. f) by NAT_D:53;
then A41: ((n + 1) -' 1) + (p .. f) <= len f by A4, NAT_D:54;
1 + 1 <= (n + 1) + (p .. f) by A5, A22, XREAL_1:7;
then 1 <= ((n + 1) + (p .. f)) -' 1 by NAT_D:55;
then 1 <= ((n + 1) -' 1) + (p .. f) by A22, NAT_D:38;
then A42: ((n + 1) -' 1) + (p .. f) in dom f by A41, FINSEQ_3:25;
(Rotate (f,p)) /. n = f /. ((n -' 1) + (p .. f)) by A3, A20, A35, Th9;
hence |.(m - i).| + |.(k - j).| = 1 by A6, A24, A40, A38, A37, A42; :: thesis: verum
end;
end;
end;
end;
assume A43: Rotate (f,p) is_sequence_on G ; :: thesis: f is_sequence_on G
thus for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) ) :: according to GOBOARD1:def 9 :: thesis: for b1 being set holds
( not b1 in dom f or not b1 + 1 in dom f or for b2, b3, b4, b5 being set 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 |.(b2 - b4).| + |.(b3 - b5).| = 1 ) )
proof
let n be Nat; :: thesis: ( n in dom f implies ex i, j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) ) )
assume A44: n in dom f ; :: thesis: ex i, j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) )
then A45: 1 <= n by FINSEQ_3:25;
A46: n <= len f by A44, FINSEQ_3:25;
per cases ( n <= p .. f or n >= p .. f ) ;
suppose A47: n <= p .. f ; :: thesis: ex i, j being 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 A45, XXREAL_0:2;
then A48: 1 <= (n + (len f)) -' (p .. f) by A4, NAT_D:38;
n + (len f) <= (len f) + (p .. f) by A47, XREAL_1:6;
then (n + (len f)) -' (p .. f) <= len f by NAT_D:53;
then (n + (len f)) -' (p .. f) in dom f by A48, FINSEQ_3:25;
then consider i, j being Nat such that
A49: [i,j] in Indices G and
A50: (Rotate (f,p)) /. ((n + (len f)) -' (p .. f)) = G * (i,j) by A1, A43;
take i ; :: thesis: ex j being 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 A49; :: thesis: f /. n = G * (i,j)
thus f /. n = G * (i,j) by A3, A45, A47, A50, Th18; :: thesis: verum
end;
suppose A51: n >= p .. f ; :: thesis: ex i, j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) )
then 1 + (p .. f) <= n + 1 by XREAL_1:6;
then A52: 1 <= (n + 1) -' (p .. f) by NAT_D:55;
n + 1 <= (len f) + (p .. f) by A5, A46, XREAL_1:7;
then (n + 1) -' (p .. f) <= len f by NAT_D:53;
then (n + 1) -' (p .. f) in dom f by A52, FINSEQ_3:25;
then consider i, j being Nat such that
A53: [i,j] in Indices G and
A54: (Rotate (f,p)) /. ((n + 1) -' (p .. f)) = G * (i,j) by A1, A43;
take i ; :: thesis: ex j being 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 A53; :: thesis: f /. n = G * (i,j)
thus f /. n = G * (i,j) by A3, A46, A51, A54, Th10; :: thesis: verum
end;
end;
end;
let n be Nat; :: thesis: ( not n in dom f or not n + 1 in dom f or for b1, b2, b3, b4 being set 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 |.(b1 - b3).| + |.(b2 - b4).| = 1 ) )
assume that
A55: n in dom f and
A56: n + 1 in dom f ; :: thesis: for b1, b2, b3, b4 being set 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 |.(b1 - b3).| + |.(b2 - b4).| = 1 )
A57: 1 <= n by A55, FINSEQ_3:25;
A58: 1 <= n + 1 by A56, FINSEQ_3:25;
A59: n <= len f by A55, FINSEQ_3:25;
A60: n + 1 <= len f by A56, FINSEQ_3:25;
let m, k, i, j be 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 |.(m - i).| + |.(k - j).| = 1 )
assume A61: ( [m,k] in Indices G & [i,j] in Indices G & f /. n = G * (m,k) & f /. (n + 1) = G * (i,j) ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1
thus |.(m - i).| + |.(k - j).| = 1 :: thesis: verum
proof
per cases ( n < p .. f or n >= p .. f ) ;
suppose A62: n < p .. f ; :: thesis: |.(m - i).| + |.(k - j).| = 1
n <= n + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= n + ((len f) -' (p .. f)) by A57, XXREAL_0:2;
then A63: 1 <= (n + (len f)) -' (p .. f) by A4, NAT_D:38;
n + (len f) <= (len f) + (p .. f) by A62, XREAL_1:6;
then (n + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A64: (n + (len f)) -' (p .. f) in dom f by A63, FINSEQ_3:25;
A65: ((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 + 1 <= (n + 1) + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= (n + 1) + ((len f) -' (p .. f)) by A58, XXREAL_0:2;
then A66: 1 <= ((n + 1) + (len f)) -' (p .. f) by A4, NAT_D:38;
A67: n + 1 <= p .. f by A62, NAT_1:13;
then A68: f /. (n + 1) = (Rotate (f,p)) /. (((n + 1) + (len f)) -' (p .. f)) by A3, A58, Th18;
(n + 1) + (len f) <= (len f) + (p .. f) by A67, XREAL_1:6;
then ((n + 1) + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A69: ((n + 1) + (len f)) -' (p .. f) in dom f by A66, FINSEQ_3:25;
f /. n = (Rotate (f,p)) /. ((n + (len f)) -' (p .. f)) by A3, A57, A62, Th18;
hence |.(m - i).| + |.(k - j).| = 1 by A1, A43, A61, A68, A65, A64, A69; :: thesis: verum
end;
suppose A70: n >= p .. f ; :: thesis: |.(m - i).| + |.(k - j).| = 1
then 1 + (p .. f) <= n + 1 by XREAL_1:6;
then A71: 1 <= (n + 1) -' (p .. f) by NAT_D:55;
n + 1 <= (len f) + (p .. f) by A5, A59, XREAL_1:7;
then (n + 1) -' (p .. f) <= len f by NAT_D:53;
then A72: (n + 1) -' (p .. f) in dom f by A71, FINSEQ_3:25;
A73: f /. n = (Rotate (f,p)) /. ((n + 1) -' (p .. f)) by A3, A59, A70, Th10;
A74: n <= n + 1 by NAT_1:11;
then A75: ((n + 1) + 1) -' (p .. f) = ((n + 1) -' (p .. f)) + 1 by A70, NAT_D:38, XXREAL_0:2;
A76: n + 1 >= p .. f by A70, A74, XXREAL_0:2;
then 1 + (p .. f) <= (n + 1) + 1 by XREAL_1:6;
then A77: 1 <= ((n + 1) + 1) -' (p .. f) by NAT_D:55;
(n + 1) + 1 <= (len f) + (p .. f) by A5, A60, XREAL_1:7;
then ((n + 1) + 1) -' (p .. f) <= len f by NAT_D:53;
then A78: ((n + 1) + 1) -' (p .. f) in dom f by A77, FINSEQ_3:25;
f /. (n + 1) = (Rotate (f,p)) /. (((n + 1) + 1) -' (p .. f)) by A3, A60, A76, Th10;
hence |.(m - i).| + |.(k - j).| = 1 by A1, A43, A61, A73, A75, A78, A72; :: thesis: verum
end;
end;
end;
end;
end;