:: Some properties of special polygonal curves
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 22, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

theorem :: SPRECT_3:1
for D being non empty set
for f being non empty FinSequence of D
for g being FinSequence of D holds (g ^ f) /. (len (g ^ f)) = f /. (len f)
proofend;

theorem Th2: :: SPRECT_3:2
for a, b, c, d being set holds Indices ((a,b) ][ (c,d)) = {[1,1],[1,2],[2,1],[2,2]}
proofend;

begin

theorem Th3: :: SPRECT_3:3
for n being Element of NAT
for p, q being Point of (TOP-REAL n)
for r being Real st 0 < r &amp; p = ((1 - r) * p) + (r * q) holds
p = q
proofend;

theorem Th4: :: SPRECT_3:4
for n being Element of NAT
for p, q being Point of (TOP-REAL n)
for r being Real st r < 1 &amp; p = ((1 - r) * q) + (r * p) holds
p = q
proofend;

theorem :: SPRECT_3:5
for n being Element of NAT
for p, q being Point of (TOP-REAL n) st p = (1 / 2) * (p + q) holds
p = q
proofend;

theorem Th6: :: SPRECT_3:6
for n being Element of NAT
for p, q, r being Point of (TOP-REAL n) st q in LSeg (p,r) &amp; r in LSeg (p,q) holds
q = r
proofend;

begin

theorem Th7: :: SPRECT_3:7
for A being non empty Subset of (TOP-REAL 2)
for p being Element of (Euclid 2)
for r being Real st A = Ball (p,r) holds
A is connected
proofend;

theorem Th8: :: SPRECT_3:8
for A, B being Subset of (TOP-REAL 2) st A is open &amp; B is_a_component_of A holds
B is open
proofend;

theorem :: SPRECT_3:9
for p, q, r, s being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal &amp; LSeg (r,s) is horizontal &amp; LSeg (p,q) meets LSeg (r,s) holds
p `2 = r `2
proofend;

theorem :: SPRECT_3:10
for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is vertical &amp; LSeg (q,r) is horizontal holds
(LSeg (p,q)) /\ (LSeg (q,r)) = {q}
proofend;

theorem :: SPRECT_3:11
for p, q, r, s being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal &amp; LSeg (s,r) is vertical &amp; r in LSeg (p,q) holds
(LSeg (p,q)) /\ (LSeg (s,r)) = {r}
proofend;

begin

theorem :: SPRECT_3:12
for j, k, i being Element of NAT
for G being Go-board st 1 <= j &amp; j <= k &amp; k <= width G &amp; 1 <= i &amp; i <= len G holds
(G * (i,j)) `2 <= (G * (i,k)) `2
proofend;

theorem :: SPRECT_3:13
for j, i, k being Element of NAT
for G being Go-board st 1 <= j &amp; j <= width G &amp; 1 <= i &amp; i <= k &amp; k <= len G holds
(G * (i,j)) `1 <= (G * (k,j)) `1
proofend;

theorem Th14: :: SPRECT_3:14
for C being Subset of (TOP-REAL 2) holds LSeg ((NW-corner C),(NE-corner C)) c= L~ (SpStSeq C)
proofend;

theorem Th15: :: SPRECT_3:15
for C being non empty compact Subset of (TOP-REAL 2) holds N-min C in LSeg ((NW-corner C),(NE-corner C))
proofend;

registration
let C be Subset of (TOP-REAL 2);
cluster LSeg ((NW-corner C),(NE-corner C)) ->  horizontal ;
coherence
 LSeg ((NW-corner C),(NE-corner C)) is horizontal
proofend;
end;

theorem :: SPRECT_3:16
for g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st g /. 1 <> p &amp; ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) &amp; g is being_S-Seq &amp; (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} holds
<*p*> ^ g is being_S-Seq
proofend;

theorem :: SPRECT_3:17
for j being Element of NAT
for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2) st 1 < j &amp; j <= len f &amp; p in L~ (mid (f,1,j)) holds
LE p,f /. j, L~ f,f /. 1,f /. (len f)
proofend;

theorem :: SPRECT_3:18
for i, j being Element of NAT
for h being FinSequence of (TOP-REAL 2) st i in dom h &amp; j in dom h holds
L~ (mid (h,i,j)) c= L~ h
proofend;

