Re: reductions in Mizar

Freek Wiedijk <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]> 
Dear all,

FWIW: "reducibility" means the property that something _can_
be reduced.  This property might be called "convertibility",
but I also favor the proposal to reuse an existing keyword.

So the obvious question: what happens when the reductions
do now terminate?  For example if I register "reduce f(x)
to f(f(x))"?

Freek
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.