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

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: GOBRD12:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

Lm3: for f being non constant standard special_circular_sequence holds
( Cl (Down (LeftComp f),((L~ f) ` )) is connected & Down (LeftComp f),((L~ f) ` ) = LeftComp f & Down (LeftComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) )
proof end;

Lm4: for f being non constant standard special_circular_sequence holds
( Cl (Down (RightComp f),((L~ f) ` )) is connected & Down (RightComp f),((L~ f) ` ) = RightComp f & Down (RightComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) )
proof end;

theorem Th5: :: GOBRD12:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence holds
( (Down (LeftComp f),((L~ f) ` )) \/ (Down (RightComp f),((L~ f) ` )) is a_union_of_components of (TOP-REAL 2) | ((L~ f) ` ) & Down (LeftComp f),((L~ f) ` ) = LeftComp f & Down (RightComp f),((L~ f) ` ) = RightComp f )
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence ex i, j being Nat st
( i <= len (GoB f) & j <= width (GoB f) & Int (cell (GoB f),i,j) c= (LeftComp f) \/ (RightComp f) )
proof end;

theorem Th10: :: GOBRD12:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence holds (L~ f) ` = (LeftComp f) \/ (RightComp f)
proof end;