Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Non-contiguous Substrings and One-to-one Finite Sequences

by
Wojciech A. Trybulec

Received April 8, 1990

MML identifier: FINSEQ_3
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_1, BOOLE, ARYTM_1, ZFMISC_1, RELAT_1, INT_1, FUNCT_1,
FINSET_1, CARD_1, TARSKI, FINSEQ_2;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
FINSEQ_1, RELAT_1, FUNCT_1, FINSEQ_2, FINSET_1, CARD_1, NAT_1, INT_1;
constructors FUNCT_2, DOMAIN_1, FINSEQ_2, REAL_1, WELLORD2, NAT_1, INT_1,
MEMBERED, PARTFUN1, XBOOLE_0;
clusters FINSEQ_1, FUNCT_1, INT_1, FINSET_1, RELSET_1, XREAL_0, MEMBERED,
ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;

begin

reserve p,q,r for FinSequence;
reserve u,v,x,y,y1,y2,z,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;

canceled;

theorem :: FINSEQ_3:9
not k + 1 in Seg k;

theorem :: FINSEQ_3:10
k <> 0 implies k in Seg(k + n);

theorem :: FINSEQ_3:11
k + n in Seg k implies n = 0;

theorem :: FINSEQ_3:12
k < n implies k + 1 in Seg n;

theorem :: FINSEQ_3:13
k in Seg n & m < k implies k - m in Seg n;

theorem :: FINSEQ_3:14
k - n in Seg k iff n < k;

theorem :: FINSEQ_3:15
Seg k misses {k + 1};

theorem :: FINSEQ_3:16
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:17
Seg k <> Seg(k + 1);

theorem :: FINSEQ_3:18
Seg k = Seg(k + n) implies n = 0;

theorem :: FINSEQ_3:19
Seg k c= Seg(k + n);

theorem :: FINSEQ_3:20
Seg k, Seg n are_c=-comparable;

canceled;

theorem :: FINSEQ_3:22
Seg k = {y} implies k = 1 & y = 1;

theorem :: FINSEQ_3:23
Seg k = {x,y} & x <> y implies k = 2 & {x,y} = {1,2};

theorem :: FINSEQ_3:24
x in dom p implies x in dom(p ^ q);

theorem :: FINSEQ_3:25
x in dom p implies x is Nat;

theorem :: FINSEQ_3:26
x in dom p implies x <> 0;

theorem :: FINSEQ_3:27
n in dom p iff 1 <= n & n <= len p;

theorem :: FINSEQ_3:28
n in dom p iff n - 1 is Nat & len p - n is Nat;

theorem :: FINSEQ_3:29
dom<* x,y *> = Seg(2);

theorem :: FINSEQ_3:30
dom<* x,y,z *> = Seg(3);

theorem :: FINSEQ_3:31
len p = len q iff dom p = dom q;

theorem :: FINSEQ_3:32
len p <= len q iff dom p c= dom q;

theorem :: FINSEQ_3:33
x in rng p implies 1 in dom p;

theorem :: FINSEQ_3:34
rng p <> {} implies 1 in dom p;

canceled 3;

theorem :: FINSEQ_3:38
{} <> <* x,y *>;

theorem :: FINSEQ_3:39
{} <> <* x,y,z *>;

theorem :: FINSEQ_3:40
<* x *> <> <* y,z *>;

theorem :: FINSEQ_3:41
<* u *> <> <* x,y,z *>;

theorem :: FINSEQ_3:42
<* u,v *> <> <* x,y,z *>;

theorem :: FINSEQ_3:43
len r = len p + len q &
(for k st k in dom p holds r.k = p.k) &
(for k st k in dom q holds r.(len p + k) = q.k) implies r = p ^ q;

theorem :: FINSEQ_3:44
for A being finite set st A c= Seg k
holds len(Sgm A) = card A;

theorem :: FINSEQ_3:45
for A being finite set st A c= Seg k
holds dom(Sgm A) = Seg(card A);

theorem :: FINSEQ_3:46
X c= Seg i & k < l & 1 <= n & m <= len(Sgm X) &
Sgm(X).m = k & Sgm(X).n = l implies m < n;

canceled;

theorem :: FINSEQ_3:48
X c= Seg i & Y c= Seg j implies
((for m,n st m in X & n in Y holds m < n) iff Sgm(X \/ Y) = Sgm(X) ^ Sgm(Y));

theorem :: FINSEQ_3:49
Sgm {} = {};

:: The other way of the one above - FINSEQ_1:72.

theorem :: FINSEQ_3:50
0 <> n implies Sgm{n} = <* n *>;

theorem :: FINSEQ_3:51
0 < n & n < m implies Sgm{n,m} = <* n,m *>;

theorem :: FINSEQ_3:52
len(Sgm(Seg k)) = k;

theorem :: FINSEQ_3:53
Sgm(Seg(k + n)) | Seg k = Sgm(Seg k);

theorem :: FINSEQ_3:54
Sgm(Seg k) = idseq k;

theorem :: FINSEQ_3:55
p | Seg n = p iff len p <= n;

