The abstract of the Mizar article:

Finite Sequences and Tuples of Elements of a Non-empty Sets

by

Czeslaw Bylinski

Received March 1, 1990

MML identifier: FINSEQ_2

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDINAL2, ARYTM, FINSEQ_1, SQUARE_1, BOOLE, ARYTM_1, FUNCT_1,
      RELAT_1, FUNCT_2, FUNCOP_1, PARTFUN1, TARSKI, FINSEQ_2;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2,
      NUMBERS, XCMPLX_0, XREAL_0, DOMAIN_1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1,
      PARTFUN1, FUNCT_2, FUNCT_3, FINSEQ_1, BINOP_1, FUNCOP_1;
 constructors DOMAIN_1, NAT_1, SQUARE_1, FUNCT_3, FINSEQ_1, BINOP_1, FUNCOP_1,
      PARTFUN1, MEMBERED, RELAT_2, XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, FINSEQ_1, RELSET_1, XREAL_0, FUNCOP_1, FUNCT_2,
      NAT_1, MEMBERED, ZFMISC_1, PARTFUN1, XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve i,j,l for Nat;
reserve k for natural number;
reserve A,a,b,x,x1,x2,x3 for set;
reserve D,D',E for non empty set;
reserve d,d1,d2,d3 for Element of D;
reserve d',d1',d2',d3' for Element of D';
reserve p,q,r for FinSequence;

:: Auxiliary theorems

theorem :: FINSEQ_2:1
    min(i,j) is Nat & max(i,j) is Nat;

theorem :: FINSEQ_2:2
   l = min(i,j) implies Seg i /\ Seg j = Seg l;

theorem :: FINSEQ_2:3
   i <= j implies max(0,i-j) = 0;

theorem :: FINSEQ_2:4
   j <= i implies max(0,i-j) = i-j;

theorem :: FINSEQ_2:5
     max(0,i-j) is Nat;

theorem :: FINSEQ_2:6
   min(0,i) = 0 & min(i,0) = 0 & max(0,i) = i & max(i,0) = i;

:: Non-empty Segments of Natural Numbers

canceled;

theorem :: FINSEQ_2:8
     i in Seg (l+1) implies i in Seg l or i = l+1;

theorem :: FINSEQ_2:9
     i in Seg l implies i in Seg(l+j);

:: Additional propositions related to Finite Sequences


theorem :: FINSEQ_2:10
  len p = i & len q = i & (for j st j in Seg i holds p.j = q.j)
    implies p = q;

theorem :: FINSEQ_2:11
   b in rng p implies ex i st i in dom p & p.i = b;

canceled;

theorem :: FINSEQ_2:13
   for D being set
   for p being FinSequence of D st i in dom p holds p.i in D;

theorem :: FINSEQ_2:14
  for D being set holds
   (for i st i in dom p holds p.i in D) implies p is FinSequence of D;

theorem :: FINSEQ_2:15
   <*d1,d2*> is FinSequence of D;

theorem :: FINSEQ_2:16
   <*d1,d2,d3*> is FinSequence of D;

canceled;

theorem :: FINSEQ_2:18
   i in dom p implies i in dom(p^q);

theorem :: FINSEQ_2:19
   len(p^<*a*>) = len p + 1;

theorem :: FINSEQ_2:20
     p^<*a*> = q^<*b*> implies p = q & a = b;

theorem :: FINSEQ_2:21
   len p = i + 1 implies ex q,a st p = q^<*a*>;

theorem :: FINSEQ_2:22
   for p being FinSequence of D
    st len p <> 0 ex q being (FinSequence of D),d st p = q^<*d*>;

theorem :: FINSEQ_2:23
   q = p|(Seg i) & len p <= i implies p = q;

theorem :: FINSEQ_2:24
     q = p|(Seg i) implies len q = min(i,len p);

theorem :: FINSEQ_2:25
   len r = i+j implies ex p,q st len p = i & len q = j & r = p^q;

theorem :: FINSEQ_2:26
   for r being FinSequence of D st len r = i+j
    ex p,q being FinSequence of D st len p = i & len q = j & r = p^q;

scheme SeqLambdaD{i()->Nat,D()->non empty set,F(set)->Element of D()}:
  ex z being FinSequence of D() st len z = i() &
   for j st j in Seg i() holds z.j = F(j);

