Re: [mizar] widening BinOp to Relation

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

On Fri, 2 Feb 2007, Jesse Alama wrote:

> > It seems that you don't have RELSET_1 present among your registrations
> > directives. Tracing back the widening relation of BinOp of A one comes
> > to Subset of [:A,A:] which is Relation-like only in the presence of a
> > suitable registration from RELSET_1 - the first one.
> >
> > Please let me know if this solved the problem.
>
> You were right -- including RELSET_1 in the registrations directive
> solved the problem.  How did you know to look at RELSET_1?

Expanding the mode 'BinOp of A' we get 'Function of [:A,A:],A', which in 
turn expands to 'quasi_total PartFunc of [:A,A:],A', and this means
'Function-like Relation of [:A,A:],A' which is eventually redefined as 
'Subset of [:[:A,A:],A:]' in RELSET_1. The registration that follows this 
redefinition completes the job - providing the 'Relation-like' attribute:

registration let X,Y;
 cluster -> Relation-like Subset of [:X,Y:];
end;

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/
======================================================================