:: SPRECT_3 semantic presentation

theorem Th1: :: SPRECT_3:1

canceled;

theorem Th2: :: SPRECT_3:2

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₂ /\ b₃ = {b₄} & b₄ in b₁ holds
b₁ /\ b₃ = {b₄}

proof end;

Lemma1: for b₁, b₂, b₃, b₄ being Real st b₄ >= 0 & b₄ <= 1 & b₃ = ((1 - b₄) * b₁) + (b₄ * b₂) & b₁ <= b₃ & b₂ < b₃ holds
b₄ = 0
by XREAL_1:181;

Lemma2: for b₁, b₂, b₃, b₄ being Real st b₄ >= 0 & b₄ <= 1 & b₃ = ((1 - b₄) * b₁) + (b₄ * b₂) & b₁ >= b₃ & b₂ > b₃ holds
b₄ = 0
by XREAL_1:182;

theorem Th3: :: SPRECT_3:3

canceled;

theorem Th4: :: SPRECT_3:4

canceled;

theorem Th5: :: SPRECT_3:5

for b₁, b₂, b₃ being Nat st b₁ -' b₂ <= b₃ holds
b₁ <= b₃ + b₂

proof end;

theorem Th6: :: SPRECT_3:6

for b₁, b₂, b₃ being Nat st b₁ <= b₂ + b₃ holds
b₁ -' b₃ <= b₂

proof end;

theorem Th7: :: SPRECT_3:7

for b₁, b₂, b₃ being Nat st b₁ <= b₂ -' b₃ & b₃ <= b₂ holds
b₁ + b₃ <= b₂

proof end;

theorem Th8: :: SPRECT_3:8

for b₁, b₂, b₃ being Nat st b₁ + b₂ <= b₃ holds
b₂ <= b₃ -' b₁

proof end;

theorem Th9: :: SPRECT_3:9

for b₁, b₂, b₃ being Nat st b₁ <= b₂ & b₂ < b₃ holds
b₂ -' b₁ < b₃ -' b₁

proof end;

theorem Th10: :: SPRECT_3:10

for b₁, b₂, b₃ being Nat st b₁ < b₂ & b₃ < b₂ holds
b₁ -' b₃ < b₂ -' b₃

proof end;

theorem Th11: :: SPRECT_3:11

for b₁ being non empty set
for b₂ being non empty FinSequence of b₁
for b₃ being FinSequence of b₁ holds (b₃ ^ b₂) /. (len (b₃ ^ b₂)) = b₂ /. (len b₂)

proof end;

theorem Th12: :: SPRECT_3:12

for b₁, b₂, b₃, b₄ being set holds Indices (b₁,b₂ ][ b₃,b₄) = {[1,1],[1,2],[2,1],[2,2]}

proof end;

theorem Th13: :: SPRECT_3:13

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being Real st 0 < b₄ & b₂ = ((1 - b₄) * b₂) + (b₄ * b₃) holds
b₂ = b₃

proof end;

theorem Th14: :: SPRECT_3:14

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being Real st b₄ < 1 & b₂ = ((1 - b₄) * b₃) + (b₄ * b₂) holds
b₂ = b₃

proof end;

theorem Th15: :: SPRECT_3:15

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st b₂ = (1 / 2) * (b₂ + b₃) holds
b₂ = b₃

proof end;

theorem Th16: :: SPRECT_3:16

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st b₃ in LSeg b₂,b₄ & b₄ in LSeg b₂,b₃ holds
b₃ = b₄

proof end;

theorem Th17: :: SPRECT_3:17

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Element of (Euclid 2)
for b₃ being Real st b₁ = Ball b₂,b₃ holds
b₁ is connected

proof end;

theorem Th18: :: SPRECT_3:18

for b₁, b₂ being Subset of (TOP-REAL 2) st b₁ is open & b₂ is_a_component_of b₁ holds
b₂ is open

proof end;

theorem Th19: :: SPRECT_3:19

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st LSeg b₁,b₂ is horizontal & b₃ in LSeg b₁,b₂ holds
b₁ `2 = b₃ `2

proof end;

