:: GOBOARD1 semantic presentation

theorem Th1: :: GOBOARD1:1
for b1, b2 being Real holds
( abs (b1 - b2) = 1 iff ( ( b1 > b2 & b1 = b2 + 1 ) or ( b1 < b2 & b2 = b1 + 1 ) ) )
proof end;

theorem Th2: :: GOBOARD1:2
for b1, b2, b3, b4 being Nat holds
( (abs (b1 - b2)) + (abs (b3 - b4)) = 1 iff ( ( abs (b1 - b2) = 1 & b3 = b4 ) or ( abs (b3 - b4) = 1 & b1 = b2 ) ) )
proof end;

theorem Th3: :: GOBOARD1:3
for b1 being Nat holds
( b1 > 1 iff ex b2 being Nat st
( b1 = b2 + 1 & b2 > 0 ) )
proof end;

scheme :: GOBOARD1:sch 1
s1{ F1() -> non empty set , F2() -> Nat, P1[ set , set ] } :
ex b1 being FinSequence of F1() st
( len b1 = F2() & ( for b2 being Nat st b2 in Seg F2() holds
P1[b2,b1 /. b2] ) )
provided
E4: for b1 being Nat st b1 in Seg F2() holds
ex b2 being Element of F1() st P1[b1,b2]
proof end;

theorem Th4: :: GOBOARD1:4
canceled;

theorem Th5: :: GOBOARD1:5
canceled;

theorem Th6: :: GOBOARD1:6
canceled;

theorem Th7: :: GOBOARD1:7
for b1 being FinSequence
for b2, b3, b4 being Nat st len b1 = b3 + 1 & b2 in dom b1 & b4 in Seg b3 & not (Del b1,b2) . b4 = b1 . b4 holds
(Del b1,b2) . b4 = b1 . (b4 + 1)
proof end;

theorem Th8: :: GOBOARD1:8
canceled;

theorem Th9: :: GOBOARD1:9
canceled;

definition
let c1 be FinSequence of REAL ;
let c2 be Nat;
redefine func . as c1 . c2 -> Real;
coherence
c1 . c2 is Real
proof end;
end;

definition
let c1 be FinSequence of REAL ;
attr a1 is increasing means :Def1: :: GOBOARD1:def 1
for b1, b2 being Nat st b1 in dom a1 & b2 in dom a1 & b1 < b2 holds
a1 . b1 < a1 . b2;
end;

:: deftheorem Def1 defines increasing GOBOARD1:def 1 :
for b1 being FinSequence of REAL holds
( b1 is increasing iff for b2, b3 being Nat st b2 in dom b1 & b3 in dom b1 & b2 < b3 holds
b1 . b2 < b1 . b3 );

definition
let c1 be FinSequence;
redefine attr a1 is constant means :Def2: :: GOBOARD1:def 2
for b1, b2 being Nat st b1 in dom a1 & b2 in dom a1 holds
a1 . b1 = a1 . b2;
compatibility
( c1 is constant iff for b1, b2 being Nat st b1 in dom c1 & b2 in dom c1 holds
c1 . b1 = c1 . b2 )
proof end;
end;

:: deftheorem Def2 defines constant GOBOARD1:def 2 :
for b1 being FinSequence holds
( b1 is constant iff for b2, b3 being Nat st b2 in dom b1 & b3 in dom b1 holds
b1 . b2 = b1 . b3 );

registration
cluster non empty increasing FinSequence of REAL ;
existence
ex b1 being FinSequence of REAL st
( not b1 is empty & b1 is increasing )
proof end;
end;

registration
let c1 be non empty set ;
cluster non empty FinSequence of a1;
existence
not for b1 being FinSequence of c1 holds b1 is empty
proof end;
end;

registration
cluster constant FinSequence of REAL ;
existence
ex b1 being FinSequence of REAL st b1 is constant
proof end;
end;

