:: Go-Board Theorem
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Copyright (c) 1992-2021 Association of Mizar Users

theorem Th1: :: GOBOARD4:1
for G being Go-board
for f1, f2 being FinSequence of () st 1 <= len f1 & 1 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,())) holds
rng f1 meets rng f2
proof end;

theorem Th2: :: GOBOARD4:2
for G being Go-board
for f1, f2 being FinSequence of () st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,())) holds
L~ f1 meets L~ f2
proof end;

theorem :: GOBOARD4:3
for G being Go-board
for f1, f2 being FinSequence of () st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,())) holds
L~ f1 meets L~ f2 by Th2;

definition
let f be Relation;
let r, s be Real;
pred f lies_between r,s means :: GOBOARD4:def 1
rng f c= [.r,s.];
end;

:: deftheorem defines lies_between GOBOARD4:def 1 :
for f being Relation
for r, s being Real holds
( f lies_between r,s iff rng f c= [.r,s.] );

definition
let f be FinSequence of REAL ;
let r, s be Real;
redefine pred f lies_between r,s means :: GOBOARD4:def 2
for n being Nat st n in dom f holds
( r <= f . n & f . n <= s );
compatibility
( f lies_between r,s iff for n being Nat st n in dom f holds
( r <= f . n & f . n <= s ) )
proof end;
end;

:: deftheorem defines lies_between GOBOARD4:def 2 :
for f being FinSequence of REAL
for r, s being Real holds
( f lies_between r,s iff for n being Nat st n in dom f holds
( r <= f . n & f . n <= s ) );

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

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

theorem :: GOBOARD4:6
for P1, P2 being Subset of ()
for p1, p2, q1, q2 being Point of () st P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 & ( for p being Point of () st p in P1 \/ P2 holds
( p1 1 <= p 1 & p 1 <= q1 1 ) ) & ( for p being Point of () st p in P1 \/ P2 holds
( p2 2 <= p 2 & p 2 <= q2 2 ) ) holds
P1 meets P2
proof end;