theorem :: FINSEQ_3:56
idseq(n + k) | Seg n = idseq n;

theorem :: FINSEQ_3:57
idseq n | Seg m = idseq m iff m <= n;

theorem :: FINSEQ_3:58
idseq n | Seg m = idseq n iff n <= m;

theorem :: FINSEQ_3:59
len p = k + l & q = p | Seg k implies len q = k;

theorem :: FINSEQ_3:60
len p = k + l & q = p | Seg k implies dom q = Seg k;

theorem :: FINSEQ_3:61
len p = k + 1 & q = p | Seg k implies p = q ^ <* p.(k + 1) *>;

theorem :: FINSEQ_3:62
p | X is FinSequence iff ex k st X /\ dom p = Seg k;

definition let p be FinSequence, A be set;
cluster p"A -> finite;
end;

theorem :: FINSEQ_3:63
card((p ^ q) " A) = card(p " A) + card(q " A);

theorem :: FINSEQ_3:64
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;

canceled;

theorem :: FINSEQ_3:66
len(p - A) = len p - card(p " A);

theorem :: FINSEQ_3:67
len(p - A) <= len p;

theorem :: FINSEQ_3:68
len(p - A) = len p implies A misses rng p;

theorem :: FINSEQ_3:69
n = len p - card(p " A) implies dom(p - A) = Seg n;

theorem :: FINSEQ_3:70
dom(p - A) c= dom p;

theorem :: FINSEQ_3:71
dom(p - A) = dom p implies A misses rng p;

theorem :: FINSEQ_3:72
rng(p - A) = rng p \ A;

theorem :: FINSEQ_3:73
rng(p - A) c= rng p;

theorem :: FINSEQ_3:74
rng(p - A) = rng p implies A misses rng p;

theorem :: FINSEQ_3:75
p - A = {} iff rng p c= A;

theorem :: FINSEQ_3:76
p - A = p iff A misses rng p;

theorem :: FINSEQ_3:77
p - {x} = p iff not x in rng p;

theorem :: FINSEQ_3:78
p - {} = p;

theorem :: FINSEQ_3:79
p - rng p = {};

theorem :: FINSEQ_3:80
(p ^ q) - A = (p - A) ^ (q - A);

theorem :: FINSEQ_3:81
{} - A = {};

theorem :: FINSEQ_3:82
<* x *> - A = <* x *> iff not x in A;

theorem :: FINSEQ_3:83
<* x *> - A = {} iff x in A;

theorem :: FINSEQ_3:84
<* x,y *> - A = {} iff x in A & y in A;

theorem :: FINSEQ_3:85
x in A & not y in A implies <* x,y *> - A = <* y *>;

theorem :: FINSEQ_3:86
<* x,y *> - A = <* y *> & x <> y implies x in A & not y in A;

theorem :: FINSEQ_3:87
not x in A & y in A implies <* x,y *> - A = <* x *>;

theorem :: FINSEQ_3:88
<* x,y *> - A = <* x *> & x <> y implies not x in A & y in A;

theorem :: FINSEQ_3:89
<* x,y *> - A = <* x,y *> iff not x in A & not y in A;

theorem :: FINSEQ_3:90
len p = k + 1 & q = p | Seg k implies
(p.(k + 1) in A iff p - A = q - A);

theorem :: FINSEQ_3:91
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:92
n in dom p implies
for B being finite set st B = {k : 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:93
p is FinSequence of D implies p - A is FinSequence of D;

theorem :: FINSEQ_3:94
p is one-to-one implies p - A is one-to-one;

theorem :: FINSEQ_3:95
p is one-to-one implies len(p - A) = len p - card(A /\ rng p);

theorem :: FINSEQ_3:96
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:97
p is one-to-one & x in rng p implies len(p - {x}) = len p - 1;

theorem :: FINSEQ_3:98
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:99
A c= Seg k implies Sgm A is one-to-one;

theorem :: FINSEQ_3:100
idseq n is one-to-one;

theorem :: FINSEQ_3:101
{} is one-to-one;

theorem :: FINSEQ_3:102
<* x *> is one-to-one;

theorem :: FINSEQ_3:103
x <> y iff <* x,y *> is one-to-one;

theorem :: FINSEQ_3:104
x <> y & y <> z & z <> x iff <* x,y,z *> is one-to-one;

theorem :: FINSEQ_3:105
p is one-to-one & rng p = {x} implies len p = 1;

theorem :: FINSEQ_3:106
p is one-to-one & rng p = {x} implies p = <* x *>;

theorem :: FINSEQ_3:107
p is one-to-one & rng p = {x,y} & x <> y implies len p = 2;

theorem :: FINSEQ_3:108
p is one-to-one & rng p = {x,y} & x <> y implies
p = <* x,y *> or p = <* y,x *>;

theorem :: FINSEQ_3:109
p is one-to-one & rng p = {x,y,z} & <* x,y,z *> is one-to-one implies
len p = 3;

theorem :: FINSEQ_3:110
p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & x <> z implies
len p = 3;
```