Set Rewrite Rules
From Event-B
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_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 |