scheme IndSeqD{D()->non empty set, P[set]}:
  for p being FinSequence of D() holds P[p]
 provided
 P[<*> D()] and
 for p being FinSequence of D() for x being Element of D()
      st P[p] holds P[p^<*x*>];

theorem :: FINSEQ_2:27
   for D' being non empty Subset of D for p being FinSequence of D'
    holds p is FinSequence of D;

theorem :: FINSEQ_2:28
   for f being Function of Seg i, D holds f is FinSequence of D;

canceled;

theorem :: FINSEQ_2:30
     for p being FinSequence of D holds p is Function of dom p, D;

theorem :: FINSEQ_2:31
     for f being Function of NAT,D holds f|(Seg i) is FinSequence of D;

theorem :: FINSEQ_2:32
     for f being Function of NAT,D st q = f|(Seg i) holds len q = i;

theorem :: FINSEQ_2:33
   for f being Function st rng p c= dom f & q = f*p holds len q = len p;

theorem :: FINSEQ_2:34
  D = Seg i implies
   for p being FinSequence for q being FinSequence of D st i <= len p
    holds p*q is FinSequence;

theorem :: FINSEQ_2:35
    D = Seg i implies
   for p being FinSequence of D' for q being FinSequence of D st i <= len p
    holds p*q is FinSequence of D';

theorem :: FINSEQ_2:36
   for A,D being set
   for p being FinSequence of A for f being Function of A,D
    holds f*p is FinSequence of D;

theorem :: FINSEQ_2:37
   for p being FinSequence of A for f being Function of A,D'
    st q = f*p holds len q = len p;

theorem :: FINSEQ_2:38
     for f being Function of A,D' holds f*(<*>A) = <*>D';

theorem :: FINSEQ_2:39
     for p being FinSequence of D for f being Function of D,D'
    st p = <*x1*> holds f*p = <*f.x1*>;

theorem :: FINSEQ_2:40
   for p being FinSequence of D for f being Function of D,D'
    st p = <*x1,x2*> holds f*p = <*f.x1,f.x2*>;

theorem :: FINSEQ_2:41
   for p being FinSequence of D for f being Function of D,D'
    st p = <*x1,x2,x3*> holds f*p = <*f.x1,f.x2,f.x3*>;

theorem :: FINSEQ_2:42
   for f being Function of Seg i,Seg j
     st (j = 0 implies i = 0) & j <= len p holds p*f is FinSequence;

theorem :: FINSEQ_2:43
   for f being Function of Seg i,Seg i st i <= len p holds p*f is FinSequence;

theorem :: FINSEQ_2:44
     for f being Function of dom p,dom p holds p*f is FinSequence;

theorem :: FINSEQ_2:45
   for f being Function of Seg i,Seg i st rng f = Seg i & i <= len p & q = p*f
    holds len q = i;

theorem :: FINSEQ_2:46
   for f being Function of dom p,dom p st rng f = dom p & q = p*f
    holds len q = len p;

theorem :: FINSEQ_2:47
   for f being Permutation of Seg i st i <= len p & q = p*f holds len q = i;

theorem :: FINSEQ_2:48
     for f being Permutation of dom p st q = p*f holds len q = len p;

theorem :: FINSEQ_2:49
   for p being FinSequence of D for f being Function of Seg i,Seg j
    st (j = 0 implies i = 0) & j <= len p holds p*f is FinSequence of D;

theorem :: FINSEQ_2:50
   for p being FinSequence of D for f being Function of Seg i,Seg i
    st i <= len p holds p*f is FinSequence of D;

theorem :: FINSEQ_2:51
   for p being FinSequence of D for f being Function of dom p,dom p
    holds p*f is FinSequence of D;

theorem :: FINSEQ_2:52
   id Seg k is FinSequence of NAT;

definition let i be natural number;
  func idseq i -> FinSequence equals
:: FINSEQ_2:def 1
  id Seg i;
end;

canceled;

theorem :: FINSEQ_2:54
   dom idseq k = Seg k;

theorem :: FINSEQ_2:55
   len idseq k = k;

theorem :: FINSEQ_2:56
   j in Seg i implies (idseq i).j = j;

theorem :: FINSEQ_2:57
     i<>0 implies for k being Element of Seg i holds (idseq i).k = k;

theorem :: FINSEQ_2:58
     idseq 0 = {};

theorem :: FINSEQ_2:59
   idseq 1 = <*1*>;

theorem :: FINSEQ_2:60
   idseq (i+1) = (idseq i) ^ <*i+1*>;