theorem :: SPRECT_3:19
for i, j being Element of NAT st 1 <= i &amp; i < j holds
for f being FinSequence of (TOP-REAL 2) st j <= len f holds
L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j)))
proofend;

theorem :: SPRECT_3:20
for i, j being Element of NAT
for f being FinSequence of (TOP-REAL 2) st 1 <= i &amp; i < j &amp; j <= len f holds
L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1)))
proofend;

theorem :: SPRECT_3:21
for f, g being FinSequence of (TOP-REAL 2) st f is being_S-Seq &amp; g is being_S-Seq &amp; ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) &amp; L~ f misses L~ g &amp; (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ f) = {(f /. (len f))} &amp; (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ g) = {(g /. 1)} holds
f ^ g is being_S-Seq
proofend;

theorem :: SPRECT_3:22
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
(R_Cut (f,p)) /. 1 = f /. 1
proofend;

theorem :: SPRECT_3:23
for j being Element of NAT
for f being S-Sequence_in_R2
for p, q being Point of (TOP-REAL 2) st 1 <= j &amp; j < len f &amp; p in LSeg (f,j) &amp; q in LSeg ((f /. j),p) holds
LE q,p, L~ f,f /. 1,f /. (len f)
proofend;

begin

theorem Th24: :: SPRECT_3:24
for f being non constant standard special_circular_sequence holds
( LeftComp f is open &amp; RightComp f is open )
proofend;

registration
let f be non constant standard special_circular_sequence;
cluster L~ f ->  non horizontal non vertical ;
coherence
 ( not L~ f is vertical &amp; not L~ f is horizontal )
proofend;
cluster LeftComp f ->  being_Region ;
coherence
 LeftComp f is being_Region
proofend;
cluster RightComp f ->  being_Region ;
coherence
 RightComp f is being_Region
proofend;
end;

theorem Th25: :: SPRECT_3:25
for f being non constant standard special_circular_sequence holds RightComp f misses L~ f
proofend;

theorem Th26: :: SPRECT_3:26
for f being non constant standard special_circular_sequence holds LeftComp f misses L~ f
proofend;

theorem Th27: :: SPRECT_3:27
for f being non constant standard special_circular_sequence holds i_w_n f < i_e_n f
proofend;

theorem Th28: :: SPRECT_3:28
for f being non constant standard special_circular_sequence ex i being Element of NAT st
( 1 <= i &amp; i < len (GoB f) &amp; N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )
proofend;

theorem Th29: :: SPRECT_3:29
for i being Element of NAT
for f being non constant standard clockwise_oriented special_circular_sequence st i in dom (GoB f) &amp; f /. 1 = (GoB f) * (i,(width (GoB f))) &amp; f /. 1 = N-min (L~ f) holds
( f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) &amp; f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) )
proofend;

theorem :: SPRECT_3:30
for i, j being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= i &amp; i < j &amp; j <= len f &amp; f /. 1 in L~ (mid (f,i,j)) &amp; not i = 1 holds
j = len f
proofend;

theorem :: SPRECT_3:31
for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f))
proofend;

begin

theorem Th32: :: SPRECT_3:32
for f being rectangular FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) holds
( not p in L~ f or p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )
proofend;

registration
cluster non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like V236( the U1 of (TOP-REAL 2)) special unfolded s.c.c. rectangular for FinSequence of the U1 of (TOP-REAL 2);
existence
 ex b1 being special_circular_sequence st b1 is rectangular
proofend;
end;

theorem Th33: :: SPRECT_3:33
for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f &amp; g /. (len g) in RightComp f holds
L~ f meets L~ g
proofend;

theorem Th34: :: SPRECT_3:34
for f being rectangular special_circular_sequence holds SpStSeq (L~ f) = f
proofend;

theorem Th35: :: SPRECT_3:35
for f being rectangular special_circular_sequence holds L~ f =  {  p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) &amp; p `2 <= N-bound (L~ f) &amp; p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) &amp; p `1 >= W-bound (L~ f) &amp; p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) &amp; p `1 >= W-bound (L~ f) &amp; p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) &amp; p `2 <= N-bound (L~ f) &amp; p `2 >= S-bound (L~ f) ) )  }
proofend;

theorem Th36: :: SPRECT_3:36
for f being rectangular special_circular_sequence holds GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))
proofend;

theorem Th37: :: SPRECT_3:37
for f being rectangular special_circular_sequence holds
( LeftComp f =  {  p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) )  }  &amp; RightComp f =  {  q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 &amp; q `1 < E-bound (L~ f) &amp; S-bound (L~ f) < q `2 &amp; q `2 < N-bound (L~ f) )  }  )
proofend;