theorem Th20: :: SPRECT_3:20

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st LSeg b₁,b₂ is vertical & b₃ in LSeg b₁,b₂ holds
b₁ `1 = b₃ `1

proof end;

theorem Th21: :: SPRECT_3:21

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2) st LSeg b₁,b₂ is horizontal & LSeg b₃,b₄ is horizontal & LSeg b₁,b₂ meets LSeg b₃,b₄ holds
b₁ `2 = b₃ `2

proof end;

theorem Th22: :: SPRECT_3:22

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st LSeg b₁,b₂ is vertical & LSeg b₂,b₃ is horizontal holds
(LSeg b₁,b₂) /\ (LSeg b₂,b₃) = {b₂}

proof end;

theorem Th23: :: SPRECT_3:23

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2) st LSeg b₁,b₂ is horizontal & LSeg b₄,b₃ is vertical & b₃ in LSeg b₁,b₂ holds
(LSeg b₁,b₂) /\ (LSeg b₄,b₃) = {b₃}

proof end;

theorem Th24: :: SPRECT_3:24

for b₁, b₂, b₃ being Nat
for b₄ being Go-board st 1 <= b₁ & b₁ <= b₂ & b₂ <= width b₄ & 1 <= b₃ & b₃ <= len b₄ holds
(b₄ * b₃,b₁) `2 <= (b₄ * b₃,b₂) `2

proof end;

theorem Th25: :: SPRECT_3:25

for b₁, b₂, b₃ being Nat
for b₄ being Go-board st 1 <= b₁ & b₁ <= width b₄ & 1 <= b₂ & b₂ <= b₃ & b₃ <= len b₄ holds
(b₄ * b₂,b₁) `1 <= (b₄ * b₃,b₁) `1

proof end;

theorem Th26: :: SPRECT_3:26

for b₁ being Subset of (TOP-REAL 2) holds LSeg (NW-corner b₁),(NE-corner b₁) c= L~ (SpStSeq b₁)

proof end;

theorem Th27: :: SPRECT_3:27

for b₁ being Subset of (TOP-REAL 2) holds N-most b₁ c= LSeg (NW-corner b₁),(NE-corner b₁)

proof end;

theorem Th28: :: SPRECT_3:28

for b₁ being non empty compact Subset of (TOP-REAL 2) holds N-min b₁ in LSeg (NW-corner b₁),(NE-corner b₁)

proof end;

theorem Th29: :: SPRECT_3:29

for b₁ being Subset of (TOP-REAL 2) holds LSeg (NW-corner b₁),(NE-corner b₁) is horizontal

proof end;

theorem Th30: :: SPRECT_3:30

canceled;

theorem Th31: :: SPRECT_3:31

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ /. 1 <> b₂ & ( (b₁ /. 1) `1 = b₂ `1 or (b₁ /. 1) `2 = b₂ `2 ) & b₁ is_S-Seq & (LSeg b₂,(b₁ /. 1)) /\ (L~ b₁) = {(b₁ /. 1)} holds
<*b₂*> ^ b₁ is_S-Seq

proof end;

theorem Th32: :: SPRECT_3:32

canceled;

theorem Th33: :: SPRECT_3:33

for b₁ being Nat
for b₂ being S-Sequence_in_R2
for b₃ being Point of (TOP-REAL 2) st 1 < b₁ & b₁ <= len b₂ & b₃ in L~ (mid b₂,1,b₁) holds
LE b₃,b₂ /. b₁, L~ b₂,b₂ /. 1,b₂ /. (len b₂)

proof end;

theorem Th34: :: SPRECT_3:34

for b₁, b₂ being Nat
for b₃ being FinSequence of (TOP-REAL 2) st b₁ in dom b₃ & b₂ in dom b₃ holds
L~ (mid b₃,b₁,b₂) c= L~ b₃

proof end;

theorem Th35: :: SPRECT_3:35

for b₁, b₂ being Nat st 1 <= b₁ & b₁ < b₂ holds
for b₃ being FinSequence of (TOP-REAL 2) st b₂ <= len b₃ holds
L~ (mid b₃,b₁,b₂) = (LSeg b₃,b₁) \/ (L~ (mid b₃,(b₁ + 1),b₂))

proof end;

