Arithmetic Rewrite Rules: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>Nicolas
m added SIMP_CARD_SETMINUS and SIMP_CARD_CPROD
imported>Laurent
m Fixed rule names to make them easy to extract
Line 1: Line 1:
{{RRHeader}}
{{RRHeader}}
{{RRRow}}| ||<font size="-2"> SIMP_SPECIAL_MOD_0 </font>||<math>  0 \,\bmod\,  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_MOD_0}}||<math>  0 \,\bmod\,  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}| ||<font size="-2"> SIMP_SPECIAL_MOD_1 </font>||<math>  E \,\bmod\,  1 \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_MOD_1}}||<math>  E \,\bmod\,  1 \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MIN_SING </font>||<math>  \min (\{ E\} ) \;\;\defi\;\;  E </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_MIN_SING}}||<math>  \min (\{ E\} ) \;\;\defi\;\;  E </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MAX_SING </font>||<math>  \max (\{ E\} ) \;\;\defi\;\;  E </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_MAX_SING}}||<math>  \max (\{ E\} ) \;\;\defi\;\;  E </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MIN_NATURAL </font>||<math>  \min (\nat ) \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MIN_NATURAL}}||<math>  \min (\nat ) \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MIN_NATURAL1 </font>||<math>  \min (\natn ) \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MIN_NATURAL1}}||<math>  \min (\natn ) \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MIN_BUNION_SING </font>||<math>  \begin{array}{cl} & \min (S \bunion  \ldots  \bunion  \{ \min (T)\}  \bunion  \ldots  \bunion  U) \\ \defi & \min (S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U) \\ \end{array} </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MIN_BUNION_SING}}||<math>  \begin{array}{cl} & \min (S \bunion  \ldots  \bunion  \{ \min (T)\}  \bunion  \ldots  \bunion  U) \\ \defi & \min (S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U) \\ \end{array} </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MAX_BUNION_SING </font>||<math>  \begin{array}{cl} & \max (S \bunion  \ldots  \bunion  \{ \max (T)\}  \bunion  \ldots  \bunion  U) \\ \defi &  \max (S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U) \\  \end{array} </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MAX_BUNION_SING}}||<math>  \begin{array}{cl} & \max (S \bunion  \ldots  \bunion  \{ \max (T)\}  \bunion  \ldots  \bunion  U) \\ \defi &  \max (S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U) \\  \end{array} </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MIN_UPTO </font>||<math>  \min (E \upto  F) \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MIN_UPTO}}||<math>  \min (E \upto  F) \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MAX_UPTO </font>||<math>  \max (E \upto  F) \;\;\defi\;\;  F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MAX_UPTO}}||<math>  \max (E \upto  F) \;\;\defi\;\;  F </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_MIN </font>||<math>  \min (\{ E, \ldots  , i, \ldots  , j, \ldots , H\} ) \;\;\defi\;\;  \min (\{ E, \ldots  , i, \ldots , H\} ) </math>|| where <math>i</math> and <math>j</math> are literals and <math>i \leq j</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_MIN}}||<math>  \min (\{ E, \ldots  , i, \ldots  , j, \ldots , H\} ) \;\;\defi\;\;  \min (\{ E, \ldots  , i, \ldots , H\} ) </math>|| where <math>i</math> and <math>j</math> are literals and <math>i \leq j</math> ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_MAX </font>||<math>  \max (\{ E, \ldots  , i, \ldots  , j, \ldots , H\} ) \;\;\defi\;\;  \max (\{ E, \ldots  , i, \ldots , H\} ) </math>|| where <math>i</math> and <math>j</math> are literals and <math>i \geq j</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_MAX}}||<math>  \max (\{ E, \ldots  , i, \ldots  , j, \ldots , H\} ) \;\;\defi\;\;  \max (\{ E, \ldots  , i, \ldots , H\} ) </math>|| where <math>i</math> and <math>j</math> are literals and <math>i \geq j</math> ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_MIN_UPTO </font>||<math>  \min (\{ i, \ldots  , j\} ) \;\;\defi\;\;  A \;\;(computation) </math>|| where <math>i, ... ,\,j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_MIN_UPTO}}||<math>  \min (\{ i, \ldots  , j\} ) \;\;\defi\;\;  A \;\;(computation) </math>|| where <math>i, ... ,\,j</math> are literals ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_MAX_UPTO </font>||<math>  \max (\{ i, \ldots  , j\} ) \;\;\defi\;\;  A \;\;(computation) </math>|| where <math>i, ... ,\,j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_MAX_UPTO}}||<math>  \max (\{ i, \ldots  , j\} ) \;\;\defi\;\;  A \;\;(computation) </math>|| where <math>i, ... ,\,j</math> are literals ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_CARD </font>||<math>  \card (\emptyset ) \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_CARD}}||<math>  \card (\emptyset ) \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_SING </font>||<math>  \card (\{ E\} ) \;\;\defi\;\;  1 </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_SING}}||<math>  \card (\{ E\} ) \;\;\defi\;\;  1 </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_EQUAL_CARD </font>||<math>  \card (S) = 0 \;\;\defi\;\;  S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_CARD}}||<math>  \card (S) = 0 \;\;\defi\;\;  S = \emptyset </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_POW </font>||<math>  \card (\pow (S)) \;\;\defi\;\;  2 ^ \card (S) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_POW}}||<math>  \card (\pow (S)) \;\;\defi\;\;  2 ^ \card (S) </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_BUNION </font>||<math>  \card (S \bunion  T) \;\;\defi\;\;  \card (S) + \card (T) - \card (S \binter  T) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_BUNION}}||<math>  \card (S \bunion  T) \;\;\defi\;\;  \card (S) + \card (T) - \card (S \binter  T) </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_SETMINUS </font>||<math>  \card (S \setminus  T) \;\;\defi\;\;  \card (S) - \card (S \binter  T) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_SETMINUS}}||<math>  \card (S \setminus  T) \;\;\defi\;\;  \card (S) - \card (S \binter  T) </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_CPROD </font>||<math>  \card (S \cprod  T) \;\;\defi\;\;  \card (S) * \card (T) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_CPROD}}||<math>  \card (S \cprod  T) \;\;\defi\;\;  \card (S) * \card (T) </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_CONVERSE </font>||<math>  \card (r^{-1} ) \;\;\defi\;\;  \card (r) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_CONVERSE}}||<math>  \card (r^{-1} ) \;\;\defi\;\;  \card (r) </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_ID </font>||<math>  \card (\id (S)) \;\;\defi\;\;  \card (S) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_ID}}||<math>  \card (\id (S)) \;\;\defi\;\;  \card (S) </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_LAMBDA </font>||<math>  \card (\lambda x\qdot (P \mid  E)) \;\;\defi\;\;  \card (\{ x \qdot  P \mid  x\} ) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_LAMBDA}}||<math>  \card (\lambda x\qdot (P \mid  E)) \;\;\defi\;\;  \card (\{ x \qdot  P \mid  x\} ) </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_COMPSET </font>||<math>  \card (\{ x \qdot  x \in  S \mid  x\} ) \;\;\defi\;\;  \card (S) </math>|| where <math>x</math> non free in <math>S</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_COMPSET}}||<math>  \card (\{ x \qdot  x \in  S \mid  x\} ) \;\;\defi\;\;  \card (S) </math>|| where <math>x</math> non free in <math>S</math> ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_CARD_UPTO </font>||<math>  \card (i \upto  j) \;\;\defi\;\;  j-i+1 </math>|| where <math>i</math> and <math>j</math> are literals and <math>i \leq j</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_CARD_UPTO}}||<math>  \card (i \upto  j) \;\;\defi\;\;  j-i+1 </math>|| where <math>i</math> and <math>j</math> are literals and <math>i \leq j</math> ||  A
{{RRRow}}|*||<font size="-2"> SIMP_TYPE_CARD </font>||<math>  \card (\mathit{Tenum}) \;\;\defi\;\;  N </math>|| where <math>\mathit{Tenum}</math> is a carrier set containing <math>N</math> elements ||  A
{{RRRow}}|*||{{Rulename|SIMP_TYPE_CARD}}||<math>  \card (\mathit{Tenum}) \;\;\defi\;\;  N </math>|| where <math>\mathit{Tenum}</math> is a carrier set containing <math>N</math> elements ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_GE_CARD_0 </font>||<math>  \card (S) \geq  1 \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_GE_CARD_0}}||<math>  \card (S) \geq  1 \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_LE_CARD_1 </font>||<math>  1 \leq  \card (S) \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LE_CARD_1}}||<math>  1 \leq  \card (S) \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_LE_CARD_0 </font>||<math>  0 \leq  \card (S) \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LE_CARD_0}}||<math>  0 \leq  \card (S) \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_GE_CARD_0 </font>||<math>  \card (S) \geq  0 \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_GE_CARD_0}}||<math>  \card (S) \geq  0 \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_GT_CARD_0 </font>||<math>  \card (S) > 0 \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_GT_CARD_0}}||<math>  \card (S) > 0 \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_LT_CARD_0 </font>||<math>  0 < \card (S) \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LT_CARD_0}}||<math>  0 < \card (S) \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_EQUAL_CARD_1 </font>||<math>  \card (S) = 1 \;\;\defi\;\;  \exists x \qdot  S = \{ x\} </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL_CARD_1}}||<math>  \card (S) = 1 \;\;\defi\;\;  \exists x \qdot  S = \{ x\} </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_NATURAL </font>||<math>  \card (S) \in  \nat  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_NATURAL}}||<math>  \card (S) \in  \nat  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_CARD_NATURAL1 </font>||<math>  \card (S) \in  \natn  \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_NATURAL1}}||<math>  \card (S) \in  \natn  \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_IN_NATURAL </font>||<math>  i \in  \nat  \;\;\defi\;\;  \btrue </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_NATURAL}}||<math>  i \in  \nat  \;\;\defi\;\;  \btrue </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}| ||<font size="-2"> SIMP_SPECIAL_IN_NATURAL1 </font>||<math>  0 \in  \natn  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_IN_NATURAL1}}||<math>  0 \in  \natn  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_IN_NATURAL1 </font>||<math>  i \in  \natn  \;\;\defi\;\;  \btrue </math>|| where <math>i</math> is a literal and <math>1 \leq i</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_NATURAL1}}||<math>  i \in  \natn  \;\;\defi\;\;  \btrue </math>|| where <math>i</math> is a literal and <math>1 \leq i</math> ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_UPTO </font>||<math>  i \upto  j \;\;\defi\;\;  \emptyset </math>|| where <math>i</math> and <math>j</math> are literals and <math>j < i</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_UPTO}}||<math>  i \upto  j \;\;\defi\;\;  \emptyset </math>|| where <math>i</math> and <math>j</math> are literals and <math>j < i</math> ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_IN_MINUS_NATURAL </font>||<math>  -i \in  \nat  \;\;\defi\;\;  \bfalse </math>|| where <math>i</math> is a literal and <math>1 \leq i</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_MINUS_NATURAL}}||<math>  -i \in  \nat  \;\;\defi\;\;  \bfalse </math>|| where <math>i</math> is a literal and <math>1 \leq i</math> ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_IN_MINUS_NATURAL1 </font>||<math>  -i \in  \natn  \;\;\defi\;\;  \bfalse </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_MINUS_NATURAL1}}||<math>  -i \in  \natn  \;\;\defi\;\;  \bfalse </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}| ||<font size="-2"> SIMP_SPECIAL_KBOOL_BTRUE </font>||<math>  \bool (\btrue ) \;\;\defi\;\;  \True </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_KBOOL_BTRUE}}||<math>  \bool (\btrue ) \;\;\defi\;\;  \True </math>||  ||  A
{{RRRow}}| ||<font size="-2"> SIMP_SPECIAL_KBOOL_BFALSE </font>||<math>  \bool (\bfalse ) \;\;\defi\;\;  \False </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_KBOOL_BFALSE}}||<math>  \bool (\bfalse ) \;\;\defi\;\;  \False </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_EQUAL_KBOOL_TRUE </font>||<math>  \bool (P) = \True  \;\;\defi\;\;  P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL_KBOOL_TRUE}}||<math>  \bool (P) = \True  \;\;\defi\;\;  P </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_EQUAL_KBOOL_FALSE </font>||<math>  \bool (P) = \False  \;\;\defi\;\;  \lnot\, P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL_KBOOL_FALSE}}||<math>  \bool (P) = \False  \;\;\defi\;\;  \lnot\, P </math>||  ||  A
{{RRRow}}|*||<font size="-2"> DEF_EQUAL_MIN </font>||<math>  E = \min (S) \;\;\defi\;\;  E \in  S \land  (\forall x \qdot  x \in  S \limp  E \leq  x) </math>|| where <math>x</math> non free in <math>S, E</math> ||  M
{{RRRow}}|*||{{Rulename|DEF_EQUAL_MIN}}||<math>  E = \min (S) \;\;\defi\;\;  E \in  S \land  (\forall x \qdot  x \in  S \limp  E \leq  x) </math>|| where <math>x</math> non free in <math>S, E</math> ||  M
{{RRRow}}|*||<font size="-2"> DEF_EQUAL_MAX </font>||<math>  E = \max (S) \;\;\defi\;\;  E \in  S \land  (\forall x \qdot  x \in  S \limp  E \geq  x) </math>|| where <math>x</math> non free in <math>S, E</math> ||  M
{{RRRow}}|*||{{Rulename|DEF_EQUAL_MAX}}||<math>  E = \max (S) \;\;\defi\;\;  E \in  S \land  (\forall x \qdot  x \in  S \limp  E \geq  x) </math>|| where <math>x</math> non free in <math>S, E</math> ||  M
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_PLUS </font>||<math>  E + \ldots  + 0 + \ldots  + F \;\;\defi\;\;  E + \ldots  + F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PLUS}}||<math>  E + \ldots  + 0 + \ldots  + F \;\;\defi\;\;  E + \ldots  + F </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_MINUS_R </font>||<math>  E - 0 \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_MINUS_R}}||<math>  E - 0 \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_MINUS_L </font>||<math>  0 - E \;\;\defi\;\;  -E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_MINUS_L}}||<math>  0 - E \;\;\defi\;\;  -E </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MINUS_MINUS </font>||<math>  - (- E) \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MINUS_MINUS}}||<math>  - (- E) \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MULTI_MINUS </font>||<math>  E - E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_MINUS}}||<math>  E - E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_PROD_0 </font>||<math>  E * \ldots  * 0 * \ldots  * F \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_0}}||<math>  E * \ldots  * 0 * \ldots  * F \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_PROD_1 </font>||<math>  E * \ldots  * 1 * \ldots  * F \;\;\defi\;\;  E * \ldots  * F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_1}}||<math>  E * \ldots  * 1 * \ldots  * F \;\;\defi\;\;  E * \ldots  * F </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_PROD_MINUS_EVEN </font>||<math>  (-E) * \ldots  * (-F) \;\;\defi\;\;  E * \ldots  * F </math>|| if an even number of <math>-</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_MINUS_EVEN}}||<math>  (-E) * \ldots  * (-F) \;\;\defi\;\;  E * \ldots  * F </math>|| if an even number of <math>-</math> ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_PROD_MINUS_ODD </font>||<math>  (-E) * \ldots  * (-F) \;\;\defi\;\;  -(E * \ldots  * F) </math>|| if an odd number of <math>-</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_MINUS_ODD}}||<math>  (-E) * \ldots  * (-F) \;\;\defi\;\;  -(E * \ldots  * F) </math>|| if an odd number of <math>-</math> ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_MINUS </font>||<math>  - (i) \;\;\defi\;\;  (-i) </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_MINUS}}||<math>  - (i) \;\;\defi\;\;  (-i) </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_MINUS_MINUS </font>||<math>  - (-i) \;\;\defi\;\;  i </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_MINUS_MINUS}}||<math>  - (-i) \;\;\defi\;\;  i </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_EQUAL </font>||<math>  i = j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL}}||<math>  i = j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_LE </font>||<math>  i \leq  j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LE}}||<math>  i \leq  j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_LT </font>||<math>  i < j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LT}}||<math>  i < j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_GE </font>||<math>  i \geq  j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_GE}}||<math>  i \geq  j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||<font size="-2"> SIMP_LIT_GT </font>||<math>  i > j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_GT}}||<math>  i > j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||<font size="-2"> SIMP_DIV_MINUS </font>||<math>  (- E) \div  (-F) \;\;\defi\;\;  E \div  F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_DIV_MINUS}}||<math>  (- E) \div  (-F) \;\;\defi\;\;  E \div  F </math>||  ||  A
{{RRRow}}| ||<font size="-2"> SIMP_SPECIAL_DIV_1 </font>||<math>  E \div  1 \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DIV_1}}||<math>  E \div  1 \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_DIV_0 </font>||<math>  0 \div  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DIV_0}}||<math>  0 \div  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_EXPN_1_R </font>||<math>  E ^ 1 \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EXPN_1_R}}||<math>  E ^ 1 \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_EXPN_1_L </font>||<math>  1 ^ E \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EXPN_1_L}}||<math>  1 ^ E \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_SPECIAL_EXPN_0 </font>||<math>  E ^ 0 \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EXPN_0}}||<math>  E ^ 0 \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MULTI_LE </font>||<math>  E \leq  E \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_LE}}||<math>  E \leq  E \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MULTI_LT </font>||<math>  E < E \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_LT}}||<math>  E < E \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MULTI_GE </font>||<math>  E \geq  E \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_GE}}||<math>  E \geq  E \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MULTI_GT </font>||<math>  E > E \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_GT}}||<math>  E > E \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MULTI_DIV </font>||<math>  E \div  E \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DIV}}||<math>  E \div  E \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MULTI_DIV_PROD </font>||<math>  (X * \ldots * E * \ldots * Y) \div  E \;\;\defi\;\;  X * \ldots * Y </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DIV_PROD}}||<math>  (X * \ldots * E * \ldots * Y) \div  E \;\;\defi\;\;  X * \ldots * Y </math>||  ||  A
{{RRRow}}|*||<font size="-2"> SIMP_MULTI_MOD </font>||<math>  E \,\bmod\,  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_MOD}}||<math>  E \,\bmod\,  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||<font size="-2"> DISTRI_PROD_PLUS </font>||<math>  a * (b + c) \;\;\defi\;\;  (a * b) + (a * c) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_PROD_PLUS}}||<math>  a * (b + c) \;\;\defi\;\;  (a * b) + (a * c) </math>||  ||  M
{{RRRow}}|*||<font size="-2"> DISTRI_PROD_MINUS </font>||<math>  a * (b - c) \;\;\defi\;\;  (a * b) - (a * c) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_PROD_MINUS}}||<math>  a * (b - c) \;\;\defi\;\;  (a * b) - (a * c) </math>||  ||  M
{{RRRow}}|*||<font size="-2"> DERIV_LE_CARD </font>||<math>  \card (S) \leq  \card (T) \;\;\defi\;\;  S \subseteq  T </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||{{Rulename|DERIV_LE_CARD}}||<math>  \card (S) \leq  \card (T) \;\;\defi\;\;  S \subseteq  T </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||<font size="-2"> DERIV_GE_CARD </font>||<math>  \card (S) \geq  \card (T) \;\;\defi\;\;  T \subseteq  S </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||{{Rulename|DERIV_GE_CARD}}||<math>  \card (S) \geq  \card (T) \;\;\defi\;\;  T \subseteq  S </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||<font size="-2"> DERIV_LT_CARD </font>||<math>  \card (S) < \card (T) \;\;\defi\;\;  S  \subset  T </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||{{Rulename|DERIV_LT_CARD}}||<math>  \card (S) < \card (T) \;\;\defi\;\;  S  \subset  T </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||<font size="-2"> DERIV_GT_CARD </font>||<math>  \card (S) > \card (T) \;\;\defi\;\;  T  \subset  S </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||{{Rulename|DERIV_GT_CARD}}||<math>  \card (S) > \card (T) \;\;\defi\;\;  T  \subset  S </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||<font size="-2"> DERIV_EQUAL_CARD </font>||<math>  \card (S) = \card (T) \;\;\defi\;\;  S = T  </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M  
{{RRRow}}|*||{{Rulename|DERIV_EQUAL_CARD}}||<math>  \card (S) = \card (T) \;\;\defi\;\;  S = T  </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M  
|}
|}


