:: GOBOARD9 semantic presentation

Lm1: for a being natural number holds a -' a = 0
by BINARITH:51;

Lm2: for a, b being natural number holds a -' b <= a
by BINARITH:52;

theorem :: GOBOARD9:1

canceled;

theorem :: GOBOARD9:2

canceled;

theorem Th3: :: GOBOARD9:3

for GX being TopSpace
for A1, A2, B being Subset of GX st A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 holds
A1 misses A2

proof end;

theorem Th4: :: GOBOARD9:4

for GX being TopSpace
for A, B being Subset of GX
for AA being Subset of (GX | B) st A = AA holds
GX | A = (GX | B) | AA

proof end;

theorem Th5: :: GOBOARD9:5

for GX being non empty TopSpace
for A, B being non empty Subset of GX st A c= B & A is connected holds
ex C being Subset of GX st
( C is_a_component_of B & A c= C )

proof end;

theorem Th6: :: GOBOARD9:6

for GX being non empty TopSpace
for A, B, C, D being Subset of GX st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D holds
B c= C

proof end;

theorem Th7: :: GOBOARD9:7

for p, q being Point of (TOP-REAL 2) holds LSeg p,q is convex

proof end;

theorem Th8: :: GOBOARD9:8

for p, q being Point of (TOP-REAL 2) holds LSeg p,q is connected

proof end;

registration

cluster non empty convex Element of K40(the carrier of (TOP-REAL 2));
existence

proof end;

end;

theorem Th9: :: GOBOARD9:9

for P, Q being convex Subset of (TOP-REAL 2) holds P /\ Q is convex

proof end;

theorem Th10: :: GOBOARD9:10

for f being FinSequence of (TOP-REAL 2) holds Rev (X_axis f) = X_axis (Rev f)

proof end;

theorem Th11: :: GOBOARD9:11

for f being FinSequence of (TOP-REAL 2) holds Rev (Y_axis f) = Y_axis (Rev f)

proof end;

Lm3: for f, ff being non empty FinSequence of (TOP-REAL 2) st ff = Rev f holds
GoB ff = GoB f

proof end;

registration

cluster non constant set ;
existence

proof end;

end;

registration

let f be non constant FinSequence;
cluster Rev f -> non constant ;
coherence

proof end;

end;

definition

let f be standard special_circular_sequence;
:: original: Rev
redefine func Rev f -> standard special_circular_sequence;
coherence

proof end;

end;

theorem Th12: :: GOBOARD9:12

for f being non constant standard special_circular_sequence
for i, j being Nat st i >= 1 & j >= 1 & i + j = len f holds
left_cell f,i = right_cell (Rev f),j

proof end;

theorem Th13: :: GOBOARD9:13

for f being non constant standard special_circular_sequence
for i, j being Nat st i >= 1 & j >= 1 & i + j = len f holds
left_cell (Rev f),i = right_cell f,j

proof end;

theorem Th14: :: GOBOARD9:14

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
ex i, j being Nat st
( i <= len (GoB f) & j <= width (GoB f) & cell (GoB f),i,j = left_cell f,k )

proof end;

theorem Th15: :: GOBOARD9:15

for j being Nat
for G being Go-board st j <= width G holds
Int (h_strip G,j) is convex

proof end;

theorem Th16: :: GOBOARD9:16

for i being Nat
for G being Go-board st i <= len G holds
Int (v_strip G,i) is convex

proof end;

theorem Th17: :: GOBOARD9:17

for i, j being Nat
for G being Go-board st i <= len G & j <= width G holds
Int (cell G,i,j) <> {}

proof end;

theorem Th18: :: GOBOARD9:18

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
Int (left_cell f,k) <> {}

proof end;

theorem Th19: :: GOBOARD9:19

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
Int (right_cell f,k) <> {}

proof end;

theorem Th20: :: GOBOARD9:20

for i, j being Nat
for G being Go-board st i <= len G & j <= width G holds
Int (cell G,i,j) is convex

proof end;

theorem Th21: :: GOBOARD9:21

for i, j being Nat
for G being Go-board st i <= len G & j <= width G holds
Int (cell G,i,j) is connected

proof end;

theorem Th22: :: GOBOARD9:22

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
Int (left_cell f,k) is connected

proof end;

theorem Th23: :: GOBOARD9:23

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
Int (right_cell f,k) is connected

proof end;

definition

let f be non constant standard special_circular_sequence;
4 < len f by GOBOARD7:36;
then A1: 1 + 1 < len f by XREAL_1:2;
then A2: Int (left_cell f,1) <> {} by Th18;
A3: Int (right_cell f,1) <> {} by A1, Th19;
func LeftComp f -> Subset of (TOP-REAL 2) means :Def1: :: GOBOARD9:def 1
( it is_a_component_of (L~ f) ` & Int (left_cell f,1) c= it );
existence

proof end;

uniqueness

proof end;

func RightComp f -> Subset of (TOP-REAL 2) means :Def2: :: GOBOARD9:def 2
( it is_a_component_of (L~ f) ` & Int (right_cell f,1) c= it );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines LeftComp GOBOARD9:def 1 :

:: deftheorem Def2 defines RightComp GOBOARD9:def 2 :

theorem Th24: :: GOBOARD9:24

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
Int (left_cell f,k) c= LeftComp f

proof end;

theorem :: GOBOARD9:25

for f being non constant standard special_circular_sequence holds GoB (Rev f) = GoB f by Lm3;

theorem Th26: :: GOBOARD9:26

for f being non constant standard special_circular_sequence holds RightComp f = LeftComp (Rev f)

proof end;

theorem :: GOBOARD9:27

for f being non constant standard special_circular_sequence holds RightComp (Rev f) = LeftComp f

proof end;

theorem :: GOBOARD9:28

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
Int (right_cell f,k) c= RightComp f

proof end;