begin
definition
let G be
Matrix of
(TOP-REAL 2);
let i be
Nat;
func v_strip (
G,
i)
-> Subset of
(TOP-REAL 2) equals :
Def1:
{ |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } if ( 1
<= i &
i < len G )
{ |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } if i >= len G otherwise { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ;
coherence
( ( 1 <= i & i < len G implies { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } is Subset of (TOP-REAL 2) ) & ( i >= len G implies { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len G ) & not i >= len G implies { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2) ) )
correctness
consistency
for b1 being Subset of (TOP-REAL 2) st 1 <= i & i < len G & i >= len G holds
( b1 = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } iff b1 = { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } );
;
func h_strip (
G,
i)
-> Subset of
(TOP-REAL 2) equals :
Def2:
{ |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } if ( 1
<= i &
i < width G )
{ |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } if i >= width G otherwise { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ;
coherence
( ( 1 <= i & i < width G implies { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } is Subset of (TOP-REAL 2) ) & ( i >= width G implies { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < width G ) & not i >= width G implies { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) ) )
correctness
consistency
for b1 being Subset of (TOP-REAL 2) st 1 <= i & i < width G & i >= width G holds
( b1 = { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } iff b1 = { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } );
;
end;
::
deftheorem Def1 defines
v_strip GOBOARD5:def 1 :
for G being Matrix of (TOP-REAL 2)
for i being Nat holds
( ( 1 <= i & i < len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } ) & ( i >= len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } ) & ( ( not 1 <= i or not i < len G ) & not i >= len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ) );
::
deftheorem Def2 defines
h_strip GOBOARD5:def 2 :
for G being Matrix of (TOP-REAL 2)
for i being Nat holds
( ( 1 <= i & i < width G implies h_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } ) & ( i >= width G implies h_strip (G,i) = { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } ) & ( ( not 1 <= i or not i < width G ) & not i >= width G implies h_strip (G,i) = { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ) );
Lm1:
for f being FinSequence of (TOP-REAL 2) holds dom (X_axis f) = dom f
Lm2:
for f being FinSequence of (TOP-REAL 2) holds dom (Y_axis f) = dom f
definition
let f be
standard special_circular_sequence;
let k be
Element of
NAT ;
assume that A1:
1
<= k
and A2:
k + 1
<= len f
;
k <= k + 1
by NAT_1:11;
then
k <= len f
by A2, XXREAL_0:2;
then A3:
k in dom f
by A1, FINSEQ_3:25;
then consider i1,
j1 being
Element of
NAT such that A4:
[i1,j1] in Indices (GoB f)
and A5:
f /. k = (GoB f) * (
i1,
j1)
by Th11;
k + 1
>= 1
by NAT_1:11;
then A6:
k + 1
in dom f
by A2, FINSEQ_3:25;
then consider i2,
j2 being
Element of
NAT such that A7:
[i2,j2] in Indices (GoB f)
and A8:
f /. (k + 1) = (GoB f) * (
i2,
j2)
by Th11;
A9:
(abs (i1 - i2)) + (abs (j1 - j2)) = 1
by A3, A4, A5, A6, A7, A8, Th12;
A10:
now ( ( abs (i1 - i2) = 1 & j1 = j2 & ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 ) or ( i1 = i2 & abs (j1 - j2) = 1 & ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 ) )
per cases
( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( i1 = i2 & abs (j1 - j2) = 1 ) )
by A9, SEQM_3:42;
case that A11:
abs (i1 - i2) = 1
and A12:
j1 = j2
;
( ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 )
end;
case that A13:
i1 = i2
and A14:
abs (j1 - j2) = 1
;
( ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 )
end;
end;
end;
func right_cell (
f,
k)
-> Subset of
(TOP-REAL 2) means :
Def6:
for
i1,
j1,
i2,
j2 being
Element of
NAT st
[i1,j1] in Indices (GoB f) &
[i2,j2] in Indices (GoB f) &
f /. k = (GoB f) * (
i1,
j1) &
f /. (k + 1) = (GoB f) * (
i2,
j2) & not (
i1 = i2 &
j1 + 1
= j2 &
it = cell (
(GoB f),
i1,
j1) ) & not (
i1 + 1
= i2 &
j1 = j2 &
it = cell (
(GoB f),
i1,
(j1 -' 1)) ) & not (
i1 = i2 + 1 &
j1 = j2 &
it = cell (
(GoB f),
i2,
j2) ) holds
(
i1 = i2 &
j1 = j2 + 1 &
it = cell (
(GoB f),
(i1 -' 1),
j2) );
existence
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) )
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell ((GoB f),(i1 -' 1),j2) ) ) holds
b1 = b2
func left_cell (
f,
k)
-> Subset of
(TOP-REAL 2) means :
Def7:
for
i1,
j1,
i2,
j2 being
Element of
NAT st
[i1,j1] in Indices (GoB f) &
[i2,j2] in Indices (GoB f) &
f /. k = (GoB f) * (
i1,
j1) &
f /. (k + 1) = (GoB f) * (
i2,
j2) & not (
i1 = i2 &
j1 + 1
= j2 &
it = cell (
(GoB f),
(i1 -' 1),
j1) ) & not (
i1 + 1
= i2 &
j1 = j2 &
it = cell (
(GoB f),
i1,
j1) ) & not (
i1 = i2 + 1 &
j1 = j2 &
it = cell (
(GoB f),
i2,
(j2 -' 1)) ) holds
(
i1 = i2 &
j1 = j2 + 1 &
it = cell (
(GoB f),
i1,
j2) );
existence
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) )
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell ((GoB f),i1,j2) ) ) holds
b1 = b2
end;
::
deftheorem Def6 defines
right_cell GOBOARD5:def 6 :
for f being standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
for b3 being Subset of (TOP-REAL 2) holds
( b3 = right_cell (f,k) iff for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b3 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b3 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b3 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b3 = cell ((GoB f),(i1 -' 1),j2) ) );
::
deftheorem Def7 defines
left_cell GOBOARD5:def 7 :
for f being standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
for b3 being Subset of (TOP-REAL 2) holds
( b3 = left_cell (f,k) iff for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b3 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b3 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b3 = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b3 = cell ((GoB f),i1,j2) ) );
theorem Th27:
for
k,
i,
j being
Element of
NAT for
f being
standard special_circular_sequence st 1
<= k &
k + 1
<= len f &
[(i + 1),j] in Indices (GoB f) &
[(i + 1),(j + 1)] in Indices (GoB f) &
f /. k = (GoB f) * (
(i + 1),
j) &
f /. (k + 1) = (GoB f) * (
(i + 1),
(j + 1)) holds
(
left_cell (
f,
k)
= cell (
(GoB f),
i,
j) &
right_cell (
f,
k)
= cell (
(GoB f),
(i + 1),
j) )
theorem Th28:
for
k,
i,
j being
Element of
NAT for
f being
standard special_circular_sequence st 1
<= k &
k + 1
<= len f &
[i,(j + 1)] in Indices (GoB f) &
[(i + 1),(j + 1)] in Indices (GoB f) &
f /. k = (GoB f) * (
i,
(j + 1)) &
f /. (k + 1) = (GoB f) * (
(i + 1),
(j + 1)) holds
(
left_cell (
f,
k)
= cell (
(GoB f),
i,
(j + 1)) &
right_cell (
f,
k)
= cell (
(GoB f),
i,
j) )
theorem Th29:
for
k,
i,
j being
Element of
NAT for
f being
standard special_circular_sequence st 1
<= k &
k + 1
<= len f &
[i,(j + 1)] in Indices (GoB f) &
[(i + 1),(j + 1)] in Indices (GoB f) &
f /. k = (GoB f) * (
(i + 1),
(j + 1)) &
f /. (k + 1) = (GoB f) * (
i,
(j + 1)) holds
(
left_cell (
f,
k)
= cell (
(GoB f),
i,
j) &
right_cell (
f,
k)
= cell (
(GoB f),
i,
(j + 1)) )
theorem Th30:
for
k,
i,
j being
Element of
NAT for
f being
standard special_circular_sequence st 1
<= k &
k + 1
<= len f &
[(i + 1),(j + 1)] in Indices (GoB f) &
[(i + 1),j] in Indices (GoB f) &
f /. k = (GoB f) * (
(i + 1),
(j + 1)) &
f /. (k + 1) = (GoB f) * (
(i + 1),
j) holds
(
left_cell (
f,
k)
= cell (
(GoB f),
(i + 1),
j) &
right_cell (
f,
k)
= cell (
(GoB f),
i,
j) )