theorem Th36: :: SPRECT_3:36

for b₁, b₂ being Nat
for b₃ being FinSequence of (TOP-REAL 2) st 1 <= b₁ & b₁ < b₂ & b₂ <= len b₃ holds
L~ (mid b₃,b₁,b₂) = (L~ (mid b₃,b₁,(b₂ -' 1))) \/ (LSeg b₃,(b₂ -' 1))

proof end;

theorem Th37: :: SPRECT_3:37

canceled;

theorem Th38: :: SPRECT_3:38

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is_S-Seq & b₂ is_S-Seq & ( (b₁ /. (len b₁)) `1 = (b₂ /. 1) `1 or (b₁ /. (len b₁)) `2 = (b₂ /. 1) `2 ) & L~ b₁ misses L~ b₂ & (LSeg (b₁ /. (len b₁)),(b₂ /. 1)) /\ (L~ b₁) = {(b₁ /. (len b₁))} & (LSeg (b₁ /. (len b₁)),(b₂ /. 1)) /\ (L~ b₂) = {(b₂ /. 1)} holds
b₁ ^ b₂ is_S-Seq

proof end;

theorem Th39: :: SPRECT_3:39

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ holds
(R_Cut b₁,b₂) /. 1 = b₁ /. 1

proof end;

theorem Th40: :: SPRECT_3:40

for b₁ being Nat
for b₂ being S-Sequence_in_R2
for b₃, b₄ being Point of (TOP-REAL 2) st 1 <= b₁ & b₁ < len b₂ & b₃ in LSeg b₂,b₁ & b₄ in LSeg (b₂ /. b₁),b₃ holds
LE b₄,b₃, L~ b₂,b₂ /. 1,b₂ /. (len b₂)

proof end;

theorem Th41: :: SPRECT_3:41

for b₁ being non constant standard special_circular_sequence holds
( LeftComp b₁ is open & RightComp b₁ is open )

proof end;

registration

let c₁ be non constant standard special_circular_sequence;
cluster L~ a₁ -> non horizontal non vertical ;
coherence

proof end;

cluster LeftComp a₁ -> being_Region ;
coherence

proof end;

cluster RightComp a₁ -> being_Region ;
coherence

proof end;

end;

theorem Th42: :: SPRECT_3:42

for b₁ being non constant standard special_circular_sequence holds RightComp b₁ misses L~ b₁

proof end;

theorem Th43: :: SPRECT_3:43

for b₁ being non constant standard special_circular_sequence holds LeftComp b₁ misses L~ b₁

proof end;

theorem Th44: :: SPRECT_3:44

for b₁ being non constant standard special_circular_sequence holds i_w_n b₁ < i_e_n b₁

proof end;

theorem Th45: :: SPRECT_3:45

for b₁ being non constant standard special_circular_sequence ex b₂ being Nat st
( 1 <= b₂ & b₂ < len (GoB b₁) & N-min (L~ b₁) = (GoB b₁) * b₂,(width (GoB b₁)) )

proof end;

theorem Th46: :: SPRECT_3:46

for b₁ being Nat
for b₂ being clockwise_oriented non constant standard special_circular_sequence st b₁ in dom (GoB b₂) & b₂ /. 1 = (GoB b₂) * b₁,(width (GoB b₂)) & b₂ /. 1 = N-min (L~ b₂) holds
( b₂ /. 2 = (GoB b₂) * (b₁ + 1),(width (GoB b₂)) & b₂ /. ((len b₂) -' 1) = (GoB b₂) * b₁,((width (GoB b₂)) -' 1) )

proof end;

theorem Th47: :: SPRECT_3:47

for b₁, b₂ being Nat
for b₃ being non constant standard special_circular_sequence st 1 <= b₁ & b₁ < b₂ & b₂ <= len b₃ & b₃ /. 1 in L~ (mid b₃,b₁,b₂) & not b₁ = 1 holds
b₂ = len b₃

proof end;

theorem Th48: :: SPRECT_3:48

for b₁ being clockwise_oriented non constant standard special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
LSeg (b₁ /. 1),(b₁ /. 2) c= L~ (SpStSeq (L~ b₁))

proof end;

theorem Th49: :: SPRECT_3:49

for b₁ being rectangular FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) holds
( not b₂ in L~ b₁ or b₂ `1 = W-bound (L~ b₁) or b₂ `1 = E-bound (L~ b₁) or b₂ `2 = S-bound (L~ b₁) or b₂ `2 = N-bound (L~ b₁) )

