:: GOBOARD5 semantic presentation

theorem Th1: :: GOBOARD5:1
for b1 being tabular FinSequence
for b2, b3 being Nat st [b2,b3] in Indices b1 holds
( 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= width b1 )
proof end;

definition
let c1 be Matrix of (TOP-REAL 2);
let c2 be Nat;
func v_strip c1,c2 -> Subset of (TOP-REAL 2) equals :Def1: :: GOBOARD5:def 1
{ |[b1,b2]| where B is Real, B is Real : ( (a1 * a2,1) `1 <= b1 & b1 <= (a1 * (a2 + 1),1) `1 ) } if ( 1 <= a2 & a2 < len a1 )
{ |[b1,b2]| where B is Real, B is Real : (a1 * a2,1) `1 <= b1 } if a2 >= len a1
otherwise { |[b1,b2]| where B is Real, B is Real : b1 <= (a1 * (a2 + 1),1) `1 } ;
coherence
( ( 1 <= c2 & c2 < len c1 implies { |[b1,b2]| where B is Real, B is Real : ( (c1 * c2,1) `1 <= b1 & b1 <= (c1 * (c2 + 1),1) `1 ) } is Subset of (TOP-REAL 2) ) & ( c2 >= len c1 implies { |[b1,b2]| where B is Real, B is Real : (c1 * c2,1) `1 <= b1 } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= c2 or not c2 < len c1 ) & not c2 >= len c1 implies { |[b1,b2]| where B is Real, B is Real : b1 <= (c1 * (c2 + 1),1) `1 } is Subset of (TOP-REAL 2) ) )
proof end;
correctness
consistency
for b1 being Subset of (TOP-REAL 2) st 1 <= c2 & c2 < len c1 & c2 >= len c1 holds
( b1 = { |[b2,b3]| where B is Real, B is Real : ( (c1 * c2,1) `1 <= b2 & b2 <= (c1 * (c2 + 1),1) `1 ) } iff b1 = { |[b2,b3]| where B is Real, B is Real : (c1 * c2,1) `1 <= b2 } );
;
func h_strip c1,c2 -> Subset of (TOP-REAL 2) equals :Def2: :: GOBOARD5:def 2
{ |[b1,b2]| where B is Real, B is Real : ( (a1 * 1,a2) `2 <= b2 & b2 <= (a1 * 1,(a2 + 1)) `2 ) } if ( 1 <= a2 & a2 < width a1 )
{ |[b1,b2]| where B is Real, B is Real : (a1 * 1,a2) `2 <= b2 } if a2 >= width a1
otherwise { |[b1,b2]| where B is Real, B is Real : b2 <= (a1 * 1,(a2 + 1)) `2 } ;
coherence
( ( 1 <= c2 & c2 < width c1 implies { |[b1,b2]| where B is Real, B is Real : ( (c1 * 1,c2) `2 <= b2 & b2 <= (c1 * 1,(c2 + 1)) `2 ) } is Subset of (TOP-REAL 2) ) & ( c2 >= width c1 implies { |[b1,b2]| where B is Real, B is Real : (c1 * 1,c2) `2 <= b2 } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= c2 or not c2 < width c1 ) & not c2 >= width c1 implies { |[b1,b2]| where B is Real, B is Real : b2 <= (c1 * 1,(c2 + 1)) `2 } is Subset of (TOP-REAL 2) ) )
proof end;
correctness
consistency
for b1 being Subset of (TOP-REAL 2) st 1 <= c2 & c2 < width c1 & c2 >= width c1 holds
( b1 = { |[b2,b3]| where B is Real, B is Real : ( (c1 * 1,c2) `2 <= b3 & b3 <= (c1 * 1,(c2 + 1)) `2 ) } iff b1 = { |[b2,b3]| where B is Real, B is Real : (c1 * 1,c2) `2 <= b3 } );
;
end;

