Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users

The abstract of the Mizar article:

Subsequences of Standard Special Circular Sequences in $\cal E^2_\rm T$

by
Yatsuka Nakamura,
Roman Matuszewski, and
Adam Grabowski

Received May 12, 1997

MML identifier: JORDAN4
[ Mizar article, MML identifier index ]


environ

 vocabulary ARYTM_1, NAT_1, RELAT_1, ARYTM_3, FINSEQ_1, FINSEQ_6, FUNCT_1,
      FINSEQ_5, RFINSEQ, EUCLID, TOPREAL1, JORDAN3, SEQM_3, GOBOARD5, TARSKI,
      BOOLE, PRE_TOPC, TOPREAL4, TOPREAL2, MCART_1, JORDAN4, FINSEQ_4;
 notation TARSKI, XBOOLE_0, XREAL_0, REAL_1, NAT_1, BINARITH, RELAT_1,
      FINSEQ_1, FUNCT_1, FINSEQ_4, FINSEQ_5, STRUCT_0, TOPREAL1, TOPREAL2,
      TOPREAL4, GOBOARD1, GOBOARD5, PRE_TOPC, EUCLID, FINSEQ_6, RFINSEQ,
      JORDAN3;
 constructors GOBOARD9, BINARITH, TOPREAL4, TOPREAL2, REAL_1, RFINSEQ, JORDAN3,
      FINSEQ_4, MEMBERED;
 clusters STRUCT_0, GOBOARD5, RELSET_1, EUCLID, SPPOL_2, XREAL_0, ARYTM_3,
      MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

reserve i, i1, i2, i3, j, k, n for Nat,
        r, r1, r2, s, s1 for Real;

theorem :: JORDAN4:1
n-'i=0 implies n<=i;

theorem :: JORDAN4:2
i<=j implies j+k-'i=j+k-i;

theorem :: JORDAN4:3
i<=j implies j+k-'i=j-'i+k;

theorem :: JORDAN4:4
i1<>0 & i2=i3*i1 implies i3<=i2;

theorem :: JORDAN4:5
i1<i2 implies i1 div i2=0;

theorem :: JORDAN4:6
0<j & j<i & i<j+j implies i mod j<>0;

theorem :: JORDAN4:7
0<j & j<=i & i<j+j implies i mod j=i-j & i mod j=i-'j;

theorem :: JORDAN4:8
(j+j)mod j=0;

theorem :: JORDAN4:9
0<k & k<=j & k mod j=0 implies k=j;

begin :: Some facts about cutting of finite sequences

reserve D for non empty set,
        f1 for FinSequence of D;

canceled 4;

theorem :: JORDAN4:14
for f1 st f1 is circular & 1<=len f1 holds f1.1=f1.len f1;

theorem :: JORDAN4:15
for f1,i1,i2 st i1<=i2 holds
  (f1|i1)|i2=f1|i1 & (f1|i2)|i1=f1|i1;

theorem :: JORDAN4:16
(<*>D)|i=<*>D;

theorem :: JORDAN4:17
Rev (<*>D)=<*>D;

theorem :: JORDAN4:18
for f1,k st k<len f1 holds
   (f1/^k).len (f1/^k)=f1.len f1 & (f1/^k)/.len (f1/^k)=f1/.len f1;

theorem :: JORDAN4:19
for g being FinSequence of TOP-REAL 2,i
st g is_S-Seq & i+1<len g holds g/^i is_S-Seq;

theorem :: JORDAN4:20
for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1
  holds len mid(f1,i2,i1)=i1-'i2+1;

theorem :: JORDAN4:21
for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1
  holds len mid(f1,i1,i2)=i1-'i2+1;

theorem :: JORDAN4:22
for f1,i1,i2,j st 1<=i1 & i1<=i2 & i2<=len f1
 holds mid(f1,i1,i2).(len mid(f1,i1,i2))=f1.i2;

