Relation Rewrite Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Frederic No edit summary |
imported>Frederic No edit summary |
||
Line 134: | Line 134: | ||
{{RRRow}}|<font size="-2"> DEF_IN_TSURJ </font>||<math> f \in S \tsur T \;\;\defi\;\; f \in S \psur T \land \dom (f) = S </math>|| || M | {{RRRow}}|<font size="-2"> DEF_IN_TSURJ </font>||<math> f \in S \tsur T \;\;\defi\;\; f \in S \psur T \land \dom (f) = S </math>|| || M | ||
{{RRRow}}|<font size="-2"> DEF_IN_BIJ </font>||<math> f \in S \tbij T \;\;\defi\;\; f \in S \tinj T \land \ran (f) = T </math>|| || M | {{RRRow}}|<font size="-2"> DEF_IN_BIJ </font>||<math> f \in S \tbij T \;\;\defi\;\; f \in S \tinj T \land \ran (f) = T </math>|| || M | ||
{{RRRow}}|<font size="-2"> DISTRI_BCOMP_BUNION </font>||<math> r \bcomp (s \bunion t) \;\;\defi\;\; (r \bcomp s) \bunion (r \bcomp s) </math>|| || M | {{RRRow}}|<font size="-2"> DISTRI_BCOMP_BUNION </font>||<math> r \bcomp (s \bunion t) \;\;\defi\;\; (r \bcomp s) \bunion (r \bcomp s) </math>|| || M | ||
{{RRRow}}|<font size="-2"> DISTRI_FCOMP_BUNION_R </font>||<math> p \fcomp (q \bunion r) \;\;\defi\;\; (p \fcomp q) \bunion (p \fcomp r) </math>|| || M | {{RRRow}}|<font size="-2"> DISTRI_FCOMP_BUNION_R </font>||<math> p \fcomp (q \bunion r) \;\;\defi\;\; (p \fcomp q) \bunion (p \fcomp r) </math>|| || M | ||
Line 188: | Line 187: | ||
{{RRRow}}|<font size="-2"> DISTRI_DOM_BUNION </font>||<math> \dom (p \bunion q) \;\;\defi\;\; \dom (p) \bunion \dom (q) </math>|| || M | {{RRRow}}|<font size="-2"> DISTRI_DOM_BUNION </font>||<math> \dom (p \bunion q) \;\;\defi\;\; \dom (p) \bunion \dom (q) </math>|| || M | ||
{{RRRow}}|<font size="-2"> DISTRI_RAN_BUNION </font>||<math> \ran (p \bunion q) \;\;\defi\;\; \ran (p) \bunion \ran (q) </math>|| || M | {{RRRow}}|<font size="-2"> DISTRI_RAN_BUNION </font>||<math> \ran (p \bunion q) \;\;\defi\;\; \ran (p) \bunion \ran (q) </math>|| || M | ||
|} | |} | ||
Revision as of 10:13, 30 January 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 is a type expression | A | ||
SIMP_SPECIAL_DOMRES_L | A | |||
SIMP_SPECIAL_DOMRES_R | A | |||
SIMP_TYPE_DOMRES | where is a type expression | 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 is a type expression | 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 is a type expression | A | ||
SIMP_MULTI_DOMSUB_DOM | A | |||
SIMP_DOMSUB_ID | A | |||
SIMP_SPECIAL_RANSUB_R | A | |||
SIMP_SPECIAL_RANSUB_L | A | |||
SIMP_TYPE_RANSUB | where is a type expression | A | ||
SIMP_MULTI_RANSUB_RAN | A | |||
SIMP_RANSUB_ID | A | |||
SIMP_SPECIAL_FCOMP | A | |||
SIMP_TYPE_FCOMP_ID | where is a type expression | A | ||
SIMP_TYPE_FCOMP_R | where is a type expression equal to | A | ||
SIMP_TYPE_FCOMP_L | where is a type expression equal to | A | ||
SIMP_FCOMP_ID | A | |||
SIMP_SPECIAL_BCOMP | A | |||
SIMP_TYPE_BCOMP_ID | where is a type expression | A | ||
SIMP_TYPE_BCOMP_L | where is a type expression equal to | A | ||
SIMP_TYPE_BCOMP_R | where is a type expression equal to | A | ||
SIMP_BCOMP_ID | A | |||
SIMP_SPECIAL_DPROD_R | A | |||
SIMP_SPECIAL_DPROD_L | A | |||
SIMP_TYPE_DPROD | where \mathit{Ta} and \mathit{Tb} are type expressions and and | A | ||
SIMP_SPECIAL_PPROD_R | A | |||
SIMP_SPECIAL_PPROD_L | A | |||
SIMP_TYPE_PPROD | where \mathit{Ta} and \mathit{Tb} are type expressions and and | A | ||
SIMP_SPECIAL_RELIMAGE_R | A | |||
SIMP_SPECIAL_RELIMAGE_L | A | |||
SIMP_TYPE_RELIMAGE | where is a type expression | A | ||
SIMP_MULTI_RELIMAGE_DOM | A | |||
SIMP_TYPE_RELIMAGE_ID | where is a type expression | A | ||
SIMP_RELIMAGE_ID | A | |||
SIMP_MULTI_RELIMAGE_CPROD_SING | where is a single expression | A | ||
SIMP_MULTI_RELIMAGE_SING_MAPSTO | where is a single expression | 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 is a type expression equal to | 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 | |||
DEF_BCOMP | M | |||
DERIV_ID_SING | where is a single expression | 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 is a type expression equal to | A | ||
SIMP_TYPE_RAN | where is a type expression equal to | 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 |