WELLFND1:1

[trybulec]

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

[Josef Urban]

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
>
>
>

[trybulec]

Josef Urban wrote:

>
> 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.

I have moved it to GRFUNC_1.  (In the proof a theorem  from GRFUNC_1 is
used. I tried to generalize it, too.
With the same result).

Regards,
Andrzej