Re: reductions in Mizar

On 1/31/12, Artur Kornilowicz <[email protected]> wrote:
> On Wed, 25 Jan 2012, [email protected] 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
>
>