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

definition
let E be non empty set ;
let S be FinSequence-DOMAIN of the carrier of (TOP-REAL 2);
let F be Function of E,S;
let e be Element of E;
:: original: .
redefine func F . e -> FinSequence of (TOP-REAL 2);
coherence
F . e is FinSequence of (TOP-REAL 2)
proof end;
end;

definition
let F be Function;
func Values F -> set equals :: GOBRD13:def 1
Union (rngs F);
correctness
coherence
Union (rngs F) is set
;
;
end;

:: deftheorem defines Values GOBRD13:def 1 :
for F being Function holds Values F = Union (rngs F);

theorem Th1: :: GOBRD13:1  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 D being non empty set
for M being FinSequence of D * holds M . i is FinSequence of D
proof end;

registration
let D be set ;
cluster -> FinSequence-yielding FinSequence of D * ;
coherence
for b1 being FinSequence of D * holds b1 is FinSequence-yielding
proof end;
end;

registration
cluster FinSequence-yielding -> Function-yielding set ;
coherence
for b1 being Function st b1 is FinSequence-yielding holds
b1 is Function-yielding
proof end;
end;

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

theorem Th3: :: GOBRD13:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for M being FinSequence of D * holds Values M = union { (rng f) where f is Element of D * : f in rng M }
proof end;

registration
let D be non empty set ;
let M be FinSequence of D * ;
cluster Values M -> finite ;
coherence
Values M is finite
proof end;
end;

theorem Th4: :: GOBRD13:4  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 D being non empty set
for f being FinSequence of D
for M being Matrix of D st i in dom M & M . i = f holds
len f = width M
proof end;

theorem Th5: :: GOBRD13:5  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 D being non empty set
for f being FinSequence of D
for M being Matrix of D st i in dom M & M . i = f & j in dom f holds
[i,j] in Indices M
proof end;

theorem Th6: :: GOBRD13:6  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 D being non empty set
for f being FinSequence of D
for M being Matrix of D st [i,j] in Indices M & M . i = f holds
( len f = width M & j in dom f )
proof end;

theorem Th7: :: GOBRD13:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for M being Matrix of D holds Values M = { (M * i,j) where i, j is Nat : [i,j] in Indices M }
proof end;

theorem :: GOBRD13:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for M being Matrix of D holds card (Values M) <= (len M) * (width M)
proof end;

theorem :: GOBRD13:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for G being Matrix of (TOP-REAL 2) st f is_sequence_on G holds
rng f c= Values G
proof end;

theorem Th10: :: GOBRD13:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, j2 being Nat
for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 & G1 * i1,j1 = G2 * 1,j2 holds
i1 = 1
proof end;

theorem Th11: :: GOBRD13:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, j2 being Nat
for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 & G1 * i1,j1 = G2 * (len G2),j2 holds
i1 = len G1
proof end;

theorem Th12: :: GOBRD13:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, i2 being Nat
for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= i2 & i2 <= len G2 & G1 * i1,j1 = G2 * i2,1 holds
j1 = 1
proof end;

theorem Th13: :: GOBRD13:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, i2 being Nat
for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= i2 & i2 <= len G2 & G1 * i1,j1 = G2 * i2,(width G2) holds
j1 = width G1
proof end;

theorem Th14: :: GOBRD13:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, i2, j2 being Nat
for G1, G2 being Go-board st Values G1 c= Values G2 & 1 <= i1 & i1 < len G1 & 1 <= j1 & j1 <= width G1 & 1 <= i2 & i2 < len G2 & 1 <= j2 & j2 <= width G2 & G1 * i1,j1 = G2 * i2,j2 holds
(G2 * (i2 + 1),j2) `1 <= (G1 * (i1 + 1),j1) `1
proof end;

