Re: [Rodin-b-sharp-user] Witness in INITIALISATION for two linked disappearing variables

[Mathieu C. <mat...@sy...>]

On Mon, Feb 23, 2009 at 12:10 PM, Matthias Schmalz <
Mat...@in...> wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> How about the following witnesses:
>
> x': x' = z'
> and
> y': y' = z'

Ah, yes, I've overlooked that simple solution ! Thanks :-)


> I have not checked, but I think there is currently no way to give your
> gluing invariant itself as a witness.

Son confirmed that it is not possible for now.

-Mathieu

--
_________________________________________________________________________
SYSTEREL     mailto:mat...@sy...    http://www.systerel.fr
Porte de l'Arbois - Bât A, 1090 rue René Descartes,   tel: 04 42 90 65 51
13857 Aix En Provence - cedex 3                       fax: 04 42 90 41 29
           F2F5 442F F2AC E1D5 9D31  3EFC 842A BC4A 123B 9A65