proof end;

registration

cluster rectangular FinSequence of the carrier of (TOP-REAL 2);
existence

proof end;

end;

theorem Th50: :: SPRECT_3:50

for b₁ being rectangular special_circular_sequence
for b₂ being S-Sequence_in_R2 st b₂ /. 1 in LeftComp b₁ & b₂ /. (len b₂) in RightComp b₁ holds
L~ b₁ meets L~ b₂

proof end;

theorem Th51: :: SPRECT_3:51

for b₁ being rectangular special_circular_sequence holds SpStSeq (L~ b₁) = b₁

proof end;

theorem Th52: :: SPRECT_3:52

for b₁ being rectangular special_circular_sequence holds L~ b₁ = { b₂ where B is Point of (TOP-REAL 2) : ( ( b₂ `1 = W-bound (L~ b₁) & b₂ `2 <= N-bound (L~ b₁) & b₂ `2 >= S-bound (L~ b₁) ) or ( b₂ `1 <= E-bound (L~ b₁) & b₂ `1 >= W-bound (L~ b₁) & b₂ `2 = N-bound (L~ b₁) ) or ( b₂ `1 <= E-bound (L~ b₁) & b₂ `1 >= W-bound (L~ b₁) & b₂ `2 = S-bound (L~ b₁) ) or ( b₂ `1 = E-bound (L~ b₁) & b₂ `2 <= N-bound (L~ b₁) & b₂ `2 >= S-bound (L~ b₁) ) ) }

proof end;

theorem Th53: :: SPRECT_3:53

for b₁ being rectangular special_circular_sequence holds GoB b₁ = (b₁ /. 4),(b₁ /. 1) ][ (b₁ /. 3),(b₁ /. 2)

proof end;

theorem Th54: :: SPRECT_3:54

for b₁ being rectangular special_circular_sequence holds
( LeftComp b₁ = { b₂ where B is Point of (TOP-REAL 2) : ( not W-bound (L~ b₁) <= b₂ `1 or not b₂ `1 <= E-bound (L~ b₁) or not S-bound (L~ b₁) <= b₂ `2 or not b₂ `2 <= N-bound (L~ b₁) ) } & RightComp b₁ = { b₂ where B is Point of (TOP-REAL 2) : ( W-bound (L~ b₁) < b₂ `1 & b₂ `1 < E-bound (L~ b₁) & S-bound (L~ b₁) < b₂ `2 & b₂ `2 < N-bound (L~ b₁) ) } )

proof end;

registration

cluster clockwise_oriented rectangular FinSequence of the carrier of (TOP-REAL 2);
existence

proof end;

end;

registration

cluster rectangular -> clockwise_oriented rectangular FinSequence of the carrier of (TOP-REAL 2);
coherence

proof end;

end;

theorem Th55: :: SPRECT_3:55

for b₁ being rectangular special_circular_sequence
for b₂ being S-Sequence_in_R2 st b₂ /. 1 in LeftComp b₁ & b₂ /. (len b₂) in RightComp b₁ holds
Last_Point (L~ b₂),(b₂ /. 1),(b₂ /. (len b₂)),(L~ b₁) <> NW-corner (L~ b₁)

proof end;

theorem Th56: :: SPRECT_3:56

proof end;

theorem Th57: :: SPRECT_3:57

for b₁ being rectangular special_circular_sequence
for b₂ being Point of (TOP-REAL 2) st ( W-bound (L~ b₁) > b₂ `1 or b₂ `1 > E-bound (L~ b₁) or S-bound (L~ b₁) > b₂ `2 or b₂ `2 > N-bound (L~ b₁) ) holds
b₂ in LeftComp b₁

proof end;

theorem Th58: :: SPRECT_3:58

for b₁ being clockwise_oriented non constant standard special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
LeftComp (SpStSeq (L~ b₁)) c= LeftComp b₁

proof end;

theorem Th59: :: SPRECT_3:59

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) holds
( <*b₂,b₃*> is_in_the_area_of b₁ iff ( <*b₂*> is_in_the_area_of b₁ & <*b₃*> is_in_the_area_of b₁ ) )