theorem Th15: :: GOBRD13:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, i2, j2 being Nat
for G1, G2 being Go-board st G1 * (i1 -' 1),j1 in Values G2 & 1 < i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 & 1 < i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 & G1 * i1,j1 = G2 * i2,j2 holds
(G1 * (i1 -' 1),j1) `1 <= (G2 * (i2 -' 1),j2) `1
proof end;

theorem Th16: :: GOBRD13:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, i2, j2 being Nat
for G1, G2 being Go-board st G1 * i1,(j1 + 1) in Values G2 & 1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 < width G1 & 1 <= i2 & i2 <= len G2 & 1 <= j2 & j2 < width G2 & G1 * i1,j1 = G2 * i2,j2 holds
(G2 * i2,(j2 + 1)) `2 <= (G1 * i1,(j1 + 1)) `2
proof end;

theorem Th17: :: GOBRD13:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, i2, j2 being Nat
for G1, G2 being Go-board st Values G1 c= Values G2 & 1 <= i1 & i1 <= len G1 & 1 < j1 & j1 <= width G1 & 1 <= i2 & i2 <= len G2 & 1 < j2 & j2 <= width G2 & G1 * i1,j1 = G2 * i2,j2 holds
(G1 * i1,(j1 -' 1)) `2 <= (G2 * i2,(j2 -' 1)) `2
proof end;

Lm1: for i, j being Nat
for D being non empty set
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
M * i,j in Values M
proof end;

theorem Th18: :: GOBRD13:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, i2, j2 being Nat
for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * i1,j1 = G2 * i2,j2 holds
cell G2,i2,j2 c= cell G1,i1,j1
proof end;

theorem Th19: :: GOBRD13:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, i2, j2 being Nat
for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * i1,j1 = G2 * i2,j2 holds
cell G2,(i2 -' 1),j2 c= cell G1,(i1 -' 1),j1
proof end;

theorem Th20: :: GOBRD13:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, i2, j2 being Nat
for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * i1,j1 = G2 * i2,j2 holds
cell G2,i2,(j2 -' 1) c= cell G1,i1,(j1 -' 1)
proof end;

Lm2: for i, j being Nat
for f being non empty FinSequence of (TOP-REAL 2) st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
ex k being Nat st
( k in dom f & (f /. k) `1 = ((GoB f) * i,j) `1 )
proof end;

Lm3: for i, j being Nat
for f being non empty FinSequence of (TOP-REAL 2) st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds
ex k being Nat st
( k in dom f & (f /. k) `2 = ((GoB f) * i,j) `2 )
proof end;

theorem Th21: :: GOBRD13:21  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 f being standard special_circular_sequence st f is_sequence_on G holds
Values (GoB f) c= Values G
proof end;

definition
let f be FinSequence of (TOP-REAL 2);
let G be Go-board;
let k be Nat;
assume that
A1: ( 1 <= k & k + 1 <= len f ) and
A2: f is_sequence_on G ;
consider i1, j1, i2, j2 being Nat such that
A3: ( [i1,j1] in Indices G & f /. k = G * i1,j1 ) and
A4: ( [i2,j2] in Indices G & f /. (k + 1) = G * i2,j2 ) and
A5: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, JORDAN8:6;
func right_cell f,k,G -> Subset of (TOP-REAL 2) means :Def2: :: GOBRD13:def 2
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & it = cell G,i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell G,i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell G,i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & it = cell G,(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 G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell G,i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell G,i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell G,i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell G,(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 G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell G,i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell G,i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell G,i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell G,(i1 -' 1),j2 ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell G,i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell G,i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell G,i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell G,(i1 -' 1),j2 ) ) holds
b1 = b2
proof end;
func left_cell f,k,G -> Subset of (TOP-REAL 2) means :Def3: :: GOBRD13:def 3
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & it = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & it = cell G,i1,j2 );
existence
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell G,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 G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell G,i1,j2 ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell G,i1,j2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines right_cell GOBRD13:def 2 :
for f being FinSequence of (TOP-REAL 2)
for G being Go-board
for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
for b4 being Subset of (TOP-REAL 2) holds
( b4 = right_cell f,k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b4 = cell G,i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b4 = cell G,i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b4 = cell G,i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b4 = cell G,(i1 -' 1),j2 ) );

:: deftheorem Def3 defines left_cell GOBRD13:def 3 :
for f being FinSequence of (TOP-REAL 2)
for G being Go-board
for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
for b4 being Subset of (TOP-REAL 2) holds
( b4 = left_cell f,k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b4 = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b4 = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b4 = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b4 = cell G,i1,j2 ) );

theorem Th22: :: GOBRD13:22  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * i,(j + 1) holds
left_cell f,k,G = cell G,(i -' 1),j
proof end;

theorem Th23: :: GOBRD13:23  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * i,(j + 1) holds
right_cell f,k,G = cell G,i,j
proof end;

theorem Th24: :: GOBRD13:24  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * (i + 1),j holds
left_cell f,k,G = cell G,i,j
proof end;

theorem Th25: :: GOBRD13:25  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * (i + 1),j holds
right_cell f,k,G = cell G,i,(j -' 1)
proof end;

theorem Th26: :: GOBRD13:26  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i + 1),j & f /. (k + 1) = G * i,j holds
left_cell f,k,G = cell G,i,(j -' 1)
proof end;

theorem Th27: :: GOBRD13:27  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i + 1),j & f /. (k + 1) = G * i,j holds
right_cell f,k,G = cell G,i,j
proof end;

theorem Th28: :: GOBRD13: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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * i,(j + 1) & f /. (k + 1) = G * i,j holds
left_cell f,k,G = cell G,i,j
proof end;

theorem Th29: :: GOBRD13: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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * i,(j + 1) & f /. (k + 1) = G * i,j holds
right_cell f,k,G = cell G,(i -' 1),j
proof end;

theorem :: GOBRD13:30  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
(left_cell f,k,G) /\ (right_cell f,k,G) = LSeg f,k
proof end;

theorem :: GOBRD13:31  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
right_cell f,k,G is closed
proof end;

theorem :: GOBRD13:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat
for f being FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & k + 1 <= n holds
( left_cell f,k,G = left_cell (f | n),k,G & right_cell f,k,G = right_cell (f | n),k,G )
proof end;

theorem :: GOBRD13:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat
for f being FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len (f /^ n) & n <= len f & f is_sequence_on G holds
( left_cell f,(k + n),G = left_cell (f /^ n),k,G & right_cell f,(k + n),G = right_cell (f /^ n),k,G )
proof end;

theorem :: GOBRD13:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for G being Go-board
for f being standard special_circular_sequence st 1 <= n & n + 1 <= len f & f is_sequence_on G holds
( left_cell f,n,G c= left_cell f,n & right_cell f,n,G c= right_cell f,n )
proof end;

definition
let f be FinSequence of (TOP-REAL 2);
let G be Go-board;
let k be Nat;
assume that
A1: ( 1 <= k & k + 1 <= len f ) and
A2: f is_sequence_on G ;
consider i1, j1, i2, j2 being Nat such that
A3: ( [i1,j1] in Indices G & f /. k = G * i1,j1 ) and
A4: ( [i2,j2] in Indices G & f /. (k + 1) = G * i2,j2 ) and
A5: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, JORDAN8:6;
func front_right_cell f,k,G -> Subset of (TOP-REAL 2) means :Def4: :: GOBRD13:def 4
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & it = cell G,i2,j2 ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell G,i2,(j2 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell G,(i2 -' 1),j2 ) holds
( i1 = i2 & j1 = j2 + 1 & it = cell G,(i2 -' 1),(j2 -' 1) );
existence
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell G,i2,j2 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell G,i2,(j2 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell G,(i2 -' 1),j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell G,(i2 -' 1),(j2 -' 1) )
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 G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell G,i2,j2 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell G,i2,(j2 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell G,(i2 -' 1),j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell G,(i2 -' 1),(j2 -' 1) ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell G,i2,j2 ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell G,i2,(j2 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell G,(i2 -' 1),j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell G,(i2 -' 1),(j2 -' 1) ) ) holds
b1 = b2
proof end;
func front_left_cell f,k,G -> Subset of (TOP-REAL 2) means :Def5: :: GOBRD13:def 5
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & it = cell G,(i2 -' 1),j2 ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell G,i2,j2 ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell G,(i2 -' 1),(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & it = cell G,i2,(j2 -' 1) );
existence
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell G,(i2 -' 1),j2 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell G,i2,j2 ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell G,(i2 -' 1),(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell G,i2,(j2 -' 1) )
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 G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell G,(i2 -' 1),j2 ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell G,i2,j2 ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell G,(i2 -' 1),(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell G,i2,(j2 -' 1) ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell G,(i2 -' 1),j2 ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell G,i2,j2 ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell G,(i2 -' 1),(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell G,i2,(j2 -' 1) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines front_right_cell GOBRD13:def 4 :
for f being FinSequence of (TOP-REAL 2)
for G being Go-board
for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
for b4 being Subset of (TOP-REAL 2) holds
( b4 = front_right_cell f,k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b4 = cell G,i2,j2 ) & not ( i1 + 1 = i2 & j1 = j2 & b4 = cell G,i2,(j2 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b4 = cell G,(i2 -' 1),j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b4 = cell G,(i2 -' 1),(j2 -' 1) ) );

:: deftheorem Def5 defines front_left_cell GOBRD13:def 5 :
for f being FinSequence of (TOP-REAL 2)
for G being Go-board
for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
for b4 being Subset of (TOP-REAL 2) holds
( b4 = front_left_cell f,k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b4 = cell G,(i2 -' 1),j2 ) & not ( i1 + 1 = i2 & j1 = j2 & b4 = cell G,i2,j2 ) & not ( i1 = i2 + 1 & j1 = j2 & b4 = cell G,(i2 -' 1),(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b4 = cell G,i2,(j2 -' 1) ) );

theorem :: GOBRD13:35  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * i,(j + 1) holds
front_left_cell f,k,G = cell G,(i -' 1),(j + 1)
proof end;

theorem :: GOBRD13:36  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * i,(j + 1) holds
front_right_cell f,k,G = cell G,i,(j + 1)
proof end;

theorem :: GOBRD13:37  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * (i + 1),j holds
front_left_cell f,k,G = cell G,(i + 1),j
proof end;

theorem :: GOBRD13:38  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * (i + 1),j holds
front_right_cell f,k,G = cell G,(i + 1),(j -' 1)
proof end;

theorem :: GOBRD13:39  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i + 1),j & f /. (k + 1) = G * i,j holds
front_left_cell f,k,G = cell G,(i -' 1),(j -' 1)
proof end;

theorem :: GOBRD13:40  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i + 1),j & f /. (k + 1) = G * i,j holds
front_right_cell f,k,G = cell G,(i -' 1),j
proof end;

theorem :: GOBRD13:41  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * i,(j + 1) & f /. (k + 1) = G * i,j holds
front_left_cell f,k,G = cell G,i,(j -' 1)
proof end;

theorem :: GOBRD13:42  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 FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * i,(j + 1) & f /. (k + 1) = G * i,j holds
front_right_cell f,k,G = cell G,(i -' 1),(j -' 1)
proof end;

theorem :: GOBRD13:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat
for f being FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & k + 1 <= n holds
( front_left_cell f,k,G = front_left_cell (f | n),k,G & front_right_cell f,k,G = front_right_cell (f | n),k,G )
proof end;

definition
let D be set ;
let f be FinSequence of D;
let G be Matrix of D;
let k be Nat;
pred f turns_right k,G means :Def6: :: GOBRD13:def 6
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * (i2 + 1),j2 ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * i2,(j2 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * i2,(j2 + 1) ) holds
( i1 = i2 & j1 = j2 + 1 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * (i2 -' 1),j2 );
pred f turns_left k,G means :Def7: :: GOBRD13:def 7
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * (i2 -' 1),j2 ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * i2,(j2 + 1) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * (i2 + 1),j2 );
pred f goes_straight k,G means :Def8: :: GOBRD13:def 8
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * i2,(j2 + 1) ) & not ( i1 + 1 = i2 & j1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * (i2 + 1),j2 ) & not ( i1 = i2 + 1 & j1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * (i2 -' 1),j2 ) holds
( i1 = i2 & j1 = j2 + 1 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * i2,(j2 -' 1) );
end;

:: deftheorem Def6 defines turns_right GOBRD13:def 6 :
for D being set
for f being FinSequence of D
for G being Matrix of D
for k being Nat holds
( f turns_right k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * (i2 + 1),j2 ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * i2,(j2 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * i2,(j2 + 1) ) holds
( i1 = i2 & j1 = j2 + 1 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * (i2 -' 1),j2 ) );

:: deftheorem Def7 defines turns_left GOBRD13:def 7 :
for D being set
for f being FinSequence of D
for G being Matrix of D
for k being Nat holds
( f turns_left k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * (i2 -' 1),j2 ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * i2,(j2 + 1) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * (i2 + 1),j2 ) );

:: deftheorem Def8 defines goes_straight GOBRD13:def 8 :
for D being set
for f being FinSequence of D
for G being Matrix of D
for k being Nat holds
( f goes_straight k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * i2,(j2 + 1) ) & not ( i1 + 1 = i2 & j1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * (i2 + 1),j2 ) & not ( i1 = i2 + 1 & j1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * (i2 -' 1),j2 ) holds
( i1 = i2 & j1 = j2 + 1 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * i2,(j2 -' 1) ) );

theorem :: GOBRD13:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat
for D being set
for f being FinSequence of D
for G being Matrix of D st 1 <= k & k + 2 <= len f & k + 2 <= n & f | n turns_right k,G holds
f turns_right k,G
proof end;

theorem :: GOBRD13:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat
for D being set
for f being FinSequence of D
for G being Matrix of D st 1 <= k & k + 2 <= len f & k + 2 <= n & f | n turns_left k,G holds
f turns_left k,G
proof end;

theorem :: GOBRD13:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat
for D being set
for f being FinSequence of D
for G being Matrix of D st 1 <= k & k + 2 <= len f & k + 2 <= n & f | n goes_straight k,G holds
f goes_straight k,G
proof end;

theorem :: GOBRD13:47  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 D being set
for f1, f2 being FinSequence of D
for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_right k -' 1,G & f2 turns_right k -' 1,G holds
f1 | (k + 1) = f2 | (k + 1)
proof end;

theorem :: GOBRD13:48  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 D being set
for f1, f2 being FinSequence of D
for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_left k -' 1,G & f2 turns_left k -' 1,G holds
f1 | (k + 1) = f2 | (k + 1)
proof end;

theorem :: GOBRD13:49  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 D being set
for f1, f2 being FinSequence of D
for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 goes_straight k -' 1,G & f2 goes_straight k -' 1,G holds
f1 | (k + 1) = f2 | (k + 1)
proof end;

theorem :: GOBRD13:50  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 D being non empty set
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
M * i,j in Values M by Lm1;