:: deftheorem Def1 defines v_strip GOBOARD5:def 1 :
for b1 being Matrix of (TOP-REAL 2)
for b2 being Nat holds
( ( 1 <= b2 & b2 < len b1 implies v_strip b1,b2 = { |[b3,b4]| where B is Real, B is Real : ( (b1 * b2,1) `1 <= b3 & b3 <= (b1 * (b2 + 1),1) `1 ) } ) & ( b2 >= len b1 implies v_strip b1,b2 = { |[b3,b4]| where B is Real, B is Real : (b1 * b2,1) `1 <= b3 } ) & ( ( not 1 <= b2 or not b2 < len b1 ) & not b2 >= len b1 implies v_strip b1,b2 = { |[b3,b4]| where B is Real, B is Real : b3 <= (b1 * (b2 + 1),1) `1 } ) );

:: deftheorem Def2 defines h_strip GOBOARD5:def 2 :
for b1 being Matrix of (TOP-REAL 2)
for b2 being Nat holds
( ( 1 <= b2 & b2 < width b1 implies h_strip b1,b2 = { |[b3,b4]| where B is Real, B is Real : ( (b1 * 1,b2) `2 <= b4 & b4 <= (b1 * 1,(b2 + 1)) `2 ) } ) & ( b2 >= width b1 implies h_strip b1,b2 = { |[b3,b4]| where B is Real, B is Real : (b1 * 1,b2) `2 <= b4 } ) & ( ( not 1 <= b2 or not b2 < width b1 ) & not b2 >= width b1 implies h_strip b1,b2 = { |[b3,b4]| where B is Real, B is Real : b4 <= (b1 * 1,(b2 + 1)) `2 } ) );

theorem Th2: :: GOBOARD5:2
for b1, b2 being Nat
for b3 being Matrix of (TOP-REAL 2) st b3 is Y_equal-in-column & 1 <= b1 & b1 <= width b3 & 1 <= b2 & b2 <= len b3 holds
(b3 * b2,b1) `2 = (b3 * 1,b1) `2
proof end;

theorem Th3: :: GOBOARD5:3
for b1, b2 being Nat
for b3 being Matrix of (TOP-REAL 2) st b3 is X_equal-in-line & 1 <= b1 & b1 <= width b3 & 1 <= b2 & b2 <= len b3 holds
(b3 * b2,b1) `1 = (b3 * b2,1) `1
proof end;

theorem Th4: :: GOBOARD5:4
for b1, b2, b3 being Nat
for b4 being Matrix of (TOP-REAL 2) st b4 is X_increasing-in-column & 1 <= b1 & b1 <= width b4 & 1 <= b2 & b2 < b3 & b3 <= len b4 holds
(b4 * b2,b1) `1 < (b4 * b3,b1) `1
proof end;

theorem Th5: :: GOBOARD5:5
for b1, b2, b3 being Nat
for b4 being Matrix of (TOP-REAL 2) st b4 is Y_increasing-in-line & 1 <= b1 & b1 < b2 & b2 <= width b4 & 1 <= b3 & b3 <= len b4 holds
(b4 * b3,b1) `2 < (b4 * b3,b2) `2
proof end;

theorem Th6: :: GOBOARD5:6
for b1, b2 being Nat
for b3 being Matrix of (TOP-REAL 2) st b3 is Y_equal-in-column & 1 <= b1 & b1 < width b3 & 1 <= b2 & b2 <= len b3 holds
h_strip b3,b1 = { |[b4,b5]| where B is Real, B is Real : ( (b3 * b2,b1) `2 <= b5 & b5 <= (b3 * b2,(b1 + 1)) `2 ) }
proof end;

theorem Th7: :: GOBOARD5:7
for b1 being Nat
for b2 being Matrix of (TOP-REAL 2) st not b2 is empty-yielding & b2 is Y_equal-in-column & 1 <= b1 & b1 <= len b2 holds
h_strip b2,(width b2) = { |[b3,b4]| where B is Real, B is Real : (b2 * b1,(width b2)) `2 <= b4 }
proof end;

theorem Th8: :: GOBOARD5:8
for b1 being Nat
for b2 being Matrix of (TOP-REAL 2) st not b2 is empty-yielding & b2 is Y_equal-in-column & 1 <= b1 & b1 <= len b2 holds
h_strip b2,0 = { |[b3,b4]| where B is Real, B is Real : b4 <= (b2 * b1,1) `2 }
proof end;

