:: by Yatsuka Nakamura and Andrzej Trybulec

::

:: Received May 26, 1995

:: Copyright (c) 1995-2018 Association of Mizar Users

definition

let G be Matrix of (TOP-REAL 2);

let i be Nat;

( ( 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) ) )

consistency

for b_{1} being Subset of (TOP-REAL 2) st 1 <= i & i < len G & i >= len G holds

( b_{1} = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } iff b_{1} = { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } );

;

( ( 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) ) )

consistency

for b_{1} being Subset of (TOP-REAL 2) st 1 <= i & i < width G & i >= width G holds

( b_{1} = { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } iff b_{1} = { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } );

;

end;
let i be Nat;

func v_strip (G,i) -> Subset of (TOP-REAL 2) equals :Def1: :: GOBOARD5:def 1

{ |[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 { |[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 } ;

( ( 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) ) )

proof end;

correctness consistency

for b

( b

;

func h_strip (G,i) -> Subset of (TOP-REAL 2) equals :Def2: :: GOBOARD5:def 2

{ |[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 { |[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 } ;

( ( 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) ) )

proof end;

correctness consistency

for b

( b

;

:: 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 } ) );

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 } ) );

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 } ) );

theorem Th1: :: GOBOARD5:1

for i, j being Nat

for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G holds

(G * (i,j)) `2 = (G * (1,j)) `2

for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G holds

(G * (i,j)) `2 = (G * (1,j)) `2

proof end;

theorem Th2: :: GOBOARD5:2

for i, j being Nat

for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G holds

(G * (i,j)) `1 = (G * (i,1)) `1

for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G holds

(G * (i,j)) `1 = (G * (i,1)) `1

proof end;

theorem Th3: :: GOBOARD5:3

for i1, i2, j being Nat

for G being Matrix of (TOP-REAL 2) st G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds

(G * (i1,j)) `1 < (G * (i2,j)) `1

for G being Matrix of (TOP-REAL 2) st G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds

(G * (i1,j)) `1 < (G * (i2,j)) `1

proof end;

theorem Th4: :: GOBOARD5:4

for i, j1, j2 being Nat

for G being Matrix of (TOP-REAL 2) st G is Y_increasing-in-line & 1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G holds

(G * (i,j1)) `2 < (G * (i,j2)) `2

for G being Matrix of (TOP-REAL 2) st G is Y_increasing-in-line & 1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G holds

(G * (i,j1)) `2 < (G * (i,j2)) `2

proof end;

theorem Th5: :: GOBOARD5:5

for i, j being Nat

for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G holds

h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }

for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G holds

h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) }

proof end;

theorem Th6: :: GOBOARD5:6

for i being Nat

for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds

h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s }

for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds

h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s }

proof end;

theorem Th7: :: GOBOARD5:7

for i being Nat

for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds

h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 }

for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds

h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 }

proof end;

theorem Th8: :: GOBOARD5:8

for i, j being Nat

for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G holds

v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) }

for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G holds

v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) }

proof end;

theorem Th9: :: GOBOARD5:9

for j being Nat

for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds

v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r }

for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds

v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r }

proof end;

theorem Th10: :: GOBOARD5:10

for j being Nat

for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds

v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 }

for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds

v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 }

proof end;

definition

let G be Matrix of (TOP-REAL 2);

let i, j be Nat;

coherence

(v_strip (G,i)) /\ (h_strip (G,j)) is Subset of (TOP-REAL 2);

;

end;
let i, j be Nat;

func cell (G,i,j) -> Subset of (TOP-REAL 2) equals :: GOBOARD5:def 3

(v_strip (G,i)) /\ (h_strip (G,j));

correctness (v_strip (G,i)) /\ (h_strip (G,j));

coherence

(v_strip (G,i)) /\ (h_strip (G,j)) is Subset of (TOP-REAL 2);

;

:: deftheorem defines cell GOBOARD5:def 3 :

for G being Matrix of (TOP-REAL 2)

for i, j being Nat holds cell (G,i,j) = (v_strip (G,i)) /\ (h_strip (G,j));

for G being Matrix of (TOP-REAL 2)

for i, j being Nat holds cell (G,i,j) = (v_strip (G,i)) /\ (h_strip (G,j));

:: deftheorem defines s.c.c. GOBOARD5:def 4 :

for IT being FinSequence of (TOP-REAL 2) holds

( IT is s.c.c. iff for i, j being Nat st i + 1 < j & ( ( i > 1 & j < len IT ) or j + 1 < len IT ) holds

LSeg (IT,i) misses LSeg (IT,j) );

for IT being FinSequence of (TOP-REAL 2) holds

( IT is s.c.c. iff for i, j being Nat st i + 1 < j & ( ( i > 1 & j < len IT ) or j + 1 < len IT ) holds

LSeg (IT,i) misses LSeg (IT,j) );

:: deftheorem Def5 defines standard GOBOARD5:def 5 :

