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:: Some Properties of Restrictions of Finite Sequences
by
Czeslaw Bylinski
Received January 25, 1995
MML identifier: FINSEQ_5
[ Mizar article, MML identifier index ]
environ

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


begin

reserve i,j,k,m,n for Nat;

theorem :: FINSEQ_5:1
   i <= n implies n - i + 1 is Nat;

theorem :: FINSEQ_5:2
   i in Seg n implies n - i + 1 in Seg n;

theorem :: FINSEQ_5:3
   for f being Function, x,y being set st f"{y} = {x}
    holds x in dom f & y in rng f & f.x = y;

theorem :: FINSEQ_5:4
     for f being Function holds f is one-to-one iff
    for x being set st x in dom f holds f"{f.x} = {x};

theorem :: FINSEQ_5:5
     for f being Function, y1,y2 being set
    st f is one-to-one & y1 in rng f & y2 in rng f & f"{y1} = f"{y2}
   holds y1 = y2;

definition let x be set;
 cluster <*x*> -> non empty;
end;

definition
 cluster empty -> trivial set;
end;

definition let x be set;
 cluster <*x*> -> trivial;

 let y be set;
 cluster <*x,y*> -> non trivial;
end;

definition
 cluster one-to-one non empty FinSequence;
end;

theorem :: FINSEQ_5:6
   for f being non empty FinSequence holds 1 in dom f & len f in dom f;

theorem :: FINSEQ_5:7
     for f being non empty FinSequence ex i st i+1 = len f;

theorem :: FINSEQ_5:8
  for x being set, f being FinSequence holds len(<*x*>^f) = 1 + len f;

scheme domSeqLambda{A()->Nat,F(set) -> set}:
   ex p being FinSequence st len p = A() & for k st k in dom p holds p.k=F(k);

canceled;

theorem :: FINSEQ_5:10
     for f being FinSequence, p,q being set
     st p in rng f & q in rng f & p..f = q..f
    holds p = q;

theorem :: FINSEQ_5:11
  for f,g being FinSequence st n+1 in dom f & g = f|Seg n holds
    f|Seg(n+1) = g^<*f.(n+1)*>;

theorem :: FINSEQ_5:12
   for f being one-to-one FinSequence st i in dom f holds (f.i)..f = i;

reserve D for non empty set, p for Element of D, f,g for FinSequence of D;

definition let D be non empty set;
 cluster one-to-one non empty FinSequence of D;
end;

:: FINSEQ_1:17

theorem :: FINSEQ_5:13
     dom f = dom g & (for i st i in dom f holds f/.i = g/.i) implies f = g;

:: FINSEQ_1:18

theorem :: FINSEQ_5:14
 len f = len g & (for k st 1 <= k & k <= len f holds f/.k = g/.k)
  implies f = g;

theorem :: FINSEQ_5:15
  len f = 1 implies f = <*f/.1*>;

theorem :: FINSEQ_5:16
 for D being non empty set, p being Element of D,
     f being FinSequence of D holds
   (<*p*>^f)/.1 = p;

canceled;

theorem :: FINSEQ_5:18
 for D being set, f being FinSequence of D holds
   len(f|i) <= len f;

theorem :: FINSEQ_5:19
 for D being set, f being FinSequence of D holds
   len(f|i) <= i;

theorem :: FINSEQ_5:20
 for D being set, f being FinSequence of D holds
   dom(f|i) c= dom f;

theorem :: FINSEQ_5:21
   rng(f|i) c= rng f;

canceled;

theorem :: FINSEQ_5:23
  for D being set, f being FinSequence of D holds
   f is non empty implies f|1 = <*f/.1*>;

theorem :: FINSEQ_5:24
     i+1 = len f implies f = (f|i)^<*f/.len f*>;

definition let i,D; let f be one-to-one FinSequence of D;
 cluster f|i -> one-to-one;
end;

theorem :: FINSEQ_5:25
 for D being set, f, g being FinSequence of D holds
   i <= len f implies (f^g)|i = f|i;

theorem :: FINSEQ_5:26
   for D being set, f, g being FinSequence of D holds
   (f^g)|(len f) = f;

theorem :: FINSEQ_5:27
   for D being set, f being FinSequence of D holds
  p in rng f implies (f-|p)^<*p*> = f|(p..f);

theorem :: FINSEQ_5:28
     len(f/^i) <= len f;

theorem :: FINSEQ_5:29
   i in dom(f/^n) implies n+i in dom f;

theorem :: FINSEQ_5:30
   i in dom(f/^n) implies (f/^n)/.i = f/.(n+i);

theorem :: FINSEQ_5:31
   f/^0 = f;

theorem :: FINSEQ_5:32
     f is non empty implies f = <*f/.1*>^(f/^1);

theorem :: FINSEQ_5:33
     i+1 = len f implies f/^i = <*f/.len f*>;

theorem :: FINSEQ_5:34
   j+1 = i & i in dom f implies <*f/.i*>^(f/^i) = f/^j;

theorem :: FINSEQ_5:35
 for D being set, f being FinSequence of D holds
   len f <= i implies f/^i is empty;

theorem :: FINSEQ_5:36
   rng(f/^n) c= rng f;

definition let i,D; let f be one-to-one FinSequence of D;
 cluster f/^i -> one-to-one;
end;

theorem :: FINSEQ_5:37
   f is one-to-one implies rng(f|n) misses rng(f/^n);

theorem :: FINSEQ_5:38
     p in rng f implies f |-- p = f/^(p..f);

theorem :: FINSEQ_5:39
   (f^g)/^(len f + i) = g/^i;

theorem :: FINSEQ_5:40
     (f^g)/^(len f) = g;

