Difference between revisions of "Relation Rewrite Rules"
From Event-B
Jump to navigationJump to searchimported>Laurent m |
imported>Laurent (Put back rule SIMP_FUNIMAGE_CONVERSE_FUNIMAGE) |
||
Line 94: | Line 94: | ||
{{RRRow}}|*||<font size="-2"> SIMP_FUNIMAGE_ID </font>||<math> \id (S)(x) \;\;\defi\;\; x </math>|| || A | {{RRRow}}|*||<font size="-2"> SIMP_FUNIMAGE_ID </font>||<math> \id (S)(x) \;\;\defi\;\; x </math>|| || A | ||
{{RRRow}}|*||<font size="-2"> SIMP_FUNIMAGE_FUNIMAGE_CONVERSE </font>||<math> f(f^{-1} (E)) \;\;\defi\;\; E </math>|| || A | {{RRRow}}|*||<font size="-2"> SIMP_FUNIMAGE_FUNIMAGE_CONVERSE </font>||<math> f(f^{-1} (E)) \;\;\defi\;\; E </math>|| || A | ||
+ | {{RRRow}}|*||<font size="-2"> SIMP_FUNIMAGE_CONVERSE_FUNIMAGE </font>||<math> f^{-1}(f(E)) \;\;\defi\;\; E </math>|| || A | ||
{{RRRow}}|*||<font size="-2"> SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM </font>||<math> \{x \mapsto a, \ldots, y \mapsto b\}(\{a \mapsto x, \ldots, b \mapsto y\}(E)) \;\;\defi\;\; E </math>|| || A | {{RRRow}}|*||<font size="-2"> SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM </font>||<math> \{x \mapsto a, \ldots, y \mapsto b\}(\{a \mapsto x, \ldots, b \mapsto y\}(E)) \;\;\defi\;\; E </math>|| || A | ||
{{RRRow}}|*||<font size="-2"> DEF_BCOMP </font>||<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>|| || M | {{RRRow}}|*||<font size="-2"> DEF_BCOMP </font>||<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>|| || M |
Revision as of 08:51, 3 July 2009
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | SIMP_DOM_COMPSET | ![]() |
A | |
* | SIMP_DOM_CONVERSE | ![]() |
A | |
* | SIMP_RAN_COMPSET | ![]() |
A | |
* | SIMP_RAN_CONVERSE | ![]() |
A | |
* | SIMP_SPECIAL_OVERL | ![]() |
A | |
* | SIMP_MULTI_OVERL | ![]() |
A | |
* | SIMP_TYPE_OVERL_CPROD | ![]() |
where ![]() |
A |
SIMP_SPECIAL_DOMRES_L | ![]() |
A | ||
SIMP_SPECIAL_DOMRES_R | ![]() |
A | ||
* | SIMP_TYPE_DOMRES | ![]() |
where ![]() |
A |
* | SIMP_MULTI_DOMRES_DOM | ![]() |
A | |
* | SIMP_MULTI_DOMRES_RAN | ![]() |
A | |
* | SIMP_DOMRES_ID | ![]() |
A | |
SIMP_SPECIAL_RANRES_R | ![]() |
A | ||
SIMP_SPECIAL_RANRES_L | ![]() |
A | ||
* | SIMP_TYPE_RANRES | ![]() |
where ![]() |
A |
* | SIMP_MULTI_RANRES_RAN | ![]() |
A | |
* | SIMP_MULTI_RANRES_DOM | ![]() |
A | |
* | SIMP_RANRES_ID | ![]() |
A | |
SIMP_SPECIAL_DOMSUB_L | ![]() |
A | ||
SIMP_SPECIAL_DOMSUB_R | ![]() |
A | ||
* | SIMP_TYPE_DOMSUB | ![]() |
where ![]() |
A |
* | SIMP_MULTI_DOMSUB_DOM | ![]() |
A | |
* | SIMP_DOMSUB_ID | ![]() |
A | |
SIMP_SPECIAL_RANSUB_R | ![]() |
A | ||
SIMP_SPECIAL_RANSUB_L | ![]() |
A | ||
* | SIMP_TYPE_RANSUB | ![]() |
where ![]() |
A |
* | SIMP_MULTI_RANSUB_RAN | ![]() |
A | |
* | SIMP_RANSUB_ID | ![]() |
A | |
SIMP_SPECIAL_FCOMP | ![]() |
A | ||
* | SIMP_TYPE_FCOMP_ID | ![]() |
where ![]() |
A |
* | SIMP_TYPE_FCOMP_R | ![]() |
where ![]() ![]() |
A |
* | SIMP_TYPE_FCOMP_L | ![]() |
where ![]() ![]() |
A |
* | SIMP_FCOMP_ID | ![]() |
A | |
SIMP_SPECIAL_BCOMP | ![]() |
A | ||
* | SIMP_TYPE_BCOMP_ID | ![]() |
where ![]() |
A |
* | SIMP_TYPE_BCOMP_L | ![]() |
where ![]() ![]() |
A |
* | SIMP_TYPE_BCOMP_R | ![]() |
where ![]() ![]() |
A |
* | SIMP_BCOMP_ID | ![]() |
A | |
SIMP_SPECIAL_DPROD_R | ![]() |
A | ||
SIMP_SPECIAL_DPROD_L | ![]() |
A | ||
* | SIMP_TYPE_DPROD | ![]() |
where ![]() ![]() ![]() ![]() |
A |
SIMP_SPECIAL_PPROD_R | ![]() |
A | ||
SIMP_SPECIAL_PPROD_L | ![]() |
A | ||
* | SIMP_TYPE_PPROD | ![]() |
where ![]() ![]() ![]() ![]() |
A |
* | SIMP_SPECIAL_RELIMAGE_R | ![]() |
A | |
SIMP_SPECIAL_RELIMAGE_L | ![]() |
A | ||
* | SIMP_TYPE_RELIMAGE | ![]() |
where ![]() |
A |
* | SIMP_MULTI_RELIMAGE_DOM | ![]() |
A | |
* | SIMP_TYPE_RELIMAGE_ID | ![]() |
where ![]() |
A |
* | SIMP_RELIMAGE_ID | ![]() |
A | |
* | SIMP_MULTI_RELIMAGE_CPROD_SING | ![]() |
where ![]() |
A |
* | SIMP_MULTI_RELIMAGE_SING_MAPSTO | ![]() |
where ![]() |
A |
* | SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB | ![]() |
A | |
* | SIMP_MULTI_RELIMAGE_CONVERSE_RANRES | ![]() |
A | |
* | SIMP_RELIMAGE_CONVERSE_DOMSUB | ![]() |
A | |
* | DERIV_RELIMAGE_RANSUB | ![]() |
M | |
* | DERIV_RELIMAGE_RANRES | ![]() |
M | |
* | SIMP_MULTI_RELIMAGE_DOMSUB | ![]() |
A | |
* | DERIV_RELIMAGE_DOMSUB | ![]() |
M | |
* | DERIV_RELIMAGE_DOMRES | ![]() |
M | |
SIMP_SPECIAL_CONVERSE | ![]() |
A | ||
* | SIMP_CONVERSE_ID | ![]() |
A | |
* | SIMP_TYPE_CONVERSE | ![]() |
where ![]() ![]() |
A |
* | SIMP_CONVERSE_SETENUM | ![]() |
A | |
* | SIMP_CONVERSE_COMPSET | ![]() |
A | |
SIMP_SPECIAL_ID | ![]() |
A | ||
* | SIMP_DOM_ID | ![]() |
A | |
* | SIMP_RAN_ID | ![]() |
A | |
* | SIMP_FCOMP_ID_L | ![]() |
A | |
* | SIMP_FCOMP_ID_R | ![]() |
A | |
SIMP_SPECIAL_REL_R | ![]() |
idem for operators ![]() |
A | |
SIMP_SPECIAL_REL_L | ![]() |
idem for operators ![]() |
A | |
SIMP_SPECIAL_EQUAL_REL | ![]() |
idem for operators ![]() |
A | |
SIMP_SPECIAL_EQUAL_RELDOM | ![]() |
idem for operators ![]() |
A | |
SIMP_SPECIAL_PRJ1 | ![]() |
A | ||
SIMP_SPECIAL_PRJ2 | ![]() |
A | ||
* | SIMP_FUNIMAGE_PRJ1 | ![]() |
A | |
* | SIMP_FUNIMAGE_PRJ2 | ![]() |
A | |
* | SIMP_DOM_PRJ1 | ![]() |
A | |
* | SIMP_DOM_PRJ2 | ![]() |
A | |
* | SIMP_RAN_PRJ1 | ![]() |
A | |
* | SIMP_RAN_PRJ2 | ![]() |
A | |
SIMP_SPECIAL_LAMBDA | ![]() |
A | ||
* | SIMP_FUNIMAGE_LAMBDA | ![]() |
A | |
* | SIMP_DOM_LAMBDA | ![]() |
A | |
* | SIMP_RAN_LAMBDA | ![]() |
A | |
* | SIMP_MULTI_FUNIMAGE_SETENUM_LL | ![]() |
A | |
* | SIMP_MULTI_FUNIMAGE_SETENUM_LR | ![]() |
A | |
* | SIMP_MULTI_FUNIMAGE_OVERL_SETENUM | ![]() |
A | |
* | SIMP_MULTI_FUNIMAGE_BUNION_SETENUM | ![]() |
A | |
* | SIMP_FUNIMAGE_CPROD | ![]() |
A | |
* | SIMP_FUNIMAGE_ID | ![]() |
A | |
* | SIMP_FUNIMAGE_FUNIMAGE_CONVERSE | ![]() |
A | |
* | SIMP_FUNIMAGE_CONVERSE_FUNIMAGE | ![]() |
A | |
* | SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM | ![]() |
A | |
* | DEF_BCOMP | ![]() |
M | |
* | DERIV_ID_SING | ![]() |
where ![]() |
M |
* | SIMP_SPECIAL_DOM | ![]() |
A | |
* | SIMP_SPECIAL_RAN | ![]() |
A | |
* | SIMP_CONVERSE_CONVERSE | ![]() |
A | |
* | DERIV_RELIMAGE_FCOMP | ![]() |
M | |
* | DERIV_FCOMP_DOMRES | ![]() |
M | |
* | DERIV_FCOMP_DOMSUB | ![]() |
M | |
* | DERIV_FCOMP_RANRES | ![]() |
M | |
* | DERIV_FCOMP_RANSUB | ![]() |
M | |
SIMP_SPECIAL_EQUAL_RELDOMRAN | ![]() |
idem for operators ![]() |
A | |
* | SIMP_TYPE_DOM | ![]() |
where ![]() ![]() |
A |
* | SIMP_TYPE_RAN | ![]() |
where ![]() ![]() |
A |
* | SIMP_MULTI_DOM_CPROD | ![]() |
A | |
* | SIMP_MULTI_RAN_CPROD | ![]() |
A | |
* | DEF_IN_DOM | ![]() |
M | |
* | DEF_IN_RAN | ![]() |
M | |
* | DEF_IN_CONVERSE | ![]() |
M | |
* | DEF_IN_DOMRES | ![]() |
M | |
* | DEF_IN_RANRES | ![]() |
M | |
* | DEF_IN_DOMSUB | ![]() |
M | |
* | DEF_IN_RANSUB | ![]() |
M | |
* | DEF_IN_RELIMAGE | ![]() |
M | |
* | DEF_IN_FCOMP | ![]() |
M | |
* | DEF_OVERL | ![]() |
M | |
* | DEF_IN_ID | ![]() |
M | |
* | DEF_IN_DPROD | ![]() |
M | |
* | DEF_IN_PPROD | ![]() |
M | |
* | DEF_IN_RELDOM | ![]() |
M | |
* | DEF_IN_RELRAN | ![]() |
M | |
* | DEF_IN_RELDOMRAN | ![]() |
M | |
* | DEF_IN_FCT | ![]() |
M | |
* | DEF_IN_TFCT | ![]() |
M | |
* | DEF_IN_INJ | ![]() |
M | |
* | DEF_IN_TINJ | ![]() |
M | |
* | DEF_IN_SURJ | ![]() |
M | |
* | DEF_IN_TSURJ | ![]() |
M | |
* | DEF_IN_BIJ | ![]() |
M | |
* | DISTRI_BCOMP_BUNION | ![]() |
M | |
* | DISTRI_FCOMP_BUNION_R | ![]() |
M | |
* | DISTRI_FCOMP_BUNION_L | ![]() |
M | |
* | DISTRI_DPROD_BUNION | ![]() |
M | |
* | DISTRI_DPROD_BINTER | ![]() |
M | |
* | DISTRI_DPROD_SETMINUS | ![]() |
M | |
* | DISTRI_DPROD_OVERL | ![]() |
M | |
* | DISTRI_PPROD_BUNION | ![]() |
M | |
* | DISTRI_PPROD_BINTER | ![]() |
M | |
* | DISTRI_PPROD_SETMINUS | ![]() |
M | |
* | DISTRI_PPROD_OVERL | ![]() |
M | |
* | DISTRI_OVERL_BUNION_L | ![]() |
M | |
* | DISTRI_OVERL_BINTER_L | ![]() |
M | |
* | DISTRI_DOMRES_BUNION_R | ![]() |
M | |
* | DISTRI_DOMRES_BUNION_L | ![]() |
M | |
* | DISTRI_DOMRES_BINTER_R | ![]() |
M | |
* | DISTRI_DOMRES_BINTER_L | ![]() |
M | |
* | DISTRI_DOMRES_SETMINUS_R | ![]() |
M | |
* | DISTRI_DOMRES_SETMINUS_L | ![]() |
M | |
* | DISTRI_DOMRES_DPROD | ![]() |
M | |
* | DISTRI_DOMRES_OVERL | ![]() |
M | |
* | DISTRI_DOMSUB_BUNION_R | ![]() |
M | |
* | DISTRI_DOMSUB_BUNION_L | ![]() |
M | |
* | DISTRI_DOMSUB_BINTER_R | ![]() |
M | |
* | DISTRI_DOMSUB_BINTER_L | ![]() |
M | |
* | DISTRI_DOMSUB_DPROD | ![]() |
M | |
* | DISTRI_DOMSUB_OVERL | ![]() |
M | |
* | DISTRI_RANRES_BUNION_R | ![]() |
M | |
* | DISTRI_RANRES_BUNION_L | ![]() |
M | |
* | DISTRI_RANRES_BINTER_R | ![]() |
M | |
* | DISTRI_RANRES_BINTER_L | ![]() |
M | |
* | DISTRI_RANRES_SETMINUS_R | ![]() |
M | |
* | DISTRI_RANRES_SETMINUS_L | ![]() |
M | |
* | DISTRI_RANSUB_BUNION_R | ![]() |
M | |
* | DISTRI_RANSUB_BUNION_L | ![]() |
M | |
* | DISTRI_RANSUB_BINTER_R | ![]() |
M | |
* | DISTRI_RANSUB_BINTER_L | ![]() |
M | |
* | DISTRI_CONVERSE_BUNION | ![]() |
M | |
* | DISTRI_CONVERSE_BINTER | ![]() |
M | |
* | DISTRI_CONVERSE_SETMINUS | ![]() |
M | |
* | DISTRI_CONVERSE_BCOMP | ![]() |
M | |
* | DISTRI_CONVERSE_FCOMP | ![]() |
M | |
* | DISTRI_CONVERSE_PPROD | ![]() |
M | |
* | DISTRI_CONVERSE_DOMRES | ![]() |
M | |
* | DISTRI_CONVERSE_DOMSUB | ![]() |
M | |
* | DISTRI_CONVERSE_RANRES | ![]() |
M | |
* | DISTRI_CONVERSE_RANSUB | ![]() |
M | |
* | DISTRI_DOM_BUNION | ![]() |
M | |
* | DISTRI_RAN_BUNION | ![]() |
M | |
* | DISTRI_RELIMAGE_BUNION_R | ![]() |
M | |
* | DISTRI_RELIMAGE_BUNION_L | ![]() |
M | |
* | DISTRI_DOM_BUNION | ![]() |
M | |
* | DISTRI_RAN_BUNION | ![]() |
M |