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