theorem :: FINSEQ_5:41
   p in rng f implies f/.(p..f) = p;

theorem :: FINSEQ_5:42
   i in dom f implies f/.i..f <= i;

theorem :: FINSEQ_5:43
     p in rng(f|i) implies p..(f|i) = p..f;

theorem :: FINSEQ_5:44
     i in dom f & f is one-to-one implies f/.i..f = i;

definition let D, f; let p be set;
 func f-:p -> FinSequence of D equals
:: FINSEQ_5:def 1
  f|(p..f);
end;

theorem :: FINSEQ_5:45
   p in rng f implies len(f-:p) = p..f;

theorem :: FINSEQ_5:46
   p in rng f & i in Seg(p..f) implies (f-:p)/.i = f/.i;

theorem :: FINSEQ_5:47
     p in rng f implies (f-:p)/.1 = f/.1;

theorem :: FINSEQ_5:48
     p in rng f implies (f-:p)/.(p..f) = p;

theorem :: FINSEQ_5:49
   for x being set holds
   x in rng f & p in rng f & x..f<=p..f implies x in rng(f-:p);

theorem :: FINSEQ_5:50
     p in rng f implies f-:p is non empty;

theorem :: FINSEQ_5:51
     rng(f-:p) c= rng f;

definition let D,p; let f be one-to-one FinSequence of D;
 cluster f-:p -> one-to-one;
end;

definition let D, f, p;
 func f:-p -> FinSequence of D equals
:: FINSEQ_5:def 2
  <*p*>^(f/^p..f);
end;

theorem :: FINSEQ_5:52
  p in rng f implies ex i st i+1 = p..f & f:-p = f/^i;

theorem :: FINSEQ_5:53
   p in rng f implies len (f:-p) = len f - p..f + 1;

theorem :: FINSEQ_5:54
  p in rng f & j+1 in dom(f:-p) implies j+p..f in dom f;

definition let D,p,f;
 cluster f:-p -> non empty;
end;

theorem :: FINSEQ_5:55
   p in rng f & j+1 in dom(f:-p) implies (f:-p)/.(j+1) = f/.(j+p..f);

theorem :: FINSEQ_5:56
    (f:-p)/.1 = p;

theorem :: FINSEQ_5:57
     p in rng f implies (f:-p)/.(len(f:-p)) = f/.len f;

theorem :: FINSEQ_5:58
     p in rng f implies rng(f:-p) c= rng f;

theorem :: FINSEQ_5:59
     p in rng f & f is one-to-one implies f:-p is one-to-one;

definition let f be FinSequence;
 func Rev f -> FinSequence means
:: FINSEQ_5:def 3
 len it = len f & for i st i in dom it holds it.i = f.(len f - i + 1);
end;

theorem :: FINSEQ_5:60
   for f being FinSequence holds dom f = dom Rev f & rng f = rng Rev f;

theorem :: FINSEQ_5:61
  for f being FinSequence st i in dom f holds (Rev f).i = f.(len f - i + 1);

theorem :: FINSEQ_5:62
  for f being FinSequence, i,j being Nat
    st i in dom f & i+j = len f + 1
  holds j in dom Rev f;

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

theorem :: FINSEQ_5:63
     for x being set holds Rev <*x*> = <*x*>;

theorem :: FINSEQ_5:64
     for x1,x2 being set holds Rev <*x1,x2*> = <*x2,x1*>;

theorem :: FINSEQ_5:65
  for f being FinSequence
   holds f.1 = (Rev f).(len f) & f.(len f) = (Rev f).1;

definition let f be one-to-one FinSequence;
 cluster Rev f -> one-to-one;
end;

theorem :: FINSEQ_5:66
  for f being FinSequence, x being set holds Rev(f^<*x*>) = <*x*>^(Rev f);

theorem :: FINSEQ_5:67
     for f,g being FinSequence holds Rev(f^g) = (Rev g)^(Rev f);

definition let D,f;
 redefine func Rev f -> FinSequence of D;
end;

theorem :: FINSEQ_5:68
     f is non empty implies f/.1 = (Rev f)/.len f & f/.len f = (Rev f)/.1;

theorem :: FINSEQ_5:69
     i in dom f & i+j = len f + 1 implies f/.i = (Rev f)/.j;

definition let D,f,p,n;
  func Ins(f,n,p) -> FinSequence of D equals
:: FINSEQ_5:def 4
  (f|n)^<*p*>^(f/^n);
end;

theorem :: FINSEQ_5:70
     Ins(f,0,p) = <*p*>^f;

theorem :: FINSEQ_5:71
   len f <= n implies Ins(f,n,p) = f^<*p*>;

theorem :: FINSEQ_5:72
   len(Ins(f,n,p)) = len f + 1;

theorem :: FINSEQ_5:73
   rng Ins(f,n,p) = {p} \/ rng f;

definition let D,f,n,p;
 cluster Ins(f,n,p) -> non empty;
end;

theorem :: FINSEQ_5:74
     p in rng Ins(f,n,p);

theorem :: FINSEQ_5:75
   i in dom(f|n) implies (Ins(f,n,p))/.i = f/.i;

theorem :: FINSEQ_5:76
     n <= len f implies (Ins(f,n,p))/.(n+1) = p;

theorem :: FINSEQ_5:77
     n+1 <= i & i <= len f implies (Ins(f,n,p))/.(i+1) = f/.i;

theorem :: FINSEQ_5:78
     1 <= n & f is non empty implies (Ins(f,n,p))/.1 = f/.1;

theorem :: FINSEQ_5:79
     f is one-to-one & not p in rng f implies Ins(f,n,p) is one-to-one;
The abstract of the Mizar article:

Some Properties of Restrictions of Finite Sequences
