The Mizar abstract of FINSEQ

Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users
The abstract of the Mizar article:: On the Decomposition of Finite Sequences
by
Andrzej Trybulec
Received May 24, 1995
MML identifier: FINSEQ_6
[ Mizar article, MML identifier index ]
environ

 vocabulary FINSEQ_1, REALSET1, FINSEQ_5, RELAT_1, BOOLE, FUNCT_1, FINSEQ_4,
      ARYTM_1, RLSUB_2, RFINSEQ, FINSEQ_6, ORDINAL2, ARYTM;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS,
      XCMPLX_0, XREAL_0, NAT_1, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, FINSEQ_4,
      RFINSEQ, FINSEQ_5, REALSET1, TOPREAL1;
 constructors REAL_1, NAT_1, MATRIX_2, FINSEQ_5, ENUMSET1, RFINSEQ, TOPREAL1,
      REALSET1, FINSEQ_4, INT_1, MEMBERED, XBOOLE_0;
 clusters RELSET_1, FINSEQ_5, FUNCT_1, GOBOARD4, FINSEQ_1, INT_1, REALSET1,
      ZFMISC_1, XBOOLE_0, ORDINAL2, ARYTM_3;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

reserve x,y,z for set;

definition let x,y,z;
 cluster <*x,y,z*> -> non trivial;
end;

definition let f be non empty FinSequence;
 cluster Rev f -> non empty;
end;

begin

reserve f,f1,f2,f3 for FinSequence,
        p,p1,p2,p3 for set,
        i,k for Nat;

canceled 2;

theorem :: FINSEQ_6:3
 for X being set, i st X c= Seg i & 1 in X holds (Sgm X).1 = 1;

theorem :: FINSEQ_6:4
 for f being FinSequence holds
 k in dom f & (for i st 1 <= i & i < k holds f.i <> f.k)
   implies (f.k)..f = k;

theorem :: FINSEQ_6:5
 <*p1,p2*>| Seg 1 = <*p1*>;

theorem :: FINSEQ_6:6
 <*p1,p2,p3*>| Seg 1 = <*p1*>;

theorem :: FINSEQ_6:7
 <*p1,p2,p3*>| Seg 2 = <*p1,p2*>;

theorem :: FINSEQ_6:8
 p in rng f1 implies p..(f1^f2) = p..f1;

theorem :: FINSEQ_6:9
 p in rng f2 \ rng f1 implies p..(f1^f2) = len f1 + p..f2;

theorem :: FINSEQ_6:10
 p in rng f1 implies (f1^f2)|--p = (f1|--p)^f2;

theorem :: FINSEQ_6:11
 p in rng f2 \ rng f1 implies (f1^f2)|--p = f2|--p;

theorem :: FINSEQ_6:12
 f1 c= f1^f2;

theorem :: FINSEQ_6:13
 for A being set st A c= dom f1 holds (f1^f2)|A = f1 | A;

theorem :: FINSEQ_6:14
 p in rng f1 implies (f1^f2)-|p = f1-|p;

definition let f1; let i be natural number;
 cluster f1|Seg i -> FinSequence-like;
end;

theorem :: FINSEQ_6:15
 f1 c= f2 implies f3^f1 c= f3^f2;

theorem :: FINSEQ_6:16
 (f1^f2)|Seg(len f1 + i) = f1^(f2|Seg i);

theorem :: FINSEQ_6:17
 p in rng f2 \ rng f1 implies (f1^f2)-|p = f1^(f2-|p);

canceled;

theorem :: FINSEQ_6:19
 f1^f2 just_once_values p implies p in rng f1 \+\ rng f2;

theorem :: FINSEQ_6:20
   f1^f2 just_once_values p & p in rng f1 implies f1 just_once_values p;

theorem :: FINSEQ_6:21
 rng f is non trivial implies f is non trivial;

theorem :: FINSEQ_6:22
 p..<*p*> = 1;

theorem :: FINSEQ_6:23
 p1..<*p1,p2*> = 1;

theorem :: FINSEQ_6:24
 p1 <> p2 implies p2..<*p1,p2*> = 2;

theorem :: FINSEQ_6:25
 p1..<*p1,p2,p3*> = 1;

theorem :: FINSEQ_6:26
 p1 <> p2 implies p2..<*p1,p2,p3*> = 2;

theorem :: FINSEQ_6:27
 p1 <> p3 & p2 <> p3 implies p3..<*p1,p2,p3*> = 3;

theorem :: FINSEQ_6:28
 for f being FinSequence holds
 Rev(<*p*>^f) = Rev f ^ <*p*>;

theorem :: FINSEQ_6:29
 for f being FinSequence holds
 Rev Rev f = f;

theorem :: FINSEQ_6:30
 x <> y implies <*x,y*> -| y = <*x*>;

theorem :: FINSEQ_6:31
 x <> y implies <*x,y,z*> -| y = <*x*>;

theorem :: FINSEQ_6:32
 x <> z & y <> z implies <*x,y,z*> -| z = <*x,y*>;

