[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Re: strict



On Tue, 9 Jan 2007, Jesse Alama wrote:

The error definitely lies with the theorem, not with the summaries of
the error messages at the bottom of the file:

theorem
F2 is strict;
::>        *4

Yes, it couldn't be that easy ;-)

Here's my environment; it's nasty:

vocabularies FINSET_1, POLYFORM, FUNCT_1, FUNCT_2, ZFMISC_1, CARD_1, SUBSET_1, TARSKI, BOOLE, MCART_1, RELAT_1, NAT_1, XCMPLX_0, ORDINAL2, VECTSP_1, VECTSP_9, INT_1, BINOP_1, MCART_2, RLVECT_1, GROUP_1; notations FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, CARD_1, SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, XCMPLX_0, ORDINAL2, VECTSP_1, VECTSP_9, INT_1, STRUCT_0, BINOP_1, LATTICES, MCART_2, RLVECT_1, GROUP_1; constructors FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, CARD_1, ZFMISC_1, SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, ORDINAL2, VECTSP_1, VECTSP_9, INT_1, STRUCT_0, BINOP_1, LATTICES, MCART_2, FRAENKEL, ENUMSET1, RLVECT_1, GROUP_1; registrations FRAENKEL, FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1, SUBSET_1, NAT_1, INT_1, VECTSP_1, STRUCT_0;
requirements NUMERALS, BOOLE, ARITHM, SUBSET;
definitions XBOOLE_0, RELAT_1, FUNCT_1, SUBSET_1, FUNCT_2, MCART_2, ENUMSET1, RLVECT_1, BINOP_1, STRUCT_0, GROUP_1; theorems XBOOLE_0, FUNCT_1, RELAT_1, XBOOLE_1, TARSKI, ZFMISC_1, MCART_1, SUBSET_1, FUNCT_2, MCART_2, ENUMSET1, BINOP_1, STRUCT_0, GROUP_1; schemes FUNCT_1, BINOP_1;

Could it be that something in my environment is messed up?

Exactly - the offending part are the notations imported from RLVECT_1 after VECTSP_1 - this way your "strict" is the one automagically defined for LoopStr instead for doubleLoopStr! The order of imported notations is relevant, and it's best to use the 'mml.lar' list to control it - please see the thread at:

http://mizar.uwb.edu.pl/forum/archive/0609/msg00071.html

If your work dosn't depend on this unfortunate transposition, you should be able to just change the order of these two directives without any other changes to your article and get rid of the *4.

Best,
Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================