Set Rewrite Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Nicolas m Added SIMP_IN_COMPSET_GENERAL |
imported>Laurent m Fixed rule names to make them easy to extract |
||
Line 1: | Line 1: | ||
{{RRHeader}} | {{RRHeader}} | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BTRUE}}||<math> P \land \ldots \land \btrue \land \ldots \land Q \;\;\defi\;\; P \land \ldots \land Q </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BFALSE}}||<math> P \land \ldots \land \bfalse \land \ldots \land Q \;\;\defi\;\; \bfalse </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_AND}}||<math> P \land \ldots \land Q \ | |||
\begin{array}{ll} | \begin{array}{ll} | ||
& s = s_1\bunion s_2\bunion\cdots\bunion s_n\\ | & s = s_1\bunion s_2\bunion\cdots\bunion s_n\\ | ||
Line 191: | Line 191: | ||
\land& s_{n-1}\binter s_n = \emptyset | \land& s_{n-1}\binter s_n = \emptyset | ||
\end{array}</math>|| || AM | \end{array}</math>|| || AM | ||
{{RRRow}}| || | {{RRRow}}| ||{{Rulename|SUBST_FORALL_AND}}||<math> | ||
\begin{array}{ll} | \begin{array}{ll} | ||
\forall x, \ldots, y, \ldots, z \qdot P(y) \land \ldots \land y = E \land \ldots \land Q(y) \limp R(y) \;\;\defi\;\;\\ | \forall x, \ldots, y, \ldots, z \qdot P(y) \land \ldots \land y = E \land \ldots \land Q(y) \limp R(y) \;\;\defi\;\;\\ |
Revision as of 10:29, 8 July 2009
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | SIMP_SPECIAL_AND_BTRUE |
A | ||
* | SIMP_SPECIAL_AND_BFALSE |
A | ||
* | SIMP_MULTI_AND |
A | ||
* | SIMP_MULTI_AND_NOT |
A | ||
* | SIMP_SPECIAL_OR_BTRUE |
A | ||
* | SIMP_SPECIAL_OR_BFALSE |
A | ||
* | SIMP_MULTI_OR |
A | ||
* | SIMP_MULTI_OR_NOT |
A | ||
* | SIMP_SPECIAL_IMP_BTRUE_R |
A | ||
* | SIMP_SPECIAL_IMP_BTRUE_L |
A | ||
* | SIMP_SPECIAL_IMP_BFALSE_R |
A | ||
* | SIMP_SPECIAL_IMP_BFALSE_L |
A | ||
* | SIMP_MULTI_IMP |
A | ||
* | SIMP_MULTI_IMP_OR |
A | ||
* | SIMP_MULTI_IMP_AND_NOT_R |
A | ||
* | SIMP_MULTI_IMP_AND_NOT_L |
A | ||
* | SIMP_MULTI_EQV |
A | ||
* | SIMP_MULTI_EQV_NOT |
A | ||
* | SIMP_MULTI_EQV_NOT_NOT |
A | ||
* | SIMP_SPECIAL_NOT_BTRUE |
A | ||
* | SIMP_SPECIAL_NOT_BFALSE |
A | ||
* | SIMP_NOT_NOT |
A | ||
* | SIMP_NOTEQUAL |
A | ||
* | SIMP_NOTIN |
A | ||
* | SIMP_NOTSUBSET |
A | ||
* | SIMP_NOTSUBSETEQ |
A | ||
* | SIMP_NOT_LE |
A | ||
* | SIMP_NOT_GE |
A | ||
* | SIMP_NOT_LT |
A | ||
* | SIMP_NOT_GT |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_FALSE_R |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_FALSE_L |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_TRUE_R |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_TRUE_L |
A | ||
* | SIMP_FORALL_AND |
A | ||
* | SIMP_EXISTS_OR |
A | ||
* | SIMP_FORALL |
A | ||
* | SIMP_EXISTS |
A | ||
* | SIMP_MULTI_EQUAL |
A | ||
* | SIMP_MULTI_NOTEQUAL |
A | ||
* | SIMP_EQUAL_MAPSTO |
A | ||
* | SIMP_EQUAL_SING |
A | ||
* | SIMP_SPECIAL_EQUAL_TRUE |
A | ||
* | SIMP_TYPE_SUBSETEQ |
where is a type expression | A | |
* | SIMP_SUBSETEQ_SING |
where is a single expression | A | |
* | SIMP_SPECIAL_SUBSETEQ |
A | ||
* | SIMP_MULTI_SUBSETEQ |
A | ||
* | SIMP_SUBSETEQ_BUNION |
A | ||
* | SIMP_SUBSETEQ_BINTER |
A | ||
* | DERIV_SUBSETEQ_BUNION |
M | ||
* | DERIV_SUBSETEQ_BINTER |
M | ||
* | SIMP_SUBSET_BUNION |
A | ||
* | SIMP_SUBSET_BINTER |
A | ||
* | SIMP_SPECIAL_IN |
A | ||
* | SIMP_MULTI_IN |
A | ||
* | SIMP_IN_SING |
A | ||
* | SIMP_MULTI_SETENUM |
A | ||
* | SIMP_SPECIAL_BINTER |
A | ||
* | SIMP_TYPE_BINTER |
where is a type expression | A | |
* | SIMP_MULTI_BINTER |
A | ||
* | SIMP_MULTI_EQUAL_BINTER |
A | ||
* | SIMP_SPECIAL_BUNION |
A | ||
* | SIMP_TYPE_BUNION |
where is a type expression | A | |
* | SIMP_MULTI_BUNION |
A | ||
* | SIMP_MULTI_EQUAL_BUNION |
A | ||
* | SIMP_MULTI_SETMINUS |
A | ||
* | SIMP_SPECIAL_SETMINUS_R |
A | ||
* | SIMP_SPECIAL_SETMINUS_L |
A | ||
* | SIMP_TYPE_SETMINUS |
where is a type expression | A | |
* | SIMP_TYPE_SETMINUS_SETMINUS |
where is a type expression | A | |
* | SIMP_TYPE_KUNION |
where is a type expression and | A | |
* | SIMP_KUNION_POW |
A | ||
* | SIMP_KUNION_POW1 |
A | ||
SIMP_SPECIAL_KUNION |
A | |||
SIMP_SPECIAL_QUNION |
A | |||
SIMP_SPECIAL_KINTER |
A | |||
* | SIMP_TYPE_KINTER |
where is a type expression | A | |
SIMP_SPECIAL_POW |
A | |||
SIMP_SPECIAL_POW1 |
A | |||
SIMP_SPECIAL_CPROD_R |
A | |||
SIMP_SPECIAL_CPROD_L |
A | |||
* | SIMP_COMPSET_EQUAL |
where non free in | A | |
* | SIMP_COMPSET_IN |
where non free in | A | |
SIMP_SPECIAL_COMPSET_BFALSE |
A | |||
SIMP_SPECIAL_COMPSET_BTRUE |
where the type od is | A | ||
* | SIMP_SUBSETEQ_COMPSET_L |
where non free in | A | |
SIMP_SPECIAL_EQUAL_COMPSET |
A | |||
* | SIMP_IN_COMPSET |
A | ||
* | SIMP_IN_COMPSET_GENERAL |
A | ||
* | SIMP_SUBSETEQ_COMPSET_R |
where non free in | A | |
SIMP_SPECIAL_OVERL |
A | |||
* | SIMP_MULTI_OVERL |
A | ||
* | SIMP_TYPE_OVERL_CPROD |
where is a type expression | A | |
* | SIMP_SPECIAL_KBOOL_BTRUE |
A | ||
* | SIMP_SPECIAL_KBOOL_BFALSE |
A | ||
* | DISTRI_SUBSETEQ_BUNION_SING |
where is a single expression | M | |
DEF_FINITE |
M | |||
* | SIMP_SPECIAL_FINITE |
A | ||
* | SIMP_FINITE_SETENUM |
A | ||
* | SIMP_FINITE_BUNION |
A | ||
* | SIMP_FINITE_POW |
A | ||
* | DERIV_FINITE_CPROD |
A | ||
* | SIMP_FINITE_CONVERSE |
A | ||
* | SIMP_FINITE_UPTO |
A | ||
* | SIMP_FINITE_BINTER_L |
M | ||
* | SIMP_FINITE_BINTER_R |
M | ||
* | SIMP_FINITE_SETMINUS |
M | ||
* | SIMP_FINITE_DOMRES |
M | ||
* | SIMP_FINITE_RANRES |
M | ||
* | SIMP_FINITE_DOMSUB |
M | ||
* | SIMP_FINITE_RANSUB |
M | ||
* | SIMP_FINITE_RELIMAGE |
M | ||
* | SIMP_FINITE_CPROD |
M | ||
* | SIMP_FINITE_OVERL |
M | ||
* | SIMP_FINITE_REL |
M | ||
* | SIMP_FINITE_FCOMP |
M | ||
* | SIMP_FINITE_BCOMP |
M | ||
* | SIMP_FINITE_DPROD |
M | ||
* | SIMP_FINITE_PPROD |
M | ||
* | SIMP_FINITE_COMPSET |
where non free in | M | |
* | SIMP_FINITE_RAN |
M | ||
* | SIMP_FINITE_DOM |
M | ||
* | SIMP_FINITE_QUNION |
M | ||
* | SIMP_FINITE_QINTER |
M | ||
* | SIMP_FINITE_ID |
A | ||
* | SIMP_FINITE_NATURAL |
A | ||
* | SIMP_FINITE_NATURAL1 |
A | ||
* | SIMP_FINITE_INTEGER |
A | ||
* | SIMP_FINITE_LAMBDA |
A | ||
* | SIMP_TYPE_EQUAL_EMPTY |
where is a type expression | A | |
* | SIMP_TYPE_IN |
where is a type expression | A | |
SIMP_SPECIAL_FORALL_BTRUE |
A | |||
SIMP_SPECIAL_FORALL_BFALSE |
A | |||
SIMP_SPECIAL_EXISTS_BTRUE |
A | |||
SIMP_SPECIAL_EXISTS_BFALSE |
A | |||
* | SIMP_SPECIAL_EQV_BTRUE |
A | ||
* | SIMP_SPECIAL_EQV_BFALSE |
A | ||
* | DEF_SUBSET |
A | ||
SIMP_SPECIAL_SUBSET_R |
A | |||
SIMP_SPECIAL_SUBSET_L |
A | |||
* | SIMP_TYPE_SUBSET_L |
where is a type expression | A | |
* | SIMP_MULTI_SUBSET |
A | ||
* | DISTRI_AND_OR |
M | ||
* | DISTRI_OR_AND |
M | ||
* | DEF_OR |
M | ||
* | DERIV_IMP |
M | ||
* | DERIV_IMP_IMP |
M | ||
* | DISTRI_IMP_AND |
M | ||
* | DISTRI_IMP_OR |
M | ||
* | DEF_EQV |
M | ||
* | DISTRI_NOT_AND |
M | ||
* | DISTRI_NOT_OR |
M | ||
* | DERIV_NOT_IMP |
M | ||
* | DERIV_NOT_FORALL |
M | ||
* | DERIV_NOT_EXISTS |
M | ||
* | DEF_SPECIAL_NOT_EQUAL |
M | ||
* | DEF_IN_MAPSTO |
M | ||
* | DEF_IN_POW |
M | ||
* | DEF_SUBSETEQ |
M | ||
* | DEF_IN_BUNION |
M | ||
* | DEF_IN_BINTER |
M | ||
* | DEF_IN_SETMINUS |
M | ||
* | DEF_IN_SETENUM |
M | ||
* | DEF_IN_KUNION |
M | ||
* | DEF_IN_QUNION |
M | ||
* | DEF_IN_KINTER |
M | ||
* | DEF_IN_QINTER |
M | ||
* | DEF_IN_UPTO |
M | ||
* | DISTRI_BUNION_BINTER |
M | ||
* | DISTRI_BINTER_BUNION |
M | ||
* | DISTRI_BINTER_SETMINUS |
M | ||
* | DISTRI_SETMINUS_BUNION |
M | ||
* | DERIV_TYPE_SETMINUS_BINTER |
where is a type expression | M | |
* | DERIV_TYPE_SETMINUS_BUNION |
where is a type expression | M | |
* | DERIV_TYPE_SETMINUS_SETMINUS |
where is a type expression | M | |
* | DISTRI_CPROD_BINTER |
M | ||
* | DISTRI_CPROD_BUNION |
M | ||
* | DISTRI_CPROD_SETMINUS |
M | ||
* | DERIV_SUBSETEQ |
where is the type of and | M | |
* | DERIV_EQUAL |
where is the type of and | M | |
* | DERIV_SUBSETEQ_SETMINUS_L |
M | ||
* | DERIV_SUBSETEQ_SETMINUS_R |
M | ||
* | DEF_PARTITION |
AM | ||
SUBST_FORALL_AND |
A |