theorem :: JORDAN4:23
for f1,i1,i2,j st 1<=i1 & i1<=len f1 & 1<=i2 & i2<=len f1
 holds mid(f1,i1,i2).(len mid(f1,i1,i2))=f1.i2;

theorem :: JORDAN4:24
for f1,i1,i2,j st 1<=i2 & i2<=i1 & i1<=len f1 & 1<=j
  & j<=i1-'i2+1 holds mid(f1,i1,i2).j=f1.(i1-'j+1);

theorem :: JORDAN4:25
for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1 & 1<=j & j<=i1-'i2+1
  holds mid(f1,i1,i2).j=mid(f1,i2,i1).(i1-i2+1-j+1)
    & i1-i2+1-j+1=i1-'i2+1-'j+1;

theorem :: JORDAN4:26
for f1,i1,i2 st 1<=i1 & i1<=i2 & i2<=len f1 & 1<=j & j<=i2-'i1+1
  holds mid(f1,i1,i2).j=mid(f1,i2,i1).(i2-i1+1-j+1)
    & i2-i1+1-j+1=i2-'i1+1-'j+1;

theorem :: JORDAN4:27
for f1,k st 1<=k & k<=len f1
  holds mid(f1,k,k)=<*f1/.k*> & len mid(f1,k,k)=1;

theorem :: JORDAN4:28
mid(f1,0,0)=f1|1;

theorem :: JORDAN4:29
for f1,k st len f1<k
  holds mid(f1,k,k)=<*>D;

theorem :: JORDAN4:30
for f1,i1,i2 holds mid(f1,i1,i2)=Rev mid(f1,i2,i1);

