Re: [mizar] 'Environmental' problems

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Dear Boris,

On Wed, 31 Mar 2010, [KOI8-R] âÏÒÉÓ ûÍÉÎËÅ wrote:

> So, what I have:
> environ
>  vocabularies ARYTM_3, NAT_1;
>  notations    ARYTM_3, NAT_1;
>  constructors ARYTM_3, NAT_1;
>  registrations NAT_1;
> begin
>  reserve x, y for Nat;
>  theorem x + y = x + y
> ::>         *103    *103
>  proof
>  end;
> ::> 103: Unknown functor

Try with the following environment (explanation follows):

environ
  vocabularies ARYTM_3,NAT_1;
  notations    XCMPLX_0,NAT_1;
  constructors NAT_1;
  registrations XCMPLX_0;
begin
  reserve x, y for Nat;

  theorem x + y = x + y
  proof
  end;
::> *70

::> 70: Something remains to be proved

> I've added 'registrations NAT_1' line because there is a cluster:
> registration
>  let n,k be Nat;
>  cluster n + k -> natural;
> end;
> in NAT_1. So I expected, that it would be enough, but it wasn't.
> Could you explain me, why the functor '+' is still unknown? How to
> correct the situation and why it will be correct?

It's XCMPLX_0 and not NAT_1 that introduces the notation of addition of 
numbers (the definition in NAT_1 has arguments of type 'Element of NAT').
So without the proper notation, the registration you have is not used.

Regards,

Adam Naumowicz

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================