:: PRGCOR_2 semantic presentation

Lemma1: for b₁ being set
for b₂ being Nat st b₁ in b₂ holds
b₁ is Nat

proof end;

theorem Th1: :: PRGCOR_2:1

for b₁, b₂ being Nat holds
( b₁ in b₂ iff b₁ < b₂ )

proof end;

Lemma3: for b₁ being XFinSequence
for b₂ being set holds
( rng b₁ c= b₂ iff b₁ is XFinSequence of b₂ )
by ORDINAL1:def 8;

registration

let c₁ be non empty set ;
cluster non empty T-Sequence of a₁;
existence

proof end;

end;

theorem Th2: :: PRGCOR_2:2

for b₁ being non empty set
for b₂ being non empty XFinSequence of b₁ holds len b₂ > 0

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
func FS2XFS c₂ -> XFinSequence of a₁ means :Def1: :: PRGCOR_2:def 1
( len a₃ = len a₂ & ( for b₁ being Nat st b₁ < len a₂ holds
a₂ . (b₁ + 1) = a₃ . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines FS2XFS PRGCOR_2:def 1 :

definition

let c₁ be set ;
let c₂ be XFinSequence of c₁;
func XFS2FS c₂ -> FinSequence of a₁ means :: PRGCOR_2:def 2
( len a₃ = len a₂ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₂ holds
a₂ . (b₁ -' 1) = a₃ . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines XFS2FS PRGCOR_2:def 2 :

theorem Th3: :: PRGCOR_2:3

for b₁ being Nat
for b₂ being set holds b₁ --> b₂ is XFinSequence

proof end;

theorem Th4: :: PRGCOR_2:4

for b₁ being set
for b₂ being Nat
for b₃ being set st b₃ in b₁ holds
( b₂ --> b₃ is XFinSequence of b₁ & ( for b₄ being XFinSequence st b₄ = b₂ --> b₃ holds
len b₄ = b₂ ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be Nat;
assume E8: ( c₃ > len c₂ & NAT c= c₁ ) ;
func FS2XFS* c₂,c₃ -> non empty XFinSequence of a₁ means :Def3: :: PRGCOR_2:def 3
( len a₂ = a₄ . 0 & len a₄ = a₃ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₂ holds
a₄ . b₁ = a₂ . b₁ ) & ( for b₁ being Nat st len a₂ < b₁ & b₁ < a₃ holds
a₄ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines FS2XFS* PRGCOR_2:def 3 :

definition

let c₁ be non empty set ;
let c₂ be non empty XFinSequence of c₁;
assume E9: ( NAT c= c₁ & c₂ . 0 is Nat & c₂ . 0 in len c₂ ) ;
func XFS2FS* c₂ -> FinSequence of a₁ means :Def4: :: PRGCOR_2:def 4
for b₁ being Nat st b₁ = a₂ . 0 holds
( len a₃ = b₁ & ( for b₂ being Nat st 1 <= b₂ & b₂ <= b₁ holds
a₃ . b₂ = a₂ . b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines XFS2FS* PRGCOR_2:def 4 :

theorem Th5: :: PRGCOR_2:5

for b₁ being non empty set
for b₂ being non empty XFinSequence of b₁ st NAT c= b₁ & b₂ . 0 = 0 & 0 < len b₂ holds
XFS2FS* b₂ = {}

proof end;

definition

let c₁ be non empty set ;
let c₂ be XFinSequence of c₁;
let c₃ be FinSequence of c₁;
pred c₂ is_an_xrep_of c₃ means :Def5: :: PRGCOR_2:def 5
( NAT c= a₁ & a₂ . 0 = len a₃ & len a₃ < len a₂ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₃ holds
a₂ . b₁ = a₃ . b₁ ) );

end;

:: deftheorem Def5 defines is_an_xrep_of PRGCOR_2:def 5 :

theorem Th6: :: PRGCOR_2:6

for b₁ being non empty set
for b₂ being non empty XFinSequence of b₁ st NAT c= b₁ & b₂ . 0 is Nat & b₂ . 0 in len b₂ holds
b₂ is_an_xrep_of XFS2FS* b₂

proof end;

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
func IFLGT c₁,c₂,c₃,c₄,c₅ -> set equals :Def6: :: PRGCOR_2:def 6
a₃ if a₁ in a₂
a₄ if a₁ = a₂
otherwise a₅;
correctness ;

end;

:: deftheorem Def6 defines IFLGT PRGCOR_2:def 6 :

theorem Th7: :: PRGCOR_2:7

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat st NAT c= b₁ & b₃ > len b₂ holds
ex b₄ being XFinSequence of b₁ st
( len b₄ = b₃ & b₄ is_an_xrep_of b₂ )

proof end;

definition

let c₁ be XFinSequence of REAL ;
let c₂ be Nat;
redefine func . as c₁ . c₂ -> Real;
coherence

proof end;

end;

definition

let c₁, c₂ be XFinSequence of REAL ;
assume E14: ( c₂ . 0 is Nat & 0 <= c₂ . 0 & c₂ . 0 < len c₁ ) ;
func inner_prd_prg c₁,c₂ -> Real means :Def7: :: PRGCOR_2:def 7
ex b₁ being XFinSequence of REAL ex b₂ being Integer st
( len b₁ = len a₁ & b₁ . 0 = 0 & b₂ = a₂ . 0 & ( b₂ <> 0 implies for b₃ being Nat st b₃ < b₂ holds
b₁ . (b₃ + 1) = (b₁ . b₃) + ((a₁ . (b₃ + 1)) * (a₂ . (b₃ + 1))) ) & a₃ = b₁ . b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines inner_prd_prg PRGCOR_2:def 7 :

theorem Th8: :: PRGCOR_2:8

for b₁ being FinSequence of REAL
for b₂ being XFinSequence of REAL st len b₂ > len b₁ & b₂ . 0 = 0 & ( for b₃ being Nat st b₃ < len b₁ holds
b₂ . (b₃ + 1) = (b₂ . b₃) + (b₁ . (b₃ + 1)) ) holds
Sum b₁ = b₂ . (len b₁)

proof end;

theorem Th9: :: PRGCOR_2:9

for b₁ being FinSequence of REAL ex b₂ being XFinSequence of REAL st
( len b₂ = (len b₁) + 1 & b₂ . 0 = 0 & ( for b₃ being Nat st b₃ < len b₁ holds
b₂ . (b₃ + 1) = (b₂ . b₃) + (b₁ . (b₃ + 1)) ) & Sum b₁ = b₂ . (len b₁) )

proof end;

theorem Th10: :: PRGCOR_2:10

for b₁, b₂ being FinSequence of REAL
for b₃ being Nat st len b₁ = len b₂ & b₃ > len b₁ holds
|(b₁,b₂)| = inner_prd_prg (FS2XFS* b₁,b₃),(FS2XFS* b₂,b₃)

proof end;

definition

let c₁, c₂ be XFinSequence of REAL ;
let c₃ be Real;
let c₄ be Integer;
pred c₄ scalar_prd_prg c₂,c₃,c₁ means :Def8: :: PRGCOR_2:def 8
( len a₂ = a₄ & len a₁ = a₄ & ex b₁ being Integer st
( a₂ . 0 = a₁ . 0 & b₁ = a₁ . 0 & ( b₁ <> 0 implies for b₂ being Nat st 1 <= b₂ & b₂ <= b₁ holds
a₂ . b₂ = a₃ * (a₁ . b₂) ) ) );

end;

:: deftheorem Def8 defines scalar_prd_prg PRGCOR_2:def 8 :

theorem Th11: :: PRGCOR_2:11

for b₁ being non empty XFinSequence of REAL
for b₂ being Real
for b₃ being Nat st b₁ . 0 is Nat & len b₁ = b₃ & 0 <= b₁ . 0 & b₁ . 0 < b₃ holds
( ex b₄ being XFinSequence of REAL st b₃ scalar_prd_prg b₄,b₂,b₁ & ( for b₄ being non empty XFinSequence of REAL st b₃ scalar_prd_prg b₄,b₂,b₁ holds
XFS2FS* b₄ = b₂ * (XFS2FS* b₁) ) )

proof end;

definition

let c₁, c₂ be XFinSequence of REAL ;
let c₃ be Integer;
pred c₃ vector_minus_prg c₂,c₁ means :Def9: :: PRGCOR_2:def 9
( len a₂ = a₃ & len a₁ = a₃ & ex b₁ being Integer st
( a₂ . 0 = a₁ . 0 & b₁ = a₁ . 0 & ( b₁ <> 0 implies for b₂ being Nat st 1 <= b₂ & b₂ <= b₁ holds
a₂ . b₂ = - (a₁ . b₂) ) ) );

end;

:: deftheorem Def9 defines vector_minus_prg PRGCOR_2:def 9 :

theorem Th12: :: PRGCOR_2:12

for b₁ being non empty XFinSequence of REAL
for b₂ being Nat st b₁ . 0 is Nat & len b₁ = b₂ & 0 <= b₁ . 0 & b₁ . 0 < b₂ holds
( ex b₃ being XFinSequence of REAL st b₂ vector_minus_prg b₃,b₁ & ( for b₃ being non empty XFinSequence of REAL st b₂ vector_minus_prg b₃,b₁ holds
XFS2FS* b₃ = - (XFS2FS* b₁) ) )

proof end;

definition

let c₁, c₂, c₃ be XFinSequence of REAL ;
let c₄ be Integer;
pred c₄ vector_add_prg c₃,c₁,c₂ means :Def10: :: PRGCOR_2:def 10
( len a₃ = a₄ & len a₁ = a₄ & len a₂ = a₄ & ex b₁ being Integer st
( a₃ . 0 = a₂ . 0 & b₁ = a₂ . 0 & ( b₁ <> 0 implies for b₂ being Nat st 1 <= b₂ & b₂ <= b₁ holds
a₃ . b₂ = (a₁ . b₂) + (a₂ . b₂) ) ) );

end;

:: deftheorem Def10 defines vector_add_prg PRGCOR_2:def 10 :

theorem Th13: :: PRGCOR_2:13

for b₁, b₂ being non empty XFinSequence of REAL
for b₃ being Nat st b₂ . 0 is Nat & len b₁ = b₃ & len b₂ = b₃ & b₁ . 0 = b₂ . 0 & 0 <= b₂ . 0 & b₂ . 0 < b₃ holds
( ex b₄ being XFinSequence of REAL st b₃ vector_add_prg b₄,b₁,b₂ & ( for b₄ being non empty XFinSequence of REAL st b₃ vector_add_prg b₄,b₁,b₂ holds
XFS2FS* b₄ = (XFS2FS* b₁) + (XFS2FS* b₂) ) )

proof end;

definition

let c₁, c₂, c₃ be XFinSequence of REAL ;
let c₄ be Integer;
pred c₄ vector_sub_prg c₃,c₁,c₂ means :Def11: :: PRGCOR_2:def 11
( len a₃ = a₄ & len a₁ = a₄ & len a₂ = a₄ & ex b₁ being Integer st
( a₃ . 0 = a₂ . 0 & b₁ = a₂ . 0 & ( b₁ <> 0 implies for b₂ being Nat st 1 <= b₂ & b₂ <= b₁ holds
a₃ . b₂ = (a₁ . b₂) - (a₂ . b₂) ) ) );

end;

:: deftheorem Def11 defines vector_sub_prg PRGCOR_2:def 11 :

theorem Th14: :: PRGCOR_2:14

for b₁, b₂ being non empty XFinSequence of REAL
for b₃ being Nat st b₂ . 0 is Nat & len b₁ = b₃ & len b₂ = b₃ & b₁ . 0 = b₂ . 0 & 0 <= b₂ . 0 & b₂ . 0 < b₃ holds
( ex b₄ being XFinSequence of REAL st b₃ vector_sub_prg b₄,b₁,b₂ & ( for b₄ being non empty XFinSequence of REAL st b₃ vector_sub_prg b₄,b₁,b₂ holds
XFS2FS* b₄ = (XFS2FS* b₁) - (XFS2FS* b₂) ) )

proof end;