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

theorem Th1: :: GOBOARD5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being tabular FinSequence
for i, j being Nat st [i,j] in Indices M holds
( 1 <= i & i <= len M & 1 <= j & j <= width M )
proof end;

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

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

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

theorem Th2: :: GOBOARD5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i being Nat
for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G holds
(G * i,j) `2 = (G * 1,j) `2
proof end;

theorem Th3: :: GOBOARD5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i being Nat
for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G holds
(G * i,j) `1 = (G * i,1) `1
proof end;

theorem Th4: :: GOBOARD5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i1, i2 being Nat
for G being Matrix of (TOP-REAL 2) st G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds
(G * i1,j) `1 < (G * i2,j) `1
proof end;

theorem Th5: :: GOBOARD5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j1, j2, i being Nat
for G being Matrix of (TOP-REAL 2) st G is Y_increasing-in-line & 1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G holds
(G * i,j1) `2 < (G * i,j2) `2
proof end;

theorem Th6: :: GOBOARD5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i being Nat
for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G holds
h_strip G,j = { |[r,s]| where r, s is Real : ( (G * i,j) `2 <= s & s <= (G * i,(j + 1)) `2 ) }
proof end;

theorem Th7: :: GOBOARD5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is Y_equal-in-column & 1 <= i & i <= len G holds
h_strip G,(width G) = { |[r,s]| where r, s is Real : (G * i,(width G)) `2 <= s }
proof end;

theorem Th8: :: GOBOARD5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is Y_equal-in-column & 1 <= i & i <= len G holds
h_strip G,0 = { |[r,s]| where r, s is Real : s <= (G * i,1) `2 }
proof end;

theorem Th9: :: GOBOARD5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G holds
v_strip G,i = { |[r,s]| where r, s is Real : ( (G * i,j) `1 <= r & r <= (G * (i + 1),j) `1 ) }
proof end;

theorem Th10: :: GOBOARD5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j being Nat
for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is X_equal-in-line & 1 <= j & j <= width G holds
v_strip G,(len G) = { |[r,s]| where r, s is Real : (G * (len G),j) `1 <= r }
proof end;

theorem Th11: :: GOBOARD5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j being Nat
for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is X_equal-in-line & 1 <= j & j <= width G holds
v_strip G,0 = { |[r,s]| where r, s is Real : r <= (G * 1,j) `1 }
proof end;

definition
let G be Matrix of (TOP-REAL 2);
let i, j be Nat;
func cell G,i,j -> Subset of (TOP-REAL 2) equals :: GOBOARD5:def 3
(v_strip G,i) /\ (h_strip G,j);
correctness
coherence
(v_strip G,i) /\ (h_strip G,j) is Subset of (TOP-REAL 2);
;
end;

:: deftheorem defines cell GOBOARD5:def 3 :
for G being Matrix of (TOP-REAL 2)
for i, j being Nat holds cell G,i,j = (v_strip G,i) /\ (h_strip G,j);

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

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

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

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

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;

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

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

theorem Th12: :: GOBOARD5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non empty FinSequence of (TOP-REAL 2)
for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * i,j )
proof end;

theorem Th13: :: GOBOARD5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non empty standard FinSequence of (TOP-REAL 2)
for n being Nat st n in dom f & n + 1 in dom f holds
for m, k, i, j being Nat st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * m,k & f /. (n + 1) = (GoB f) * i,j holds
(abs (m - i)) + (abs (k - j)) = 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 f be standard special_circular_sequence;
let k be Nat;
assume A1: ( 1 <= k & k + 1 <= len f ) ;
k <= k + 1 by NAT_1:29;
then k <= len f by A1, XREAL_1:2;
then A2: k in dom f by A1, FINSEQ_3:27;
then consider i1, j1 being Nat such that
A3: ( [i1,j1] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 ) by Th12;
k + 1 >= 1 by NAT_1:29;
then A4: k + 1 in dom f by A1, FINSEQ_3:27;
then consider i2, j2 being Nat such that
A5: ( [i2,j2] in Indices (GoB f) & f /. (k + 1) = (GoB f) * i2,j2 ) by Th12;
A6: (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A2, A3, A4, A5, Th13;
A7: now
per cases ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( i1 = i2 & abs (j1 - j2) = 1 ) ) by A6, GOBOARD1:2;
case that A8: abs (i1 - i2) = 1 and
A9: j1 = j2 ; :: thesis: ( ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 )
( i1 - i2 >= 0 or i1 - i2 < 0 ) ;
then ( i1 - i2 = 1 or - (i1 - i2) = 1 ) by A8, ABSVALUE:def 1;
hence ( i1 = i2 + 1 or i1 + 1 = i2 ) ; :: thesis: j1 = j2
thus j1 = j2 by A9; :: thesis: verum
end;
case that A10: i1 = i2 and
A11: abs (j1 - j2) = 1 ; :: thesis: ( ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 )
( j1 - j2 >= 0 or j1 - j2 < 0 ) ;
then ( j1 - j2 = 1 or - (j1 - j2) = 1 ) by A11, ABSVALUE:def 1;
hence ( j1 = j2 + 1 or j1 + 1 = j2 ) ; :: thesis: i1 = i2
thus i1 = i2 by A10; :: thesis: verum
end;
end;
end;
func right_cell f,k -> Subset of (TOP-REAL 2) means :Def6: :: GOBOARD5:def 6
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & it = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & it = cell (GoB f),(i1 -' 1),j2 );
existence
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (GoB f),(i1 -' 1),j2 )
proof end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (GoB f),(i1 -' 1),j2 ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell (GoB f),(i1 -' 1),j2 ) ) holds
b1 = b2
proof end;
func left_cell f,k -> Subset of (TOP-REAL 2) means :Def7: :: GOBOARD5:def 7
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & it = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & it = cell (GoB f),i1,j2 );
existence
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (GoB f),i1,j2 )
proof end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (GoB f),i1,j2 ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell (GoB f),i1,j2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines right_cell GOBOARD5:def 6 :
for f being standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
for b3 being Subset of (TOP-REAL 2) holds
( b3 = right_cell f,k iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b3 = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b3 = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b3 = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b3 = cell (GoB f),(i1 -' 1),j2 ) );

:: deftheorem Def7 defines left_cell GOBOARD5:def 7 :
for f being standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
for b3 being Subset of (TOP-REAL 2) holds
( b3 = left_cell f,k iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b3 = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b3 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b3 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b3 = cell (GoB f),i1,j2 ) );

theorem Th14: :: GOBOARD5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G holds
LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) c= v_strip G,i
proof end;

