environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, AFINSQ_1, SUBSET_1, TARSKI, CARD_1, FUNCT_1, RELAT_1, ORDINAL1, FINSEQ_1, XXREAL_0, ARYTM_3, ARYTM_1, FUNCOP_1, ORDINAL4, REAL_1, INT_1, CARD_3, PARTFUN1, RVSUM_1, FINSEQ_2, PRGCOR_2, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, CARD_1, ORDINAL4, XREAL_0, REAL_1, VALUED_0, XCMPLX_0, NAT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, AFINSQ_1, INT_1, RVSUM_1, NAT_D, FINSEQ_2, XXREAL_0;
definitions TARSKI;
theorems FUNCT_1, NAT_1, RELAT_1, ORDINAL1, FINSEQ_1, FUNCOP_1, AFINSQ_1, RVSUM_1, FINSEQ_4, FINSEQ_2, XREAL_1, XXREAL_0, PARTFUN1, VALUED_1, XREAL_0, FINSEQ_5, CARD_1, NUMBERS, TARSKI;
schemes NAT_1, AFINSQ_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, AFINSQ_1, VALUED_0, FINSEQ_2, CARD_1;
constructors HIDDEN, XXREAL_0, REAL_1, NAT_1, PARTFUN1, NAT_D, AFINSQ_1, BINOP_2, INT_1, VALUED_1, RVSUM_1, RELSET_1, ORDINAL4, FUNCOP_1, FUNCT_7, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities CARD_1, ORDINAL1;
expansions TARSKI;
::
deftheorem Def2 defines
IFLGT PRGCOR_2:def 2 :
for x being object
for y being set
for a, b, c being object 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 ) );
::#define V_SIZE 1024
:: float inner_prd_prg(float a[V_SIZE],float b[V_SIZE]){
:: int n,i; float s[V_SIZE];
:: s[0]=0;
:: n=(int)(b[0]);
:: if (n != 0)
:: { for(i=0;i<n;i++)s[i+1]=s[i]+a[i+1]*b[i+1];
:: }
:: return s[n];
:: }