begin
:: deftheorem defines Seg FINSEQ_1:def 1 :
theorem
canceled;
theorem
canceled;
theorem Th3:
for
a,
b being
Nat holds
(
a in Seg b iff ( 1
<= a &
a <= b ) )
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem
:: 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
canceled;
theorem
canceled;
theorem
theorem
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem Th21:
:: 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
canceled;
theorem Th23:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
Lm4:
for q being FinSequence holds
( q = {} iff len q = 0 )
;
theorem
:: deftheorem defines <* FINSEQ_1:def 5 :
:: deftheorem defines <*> FINSEQ_1:def 6 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem Def7 defines ^ FINSEQ_1:def 7 :
theorem Th33:
theorem
canceled;
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem
theorem Th47:
theorem Th48:
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
canceled;
theorem Th50:
:: 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
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem Th55:
theorem Th56:
theorem Th57:
theorem
theorem Th59:
theorem
theorem Th61:
theorem Th62:
theorem Th63:
theorem
:: deftheorem Def11 defines * FINSEQ_1:def 11 :
theorem
theorem
:: deftheorem Def12 defines FinSubsequence-like FINSEQ_1:def 12 :
definition
let X be
set ;
given k being
Nat such that A1:
X c= Seg k
;
func Sgm X -> FinSequence of
NAT means :
Def13:
(
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th71:
:: deftheorem defines Seq FINSEQ_1:def 14 :
theorem
begin
theorem
begin
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem defines | FINSEQ_1:def 15 :
theorem
theorem
theorem
theorem
definition
let R be
Relation;
func R [*] -> Relation means
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
for
D1,
D2 being
set st
D1 c= D2 holds
D1 * c= D2 *
theorem
theorem
theorem
Lm6:
( 1 in Seg 3 & 2 in Seg 3 )
;
Lm7:
3 in Seg 3
;
Lm8:
( 1 in Seg 4 & 2 in Seg 4 )
;
Lm9:
( 3 in Seg 4 & 4 in Seg 4 )
;
Lm10:
( 1 in Seg 5 & 2 in Seg 5 )
;
Lm11:
( 3 in Seg 5 & 4 in Seg 5 )
;
Lm12:
5 in Seg 5
;
Lm13:
( 1 in Seg 6 & 2 in Seg 6 )
;
Lm14:
( 3 in Seg 6 & 4 in Seg 6 )
;
Lm15:
( 5 in Seg 6 & 6 in Seg 6 )
;
Lm16:
( 1 in Seg 7 & 2 in Seg 7 )
;
Lm17:
( 3 in Seg 7 & 4 in Seg 7 )
;
Lm18:
( 5 in Seg 7 & 6 in Seg 7 )
;
Lm19:
7 in Seg 7
;
Lm20:
( 1 in Seg 8 & 2 in Seg 8 )
;
Lm21:
( 3 in Seg 8 & 4 in Seg 8 )
;
Lm22:
( 5 in Seg 8 & 6 in Seg 8 )
;
Lm23:
( 7 in Seg 8 & 8 in Seg 8 )
;
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
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:
theorem
:: deftheorem defines = FINSEQ_1:def 17 :
theorem
theorem
theorem
:: deftheorem Def18 defines -long FINSEQ_1:def 18 :
:: deftheorem Def19 defines FinSequence-membered FINSEQ_1:def 19 :
theorem
theorem
theorem
theorem
theorem
theorem