:: Basic Properties and Concept of Selected Subsequence of Zero Based FiniteSequences
:: by Yatsuka Nakamura and Hisashi Ito
::
:: Received June 27, 2008
:: Copyright (c) 2008 Association of Mizar Users

theorem AB470: :: AFINSQ_2:1

for x being set
for i being Nat st x in i holds
x is Element of NAT

proof end;

registration

cluster -> natural-membered set ;
coherence
for b₁ being Nat holds b₁ is natural-membered

proof end;

end;

theorem AE221f: :: AFINSQ_2:2

for X0 being finite natural-membered set ex m being Nat st X0 c= m

proof end;

theorem Th11: :: AFINSQ_2:3

for p being XFinSequence
for b being set st b in rng p holds
ex i being Element of NAT st
( i in dom p & p . i = b )

proof end;

theorem Th14: :: AFINSQ_2:4

for D being set
for p being XFinSequence st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is XFinSequence of D

proof end;

scheme :: AFINSQ_2:sch 1
XSeqLambdaD{ F₁() -> Nat, F₂() -> non empty set , F₃( set ) -> Element of F₂() } :

ex z being XFinSequence of F₂() st
( len z = F₁() & ( for j being Nat st j in F₁() holds
z . j = F₃(j) ) )

proof end;

theorem Th10: :: AFINSQ_2:5

for p, q being XFinSequence st len p = len q & ( for j being Nat st j in dom p holds
p . j = q . j ) holds
p = q

proof end;

definition

let f be XFinSequence of REAL ;
let a be Element of REAL ;
:: original: +
redefine func f + a -> XFinSequence of REAL ;
coherence
a + f is XFinSequence of REAL

proof end;

end;

theorem AC500: :: AFINSQ_2:6

for f being XFinSequence of REAL
for a being Element of REAL holds
( len (f + a) = len f & ( for i being Nat st i < len f holds
(f + a) . i = (f . i) + a ) )

proof end;

theorem AE359: :: AFINSQ_2:7

for f1, f2 being XFinSequence
for i being Nat st i < len f1 holds
(f1 ^ f2) . i = f1 . i

proof end;

definition

