:: Basic Properties and Concept of Selected Subsequence of Zero Based Finite
:: Sequences
::  by Yatsuka Nakamura and Hisashi Ito
::
:: Received June 27, 2008
:: Copyright (c) 2008-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, SUBSET_1, FUNCT_1, NAT_1, TARSKI, MEMBERED, ORDINAL1,
      FINSET_1, RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, XXREAL_0,
      CARD_1, XBOOLE_0, ORDINAL4, FINSEQ_5, RFINSEQ, JORDAN3, CARD_3, XCMPLX_0,
      AFINSQ_2, BINOP_1, SETWISEO, FINSOP_1, FUNCOP_1, BINOP_2, VALUED_0,
      FUNCT_2, INT_1, PRGCOR_2, XREAL_0, SEQ_1, SERIES_1, VALUED_1, RAT_1,
      SQUARE_1, COMPLEX1, PARTFUN3, PRE_POLY, AMISTD_1, AMISTD_2, REAL_1,
      ORDINAL2;
 notations TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, CARD_1, NUMBERS,
      RELAT_1, FUNCT_1, XCMPLX_0, NAT_1, FINSET_1, XXREAL_0, NAT_D, AFINSQ_1,
      SEQ_1, MEMBERED, VALUED_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, INT_1,
      BINOP_1, BINOP_2, SETWISEO, FINSOP_1, FINSEQ_1, RECDEF_1, VALUED_0,
      SERIES_1, RAT_1, PARTFUN3, RFINSEQ, ORDINAL2;
 constructors SERIES_1, PARTFUN3, WELLORD2, SETWISEO, FINSOP_1, NAT_D,
      RECDEF_1, BINOP_2, RELSET_1, AFINSQ_1, FUNCOP_1, SQUARE_1, BINOP_1,
      XTUPLE_0, RFINSEQ, ORDINAL2;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1,
      NUMBERS, XXREAL_0, XREAL_0, NAT_1, BINOP_2, CARD_1, FINSEQ_1, AFINSQ_1,
      ORDINAL2, RELSET_1, ORDINAL3, VALUED_1, VALUED_0, MEMBERED;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preparation

reserve i,j,k,n,m for Nat,
  x,y,z,y1,y2 for object, X,Y,D for set,
  p,q for XFinSequence;

theorem :: AFINSQ_2:1
  x in i implies x is Element of NAT;

begin

theorem :: AFINSQ_2:2
  for X0 being finite natural-membered set holds ex n st X0 c= Segm n;

theorem :: AFINSQ_2:3  :: from FINSEQ_2:11
x in rng p implies ex
  i being Element of NAT st i in dom p & p.i = x;

theorem :: AFINSQ_2:4  ::from FINSEQ_2:14
  for p st for i st i in dom p holds p.i in D
   holds p is XFinSequence of D;

scheme :: AFINSQ_2:sch 1
  XSeqLambdaD{i()->Nat,D()->non empty set,F(set)->Element of D()}:
  ex p being XFinSequence of D() st len p = i() &
    for j st j in i() holds p.j = F(j);



registration
  cluster empty natural-valued for XFinSequence;
  let p be complex-valued Sequence-like Function;
  cluster -p -> Sequence-like;
  cluster p" -> Sequence-like;
  cluster p^2 -> Sequence-like;
