:: GOBOARD4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: GOBOARD4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) 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,(width G)) holds
rng f1 meets rng f2
proof end;

theorem Th2: :: GOBOARD4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) 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,(width G)) holds
L~ f1 meets L~ f2
proof end;

theorem :: GOBOARD4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) 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,(width G)) holds
L~ f1 meets L~ f2 by Th2;

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

:: deftheorem Def1 defines lies_between GOBOARD4:def 1 :
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence of (TOP-REAL 2) 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence of (TOP-REAL 2) 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GOBOARD4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GOBOARD4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P1, P2 being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p1 `1 <= p `1 & p `1 <= q1 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p2 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P1 meets P2
proof end;