theorem :: FINSEQ_2:61
   idseq 2 = <*1,2*>;

theorem :: FINSEQ_2:62
     idseq 3 = <*1,2,3*>;

theorem :: FINSEQ_2:63
     p*(idseq k) = p|(Seg k);

theorem :: FINSEQ_2:64
   len p <= k implies p*(idseq k) = p;

theorem :: FINSEQ_2:65
     idseq k is Permutation of Seg k;

theorem :: FINSEQ_2:66
  (Seg k) --> a is FinSequence;

definition let i be natural number, a be set;
  func i |-> a -> FinSequence equals
:: FINSEQ_2:def 2
  Seg i --> a;
end;

canceled;

theorem :: FINSEQ_2:68
   dom(k |-> a) = Seg k;

theorem :: FINSEQ_2:69
   len(k |-> a) = k;

theorem :: FINSEQ_2:70
   b in Seg k implies (k |-> a).b = a;

theorem :: FINSEQ_2:71
     k<>0 implies for w being Element of Seg k holds (k |-> d).w = d;

theorem :: FINSEQ_2:72
   0 |-> a = {};

theorem :: FINSEQ_2:73
   1 |-> a = <*a*>;

theorem :: FINSEQ_2:74
   (i+1) |-> a = (i |-> a) ^ <*a*>;

theorem :: FINSEQ_2:75
   2 |-> a = <*a,a*>;

theorem :: FINSEQ_2:76
     3 |-> a = <*a,a,a*>;

theorem :: FINSEQ_2:77
   k |-> d is FinSequence of D;

theorem :: FINSEQ_2:78
   for F being Function st [:rng p,rng q:] c= dom F
    holds F.:(p,q) is FinSequence;

theorem :: FINSEQ_2:79
   for F being Function st [:rng p,rng q:] c= dom F & r = F.:(p,q)
    holds len r = min(len p,len q);

theorem :: FINSEQ_2:80
   for F being Function st [:{a},rng p:] c= dom F
    holds F[;](a,p) is FinSequence;

theorem :: FINSEQ_2:81
   for F being Function st [:{a},rng p:] c= dom F & r = F[;](a,p)
    holds len r = len p;

theorem :: FINSEQ_2:82
   for F being Function st [:rng p,{a}:] c= dom F
    holds F[:](p,a) is FinSequence;

theorem :: FINSEQ_2:83
   for F being Function st [:rng p,{a}:] c= dom F & r = F[:](p,a)
    holds len r = len p;

