Difference between revisions of "Relation Rewrite Rules"
From Event-B
Jump to navigationJump to searchimported>Laurent (Fixed rule DISTRI_BCOMP_BUNION) |
imported>Laurent (Fixed broken rules DISTRI_DOMSUB_BUNION_L, DISTRI_DOMSUB_BINTER_L, DISTRI_RANSUB_BUNION_R and DISTRI_RANSUB_BINTER_R) |
||
Line 157: | Line 157: | ||
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_OVERL}}||<math> s \domres (r \ovl q) \;\;\defi\;\; (s \domres r) \ovl (s \domres q) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_DOMRES_OVERL}}||<math> s \domres (r \ovl q) \;\;\defi\;\; (s \domres r) \ovl (s \domres q) </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BUNION_R}}||<math> s \domsub (p \bunion q) \;\;\defi\;\; (s \domsub p) \bunion (s \domsub q) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BUNION_R}}||<math> s \domsub (p \bunion q) \;\;\defi\;\; (s \domsub p) \bunion (s \domsub q) </math>|| || M | ||
− | {{RRRow}}| | + | {{RRRow}}|b||{{Rulename|DISTRI_DOMSUB_BUNION_L}}||<math> (s \bunion t) \domsub r \;\;\defi\;\; (s \domsub r) \binter (t \domsub r) </math>|| || M |
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BINTER_R}}||<math> s \domsub (p \binter q) \;\;\defi\;\; (s \domsub p) \binter (s \domsub q) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BINTER_R}}||<math> s \domsub (p \binter q) \;\;\defi\;\; (s \domsub p) \binter (s \domsub q) </math>|| || M | ||
− | {{RRRow}}| | + | {{RRRow}}|b||{{Rulename|DISTRI_DOMSUB_BINTER_L}}||<math> (s \binter t) \domsub r \;\;\defi\;\; (s \domsub r) \bunion (t \domsub r) </math>|| || M |
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_DPROD}}||<math> A \domsub (r \dprod s) \;\;\defi\;\; (A \domsub r) \dprod (A \domsub s) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_DPROD}}||<math> A \domsub (r \dprod s) \;\;\defi\;\; (A \domsub r) \dprod (A \domsub s) </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_OVERL}}||<math> A \domsub (r \ovl s) \;\;\defi\;\; (A \domsub r) \ovl (A \domsub s) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_OVERL}}||<math> A \domsub (r \ovl s) \;\;\defi\;\; (A \domsub r) \ovl (A \domsub s) </math>|| || M | ||
Line 168: | Line 168: | ||
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_SETMINUS_R}}||<math> r \ranres (s \setminus t) \;\;\defi\;\; (r \ranres s) \setminus (r \ranres t) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_RANRES_SETMINUS_R}}||<math> r \ranres (s \setminus t) \;\;\defi\;\; (r \ranres s) \setminus (r \ranres t) </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_SETMINUS_L}}||<math> (p \setminus q) \ranres s \;\;\defi\;\; (p \ranres s) \setminus (q \ranres s) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_RANRES_SETMINUS_L}}||<math> (p \setminus q) \ranres s \;\;\defi\;\; (p \ranres s) \setminus (q \ranres s) </math>|| || M | ||
− | {{RRRow}}| | + | {{RRRow}}|b||{{Rulename|DISTRI_RANSUB_BUNION_R}}||<math> r \ransub (s\bunion t) \;\;\defi\;\; (r \ransub s) \binter (r \ransub t) </math>|| || M |
{{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BUNION_L}}||<math> (p \bunion q) \ransub s \;\;\defi\;\; (p \ransub s) \bunion (q \ransub s) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BUNION_L}}||<math> (p \bunion q) \ransub s \;\;\defi\;\; (p \ransub s) \bunion (q \ransub s) </math>|| || M | ||
− | {{RRRow}}| | + | {{RRRow}}|b||{{Rulename|DISTRI_RANSUB_BINTER_R}}||<math> r \ransub (s \binter t) \;\;\defi\;\; (r \ransub s) \bunion (r \ransub t) </math>|| || M |
{{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BINTER_L}}||<math> (p \binter q) \ransub s \;\;\defi\;\; (p \ransub s) \binter (q \ransub s) </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BINTER_L}}||<math> (p \binter q) \ransub s \;\;\defi\;\; (p \ransub s) \binter (q \ransub s) </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_BUNION}}||<math> (p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1} </math>|| || M | {{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_BUNION}}||<math> (p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1} </math>|| || M |
Revision as of 23:11, 18 December 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 |
![]() |
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 |
![]() |
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 |
![]() |
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 |
![]() |
where ![]() ![]() |
A |
* | SIMP_RAN_ID |
![]() |
where ![]() ![]() |
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 |
![]() |
where ![]() ![]() |
A |
* | SIMP_DOM_PRJ2 |
![]() |
where ![]() ![]() |
A |
* | SIMP_RAN_PRJ1 |
![]() |
where ![]() ![]() |
A |
* | SIMP_RAN_PRJ2 |
![]() |
where ![]() ![]() |
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 | |
b | DISTRI_DOMSUB_BUNION_L |
![]() |
M | |
* | DISTRI_DOMSUB_BINTER_R |
![]() |
M | |
b | 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 | |
b | DISTRI_RANSUB_BUNION_R |
![]() |
M | |
* | DISTRI_RANSUB_BUNION_L |
![]() |
M | |
b | 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 | |
* | DERIV_DOM_TOTALREL |
![]() |
with hypothesis ![]() ![]() ![]() |
M |
DERIV_RAN_SURJREL |
![]() |
with hypothesis ![]() ![]() ![]() |
M | |
prjone-total |
![]() |
A | ||
prjtwo-total |
![]() |
A | ||
prjone-functional |
![]() |
where \mathit{op} is one of ![]() |
A | |
prjtwo-functional |
![]() |
where \mathit{op} is one of ![]() |
A | |
prj-expand |
![]() |
M |