[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Why I cannot quote a theorem
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