Re: [mizar] Re: strict

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> 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.

It turns out that transposing RLVECT_1 and VECTSP_1 in the
constructors directive doesn't eliminate the *4.  Are there some other
"strict"'s that are being imported here that I don't know about?  How
did you find out that it was the order of RLVECT_1 and VECTSP_1 that
might be the source of the problem?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*10: Too many basic sentences in an inference