Re: [mizar] reductions in Mizar

[Josef Urban <josef.urban@gmail.com>]

On 1/31/12, Artur Kornilowicz <arturk@math.uwb.edu.pl> wrote:
> On Wed, 25 Jan 2012, trybulec@math.uwb.edu.pl wrote:
>
>>>> registration
>>>>    let x_1,...,x_n;
>>>>    reduce term1(x_1,...,x_n) to term2(x_1,...,x_n);
>>>>    reducibility
>>>>    proof
>>>>      thus term1(x_1,...,x_n) = term2(x_1,...,x_n);
>>>>    end;
>>>> end;
>>>
>>> I never remember the "correctness condition" keywords (coherence,
>>> compatibility, etc) used in different contexts. I just looked up the
>>> keyword used for "identify", and it is "compatibility".
>
>
> "correctness" can be used instead of "coherence", "compatibility",
> "reducibility", etc.

http://en.wikiquote.org/wiki/William_of_Occam

Josef

>
> Artur
>
>