Revision as of 10:33, 8 July 2009

  Name Rule Side Condition A/M
SIMP_SPECIAL_MOD_0
 0 \,\bmod\, E \;\;\defi\;\; 0 A
SIMP_SPECIAL_MOD_1
 E \,\bmod\, 1 \;\;\defi\;\; 0 A
*
SIMP_MIN_SING
 \min (\{ E\} ) \;\;\defi\;\; E where E is a single expression A
*
SIMP_MAX_SING
 \max (\{ E\} ) \;\;\defi\;\; E where E is a single expression A
*
SIMP_MIN_NATURAL
 \min (\nat ) \;\;\defi\;\; 0 A
*
SIMP_MIN_NATURAL1
 \min (\natn ) \;\;\defi\;\; 1 A
*
SIMP_MIN_BUNION_SING
 \begin{array}{cl} & \min (S \bunion \ldots \bunion \{ \min (T)\} \bunion \ldots \bunion U) \\ \defi & \min (S \bunion \ldots \bunion T \bunion \ldots \bunion U) \\ \end{array} A
*
SIMP_MAX_BUNION_SING
 \begin{array}{cl} & \max (S \bunion \ldots \bunion \{ \max (T)\} \bunion \ldots \bunion U) \\ \defi & \max (S \bunion \ldots \bunion T \bunion \ldots \bunion U) \\ \end{array} A