theorem :: FINSEQ_6:33
   <*x,y*>|--x = <*y*>;

theorem :: FINSEQ_6:34
 x <> y implies <*x,y,z*>|--y = <*z*>;

theorem :: FINSEQ_6:35
   <*x,y,z*>|--x = <*y,z*>;

theorem :: FINSEQ_6:36
 <*z*>|--z = {} & <*z*>-|z = {};

theorem :: FINSEQ_6:37
 x <> y implies <*x,y*> |-- y = {};

theorem :: FINSEQ_6:38
 x <> z & y <> z implies <*x,y,z*> |-- z = {};

theorem :: FINSEQ_6:39
 x in rng f & y in rng(f-|x) implies f-|x-|y = f-|y;

theorem :: FINSEQ_6:40
 not x in rng f1 implies x..(f1^<*x*>^f2) = len f1 + 1;

theorem :: FINSEQ_6:41
 f just_once_values x implies x..f + x..Rev f = len f + 1;

theorem :: FINSEQ_6:42
 f just_once_values x implies Rev(f-|x) = Rev f |--x;

theorem :: FINSEQ_6:43
   f just_once_values x implies Rev f just_once_values x;

begin

reserve D for non empty set,
        p,p1,p2,p3 for Element of D,
        f,f1,f2 for FinSequence of D;

theorem :: FINSEQ_6:44
 p in rng f implies f-:p = (f -| p)^<*p*>;

theorem :: FINSEQ_6:45
 p in rng f implies f:-p = <*p*>^(f |-- p);

theorem :: FINSEQ_6:46
 f <> {} implies f/.1 in rng f;

theorem :: FINSEQ_6:47
 f <> {} implies f/.1..f = 1;

theorem :: FINSEQ_6:48
 f <> {} & f/.1 = p implies f-:p = <*p*> & f:-p = f;

theorem :: FINSEQ_6:49
 (<*p1*>^f)/^1 = f;

theorem :: FINSEQ_6:50
 <*p1,p2*>/^1 = <*p2*>;

theorem :: FINSEQ_6:51
 <*p1,p2,p3*>/^1 = <*p2,p3*>;

theorem :: FINSEQ_6:52
 k in dom f & (for i st 1 <= i & i < k holds f/.i <> f/.k)
   implies f/.k..f = k;

theorem :: FINSEQ_6:53
 p1 <> p2 implies <*p1,p2*>-:p2 = <*p1,p2*>;

theorem :: FINSEQ_6:54
 p1 <> p2 implies <*p1,p2,p3*>-:p2 = <*p1,p2*>;

theorem :: FINSEQ_6:55
 p1 <> p3 & p2 <> p3 implies <*p1,p2,p3*>-:p3 = <*p1,p2,p3*>;

theorem :: FINSEQ_6:56
   <*p*>:-p = <*p*> & <*p*>-:p = <*p*>;

theorem :: FINSEQ_6:57
 p1 <> p2 implies <*p1,p2*>:-p2 = <*p2*>;

theorem :: FINSEQ_6:58
 p1 <> p2 implies <*p1,p2,p3*>:-p2 = <*p2,p3*>;

theorem :: FINSEQ_6:59
 p1 <> p3 & p2 <> p3 implies <*p1,p2,p3*>:-p3 = <*p3*>;

canceled;

theorem :: FINSEQ_6:61
 p in rng f & p..f > k implies p..f = k + p..(f/^k);

theorem :: FINSEQ_6:62
 p in rng f & p..f > k implies p in rng(f/^k);

theorem :: FINSEQ_6:63
  k < i & i in dom f implies f/.i in rng(f/^k);

theorem :: FINSEQ_6:64
 p in rng f & p..f > k implies (f/^k)-:p = (f-:p)/^k;

theorem :: FINSEQ_6:65
 p in rng f & p..f <> 1 implies (f/^1)-:p = (f-:p)/^1;

theorem :: FINSEQ_6:66
  p in rng(f:-p);

theorem :: FINSEQ_6:67
 x in rng f & p in rng f & x..f >= p..f implies x in rng(f:-p);

theorem :: FINSEQ_6:68
  p in rng f & k <= len f & k >= p..f implies f/.k in rng(f:-p);

theorem :: FINSEQ_6:69
 p in rng f1 implies (f1^f2):-p = (f1:-p)^f2;

theorem :: FINSEQ_6:70
 p in rng f2 \ rng f1 implies (f1^f2):-p = f2:-p;

theorem :: FINSEQ_6:71
 p in rng f1 implies (f1^f2)-:p = f1-:p;

theorem :: FINSEQ_6:72
 p in rng f2 \ rng f1 implies (f1^f2)-:p = f1^(f2-:p);

theorem :: FINSEQ_6:73
    f:-p:-p = f:-p;

theorem :: FINSEQ_6:74
 p1 in rng f & p2 in rng f \ rng(f-:p1) implies f|--p2 = f|--p1|--p2;

