:: GOBRD12 semantic presentation

Lemma1: for b₁ being non constant standard special_circular_sequence holds (L~ b₁) ` = the carrier of ((TOP-REAL 2) | ((L~ b₁) ` ))

proof end;

Lemma2: the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:25;

theorem Th1: :: GOBRD12:1

canceled;

theorem Th2: :: GOBRD12:2

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st b₂ <= len (GoB b₁) & b₃ <= width (GoB b₁) holds
Int (cell (GoB b₁),b₂,b₃) c= (L~ b₁) `

proof end;

theorem Th3: :: GOBRD12:3

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st b₂ <= len (GoB b₁) & b₃ <= width (GoB b₁) holds
Cl (Down (Int (cell (GoB b₁),b₂,b₃)),((L~ b₁) ` )) = (cell (GoB b₁),b₂,b₃) /\ ((L~ b₁) ` )

proof end;

theorem Th4: :: GOBRD12:4

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st b₂ <= len (GoB b₁) & b₃ <= width (GoB b₁) holds
( Cl (Down (Int (cell (GoB b₁),b₂,b₃)),((L~ b₁) ` )) is connected & Down (Int (cell (GoB b₁),b₂,b₃)),((L~ b₁) ` ) = Int (cell (GoB b₁),b₂,b₃) )

proof end;

Lemma6: for b₁ being non constant standard special_circular_sequence holds
( Cl (Down (LeftComp b₁),((L~ b₁) ` )) is connected & Down (LeftComp b₁),((L~ b₁) ` ) = LeftComp b₁ & Down (LeftComp b₁),((L~ b₁) ` ) is_a_component_of (TOP-REAL 2) | ((L~ b₁) ` ) )

proof end;

Lemma7: for b₁ being non constant standard special_circular_sequence holds
( Cl (Down (RightComp b₁),((L~ b₁) ` )) is connected & Down (RightComp b₁),((L~ b₁) ` ) = RightComp b₁ & Down (RightComp b₁),((L~ b₁) ` ) is_a_component_of (TOP-REAL 2) | ((L~ b₁) ` ) )

proof end;

theorem Th5: :: GOBRD12:5

for b₁ being non constant standard special_circular_sequence holds (L~ b₁) ` = union { (Cl (Down (Int (cell (GoB b₁),b₂,b₃)),((L~ b₁) ` ))) where B is Nat, B is Nat : ( b₂ <= len (GoB b₁) & b₃ <= width (GoB b₁) ) }

proof end;

theorem Th6: :: GOBRD12:6

for b₁ being non constant standard special_circular_sequence holds
( (Down (LeftComp b₁),((L~ b₁) ` )) \/ (Down (RightComp b₁),((L~ b₁) ` )) is a_union_of_components of (TOP-REAL 2) | ((L~ b₁) ` ) & Down (LeftComp b₁),((L~ b₁) ` ) = LeftComp b₁ & Down (RightComp b₁),((L~ b₁) ` ) = RightComp b₁ )

proof end;

Lemma10: for b₁ being non constant standard special_circular_sequence
for b₂, b₃, b₄, b₅ being Nat st b₂ <= len (GoB b₁) & b₃ <= width (GoB b₁) & b₄ <= len (GoB b₁) & b₅ <= width (GoB b₁) & ( b₄ = b₂ + 1 or b₂ = b₄ + 1 ) & b₃ = b₅ & Int (cell (GoB b₁),b₂,b₃) c= (LeftComp b₁) \/ (RightComp b₁) holds
Int (cell (GoB b₁),b₄,b₅) c= (LeftComp b₁) \/ (RightComp b₁)

proof end;

Lemma11: for b₁ being non constant standard special_circular_sequence
for b₂, b₃, b₄, b₅ being Nat st b₂ <= len (GoB b₁) & b₃ <= width (GoB b₁) & b₄ <= len (GoB b₁) & b₅ <= width (GoB b₁) & ( b₅ = b₃ + 1 or b₃ = b₅ + 1 ) & b₂ = b₄ & Int (cell (GoB b₁),b₂,b₃) c= (LeftComp b₁) \/ (RightComp b₁) holds
Int (cell (GoB b₁),b₄,b₅) c= (LeftComp b₁) \/ (RightComp b₁)

proof end;

theorem Th7: :: GOBRD12:7

for b₁ being non constant standard special_circular_sequence
for b₂, b₃, b₄, b₅ being Nat st b₂ <= len (GoB b₁) & b₃ <= width (GoB b₁) & b₄ <= len (GoB b₁) & b₅ <= width (GoB b₁) & b₂,b₃,b₄,b₅ are_adjacent2 holds
( Int (cell (GoB b₁),b₂,b₃) c= (LeftComp b₁) \/ (RightComp b₁) iff Int (cell (GoB b₁),b₄,b₅) c= (LeftComp b₁) \/ (RightComp b₁) )

proof end;

theorem Th8: :: GOBRD12:8

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being FinSequence of NAT st len b₂ = len b₃ & ex b₄ being Nat st
( b₄ in dom b₂ & Int (cell (GoB b₁),(b₂ /. b₄),(b₃ /. b₄)) c= (LeftComp b₁) \/ (RightComp b₁) ) & ( for b₄ being Nat st 1 <= b₄ & b₄ < len b₂ holds
b₂ /. b₄,b₃ /. b₄,b₂ /. (b₄ + 1),b₃ /. (b₄ + 1) are_adjacent2 ) & ( for b₄, b₅, b₆ being Nat st b₄ in dom b₂ & b₅ = b₂ . b₄ & b₆ = b₃ . b₄ holds
( b₅ <= len (GoB b₁) & b₆ <= width (GoB b₁) ) ) holds
for b₄ being Nat st b₄ in dom b₂ holds
Int (cell (GoB b₁),(b₂ /. b₄),(b₃ /. b₄)) c= (LeftComp b₁) \/ (RightComp b₁)

proof end;

theorem Th9: :: GOBRD12:9

for b₁ being non constant standard special_circular_sequence ex b₂, b₃ being Nat st
( b₂ <= len (GoB b₁) & b₃ <= width (GoB b₁) & Int (cell (GoB b₁),b₂,b₃) c= (LeftComp b₁) \/ (RightComp b₁) )

proof end;

theorem Th10: :: GOBRD12:10

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st b₂ <= len (GoB b₁) & b₃ <= width (GoB b₁) holds
Int (cell (GoB b₁),b₂,b₃) c= (LeftComp b₁) \/ (RightComp b₁)

proof end;

theorem Th11: :: GOBRD12:11

proof end;