theorem Th15: :: GOBOARD5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G holds
LSeg (G * i,j),(G * i,(j + 1)) c= v_strip G,i
proof end;

theorem Th16: :: GOBOARD5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i being Nat
for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is Y_equal-in-column & G is Y_increasing-in-line & j < width G & 1 <= i & i < len G holds
LSeg (G * i,(j + 1)),(G * (i + 1),(j + 1)) c= h_strip G,j
proof end;

theorem Th17: :: GOBOARD5:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i being Nat
for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G holds
LSeg (G * i,j),(G * (i + 1),j) c= h_strip G,j
proof end;

theorem Th18: :: GOBOARD5:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G holds
LSeg (G * i,j),(G * i,(j + 1)) c= h_strip G,j
proof end;

theorem Th19: :: GOBOARD5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for G being Go-board st i < len G & 1 <= j & j < width G holds
LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) c= cell G,i,j
proof end;

theorem Th20: :: GOBOARD5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for G being Go-board st 1 <= i & i <= len G & 1 <= j & j < width G holds
LSeg (G * i,j),(G * i,(j + 1)) c= cell G,i,j
proof end;

theorem Th21: :: GOBOARD5:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i being Nat
for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i & i + 1 <= len G holds
LSeg (G * i,j),(G * (i + 1),j) c= v_strip G,i
proof end;

theorem Th22: :: GOBOARD5:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i being Nat
for G being Go-board st j < width G & 1 <= i & i < len G holds
LSeg (G * i,(j + 1)),(G * (i + 1),(j + 1)) c= cell G,i,j
proof end;

theorem Th23: :: GOBOARD5:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for G being Go-board st 1 <= i & i < len G & 1 <= j & j <= width G holds
LSeg (G * i,j),(G * (i + 1),j) c= cell G,i,j
proof end;

theorem Th24: :: GOBOARD5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G holds
(v_strip G,i) /\ (v_strip G,(i + 1)) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 }
proof end;

theorem Th25: :: GOBOARD5:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j being Nat
for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G holds
(h_strip G,j) /\ (h_strip G,(j + 1)) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * 1,(j + 1)) `2 }
proof end;

theorem Th26: :: GOBOARD5:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for G being Go-board st i < len G & 1 <= j & j < width G holds
(cell G,i,j) /\ (cell G,(i + 1),j) = LSeg (G * (i + 1),j),(G * (i + 1),(j + 1))
proof end;

theorem Th27: :: GOBOARD5:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i being Nat
for G being Go-board st j < width G & 1 <= i & i < len G holds
(cell G,i,j) /\ (cell G,i,(j + 1)) = LSeg (G * i,(j + 1)),(G * (i + 1),(j + 1))
proof end;

theorem Th28: :: GOBOARD5:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i, j being Nat
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * (i + 1),j & f /. (k + 1) = (GoB f) * (i + 1),(j + 1) holds
( left_cell f,k = cell (GoB f),i,j & right_cell f,k = cell (GoB f),(i + 1),j )
proof end;

theorem Th29: :: GOBOARD5:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i, j being Nat
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * i,(j + 1) & f /. (k + 1) = (GoB f) * (i + 1),(j + 1) holds
( left_cell f,k = cell (GoB f),i,(j + 1) & right_cell f,k = cell (GoB f),i,j )
proof end;

theorem Th30: :: GOBOARD5:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i, j being Nat
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * (i + 1),(j + 1) & f /. (k + 1) = (GoB f) * i,(j + 1) holds
( left_cell f,k = cell (GoB f),i,j & right_cell f,k = cell (GoB f),i,(j + 1) )
proof end;

theorem Th31: :: GOBOARD5:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i, j being Nat
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),(j + 1)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) & f /. k = (GoB f) * (i + 1),(j + 1) & f /. (k + 1) = (GoB f) * (i + 1),j holds
( left_cell f,k = cell (GoB f),(i + 1),j & right_cell f,k = cell (GoB f),i,j )
proof end;

theorem :: GOBOARD5:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
(left_cell f,k) /\ (right_cell f,k) = LSeg f,k
proof end;