*
SIMP_MIN_UPTO
 \min (E \upto F) \;\;\defi\;\; E A
*
SIMP_MAX_UPTO
 \max (E \upto F) \;\;\defi\;\; F A
*
SIMP_LIT_MIN
 \min (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \min (\{ E, \ldots , i, \ldots , H\} ) where i and j are literals and i \leq j A
*
SIMP_LIT_MAX
 \max (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \max (\{ E, \ldots , i, \ldots , H\} ) where i and j are literals and i \geq j A
*
SIMP_LIT_MIN_UPTO
 \min (\{ i, \ldots , j\} ) \;\;\defi\;\; A \;\;(computation) where i, ... ,\,j are literals A
*
SIMP_LIT_MAX_UPTO
 \max (\{ i, \ldots , j\} ) \;\;\defi\;\; A \;\;(computation) where i, ... ,\,j are literals A
*
SIMP_SPECIAL_CARD
 \card (\emptyset ) \;\;\defi\;\; 0 A
*
SIMP_CARD_SING
 \card (\{ E\} ) \;\;\defi\;\; 1 where E is a single expression A
*
SIMP_SPECIAL_EQUAL_CARD
 \card (S) = 0 \;\;\defi\;\; S = \emptyset A
*
SIMP_CARD_POW
 \card (\pow (S)) \;\;\defi\;\; 2 ^ \card (S) A
*
SIMP_CARD_BUNION
 \card (S \bunion T) \;\;\defi\;\; \card (S) + \card (T) - \card (S \binter T) A
*
SIMP_CARD_SETMINUS
 \card (S \setminus T) \;\;\defi\;\; \card (S) - \card (S \binter T) A
*
SIMP_CARD_CPROD
 \card (S \cprod T) \;\;\defi\;\; \card (S) * \card (T) A
*
SIMP_CARD_CONVERSE
 \card (r^{-1} ) \;\;\defi\;\; \card (r) A
*
SIMP_CARD_ID
 \card (\id (S)) \;\;\defi\;\; \card (S) A
*
SIMP_CARD_LAMBDA
 \card (\lambda x\qdot (P \mid E)) \;\;\defi\;\; \card (\{ x \qdot P \mid x\} ) A
*
SIMP_CARD_COMPSET
 \card (\{ x \qdot x \in S \mid x\} ) \;\;\defi\;\; \card (S) where x non free in S A
*
SIMP_LIT_CARD_UPTO
 \card (i \upto j) \;\;\defi\;\; j-i+1 where i and j are literals and i \leq j A
*
SIMP_TYPE_CARD
 \card (\mathit{Tenum}) \;\;\defi\;\; N where \mathit{Tenum} is a carrier set containing N elements A
*
SIMP_LIT_GE_CARD_0
 \card (S) \geq 1 \;\;\defi\;\; \lnot\, S = \emptyset A
*
SIMP_LIT_LE_CARD_1
 1 \leq \card (S) \;\;\defi\;\; \lnot\, S = \emptyset A
*
SIMP_LIT_LE_CARD_0
 0 \leq \card (S) \;\;\defi\;\; \btrue A
*
SIMP_LIT_GE_CARD_0
 \card (S) \geq 0 \;\;\defi\;\; \btrue A
*
SIMP_LIT_GT_CARD_0
 \card (S) > 0 \;\;\defi\;\; \lnot\, S = \emptyset A
*
SIMP_LIT_LT_CARD_0
 0 < \card (S) \;\;\defi\;\; \lnot\, S = \emptyset A
*
SIMP_LIT_EQUAL_CARD_1
 \card (S) = 1 \;\;\defi\;\; \exists x \qdot S = \{ x\} A
*
SIMP_CARD_NATURAL
 \card (S) \in \nat \;\;\defi\;\; \btrue A
*
SIMP_CARD_NATURAL1
 \card (S) \in \natn \;\;\defi\;\; \lnot\, S = \emptyset A
*
SIMP_LIT_IN_NATURAL
 i \in \nat \;\;\defi\;\; \btrue where i is a literal A
SIMP_SPECIAL_IN_NATURAL1
 0 \in \natn \;\;\defi\;\; \bfalse A
*
SIMP_LIT_IN_NATURAL1
 i \in \natn \;\;\defi\;\; \btrue where i is a literal and 1 \leq i A
*
SIMP_LIT_UPTO
 i \upto j \;\;\defi\;\; \emptyset where i and j are literals and j < i A
*
SIMP_LIT_IN_MINUS_NATURAL
 -i \in \nat \;\;\defi\;\; \bfalse where i is a literal and 1 \leq i A
*
SIMP_LIT_IN_MINUS_NATURAL1
 -i \in \natn \;\;\defi\;\; \bfalse where i is a literal A
SIMP_SPECIAL_KBOOL_BTRUE
 \bool (\btrue ) \;\;\defi\;\; \True A
SIMP_SPECIAL_KBOOL_BFALSE
 \bool (\bfalse ) \;\;\defi\;\; \False A
*
SIMP_LIT_EQUAL_KBOOL_TRUE
 \bool (P) = \True \;\;\defi\;\; P A
*
SIMP_LIT_EQUAL_KBOOL_FALSE
 \bool (P) = \False \;\;\defi\;\; \lnot\, P A
*
DEF_EQUAL_MIN
 E = \min (S) \;\;\defi\;\; E \in S \land (\forall x \qdot x \in S \limp E \leq x) where x non free in S, E M
*
DEF_EQUAL_MAX
 E = \max (S) \;\;\defi\;\; E \in S \land (\forall x \qdot x \in S \limp E \geq x) where x non free in S, E M
*
SIMP_SPECIAL_PLUS
 E + \ldots + 0 + \ldots + F \;\;\defi\;\; E + \ldots + F A
*
SIMP_SPECIAL_MINUS_R
 E - 0 \;\;\defi\;\; E A
*
SIMP_SPECIAL_MINUS_L
 0 - E \;\;\defi\;\; -E A
*
SIMP_MINUS_MINUS
 - (- E) \;\;\defi\;\; E A
*
SIMP_MULTI_MINUS
 E - E \;\;\defi\;\; 0 A
*
SIMP_SPECIAL_PROD_0
 E * \ldots * 0 * \ldots * F \;\;\defi\;\; 0 A
*
SIMP_SPECIAL_PROD_1
 E * \ldots * 1 * \ldots * F \;\;\defi\;\; E * \ldots * F A
*
SIMP_SPECIAL_PROD_MINUS_EVEN
 (-E) * \ldots * (-F) \;\;\defi\;\; E * \ldots * F if an even number of - A
*
SIMP_SPECIAL_PROD_MINUS_ODD
 (-E) * \ldots * (-F) \;\;\defi\;\; -(E * \ldots * F) if an odd number of - A
*
SIMP_LIT_MINUS
 - (i) \;\;\defi\;\; (-i) where i is a literal A
*
SIMP_LIT_MINUS_MINUS
 - (-i) \;\;\defi\;\; i where i is a literal A
*
SIMP_LIT_EQUAL
 i = j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) where i and j are literals A
*
SIMP_LIT_LE
 i \leq j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) where i and j are literals A