registration
cluster non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V236( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard rectangular clockwise_oriented for FinSequence of the U1 of (TOP-REAL 2);
existence
 ex b1 being rectangular special_circular_sequence st b1 is clockwise_oriented
proofend;
end;

registration
cluster non empty V236( the U1 of (TOP-REAL 2)) special unfolded s.c.c. rectangular  ->  rectangular clockwise_oriented for FinSequence of the U1 of (TOP-REAL 2);
coherence
 for b1 being rectangular special_circular_sequence holds b1 is clockwise_oriented
proofend;
end;

theorem :: SPRECT_3:38
for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f &amp; g /. (len g) in RightComp f holds
Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f)
proofend;

theorem :: SPRECT_3:39
for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f &amp; g /. (len g) in RightComp f holds
Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> SE-corner (L~ f)
proofend;

theorem Th40: :: SPRECT_3:40
for f being rectangular special_circular_sequence
for p being Point of (TOP-REAL 2) st ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) holds
p in LeftComp f
proofend;

theorem :: SPRECT_3:41
for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp (SpStSeq (L~ f)) c= LeftComp f
proofend;

begin

theorem Th42: :: SPRECT_3:42
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) holds
( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f &amp; <*q*> is_in_the_area_of f ) )
proofend;

theorem Th43: :: SPRECT_3:43
for f being rectangular FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st <*p*> is_in_the_area_of f &amp; ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) holds
p in L~ f
proofend;

theorem Th44: :: SPRECT_3:44
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2)
for r being Real st 0 <= r &amp; r <= 1 &amp; <*p,q*> is_in_the_area_of f holds
<*(((1 - r) * p) + (r * q))*> is_in_the_area_of f
proofend;

theorem Th45: :: SPRECT_3:45
for i being Element of NAT
for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f &amp; i in dom g holds
<*(g /. i)*> is_in_the_area_of f
proofend;

theorem Th46: :: SPRECT_3:46
for f, g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st g is_in_the_area_of f &amp; p in L~ g holds
<*p*> is_in_the_area_of f
proofend;

theorem Th47: :: SPRECT_3:47
for f being rectangular FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st not q in L~ f &amp; <*p,q*> is_in_the_area_of f holds
(LSeg (p,q)) /\ (L~ f) c= {p}
proofend;

theorem :: SPRECT_3:48
for f being rectangular FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f &amp; not q in L~ f &amp; <*q*> is_in_the_area_of f holds
(LSeg (p,q)) /\ (L~ f) = {p}
proofend;

theorem Th49: :: SPRECT_3:49
for i, j being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= i &amp; i <= len (GoB f) &amp; 1 <= j &amp; j <= width (GoB f) holds
<*((GoB f) * (i,j))*> is_in_the_area_of f
proofend;

theorem :: SPRECT_3:50
for g being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st <*p,q*> is_in_the_area_of g holds
<*((1 / 2) * (p + q))*> is_in_the_area_of g
proofend;

theorem :: SPRECT_3:51
for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f holds
Rev g is_in_the_area_of f
proofend;

theorem :: SPRECT_3:52
for f, g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st g is_in_the_area_of f &amp; <*p*> is_in_the_area_of f &amp; g is being_S-Seq &amp; p in L~ g holds
R_Cut (g,p) is_in_the_area_of f
proofend;

theorem :: SPRECT_3:53
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2) holds
( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) )
proofend;

theorem :: SPRECT_3:54
for f being rectangular special_circular_sequence
for g being S-Sequence_in_R2 st g /. 1 in LeftComp f &amp; g /. (len g) in RightComp f holds
L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f
proofend;

theorem :: SPRECT_3:55
for i, j being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= i &amp; i < len (GoB f) &amp; 1 <= j &amp; j < width (GoB f) holds
Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f))
proofend;

theorem :: SPRECT_3:56
for f, g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st g is_in_the_area_of f &amp; <*p*> is_in_the_area_of f &amp; g is being_S-Seq &amp; p in L~ g holds
L_Cut (g,p) is_in_the_area_of f
proofend;