proof end;

theorem Th60: :: SPRECT_3:60

for b₁ being rectangular FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st <*b₂*> is_in_the_area_of b₁ & ( b₂ `1 = W-bound (L~ b₁) or b₂ `1 = E-bound (L~ b₁) or b₂ `2 = S-bound (L~ b₁) or b₂ `2 = N-bound (L~ b₁) ) holds
b₂ in L~ b₁

proof end;

theorem Th61: :: SPRECT_3:61

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being Real st 0 <= b₄ & b₄ <= 1 & <*b₂,b₃*> is_in_the_area_of b₁ holds
<*(((1 - b₄) * b₂) + (b₄ * b₃))*> is_in_the_area_of b₁

proof end;

theorem Th62: :: SPRECT_3:62

for b₁ being Nat
for b₂, b₃ being FinSequence of (TOP-REAL 2) st b₃ is_in_the_area_of b₂ & b₁ in dom b₃ holds
<*(b₃ /. b₁)*> is_in_the_area_of b₂

proof end;

theorem Th63: :: SPRECT_3:63

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₂ is_in_the_area_of b₁ & b₃ in L~ b₂ holds
<*b₃*> is_in_the_area_of b₁

proof end;

theorem Th64: :: SPRECT_3:64

for b₁ being rectangular FinSequence of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) st not b₃ in L~ b₁ & <*b₂,b₃*> is_in_the_area_of b₁ holds
(LSeg b₂,b₃) /\ (L~ b₁) c= {b₂}

proof end;

theorem Th65: :: SPRECT_3:65

for b₁ being rectangular FinSequence of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) st b₂ in L~ b₁ & not b₃ in L~ b₁ & <*b₃*> is_in_the_area_of b₁ holds
(LSeg b₂,b₃) /\ (L~ b₁) = {b₂}

proof end;

theorem Th66: :: SPRECT_3:66

for b₁, b₂ being Nat
for b₃ being non constant standard special_circular_sequence st 1 <= b₁ & b₁ <= len (GoB b₃) & 1 <= b₂ & b₂ <= width (GoB b₃) holds
<*((GoB b₃) * b₁,b₂)*> is_in_the_area_of b₃

proof end;

theorem Th67: :: SPRECT_3:67

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) st <*b₂,b₃*> is_in_the_area_of b₁ holds
<*((1 / 2) * (b₂ + b₃))*> is_in_the_area_of b₁

proof end;

theorem Th68: :: SPRECT_3:68

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₂ is_in_the_area_of b₁ holds
Rev b₂ is_in_the_area_of b₁

proof end;

theorem Th69: :: SPRECT_3:69

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₂ is_in_the_area_of b₁ & <*b₃*> is_in_the_area_of b₁ & b₂ is_S-Seq & b₃ in L~ b₂ holds
R_Cut b₂,b₃ is_in_the_area_of b₁

proof end;

theorem Th70: :: SPRECT_3:70

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2) holds
( b₂ is_in_the_area_of b₁ iff b₂ is_in_the_area_of SpStSeq (L~ b₁) )

proof end;

theorem Th71: :: SPRECT_3:71

for b₁ being rectangular special_circular_sequence
for b₂ being S-Sequence_in_R2 st b₂ /. 1 in LeftComp b₁ & b₂ /. (len b₂) in RightComp b₁ holds
L_Cut b₂,(Last_Point (L~ b₂),(b₂ /. 1),(b₂ /. (len b₂)),(L~ b₁)) is_in_the_area_of b₁

proof end;

theorem Th72: :: SPRECT_3:72

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

proof end;

theorem Th73: :: SPRECT_3:73

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₂ is_in_the_area_of b₁ & <*b₃*> is_in_the_area_of b₁ & b₂ is_S-Seq & b₃ in L~ b₂ holds
L_Cut b₂,b₃ is_in_the_area_of b₁

proof end;