*
SIMP_LIT_LT
 i < j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) where i and j are literals A
*
SIMP_LIT_GE
 i \geq j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) where i and j are literals A
*
SIMP_LIT_GT
 i > j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) where i and j are literals A
*
SIMP_DIV_MINUS
 (- E) \div (-F) \;\;\defi\;\; E \div F A
SIMP_SPECIAL_DIV_1
 E \div 1 \;\;\defi\;\; E A
*
SIMP_SPECIAL_DIV_0
 0 \div E \;\;\defi\;\; 0 A
*
SIMP_SPECIAL_EXPN_1_R
 E ^ 1 \;\;\defi\;\; E A
*
SIMP_SPECIAL_EXPN_1_L
 1 ^ E \;\;\defi\;\; 1 A
*
SIMP_SPECIAL_EXPN_0
 E ^ 0 \;\;\defi\;\; 1 A
*
SIMP_MULTI_LE
 E \leq E \;\;\defi\;\; \btrue A
*
SIMP_MULTI_LT
 E < E \;\;\defi\;\; \bfalse A
*
SIMP_MULTI_GE
 E \geq E \;\;\defi\;\; \btrue A
*
SIMP_MULTI_GT
 E > E \;\;\defi\;\; \bfalse A
*
SIMP_MULTI_DIV
 E \div E \;\;\defi\;\; 1 A