for IT being non empty FinSequence of (TOP-REAL 2) holds

( IT is standard iff IT is_sequence_on GoB IT );

for IT being non empty FinSequence of (TOP-REAL 2) holds

( IT is standard iff IT is_sequence_on GoB IT );

reconsider jj = 1, zz = 0 as Element of REAL by XREAL_0:def 1;

registration

ex b_{1} being non empty FinSequence of (TOP-REAL 2) st

( not b_{1} is constant & b_{1} is special & b_{1} is unfolded & b_{1} is circular & b_{1} is s.c.c. & b_{1} is standard )
end;

cluster V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non constant non empty V39() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard for FinSequence of (TOP-REAL 2);

existence ex b

( not b

proof end;

Lm1: for f being FinSequence of (TOP-REAL 2) holds dom (X_axis f) = dom f

proof end;

Lm2: for f being FinSequence of (TOP-REAL 2) holds dom (Y_axis f) = dom f

proof end;

theorem Th11: :: GOBOARD5:11

for f being non empty FinSequence of (TOP-REAL 2)

for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )

for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )

proof end;

theorem Th12: :: GOBOARD5:12

for f being non empty standard FinSequence of (TOP-REAL 2)

for n being Nat st n in dom f & n + 1 in dom f holds

for m, k, i, j being Nat st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds

|.(m - i).| + |.(k - j).| = 1

for n being Nat st n in dom f & n + 1 in dom f holds

for m, k, i, j being Nat st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds

|.(m - i).| + |.(k - j).| = 1

proof end;

definition

mode special_circular_sequence is non empty circular special unfolded s.c.c. FinSequence of (TOP-REAL 2);

end;
definition

let f be standard special_circular_sequence;

let k be 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 Nat such that

A4: [i1,j1] in Indices (GoB f) and

A5: f /. k = (GoB f) * (i1,j1) by Th11;

A6: k + 1 in dom f by A2, FINSEQ_3:25, NAT_1:11;

then consider i2, j2 being Nat such that

A7: [i2,j2] in Indices (GoB f) and

A8: f /. (k + 1) = (GoB f) * (i2,j2) by Th11;

A9: |.(i1 - i2).| + |.(j1 - j2).| = 1 by A3, A4, A5, A6, A7, A8, Th12;

ex b_{1} being Subset of (TOP-REAL 2) st

for i1, j1, i2, j2 being 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 & b_{1} = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell ((GoB f),i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell ((GoB f),(i1 -' 1),j2) )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being 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 & b_{1} = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell ((GoB f),i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell ((GoB f),(i1 -' 1),j2) ) ) & ( for i1, j1, i2, j2 being 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 & b_{2} = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{2} = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{2} = cell ((GoB f),i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{2} = cell ((GoB f),(i1 -' 1),j2) ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of (TOP-REAL 2) st

for i1, j1, i2, j2 being 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 & b_{1} = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell ((GoB f),i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell ((GoB f),i1,j2) )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being 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 & b_{1} = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell ((GoB f),i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell ((GoB f),i1,j2) ) ) & ( for i1, j1, i2, j2 being 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 & b_{2} = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{2} = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{2} = cell ((GoB f),i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{2} = cell ((GoB f),i1,j2) ) ) holds

b_{1} = b_{2}

end;
let k be 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 Nat such that

A4: [i1,j1] in Indices (GoB f) and

A5: f /. k = (GoB f) * (i1,j1) by Th11;

A6: k + 1 in dom f by A2, FINSEQ_3:25, NAT_1:11;

then consider i2, j2 being Nat such that

A7: [i2,j2] in Indices (GoB f) and

A8: f /. (k + 1) = (GoB f) * (i2,j2) by Th11;

A9: |.(i1 - i2).| + |.(j1 - j2).| = 1 by A3, A4, A5, A6, A7, A8, Th12;

A10: now :: thesis: ( ( |.(i1 - i2).| = 1 & j1 = j2 & ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 ) or ( i1 = i2 & |.(j1 - j2).| = 1 & ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 ) )
end;

per cases
( ( |.(i1 - i2).| = 1 & j1 = j2 ) or ( i1 = i2 & |.(j1 - j2).| = 1 ) )
by A9, SEQM_3:42;

end;

func right_cell (f,k) -> Subset of (TOP-REAL 2) means :Def6: :: GOBOARD5:def 6

for i1, j1, i2, j2 being 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 for i1, j1, i2, j2 being 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) );

ex b

for i1, j1, i2, j2 being 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 & b

( i1 = i2 & j1 = j2 + 1 & b

proof end;

uniqueness for b

( i1 = i2 & j1 = j2 + 1 & b

( i1 = i2 & j1 = j2 + 1 & b

b

proof end;

func left_cell (f,k) -> Subset of (TOP-REAL 2) means :Def7: :: GOBOARD5:def 7

for i1, j1, i2, j2 being 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 for i1, j1, i2, j2 being 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) );

ex b

for i1, j1, i2, j2 being 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 & b

( i1 = i2 & j1 = j2 + 1 & b

proof end;

uniqueness for b

( i1 = i2 & j1 = j2 + 1 & b

( i1 = i2 & j1 = j2 + 1 & b

b

proof end;

:: deftheorem Def6 defines right_cell GOBOARD5:def 6 :

for f being standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

for b_{3} being Subset of (TOP-REAL 2) holds

( b_{3} = right_cell (f,k) iff for i1, j1, i2, j2 being 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 & b_{3} = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{3} = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{3} = cell ((GoB f),i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{3} = cell ((GoB f),(i1 -' 1),j2) ) );

for f being standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

for b

( b

( i1 = i2 & j1 = j2 + 1 & b

:: deftheorem Def7 defines left_cell GOBOARD5:def 7 :

for f being standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

for b_{3} being Subset of (TOP-REAL 2) holds

( b_{3} = left_cell (f,k) iff for i1, j1, i2, j2 being 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 & b_{3} = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{3} = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{3} = cell ((GoB f),i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{3} = cell ((GoB f),i1,j2) ) );

for f being standard special_circular_sequence

for k being Nat st 1 <= k & k + 1 <= len f holds

for b

( b

( i1 = i2 & j1 = j2 + 1 & b

theorem Th13: :: GOBOARD5:13

for i, j being Nat

for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G holds

LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i)

for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G holds

LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i)

proof end;

theorem Th14: :: GOBOARD5:14

for i, j being Nat

for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G holds

LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i)

for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G holds

LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i)

proof end;

theorem Th15: :: GOBOARD5:15

for i, j being Nat

for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j < width G & 1 <= i & i < len G holds

LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j)

for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j < width G & 1 <= i & i < len G holds

LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j)

proof end;

theorem Th16: :: GOBOARD5:16

for i, j being Nat

for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G holds

LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j)

for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G holds

LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j)

proof end;

theorem Th17: :: GOBOARD5:17

for i, j being Nat

for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G holds

LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j)

for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G holds

LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j)

proof end;

theorem Th18: :: GOBOARD5:18

for i, j being Nat

for G being Go-board st i < len G & 1 <= j & j < width G holds

LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)

for G being Go-board st i < len G & 1 <= j & j < width G holds

LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)

proof end;

theorem Th19: :: GOBOARD5:19

for i, j being Nat

for G being Go-board st 1 <= i & i <= len G & 1 <= j & j < width G holds

LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j)

