Re: reductions in Mizar

Hi:

One may only reduce a term to a subterm. Because of this the reduction 
does not enlarge the universe of discourse. So, maybe 'reducibility' is 
not so bad.

Regards,
Andrzej

Cytowanie Freek Wiedijk <[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
>