[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] reductions in Mizar



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