:: GOBOARD4 semantic presentation

theorem Th1: :: GOBOARD4:1
for b1 being Go-board
for b2, b3 being FinSequence of (TOP-REAL 2) st 1 <= len b2 & 1 <= len b3 & b2 is_sequence_on b1 & b3 is_sequence_on b1 & b2 /. 1 in rng (Line b1,1) & b2 /. (len b2) in rng (Line b1,(len b1)) & b3 /. 1 in rng (Col b1,1) & b3 /. (len b3) in rng (Col b1,(width b1)) holds
rng b2 meets rng b3
proof end;

theorem Th2: :: GOBOARD4:2
for b1 being Go-board
for b2, b3 being FinSequence of (TOP-REAL 2) st 2 <= len b2 & 2 <= len b3 & b2 is_sequence_on b1 & b3 is_sequence_on b1 & b2 /. 1 in rng (Line b1,1) & b2 /. (len b2) in rng (Line b1,(len b1)) & b3 /. 1 in rng (Col b1,1) & b3 /. (len b3) in rng (Col b1,(width b1)) holds
L~ b2 meets L~ b3
proof end;

theorem Th3: :: GOBOARD4:3
for b1 being Go-board
for b2, b3 being FinSequence of (TOP-REAL 2) st 2 <= len b2 & 2 <= len b3 & b2 is_sequence_on b1 & b3 is_sequence_on b1 & b2 /. 1 in rng (Line b1,1) & b2 /. (len b2) in rng (Line b1,(len b1)) & b3 /. 1 in rng (Col b1,1) & b3 /. (len b3) in rng (Col b1,(width b1)) holds
L~ b2 meets L~ b3 by Th2;

definition
let c1 be FinSequence of REAL ;
let c2, c3 be Real;
pred c1 lies_between c2,c3 means :Def1: :: GOBOARD4:def 1
for b1 being Nat st b1 in dom a1 holds
( a2 <= a1 . b1 & a1 . b1 <= a3 );
end;

:: deftheorem Def1 defines lies_between GOBOARD4:def 1 :
for b1 being FinSequence of REAL
for b2, b3 being Real holds
( b1 lies_between b2,b3 iff for b4 being Nat st b4 in dom b1 holds
( b2 <= b1 . b4 & b1 . b4 <= b3 ) );

theorem Th4: :: GOBOARD4:4
for b1, b2 being FinSequence of (TOP-REAL 2) st 2 <= len b1 & 2 <= len b2 & b1 is special & b2 is special & ( for b3 being Nat st b3 in dom b1 & b3 + 1 in dom b1 holds
b1 /. b3 <> b1 /. (b3 + 1) ) & ( for b3 being Nat st b3 in dom b2 & b3 + 1 in dom b2 holds
b2 /. b3 <> b2 /. (b3 + 1) ) & X_axis b1 lies_between (X_axis b1) . 1,(X_axis b1) . (len b1) & X_axis b2 lies_between (X_axis b1) . 1,(X_axis b1) . (len b1) & Y_axis b1 lies_between (Y_axis b2) . 1,(Y_axis b2) . (len b2) & Y_axis b2 lies_between (Y_axis b2) . 1,(Y_axis b2) . (len b2) holds
L~ b1 meets L~ b2
proof end;

theorem Th5: :: GOBOARD4:5
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 is one-to-one & b1 is special & 2 <= len b1 & b2 is one-to-one & b2 is special & 2 <= len b2 & X_axis b1 lies_between (X_axis b1) . 1,(X_axis b1) . (len b1) & X_axis b2 lies_between (X_axis b1) . 1,(X_axis b1) . (len b1) & Y_axis b1 lies_between (Y_axis b2) . 1,(Y_axis b2) . (len b2) & Y_axis b2 lies_between (Y_axis b2) . 1,(Y_axis b2) . (len b2) holds
L~ b1 meets L~ b2
proof end;

theorem Th6: :: GOBOARD4:6
canceled;

theorem Th7: :: GOBOARD4:7
canceled;

theorem Th8: :: GOBOARD4:8
for b1, b2 being Subset of (TOP-REAL 2)
for b3, b4, b5, b6 being Point of (TOP-REAL 2) st b1 is_S-P_arc_joining b3,b5 & b2 is_S-P_arc_joining b4,b6 & ( for b7 being Point of (TOP-REAL 2) st b7 in b1 \/ b2 holds
( b3 `1 <= b7 `1 & b7 `1 <= b5 `1 ) ) & ( for b7 being Point of (TOP-REAL 2) st b7 in b1 \/ b2 holds
( b4 `2 <= b7 `2 & b7 `2 <= b6 `2 ) ) holds
b1 meets b2
proof end;