theorem Th9: :: GOBOARD5:9
for b1, b2 being Nat
for b3 being Matrix of (TOP-REAL 2) st b3 is X_equal-in-line & 1 <= b1 & b1 < len b3 & 1 <= b2 & b2 <= width b3 holds
v_strip b3,b1 = { |[b4,b5]| where B is Real, B is Real : ( (b3 * b1,b2) `1 <= b4 & b4 <= (b3 * (b1 + 1),b2) `1 ) }
proof end;

theorem Th10: :: GOBOARD5:10
for b1 being Nat
for b2 being Matrix of (TOP-REAL 2) st not b2 is empty-yielding & b2 is X_equal-in-line & 1 <= b1 & b1 <= width b2 holds
v_strip b2,(len b2) = { |[b3,b4]| where B is Real, B is Real : (b2 * (len b2),b1) `1 <= b3 }
proof end;

theorem Th11: :: GOBOARD5:11
for b1 being Nat
for b2 being Matrix of (TOP-REAL 2) st not b2 is empty-yielding & b2 is X_equal-in-line & 1 <= b1 & b1 <= width b2 holds
v_strip b2,0 = { |[b3,b4]| where B is Real, B is Real : b3 <= (b2 * 1,b1) `1 }
proof end;

definition
let c1 be Matrix of (TOP-REAL 2);
let c2, c3 be Nat;
func cell c1,c2,c3 -> Subset of (TOP-REAL 2) equals :: GOBOARD5:def 3
(v_strip a1,a2) /\ (h_strip a1,a3);
correctness
coherence
(v_strip c1,c2) /\ (h_strip c1,c3) is Subset of (TOP-REAL 2);
;
end;

:: deftheorem Def3 defines cell GOBOARD5:def 3 :
for b1 being Matrix of (TOP-REAL 2)
for b2, b3 being Nat holds cell b1,b2,b3 = (v_strip b1,b2) /\ (h_strip b1,b3);

definition
let c1 be FinSequence of (TOP-REAL 2);
attr a1 is s.c.c. means :: GOBOARD5:def 4
for b1, b2 being Nat st b1 + 1 < b2 & ( ( b1 > 1 & b2 < len a1 ) or b2 + 1 < len a1 ) holds
LSeg a1,b1 misses LSeg a1,b2;
end;

:: deftheorem Def4 defines s.c.c. GOBOARD5:def 4 :
for b1 being FinSequence of (TOP-REAL 2) holds
( b1 is s.c.c. iff for b2, b3 being Nat st b2 + 1 < b3 & ( ( b2 > 1 & b3 < len b1 ) or b3 + 1 < len b1 ) holds
LSeg b1,b2 misses LSeg b1,b3 );

definition
let c1 be non empty FinSequence of (TOP-REAL 2);
attr a1 is standard means :Def5: :: GOBOARD5:def 5
a1 is_sequence_on GoB a1;
end;

:: deftheorem Def5 defines standard GOBOARD5:def 5 :
for b1 being non empty FinSequence of (TOP-REAL 2) holds
( b1 is standard iff b1 is_sequence_on GoB b1 );

registration
cluster non empty non constant special unfolded circular s.c.c. standard FinSequence of the carrier of (TOP-REAL 2);
existence
ex b1 being non empty FinSequence of (TOP-REAL 2) st
( not b1 is constant & b1 is special & b1 is unfolded & b1 is circular & b1 is s.c.c. & b1 is standard )
proof end;
end;

Lemma15: for b1 being FinSequence of (TOP-REAL 2) holds dom (X_axis b1) = dom b1
proof end;

