:: Reconstructions of Special Sequences :: by Yatsuka Nakamura and Roman Matuszewski :: :: Received December 10, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, REAL_1, SUBSET_1, XBOOLE_0, FINSEQ_1, ARYTM_3, XXREAL_0, ORDINAL4, FUNCT_1, ARYTM_1, RELAT_1, PARTFUN1, FINSEQ_5, RFINSEQ, CARD_1, TARSKI, EUCLID, TOPREAL1, RLTOPSP1, PRE_TOPC, MCART_1, SPPOL_2, GROUP_2, SUPINF_2, STRUCT_0, JORDAN3; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, RFINSEQ, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_5, SEQ_4, FINSEQ_6, STRUCT_0, TOPREAL1, PRE_TOPC, RLVECT_1, RLTOPSP1, EUCLID, SPPOL_2; constructors REAL_1, SEQ_4, RFINSEQ, NAT_D, FINSEQ_5, TOPREAL1, BINOP_2, RELSET_1, FINSEQ_6; registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_5, STRUCT_0, EUCLID, SPPOL_2, XXREAL_2, CARD_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve r1,r2 for Real; reserve n,i,i1,i2,j for Nat; reserve D for non empty set; reserve f for FinSequence of D; theorem :: JORDAN3:1 for f being FinSequence of TOP-REAL n st 2<=len f holds f.1 in L~f & f /.1 in L~f & f.len f in L~f & f/.len f in L~f; theorem :: JORDAN3:2 for p1,p2,q1,q2 being Point of TOP-REAL 2 st (p1`1 = p2`1 or p1 `2 = p2`2)& q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2) holds q1`1 = q2`1 or q1`2 = q2`2; theorem :: JORDAN3:3 for p1,p2,q1,q2 being Point of TOP-REAL 2 st (p1`1 = p2`1 or p1 `2 = p2`2)& LSeg(q1,q2) c= LSeg(p1,p2) holds q1`1 = q2`1 or q1`2 = q2`2; theorem :: JORDAN3:4 for f being FinSequence of TOP-REAL 2,n being Element of NAT st 2<=n & f is being_S-Seq holds f|n is being_S-Seq; theorem :: JORDAN3:5 for f being FinSequence of TOP-REAL 2,n being Element of NAT st n<=len f & 2<=len f-'n & f is being_S-Seq holds f/^n is being_S-Seq; theorem :: JORDAN3:6 for f being FinSequence of TOP-REAL 2,k1,k2 being Element of NAT st f is being_S-Seq & 1<=k1 & k1<=len f & 1<=k2 & k2<=len f & k1<>k2 holds mid(f,k1, k2) is being_S-Seq; begin ::---------------------------------------------------------: :: A Concept of Index for Finite Sequences in TOP-REAL 2 : ::---------------------------------------------------------: definition let f be FinSequence of TOP-REAL 2,p be Point of TOP-REAL 2; assume p in L~f; func Index(p,f) -> Element of NAT means :: JORDAN3:def 1 ex S being non empty Subset of NAT st it = min S & S = { i: p in LSeg(f,i) }; end; theorem :: JORDAN3:7 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2, i being Element of NAT st p in LSeg(f,i) holds Index(p,f) <= i; theorem :: JORDAN3:8 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in L~f holds 1<=Index(p,f) & Index(p,f) < len f; theorem :: JORDAN3:9 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in L~f holds p in LSeg(f,Index(p,f)); theorem :: JORDAN3:10 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in LSeg(f,1) holds Index(p,f) = 1; theorem :: JORDAN3:11 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st len f >= 2 holds Index(f/.1,f) = 1; theorem :: JORDAN3:12 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2,i1 being Nat st f is being_S-Seq & 1 f.i1 holds i1=Index(p,f); definition let g be FinSequence of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2; pred g is_S-Seq_joining p1,p2 means :: JORDAN3:def 2 g is being_S-Seq & g.1 = p1 & g. len g = p2; end; theorem :: JORDAN3:15 for g being FinSequence of TOP-REAL 2, p1,p2 being Point of TOP-REAL 2 st g is_S-Seq_joining p1,p2 holds Rev g is_S-Seq_joining p2,p1; theorem :: JORDAN3:16 for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2,j be Nat st p in L~f & g=<*p*>^mid(f,Index(p,f)+1,len f) & 1<=j & j+ 1<=len g holds LSeg(g,j) c= LSeg(f,Index(p,f)+j-'1); theorem :: JORDAN3:17 for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f is being_S-Seq & p in L~f & p<>f.(Index(p,f)+1) & g=<*p*>^mid(f,Index(p,f) +1,len f) holds g is_S-Seq_joining p,f/.len f; theorem :: JORDAN3:18 for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2,j be Nat st p in L~f & 1<=j & j+1<=len g & g=mid(f,1,Index(p,f))^<*p *> holds LSeg(g,j) c= LSeg(f,j); theorem :: JORDAN3:19 for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f is being_S-Seq & p in L~f & p<>f.1 & g=mid(f,1,Index(p,f))^<*p *> holds g is_S-Seq_joining f/.1,p; begin ::----------------------------------------------------------------------: :: Left and Right Cutting Functions for Finite Sequences in TOP-REAL 2 : ::----------------------------------------------------------------------: definition let f be FinSequence of TOP-REAL 2,p be Point of TOP-REAL 2; func L_Cut(f,p) -> FinSequence of TOP-REAL 2 equals :: JORDAN3:def 3 <*p*>^mid(f,Index (p,f)+1,len f) if p<>f.(Index(p,f)+1) otherwise mid(f,Index(p,f)+1,len f); func R_Cut(f,p) -> FinSequence of TOP-REAL 2 equals :: JORDAN3:def 4 mid(f,1,Index(p,f ))^<*p*> if p<>f.1 otherwise <*p*>; end; theorem :: JORDAN3:20 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f is being_S-Seq & p in L~f & p = f.(Index(p,f)+1) & p <> f.len f holds Index(p,Rev f) + Index(p,f) + 1 = len f; theorem :: JORDAN3:21 for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st f is unfolded s.n.c. & p in L~f & p <> f.(Index(p,f)+1) holds Index(p,Rev f) + Index(p,f) = len f; theorem :: JORDAN3:22 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f is being_S-Seq & p in L~f holds L_Cut(Rev f,p) = Rev R_Cut(f,p); theorem :: JORDAN3:23 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in L~f holds (L_Cut(f,p)).1=p & for i st 1 f.(Index( p,f)+1) implies (L_Cut(f,p)).i=f.(Index(p,f)+i-1)); theorem :: JORDAN3:24 for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st p in L~f holds R_Cut(f,p).(len R_Cut(f,p)) = p & for i be Element of NAT st 1<=i & i<=Index(p,f) holds R_Cut(f,p).i = f.i; theorem :: JORDAN3:25 for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st p in L~f holds ( p<>f.1 implies len R_Cut(f,p)=Index(p,f)+1 ) & ( p=f.1 implies len R_Cut(f,p)=Index(p,f) ); theorem :: JORDAN3:26 for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st p in L~f holds ( p=f.(Index(p,f)+1) implies len L_Cut(f,p) = len f-Index(p,f ) ) & ( p<>f.(Index(p,f)+1) implies len L_Cut(f,p) = len f-Index(p,f)+1 ); definition let p1,p2,q1,q2 be Point of TOP-REAL 2; pred LE q1,q2,p1,p2 means :: JORDAN3:def 5 q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2) & for r1,r2 being Real st 0<=r1 & r1<=1 & q1=(1-r1)*p1+r1*p2 & 0<=r2 & r2<=1 & q2=(1- r2)*p1+r2*p2 holds r1<=r2; end; definition let p1,p2,q1,q2 be Point of TOP-REAL 2; pred LT q1,q2,p1,p2 means :: JORDAN3:def 6 LE q1,q2,p1,p2 & q1<>q2; end; theorem :: JORDAN3:27 for p1,p2,q1,q2 being Point of TOP-REAL 2 st LE q1,q2,p1,p2 & LE q2,q1 ,p1,p2 holds q1=q2; theorem :: JORDAN3:28 for p1,p2,q1,q2 being Point of TOP-REAL 2 st q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2) & p1<>p2 holds (LE q1,q2,p1,p2 or LT q2,q1,p1,p2) & not(LE q1 ,q2,p1,p2 & LT q2,q1,p1,p2); theorem :: JORDAN3:29 for f be FinSequence of TOP-REAL 2 for p,q be Point of TOP-REAL 2 st p in L~f & q in L~f & Index(p,f)q & Index(p,f) = Index(q,f) & LE p,q,f/.(Index(p, f)),f/.(Index(p,f)+1) holds q in L~L_Cut(f,p); begin ::--------------------------------------------------------: :: Cutting Both Sides of a Finite Sequence and : :: a Discussion of Speciality of Sequences in TOP-REAL 2 : ::--------------------------------------------------------: definition let f be FinSequence of TOP-REAL 2,p,q be Point of TOP-REAL 2; func B_Cut(f,p,q) -> FinSequence of TOP-REAL 2 equals :: JORDAN3:def 7 R_Cut(L_Cut(f,p ),q) if p in L~f & q in L~f & Index(p,f)f.1 holds R_Cut(f,p) is_S-Seq_joining f/. 1,p; theorem :: JORDAN3:33 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f is being_S-Seq & p in L~f & p<>f.len f holds L_Cut(f,p) is_S-Seq_joining p,f/.len f; theorem :: JORDAN3:34 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f is being_S-Seq & p in L~f & p<>f.len f holds L_Cut(f,p) is being_S-Seq ; theorem :: JORDAN3:35 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f is being_S-Seq & p in L~f & p<>f.1 holds R_Cut(f,p) is being_S-Seq; theorem :: JORDAN3:36 for f being FinSequence of TOP-REAL 2, p,q being Point of TOP-REAL 2 st f is being_S-Seq & p in L~f & q in L~f & p<>q holds B_Cut(f,p,q) is_S-Seq_joining p,q; theorem :: JORDAN3:37 for f being FinSequence of TOP-REAL 2, p,q being Point of TOP-REAL 2 st f is being_S-Seq & p in L~f & q in L~f & p<>q holds B_Cut(f,p,q) is being_S-Seq; theorem :: JORDAN3:38 for f,g being FinSequence of TOP-REAL 2 st f.len f=g.1 & f is being_S-Seq & g is being_S-Seq & L~f /\ L~g={g.1} holds f^mid(g,2,len g) is being_S-Seq; theorem :: JORDAN3:39 for f,g being FinSequence of TOP-REAL 2 st f.len f=g.1 & f is being_S-Seq & g is being_S-Seq & L~f /\ L~g={g.1} holds f^mid(g,2,len g) is_S-Seq_joining f/.1,g/.len g; theorem :: JORDAN3:40 for f being FinSequence of TOP-REAL 2, n being Element of NAT holds L~ (f/^n) c= L~f; theorem :: JORDAN3:41 for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st p in L~f holds L~R_Cut(f,p) c= L~f; theorem :: JORDAN3:42 for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st p in L~f holds L~L_Cut(f,p) c= L~f; theorem :: JORDAN3:43 for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f.len f=g.1 & p in L~f & f is being_S-Seq & g is being_S-Seq & L~ f /\ L~g={g.1} & p<>f.len f holds L_Cut(f,p)^mid(g,2,len g) is_S-Seq_joining p, g/.len g; theorem :: JORDAN3:44 for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f.len f=g.1 & p in L~f & f is being_S-Seq & g is being_S-Seq & L~f /\ L~g={g .1} & p<>f.len f holds L_Cut(f,p)^mid(g,2,len g) is being_S-Seq; theorem :: JORDAN3:45 for f,g being FinSequence of TOP-REAL 2 st f.len f=g.1 & f is being_S-Seq & g is being_S-Seq & L~f /\ L~g={g.1} holds mid(f,1,len f-'1)^g is being_S-Seq; theorem :: JORDAN3:46 for f,g being FinSequence of TOP-REAL 2 st f.len f=g.1 & f is being_S-Seq & g is being_S-Seq & L~f /\ L~g={g.1} holds mid(f,1,len f-'1)^g is_S-Seq_joining f/.1,g/.len g; theorem :: JORDAN3:47 for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f.len f=g.1 & p in L~g & f is being_S-Seq & g is being_S-Seq & L~ f /\ L~g={g.1} & p<>g.1 holds mid(f,1,len f -'1)^R_Cut(g,p) is_S-Seq_joining f /.1,p; theorem :: JORDAN3:48 for f,g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f.len f=g.1 & p in L~g & f is being_S-Seq & g is being_S-Seq & L~f /\ L~g={g .1} & p<>g.1 holds mid(f,1,len f -'1)^R_Cut(g,p) is being_S-Seq;