:: Non-contiguous Substrings and One-to-one Finite Sequences
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: FINSEQ_3:1
theorem Th2: :: FINSEQ_3:2
theorem Th3: :: FINSEQ_3:3
theorem Th4: :: FINSEQ_3:4
theorem Th5: :: FINSEQ_3:5
theorem :: FINSEQ_3:6
theorem :: FINSEQ_3:7
theorem :: FINSEQ_3:8
canceled;
theorem Th9: :: FINSEQ_3:9
theorem :: FINSEQ_3:10
theorem Th11: :: FINSEQ_3:11
theorem :: FINSEQ_3:12
theorem Th13: :: FINSEQ_3:13
theorem :: FINSEQ_3:14
theorem Th15: :: FINSEQ_3:15
theorem :: FINSEQ_3:16
theorem :: FINSEQ_3:17
theorem :: FINSEQ_3:18
theorem Th19: :: FINSEQ_3:19
theorem Th20: :: FINSEQ_3:20
theorem :: FINSEQ_3:21
canceled;
theorem Th22: :: FINSEQ_3:22
theorem :: FINSEQ_3:23
theorem Th24: :: FINSEQ_3:24
theorem :: FINSEQ_3:25
theorem Th26: :: FINSEQ_3:26
theorem Th27: :: FINSEQ_3:27
theorem :: FINSEQ_3:28
theorem Th29: :: FINSEQ_3:29
theorem Th30: :: FINSEQ_3:30
theorem Th31: :: FINSEQ_3:31
theorem Th32: :: FINSEQ_3:32
theorem Th33: :: FINSEQ_3:33
theorem :: FINSEQ_3:34
theorem :: FINSEQ_3:35
canceled;
theorem :: FINSEQ_3:36
canceled;
theorem :: FINSEQ_3:37
canceled;
theorem Th38: :: FINSEQ_3:38
theorem :: FINSEQ_3:39
theorem Th40: :: FINSEQ_3:40
theorem :: FINSEQ_3:41
theorem :: FINSEQ_3:42
theorem Th43: :: FINSEQ_3:43
Lm1:
for A being set
for k being natural number st A c= Seg k holds
Sgm A is one-to-one
theorem Th44: :: FINSEQ_3:44
theorem :: FINSEQ_3:45
theorem Th46: :: FINSEQ_3:46
theorem :: FINSEQ_3:47
canceled;
theorem Th48: :: FINSEQ_3:48
theorem Th49: :: FINSEQ_3:49
theorem :: FINSEQ_3:50
theorem :: FINSEQ_3:51
theorem Th52: :: FINSEQ_3:52
Lm2:
for k being natural number holds (Sgm (Seg (k + 0 ))) | (Seg k) = Sgm (Seg k)
Lm3:
now
let n be
natural number ;
:: thesis: ( ( for k being natural number holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) ) implies for k being natural number holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k) )assume A1:
for
k being
natural number holds
(Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k)
;
:: thesis: for k being natural number holds (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)let k be
natural number ;
:: thesis: (Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)set X =
Sgm (Seg (k + (n + 1)));
set Y =
Sgm (Seg (k + 1));
Sgm (Seg (k + (n + 1))) = Sgm (Seg ((k + 1) + n))
;
then A2:
(Sgm (Seg (k + (n + 1)))) | (Seg (k + 1)) = Sgm (Seg (k + 1))
by A1;
(Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k)
proof
reconsider p =
(Sgm (Seg (k + 1))) | (Seg k) as
FinSequence of
NAT by FINSEQ_1:23;
A3:
rng (Sgm (Seg (k + 1))) = Seg (k + 1)
by FINSEQ_1:def 13;
A4:
Sgm (Seg (k + 1)) is
one-to-one
by Lm1;
A5:
len (Sgm (Seg (k + 1))) = k + 1
by Th52;
then A6:
(
dom (Sgm (Seg (k + 1))) = Seg (k + 1) &
k <= k + 1 )
by FINSEQ_1:def 3, NAT_1:12;
then A7:
dom p = Seg k
by A5, FINSEQ_1:21;
A8:
(Sgm (Seg (k + 1))) . (k + 1) = k + 1
proof
assume A9:
not
(Sgm (Seg (k + 1))) . (k + 1) = k + 1
;
:: thesis: contradiction
k + 1
in dom (Sgm (Seg (k + 1)))
by A6, FINSEQ_1:6;
then A10:
(
(Sgm (Seg (k + 1))) . (k + 1) in Seg (k + 1) & not
(Sgm (Seg (k + 1))) . (k + 1) in {(k + 1)} )
by A3, A9, FUNCT_1:def 5, TARSKI:def 1;
then
(Sgm (Seg (k + 1))) . (k + 1) in (Seg (k + 1)) \ {(k + 1)}
by XBOOLE_0:def 5;
then A11:
(Sgm (Seg (k + 1))) . (k + 1) in Seg k
by FINSEQ_1:12;
reconsider n =
(Sgm (Seg (k + 1))) . (k + 1) as
Element of
NAT by A10;
k + 1
in rng (Sgm (Seg (k + 1)))
by A3, FINSEQ_1:6;
then consider x being
set such that A12:
x in dom (Sgm (Seg (k + 1)))
and A13:
(Sgm (Seg (k + 1))) . x = k + 1
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A12;
A14:
( 1
<= x &
x <= k + 1 )
by A5, A12, Th27;
then
x < k + 1
by A14, XXREAL_0:1;
then
(
k + 1
< n &
n <= k &
k < k + 1 )
by A5, A11, A13, A14, FINSEQ_1:3, FINSEQ_1:def 13, XREAL_1:31;
hence
contradiction
by XXREAL_0:2;
:: thesis: verum
end;
rng p = (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
proof
thus
rng p c= (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
:: according to XBOOLE_0:def 10 :: thesis: (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} c= rng p
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} )
assume A15:
x in rng p
;
:: thesis: x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
A16:
rng p c= rng (Sgm (Seg (k + 1)))
by RELAT_1:99;
now
assume A17:
x in {(k + 1)}
;
:: thesis: contradictionconsider y being
set such that A18:
y in dom p
and A19:
p . y = x
by A15, FUNCT_1:def 5;
reconsider y =
y as
Element of
NAT by A18;
Seg k c= Seg (k + 1)
by Th19;
then A20:
(
y in dom (Sgm (Seg (k + 1))) &
(Sgm (Seg (k + 1))) . y = p . y &
x = k + 1 &
k + 1
in dom (Sgm (Seg (k + 1))) )
by A6, A7, A17, A18, FINSEQ_1:6, FUNCT_1:70, TARSKI:def 1;
(
y <= k &
k < k + 1 )
by A7, A18, FINSEQ_1:3, XREAL_1:31;
hence
contradiction
by A4, A8, A19, A20, FUNCT_1:def 8;
:: thesis: verum
end;
hence
x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
by A8, A15, A16, XBOOLE_0:def 5;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))} or x in rng p )
assume A21:
x in (rng (Sgm (Seg (k + 1)))) \ {((Sgm (Seg (k + 1))) . (k + 1))}
;
:: thesis: x in rng p
then consider y being
set such that A22:
y in dom (Sgm (Seg (k + 1)))
and A23:
(Sgm (Seg (k + 1))) . y = x
by FUNCT_1:def 5;
then
y in (Seg (k + 1)) \ {(k + 1)}
by A6, A22, XBOOLE_0:def 5;
then A24:
y in dom p
by A7, FINSEQ_1:12;
then
p . y = (Sgm (Seg (k + 1))) . y
by FUNCT_1:70;
hence
x in rng p
by A23, A24, FUNCT_1:def 5;
:: thesis: verum
end;
then A25:
rng p = Seg k
by A3, A8, FINSEQ_1:12;
now
let i,
j,
l,
m be
natural number ;
:: thesis: ( 1 <= i & i < j & j <= len p & l = p . i & m = p . j implies l < m )assume that A26:
( 1
<= i &
i < j &
j <= len p )
and A27:
(
l = p . i &
m = p . j )
;
:: thesis: l < mA28:
(
len p = k &
i <= len p & 1
<= j )
by A5, A6, A26, FINSEQ_1:21, XXREAL_0:2;
then
(
i in dom p &
j in dom p &
len (Sgm (Seg (k + 1))) = k + 1 &
k <= k + 1 )
by A7, A26, Th52, FINSEQ_1:3, NAT_1:12;
then
(
p . i = (Sgm (Seg (k + 1))) . i &
p . j = (Sgm (Seg (k + 1))) . j &
j <= len (Sgm (Seg (k + 1))) )
by A26, A28, FUNCT_1:70, XXREAL_0:2;
hence
l < m
by A26, A27, FINSEQ_1:def 13;
:: thesis: verum
end;
hence
(Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k)
by A25, FINSEQ_1:def 13;
:: thesis: verum
end;
then
(
Sgm (Seg k) = (Sgm (Seg (k + (n + 1)))) | ((Seg (k + 1)) /\ (Seg k)) &
k <= k + 1 )
by A2, NAT_1:12, RELAT_1:100;
hence
(Sgm (Seg (k + (n + 1)))) | (Seg k) = Sgm (Seg k)
by FINSEQ_1:9;
:: thesis: verum
end;
Lm4:
for n, k being natural number holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k)
theorem :: FINSEQ_3:53
Lm5:
now
let k be
Nat;
:: thesis: ( Sgm (Seg k) = idseq k implies Sgm (Seg (k + 1)) = idseq (k + 1) )assume A1:
Sgm (Seg k) = idseq k
;
:: thesis: Sgm (Seg (k + 1)) = idseq (k + 1)A2:
len (idseq (k + 1)) = k + 1
by FINSEQ_2:55;
then A3:
len (Sgm (Seg (k + 1))) = len (idseq (k + 1))
by Th52;
then X:
dom (Sgm (Seg (k + 1))) = Seg (k + 1)
by A2, FINSEQ_1:def 3;
now
let j be
Nat;
:: thesis: ( j in dom (Sgm (Seg (k + 1))) implies (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j )assume A4:
j in dom (Sgm (Seg (k + 1)))
;
:: thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . jthen A5:
j in (Seg k) \/ {(k + 1)}
by X, FINSEQ_1:11;
now
per cases
( j in Seg k or j in {(k + 1)} )
by A5, XBOOLE_0:def 3;
suppose
j in {(k + 1)}
;
:: thesis: (Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
then A7:
j = k + 1
by TARSKI:def 1;
then A8:
j in Seg (k + 1)
by FINSEQ_1:6;
set X =
Sgm (Seg (k + 1));
set Y =
Sgm (Seg k);
now
assume
(Sgm (Seg (k + 1))) . j <> j
;
:: thesis: contradictionthen A9:
( not
(Sgm (Seg (k + 1))) . j in {j} &
Seg (k + 1) c= Seg (k + 1) )
by TARSKI:def 1;
A10:
(
rng (Sgm (Seg (k + 1))) = Seg (k + 1) &
dom (Sgm (Seg (k + 1))) = Seg (k + 1) )
by A2, A3, FINSEQ_1:def 3, FINSEQ_1:def 13;
then A11:
(Sgm (Seg (k + 1))) . j in Seg (k + 1)
by A4, FUNCT_1:def 5;
then
(Sgm (Seg (k + 1))) . j in (Seg (k + 1)) \ {(k + 1)}
by A7, A9, XBOOLE_0:def 5;
then A12:
(Sgm (Seg (k + 1))) . j in Seg k
by FINSEQ_1:12;
reconsider n =
(Sgm (Seg (k + 1))) . j as
Element of
NAT by A11;
A13:
Sgm (Seg (k + 1)) is
one-to-one
by Lm1;
(Sgm (Seg (k + 1))) | (Seg k) = Sgm (Seg k)
by Lm4;
then A14:
(Sgm (Seg (k + 1))) . n =
(Sgm (Seg k)) . n
by A12, FUNCT_1:72
.=
n
by A1, A12, FUNCT_1:35
;
(
n <= k &
k < k + 1 )
by A12, FINSEQ_1:3, XREAL_1:31;
hence
contradiction
by A7, A8, A10, A11, A13, A14, FUNCT_1:def 8;
:: thesis: verum
end;
hence
(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
by A7, FINSEQ_1:6, FUNCT_1:35;
:: thesis: verum
end;
end;
end;
hence
(Sgm (Seg (k + 1))) . j = (idseq (k + 1)) . j
;
:: thesis: verum
end;
hence
Sgm (Seg (k + 1)) = idseq (k + 1)
by A3, FINSEQ_2:10;
:: thesis: verum
end;
theorem Th54: :: FINSEQ_3:54
theorem Th55: :: FINSEQ_3:55
theorem Th56: :: FINSEQ_3:56
theorem :: FINSEQ_3:57
theorem :: FINSEQ_3:58
theorem Th59: :: FINSEQ_3:59
theorem :: FINSEQ_3:60
theorem Th61: :: FINSEQ_3:61
theorem :: FINSEQ_3:62
theorem Th63: :: FINSEQ_3:63
theorem Th64: :: FINSEQ_3:64
:: deftheorem defines - FINSEQ_3:def 1 :
theorem :: FINSEQ_3:65
canceled;
theorem Th66: :: FINSEQ_3:66
theorem Th67: :: FINSEQ_3:67
theorem Th68: :: FINSEQ_3:68
theorem :: FINSEQ_3:69
theorem :: FINSEQ_3:70
theorem :: FINSEQ_3:71
theorem Th72: :: FINSEQ_3:72
theorem :: FINSEQ_3:73
theorem :: FINSEQ_3:74
theorem Th75: :: FINSEQ_3:75
theorem Th76: :: FINSEQ_3:76
theorem :: FINSEQ_3:77
theorem :: FINSEQ_3:78
theorem :: FINSEQ_3:79
Lm6:
for x, A being set holds
( <*x*> - A = <*x*> iff not x in A )
Lm7:
for x, A being set holds
( <*x*> - A = {} iff x in A )
Lm8:
for p being FinSequence
for A being set holds (p ^ {} ) - A = (p - A) ^ ({} - A)
Lm9:
for p being FinSequence
for x, A being set holds (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
Lm11:
for q, p being FinSequence
for A being set holds (p ^ q) - A = (p - A) ^ (q - A)
theorem :: FINSEQ_3:80
theorem :: FINSEQ_3:81
theorem :: FINSEQ_3:82
theorem :: FINSEQ_3:83
theorem Th84: :: FINSEQ_3:84
theorem Th85: :: FINSEQ_3:85
theorem :: FINSEQ_3:86
theorem Th87: :: FINSEQ_3:87
theorem :: FINSEQ_3:88
theorem :: FINSEQ_3:89
for
x,
y,
A being
set holds
(
<*x,y*> - A = <*x,y*> iff ( not
x in A & not
y in A ) )
theorem Th90: :: FINSEQ_3:90
theorem Th91: :: FINSEQ_3:91
Lm13:
for l being natural number st ( for p being FinSequence
for A being set st len p = l holds
for n being natural number st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n ) ) holds
for p being FinSequence
for A being set st len p = l + 1 holds
for n being natural number st n in dom p holds
for C being finite set holds
( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n )
Lm14:
for l being natural number
for p being FinSequence
for A being set st len p = l holds
for n being natural number st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n )
theorem :: FINSEQ_3:92
theorem :: FINSEQ_3:93
theorem Th94: :: FINSEQ_3:94
theorem Th95: :: FINSEQ_3:95
theorem Th96: :: FINSEQ_3:96
theorem :: FINSEQ_3:97
theorem Th98: :: FINSEQ_3:98
theorem :: FINSEQ_3:99
theorem :: FINSEQ_3:100
canceled;
theorem :: FINSEQ_3:101
canceled;
theorem Th102: :: FINSEQ_3:102
theorem Th103: :: FINSEQ_3:103
theorem Th104: :: FINSEQ_3:104
theorem Th105: :: FINSEQ_3:105
theorem :: FINSEQ_3:106
theorem Th107: :: FINSEQ_3:107
theorem :: FINSEQ_3:108
theorem Th109: :: FINSEQ_3:109
theorem :: FINSEQ_3:110
theorem :: FINSEQ_3:111
theorem :: FINSEQ_3:112
:: deftheorem defines Del FINSEQ_3:def 2 :
theorem Th113: :: FINSEQ_3:113
theorem :: FINSEQ_3:114
theorem :: FINSEQ_3:115
theorem Th116: :: FINSEQ_3:116
theorem Th117: :: FINSEQ_3:117
theorem Th118: :: FINSEQ_3:118
theorem :: FINSEQ_3:119
theorem :: FINSEQ_3:120
theorem Th121: :: FINSEQ_3:121
theorem :: FINSEQ_3:122
theorem Th123: :: FINSEQ_3:123
theorem :: FINSEQ_3:124
theorem :: FINSEQ_3:125
theorem :: FINSEQ_3:126
theorem :: FINSEQ_3:127