:: Non-contiguous Substrings and One-to-one Finite Sequences
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990-2016 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, FINSEQ_1, XBOOLE_0, ARYTM_3, CARD_1, XXREAL_0, ARYTM_1,
NAT_1, SUBSET_1, TARSKI, RELAT_1, ORDINAL4, FUNCT_1, FINSET_1, FINSEQ_2,
FUNCT_2, CARD_3, FUNCOP_1, FINSEQ_3, EQREL_1, ALG_1, FUNCT_6, SETFAM_1,
FINSEQ_4, ZFMISC_1, FUNCT_5, PARTFUN1, XCMPLX_0, ORDINAL1;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, FINSEQ_1, RELSET_1, PARTFUN1,
FUNCT_2, BINOP_1, FUNCOP_1, FINSEQ_2, FINSET_1, NAT_1, FINSEQOP,
XXREAL_0, CARD_3, FUNCT_3, FUNCT_5, FUNCT_6, EQREL_1;
constructors ENUMSET1, PARTFUN1, WELLORD2, XXREAL_0, REAL_1, NAT_1, INT_1,
FINSEQOP, RELSET_1, CARD_3, DOMAIN_1, CARD_2, EQREL_1, FUNCT_6, BINOP_1,
FUNCT_3, FUNCT_5, FINSEQ_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0,
XREAL_0, NAT_1, INT_1, FINSEQ_1, CARD_1, FINSEQ_2, FUNCOP_1, CARD_3,
CARD_2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve p,q,r for FinSequence;
reserve u,v,x,y,y1,y2,z for object, A,D,X,Y for set;
reserve i,j,k,l,m,n for Nat;
theorem :: FINSEQ_3:1
Seg 3 = {1,2,3};
theorem :: FINSEQ_3:2
Seg 4 = {1,2,3,4};
theorem :: FINSEQ_3:3
Seg 5 = {1,2,3,4,5};
theorem :: FINSEQ_3:4
Seg 6 = {1,2,3,4,5,6};
theorem :: FINSEQ_3:5
Seg 7 = {1,2,3,4,5,6,7};
theorem :: FINSEQ_3:6
Seg 8 = {1,2,3,4,5,6,7,8};
theorem :: FINSEQ_3:7
Seg k = {} iff not k in Seg k;
theorem :: FINSEQ_3:8
not k + 1 in Seg k;
theorem :: FINSEQ_3:9
k <> 0 implies k in Seg(k + n);
theorem :: FINSEQ_3:10
k + n in Seg k implies n = 0;
theorem :: FINSEQ_3:11
k < n implies k + 1 in Seg n;
theorem :: FINSEQ_3:12
k in Seg n & m < k implies k - m in Seg n;
theorem :: FINSEQ_3:13
k - n in Seg k iff n < k;
theorem :: FINSEQ_3:14
Seg k misses {k + 1};
theorem :: FINSEQ_3:15
Seg(k + 1) \ Seg k = {k + 1};
:: Theorem Seg(k + 1) \ {k + 1} = Seg k is
:: proved in RLVECT_1 and has a number 104.
theorem :: FINSEQ_3:16
Seg k <> Seg(k + 1);
theorem :: FINSEQ_3:17
Seg k = Seg(k + n) implies n = 0;
theorem :: FINSEQ_3:18
Seg k c= Seg(k + n);
theorem :: FINSEQ_3:19
Seg k, Seg n are_c=-comparable;
theorem :: FINSEQ_3:20
for y being object st Seg k = {y} holds k = 1 & y = 1;
theorem :: FINSEQ_3:21
Seg k = {x,y} & x <> y implies k = 2 & {x,y} = {1,2};
theorem :: FINSEQ_3:22
x in dom p implies x in dom(p ^ q);
theorem :: FINSEQ_3:23
x in dom p implies x is Element of NAT;
theorem :: FINSEQ_3:24
x in dom p implies x <> 0;
theorem :: FINSEQ_3:25
n in dom p iff 1 <= n & n <= len p;
theorem :: FINSEQ_3:26
n in dom p iff n - 1 is Element of NAT & len p - n is Element of NAT;
::$CT 2
theorem :: FINSEQ_3:29
len p = len q iff dom p = dom q;
theorem :: FINSEQ_3:30
len p <= len q iff dom p c= dom q;
theorem :: FINSEQ_3:31
x in rng p implies 1 in dom p;
theorem :: FINSEQ_3:32
rng p <> {} implies 1 in dom p;
theorem :: FINSEQ_3:33
{} <> <* x,y *>;
theorem :: FINSEQ_3:34
{} <> <* x,y,z *>;
theorem :: FINSEQ_3:35
<* x *> <> <* y,z *>;
theorem :: FINSEQ_3:36
<* u *> <> <* x,y,z *>;
theorem :: FINSEQ_3:37
<* u,v *> <> <* x,y,z *>;
theorem :: FINSEQ_3:38
len r = len p + len q & (for k being Nat st k in dom p holds r.k = p.k) &
(for k being Nat st k in dom q holds r.(len p + k) = q.k)
implies r = p ^ q;
theorem :: FINSEQ_3:39
for A being finite set st A c= Seg k holds len(Sgm A) = card A;
theorem :: FINSEQ_3:40
for A being finite set st A c= Seg k holds dom(Sgm A) = Seg(card A);
theorem :: FINSEQ_3:41
X c= Seg i & k < l & 1 <= n & m <= len(Sgm X) & Sgm(X).m = k &
Sgm(X).n = l implies m < n;
theorem :: FINSEQ_3:42
X c= Seg i & Y c= Seg j implies ((for m,n being Nat
st m in X & n in Y holds m < n) iff Sgm(X \/ Y) = Sgm(X) ^ Sgm(Y));
theorem :: FINSEQ_3:43
Sgm {} = {};
:: The other way of the one above - FINSEQ_1:72.
theorem :: FINSEQ_3:44
0 <> n implies Sgm{n} = <* n *>;
theorem :: FINSEQ_3:45
0 < n & n < m implies Sgm{n,m} = <* n,m *>;
theorem :: FINSEQ_3:46
len(Sgm(Seg k)) = k;
theorem :: FINSEQ_3:47
Sgm(Seg(k + n)) | Seg k = Sgm(Seg k);
theorem :: FINSEQ_3:48
Sgm(Seg k) = idseq k;
theorem :: FINSEQ_3:49
p | Seg n = p iff len p <= n;
theorem :: FINSEQ_3:50
idseq(n + k) | Seg n = idseq n;
theorem :: FINSEQ_3:51
idseq n | Seg m = idseq m iff m <= n;
theorem :: FINSEQ_3:52
idseq n | Seg m = idseq n iff n <= m;
theorem :: FINSEQ_3:53
len p = k + l & q = p | Seg k implies len q = k;
theorem :: FINSEQ_3:54
len p = k + l & q = p | Seg k implies dom q = Seg k;
theorem :: FINSEQ_3:55
len p = k + 1 & q = p | Seg k implies p = q ^ <* p.(k + 1) *>;
theorem :: FINSEQ_3:56
p | X is FinSequence iff ex k being Element of NAT st X /\ dom p = Seg k;
theorem :: FINSEQ_3:57
card((p ^ q) " A) = card(p " A) + card(q " A);
theorem :: FINSEQ_3:58
p " A c= (p ^ q) " A;
definition
let p,A;
func p - A -> FinSequence equals
:: FINSEQ_3:def 1
p * Sgm ((dom p) \ p " A);
end;
theorem :: FINSEQ_3:59
len(p - A) = len p - card(p " A);
theorem :: FINSEQ_3:60
len(p - A) <= len p;
theorem :: FINSEQ_3:61
len(p - A) = len p implies A misses rng p;
theorem :: FINSEQ_3:62
n = len p - card(p " A) implies dom(p - A) = Seg n;
theorem :: FINSEQ_3:63
dom(p - A) c= dom p;
theorem :: FINSEQ_3:64
dom(p - A) = dom p implies A misses rng p;
theorem :: FINSEQ_3:65
rng(p - A) = rng p \ A;
theorem :: FINSEQ_3:66
rng(p - A) c= rng p;
theorem :: FINSEQ_3:67
rng(p - A) = rng p implies A misses rng p;
theorem :: FINSEQ_3:68
p - A = {} iff rng p c= A;
theorem :: FINSEQ_3:69
p - A = p iff A misses rng p;
theorem :: FINSEQ_3:70
p - {x} = p iff not x in rng p;
theorem :: FINSEQ_3:71
p - {} = p;
theorem :: FINSEQ_3:72
p - rng p = {};
theorem :: FINSEQ_3:73
(p ^ q) - A = (p - A) ^ (q - A);
theorem :: FINSEQ_3:74
{} - A = {};
theorem :: FINSEQ_3:75
<* x *> - A = <* x *> iff not x in A;
theorem :: FINSEQ_3:76
<* x *> - A = {} iff x in A;
theorem :: FINSEQ_3:77
<* x,y *> - A = {} iff x in A & y in A;
theorem :: FINSEQ_3:78
x in A & not y in A implies <* x,y *> - A = <* y *>;
theorem :: FINSEQ_3:79
<* x,y *> - A = <* y *> & x <> y implies x in A & not y in A;
theorem :: FINSEQ_3:80
not x in A & y in A implies <* x,y *> - A = <* x *>;
theorem :: FINSEQ_3:81
<* x,y *> - A = <* x *> & x <> y implies not x in A & y in A;
theorem :: FINSEQ_3:82
<* x,y *> - A = <* x,y *> iff not x in A & not y in A;
theorem :: FINSEQ_3:83
len p = k + 1 & q = p | Seg k implies (p.(k + 1) in A iff p - A = q - A);
theorem :: FINSEQ_3:84
len p = k + 1 & q = p | Seg k implies (not p.(k + 1) in A iff p
- A = (q - A) ^ <* p.(k + 1) *>);
theorem :: FINSEQ_3:85
n in dom p implies for B being finite set st B = {k where k is Element
of NAT : k in dom p & k <= n & p.k in A} holds p.n in A or (p - A).(n - card B)
= p.n;
theorem :: FINSEQ_3:86
p is FinSequence of D implies p - A is FinSequence of D;
theorem :: FINSEQ_3:87
p is one-to-one implies p - A is one-to-one;
theorem :: FINSEQ_3:88
p is one-to-one implies len(p - A) = len p - card(A /\ rng p);
theorem :: FINSEQ_3:89
for A being finite set st p is one-to-one & A c= rng p holds len
(p - A) = len p - card A;
theorem :: FINSEQ_3:90
p is one-to-one & x in rng p implies len(p - {x}) = len p - 1;
theorem :: FINSEQ_3:91
rng p misses rng q & p is one-to-one & q is one-to-one iff p ^ q
is one-to-one;
theorem :: FINSEQ_3:92
A c= Seg k implies Sgm A is one-to-one;
theorem :: FINSEQ_3:93
<* x *> is one-to-one;
theorem :: FINSEQ_3:94
x <> y iff <* x,y *> is one-to-one;
theorem :: FINSEQ_3:95
x <> y & y <> z & z <> x iff <* x,y,z *> is one-to-one;
theorem :: FINSEQ_3:96
p is one-to-one & rng p = {x} implies len p = 1;
theorem :: FINSEQ_3:97
p is one-to-one & rng p = {x} implies p = <* x *>;
theorem :: FINSEQ_3:98
p is one-to-one & rng p = {x,y} & x <> y implies len p = 2;
theorem :: FINSEQ_3:99
p is one-to-one & rng p = {x,y} & x <> y implies p = <* x,y *> or p =
<* y,x *>;
theorem :: FINSEQ_3:100
p is one-to-one & rng p = {x,y,z} & <* x,y,z *> is one-to-one
implies len p = 3;
theorem :: FINSEQ_3:101
p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & x <> z implies
len p = 3;
begin :: Addenda
:: from FSM_1
theorem :: FINSEQ_3:102
for D being non empty set, df being FinSequence of D holds df is non
empty implies ex d being Element of D, df1 being FinSequence of D st d = df.1 &
df = <*d*>^df1;
theorem :: FINSEQ_3:103
for df being FinSequence, d being object holds
i in dom df implies (<*d*>^df).(i+1) = df.i;
:: from MATRIX_2, 2005.11.16, A.T.
definition
let i be natural Number;
let p be FinSequence;
func Del(p,i) -> FinSequence equals
:: FINSEQ_3:def 2
p * Sgm ((dom p) \ {i});
end;
theorem :: FINSEQ_3:104
for p being FinSequence holds
(i in dom p implies ex m being Nat st len p = m + 1 & len Del(p,i) = m) &
(not i in dom p implies Del(p,i) = p);
theorem :: FINSEQ_3:105
for D being non empty set for p being FinSequence of D holds
Del(p,i) is FinSequence of D;
:: from MATRLIN, 2005.11.16, A.T.
theorem :: FINSEQ_3:106
for p be FinSequence holds rng Del(p,i) c= rng p;
:: from GOBOARD1, 2005.11.16, A.T.
theorem :: FINSEQ_3:107
n = m + 1 & i in Seg n implies len Sgm(Seg n \ {i}) = m;
reserve J for Nat;
theorem :: FINSEQ_3:108
for i,k,m,n being Nat st n=m+1 & k in Seg n & i in Seg m holds
(1<=i & i 0 & A = {} iff i-tuples_on A = {};
:: from AMISTD_2, 2009.09.08, A.T.
registration
let i be Nat, D be set;
cluster i-tuples_on D -> with_common_domain;
end;
registration
let i be Nat, D be set;
cluster i-tuples_on D -> product-like;
end;
begin :: Moved from ALG_1, 2010.03.17
reserve n for Nat;
theorem :: FINSEQ_3:120
for D1,D2 be non empty set, p be FinSequence of D1, f be Function
of D1,D2 holds dom(f*p) = dom p & len (f*p) = len p & for n being Nat st n in
dom (f*p) holds (f*p).n = f.(p.n);
definition
let D be non empty set, R be Relation of D;
func ExtendRel(R) -> Relation of D* means
:: FINSEQ_3:def 3
for x,y be FinSequence of D
holds [x,y] in it iff len x = len y & for n st n in dom x holds [x.n,y.n] in R;
end;
theorem :: FINSEQ_3:121
for D be non empty set holds ExtendRel(id D) = id (D*);
definition
let D be non empty set, R be Equivalence_Relation of D;
let y be FinSequence of Class(R), x be FinSequence of D;
pred x is_representatives_FS y means
:: FINSEQ_3:def 4
len x = len y & for n st n in dom x holds Class(R,x.n) = y.n;
end;
theorem :: FINSEQ_3:122
for D be non empty set, R be Equivalence_Relation of D, y be
FinSequence of Class(R) ex x be FinSequence of D st x is_representatives_FS y
;
:: from FUNCT_6, 2011.04.18, A.T.
reserve x,y,y1,y2,z,a,b for object, X,Y,Z,V1,V2 for set,
f,g,h,h9,f1,f2 for Function,
i for Nat,
P for Permutation of X,
D,D1,D2,D3 for non empty set,
d1 for Element of D1,
d2 for Element of D2,
d3 for Element of D3;
theorem :: FINSEQ_3:123
x in product <*X*> iff ex y st y in X & x = <*y*>;
theorem :: FINSEQ_3:124
z in product <*X,Y*> iff ex x,y st x in X & y in Y & z = <*x,y*>;
theorem :: FINSEQ_3:125
a in product <*X,Y,Z*> iff ex x,y,z st x in X & y in Y & z in Z &
a = <*x,y,z*>;
theorem :: FINSEQ_3:126
product <*D*> = 1-tuples_on D;
theorem :: FINSEQ_3:127
product <*D1,D2*> = the set of all <*d1,d2*>;
theorem :: FINSEQ_3:128
product <*D,D*> = 2-tuples_on D;
theorem :: FINSEQ_3:129
product <*D1,D2,D3*> = the set of all <*d1,d2,d3*>;
theorem :: FINSEQ_3:130
product <*D,D,D*> = 3-tuples_on D;
theorem :: FINSEQ_3:131
for D being set holds product (i |-> D) = i-tuples_on D;
registration
let f be Function;
cluster <*f*> -> Function-yielding;
let g be Function;
cluster <*f,g*> -> Function-yielding;
let h be Function;
cluster <*f,g,h*> -> Function-yielding;
end;
theorem :: FINSEQ_3:132
doms <*f*> = <*dom f*> & rngs <*f*> = <*rng f*>;
theorem :: FINSEQ_3:133
doms <*f,g*> = <*dom f, dom g*> & rngs <*f,g*> = <*rng f, rng g *>;
theorem :: FINSEQ_3:134
doms <*f,g,h*> = <*dom f, dom g, dom h*> & rngs <*f,g,h*> = <*rng f,
rng g, rng h*>;
theorem :: FINSEQ_3:135
Union <*X*> = X & meet <*X*> = X;
theorem :: FINSEQ_3:136
Union <*X,Y*> = X \/ Y & meet <*X,Y*> = X /\ Y;
theorem :: FINSEQ_3:137
Union <*X,Y,Z*> = X \/ Y \/ Z & meet <*X,Y,Z*> = X /\ Y /\ Z;
theorem :: FINSEQ_3:138
x in dom f implies <*f*>..(1,x) = f.x & <*f,g*>..(1,x) = f.x & <*f,g,h
*>..(1,x) = f.x;
theorem :: FINSEQ_3:139
x in dom g implies <*f,g*>..(2,x) = g.x & <*f,g,h*>..(2,x) = g.x;
theorem :: FINSEQ_3:140
x in dom h implies <*f,g,h*>..(3,x) = h.x;
theorem :: FINSEQ_3:141
dom <:<*h*>:> = dom h & for x st x in dom h holds <:<*h*>:>.x = <*h.x *>;
theorem :: FINSEQ_3:142
dom <:<*f1,f2*>:> = dom f1 /\ dom f2 & for x st x in dom f1 /\
dom f2 holds <:<*f1,f2*>:>.x = <*f1.x,f2.x*>;
theorem :: FINSEQ_3:143
dom Frege<*h*> = product <*dom h*> & rng Frege<*h*> = product <*rng h
*> & for x st x in dom h holds (Frege<*h*>).<*x*> = <*h.x*>;
theorem :: FINSEQ_3:144
dom Frege<*f1,f2*> = product <*dom f1, dom f2*> & rng Frege<*f1,
f2*> = product <*rng f1, rng f2*> & for x,y st x in dom f1 & y in dom f2 holds
(Frege<*f1,f2*>).<*x,y*> = <*f1.x, f2.y*>;
theorem :: FINSEQ_3:145
x in dom f1 & x in dom f2 implies for y1,y2 holds <:f1,f2:>.x = [y1,y2
] iff <:<*f1,f2*>:>.x = <*y1,y2*>;
theorem :: FINSEQ_3:146
x in dom f1 & y in dom f2 implies for y1,y2 holds [:f1,f2:].(x,y) = [
y1,y2] iff (Frege<*f1,f2*>).<*x,y*> = <*y1,y2*>;
theorem :: FINSEQ_3:147
Funcs(<*X*>,Y) = <*Funcs(X,Y)*>;
theorem :: FINSEQ_3:148
Funcs(<*X,Y*>,Z) = <*Funcs(X,Z), Funcs(Y,Z)*>;
theorem :: FINSEQ_3:149
Funcs(X,<*Y*>) = <*Funcs(X,Y)*>;
theorem :: FINSEQ_3:150
Funcs(X,<*Y,Z*>) = <*Funcs(X,Y), Funcs(X,Z)*>;
::from JORDAN2C, 2011.07.03, A.T.
theorem :: FINSEQ_3:151
for f being FinSequence st rng f={x,y} & len f=2 holds f.1=x & f.
2=y or f.1=y & f.2=x;
:: from GLIB_001, 2011.07.30, A.T.
theorem :: FINSEQ_3:152
for X being set, k being Element of NAT st X c= Seg k holds for m
,n being Element of NAT st m in dom (Sgm X) & n = (Sgm X).m holds m <= n;
registration
let i be Nat; let D be finite set;
cluster i-tuples_on D -> finite;
end;
theorem :: FINSEQ_3:153
for p being m-element FinSequence holds len p = m;
theorem :: FINSEQ_3:154
for p being n-element FinSequence, q being FinSequence
holds (p^q).1 = p.1 & ... & (p^q).n = p.n;
reserve n for Nat;
theorem :: FINSEQ_3:155
for p being n-element FinSequence,
q being m-element FinSequence
holds (p^q).(n+(1 qua Nat)) = q.1 & ... & (p^q).(n+m) = q.m;
theorem :: FINSEQ_3:156
for p being FinSequence, k being Nat st k in dom p
for i being Nat st 1 <= i & i <= k holds i in dom p;
:: from PNPROC_1, 2012.02.20, A.T.
theorem :: FINSEQ_3:157
for q being FinSubsequence st q = {[i,x]} holds Seq q = <*x*>;
theorem :: FINSEQ_3:158
for p being FinSubsequence holds card p = len Seq p;
theorem :: FINSEQ_3:159
for q being FinSubsequence st Seq q = <*x*>
ex i being Element of NAT st q = {[i,x]};