begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem PRGCOR_2:def 1 :
canceled;
:: deftheorem PRGCOR_2:def 2 :
canceled;
:: deftheorem PRGCOR_2:def 3 :
canceled;
:: deftheorem PRGCOR_2:def 4 :
canceled;
:: deftheorem Def5 defines is_an_xrep_of PRGCOR_2:def 5 :
for D being non empty set
for p being XFinSequence of
for q being FinSequence of D holds
( p is_an_xrep_of q iff ( NAT c= D & p . 0 = len q & len q < len p & ( for i being Nat st 1 <= i & i <= len q holds
p . i = q . i ) ) );
theorem
:: deftheorem Def6 defines IFLGT PRGCOR_2:def 6 :
for x, y, a, b, c being set holds
( ( x in y implies IFLGT (x,y,a,b,c) = a ) & ( x = y implies IFLGT (x,y,a,b,c) = b ) & ( not x in y & not x = y implies IFLGT (x,y,a,b,c) = c ) );
theorem Th7:
:: deftheorem Def7 defines inner_prd_prg PRGCOR_2:def 7 :
for a, b being XFinSequence of st b . 0 is Nat & b . 0 < len a holds
for b3 being Real holds
( b3 = inner_prd_prg (a,b) iff ex s being XFinSequence of ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b3 = s . n ) );
theorem Th8:
theorem
theorem
:: deftheorem Def8 defines scalar_prd_prg PRGCOR_2:def 8 :
for b, c being XFinSequence of
for a being Real
for m being Integer holds
( m scalar_prd_prg c,a,b iff ( len c = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = a * (b . i) ) ) ) );
theorem
:: deftheorem Def9 defines vector_minus_prg PRGCOR_2:def 9 :
for b, c being XFinSequence of
for m being Integer holds
( m vector_minus_prg c,b iff ( len c = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = - (b . i) ) ) ) );
theorem
:: deftheorem Def10 defines vector_add_prg PRGCOR_2:def 10 :
for a, b, c being XFinSequence of
for m being Integer holds
( m vector_add_prg c,a,b iff ( len c = m & len a = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) + (b . i) ) ) ) );
theorem
:: deftheorem Def11 defines vector_sub_prg PRGCOR_2:def 11 :
for a, b, c being XFinSequence of
for m being Integer holds
( m vector_sub_prg c,a,b iff ( len c = m & len a = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) - (b . i) ) ) ) );
theorem