theorem :: FINSEQ_2:84
   for F being Function of [:D,D':],E
     for p being FinSequence of D for q being FinSequence of D'
    holds F.:(p,q) is FinSequence of E;

theorem :: FINSEQ_2:85
   for F being Function of [:D,D':],E
    for p being FinSequence of D for q being FinSequence of D'
     st r = F.:(p,q) holds len r = min(len p,len q);

theorem :: FINSEQ_2:86
   for F being Function of [:D,D':],E
    for p being FinSequence of D for q being FinSequence of D'
     st len p = len q & r = F.:(p,q) holds len r = len p & len r = len q;

theorem :: FINSEQ_2:87
     for F being Function of [:D,D':],E
    for p being FinSequence of D for p' being FinSequence of D'
     holds F.:(<*>D,p') = <*>E & F.:(p,<*>D') = <*>E;

theorem :: FINSEQ_2:88
     for F being Function of [:D,D':],E
    for p being FinSequence of D for q being FinSequence of D'
     st p = <*d1*> & q = <*d1'*> holds F.:(p,q) = <*F.(d1,d1')*>;

theorem :: FINSEQ_2:89
     for F being Function of [:D,D':],E
    for p being FinSequence of D for q being FinSequence of D'
     st p = <*d1,d2*> & q = <*d1',d2'*>
    holds F.:(p,q) = <*F.(d1,d1'),F.(d2,d2')*>;

theorem :: FINSEQ_2:90
     for F being Function of [:D,D':],E
    for p being FinSequence of D for q being FinSequence of D'
      st p = <*d1,d2,d3*> & q = <*d1',d2',d3'*>
     holds F.:(p,q) = <*F.(d1,d1'),F.(d2,d2'),F.(d3,d3')*>;

theorem :: FINSEQ_2:91
   for F being Function of [:D,D':],E for p being FinSequence of D'
    holds F[;](d,p) is FinSequence of E;

theorem :: FINSEQ_2:92
   for F being Function of [:D,D':],E for p being FinSequence of D'
     st r = F[;](d,p) holds len r = len p;

theorem :: FINSEQ_2:93
     for F being Function of [:D,D':],E holds F[;](d,<*>D') = <*>E;

theorem :: FINSEQ_2:94
     for F being Function of [:D,D':],E for p being FinSequence of D'
    st p = <*d1'*> holds F[;](d,p) = <*F.(d,d1')*>;

theorem :: FINSEQ_2:95
     for F being Function of [:D,D':],E for p being FinSequence of D'
    st p = <*d1',d2'*> holds F[;](d,p) = <*F.(d,d1'),F.(d,d2')*>;

theorem :: FINSEQ_2:96
     for F being Function of [:D,D':],E for p being FinSequence of D'
     st p = <*d1',d2',d3'*>
    holds F[;](d,p) = <*F.(d,d1'),F.(d,d2'),F.(d,d3')*>;

theorem :: FINSEQ_2:97
   for F being Function of [:D,D':],E for p being FinSequence of D
    holds F[:](p,d') is FinSequence of E;

theorem :: FINSEQ_2:98
   for F being Function of [:D,D':],E for p being FinSequence of D
    st r = F[:](p,d') holds len r = len p;

theorem :: FINSEQ_2:99
     for F being Function of [:D,D':],E holds F[:](<*>D,d') = <*>E;

theorem :: FINSEQ_2:100
     for F being Function of [:D,D':],E for p being FinSequence of D
    st p = <*d1*> holds F[:](p,d') = <*F.(d1,d')*>;

theorem :: FINSEQ_2:101
     for F being Function of [:D,D':],E for p being FinSequence of D
    st p = <*d1,d2*> holds F[:](p,d') = <*F.(d1,d'),F.(d2,d')*>;

theorem :: FINSEQ_2:102
     for F being Function of [:D,D':],E for p being FinSequence of D
    st p = <*d1,d2,d3*> holds F[:](p,d') = <*F.(d1,d'),F.(d2,d'),F.(d3,d')*>;

:: T u p l e s

definition let D be set;
  mode FinSequenceSet of D -> set means
:: FINSEQ_2:def 3
 a in it implies a is FinSequence of D;
end;

definition let D be set;
 cluster non empty FinSequenceSet of D;
end;

definition let D be set;
  mode FinSequence-DOMAIN of D is non empty FinSequenceSet of D;
end;

canceled;

theorem :: FINSEQ_2:104
  for D being set holds D* is FinSequence-DOMAIN of D;

definition let D be set;
 redefine func D* -> FinSequence-DOMAIN of D;
end;

theorem :: FINSEQ_2:105
     for D being set, D' being FinSequence-DOMAIN of D holds D' c= D*;

definition let D be set, S be FinSequence-DOMAIN of D;
 redefine mode Element of S -> FinSequence of D;
end;

canceled;

theorem :: FINSEQ_2:107
     for D' being non empty Subset of D, S being FinSequence-DOMAIN of D'
    holds S is FinSequence-DOMAIN of D;

reserve s for Element of D*;

definition let i be natural number; let D be set;
 func i-tuples_on D -> FinSequenceSet of D equals
:: FINSEQ_2:def 4
  { s where s is Element of D*: len s = i };
end;

definition let i be natural number, D;
 cluster i-tuples_on D -> non empty;
end;

canceled;

theorem :: FINSEQ_2:109
   for z being Element of i-tuples_on D holds len z = i;

theorem :: FINSEQ_2:110
   for D be set, z being FinSequence of D holds
    z is Element of (len z)-tuples_on D;

theorem :: FINSEQ_2:111
     i-tuples_on D = Funcs(Seg i,D);

theorem :: FINSEQ_2:112
  for D being set holds 0-tuples_on D = { <*>D };

theorem :: FINSEQ_2:113
   for D be set, z being Element of 0-tuples_on D holds z = <*>D;

theorem :: FINSEQ_2:114
    for D be set holds <*>D is Element of 0-tuples_on D;

theorem :: FINSEQ_2:115
    for z being Element of 0-tuples_on D
   for t being Element of i-tuples_on D holds z^t = t & t^z = t;

theorem :: FINSEQ_2:116
   1-tuples_on D = { <*d*>: not contradiction };

theorem :: FINSEQ_2:117
   for z being Element of 1-tuples_on D ex d st z = <*d*>;

theorem :: FINSEQ_2:118
     <*d*> is Element of 1-tuples_on D;

theorem :: FINSEQ_2:119
   2-tuples_on D = { <*d1,d2*>: not contradiction };

theorem :: FINSEQ_2:120
     for z being Element of 2-tuples_on D ex d1,d2 st z = <*d1,d2*>;

theorem :: FINSEQ_2:121
     <*d1,d2*> is Element of 2-tuples_on D;

theorem :: FINSEQ_2:122
   3-tuples_on D = { <*d1,d2,d3*>: not contradiction };

theorem :: FINSEQ_2:123
     for z being Element of 3-tuples_on D ex d1,d2,d3 st z = <*d1,d2,d3*>;

theorem :: FINSEQ_2:124
     <*d1,d2,d3*> is Element of 3-tuples_on D;

theorem :: FINSEQ_2:125
   (i+j)-tuples_on D = {z^t where z is (Element of i-tuples_on D),
                            t is Element of j-tuples_on D: not contradiction};

theorem :: FINSEQ_2:126
   for s being Element of (i+j)-tuples_on D
    ex z being (Element of i-tuples_on D), t being Element of j-tuples_on D
     st s = z^t;

theorem :: FINSEQ_2:127
     for z being Element of i-tuples_on D for t being Element of j-tuples_on D
    holds z^t is Element of (i+j)-tuples_on D;

theorem :: FINSEQ_2:128
     D* = union {i-tuples_on D: not contradiction};

theorem :: FINSEQ_2:129
     for D' being non empty Subset of D for z being Element of i-tuples_on D'
    holds z is Element of i-tuples_on D;

theorem :: FINSEQ_2:130
     i-tuples_on D = j-tuples_on D implies i = j;

theorem :: FINSEQ_2:131
     idseq i is Element of i-tuples_on NAT;

theorem :: FINSEQ_2:132
     i |-> d is Element of i-tuples_on D;

theorem :: FINSEQ_2:133
     for z being Element of i-tuples_on D for f being Function of D,D'
    holds f*z is Element of i-tuples_on D';

theorem :: FINSEQ_2:134
   for z being Element of i-tuples_on D for f being Function of Seg i,Seg i
    st rng f = Seg i holds z*f is Element of i-tuples_on D;

theorem :: FINSEQ_2:135
     for z being Element of i-tuples_on D for f being Permutation of Seg i
     holds z*f is Element of i-tuples_on D;

theorem :: FINSEQ_2:136
     for z being Element of i-tuples_on D for d holds (z^<*d*>).(i+1) = d;

theorem :: FINSEQ_2:137
     for z being Element of (i+1)-tuples_on D
    ex t being (Element of i-tuples_on D), d st z = t^<*d*>;

theorem :: FINSEQ_2:138
     for z being Element of i-tuples_on D holds z*(idseq i) = z;

theorem :: FINSEQ_2:139
     for z1,z2 being Element of i-tuples_on D
     st for j st j in Seg i holds z1.j = z2.j
    holds z1 = z2;

theorem :: FINSEQ_2:140
     for F being Function of [:D,D':],E
    for z1 being Element of i-tuples_on D
     for z2 being Element of i-tuples_on D'
      holds F.:(z1,z2) is Element of i-tuples_on E;

theorem :: FINSEQ_2:141
    for F being Function of [:D,D':],E for z being Element of i-tuples_on D'
    holds F[;](d,z) is Element of i-tuples_on E;

theorem :: FINSEQ_2:142
    for F being Function of [:D,D':],E for z being Element of i-tuples_on D
    holds F[:](z,d') is Element of i-tuples_on E;

theorem :: FINSEQ_2:143
     (i+j)|->x = (i|->x)^(j|->x);

:: Addendum, 2002.07.08

theorem :: FINSEQ_2:144
   for i, D
  for x being Element of i-tuples_on D
  holds dom x = Seg i;

theorem :: FINSEQ_2:145
    for f being Function,
      x, y being set st x in dom f & y in dom f holds
    f*<*x,y*> = <*f.x,f.y*>;

theorem :: FINSEQ_2:146
    for f being Function,
      x, y, z being set st x in dom f & y in dom f & z in dom f holds
    f*<*x,y,z*> = <*f.x,f.y,f.z*>;

theorem :: FINSEQ_2:147
    rng <*x1,x2*> = {x1,x2};

theorem :: FINSEQ_2:148
    rng <*x1,x2,x3*> = {x1,x2,x3};