Re: A question about rng being non empty

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

Hi,

Piotr Rudnicki wrote:

>I cannot get rid of these errors:
>    consider g being non empty Function;
> ::>                                  *136

If on the page

  http://megrez.mizar.org/services/ency

in the search window you write

at least(SUBSET_1:attr 1,RELAT_1:attr 1,FUNCT_1:attr 1,HIDDEN:mode
1)|exreg

and click on search button you will get 74 existential registrations
including empty (SUBSET_1:attr 1), Relation-like (RELAT_1:attr 1),
Function-like (FUNCT_1:attr 1), and set (HIDDEN:mode 1).
Type "Function" is an abbreviation of "Function-like Relation-like set".
Among them
AMISTD_1:exreg 1
CLOSURE2:exreg 1
FINSEQ_5:exreg 1
FUNCT_7:exreg1, exreg 2
POLYNOM1:exreg 9
PRVECT_1:exreg 1, exreg 2
SPRECT_1:exreg 1
TREES_3:exreg 5, exreg 6, exreg 7, exreg 8
YELLOW_6:exreg 1, exreg 3

Maybe, the best choice is PRVECT_1 because it includes only attribute
FinSequence-like more than you want. Or proposed by Artur YELLOW_6
which includes extra attribute constant. Other registrations may
need to add more constructor files.

>    consider h being non empty Function of NAT, NAT;
> ::>                                  *136

Try: 
 at least(SUBSET_1:attr 1,RELAT_1:attr 1,FUNCT_1:attr 1,RELSET_1:mode
1)|exreg

And you will get 7 registrations with PUA2MSS1:exreg 1 which you need.

>    consider f being Function of NAT,NAT;
>    rng f is non empty;
> ::>                 *4

Try:
 at least(SUBSET_1:attr 1,RELAT_1:attr 1,RELAT_1:func 2)|funcreg

And you get INDEX_1 and PUA2MSS1.

Best regards,
Grzegorz