let f be XFinSequence;
func Rev f -> XFinSequence means :Def3: :: AFINSQ_2:def 1
( len it = len f & ( for i being Element of NAT st i in dom it holds
it . i = f . ((len f) - (i + 1)) ) );
existence
ex b₁ being XFinSequence st
( len b₁ = len f & ( for i being Element of NAT st i in dom b₁ holds
b₁ . i = f . ((len f) - (i + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence st len b₁ = len f & ( for i being Element of NAT st i in dom b₁ holds
b₁ . i = f . ((len f) - (i + 1)) ) & len b₂ = len f & ( for i being Element of NAT st i in dom b₂ holds
b₂ . i = f . ((len f) - (i + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Rev AFINSQ_2:def 1 :

for f, b₂ being XFinSequence holds
( b₂ = Rev f iff ( len b₂ = len f & ( for i being Element of NAT st i in dom b₂ holds
b₂ . i = f . ((len f) - (i + 1)) ) ) );

theorem Th60: :: AFINSQ_2:8

for f being XFinSequence holds
( dom f = dom (Rev f) & rng f = rng (Rev f) )

proof end;

definition

let D be set ;
let f be XFinSequence of D;
:: original: Rev
redefine func Rev f -> XFinSequence of D;
coherence
Rev f is XFinSequence of D

proof end;

end;

theorem :: AFINSQ_2:9

for p being XFinSequence st p <> {} holds
ex q being XFinSequence ex x being set st p = q ^ <%x%>

proof end;

theorem Lm4: :: AFINSQ_2:10

for n being Nat
for f being XFinSequence st len f <= n holds
f | n = f

proof end;

theorem Th19: :: AFINSQ_2:11

for f being XFinSequence
for n, m being Nat st n <= len f & m in n holds
( (f | n) . m = f . m & m in dom f )

proof end;

theorem TH80: :: AFINSQ_2:12

for i being Element of NAT
for q being XFinSequence st i <= len q holds
len (q | i) = i

proof end;

theorem TH80f: :: AFINSQ_2:13

for i being Element of NAT
for q being XFinSequence holds len (q | i) <= i

proof end;

theorem :: AFINSQ_2:14

for f being XFinSequence
for n being Element of NAT st len f = n + 1 holds
f = (f | n) ^ <%(f . n)%>

proof end;

definition

let f be XFinSequence;
let n be Nat;
func f /^ n -> XFinSequence means :Def2: :: AFINSQ_2:def 2
( len it = (len f) -' n & ( for m being Nat st m in dom it holds
it . m = f . (m + n) ) );
existence
ex b₁ being XFinSequence st
( len b₁ = (len f) -' n & ( for m being Nat st m in dom b₁ holds
b₁ . m = f . (m + n) ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence st len b₁ = (len f) -' n & ( for m being Nat st m in dom b₁ holds
b₁ . m = f . (m + n) ) & len b₂ = (len f) -' n & ( for m being Nat st m in dom b₂ holds
b₂ . m = f . (m + n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines /^ AFINSQ_2:def 2 :

for f being XFinSequence
for n being Nat
for b₃ being XFinSequence holds
( b₃ = f /^ n iff ( len b₃ = (len f) -' n & ( for m being Nat st m in dom b₃ holds
b₃ . m = f . (m + n) ) ) );

theorem TH80e: :: AFINSQ_2:15

for f being XFinSequence
for n being Nat st n >= len f holds
f /^ n = {}

proof end;

theorem TH80b: :: AFINSQ_2:16

for f being XFinSequence
for n being Nat st n < len f holds
len (f /^ n) = (len f) - n

proof end;

theorem Th19b: :: AFINSQ_2:17

for f being XFinSequence
for n, m being Nat st m + n < len f holds
(f /^ n) . m = f . (m + n)

proof end;

registration

let f be one-to-one XFinSequence;
let n be Nat;
cluster f /^ n -> one-to-one ;
coherence
f /^ n is one-to-one

proof end;

end;

theorem AG170: :: AFINSQ_2:18

for f being XFinSequence
for n being Nat holds rng (f /^ n) c= rng f

proof end;

theorem Th31: :: AFINSQ_2:19

for f being XFinSequence holds f /^ 0 = f

proof end;

theorem Th39: :: AFINSQ_2:20

for i being Nat
for f, g being XFinSequence holds (f ^ g) /^ ((len f) + i) = g /^ i

proof end;

theorem Th40: :: AFINSQ_2:21

for f, g being XFinSequence holds (f ^ g) /^ (len f) = g

proof end;

theorem :: AFINSQ_2:22

for f being XFinSequence
for n being Element of NAT holds (f | n) ^ (f /^ n) = f

proof end;

definition

let D be set ;
let f be XFinSequence of D;
let n be Nat;
:: original: /^
redefine func f /^ n -> XFinSequence of D;
coherence
f /^ n is XFinSequence of D

proof end;

end;

definition

let f be XFinSequence;
let k1, k2 be Nat;
func mid f,k1,k2 -> XFinSequence means :AB540b: :: AFINSQ_2:def 3
for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
it = (f | k21) /^ (k11 -' 1);
existence
ex b₁ being XFinSequence st
for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
b₁ = (f | k21) /^ (k11 -' 1)

proof end;

uniqueness
for b₁, b₂ being XFinSequence st ( for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
b₁ = (f | k21) /^ (k11 -' 1) ) & ( for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
b₂ = (f | k21) /^ (k11 -' 1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem AB540b defines mid AFINSQ_2:def 3 :

for f being XFinSequence
for k1, k2 being Nat
for b₄ being XFinSequence holds
( b₄ = mid f,k1,k2 iff for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
b₄ = (f | k21) /^ (k11 -' 1) );

theorem AB540f: :: AFINSQ_2:23

for f being XFinSequence
for k1, k2 being Nat st k1 > k2 holds
mid f,k1,k2 = {}

proof end;

theorem :: AFINSQ_2:24

for f being XFinSequence
for k1, k2 being Nat st 1 <= k1 & k2 <= len f holds
mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1)

proof end;

theorem Th5: :: AFINSQ_2:25

for f being XFinSequence
for k2 being Nat holds mid f,1,k2 = f | k2

proof end;

theorem :: AFINSQ_2:26

for D being set
for f being XFinSequence of D
for k2 being Nat st len f <= k2 holds
mid f,1,k2 = f

proof end;

theorem :: AFINSQ_2:27

for f being XFinSequence
for k2 being Element of NAT holds mid f,0 ,k2 = mid f,1,k2

proof end;

theorem :: AFINSQ_2:28

for f, g being XFinSequence holds mid (f ^ g),((len f) + 1),((len f) + (len g)) = g

proof end;

definition

let D be set ;
let f be XFinSequence of D;
let k1, k2 be Nat;
:: original: mid
redefine func mid f,k1,k2 -> XFinSequence of D;
coherence
mid f,k1,k2 is XFinSequence of D

proof end;

end;

definition

let f be XFinSequence of REAL ;
func Sum f -> Element of REAL means :AC300: :: AFINSQ_2:def 4
ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & it = g . ((len f) -' 1) );
existence
ex b₁ being Element of REAL ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & b₁ = g . ((len f) -' 1) )

proof end;

uniqueness
for b₁, b₂ being Element of REAL st ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & b₁ = g . ((len f) -' 1) ) & ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & b₂ = g . ((len f) -' 1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem AC300 defines Sum AFINSQ_2:def 4 :

for f being XFinSequence of REAL
for b₂ being Element of REAL holds
( b₂ = Sum f iff ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & b₂ = g . ((len f) -' 1) ) );

registration

let f be empty XFinSequence of REAL ;
cluster Sum f -> zero ;
coherence
Sum f is empty

proof end;

end;

theorem :: AFINSQ_2:29

for f being empty XFinSequence of REAL holds Sum f = 0 ;

theorem :: AFINSQ_2:30

for h1, h2 being XFinSequence of REAL holds Sum (h1 ^ h2) = (Sum h1) + (Sum h2)

proof end;

definition

let X be finite natural-membered set ;
func Sgm0 X -> XFinSequence of NAT means :AC113: :: AFINSQ_2:def 5
( rng it = X & ( for l, m, k1, k2 being Nat st l < m & m < len it & k1 = it . l & k2 = it . m holds
k1 < k2 ) );
existence
ex b₁ being XFinSequence of NAT st
( rng b₁ = X & ( for l, m, k1, k2 being Nat st l < m & m < len b₁ & k1 = b₁ . l & k2 = b₁ . m holds
k1 < k2 ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence of NAT st rng b₁ = X & ( for l, m, k1, k2 being Nat st l < m & m < len b₁ & k1 = b₁ . l & k2 = b₁ . m holds
k1 < k2 ) & rng b₂ = X & ( for l, m, k1, k2 being Nat st l < m & m < len b₂ & k1 = b₂ . l & k2 = b₂ . m holds
k1 < k2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem AC113 defines Sgm0 AFINSQ_2:def 5 :

for X being finite natural-membered set
for b₂ being XFinSequence of NAT holds
( b₂ = Sgm0 X iff ( rng b₂ = X & ( for l, m, k1, k2 being Nat st l < m & m < len b₂ & k1 = b₂ . l & k2 = b₂ . m holds
k1 < k2 ) ) );

registration

let A be finite natural-membered set ;
cluster Sgm0 A -> one-to-one ;
coherence
Sgm0 A is one-to-one

proof end;

end;

theorem Th44: :: AFINSQ_2:31

for A being finite natural-membered set holds len (Sgm0 A) = card A

proof end;

theorem AE200: :: AFINSQ_2:32

for X, Y being finite natural-membered set st X c= Y & X <> {} holds
(Sgm0 Y) . 0 <= (Sgm0 X) . 0

proof end;

theorem AE205: :: AFINSQ_2:33

for n being Nat holds (Sgm0 {n}) . 0 = n

proof end;

definition

let B1, B2 be set ;
pred B1 <N< B2 means :AE100: :: AFINSQ_2:def 6
for n, m being Nat st n in B1 & m in B2 holds
n < m;

end;

:: deftheorem AE100 defines <N< AFINSQ_2:def 6 :

for B1, B2 being set holds
( B1 <N< B2 iff for n, m being Nat st n in B1 & m in B2 holds
n < m );

definition

let B1, B2 be set ;
pred B1 <N= B2 means :AE102: :: AFINSQ_2:def 7
for n, m being Nat st n in B1 & m in B2 holds
n <= m;

end;

:: deftheorem AE102 defines <N= AFINSQ_2:def 7 :

for B1, B2 being set holds
( B1 <N= B2 iff for n, m being Nat st n in B1 & m in B2 holds
n <= m );

theorem AG110: :: AFINSQ_2:34

for B1, B2 being set st B1 <N< B2 holds
(B1 /\ B2) /\ NAT = {}

proof end;

theorem AE101: :: AFINSQ_2:35

for B1, B2 being finite natural-membered set st B1 <N< B2 holds
B1 misses B2

proof end;

theorem AE400: :: AFINSQ_2:36

for A, B1, B2 being set st B1 <N< B2 holds
A /\ B1 <N< A /\ B2

proof end;

theorem :: AFINSQ_2:37

for X, Y being finite natural-membered set st Y <> {} & ex x being set st
( x in X & {x} <N= Y ) holds
(Sgm0 X) . 0 <= (Sgm0 Y) . 0

proof end;

theorem AE221e: :: AFINSQ_2:38

for X0, Y0 being finite natural-membered set
for i being Nat st X0 <N< Y0 & i < card X0 holds
( rng ((Sgm0 (X0 \/ Y0)) | (card X0)) = X0 & ((Sgm0 (X0 \/ Y0)) | (card X0)) . i = (Sgm0 (X0 \/ Y0)) . i )

proof end;

theorem :: AFINSQ_2:39

for X, Y being finite natural-membered set
for i being Nat st X <N< Y & i in card X holds
(Sgm0 (X \/ Y)) . i in X

proof end;

theorem AE221: :: AFINSQ_2:40

for X, Y being finite natural-membered set
for i being Nat st X <N< Y & i < len (Sgm0 X) holds
(Sgm0 X) . i = (Sgm0 (X \/ Y)) . i

proof end;

theorem AE222e: :: AFINSQ_2:41

for X0, Y0 being finite natural-membered set
for i being Nat st X0 <N< Y0 & i < card Y0 holds
( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) )

proof end;

theorem AE222f: :: AFINSQ_2:42

for X, Y being finite natural-membered set
for i being Nat st X <N< Y & i < len (Sgm0 Y) holds
(Sgm0 Y) . i = (Sgm0 (X \/ Y)) . (i + (len (Sgm0 X)))

proof end;

theorem AE222: :: AFINSQ_2:43

for X, Y being finite natural-membered set st Y <> {} & X <N< Y holds
(Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (len (Sgm0 X))

proof end;

theorem Th46: :: AFINSQ_2:44

for l, m, n, k being Nat
for X being finite natural-membered set st k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l holds
m < n

proof end;

theorem AE220: :: AFINSQ_2:45

for X, Y being finite natural-membered set st X <> {} & X <N< Y holds
(Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0

proof end;

theorem :: AFINSQ_2:46

for X, Y being finite natural-membered set holds
( X <N< Y iff Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) )

proof end;

definition

let f be XFinSequence;
let B be set ;
func SubXFinS f,B -> XFinSequence equals :: AFINSQ_2:def 8
f * (Sgm0 (B /\ (len f)));
coherence
f * (Sgm0 (B /\ (len f))) is XFinSequence

proof end;

end;

:: deftheorem defines SubXFinS AFINSQ_2:def 8 :

for f being XFinSequence
for B being set holds SubXFinS f,B = f * (Sgm0 (B /\ (len f)));

theorem AC200: :: AFINSQ_2:47

for f being XFinSequence
for B being set holds
( len (SubXFinS f,B) = card (B /\ (len f)) & ( for i being Nat st i < len (SubXFinS f,B) holds
(SubXFinS f,B) . i = f . ((Sgm0 (B /\ (len f))) . i) ) )

proof end;

definition

let D be set ;
let f be XFinSequence of D;
let B be set ;
:: original: SubXFinS
redefine func SubXFinS f,B -> XFinSequence of D;
coherence
SubXFinS f,B is XFinSequence of D

proof end;

end;

registration

let f be XFinSequence;
cluster SubXFinS f,{} -> empty ;
coherence
SubXFinS f,{} is empty

proof end;

end;

registration

let B be set ;
cluster SubXFinS {} ,B -> empty ;
coherence
SubXFinS {} ,B is empty ;

end;

theorem :: AFINSQ_2:48

for B1, B2 being finite natural-membered set
for f being XFinSequence of REAL st B1 <N< B2 holds
Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))

proof end;