Re: [mizar] structures

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

I meant that is (ground) terms
    the fixed theta_1 of  args_1      and
    the fixed theta_2 of args_2
occur in an inference, and
    the fixed theta_1 of arg_1 is theta_2 of args_2
occurs in the inference, too, then
      the fixed theta_1 of  args_1  = the fixed theta_2 of args_2
is appended to the premises. I would rather restrict it to the case when
    'the fixed theta_2 of  args_2'   widens to   'the fixed theta_1 of args_1'.   (*)

It looks like other "additional inference rules" added to the obviousness, so it is
nothing special.

With the (*) restriction (and without additional requirements) it is not particularly
useful. I guess the usefulness restricted to the modes with the definiens 'not
contradiction', that we plan to eliminate anyway. If we accept the requirements
     the fixed set = {}
then we will get automatically
     the fixed Subset of X = {}
     the fixed Function = {}
and even
     the fixed PartFunc of A,B = {}.
So it may be useful.

Andrzej




Josef Urban wrote:

> One more thing: this cannot be a fixed rule users could rely on, since the
> "is" statement can generally be undecidable. Just a rule of thumb.
>
> Josef