Re: [Rodin-b-sharp-user] Proof Rules and WD strictness

[Matthias S. <Mat...@in...>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear Laurent,

a request for clarification:

In SUBSET_INTER you require the side-condition:
"where \mathbf{T} and \mathbf{U} are not bound by \mathbf{G}"

I have always assumed that
P(u) represents a term of the form P[x := u].
In that case your side-condition is superfluous.

Do you agree? If not, what is your interpretation of P(u)?

- -Matthias


Laurent Voisin schrieb:
> Dear fellow Rodin users,
> 
> I've just changed some inference rules in the Rodin wiki, where the  
> notion of "top-level" occurrence has been replaced with:
> 
>    - either a WD strictness condition, see [1],
> 
>    - or a freeness condition,
> 
>    - or nothing when the condition was useless.
> 
> This removes from the documentation this notion of "top-level" which  
> was not formally defined and difficult to grasp.
> 
> The rules that have changed are:
> 
>    FUN_IMAGE_GOAL
>    SUBSET_INTER
>    IN_INTER
>    NOTIN_INTER
>    OV_SETENUM_L
>    OV_SETENUM_R
>    OV_L
>    OV_R
>    DIS_BINTER_R
>    DIS_BINTER_L
>    DIS_SETMINUS_R
>    DIS_SETMINUS_L
>    SIM_REL_IMAGE_R
>    SIM_REL_IMAGE_L
>    SIM_FCOMP_R
>    SIM_FCOMP_L
>    CARD_INTERV
>    CARD_EMPTY_INTERV
>    SIMP_CARD_SETMINUS_L
>    SIMP_CARD_SETMINUS_R
>    SIMP_CARD_CPROD_L
>    SIMP_CARD_CPROD_R
> 
> Could you please review these changes and report any error?
> 
> Cheers,
> Laurent.
> 
> 1: http://wiki.event-b.org/index.php/Well-definedness_in_Event-B#Strictness
> 
> 
> 
> ------------------------------------------------------------------------------
> Start uncovering the many advantages of virtual appliances
> and start using them to simplify application deployment and
> accelerate your shift to cloud computing.
> http://p.sf.net/sfu/novell-sfdev2dev
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFMl0sDczhznXSdWggRAj6iAJ9gHj+2++sxukQtNE9lgshSlgwY1gCgtfi5
BN3nDXTAawPs/zMkmkRT5u8=
=s5Dg
-----END PGP SIGNATURE-----