for G being Go-board st 1 <= i & i <= len G & 1 <= j & j < width G holds

LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j)

proof end;

theorem Th20: :: GOBOARD5:20

for i, j being Nat

for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i & i + 1 <= len G holds

LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i)

for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i & i + 1 <= len G holds

LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i)

proof end;

theorem Th21: :: GOBOARD5:21

for i, j being Nat

for G being Go-board st j < width G & 1 <= i & i < len G holds

LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)

for G being Go-board st j < width G & 1 <= i & i < len G holds

LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)

proof end;

theorem Th22: :: GOBOARD5:22

for i, j being Nat

for G being Go-board st 1 <= i & i < len G & 1 <= j & j <= width G holds

LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j)

for G being Go-board st 1 <= i & i < len G & 1 <= j & j <= width G holds

LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j)

proof end;

theorem Th23: :: GOBOARD5:23

for i being Nat

for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G holds

(v_strip (G,i)) /\ (v_strip (G,(i + 1))) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }

for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G holds

(v_strip (G,i)) /\ (v_strip (G,(i + 1))) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }

proof end;

theorem Th24: :: GOBOARD5:24

for j being Nat

for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G holds

(h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }

for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G holds

(h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }

proof end;

theorem Th25: :: GOBOARD5:25

for i, j being Nat

for G being Go-board st i < len G & 1 <= j & j < width G holds

(cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))

for G being Go-board st i < len G & 1 <= j & j < width G holds

(cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))

proof end;

theorem Th26: :: GOBOARD5:26

for i, j being Nat

for G being Go-board st j < width G & 1 <= i & i < len G holds

(cell (G,i,j)) /\ (cell (G,i,(j + 1))) = LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))

for G being Go-board st j < width G & 1 <= i & i < len G holds

(cell (G,i,j)) /\ (cell (G,i,(j + 1))) = LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))

proof end;

theorem Th27: :: GOBOARD5:27

for i, j, k being 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) )

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) )

proof end;

theorem Th28: :: GOBOARD5:28

for i, j, k being 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) )

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) )

proof end;

theorem Th29: :: GOBOARD5:29

for i, j, k being 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)) )

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)) )

proof end;

theorem Th30: :: GOBOARD5:30

for i, j, k being 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) )

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) )

proof end;

theorem :: GOBOARD5:31

for k being Nat

for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds

(left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)

for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds

(left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)

proof end;