Difference between revisions of "Relation Rewrite Rules"
From Event-B
Jump to navigationJump to searchimported>Laurent (Refactor rules about projections) |
(Rules DEF_EQUAL_FUN_IMAGE and SIMP_SPECIAL_IN_*ID have been implemented in Rodin 3.9) |
||
(5 intermediate revisions by 2 users not shown) | |||
Line 111: | Line 111: | ||
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_RANSUB}}||<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> || with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. || AM | {{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_RANSUB}}||<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> || with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. || AM | ||
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_SETMINUS}}||<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> || with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. || AM | {{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_SETMINUS}}||<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> || with hypothesis<math> F \in \mathit{A} \ \mathit{op}\ \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>. || AM | ||
− | {{RRRow}}|||{{Rulename|DEF_BCOMP}}||<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>|| || M | + | {{RRRow}}|*||{{Rulename|DEF_EQUAL_FUNIMAGE}}||<math> f(x) = y \;\;\defi\;\; x \mapsto y \in f </math>|| || M |
+ | {{RRRow}}|*||{{Rulename|DEF_BCOMP}}||<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>|| || M | ||
{{RRRow}}|||{{Rulename|DERIV_ID_SING}}||<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>|| where <math>E</math> is a single expression || M | {{RRRow}}|||{{Rulename|DERIV_ID_SING}}||<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math>|| where <math>E</math> is a single expression || M | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DOM}}||<math> \dom (\emptyset ) \;\;\defi\;\; \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DOM}}||<math> \dom (\emptyset ) \;\;\defi\;\; \emptyset </math>|| || A | ||
Line 209: | Line 210: | ||
{{RRRow}}|*||{{Rulename|DERIV_DOM_TOTALREL}}||<math> \dom (r) \;\;\defi\;\; E </math> || with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> || M | {{RRRow}}|*||{{Rulename|DERIV_DOM_TOTALREL}}||<math> \dom (r) \;\;\defi\;\; E </math> || with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> || M | ||
{{RRRow}}| ||{{Rulename|DERIV_RAN_SURJREL}}||<math> \ran (r) \;\;\defi\;\; F </math> || with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\srel,\strel, \psur, \tsur, \tbij</math> || M | {{RRRow}}| ||{{Rulename|DERIV_RAN_SURJREL}}||<math> \ran (r) \;\;\defi\;\; F </math> || with hypothesis <math>r \in E \ \mathit{op}\ F</math>, where <math>\mathit{op}</math> is one of <math>\srel,\strel, \psur, \tsur, \tbij</math> || M | ||
− | {{RRRow}}| ||{{Rulename|DERIV_PRJ1_SURJ}}||<math>\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> || where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> || A | + | {{RRRow}}|*||{{Rulename|DERIV_PRJ1_SURJ}}||<math>\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> || where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> || A |
− | {{RRRow}}| ||{{Rulename|DERIV_PRJ2_SURJ}}||<math>\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> || where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> || A | + | {{RRRow}}|*||{{Rulename|DERIV_PRJ2_SURJ}}||<math>\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> || where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> || A |
− | {{RRRow}}| ||{{Rulename|SIMP_MAPSTO_PRJ1_PRJ2}}||<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> || || A | + | {{RRRow}}|*||{{Rulename|DERIV_ID_BIJ}}||<math>\id \in\mathit{Ty}\ \mathit{op}\ \mathit{Ty}\;\;\defi\;\; \btrue </math> || where <math>\mathit{Ty}</math> is a type and <math>\mathit{op}</math> is any arrow || A |
+ | {{RRRow}}|*||{{Rulename|SIMP_MAPSTO_PRJ1_PRJ2}}||<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> || || A | ||
{{RRRow}}| ||{{Rulename|DERIV_EXPAND_PRJS}}||<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> || || M | {{RRRow}}| ||{{Rulename|DERIV_EXPAND_PRJS}}||<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> || || M | ||
{{RRRow}}|*||{{Rulename|SIMP_DOM_SUCC}}||<math>\dom(\usucc) \;\;\defi\;\; \intg</math> || || A | {{RRRow}}|*||{{Rulename|SIMP_DOM_SUCC}}||<math>\dom(\usucc) \;\;\defi\;\; \intg</math> || || A | ||
Line 218: | Line 220: | ||
{{RRRow}}|*||{{Rulename|DERIV_MULTI_IN_SETMINUS}}||<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> || || A | {{RRRow}}|*||{{Rulename|DERIV_MULTI_IN_SETMINUS}}||<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> || || A | ||
{{RRRow}}|*||{{Rulename|DEF_PRED}}||<math> \upred\;\;\defi\;\; \usucc^{-1}</math> || || A | {{RRRow}}|*||{{Rulename|DEF_PRED}}||<math> \upred\;\;\defi\;\; \usucc^{-1}</math> || || A | ||
+ | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN_ID}}||<math> E \mapsto E \in \id \;\;\defi\;\; \btrue</math> || || A | ||
+ | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN_SETMINUS_ID}}||<math>E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse</math> || || A | ||
+ | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN_DOMRES_ID}}||<math>E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S</math> || || A | ||
+ | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID}}||<math>E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r</math> || || A | ||
|} | |} |
Latest revision as of 15:13, 3 June 2024
Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_Rules.
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | SIMP_DOM_SETENUM |
![]() |
A | |
* | SIMP_DOM_CONVERSE |
![]() |
A | |
* | SIMP_RAN_SETENUM |
![]() |
A | |
* | SIMP_RAN_CONVERSE |
![]() |
A | |
* | SIMP_SPECIAL_OVERL |
![]() |
A | |
* | SIMP_MULTI_OVERL |
![]() |
there is a ![]() ![]() ![]() ![]() |
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_DOMRES_ID |
![]() |
A | |
* | SIMP_DOMRES_DOMSUB_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_RANSUB_ID |
![]() |
A | |
* | SIMP_RANRES_DOMRES_ID |
![]() |
A | |
* | SIMP_RANRES_DOMSUB_ID |
![]() |
A | |
* | SIMP_SPECIAL_DOMSUB_L |
![]() |
A | |
* | SIMP_SPECIAL_DOMSUB_R |
![]() |
A | |
* | SIMP_TYPE_DOMSUB |
![]() |
where ![]() |
A |
* | SIMP_MULTI_DOMSUB_DOM |
![]() |
A | |
* | SIMP_MULTI_DOMSUB_RAN |
![]() |
A | |
* | SIMP_DOMSUB_DOMRES_ID |
![]() |
A | |
* | SIMP_DOMSUB_DOMSUB_ID |
![]() |
A | |
* | SIMP_SPECIAL_RANSUB_R |
![]() |
A | |
* | SIMP_SPECIAL_RANSUB_L |
![]() |
A | |
* | SIMP_TYPE_RANSUB |
![]() |
where ![]() |
A |
* | SIMP_MULTI_RANSUB_DOM |
![]() |
A | |
* | SIMP_MULTI_RANSUB_RAN |
![]() |
A | |
* | SIMP_RANSUB_DOMRES_ID |
![]() |
A | |
* | SIMP_RANSUB_DOMSUB_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_DPROD_CPROD |
![]() |
A | |
* | SIMP_SPECIAL_PPROD_R |
![]() |
A | |
* | SIMP_SPECIAL_PPROD_L |
![]() |
A | |
* | SIMP_PPROD_CPROD |
![]() |
A | |
* | SIMP_SPECIAL_RELIMAGE_R |
![]() |
A | |
* | SIMP_SPECIAL_RELIMAGE_L |
![]() |
A | |
* | SIMP_TYPE_RELIMAGE |
![]() |
where ![]() |
A |
* | SIMP_MULTI_RELIMAGE_DOM |
![]() |
A | |
* | SIMP_RELIMAGE_ID |
![]() |
A | |
* | SIMP_RELIMAGE_DOMRES_ID |
![]() |
A | |
* | SIMP_RELIMAGE_DOMSUB_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_CONVERSE_CPROD |
![]() |
A | |
* | SIMP_CONVERSE_SETENUM |
![]() |
A | |
* | SIMP_CONVERSE_COMPSET |
![]() |
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_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_FUNIMAGE_LAMBDA |
![]() |
A | |
* | SIMP_DOM_LAMBDA |
![]() |
A | |
* | SIMP_RAN_LAMBDA |
![]() |
A | |
* | SIMP_IN_FUNIMAGE |
![]() |
A | |
* | SIMP_IN_FUNIMAGE_CONVERSE_L |
![]() |
A | |
* | SIMP_IN_FUNIMAGE_CONVERSE_R |
![]() |
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 | |
* | SIMP_FUNIMAGE_DOMRES |
![]() |
with hypothesis![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
AM |
* | SIMP_FUNIMAGE_DOMSUB |
![]() |
with hypothesis![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
AM |
* | SIMP_FUNIMAGE_RANRES |
![]() |
with hypothesis![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
AM |
* | SIMP_FUNIMAGE_RANSUB |
![]() |
with hypothesis![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
AM |
* | SIMP_FUNIMAGE_SETMINUS |
![]() |
with hypothesis![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
AM |
* | DEF_EQUAL_FUNIMAGE |
![]() |
M | |
* | 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 | |
DERIV_FCOMP_SING |
![]() |
A | ||
* | 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 | |
* | SIMP_MULTI_DOM_DOMRES |
![]() |
A | |
* | SIMP_MULTI_DOM_DOMSUB |
![]() |
A | |
* | SIMP_MULTI_RAN_RANRES |
![]() |
A | |
* | SIMP_MULTI_RAN_RANSUB |
![]() |
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_REL |
![]() |
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 | |
* | DERIV_DOM_TOTALREL |
![]() |
with hypothesis ![]() ![]() ![]() |
M |
DERIV_RAN_SURJREL |
![]() |
with hypothesis ![]() ![]() ![]() |
M | |
* | DERIV_PRJ1_SURJ |
![]() |
where ![]() ![]() ![]() ![]() |
A |
* | DERIV_PRJ2_SURJ |
![]() |
where ![]() ![]() ![]() ![]() |
A |
* | DERIV_ID_BIJ |
![]() |
where ![]() ![]() |
A |
* | SIMP_MAPSTO_PRJ1_PRJ2 |
![]() |
A | |
DERIV_EXPAND_PRJS |
![]() |
M | ||
* | SIMP_DOM_SUCC |
![]() |
A | |
* | SIMP_RAN_SUCC |
![]() |
A | |
* | DERIV_MULTI_IN_BUNION |
![]() |
A | |
* | DERIV_MULTI_IN_SETMINUS |
![]() |
A | |
* | DEF_PRED |
![]() |
A | |
* | SIMP_SPECIAL_IN_ID |
![]() |
A | |
* | SIMP_SPECIAL_IN_SETMINUS_ID |
![]() |
A | |
* | SIMP_SPECIAL_IN_DOMRES_ID |
![]() |
A | |
* | SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID |
![]() |
A |