:: Segments of Natural Numbers and Finite Sequences
:: by Grzegorz Bancerek and Krzysztof Hryniewiecki
::
:: Received April 1, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem defines Seg FINSEQ_1:def 1 :
theorem :: FINSEQ_1:1
canceled;
theorem :: FINSEQ_1:2
canceled;
theorem Th3: :: FINSEQ_1:3
for
a,
b being
Nat holds
(
a in Seg b iff ( 1
<= a &
a <= b ) )
theorem Th4: :: FINSEQ_1:4
theorem Th5: :: FINSEQ_1:5
theorem :: FINSEQ_1:6
theorem Th7: :: FINSEQ_1:7
theorem Th8: :: FINSEQ_1:8
theorem Th9: :: FINSEQ_1:9
theorem :: FINSEQ_1:10
theorem Th11: :: FINSEQ_1:11
theorem :: FINSEQ_1:12
:: deftheorem Def2 defines FinSequence-like FINSEQ_1:def 2 :
defpred S1[ set , set ] means ex k being Nat st
( $1 = k & $2 = k + 1 );
Lm1:
for n being Nat holds Seg n,n are_equipotent
Lm2:
for n being Nat holds card (Seg n) = card n
:: deftheorem Def3 defines len FINSEQ_1:def 3 :
theorem :: FINSEQ_1:13
canceled;
theorem :: FINSEQ_1:14
theorem :: FINSEQ_1:15
theorem :: FINSEQ_1:16
theorem Th17: :: FINSEQ_1:17
theorem Th18: :: FINSEQ_1:18
theorem Th19: :: FINSEQ_1:19
theorem :: FINSEQ_1:20
theorem Th21: :: FINSEQ_1:21
:: deftheorem Def4 defines FinSequence FINSEQ_1:def 4 :
Lm3:
for D being set
for f being FinSequence of D holds f is PartFunc of NAT ,D
theorem :: FINSEQ_1:22
canceled;
theorem Th23: :: FINSEQ_1:23
theorem :: FINSEQ_1:24
theorem :: FINSEQ_1:25
canceled;
theorem :: FINSEQ_1:26
canceled;
theorem :: FINSEQ_1:27
canceled;
Lm4:
for q being FinSequence holds
( q = {} iff len q = 0 )
;
theorem :: FINSEQ_1:28
:: deftheorem defines <* FINSEQ_1:def 5 :
:: deftheorem defines <*> FINSEQ_1:def 6 :
theorem :: FINSEQ_1:29
canceled;
theorem :: FINSEQ_1:30
canceled;
theorem :: FINSEQ_1:31
canceled;
theorem :: FINSEQ_1:32
:: deftheorem Def7 defines ^ FINSEQ_1:def 7 :
theorem Th33: :: FINSEQ_1:33
theorem :: FINSEQ_1:34
canceled;
theorem Th35: :: FINSEQ_1:35
theorem Th36: :: FINSEQ_1:36
theorem Th37: :: FINSEQ_1:37
theorem Th38: :: FINSEQ_1:38
theorem Th39: :: FINSEQ_1:39
theorem Th40: :: FINSEQ_1:40
theorem Th41: :: FINSEQ_1:41
theorem Th42: :: FINSEQ_1:42
theorem Th43: :: FINSEQ_1:43
theorem Th44: :: FINSEQ_1:44
theorem Th45: :: FINSEQ_1:45
theorem :: FINSEQ_1:46
theorem Th47: :: FINSEQ_1:47
theorem Th48: :: FINSEQ_1:48
Lm5:
for x, y, x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
:: deftheorem Def8 defines <* FINSEQ_1:def 8 :
theorem :: FINSEQ_1:49
canceled;
theorem Th50: :: FINSEQ_1:50
:: deftheorem defines <* FINSEQ_1:def 9 :
:: deftheorem defines <* FINSEQ_1:def 10 :
registration
let x,
y be
set ;
cluster <*x,y*> -> Relation-like Function-like ;
coherence
( <*x,y*> is Function-like & <*x,y*> is Relation-like )
;
let z be
set ;
cluster <*x,y,z*> -> Relation-like Function-like ;
coherence
( <*x,y,z*> is Function-like & <*x,y,z*> is Relation-like )
;
end;
theorem :: FINSEQ_1:51
canceled;
theorem :: FINSEQ_1:52
theorem :: FINSEQ_1:53
canceled;
theorem :: FINSEQ_1:54
canceled;
theorem Th55: :: FINSEQ_1:55
theorem Th56: :: FINSEQ_1:56
theorem Th57: :: FINSEQ_1:57
theorem :: FINSEQ_1:58
theorem Th59: :: FINSEQ_1:59
theorem :: FINSEQ_1:60
theorem Th61: :: FINSEQ_1:61
theorem Th62: :: FINSEQ_1:62
theorem Th63: :: FINSEQ_1:63
theorem :: FINSEQ_1:64
:: deftheorem Def11 defines * FINSEQ_1:def 11 :
theorem :: FINSEQ_1:65
theorem :: FINSEQ_1:66
:: deftheorem Def12 defines FinSubsequence-like FINSEQ_1:def 12 :
theorem :: FINSEQ_1:67
canceled;
theorem :: FINSEQ_1:68
theorem :: FINSEQ_1:69
definition
let X be
set ;
given k being
Nat such that A1:
X c= Seg k
;
func Sgm X -> FinSequence of
NAT means :
Def13:
:: FINSEQ_1:def 13
(
rng it = X & ( for
l,
m,
k1,
k2 being
Nat st 1
<= l &
l < m &
m <= len it &
k1 = it . l &
k2 = it . m holds
k1 < k2 ) );
existence
ex b1 being FinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) )
uniqueness
for b1, b2 being FinSequence of NAT st rng b1 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) & rng b2 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) holds
b1 = b2
end;
:: deftheorem Def13 defines Sgm FINSEQ_1:def 13 :
theorem :: FINSEQ_1:70
canceled;
theorem Th71: :: FINSEQ_1:71
:: deftheorem defines Seq FINSEQ_1:def 14 :
theorem :: FINSEQ_1:72
theorem :: FINSEQ_1:73
theorem :: FINSEQ_1:74
theorem :: FINSEQ_1:75
theorem :: FINSEQ_1:76
theorem :: FINSEQ_1:77
theorem :: FINSEQ_1:78
:: deftheorem defines | FINSEQ_1:def 15 :
theorem :: FINSEQ_1:79
theorem :: FINSEQ_1:80
theorem :: FINSEQ_1:81
theorem :: FINSEQ_1:82
definition
let R be
Relation;
func R [*] -> Relation means :: FINSEQ_1:def 16
for
x,
y being
set holds
(
[x,y] in it iff (
x in field R &
y in field R & ex
p being
FinSequence st
(
len p >= 1 &
p . 1
= x &
p . (len p) = y & ( for
i being
Nat st
i >= 1 &
i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) )
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) holds
b1 = b2
end;
:: deftheorem defines [*] FINSEQ_1:def 16 :
theorem :: FINSEQ_1:83
for
D1,
D2 being
set st
D1 c= D2 holds
D1 * c= D2 *
theorem :: FINSEQ_1:84
theorem :: FINSEQ_1:85
theorem :: FINSEQ_1:86
Lm6:
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 )
;
Lm7:
( 1 in Seg 4 & 2 in Seg 4 & 3 in Seg 4 & 4 in Seg 4 )
;
Lm8:
( 1 in Seg 5 & 2 in Seg 5 & 3 in Seg 5 & 4 in Seg 5 & 5 in Seg 5 )
;
Lm9:
( 1 in Seg 6 & 2 in Seg 6 & 3 in Seg 6 & 4 in Seg 6 & 5 in Seg 6 & 6 in Seg 6 )
;
Lm10:
( 1 in Seg 7 & 2 in Seg 7 & 3 in Seg 7 & 4 in Seg 7 & 5 in Seg 7 & 6 in Seg 7 & 7 in Seg 7 )
;
Lm11:
( 1 in Seg 8 & 2 in Seg 8 & 3 in Seg 8 & 4 in Seg 8 & 5 in Seg 8 & 6 in Seg 8 & 7 in Seg 8 & 8 in Seg 8 )
;
theorem Th87: :: FINSEQ_1:87
theorem Th88: :: FINSEQ_1:88
theorem Th89: :: FINSEQ_1:89
theorem Th90: :: FINSEQ_1:90
theorem Th91: :: FINSEQ_1:91
theorem :: FINSEQ_1:92
theorem :: FINSEQ_1:93
theorem :: FINSEQ_1:94
theorem :: FINSEQ_1:95
theorem :: FINSEQ_1:96
theorem :: FINSEQ_1:97
theorem :: FINSEQ_1:98
theorem :: FINSEQ_1:99
for
a,
b,
c,
d,
e,
f being
set st
<*a,b,c*> = <*d,e,f*> holds
(
a = d &
b = e &
c = f )
theorem Th100: :: FINSEQ_1:100
theorem :: FINSEQ_1:101
:: deftheorem defines = FINSEQ_1:def 17 :
theorem :: FINSEQ_1:102
theorem :: FINSEQ_1:103
theorem :: FINSEQ_1:104