theorem :: JORDAN4:31
for f being FinSequence of TOP-REAL 2,i1,i2,i
  st 1<=i1 & i1<i2 & i2<=len f & 1<=i & i<i2-'i1+1
  holds LSeg(mid(f,i1,i2),i)=LSeg(f,i+i1-'1);

theorem :: JORDAN4:32
for f being FinSequence of TOP-REAL 2,i1,i2,i
  st 1<=i1 & i1<i2 & i2<=len f & 1<=i & i<i2-'i1+1
  holds LSeg(mid(f,i2,i1),i)=LSeg(f,i2-'i);

begin :: Dividing of special circular sequences into parts

definition let n be Nat, f be FinSequence;
 func S_Drop(n,f) -> Nat equals
:: JORDAN4:def 1
  (n mod (len f -'1)) if n mod (len f -'1)<>0
   otherwise len f -'1;
end;

theorem :: JORDAN4:33
for f being FinSequence holds S_Drop(len f-'1,f)=len f-'1;

theorem :: JORDAN4:34
for n being Nat, f being FinSequence
 st 1<=n & n<=len f-'1 holds S_Drop(n,f)=n;

theorem :: JORDAN4:35
for n being Nat,f being FinSequence holds
 S_Drop(n,f)=S_Drop(n+(len f-'1),f) &
 S_Drop(n,f)=S_Drop(len f-'1+n,f);

definition let f be non constant standard special_circular_sequence,
  g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
 pred g is_a_part>_of f,i1,i2 means
:: JORDAN4:def 2
  1<=i1 & i1+1<=len f &
  1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
  (for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f));
end;

definition let f be non constant standard special_circular_sequence,
  g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
 pred g is_a_part<_of f,i1,i2 means
:: JORDAN4:def 3
  1<=i1 & i1+1<=len f &
  1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
  (for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop(len f +i1-'i,f));
end;

definition let f be non constant standard special_circular_sequence,
  g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
 pred g is_a_part_of f,i1,i2 means
:: JORDAN4:def 4
  g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2;
end;

theorem :: JORDAN4:36
    for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part_of f,i1,i2 holds
  1<=i1 & i1+1<=len f &
  1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
  ((for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f))or
  (for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop(len f +i1-'i,f)));

theorem :: JORDAN4:37
for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part>_of f,i1,i2 & i1<=i2 holds len g=i2-'i1+1 & g=mid(f,i1,i2);

theorem :: JORDAN4:38
for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part>_of f,i1,i2 & i1>i2 holds len g=len f+i2-'i1
    & g=mid(f,i1,len f-'1)^(f|i2)
    & g=mid(f,i1,len f-'1)^mid(f,1,i2);

theorem :: JORDAN4:39
for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part<_of f,i1,i2 & i1>=i2 holds len g=i1-'i2+1 & g=mid(f,i1,i2);

theorem :: JORDAN4:40
for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part<_of f,i1,i2 & i1<i2 holds len g=len f+i1-'i2
    & g=mid(f,i1,1)^mid(f,len f-'1,i2);

theorem :: JORDAN4:41
for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part>_of f,i1,i2 holds Rev g is_a_part<_of f,i2,i1;

theorem :: JORDAN4:42
for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part<_of f,i1,i2 holds Rev g is_a_part>_of f,i2,i1;

theorem :: JORDAN4:43
for f being non constant standard special_circular_sequence,
  i1,i2 being Nat st 1<=i1 & i1<=i2 & i2<len f
  holds mid(f,i1,i2) is_a_part>_of f,i1,i2;

theorem :: JORDAN4:44
for f being non constant standard special_circular_sequence,
  i1,i2 being Nat st 1<=i1 & i1<=i2 & i2<len f
  holds mid(f,i2,i1) is_a_part<_of f,i2,i1;

theorem :: JORDAN4:45
for f being non constant standard special_circular_sequence,
  i1,i2 being Nat st 1<=i2 & i1>i2 & i1<len f
  holds mid(f,i1,len f-'1)^mid(f,1,i2) is_a_part>_of f,i1,i2;

theorem :: JORDAN4:46
for f being non constant standard special_circular_sequence,
  i1,i2 being Nat st 1<=i1 & i1<i2 & i2<len f
  holds mid(f,i1,1)^mid(f,len f-'1,i2) is_a_part<_of f,i1,i2;

theorem :: JORDAN4:47
for h being FinSequence of TOP-REAL 2,i1,i2 st
1<=i1 & i1<=len h & 1<=i2 & i2<=len h holds L~mid(h,i1,i2) c= L~h;

theorem :: JORDAN4:48
for g being FinSequence of D holds
 g is one-to-one iff for i1,i2 st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g &
 (g.i1=g.i2 or g/.i1=g/.i2) holds i1=i2;

theorem :: JORDAN4:49
for f being non constant standard special_circular_sequence,
 i2 st 1<i2 & i2+1<=len f holds f|i2 is_S-Seq;

theorem :: JORDAN4:50
for f being non constant standard special_circular_sequence,
 i2 st 1<=i2 & i2+1<len f holds f/^i2 is_S-Seq;

theorem :: JORDAN4:51
for f being non constant standard special_circular_sequence,
i1,i2 st 1<=i1 & i1<i2 & i2+1<=len f holds mid(f,i1,i2) is_S-Seq;

theorem :: JORDAN4:52
for f being non constant standard special_circular_sequence,
i1,i2 st 1<i1 & i1<i2 & i2<=len f holds mid(f,i1,i2) is_S-Seq;

theorem :: JORDAN4:53
for p0,p,q1,q2 being Point of TOP-REAL 2 st
 p0 in LSeg(p,q1) & p0 in LSeg(p,q2) & p<>p0 holds
 q1 in LSeg(p,q2) or q2 in LSeg(p,q1);

theorem :: JORDAN4:54
for f being non constant standard special_circular_sequence
holds LSeg(f,1)/\ LSeg(f,len f-'1)={f.1};

theorem :: JORDAN4:55
for f being non constant standard special_circular_sequence,
  i1,i2 being Nat,g1,g2 being FinSequence of TOP-REAL 2
   st 1<=i1 & i1<i2 & i2<len f & g1=mid(f,i1,i2)
   & g2=mid(f,i1,1)^mid(f,len f-'1,i2)
  holds (L~g1)/\(L~g2)={f.i1,f.i2} & (L~g1) \/ (L~g2)=L~f;

theorem :: JORDAN4:56
for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part>_of f,i1,i2 & i1<i2 holds
  L~g is_S-P_arc_joining f/.i1,f/.i2;

theorem :: JORDAN4:57
for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part<_of f,i1,i2 & i1>i2 holds
  L~g is_S-P_arc_joining f/.i1,f/.i2;

theorem :: JORDAN4:58
for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part>_of f,i1,i2 & i1<>i2 holds
  L~g is_S-P_arc_joining f/.i1,f/.i2;

theorem :: JORDAN4:59
for f being non constant standard special_circular_sequence,
  g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
  g is_a_part<_of f,i1,i2 & i1<>i2 holds
  L~g is_S-P_arc_joining f/.i1,f/.i2;

theorem :: JORDAN4:60
for f being non constant standard special_circular_sequence,
 g being FinSequence of TOP-REAL 2,i1,i2 being Nat
  st g is_a_part_of f,i1,i2 & i1<>i2
 holds L~g is_S-P_arc_joining f/.i1,f/.i2;

theorem :: JORDAN4:61
for f being non constant standard special_circular_sequence,
 g being FinSequence of TOP-REAL 2,i1,i2 being Nat
  st g is_a_part_of f,i1,i2 & g.1<>g.len g
 holds L~g is_S-P_arc_joining f/.i1,f/.i2;

theorem :: JORDAN4:62
for f being non constant standard special_circular_sequence,
  i1,i2 being Nat st
  1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f & i1<>i2 holds
  ex g1,g2 being FinSequence of TOP-REAL 2 st
  g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2
  & (L~g1)/\(L~g2)={f.i1,f.i2} & (L~g1) \/ (L~g2)=L~f &
  L~g1 is_S-P_arc_joining f/.i1,f/.i2 &
  L~g2 is_S-P_arc_joining f/.i1,f/.i2 &
  for g being FinSequence of TOP-REAL 2 st g is_a_part_of f,i1,i2 holds
  g=g1 or g=g2;

reserve g, g1, g2 for FinSequence of TOP-REAL 2;

theorem :: JORDAN4:63
  for f being non constant standard special_circular_sequence,
    P being non empty Subset of TOP-REAL 2 st P = L~f
 holds P is_simple_closed_curve;

theorem :: JORDAN4:64
for f being non constant standard special_circular_sequence,
 g1,g2 st g1 is_a_part>_of f,i1,i2 & g2 is_a_part>_of f,i1,i2
 holds g1=g2;

theorem :: JORDAN4:65
for f being non constant standard special_circular_sequence,
 g1,g2 st g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2
 holds g1=g2;

theorem :: JORDAN4:66
for f being non constant standard special_circular_sequence,
 g1,g2 st i1<>i2 & g1 is_a_part>_of f,i1,i2 & g2 is_a_part<_of f,i1,i2
 holds g1.2<>g2.2;

theorem :: JORDAN4:67
for f being non constant standard special_circular_sequence,
 g1,g2 st i1<>i2 & g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2
 & g1.2=g2.2 holds g1=g2;

definition let f be non constant standard special_circular_sequence,
 i1,i2 be Nat;
 assume 1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f & i1<>i2;
 func Lower (f,i1,i2) -> FinSequence of TOP-REAL 2 means
:: JORDAN4:def 5
   it is_a_part_of f,i1,i2 &
   ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+1))`2<(f/.i1)`2 implies it.2=f.(i1+1))&
   ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))`2>=(f/.i1)`2
                implies it.2=f.S_Drop(i1-'1,f));

 func Upper (f,i1,i2) -> FinSequence of TOP-REAL 2 means
:: JORDAN4:def 6
    it is_a_part_of f,i1,i2 &
   ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+1))`2>(f/.i1)`2 implies it.2=f.(i1+1))&
   ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))`2<=(f/.i1)`2
                implies it.2=f.S_Drop(i1-'1,f));
end;

Back to top