[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Why I cannot quote a theorem
Piotr,
put notation FVSUM_1 after POLYNOM_1. And see
definition
let L be non empty HGrStr,
a be Element of the carrier of L,
p be FinSequence of the carrier of L;
func a*p -> FinSequence of the carrier of L means
:: POLYNOM1:def 2
dom it = dom p &
for i being set st i in dom p holds it/.i = a*(p/.i);
end;
definition let K be non empty HGrStr;
let p be FinSequence of the carrier of K;
let a be Element of the carrier of K;
func a*p -> FinSequence of the carrier of K equals
:: FVSUM_1:def 6
(a multfield)*p;
end;
Artur
On Sat, 29 Nov 2003,
Piotr
Rudnicki
wrote:
> Hi:
>
> In the text below I am unable to quote a theorem. Why?
>
>
> --
> Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
> http://web.cs.ualberta.ca/~piotr
>
> ------------------
>
> environ
>
> vocabulary ARYTM_0, ARYTM_1, ARYTM, ARYTM_2, XCMPLX_0, XREAL_0, SQUARE_1,
> OPPCAT_1, ARYTM_3, FINSEQ_1, RELAT_1, FUNCT_1, RLVECT_1, BOOLE, FINSEQ_2,
> FINSEQ_4, HAHNBAN1, COMPLEX1, BINOP_1, VECTSP_1, LATTICES, NORMSP_1,
> COMPLFLD, GROUP_1, REALSET1, POWER, POLYNOM1, ORDINAL2, ORDINAL1, INT_1,
> INT_2, INT_3, NAT_1, RAT_1, TARSKI, CARD_1, GROUP_2, CARD_3, SETWISEO,
> ALGSEQ_1, POLYNOM3, POLYNOM2, ALGSTR_2, FUNCT_4, VECTSP_2, CQC_LANG,
> FCONT_1, FUNCOP_1, PRE_TOPC, SEQ_1, FUNCT_2, QC_LANG1, PARTFUN1, SEQ_4,
> SEQ_2, COMSEQ_1, SEQM_3, COMPTRIG, RFINSEQ, ABSVALUE, POLYNOM5, UNITY,
> COMPLSP1, SIN_COS, RVSUM_1, FVSUM_1, PREPOWER, GR_CY_1, FINSET_1, NEWTON,
> MCART_1, SGRAPH1, MOD_2, GRAPH_2, CAT_1, DTCONSTR, PRALG_1, PBOOLE,
> MEMBERED;
> notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, NUMBERS, ARYTM_0, XCMPLX_0,
> XREAL_0, ZFMISC_1, REAL_1, SQUARE_1, INT_1, INT_2, NAT_1, ABSVALUE,
> POWER, RLVECT_1, CARD_3, VECTSP_1, VECTSP_2, BINOP_1, RELAT_1, FUNCT_1,
> FUNCT_2, FINSEQ_1, RAT_1, FINSEQ_2, FINSEQ_4, FINSOP_1, PARTFUN1,
> TOPREAL1, COMPLEX1, NORMSP_1, BINARITH, RVSUM_1, FVSUM_1, ALGSEQ_1,
> COMPLFLD, HAHNBAN1, POLYNOM3, POLYNOM4, POLYNOM5, COMPTRIG,
> CARD_1, COMPLSP1, GROUP_2, SIN_COS, PREPOWER, FINSET_1, GROUP_1,
> WELLFND1, MCART_1, PRE_CIRC, MOD_2, ENUMSET1, GRAPH_2, FUNCT_4, ORDINAL1,
> RLVECT_2, CQC_LANG, GROUP_6, DTCONSTR, RFINSEQ, PRALG_1, POLYNOM1,
> WSIERP_1, PBOOLE, SEQM_3, MEMBERED;
> constructors ARYTM_0, ARYTM_1, REAL_1, FINSOP_1, POWER, MONOID_0, ALGSTR_2,
> WELLORD2, INT_2, TOPREAL1, COMPLSP1, BINARITH, HAHNBAN1, POLYNOM1,
> POLYNOM4, COMPTRIG, COMPLEX1, GROUP_2, FVSUM_1, SIN_COS, POLYNOM5,
> PREPOWER, SETWOP_2, MEMBERED, WELLFND1, DOMAIN_1, PRE_CIRC, FINSEQOP,
> ALGSTR_1, MOD_2, ENUMSET1, GRAPH_2, FUNCT_4, NUMBERS, FRAENKEL, ORDINAL1,
> RLVECT_2, CQC_LANG, GROUP_6, DTCONSTR, POLYNOM2, RFINSEQ, WSIERP_1,
> PRALG_1;
> clusters XREAL_0, STRUCT_0, RELSET_1, FINSEQ_5, SEQ_1, BINARITH,
> VECTSP_1, VECTSP_2,
> GROUP_1, FINSEQ_2, COMPLFLD, POLYNOM1, POLYNOM3, MONOID_0, NAT_1, INT_1,
> COMPLEX1, POLYNOM5, FINSEQ_1, FINSET_1, CARD_1, FSM_1, MEMBERED, FUNCT_1,
> ALGSTR_1, MOD_2, NUMBERS, XBOOLE_0, ARYTM_2, SUBSET_1, ORDINAL2, ARYTM_3,
> FRAENKEL, FUNCT_2, FUNCT_4, ZFMISC_1, ORDINAL1, WSIERP_1, CQC_LANG,
> DTCONSTR, RFINSEQ, PRALG_1, GOBRD13, CARD_3, POLYRED, PRE_CIRC,
> POLYNOM4, FVSUM_1;
> requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
> definitions TARSKI, GROUP_1, VECTSP_1, XBOOLE_0, FUNCT_1, ALGSEQ_1,
> POLYNOM5;
> theorems STRUCT_0, GROUP_1, CARD_1, FINSEQ_1, ZFMISC_1, NAT_1, FUNCT_1,
> FUNCT_2, RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, VECTSP_1, PREPOWER,
> RELSET_1, COMPTRIG, COMPLFLD, COMPLSP1, BINOP_1, REAL_1, XCMPLX_1,
> GROUP_4, COMPLEX1, HAHNBAN1, SIN_COS, POWER, REAL_2, SIN_COS2, POLYNOM5,
> RAT_1, CFUNCT_1, BINARITH, INT_1, COMPLEX2, XCMPLX_0, XREAL_0, SCMFSA_7,
> AMI_5, AXIOMS, INT_3, SQUARE_1, JGRAPH_2, RVSUM_1, FVSUM_1, FINSEQ_3,
> FINSEQ_2, FINSEQ_4, POLYNOM4, GR_CY_1, SETWISEO, INT_2, SCMFSA9A,
> SCPINVAR, ABSVALUE, NAT_LAT, WSIERP_1, NAT_2, PEPIN, POLYNOM3, COMPUT_1,
> NORMSP_1, FUNCT_7, ALGSEQ_1, RLVECT_1, NEWTON, POLYNOM2, FINSET_1,
> CARD_4, PBOOLE, FUNCOP_1, POLYNOM1, MATRIX_3, PRE_CIRC, VECTSP_2, MOD_2,
> CARD_2, GRAPH_2, FINSEQ_5, PRE_FF, ARYTM_0, GRAPH_5, QC_LANG4, SUBSET_1,
> CQC_LANG, DTCONSTR, BAGORDER, RFINSEQ, GOBOARD9, HILBASIS, WELLORD2,
> CARD_3, GCD_1, ORDINAL2, TOPREAL1, FSM_1;
> schemes BINARITH, NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, PRE_CIRC, FRAENKEL,
> MATRIX_2, POLYNOM2, INT_2, DOMAIN_1, ALGSEQ_1;
>
> begin
>
> ::theorem :: FVSUM_1:92
> for K being Abelian add-associative right_zeroed
> right_complementable distributive(non empty doubleLoopStr),
> a being Element of the carrier of K,
> p being FinSequence of the carrier of K holds
> Sum(a*p) = a*(Sum p) by FVSUM_1:92;
> ::> *4
> ::>
> ::> 4: This inference is not accepted
>
=======================================
Artur Kornilowicz e-mail: arturk@math.uwb.edu.pl
Dept. of Applied Logic http://math.uwb.edu.pl/~arturk/
Institute of Computer Science fax. +48 (85) 745-7662
University of Bialystok tel. +48 (85) 745-7559 (office)
Sosnowa 64 +48 (85) 651-6193 (home)
15-887 Bialystok, Poland