definition
let c1 be FinSequence of (TOP-REAL 2);
func X_axis c1 -> FinSequence of REAL means :Def3: :: GOBOARD1:def 3
( len a2 = len a1 & ( for b1 being Nat st b1 in dom a2 holds
a2 . b1 = (a1 /. b1) `1 ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len c1 & ( for b2 being Nat st b2 in dom b1 holds
b1 . b2 = (c1 /. b2) `1 ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len c1 & ( for b3 being Nat st b3 in dom b1 holds
b1 . b3 = (c1 /. b3) `1 ) & len b2 = len c1 & ( for b3 being Nat st b3 in dom b2 holds
b2 . b3 = (c1 /. b3) `1 ) holds
b1 = b2
proof end;
func Y_axis c1 -> FinSequence of REAL means :Def4: :: GOBOARD1:def 4
( len a2 = len a1 & ( for b1 being Nat st b1 in dom a2 holds
a2 . b1 = (a1 /. b1) `2 ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len c1 & ( for b2 being Nat st b2 in dom b1 holds
b1 . b2 = (c1 /. b2) `2 ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len c1 & ( for b3 being Nat st b3 in dom b1 holds
b1 . b3 = (c1 /. b3) `2 ) & len b2 = len c1 & ( for b3 being Nat st b3 in dom b2 holds
b2 . b3 = (c1 /. b3) `2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines X_axis GOBOARD1:def 3 :
for b1 being FinSequence of (TOP-REAL 2)
for b2 being FinSequence of REAL holds
( b2 = X_axis b1 iff ( len b2 = len b1 & ( for b3 being Nat st b3 in dom b2 holds
b2 . b3 = (b1 /. b3) `1 ) ) );

:: deftheorem Def4 defines Y_axis GOBOARD1:def 4 :
for b1 being FinSequence of (TOP-REAL 2)
for b2 being FinSequence of REAL holds
( b2 = Y_axis b1 iff ( len b2 = len b1 & ( for b3 being Nat st b3 in dom b2 holds
b2 . b3 = (b1 /. b3) `2 ) ) );

theorem Th10: :: GOBOARD1:10
canceled;

theorem Th11: :: GOBOARD1:11
canceled;

theorem Th12: :: GOBOARD1:12
canceled;

theorem Th13: :: GOBOARD1:13
canceled;

theorem Th14: :: GOBOARD1:14
for b1 being FinSequence of REAL
for b2, b3, b4 being Nat st b1 <> {} & rng b1 c= Seg b2 & b1 . (len b1) = b2 & ( for b5 being Nat st 1 <= b5 & b5 <= (len b1) - 1 holds
for b6, b7 being Real st b6 = b1 . b5 & b7 = b1 . (b5 + 1) & not abs (b6 - b7) = 1 holds
b6 = b7 ) & b3 in Seg b2 & b3 + 1 in Seg b2 & b4 in dom b1 & b1 . b4 = b3 & ( for b5 being Nat st b5 in dom b1 & b1 . b5 = b3 holds
b5 <= b4 ) holds
( b4 + 1 in dom b1 & b1 . (b4 + 1) = b3 + 1 )
proof end;

theorem Th15: :: GOBOARD1:15
for b1 being FinSequence of REAL
for b2 being Nat st b1 <> {} & rng b1 c= Seg b2 & b1 . 1 = 1 & b1 . (len b1) = b2 & ( for b3 being Nat st 1 <= b3 & b3 <= (len b1) - 1 holds
for b4, b5 being Real st b4 = b1 . b3 & b5 = b1 . (b3 + 1) & not abs (b4 - b5) = 1 holds
b4 = b5 ) holds
( ( for b3 being Nat st b3 in Seg b2 holds
ex b4 being Nat st
( b4 in dom b1 & b1 . b4 = b3 ) ) & ( for b3, b4, b5 being Nat
for b6 being Real st b3 in dom b1 & b1 . b3 = b5 & ( for b7 being Nat st b7 in dom b1 & b1 . b7 = b5 holds
b7 <= b3 ) & b3 < b4 & b4 in dom b1 & b6 = b1 . b4 holds
b5 < b6 ) )
proof end;

theorem Th16: :: GOBOARD1:16
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Nat st b2 in dom b1 & 2 <= len b1 holds
b1 /. b2 in L~ b1
proof end;

theorem Th17: :: GOBOARD1:17
for b1 being non empty set
for b2 being Matrix of b1
for b3, b4 being Nat st b4 in dom b2 & b3 in Seg (width b2) holds
(Col b2,b3) . b4 = (Line b2,b4) . b3
proof end;

definition
let c1 be non empty set ;
let c2 be Matrix of c1;
redefine attr empty-yielding as a2 is empty-yielding means :Def5: :: GOBOARD1:def 5
( 0 = len a2 or 0 = width a2 );
compatibility
( c2 is empty-yielding iff ( 0 = len c2 or 0 = width c2 ) )
proof end;
end;

:: deftheorem Def5 defines empty-yielding GOBOARD1:def 5 :
for b1 being non empty set
for b2 being Matrix of b1 holds
( b2 is empty-yielding iff ( 0 = len b2 or 0 = width b2 ) );

definition
let c1 be Matrix of (TOP-REAL 2);
attr a1 is X_equal-in-line means :Def6: :: GOBOARD1:def 6
for b1 being Nat st b1 in dom a1 holds
X_axis (Line a1,b1) is constant;
attr a1 is Y_equal-in-column means :Def7: :: GOBOARD1:def 7
for b1 being Nat st b1 in Seg (width a1) holds
Y_axis (Col a1,b1) is constant;
attr a1 is Y_increasing-in-line means :Def8: :: GOBOARD1:def 8
for b1 being Nat st b1 in dom a1 holds
Y_axis (Line a1,b1) is increasing;
attr a1 is X_increasing-in-column means :Def9: :: GOBOARD1:def 9
for b1 being Nat st b1 in Seg (width a1) holds
X_axis (Col a1,b1) is increasing;
end;

:: deftheorem Def6 defines X_equal-in-line GOBOARD1:def 6 :
for b1 being Matrix of (TOP-REAL 2) holds
( b1 is X_equal-in-line iff for b2 being Nat st b2 in dom b1 holds
X_axis (Line b1,b2) is constant );

:: deftheorem Def7 defines Y_equal-in-column GOBOARD1:def 7 :
for b1 being Matrix of (TOP-REAL 2) holds
( b1 is Y_equal-in-column iff for b2 being Nat st b2 in Seg (width b1) holds
Y_axis (Col b1,b2) is constant );

:: deftheorem Def8 defines Y_increasing-in-line GOBOARD1:def 8 :
for b1 being Matrix of (TOP-REAL 2) holds
( b1 is Y_increasing-in-line iff for b2 being Nat st b2 in dom b1 holds
Y_axis (Line b1,b2) is increasing );

:: deftheorem Def9 defines X_increasing-in-column GOBOARD1:def 9 :
for b1 being Matrix of (TOP-REAL 2) holds
( b1 is X_increasing-in-column iff for b2 being Nat st b2 in Seg (width b1) holds
X_axis (Col b1,b2) is increasing );

Lemma17: for b1 being non empty set
for b2 being Matrix of b1 holds
( not b2 is empty-yielding iff ( 0 < len b2 & 0 < width b2 ) )
proof end;

registration
cluster V4 X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) * ;
existence
ex b1 being Matrix of (TOP-REAL 2) st
( not b1 is empty-yielding & b1 is X_equal-in-line & b1 is Y_equal-in-column & b1 is Y_increasing-in-line & b1 is X_increasing-in-column )
proof end;
end;

theorem Th18: :: GOBOARD1:18
canceled;

theorem Th19: :: GOBOARD1:19
for b1 being X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2)
for b2 being set
for b3, b4 being Nat st b2 in rng (Line b1,b3) & b2 in rng (Line b1,b4) & b3 in dom b1 & b4 in dom b1 holds
b3 = b4
proof end;

theorem Th20: :: GOBOARD1:20
for b1 being Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2)
for b2 being set
for b3, b4 being Nat st b2 in rng (Col b1,b3) & b2 in rng (Col b1,b4) & b3 in Seg (width b1) & b4 in Seg (width b1) holds
b3 = b4
proof end;

definition
mode Go-board is V4 X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column Matrix of (TOP-REAL 2);
end;

theorem Th21: :: GOBOARD1:21
for b1, b2, b3, b4 being Nat
for b5 being set
for b6 being Go-board st b5 = b6 * b1,b2 & b5 = b6 * b3,b4 & [b1,b2] in Indices b6 & [b3,b4] in Indices b6 holds
( b1 = b3 & b2 = b4 )
proof end;

theorem Th22: :: GOBOARD1:22
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Nat
for b3 being Go-board st b2 in dom b1 & b1 /. 1 in rng (Col b3,1) holds
(b1 | b2) /. 1 in rng (Col b3,1)
proof end;

theorem Th23: :: GOBOARD1:23
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Nat
for b3 being Go-board st b2 in dom b1 & b1 /. b2 in rng (Col b3,(width b3)) holds
(b1 | b2) /. (len (b1 | b2)) in rng (Col b3,(width b3))
proof end;

theorem Th24: :: GOBOARD1:24
for b1 being FinSequence of (TOP-REAL 2)
for b2, b3, b4, b5 being Nat
for b6 being Go-board st rng b1 misses rng (Col b6,b2) & b1 /. b3 = b6 * b4,b5 & b3 in dom b1 & b4 in dom b6 holds
b2 <> b5
proof end;

definition
let c1 be Go-board;
let c2 be Nat;
assume E21: ( c2 in Seg (width c1) & width c1 > 1 ) ;
func DelCol c1,c2 -> Go-board means :Def10: :: GOBOARD1:def 10
( len a3 = len a1 & ( for b1 being Nat st b1 in dom a1 holds
a3 . b1 = Del (Line a1,b1),a2 ) );
existence
ex b1 being Go-board st
( len b1 = len c1 & ( for b2 being Nat st b2 in dom c1 holds
b1 . b2 = Del (Line c1,b2),c2 ) )
proof end;
uniqueness
for b1, b2 being Go-board st len b1 = len c1 & ( for b3 being Nat st b3 in dom c1 holds
b1 . b3 = Del (Line c1,b3),c2 ) & len b2 = len c1 & ( for b3 being Nat st b3 in dom c1 holds
b2 . b3 = Del (Line c1,b3),c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines DelCol GOBOARD1:def 10 :
for b1 being Go-board
for b2 being Nat st b2 in Seg (width b1) & width b1 > 1 holds
for b3 being Go-board holds
( b3 = DelCol b1,b2 iff ( len b3 = len b1 & ( for b4 being Nat st b4 in dom b1 holds
b3 . b4 = Del (Line b1,b4),b2 ) ) );

theorem Th25: :: GOBOARD1:25
for b1, b2 being Nat
for b3 being Go-board st b1 in Seg (width b3) & width b3 > 1 & b2 in dom b3 holds
Line (DelCol b3,b1),b2 = Del (Line b3,b2),b1
proof end;

theorem Th26: :: GOBOARD1:26
for b1, b2 being Nat
for b3 being Go-board st b1 in Seg (width b3) & width b3 = b2 + 1 & b2 > 0 holds
width (DelCol b3,b1) = b2
proof end;

theorem Th27: :: GOBOARD1:27
for b1 being Nat
for b2 being Go-board st b1 in Seg (width b2) & width b2 > 1 holds
width b2 = (width (DelCol b2,b1)) + 1
proof end;

theorem Th28: :: GOBOARD1:28
for b1, b2, b3 being Nat
for b4 being Go-board st b1 in Seg (width b4) & width b4 > 1 & b2 in dom b4 & b3 in Seg (width (DelCol b4,b1)) holds
(DelCol b4,b1) * b2,b3 = (Del (Line b4,b2),b1) . b3
proof end;

theorem Th29: :: GOBOARD1:29
for b1, b2, b3 being Nat
for b4 being Go-board st b1 in Seg (width b4) & width b4 = b2 + 1 & b2 > 0 & 1 <= b3 & b3 < b1 holds
( Col (DelCol b4,b1),b3 = Col b4,b3 & b3 in Seg (width (DelCol b4,b1)) & b3 in Seg (width b4) )
proof end;

theorem Th30: :: GOBOARD1:30
for b1, b2, b3 being Nat
for b4 being Go-board st b1 in Seg (width b4) & width b4 = b2 + 1 & b2 > 0 & b1 <= b3 & b3 <= b2 holds
( Col (DelCol b4,b1),b3 = Col b4,(b3 + 1) & b3 in Seg (width (DelCol b4,b1)) & b3 + 1 in Seg (width b4) )
proof end;

theorem Th31: :: GOBOARD1:31
for b1, b2, b3, b4 being Nat
for b5 being Go-board st b1 in Seg (width b5) & width b5 = b2 + 1 & b2 > 0 & b3 in dom b5 & 1 <= b4 & b4 < b1 holds
( (DelCol b5,b1) * b3,b4 = b5 * b3,b4 & b4 in Seg (width b5) )
proof end;

theorem Th32: :: GOBOARD1:32
for b1, b2, b3, b4 being Nat
for b5 being Go-board st b1 in Seg (width b5) & width b5 = b2 + 1 & b2 > 0 & b3 in dom b5 & b1 <= b4 & b4 <= b2 holds
( (DelCol b5,b1) * b3,b4 = b5 * b3,(b4 + 1) & b4 + 1 in Seg (width b5) )
proof end;

theorem Th33: :: GOBOARD1:33
for b1, b2 being Nat
for b3 being Go-board st width b3 = b1 + 1 & b1 > 0 & b2 in Seg b1 holds
( Col (DelCol b3,1),b2 = Col b3,(b2 + 1) & b2 in Seg (width (DelCol b3,1)) & b2 + 1 in Seg (width b3) )
proof end;

theorem Th34: :: GOBOARD1:34
for b1, b2, b3 being Nat
for b4 being Go-board st width b4 = b1 + 1 & b1 > 0 & b2 in Seg b1 & b3 in dom b4 holds
( (DelCol b4,1) * b3,b2 = b4 * b3,(b2 + 1) & 1 in Seg (width b4) )
proof end;

theorem Th35: :: GOBOARD1:35
for b1, b2 being Nat
for b3 being Go-board st width b3 = b1 + 1 & b1 > 0 & b2 in Seg b1 holds
( Col (DelCol b3,(width b3)),b2 = Col b3,b2 & b2 in Seg (width (DelCol b3,(width b3))) )
proof end;

theorem Th36: :: GOBOARD1:36
for b1, b2, b3 being Nat
for b4 being Go-board st width b4 = b1 + 1 & b1 > 0 & b2 in Seg b1 & b3 in dom b4 holds
( b2 in Seg (width b4) & (DelCol b4,(width b4)) * b3,b2 = b4 * b3,b2 & width b4 in Seg (width b4) )
proof end;

theorem Th37: :: GOBOARD1:37
for b1 being FinSequence of (TOP-REAL 2)
for b2, b3, b4 being Nat
for b5 being Go-board st rng b1 misses rng (Col b5,b2) & b1 /. b3 in rng (Line b5,b4) & b3 in dom b1 & b2 in Seg (width b5) & b4 in dom b5 & width b5 > 1 holds
b1 /. b3 in rng (Line (DelCol b5,b2),b4)
proof end;

definition
let c1 be set ;
let c2 be FinSequence of c1;
let c3 be Matrix of c1;
pred c2 is_sequence_on c3 means :Def11: :: GOBOARD1:def 11
( ( for b1 being Nat st b1 in dom a2 holds
ex b2, b3 being Nat st
( [b2,b3] in Indices a3 & a2 /. b1 = a3 * b2,b3 ) ) & ( for b1 being Nat st b1 in dom a2 & b1 + 1 in dom a2 holds
for b2, b3, b4, b5 being Nat st [b2,b3] in Indices a3 & [b4,b5] in Indices a3 & a2 /. b1 = a3 * b2,b3 & a2 /. (b1 + 1) = a3 * b4,b5 holds
(abs (b2 - b4)) + (abs (b3 - b5)) = 1 ) );
end;

:: deftheorem Def11 defines is_sequence_on GOBOARD1:def 11 :
for b1 being set
for b2 being FinSequence of b1
for b3 being Matrix of b1 holds
( b2 is_sequence_on b3 iff ( ( for b4 being Nat st b4 in dom b2 holds
ex b5, b6 being Nat st
( [b5,b6] in Indices b3 & b2 /. b4 = b3 * b5,b6 ) ) & ( for b4 being Nat st b4 in dom b2 & b4 + 1 in dom b2 holds
for b5, b6, b7, b8 being Nat st [b5,b6] in Indices b3 & [b7,b8] in Indices b3 & b2 /. b4 = b3 * b5,b6 & b2 /. (b4 + 1) = b3 * b7,b8 holds
(abs (b5 - b7)) + (abs (b6 - b8)) = 1 ) ) );

Lemma31: for b1 being set
for b2 being Matrix of b1 holds <*> b1 is_sequence_on b2
proof end;

theorem Th38: :: GOBOARD1:38
for b1 being Nat
for b2 being set
for b3 being FinSequence of b2
for b4 being Matrix of b2 holds
( ( b1 in dom b3 implies 1 <= len (b3 | b1) ) & ( b3 is_sequence_on b4 implies b3 | b1 is_sequence_on b4 ) )
proof end;

theorem Th39: :: GOBOARD1:39
for b1, b2 being FinSequence of (TOP-REAL 2)
for b3 being set
for b4 being Matrix of b3 st ( for b5 being Nat st b5 in dom b1 holds
ex b6, b7 being Nat st
( [b6,b7] in Indices b4 & b1 /. b5 = b4 * b6,b7 ) ) & ( for b5 being Nat st b5 in dom b2 holds
ex b6, b7 being Nat st
( [b6,b7] in Indices b4 & b2 /. b5 = b4 * b6,b7 ) ) holds
for b5 being Nat st b5 in dom (b1 ^ b2) holds
ex b6, b7 being Nat st
( [b6,b7] in Indices b4 & (b1 ^ b2) /. b5 = b4 * b6,b7 )
proof end;

theorem Th40: :: GOBOARD1:40
for b1, b2 being FinSequence of (TOP-REAL 2)
for b3 being set
for b4 being Matrix of b3 st ( for b5 being Nat st b5 in dom b1 & b5 + 1 in dom b1 holds
for b6, b7, b8, b9 being Nat st [b6,b7] in Indices b4 & [b8,b9] in Indices b4 & b1 /. b5 = b4 * b6,b7 & b1 /. (b5 + 1) = b4 * b8,b9 holds
(abs (b6 - b8)) + (abs (b7 - b9)) = 1 ) & ( for b5 being Nat st b5 in dom b2 & b5 + 1 in dom b2 holds
for b6, b7, b8, b9 being Nat st [b6,b7] in Indices b4 & [b8,b9] in Indices b4 & b2 /. b5 = b4 * b6,b7 & b2 /. (b5 + 1) = b4 * b8,b9 holds
(abs (b6 - b8)) + (abs (b7 - b9)) = 1 ) & ( for b5, b6, b7, b8 being Nat st [b5,b6] in Indices b4 & [b7,b8] in Indices b4 & b1 /. (len b1) = b4 * b5,b6 & b2 /. 1 = b4 * b7,b8 & len b1 in dom b1 & 1 in dom b2 holds
(abs (b5 - b7)) + (abs (b6 - b8)) = 1 ) holds
for b5 being Nat st b5 in dom (b1 ^ b2) & b5 + 1 in dom (b1 ^ b2) holds
for b6, b7, b8, b9 being Nat st [b6,b7] in Indices b4 & [b8,b9] in Indices b4 & (b1 ^ b2) /. b5 = b4 * b6,b7 & (b1 ^ b2) /. (b5 + 1) = b4 * b8,b9 holds
(abs (b6 - b8)) + (abs (b7 - b9)) = 1
proof end;

theorem Th41: :: GOBOARD1:41
for b1 being Nat
for b2 being Go-board
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on b2 & b1 in Seg (width b2) & rng b3 misses rng (Col b2,b1) & width b2 > 1 holds
b3 is_sequence_on DelCol b2,b1
proof end;

theorem Th42: :: GOBOARD1:42
for b1 being Nat
for b2 being Go-board
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on b2 & b1 in dom b3 holds
ex b4 being Nat st
( b4 in dom b2 & b3 /. b1 in rng (Line b2,b4) )
proof end;

theorem Th43: :: GOBOARD1:43
for b1, b2 being Nat
for b3 being Go-board
for b4 being FinSequence of (TOP-REAL 2) st b4 is_sequence_on b3 & b1 in dom b4 & b1 + 1 in dom b4 & b2 in dom b3 & b4 /. b1 in rng (Line b3,b2) & not b4 /. (b1 + 1) in rng (Line b3,b2) holds
for b5 being Nat st b4 /. (b1 + 1) in rng (Line b3,b5) & b5 in dom b3 holds
abs (b2 - b5) = 1
proof end;

theorem Th44: :: GOBOARD1:44
for b1, b2 being Nat
for b3 being Go-board
for b4 being FinSequence of (TOP-REAL 2) st 1 <= len b4 & b4 /. (len b4) in rng (Line b3,(len b3)) & b4 is_sequence_on b3 & b1 in dom b3 & b1 + 1 in dom b3 & b2 in dom b4 & b4 /. b2 in rng (Line b3,b1) & ( for b5 being Nat st b5 in dom b4 & b4 /. b5 in rng (Line b3,b1) holds
b5 <= b2 ) holds
( b2 + 1 in dom b4 & b4 /. (b2 + 1) in rng (Line b3,(b1 + 1)) )
proof end;

theorem Th45: :: GOBOARD1:45
for b1 being Go-board
for b2 being FinSequence of (TOP-REAL 2) st 1 <= len b2 & b2 /. 1 in rng (Line b1,1) & b2 /. (len b2) in rng (Line b1,(len b1)) & b2 is_sequence_on b1 holds
( ( for b3 being Nat st 1 <= b3 & b3 <= len b1 holds
ex b4 being Nat st
( b4 in dom b2 & b2 /. b4 in rng (Line b1,b3) ) ) & ( for b3 being Nat st 1 <= b3 & b3 <= len b1 & 2 <= len b2 holds
L~ b2 meets rng (Line b1,b3) ) & ( for b3, b4, b5, b6 being Nat st 1 <= b3 & b3 <= len b1 & 1 <= b4 & b4 <= len b1 & b5 in dom b2 & b6 in dom b2 & b2 /. b5 in rng (Line b1,b3) & ( for b7 being Nat st b7 in dom b2 & b2 /. b7 in rng (Line b1,b3) holds
b7 <= b5 ) & b5 < b6 & b2 /. b6 in rng (Line b1,b4) holds
b3 < b4 ) )
proof end;

theorem Th46: :: GOBOARD1:46
for b1 being Nat
for b2 being Go-board
for b3 being FinSequence of (TOP-REAL 2) st b3 is_sequence_on b2 & b1 in dom b3 holds
ex b4 being Nat st
( b4 in Seg (width b2) & b3 /. b1 in rng (Col b2,b4) )
proof end;

theorem Th47: :: GOBOARD1:47
for b1, b2 being Nat
for b3 being Go-board
for b4 being FinSequence of (TOP-REAL 2) st b4 is_sequence_on b3 & b1 in dom b4 & b1 + 1 in dom b4 & b2 in Seg (width b3) & b4 /. b1 in rng (Col b3,b2) & not b4 /. (b1 + 1) in rng (Col b3,b2) holds
for b5 being Nat st b4 /. (b1 + 1) in rng (Col b3,b5) & b5 in Seg (width b3) holds
abs (b2 - b5) = 1
proof end;

theorem Th48: :: GOBOARD1:48
for b1, b2 being Nat
for b3 being Go-board
for b4 being FinSequence of (TOP-REAL 2) st 1 <= len b4 & b4 /. (len b4) in rng (Col b3,(width b3)) & b4 is_sequence_on b3 & b1 in Seg (width b3) & b1 + 1 in Seg (width b3) & b2 in dom b4 & b4 /. b2 in rng (Col b3,b1) & ( for b5 being Nat st b5 in dom b4 & b4 /. b5 in rng (Col b3,b1) holds
b5 <= b2 ) holds
( b2 + 1 in dom b4 & b4 /. (b2 + 1) in rng (Col b3,(b1 + 1)) )
proof end;

theorem Th49: :: GOBOARD1:49
for b1 being Go-board
for b2 being FinSequence of (TOP-REAL 2) st 1 <= len b2 & b2 /. 1 in rng (Col b1,1) & b2 /. (len b2) in rng (Col b1,(width b1)) & b2 is_sequence_on b1 holds
( ( for b3 being Nat st 1 <= b3 & b3 <= width b1 holds
ex b4 being Nat st
( b4 in dom b2 & b2 /. b4 in rng (Col b1,b3) ) ) & ( for b3 being Nat st 1 <= b3 & b3 <= width b1 & 2 <= len b2 holds
L~ b2 meets rng (Col b1,b3) ) & ( for b3, b4, b5, b6 being Nat st 1 <= b3 & b3 <= width b1 & 1 <= b4 & b4 <= width b1 & b5 in dom b2 & b6 in dom b2 & b2 /. b5 in rng (Col b1,b3) & ( for b7 being Nat st b7 in dom b2 & b2 /. b7 in rng (Col b1,b3) holds
b7 <= b5 ) & b5 < b6 & b2 /. b6 in rng (Col b1,b4) holds
b3 < b4 ) )
proof end;

theorem Th50: :: GOBOARD1:50
for b1, b2 being Nat
for b3 being Go-board
for b4 being FinSequence of (TOP-REAL 2) st b1 in dom b4 & b4 /. b1 in rng (Col b3,b2) & b2 in Seg (width b3) & b4 /. 1 in rng (Col b3,1) & b4 is_sequence_on b3 & ( for b5 being Nat st b5 in dom b4 & b4 /. b5 in rng (Col b3,b2) holds
b1 <= b5 ) holds
for b5 being Nat st b5 in dom b4 & b5 <= b1 holds
for b6 being Nat st b6 in Seg (width b3) & b4 /. b5 in rng (Col b3,b6) holds
b6 <= b2
proof end;

theorem Th51: :: GOBOARD1:51
for b1 being Go-board
for b2 being FinSequence of (TOP-REAL 2) st b2 is_sequence_on b1 & b2 /. 1 in rng (Col b1,1) & b2 /. (len b2) in rng (Col b1,(width b1)) & width b1 > 1 & 1 <= len b2 holds
ex b3 being FinSequence of (TOP-REAL 2) st
( b3 /. 1 in rng (Col (DelCol b1,(width b1)),1) & b3 /. (len b3) in rng (Col (DelCol b1,(width b1)),(width (DelCol b1,(width b1)))) & 1 <= len b3 & b3 is_sequence_on DelCol b1,(width b1) & rng b3 c= rng b2 )
proof end;

theorem Th52: :: GOBOARD1:52
for b1 being Go-board
for b2 being FinSequence of (TOP-REAL 2) st b2 is_sequence_on b1 & (rng b2) /\ (rng (Col b1,1)) <> {} & (rng b2) /\ (rng (Col b1,(width b1))) <> {} holds
ex b3 being FinSequence of (TOP-REAL 2) st
( rng b3 c= rng b2 & b3 /. 1 in rng (Col b1,1) & b3 /. (len b3) in rng (Col b1,(width b1)) & 1 <= len b3 & b3 is_sequence_on b1 )
proof end;

theorem Th53: :: GOBOARD1:53
for b1, b2 being Nat
for b3 being Go-board
for b4 being FinSequence of (TOP-REAL 2) st b1 in dom b3 & b4 is_sequence_on b3 & b4 /. (len b4) in rng (Line b3,(len b3)) & b2 in dom b4 & b4 /. b2 in rng (Line b3,b1) holds
( ( for b5 being Nat st b1 <= b5 & b5 <= len b3 holds
ex b6 being Nat st
( b6 in dom b4 & b2 <= b6 & b4 /. b6 in rng (Line b3,b5) ) ) & ( for b5 being Nat st b1 < b5 & b5 <= len b3 holds
ex b6 being Nat st
( b6 in dom b4 & b2 < b6 & b4 /. b6 in rng (Line b3,b5) ) ) )
proof end;