:: GOBRD12 semantic presentation

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

proof end;

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

theorem :: GOBRD12:1

canceled;

theorem Th2: :: GOBRD12:2

for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
Int (cell (GoB f),i,j) c= (L~ f) `

proof end;

theorem Th3: :: GOBRD12:3

for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
Cl (Down (Int (cell (GoB f),i,j)),((L~ f) ` )) = (cell (GoB f),i,j) /\ ((L~ f) ` )

proof end;

theorem Th4: :: GOBRD12:4

for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
( Cl (Down (Int (cell (GoB f),i,j)),((L~ f) ` )) is connected & Down (Int (cell (GoB f),i,j)),((L~ f) ` ) = Int (cell (GoB f),i,j) )

proof end;

proof end;

proof end;

theorem Th5: :: GOBRD12:5

for f being non constant standard special_circular_sequence holds (L~ f) ` = union { (Cl (Down (Int (cell (GoB f),i,j)),((L~ f) ` ))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }

proof end;

theorem Th6: :: GOBRD12:6

proof end;

Lm5: for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Nat st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 & Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) holds
Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f)

proof end;

Lm6: for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Nat st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( j2 = j1 + 1 or j1 = j2 + 1 ) & i1 = i2 & Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) holds
Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f)

proof end;

theorem Th7: :: GOBRD12:7

for f being non constant standard special_circular_sequence
for i1, j1, i2, j2 being Nat st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent2 holds
( Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) )

proof end;

theorem Th8: :: GOBRD12:8

for f being non constant standard special_circular_sequence
for F1, F2 being FinSequence of NAT st len F1 = len F2 & ex i being Nat st
( i in dom F1 & Int (cell (GoB f),(F1 /. i),(F2 /. i)) c= (LeftComp f) \/ (RightComp f) ) & ( for i being Nat st 1 <= i & i < len F1 holds
F1 /. i,F2 /. i,F1 /. (i + 1),F2 /. (i + 1) are_adjacent2 ) & ( for i, k1, k2 being Nat st i in dom F1 & k1 = F1 . i & k2 = F2 . i holds
( k1 <= len (GoB f) & k2 <= width (GoB f) ) ) holds
for i being Nat st i in dom F1 holds
Int (cell (GoB f),(F1 /. i),(F2 /. i)) c= (LeftComp f) \/ (RightComp f)

proof end;

theorem Th9: :: GOBRD12:9

proof end;

theorem Th10: :: GOBRD12:10

for f being non constant standard special_circular_sequence
for i, j being Nat st i <= len (GoB f) & j <= width (GoB f) holds
Int (cell (GoB f),i,j) c= (LeftComp f) \/ (RightComp f)

proof end;

theorem :: GOBRD12:11

proof end;