theorem :: FINSEQ_6:75
 p in rng f implies rng f = rng(f-:p) \/ rng(f:-p);

theorem :: FINSEQ_6:76
 p1 in rng f & p2 in rng f \ rng(f-:p1) implies f:-p1:-p2 = f:-p2;

theorem :: FINSEQ_6:77
 p in rng f implies p..(f-:p) = p..f;

theorem :: FINSEQ_6:78
 f|i|i = f|i;

theorem :: FINSEQ_6:79
  p in rng f implies f-:p-:p = f-:p;

theorem :: FINSEQ_6:80
 p1 in rng f & p2 in rng(f-:p1) implies f-:p1-:p2 = f-:p2;

theorem :: FINSEQ_6:81
 p in rng f implies (f-:p)^((f:-p)/^1) = f;

theorem :: FINSEQ_6:82
 f1 <> {} implies (f1^f2)/^1 = (f1/^1)^f2;

theorem :: FINSEQ_6:83
 p2 in rng f & p2..f <> 1 implies p2 in rng(f/^1);

theorem :: FINSEQ_6:84
 p..(f:-p) = 1;

canceled;

theorem :: FINSEQ_6:86
 <*>D/^k = <*>D;

theorem :: FINSEQ_6:87
  f/^(i+k) = f/^i/^k;

theorem :: FINSEQ_6:88
 p in rng f & p..f > k implies (f/^k):-p = f:-p;

theorem :: FINSEQ_6:89
 p in rng f & p..f <> 1 implies (f/^1):-p = f:-p;

theorem :: FINSEQ_6:90
 i + k = len f implies Rev(f/^k) = Rev f|i;

theorem :: FINSEQ_6:91
 i + k = len f implies Rev(f|k) = Rev f/^i;

theorem :: FINSEQ_6:92
 f just_once_values p implies Rev(f|--p) = Rev f -|p;

theorem :: FINSEQ_6:93
 f just_once_values p implies Rev(f:-p) = Rev f -:p;

theorem :: FINSEQ_6:94
 f just_once_values p implies Rev(f-:p) = Rev f :-p;

begin :: rotation, circular

definition let D be non empty set;
 let IT be FinSequence of D;
 attr IT is circular means
:: FINSEQ_6:def 1
 IT/.1 = IT/.len IT;
end;

definition let D,f,p;
 func Rotate(f,p) -> FinSequence of D equals
:: FINSEQ_6:def 2
 (f:-p)^((f-:p)/^1) if p in rng f
   otherwise f;
end;

definition let D; let f be non empty FinSequence of D, p be Element of D;
 cluster Rotate(f,p) -> non empty;
end;

definition let D;
 cluster circular non empty trivial FinSequence of D;
 cluster circular non empty non trivial FinSequence of D;
end;

theorem :: FINSEQ_6:95
 Rotate(f,f/.1) = f;

definition let D,p; let f be circular non empty FinSequence of D;
 cluster Rotate(f,p) -> circular;
end;

theorem :: FINSEQ_6:96
   f is circular & p in rng f implies rng Rotate(f,p) = rng f;

theorem :: FINSEQ_6:97
 p in rng f implies p in rng Rotate(f,p);

theorem :: FINSEQ_6:98
 p in rng f implies (Rotate(f,p))/.1 = p;

theorem :: FINSEQ_6:99
 Rotate(Rotate(f,p),p) = Rotate(f,p);

theorem :: FINSEQ_6:100
   Rotate(<*p*>,p) = <*p*>;

theorem :: FINSEQ_6:101
 Rotate(<*p1,p2*>,p1) = <*p1,p2*>;

theorem :: FINSEQ_6:102
   Rotate(<*p1,p2*>,p2) = <*p2,p2*>;

theorem :: FINSEQ_6:103
 Rotate(<*p1,p2,p3*>,p1) = <*p1,p2,p3*>;

theorem :: FINSEQ_6:104
   p1 <> p2 implies Rotate(<*p1,p2,p3*>,p2) = <*p2,p3,p2*>;

theorem :: FINSEQ_6:105
   p2 <> p3 implies Rotate(<*p1,p2,p3*>,p3) = <*p3,p2,p3*>;

theorem :: FINSEQ_6:106
   for f being circular non trivial FinSequence of D
  holds rng(f/^1) = rng f;

theorem :: FINSEQ_6:107
  rng(f/^1) c= rng Rotate(f,p);

theorem :: FINSEQ_6:108
 p2 in rng f \ rng(f-:p1) implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2);

theorem :: FINSEQ_6:109
 p2..f <> 1 & p2 in rng f \ rng(f:-p1)
     implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2);

theorem :: FINSEQ_6:110
 p2 in rng(f/^1) & f just_once_values p2
   implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2);

theorem :: FINSEQ_6:111
   f is circular & f just_once_values p2
    implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2);

theorem :: FINSEQ_6:112
   f is circular & f just_once_values p implies
  Rev Rotate(f,p) = Rotate(Rev f,p);
The abstract of the Mizar article:

On the Decomposition of Finite Sequences
