Re: WELLFND1:1

Hi Andrzej,

Right you are. I was probably annoyed to find a generally useful theorem 
about functions in an article on well-foundedness, and guessed too quickly 
that it could also use some generalization. If I bothered to prove it, 
I'd experience one of the bright sides of verification - proving false 
things becomes difficult :-).

I'd rather suggest moving the theorem to some article about functions, or 
changing the comment appropriately and leaving it there until the moving is done.

Best,
Josef


On Wed, 8 Oct 2008, trybulec wrote:

> A comment in OSALG_1:
>
> :: REVISE:: WELLFND1:1 should be generalised to Relation and moved to RELAT_1
>
> The problem is that WELLFND1:1
>
> theorem :: WELLFND1:1
> for X being set, f, g being Function st f c= g & X c= dom f holds f|X = g|X
>
> is not true for Relations, e.g.
>
>   f = { [1,2] }   g = {[1,2],[1,3]}  X = {1}
>
> So, I have removed the comment.
>
> Regards,
> Andrzej
>
>
>