cluster abs p -> Sequence-like;
  let q be complex-valued Sequence-like Function;
  cluster p+q -> Sequence-like;
  cluster p-q -> Sequence-like;
  cluster p(#)q -> Sequence-like;
  cluster p/"q -> Sequence-like;
end;

registration
  let p be complex-valued finite Function;
  cluster -p -> finite;
  cluster p" -> finite;
  cluster p^2 -> finite;
  cluster abs p -> finite;
  let q be complex-valued Function;
  cluster p+q -> finite;
  cluster p-q -> finite;
  cluster p(#)q -> finite;
  cluster p/"q -> finite;
  cluster q/"p -> finite;
end;

registration
  let p be complex-valued Sequence-like Function;
  let c be Complex;
  cluster c+p -> Sequence-like;
  cluster p-c -> Sequence-like;
  cluster c(#)p -> Sequence-like;
end;

registration
  let p be complex-valued finite Function;
  let c be Complex;
  cluster c+p -> finite;
  cluster p-c -> finite;
  cluster c(#)p -> finite;
end;



definition
  let p;
  func Rev p -> XFinSequence means
:: AFINSQ_2:def 1

  len it = len p & for i st i in dom it holds it.i = p.(len p - (i + 1));
end;

theorem :: AFINSQ_2:5  ::from FINSEQ_5:60
  dom p = dom Rev p & rng p = rng Rev p;

registration
  let D be set, f be XFinSequence of D;
  cluster Rev f -> D -valued;
end;

definition
  let p,n;
  func p /^ n -> XFinSequence means
:: AFINSQ_2:def 2
  len it = len p -' n & for m st m in dom it holds it.m = p.(m+n);
end;

theorem :: AFINSQ_2:6
  n >= len p implies p/^n={};

theorem :: AFINSQ_2:7
  n < len p implies len (p/^n) = len p -n;

theorem :: AFINSQ_2:8
  m+n<len p implies (p/^n).m = p.(m+n);

registration
  let f be one-to-one XFinSequence, n;
  cluster f/^n -> one-to-one;
end;

theorem :: AFINSQ_2:9
  rng (p/^n) c= rng p;

theorem :: AFINSQ_2:10  ::FINSEQ_5:31
 p/^0 = p;

theorem :: AFINSQ_2:11  ::FINSEQ_5:39
  (p^q)/^(len p + i) = q/^i;

theorem :: AFINSQ_2:12  ::FINSEQ_5:40
  (p^q)/^(len p) = q;

theorem :: AFINSQ_2:13  ::RFINSEQ:21
  (p|n)^(p/^n) = p;

registration
  let f be XFinSequence;
  cluster f|0 -> empty;
  let n be Nat;
  cluster f/^(dom f + n) -> empty;
  reduce f|(len f + n) to f;
  reduce (f|n)^(f/^n) to f;
end;

registration
  let D be set, f be XFinSequence of D, n;
  cluster f /^ n -> D -valued;
end;

reserve k1,k2 for Nat;

definition
  let p,k1,k2;
  func mid(p,k1,k2) -> XFinSequence equals
:: AFINSQ_2:def 3
  (p|k2)/^(k1-'1);
end;

theorem :: AFINSQ_2:14
  k1>k2 implies mid(p,k1,k2) = {};

theorem :: AFINSQ_2:15
  1<=k1 & k2<=len p implies mid(p,k1,k2) = (p/^(k1-'1))|(k2+1-'k1);

theorem :: AFINSQ_2:16  :: FINSEQ_8:5
  mid(p,1,k)=p|k;

theorem :: AFINSQ_2:17 :: FINSEQ_8:6
  len p<=k implies mid(p,1,k)=p;

theorem :: AFINSQ_2:18 :: FINSEQ_8:8
  mid(p,0,k)=mid(p,1,k);

theorem :: AFINSQ_2:19 :: FINSEQ_8:9
  mid(p^q,len p+1,len p+len q)=q;

registration
  let D be set, f be XFinSequence of D, k1,k2;
  cluster mid(f,k1,k2) -> D-valued;
end;

begin :: Selected Subsequences

definition
  let X be finite natural-membered set;
  func Sgm0 X -> XFinSequence of NAT means
:: AFINSQ_2:def 4
  rng it = X & for l,m,k1,k2 being Nat st
    l < m & m < len it & k1=it.l & k2=it.m holds k1 < k2;
end;

registration
  let A be finite natural-membered set;
  cluster Sgm0 A -> one-to-one;
end;

theorem :: AFINSQ_2:20  :: FINSEQ_3:44
  for A being finite natural-membered set holds len(Sgm0 A) = card A;

theorem :: AFINSQ_2:21
  for X,Y being finite natural-membered set st X c= Y & X <> {}
  holds (Sgm0 Y).0 <= (Sgm0 X).0;

theorem :: AFINSQ_2:22
  (Sgm0 {n}).0=n;

definition
  let B1,B2 be set;
  pred B1 <N< B2 means
:: AFINSQ_2:def 5

  for n,m being Nat st n in B1 & m in B2 holds n<m;
end;

definition
  let B1,B2 be set;
  pred B1 <N= B2 means
:: AFINSQ_2:def 6

  for n,m st n in B1 & m in B2 holds n <= m;
end;

theorem :: AFINSQ_2:23
  for B1,B2 being set st B1 <N< B2 holds B1/\B2/\NAT={};

theorem :: AFINSQ_2:24
  for B1,B2 being finite natural-membered set st B1 <N< B2 holds
  B1 misses B2;

theorem :: AFINSQ_2:25
  for A,B1,B2 being set st B1 <N< B2 holds A/\ B1 <N< A/\B2;

theorem :: AFINSQ_2:26
  for X,Y being finite natural-membered set st Y <> {} & (ex x being set
  st x in X & {x} <N= Y) holds (Sgm0 X).0 <= (Sgm0 Y).0;

theorem :: AFINSQ_2:27
  for X0,Y0 being finite natural-membered set st
    X0 <N< Y0 & i < (card X0) holds
  rng((Sgm0 (X0\/Y0))|(card X0))=X0 &
  ((Sgm0 (X0\/Y0))|(card X0)).i = (Sgm0 (X0 \/ Y0)).i;

theorem :: AFINSQ_2:28
  for X,Y being finite natural-membered set st
     X <N< Y & i in card (X) holds (Sgm0 (X\/Y)).i in X;

theorem :: AFINSQ_2:29
  for X,Y being finite natural-membered set st X <N<
  Y & i< len (Sgm0 X) holds (Sgm0 X).i = (Sgm0 (X \/ Y)).i;

theorem :: AFINSQ_2:30
  for X0,Y0 being finite natural-membered set st X0
<N< Y0 & i < (card Y0) holds rng((Sgm0 (X0\/Y0))/^(card X0))=Y0 & ((Sgm0 (X0\/
  Y0))/^(card X0)).i = (Sgm0 (X0 \/ Y0)).(i+(card X0));

theorem :: AFINSQ_2:31
  for X,Y being finite natural-membered set st X <N< Y
  & i< len (Sgm0 Y) holds (Sgm0 Y).i = (Sgm0 (X \/ Y)).(i+len (Sgm0 X));

theorem :: AFINSQ_2:32
  for X,Y being finite natural-membered set st Y <> {} & X <N< Y
  holds (Sgm0 Y).0 = (Sgm0 (X \/ Y)).(len (Sgm0 X));

theorem :: AFINSQ_2:33  ::from FINSEQ_3:46
  for l,m,n,k being Nat,X being finite natural-membered set st k <
  l & m < len(Sgm0 X) & (Sgm0(X)).m = k & (Sgm0(X)).n = l holds m < n;

theorem :: AFINSQ_2:34
  for X,Y being finite natural-membered set st X <> {} & X <N< Y
  holds (Sgm0 X).0 = (Sgm0 (X \/ Y)).0;

theorem :: AFINSQ_2:35  ::from FINSEQ_3
  for X,Y being finite natural-membered set holds
X <N< Y iff Sgm0(X \/Y) = Sgm0(X) ^ Sgm0(Y);

definition
  let f be XFinSequence;
  let B be set;
  ::Following is a subsequence selected from f by B.
  func SubXFinS (f,B) -> XFinSequence equals
:: AFINSQ_2:def 7
  f*Sgm0(B /\ Segm len f);
end;

theorem :: AFINSQ_2:36
  for B being set holds len SubXFinS (p,B)=
   card (B/\ Segm(len p)) &
  for i st i < len SubXFinS (p,B) holds SubXFinS
  (p,B).i=p.((Sgm0 (B/\ Segm(len p))).i);

registration
  let D be set;
  let f be XFinSequence of D, B be set;
  cluster SubXFinS(f,B) -> D-valued;
end;

registration
  let p;
  cluster SubXFinS (p,{}) -> empty;
end;

registration
  let B be set;
  cluster SubXFinS ({},B) -> empty;
end;

 :: AFINSQ_2:48 => AFINSQ_2:83

reserve D for non empty set,
  F,G for XFinSequence of D,
  b for BinOp of D,
  d,d1,d2 for Element of D;

scheme :: AFINSQ_2:sch 2
  Sch5{D()->set, P[set]}: for F be XFinSequence of D() holds P[F]
provided
 P[<%>D()] and
 for F be XFinSequence of D(),d be Element of D() st P[F] holds P[F^<%d%>];

definition
  let D;
  let F be XFinSequence;
  assume F is D-valued;
  let b;
  assume  b is having_a_unity or len F >= 1;
  func b "**" F -> Element of D means
:: AFINSQ_2:def 8  :: STIRL2_1:def 3
  it = the_unity_wrt b if b is having_a_unity & len F = 0
    otherwise ex f be sequence of D st f.0 = F.0 &
   (for n st n+1 < len F holds f.(n + 1) = b.(f.n,F.(n + 1))) &
it = f.(len F-1);
end;

theorem :: AFINSQ_2:37
  b "**" <%d%> = d;

theorem :: AFINSQ_2:38
  b "**" <%d1,d2%> = b.(d1,d2);

theorem :: AFINSQ_2:39
  b "**" <%d,d1,d2%> = b.(b.(d,d1),d2);

theorem :: AFINSQ_2:40   :: STIRL2_1:45
  b is having_a_unity or len F > 0 implies b "**" (F ^ <% d %>) =
  b.(b "**" F,d);

::$CT

theorem :: AFINSQ_2:42  :: STIRL2_1:47
  b is associative & (b is having_a_unity or len F >= 1 & len G >= 1)
  implies b "**" (F ^ G) = b.(b "**" F,b "**" G);

theorem :: AFINSQ_2:43  :: CARD_FIN:42
  n in dom F & (b is having_a_unity or n <> 0 ) implies
   b.(b "**" F|n, F.n) = b "**" F|(n+1);

theorem :: AFINSQ_2:44  :: CARD_FIN:47
b is having_a_unity or len F >= 1 implies b "**" F = b "**" (XFS2FS F);

theorem :: AFINSQ_2:45  ::CARD_FIN:43
  for P be Permutation of dom F st b is commutative associative &
    (b is having_a_unity or len F >= 1) &
    G = F * P holds b "**" F = b "**" G;

theorem :: AFINSQ_2:46 :: CARD_FIN:62
  for bFG be XFinSequence of D st b is commutative associative &
         (b is having_a_unity or len F >= 1) &
         len F=len G & len F=len bFG &
         (for n st n in dom bFG holds bFG.n=b.(F.n,G.n))
  holds b "**" F^G = b "**" bFG;

theorem :: AFINSQ_2:47
  for D1,D2 be non empty set
    for b1 be BinOp of D1,b2 be BinOp of D2 st
        len F >= 1 &
        D c= D1 /\ D2 &
        for x,y st x in D & y in D holds b1.(x,y)=b2.(x,y) & b1.(x,y) in D
    holds b1 "**" F = b2 "**" F;

reserve F for XFinSequence,
        rF,rF1,rF2 for real-valued XFinSequence,
        r for Real,
        cF,cF1,cF2 for complex-valued XFinSequence,
        c,c1,c2 for Complex;

definition
  let F;
  func Sum F ->Element of COMPLEX equals
:: AFINSQ_2:def 9
    addcomplex "**" F;
end;

registration
  let f be empty complex-valued XFinSequence;
  cluster Sum f -> zero;
end;

theorem :: AFINSQ_2:48
   F is real-valued implies Sum F = addreal "**" F;

theorem :: AFINSQ_2:49
  F is RAT-valued implies Sum F = addrat "**" F;

theorem :: AFINSQ_2:50
  F is INT-valued implies Sum F = addint "**" F;

theorem :: AFINSQ_2:51
  F is natural-valued implies Sum F = addnat "**" F;

registration
  let F be real-valued XFinSequence;
  cluster Sum F -> real;
end;

registration
  let F be RAT-valued XFinSequence;
  cluster Sum F -> rational;
end;

registration
  let F be INT-valued XFinSequence;
  cluster Sum F -> integer;
end;

registration
  let F be natural-valued XFinSequence;
  cluster Sum F -> natural;
end;

registration
  cluster natural-valued -> nonnegative-yielding for Relation;
end;

theorem :: AFINSQ_2:52
  cF = {} implies Sum cF = 0;

theorem :: AFINSQ_2:53
   Sum <%c%> = c;

theorem :: AFINSQ_2:54
   Sum <%c1,c2%> = c1 + c2;

theorem :: AFINSQ_2:55  :: RLVECT_1:58 NUMERAL1:1
  Sum(cF1^cF2)=Sum(cF1)+Sum(cF2);

theorem :: AFINSQ_2:56 :: NUMERAL1:2
  for S being Real_Sequence st rF=S|(n+1) holds Sum rF = Partial_Sums(S).n;

theorem :: AFINSQ_2:57  :: NUMERAL1:4
  len rF1 = len rF2 &
  (for i st i in dom rF1 holds rF1.i<=rF2.i) implies
  Sum rF1 <= Sum rF2;

theorem :: AFINSQ_2:58
  Sum (n-->c) = n*c;

theorem :: AFINSQ_2:59 :: STIRL2_1:50
  (for n st n in dom rF holds rF.n <= r) implies
   Sum rF <= len rF * r;

theorem :: AFINSQ_2:60 :: STIRL2_1:51
  (for n st n in dom rF holds rF.n >= r) implies
  Sum rF >= len rF *r;

theorem :: AFINSQ_2:61  :: STIRL2_1:52
  rF is nonnegative-yielding & len rF > 0 &
  (ex x st x in dom rF & rF.x = r) implies Sum rF >= r;

theorem :: AFINSQ_2:62  :: STIRL2_1:53
  rF is nonnegative-yielding implies
  (Sum rF=0 iff (len rF=0 or rF = len rF --> 0));

theorem :: AFINSQ_2:63
  c(#)cF|n = (c(#)cF)|n;

theorem :: AFINSQ_2:64
  c * Sum cF = Sum (c(#)cF);

theorem :: AFINSQ_2:65  :: CARD_FIN:44
   n in dom cF implies Sum (cF|n) + cF.n = Sum (cF|(n+1));

theorem :: AFINSQ_2:66  ::CARD_FIN:13
for f be Function st
  f.y=x & y in dom f holds {y}\/(f|(dom f\{y}))"{x}=f"{x};

theorem :: AFINSQ_2:67  :: CARD_FIN:15
 for x,y being object
 for f be Function st f.y<>x holds (f|(dom f\{y}))"{x}=f"{x};

theorem :: AFINSQ_2:68 :: CATALAN2:45
  rng cF c= {0,c} implies Sum cF = c * card (cF"{c});

theorem :: AFINSQ_2:69 :: CATALAN2:48
  Sum cF = Sum Rev cF;

theorem :: AFINSQ_2:70
  for f be Function,p,q,fp,fq be XFinSequence st
       rng p c= dom f & rng q c= dom f & fp = f*p & fq = f*q
    holds fp ^ fq = f*(p^q);

theorem :: AFINSQ_2:71
  for B1,B2 being finite natural-membered set st
     B1 <N< B2 holds
Sum (SubXFinS(cF,B1\/B2))=Sum (SubXFinS(cF,B1))+Sum(SubXFinS(cF,B2));

:: missing, 2010.05.15, A.T.

theorem :: AFINSQ_2:72
 b is having_a_unity implies b "**" <%>D = the_unity_wrt b;

definition
  let D be set, F be XFinSequence of D^omega;
  func FlattenSeq F -> Element of D^omega means
:: AFINSQ_2:def 10

  ex g being BinOp of D^omega st
  (for p, q being Element of D^omega holds g.(p,q) = p^q) & it = g "**" F;
end;

theorem :: AFINSQ_2:73
  for D being set, d be Element of D^omega holds FlattenSeq <%d%> = d;

theorem :: AFINSQ_2:74
  for D being set holds FlattenSeq <%>(D^omega) = <%>D;

theorem :: AFINSQ_2:75
  for D being set, F,G be XFinSequence of D^omega holds
  FlattenSeq (F ^ G) = FlattenSeq F ^ FlattenSeq G;

theorem :: AFINSQ_2:76
  for D being set, p,q be Element of D^omega holds FlattenSeq <% p,q %> = p ^ q
;

theorem :: AFINSQ_2:77
  for D being set, p,q,r be Element of D^omega holds
  FlattenSeq <% p,q,r %> = p ^ q ^ r;

theorem :: AFINSQ_2:78
  p c= q implies p ^ (q /^ len p) = q;

reserve r,s for XFinSequence;

theorem :: AFINSQ_2:79
  p c= q implies ex r st p^r = q;

theorem :: AFINSQ_2:80
  for p,q being XFinSequence of D st p c= q
    ex r being XFinSequence of D st p^r = q;

theorem :: AFINSQ_2:81
  q c= r implies p^q c= p^r;

theorem :: AFINSQ_2:82
  for D being set, F,G be XFinSequence of D^omega holds
    F c= G implies FlattenSeq F c= FlattenSeq G;

registration let p; let q be non empty XFinSequence;
  cluster p^q -> non empty;
  cluster q^p -> non empty;
end;

theorem :: AFINSQ_2:83
  CutLastLoc(p^<%x%>) = p;

:: generalizes BALLOT_1:1 to empty D
theorem :: AFINSQ_2:84
  for D being set, p being XFinSequence of D, n being Nat
  holds XFS2FS(p|n) = (XFS2FS p)|n & XFS2FS(p/^n) = (XFS2FS p)/^n;

theorem :: AFINSQ_2:85  :: from BALLOT_1:5
  for D being set
  for d be FinSequence of D holds XFS2FS (FS2XFS d) = d;

registration
  let D be set, f be FinSequence of D;
  reduce XFS2FS (FS2XFS f) to f;
end;

theorem :: AFINSQ_2:86
  for D being set, p being FinSequence of D, n being Nat
  holds (FS2XFS p)|n = FS2XFS(p|n) & (FS2XFS p)/^n = FS2XFS(p/^n);

:: analogous theorem of FINSEQ_5:34
theorem :: AFINSQ_2:87
  for D being set, p being one-to-one XFinSequence of D, n being Nat
  holds rng(p|n) misses rng(p/^n);

registration
  cluster finite for Ordinal-Sequence;
end;

registration
  let A be finite Ordinal-Sequence, n be Nat;
  cluster A /^ n -> Ordinal-yielding;
end;