Re: [Rodin-b-sharp-user] Help with arithmetic goals

[Laurent V. <lau...@sy...>]

Dear Alexei,

Le 16 mars 2011 à 22:02, Alexei Iliasov a écrit :

> Regarding cardinality, may I suggest adding the following interactive rule:
> 
> ∀ a, b · a ∈ ℙ(ℕ) ∧ b ⊆ a ∧ finite(a) ⇒  card(a ∖ b) = card(a) − card(b)
> 
> This is a statement via which few other useful cardinality-related 
> properties may be discharged.

Thank you very much for this suggestion.  I've just added a slightly more general version of this rule in the wiki as SIMP_CARD_SETMINUS (see http://wiki.event-b.org/index.php/Arithmetic_Rewrite_Rules).

Matthias, can you please review this new rule of the wiki at your convenience?

Cheers,
Laurent.