:: GOBOARD9 semantic presentation

Lemma1: for b₁ being natural number holds b₁ -' b₁ = 0
by BINARITH:51;

Lemma2: for b₁, b₂ being natural number holds b₁ -' b₂ <= b₁
by BINARITH:52;

theorem Th1: :: GOBOARD9:1

canceled;

theorem Th2: :: GOBOARD9:2

canceled;

theorem Th3: :: GOBOARD9:3

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is_a_component_of b₄ & b₃ is_a_component_of b₄ & not b₂ = b₃ holds
b₂ misses b₃

proof end;

theorem Th4: :: GOBOARD9:4

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Subset of (b₁ | b₃) st b₂ = b₄ holds
b₁ | b₂ = (b₁ | b₃) | b₄

proof end;

theorem Th5: :: GOBOARD9:5

for b₁ being non empty TopSpace
for b₂, b₃ being non empty Subset of b₁ st b₂ c= b₃ & b₂ is connected holds
ex b₄ being Subset of b₁ st
( b₄ is_a_component_of b₃ & b₂ c= b₄ )

proof end;

theorem Th6: :: GOBOARD9:6

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₃ is connected & b₄ is_a_component_of b₅ & b₂ c= b₄ & b₂ meets b₃ & b₃ c= b₅ holds
b₃ c= b₄

proof end;

theorem Th7: :: GOBOARD9:7

for b₁, b₂ being Point of (TOP-REAL 2) holds LSeg b₁,b₂ is convex

proof end;

theorem Th8: :: GOBOARD9:8

for b₁, b₂ being Point of (TOP-REAL 2) holds LSeg b₁,b₂ 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 b₁, b₂ being convex Subset of (TOP-REAL 2) holds b₁ /\ b₂ is convex

proof end;

theorem Th10: :: GOBOARD9:10

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

proof end;

theorem Th11: :: GOBOARD9:11

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

proof end;

Lemma12: for b₁, b₂ being non empty FinSequence of (TOP-REAL 2) st b₂ = Rev b₁ holds
GoB b₂ = GoB b₁

proof end;

registration

cluster non constant set ;
existence

proof end;

end;

registration

let c₁ be non constant FinSequence;
cluster Rev a₁ -> non constant ;
coherence

proof end;

end;

definition

let c₁ be standard special_circular_sequence;
redefine func Rev as Rev c₁ -> standard special_circular_sequence;
coherence

proof end;

end;

theorem Th12: :: GOBOARD9:12

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st b₂ >= 1 & b₃ >= 1 & b₂ + b₃ = len b₁ holds
left_cell b₁,b₂ = right_cell (Rev b₁),b₃

proof end;

theorem Th13: :: GOBOARD9:13

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st b₂ >= 1 & b₃ >= 1 & b₂ + b₃ = len b₁ holds
left_cell (Rev b₁),b₂ = right_cell b₁,b₃

proof end;

theorem Th14: :: GOBOARD9:14

for b₁ being non constant standard special_circular_sequence
for b₂ being Nat st 1 <= b₂ & b₂ + 1 <= len b₁ holds
ex b₃, b₄ being Nat st
( b₃ <= len (GoB b₁) & b₄ <= width (GoB b₁) & cell (GoB b₁),b₃,b₄ = left_cell b₁,b₂ )

proof end;

theorem Th15: :: GOBOARD9:15

for b₁ being Nat
for b₂ being Go-board st b₁ <= width b₂ holds
Int (h_strip b₂,b₁) is convex

proof end;

theorem Th16: :: GOBOARD9:16

for b₁ being Nat
for b₂ being Go-board st b₁ <= len b₂ holds
Int (v_strip b₂,b₁) is convex

proof end;

theorem Th17: :: GOBOARD9:17

for b₁, b₂ being Nat
for b₃ being Go-board st b₁ <= len b₃ & b₂ <= width b₃ holds
Int (cell b₃,b₁,b₂) <> {}

proof end;

theorem Th18: :: GOBOARD9:18

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

proof end;

theorem Th19: :: GOBOARD9:19

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

proof end;

theorem Th20: :: GOBOARD9:20

for b₁, b₂ being Nat
for b₃ being Go-board st b₁ <= len b₃ & b₂ <= width b₃ holds
Int (cell b₃,b₁,b₂) is convex

proof end;

theorem Th21: :: GOBOARD9:21

for b₁, b₂ being Nat
for b₃ being Go-board st b₁ <= len b₃ & b₂ <= width b₃ holds
Int (cell b₃,b₁,b₂) is connected

proof end;

theorem Th22: :: GOBOARD9:22

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

proof end;

theorem Th23: :: GOBOARD9:23

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

proof end;

definition

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

proof end;

uniqueness

proof end;

func RightComp c₁ -> Subset of (TOP-REAL 2) means :Def2: :: GOBOARD9:def 2
( a₂ is_a_component_of (L~ a₁) ` & Int (right_cell a₁,1) c= a₂ );
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 b₁ being non constant standard special_circular_sequence
for b₂ being Nat st 1 <= b₂ & b₂ + 1 <= len b₁ holds
Int (left_cell b₁,b₂) c= LeftComp b₁

proof end;

theorem Th25: :: GOBOARD9:25

for b₁ being non constant standard special_circular_sequence holds GoB (Rev b₁) = GoB b₁ by Lemma12;

theorem Th26: :: GOBOARD9:26

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

proof end;

theorem Th27: :: GOBOARD9:27

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

proof end;

theorem Th28: :: GOBOARD9:28

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

proof end;