*
SIMP_MULTI_DIV_PROD
 (X * \ldots * E * \ldots * Y) \div E \;\;\defi\;\; X * \ldots * Y A
*
SIMP_MULTI_MOD
 E \,\bmod\, E \;\;\defi\;\; 0 A
*
DISTRI_PROD_PLUS
 a * (b + c) \;\;\defi\;\; (a * b) + (a * c) M
*
DISTRI_PROD_MINUS
 a * (b - c) \;\;\defi\;\; (a * b) - (a * c) M
*
DERIV_LE_CARD
 \card (S) \leq \card (T) \;\;\defi\;\; S \subseteq T S and T must be of the same type M
*
DERIV_GE_CARD
 \card (S) \geq \card (T) \;\;\defi\;\; T \subseteq S S and T must be of the same type M
*
DERIV_LT_CARD
 \card (S) < \card (T) \;\;\defi\;\; S \subset T S and T must be of the same type M
*
DERIV_GT_CARD
 \card (S) > \card (T) \;\;\defi\;\; T \subset S S and T must be of the same type M
*
DERIV_EQUAL_CARD
 \card (S) = \card (T) \;\;\defi\;\; S = T S and T must be of the same type M
Retrieved from ‘https://wiki.event-b.org/index.php?title=Arithmetic_Rewrite_Rules&oldid=805’