Lemma16: for b1 being FinSequence of (TOP-REAL 2) holds dom (Y_axis b1) = dom b1
proof end;

theorem Th12: :: GOBOARD5:12
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Nat st b2 in dom b1 holds
ex b3, b4 being Nat st
( [b3,b4] in Indices (GoB b1) & b1 /. b2 = (GoB b1) * b3,b4 )
proof end;

theorem Th13: :: GOBOARD5:13
for b1 being non empty standard FinSequence of (TOP-REAL 2)
for b2 being Nat st b2 in dom b1 & b2 + 1 in dom b1 holds
for b3, b4, b5, b6 being Nat st [b3,b4] in Indices (GoB b1) & [b5,b6] in Indices (GoB b1) & b1 /. b2 = (GoB b1) * b3,b4 & b1 /. (b2 + 1) = (GoB b1) * b5,b6 holds
(abs (b3 - b5)) + (abs (b4 - b6)) = 1
proof end;

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

definition
let c1 be standard special_circular_sequence;
let c2 be Nat;
assume E19: ( 1 <= c2 & c2 + 1 <= len c1 ) ;
c2 <= c2 + 1 by NAT_1:29;
then c2 <= len c1 by E19, XREAL_1:2;
then E20: c2 in dom c1 by E19, FINSEQ_3:27;
then consider c3, c4 being Nat such that
E21: ( [c3,c4] in Indices (GoB c1) & c1 /. c2 = (GoB c1) * c3,c4 ) by Th12;
c2 + 1 >= 1 by NAT_1:29;
then E22: c2 + 1 in dom c1 by E19, FINSEQ_3:27;
then consider c5, c6 being Nat such that
E23: ( [c5,c6] in Indices (GoB c1) & c1 /. (c2 + 1) = (GoB c1) * c5,c6 ) by Th12;
E24: (abs (c3 - c5)) + (abs (c4 - c6)) = 1 by E20, E21, E22, E23, Th13;
E25: now
per cases ( ( abs (c3 - c5) = 1 & c4 = c6 ) or ( c3 = c5 & abs (c4 - c6) = 1 ) ) by E24, GOBOARD1:2;
case that E26: abs (c3 - c5) = 1 and
E27: c4 = c6 ;
( c3 - c5 >= 0 or c3 - c5 < 0 ) ;
then ( c3 - c5 = 1 or - (c3 - c5) = 1 ) by E26, ABSVALUE:def 1;
hence ( c3 = c5 + 1 or c3 + 1 = c5 ) ;
thus c4 = c6 by E27;
end;
case that E26: c3 = c5 and
E27: abs (c4 - c6) = 1 ;
( c4 - c6 >= 0 or c4 - c6 < 0 ) ;
then ( c4 - c6 = 1 or - (c4 - c6) = 1 ) by E27, ABSVALUE:def 1;
hence ( c4 = c6 + 1 or c4 + 1 = c6 ) ;
thus c3 = c5 by E26;
end;
end;
end;
func right_cell c1,c2 -> Subset of (TOP-REAL 2) means :Def6: :: GOBOARD5:def 6
for b1, b2, b3, b4 being Nat st [b1,b2] in Indices (GoB a1) & [b3,b4] in Indices (GoB a1) & a1 /. a2 = (GoB a1) * b1,b2 & a1 /. (a2 + 1) = (GoB a1) * b3,b4 & not ( b1 = b3 & b2 + 1 = b4 & a3 = cell (GoB a1),b1,b2 ) & not ( b1 + 1 = b3 & b2 = b4 & a3 = cell (GoB a1),b1,(b2 -' 1) ) & not ( b1 = b3 + 1 & b2 = b4 & a3 = cell (GoB a1),b3,b4 ) holds
( b1 = b3 & b2 = b4 + 1 & a3 = cell (GoB a1),(b1 -' 1),b4 );
existence
ex b1 being Subset of (TOP-REAL 2) st
for b2, b3, b4, b5 being Nat st [b2,b3] in Indices (GoB c1) & [b4,b5] in Indices (GoB c1) & c1 /. c2 = (GoB c1) * b2,b3 & c1 /. (c2 + 1) = (GoB c1) * b4,b5 & not ( b2 = b4 & b3 + 1 = b5 & b1 = cell (GoB c1),b2,b3 ) & not ( b2 + 1 = b4 & b3 = b5 & b1 = cell (GoB c1),b2,(b3 -' 1) ) & not ( b2 = b4 + 1 & b3 = b5 & b1 = cell (GoB c1),b4,b5 ) holds
( b2 = b4 & b3 = b5 + 1 & b1 = cell (GoB c1),(b2 -' 1),b5 )
proof end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for b3, b4, b5, b6 being Nat st [b3,b4] in Indices (GoB c1) & [b5,b6] in Indices (GoB c1) & c1 /. c2 = (GoB c1) * b3,b4 & c1 /. (c2 + 1) = (GoB c1) * b5,b6 & not ( b3 = b5 & b4 + 1 = b6 & b1 = cell (GoB c1),b3,b4 ) & not ( b3 + 1 = b5 & b4 = b6 & b1 = cell (GoB c1),b3,(b4 -' 1) ) & not ( b3 = b5 + 1 & b4 = b6 & b1 = cell (GoB c1),b5,b6 ) holds
( b3 = b5 & b4 = b6 + 1 & b1 = cell (GoB c1),(b3 -' 1),b6 ) ) & ( for b3, b4, b5, b6 being Nat st [b3,b4] in Indices (GoB c1) & [b5,b6] in Indices (GoB c1) & c1 /. c2 = (GoB c1) * b3,b4 & c1 /. (c2 + 1) = (GoB c1) * b5,b6 & not ( b3 = b5 & b4 + 1 = b6 & b2 = cell (GoB c1),b3,b4 ) & not ( b3 + 1 = b5 & b4 = b6 & b2 = cell (GoB c1),b3,(b4 -' 1) ) & not ( b3 = b5 + 1 & b4 = b6 & b2 = cell (GoB c1),b5,b6 ) holds
( b3 = b5 & b4 = b6 + 1 & b2 = cell (GoB c1),(b3 -' 1),b6 ) ) holds
b1 = b2
proof end;
func left_cell c1,c2 -> Subset of (TOP-REAL 2) means :Def7: :: GOBOARD5:def 7
for b1, b2, b3, b4 being Nat st [b1,b2] in Indices (GoB a1) & [b3,b4] in Indices (GoB a1) & a1 /. a2 = (GoB a1) * b1,b2 & a1 /. (a2 + 1) = (GoB a1) * b3,b4 & not ( b1 = b3 & b2 + 1 = b4 & a3 = cell (GoB a1),(b1 -' 1),b2 ) & not ( b1 + 1 = b3 & b2 = b4 & a3 = cell (GoB a1),b1,b2 ) & not ( b1 = b3 + 1 & b2 = b4 & a3 = cell (GoB a1),b3,(b4 -' 1) ) holds
( b1 = b3 & b2 = b4 + 1 & a3 = cell (GoB a1),b1,b4 );
existence
ex b1 being Subset of (TOP-REAL 2) st
for b2, b3, b4, b5 being Nat st [b2,b3] in Indices (GoB c1) & [b4,b5] in Indices (GoB c1) & c1 /. c2 = (GoB c1) * b2,b3 & c1 /. (c2 + 1) = (GoB c1) * b4,b5 & not ( b2 = b4 & b3 + 1 = b5 & b1 = cell (GoB c1),(b2 -' 1),b3 ) & not ( b2 + 1 = b4 & b3 = b5 & b1 = cell (GoB c1),b2,b3 ) & not ( b2 = b4 + 1 & b3 = b5 & b1 = cell (GoB c1),b4,(b5 -' 1) ) holds
( b2 = b4 & b3 = b5 + 1 & b1 = cell (GoB c1),b2,b5 )
proof end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for b3, b4, b5, b6 being Nat st [b3,b4] in Indices (GoB c1) & [b5,b6] in Indices (GoB c1) & c1 /. c2 = (GoB c1) * b3,b4 & c1 /. (c2 + 1) = (GoB c1) * b5,b6 & not ( b3 = b5 & b4 + 1 = b6 & b1 = cell (GoB c1),(b3 -' 1),b4 ) & not ( b3 + 1 = b5 & b4 = b6 & b1 = cell (GoB c1),b3,b4 ) & not ( b3 = b5 + 1 & b4 = b6 & b1 = cell (GoB c1),b5,(b6 -' 1) ) holds
( b3 = b5 & b4 = b6 + 1 & b1 = cell (GoB c1),b3,b6 ) ) & ( for b3, b4, b5, b6 being Nat st [b3,b4] in Indices (GoB c1) & [b5,b6] in Indices (GoB c1) & c1 /. c2 = (GoB c1) * b3,b4 & c1 /. (c2 + 1) = (GoB c1) * b5,b6 & not ( b3 = b5 & b4 + 1 = b6 & b2 = cell (GoB c1),(b3 -' 1),b4 ) & not ( b3 + 1 = b5 & b4 = b6 & b2 = cell (GoB c1),b3,b4 ) & not ( b3 = b5 + 1 & b4 = b6 & b2 = cell (GoB c1),b5,(b6 -' 1) ) holds
( b3 = b5 & b4 = b6 + 1 & b2 = cell (GoB c1),b3,b6 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines right_cell GOBOARD5:def 6 :
for b1 being standard special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 1 <= len b1 holds
for b3 being Subset of (TOP-REAL 2) holds
( b3 = right_cell b1,b2 iff for b4, b5, b6, b7 being Nat st [b4,b5] in Indices (GoB b1) & [b6,b7] in Indices (GoB b1) & b1 /. b2 = (GoB b1) * b4,b5 & b1 /. (b2 + 1) = (GoB b1) * b6,b7 & not ( b4 = b6 & b5 + 1 = b7 & b3 = cell (GoB b1),b4,b5 ) & not ( b4 + 1 = b6 & b5 = b7 & b3 = cell (GoB b1),b4,(b5 -' 1) ) & not ( b4 = b6 + 1 & b5 = b7 & b3 = cell (GoB b1),b6,b7 ) holds
( b4 = b6 & b5 = b7 + 1 & b3 = cell (GoB b1),(b4 -' 1),b7 ) );

:: deftheorem Def7 defines left_cell GOBOARD5:def 7 :
for b1 being standard special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 1 <= len b1 holds
for b3 being Subset of (TOP-REAL 2) holds
( b3 = left_cell b1,b2 iff for b4, b5, b6, b7 being Nat st [b4,b5] in Indices (GoB b1) & [b6,b7] in Indices (GoB b1) & b1 /. b2 = (GoB b1) * b4,b5 & b1 /. (b2 + 1) = (GoB b1) * b6,b7 & not ( b4 = b6 & b5 + 1 = b7 & b3 = cell (GoB b1),(b4 -' 1),b5 ) & not ( b4 + 1 = b6 & b5 = b7 & b3 = cell (GoB b1),b4,b5 ) & not ( b4 = b6 + 1 & b5 = b7 & b3 = cell (GoB b1),b6,(b7 -' 1) ) holds
( b4 = b6 & b5 = b7 + 1 & b3 = cell (GoB b1),b4,b7 ) );

theorem Th14: :: GOBOARD5:14
for b1, b2 being Nat
for b3 being Matrix of (TOP-REAL 2) st not b3 is empty-yielding & b3 is X_equal-in-line & b3 is X_increasing-in-column & b1 < len b3 & 1 <= b2 & b2 < width b3 holds
LSeg (b3 * (b1 + 1),b2),(b3 * (b1 + 1),(b2 + 1)) c= v_strip b3,b1
proof end;

theorem Th15: :: GOBOARD5:15
for b1, b2 being Nat
for b3 being Matrix of (TOP-REAL 2) st not b3 is empty-yielding & b3 is X_equal-in-line & b3 is X_increasing-in-column & 1 <= b1 & b1 <= len b3 & 1 <= b2 & b2 < width b3 holds
LSeg (b3 * b1,b2),(b3 * b1,(b2 + 1)) c= v_strip b3,b1
proof end;

theorem Th16: :: GOBOARD5:16
for b1, b2 being Nat
for b3 being Matrix of (TOP-REAL 2) st not b3 is empty-yielding & b3 is Y_equal-in-column & b3 is Y_increasing-in-line & b1 < width b3 & 1 <= b2 & b2 < len b3 holds
LSeg (b3 * b2,(b1 + 1)),(b3 * (b2 + 1),(b1 + 1)) c= h_strip b3,b1
proof end;

theorem Th17: :: GOBOARD5:17
for b1, b2 being Nat
for b3 being Matrix of (TOP-REAL 2) st not b3 is empty-yielding & b3 is Y_equal-in-column & b3 is Y_increasing-in-line & 1 <= b1 & b1 <= width b3 & 1 <= b2 & b2 < len b3 holds
LSeg (b3 * b2,b1),(b3 * (b2 + 1),b1) c= h_strip b3,b1
proof end;

theorem Th18: :: GOBOARD5:18
for b1, b2 being Nat
for b3 being Matrix of (TOP-REAL 2) st b3 is Y_equal-in-column & b3 is Y_increasing-in-line & 1 <= b1 & b1 <= len b3 & 1 <= b2 & b2 + 1 <= width b3 holds
LSeg (b3 * b1,b2),(b3 * b1,(b2 + 1)) c= h_strip b3,b2
proof end;

theorem Th19: :: GOBOARD5:19
for b1, b2 being Nat
for b3 being Go-board st b1 < len b3 & 1 <= b2 & b2 < width b3 holds
LSeg (b3 * (b1 + 1),b2),(b3 * (b1 + 1),(b2 + 1)) c= cell b3,b1,b2
proof end;

theorem Th20: :: GOBOARD5:20
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 <= len b3 & 1 <= b2 & b2 < width b3 holds
LSeg (b3 * b1,b2),(b3 * b1,(b2 + 1)) c= cell b3,b1,b2
proof end;

theorem Th21: :: GOBOARD5:21
for b1, b2 being Nat
for b3 being Matrix of (TOP-REAL 2) st b3 is X_equal-in-line & b3 is X_increasing-in-column & 1 <= b1 & b1 <= width b3 & 1 <= b2 & b2 + 1 <= len b3 holds
LSeg (b3 * b2,b1),(b3 * (b2 + 1),b1) c= v_strip b3,b2
proof end;

theorem Th22: :: GOBOARD5:22
for b1, b2 being Nat
for b3 being Go-board st b1 < width b3 & 1 <= b2 & b2 < len b3 holds
LSeg (b3 * b2,(b1 + 1)),(b3 * (b2 + 1),(b1 + 1)) c= cell b3,b2,b1
proof end;

theorem Th23: :: GOBOARD5:23
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 < len b3 & 1 <= b2 & b2 <= width b3 holds
LSeg (b3 * b1,b2),(b3 * (b1 + 1),b2) c= cell b3,b1,b2
proof end;

theorem Th24: :: GOBOARD5:24
for b1 being Nat
for b2 being Matrix of (TOP-REAL 2) st not b2 is empty-yielding & b2 is X_equal-in-line & b2 is X_increasing-in-column & b1 + 1 <= len b2 holds
(v_strip b2,b1) /\ (v_strip b2,(b1 + 1)) = { b3 where B is Point of (TOP-REAL 2) : b3 `1 = (b2 * (b1 + 1),1) `1 }
proof end;

theorem Th25: :: GOBOARD5:25
for b1 being Nat
for b2 being Matrix of (TOP-REAL 2) st not b2 is empty-yielding & b2 is Y_equal-in-column & b2 is Y_increasing-in-line & b1 + 1 <= width b2 holds
(h_strip b2,b1) /\ (h_strip b2,(b1 + 1)) = { b3 where B is Point of (TOP-REAL 2) : b3 `2 = (b2 * 1,(b1 + 1)) `2 }
proof end;

theorem Th26: :: GOBOARD5:26
for b1, b2 being Nat
for b3 being Go-board st b1 < len b3 & 1 <= b2 & b2 < width b3 holds
(cell b3,b1,b2) /\ (cell b3,(b1 + 1),b2) = LSeg (b3 * (b1 + 1),b2),(b3 * (b1 + 1),(b2 + 1))
proof end;

theorem Th27: :: GOBOARD5:27
for b1, b2 being Nat
for b3 being Go-board st b1 < width b3 & 1 <= b2 & b2 < len b3 holds
(cell b3,b2,b1) /\ (cell b3,b2,(b1 + 1)) = LSeg (b3 * b2,(b1 + 1)),(b3 * (b2 + 1),(b1 + 1))
proof end;

theorem Th28: :: GOBOARD5:28
for b1, b2, b3 being Nat
for b4 being standard special_circular_sequence st 1 <= b1 & b1 + 1 <= len b4 & [(b2 + 1),b3] in Indices (GoB b4) & [(b2 + 1),(b3 + 1)] in Indices (GoB b4) & b4 /. b1 = (GoB b4) * (b2 + 1),b3 & b4 /. (b1 + 1) = (GoB b4) * (b2 + 1),(b3 + 1) holds
( left_cell b4,b1 = cell (GoB b4),b2,b3 & right_cell b4,b1 = cell (GoB b4),(b2 + 1),b3 )
proof end;

theorem Th29: :: GOBOARD5:29
for b1, b2, b3 being Nat
for b4 being standard special_circular_sequence st 1 <= b1 & b1 + 1 <= len b4 & [b2,(b3 + 1)] in Indices (GoB b4) & [(b2 + 1),(b3 + 1)] in Indices (GoB b4) & b4 /. b1 = (GoB b4) * b2,(b3 + 1) & b4 /. (b1 + 1) = (GoB b4) * (b2 + 1),(b3 + 1) holds
( left_cell b4,b1 = cell (GoB b4),b2,(b3 + 1) & right_cell b4,b1 = cell (GoB b4),b2,b3 )
proof end;

theorem Th30: :: GOBOARD5:30
for b1, b2, b3 being Nat
for b4 being standard special_circular_sequence st 1 <= b1 & b1 + 1 <= len b4 & [b2,(b3 + 1)] in Indices (GoB b4) & [(b2 + 1),(b3 + 1)] in Indices (GoB b4) & b4 /. b1 = (GoB b4) * (b2 + 1),(b3 + 1) & b4 /. (b1 + 1) = (GoB b4) * b2,(b3 + 1) holds
( left_cell b4,b1 = cell (GoB b4),b2,b3 & right_cell b4,b1 = cell (GoB b4),b2,(b3 + 1) )
proof end;

theorem Th31: :: GOBOARD5:31
for b1, b2, b3 being Nat
for b4 being standard special_circular_sequence st 1 <= b1 & b1 + 1 <= len b4 & [(b2 + 1),(b3 + 1)] in Indices (GoB b4) & [(b2 + 1),b3] in Indices (GoB b4) & b4 /. b1 = (GoB b4) * (b2 + 1),(b3 + 1) & b4 /. (b1 + 1) = (GoB b4) * (b2 + 1),b3 holds
( left_cell b4,b1 = cell (GoB b4),(b2 + 1),b3 & right_cell b4,b1 = cell (GoB b4),b2,b3 )
proof end;

theorem Th32: :: GOBOARD5:32
for b1 being Nat
for b2 being standard special_circular_sequence st 1 <= b1 & b1 + 1 <= len b2 holds
(left_cell b2,b1) /\ (right_cell b2,b1) = LSeg b2,b1
proof end;