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

Re: [mizar] reductions in Mizar

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. 

Artur