Difference between pages "Refactoring Framework" and "Relation Rewrite Rules"
From Event-B
(Difference between pages)
Jump to navigationJump to searchimported>Renato (→News) |
imported>Frederic |
||
Line 1: | Line 1: | ||
− | {| | + | {{RRHeader}} |
− | | | + | {{RRRow}}|<font size="-2"> SIMP_DOM_COMPSET </font>||<math> \dom (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ x, \ldots , y\} </math>|| || A |
+ | {{RRRow}}|<font size="-2"> SIMP_DOM_CONVERSE </font>||<math> \dom (r^{-1} ) \;\;\defi\;\; \ran (r) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_RAN_COMPSET </font>||<math> \ran (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ a, \ldots , b\} </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_RAN_CONVERSE </font>||<math> \ran (r^{-1} ) \;\;\defi\;\; \dom (r) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_OVERL </font>||<math> r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s </math>|| || A | ||
+ | {{RRRow}}|<font size="-2">SIMP_MULTI_OVERL</font>||<math>\begin{array}{cl} & r \ovl \ldots \ovl s \ovl \ldots \ovl s \ovl \ldots \ovl u \\ \defi & r \ovl \ldots \ovl \ldots \ovl s \ovl \ldots \ovl u \end{array}</math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_OVERL_CPROD </font>||<math> r \ovl (\mathit{Ty} \cprod S) \;\;\defi\;\; (\mathit{Ty} \cprod S) </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_DOMRES_L </font>||<math> \emptyset \domres r \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_DOMRES_R </font>||<math> S \domres \emptyset \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_DOMRES </font>||<math> \mathit{Ty} \domres r \;\;\defi\;\; r </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_DOMRES_DOM </font>||<math> \dom (r) \domres r \;\;\defi\;\; r </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_DOMRES_RAN </font>||<math> \ran (r) \domres r^{-1} \;\;\defi\;\; r^{-1} </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_DOMRES_ID </font>||<math> S \domres \id (T) \;\;\defi\;\; \id (S \binter T) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_RANRES_R </font>||<math> r \ranres \emptyset \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_RANRES_L </font>||<math> \emptyset \ranres S \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_RANRES </font>||<math> r \ranres \mathit{Ty} \;\;\defi\;\; r </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_RANRES_RAN </font>||<math> r \ranres \ran (r) \;\;\defi\;\; r </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_RANRES_DOM </font>||<math> r^{-1} \ranres \dom (r) \;\;\defi\;\; r^{-1} </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_RANRES_ID </font>||<math> \id (S) \ranres T \;\;\defi\;\; \id (S \binter T) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_DOMSUB_L </font>||<math> \emptyset \domsub r \;\;\defi\;\; r </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_DOMSUB_R </font>||<math> S \domsub \emptyset \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_DOMSUB </font>||<math> \mathit{Ty} \domsub r \;\;\defi\;\; \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_DOMSUB_DOM </font>||<math> \dom (r) \domsub r \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_DOMSUB_ID </font>||<math> S \domsub \id (T) \;\;\defi\;\; \id (T \setminus S) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_RANSUB_R </font>||<math> r \ransub \emptyset \;\;\defi\;\; r </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_RANSUB_L </font>||<math> \emptyset \ransub S \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_RANSUB </font>||<math> r \ransub \mathit{Ty} \;\;\defi\;\; \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_RANSUB_RAN </font>||<math> r \ransub \ran (r) \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_RANSUB_ID </font>||<math> \id (S) \ransub T \;\;\defi\;\; \id (S \setminus T) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_FCOMP </font>||<math> r \fcomp \ldots \fcomp \emptyset \fcomp \ldots \fcomp s \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_FCOMP_ID </font>||<math> r \fcomp \ldots \fcomp \id (\mathit{Ty}) \fcomp \ldots \fcomp s \;\;\defi\;\; r \fcomp \ldots \fcomp s </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_FCOMP_R </font>||<math> r \fcomp \mathit{Ty} \;\;\defi\;\; \dom (r) \cprod \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_FCOMP_L </font>||<math> \mathit{Ty} \fcomp r \;\;\defi\;\; \mathit{Ta} \cprod \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_FCOMP_ID </font>||<math> r \fcomp \ldots \fcomp \id (S) \fcomp \id (T) \fcomp \ldots s \;\;\defi\;\; r \fcomp \ldots \fcomp \id (S \binter T) \fcomp \ldots \fcomp s </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_BCOMP </font>||<math> r \bcomp \ldots \bcomp \emptyset \bcomp \ldots \bcomp s \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_BCOMP_ID </font>||<math> r \bcomp \ldots \bcomp \id (\mathit{Ty}) \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp s </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_BCOMP_L </font>||<math> \mathit{Ty} \bcomp r \;\;\defi\;\; \dom (r) \cprod \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_BCOMP_R </font>||<math> r \bcomp \mathit{Ty} \;\;\defi\;\; \mathit{Ta} \cprod \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_BCOMP_ID </font>||<math> r \bcomp \ldots \bcomp \id (S) \bcomp \id (T) \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp \id (S \binter T) \bcomp \ldots \bcomp s </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_DPROD_R </font>||<math> r \dprod \emptyset \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_DPROD_L </font>||<math> \emptyset \dprod r \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_DPROD </font>||<math> \mathit{Ta} \dprod \mathit{Tb} \;\;\defi\;\; Tc \cprod (Td \cprod Te) </math>|| where \mathit{Ta} and \mathit{Tb} are type expressions and <math>\mathit{Ta} = \mathit{Tc} \cprod \mathit{Td}</math> and <math>\mathit{Tb} = \mathit{Tc} \cprod \mathit{Te}</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_PPROD_R </font>||<math> r \pprod \emptyset \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_PPROD_L </font>||<math> \emptyset \pprod r \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_PPROD </font>||<math> \mathit{Ta} \pprod \mathit{Tb} \;\;\defi\;\; (Tc \cprod Te) \cprod (Td \cprod Tf) </math>|| where \mathit{Ta} and \mathit{Tb} are type expressions and <math>\mathit{Ta} = \mathit{Tc} \cprod \mathit{Td}</math> and <math>\mathit{Tb} = \mathit{Te} \cprod \mathit{Tf}</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_RELIMAGE_R </font>||<math> r[\emptyset ] \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_RELIMAGE_L </font>||<math> \emptyset [S] \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_RELIMAGE </font>||<math> r[Ty] \;\;\defi\;\; \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_RELIMAGE_DOM </font>||<math> r[\dom (r)] \;\;\defi\;\; \ran (r) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_RELIMAGE_ID </font>||<math> \id (\mathit{Ty})[T] \;\;\defi\;\; T </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_RELIMAGE_ID </font>||<math> \id (S)[T] \;\;\defi\;\; S \binter T </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_RELIMAGE_CPROD_SING </font>||<math> (\{ E\} \cprod S)[\{ E\} ] \;\;\defi\;\; S </math>|| where <math>E</math> is a single expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_RELIMAGE_SING_MAPSTO </font>||<math> \{ E \mapsto F\} [\{ E\} ] \;\;\defi\;\; \{ F\} </math>|| where <math>E</math> is a single expression || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB </font>||<math> (r \ransub S)^{-1} [S] \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_RELIMAGE_CONVERSE_RANRES </font>||<math> (r \ranres S)^{-1} [S] \;\;\defi\;\; r^{-1} [S] </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_RELIMAGE_CONVERSE_DOMSUB </font>||<math> (S \domsub r)^{-1} [T] \;\;\defi\;\; r^{-1} [T] \setminus S </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> DERIV_RELIMAGE_RANSUB </font>||<math> (r \ransub S)[T] \;\;\defi\;\; r[T] \setminus S </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DERIV_RELIMAGE_RANRES </font>||<math> (r \ranres S)[T] \;\;\defi\;\; r[T] \binter S </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_RELIMAGE_DOMSUB </font>||<math> (S \domsub r)[S] \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> DERIV_RELIMAGE_DOMSUB </font>||<math> (S \domsub r)[T] \;\;\defi\;\; r[T \setminus S] </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DERIV_RELIMAGE_DOMRES </font>||<math> (S \domres r)[T] \;\;\defi\;\; r[S \binter T] </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_CONVERSE </font>||<math> \emptyset ^{-1} \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_CONVERSE_ID </font>||<math> \id (S)^{-1} \;\;\defi\;\; \id (S) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_CONVERSE </font>||<math> \mathit{Ty}^{-1} \;\;\defi\;\; \mathit{Tb} \cprod \mathit{Ta} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_CONVERSE_SETENUM </font>||<math> \{ x \mapsto a, \ldots , y \mapsto b\} ^{-1} \;\;\defi\;\; \{ a \mapsto x, \ldots , b \mapsto y\} </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_CONVERSE_COMPSET </font>||<math> \{ x, \ldots , y \qdot P \mid x, \ldots , y\} ^{-1} \;\;\defi\;\; \{ y, \ldots , x \qdot P \mid y, \ldots , x\} </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_ID </font>||<math> \id (\emptyset ) \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_DOM_ID </font>||<math> \dom (\id (S)) \;\;\defi\;\; S </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_RAN_ID </font>||<math> \ran (\id (S)) \;\;\defi\;\; S </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_FCOMP_ID_L </font>||<math> (\id (S) \fcomp r) \;\;\defi\;\; S \domres r </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_FCOMP_ID_R </font>||<math> r \fcomp \id (S) \;\;\defi\;\; r \ranres S </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_REL_R </font>||<math> S \rel \emptyset \;\;\defi\;\; \{ \emptyset \} </math>|| idem for operators <math>\srel \pfun \pinj \psur</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_REL_L </font>||<math> \emptyset \rel S \;\;\defi\;\; \{ \emptyset \} </math>|| idem for operators <math>\trel \pfun \tfun \pinj \tinj</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_EQUAL_REL </font>||<math> A \rel B = \emptyset \;\;\defi\;\; \bfalse </math>|| idem for operators <math>\pfun \pinj</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_EQUAL_RELDOM </font>||<math> A \trel B = \emptyset \;\;\defi\;\; \lnot\, A = \emptyset \land B = \emptyset </math>|| idem for operators <math>\tfun \tinj \tsur \tbij</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_PRJ1 </font>||<math> \prjone (\emptyset ) \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_PRJ2 </font>||<math> \prjtwo (\emptyset ) \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_FUNIMAGE_PRJ1 </font>||<math> \prjone (r)(E \mapsto F) \;\;\defi\;\; E </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_FUNIMAGE_PRJ2 </font>||<math> \prjtwo (r)(E \mapsto F) \;\;\defi\;\; F </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_DOM_PRJ1 </font>||<math> \dom (\prjone (r)) \;\;\defi\;\; r </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_DOM_PRJ2 </font>||<math> \dom (\prjtwo (r)) \;\;\defi\;\; r </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_RAN_PRJ1 </font>||<math> \ran (\prjone (r)) \;\;\defi\;\; \dom (r) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_RAN_PRJ2 </font>||<math> \ran (\prjtwo (r)) \;\;\defi\;\; \ran (r) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_LAMBDA </font>||<math> (\lambda x \qdot \bfalse \mid E) \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_FUNIMAGE_LAMBDA </font>||<math> (\lambda x \qdot P(x) \mid E(x))(y) \;\;\defi\;\; E(y) </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_DOM_LAMBDA </font>||<math> \dom (\lambda x \qdot P \mid E) \;\;\defi\;\; \{ x\qdot P \mid x\} </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_RAN_LAMBDA </font>||<math> \ran (\lambda x \qdot P \mid E) \;\;\defi\;\; \{ x\qdot P \mid E\} </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_FUNIMAGE_SETENUM_LL </font>||<math> \{ A \mapsto E, \ldots , B \mapsto E\} (x) \;\;\defi\;\; E </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_FUNIMAGE_SETENUM_LR </font>||<math> \{ A \mapsto E, \ldots , x \mapsto y, \ldots , B \mapsto F\} (x) \;\;\defi\;\; y </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_FUNIMAGE_OVERL_SETENUM </font>||<math> (r \ovl \ldots \ovl \{ A \mapsto E, \ldots , x \mapsto y, \ldots , B \mapsto F\} )(x) \;\;\defi\;\; y </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_FUNIMAGE_BUNION_SETENUM </font>||<math> (r \bunion \ldots \bunion \{ A \mapsto E, \ldots , x \mapsto y, \ldots , B \mapsto F\} )(x) \;\;\defi\;\; y </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_FUNIMAGE_CPROD </font>||<math> (S \cprod \{ F\} )(x) \;\;\defi\;\; F </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_CONVERSE_FUNIMAGE </font>||<math> f(f(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"> DERIV_ID_SING </font>||<math> \id (\{ E\} ) \;\;\defi\;\; \{ E \mapsto E\} </math>|| where <math>E</math> is a single expression || M | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_DOM </font>||<math> \dom (\emptyset ) \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_RAN </font>||<math> \ran (\emptyset ) \;\;\defi\;\; \emptyset </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_CONVERSE_CONVERSE </font>||<math> r^{-1-1} \;\;\defi\;\; r </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> DERIV_RELIMAGE_FCOMP </font>||<math> (p \fcomp q)[s] \;\;\defi\;\; q[p[s]] </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DERIV_FCOMP_DOMRES </font>||<math> (s \domres p) \fcomp q \;\;\defi\;\; s \domres (p \fcomp q) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DERIV_FCOMP_DOMSUB </font>||<math> (s \domsub p) \fcomp q \;\;\defi\;\; s \domsub (p \fcomp q) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DERIV_FCOMP_RANRES </font>||<math> p \fcomp (q \ranres s) \;\;\defi\;\; (p \fcomp q) \ranres s </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DERIV_FCOMP_RANSUB </font>||<math> p \fcomp (q \ransub s) \;\;\defi\;\; (p \fcomp q) \ransub s </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> SIMP_SPECIAL_EQUAL_RELDOMRAN </font>||<math> \emptyset \strel \emptyset \;\;\defi\;\; \{ \emptyset \} </math>|| idem for operators <math>\tsur \tbij</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_DOM </font>||<math> \dom (\mathit{Ty}) \;\;\defi\;\; \mathit{Ta} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \rel \mathit{Tb}</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_TYPE_RAN </font>||<math> \ran (\mathit{Ty}) \;\;\defi\;\; \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \rel \mathit{Tb}</math> || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_DOM_CPROD </font>||<math> \dom (E \cprod E) \;\;\defi\;\; E </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> SIMP_MULTI_RAN_CPROD </font>||<math> \ran (E \cprod E) \;\;\defi\;\; E </math>|| || A | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_DOM </font>||<math> E \in \dom (r) \;\;\defi\;\; \exists y \qdot E \mapsto y \in r </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_RAN </font>||<math> F \in \ran (r) \;\;\defi\;\; \exists x \qdot x \mapsto F \in r </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_CONVERSE </font>||<math> E \mapsto F \in r^{-1} \;\;\defi\;\; F \mapsto E \in r </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_DOMRES </font>||<math> E \mapsto F \in S \domres r \;\;\defi\;\; E \in S \land E \mapsto F \in r </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_RANRES </font>||<math> E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \in T </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_DOMSUB </font>||<math> E \mapsto F \in S \domsub r \;\;\defi\;\; E \notin S \land E \mapsto F \in r </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_RANSUB </font>||<math> E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \notin T </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_RELIMAGE </font>||<math> F \in r[w] \;\;\defi\;\; \exists x \qdot x \in w \land x \mapsto F \in r </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_FCOMP </font>||<math> E \mapsto F \in (p \fcomp q) \;\;\defi\;\; \exists x \qdot E \mapsto x \in p \land x \mapsto F \in q </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_OVERL </font>||<math> p \ovl q \;\;\defi\;\; (\dom (q) \domsub p) \bunion q </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_ID </font>||<math> E \mapsto F \in \id (S) \;\;\defi\;\; E \in S \land F = E </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_DPROD </font>||<math> E \mapsto (F \mapsto G) \in p \dprod q \;\;\defi\;\; E \mapsto F \in p \land E \mapsto G \in q </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_PPROD </font>||<math> (E \mapsto G) \mapsto (F \mapsto H) \in p \pprod q \;\;\defi\;\; E \mapsto F \in p \land G \mapsto H \in q </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_RELDOM </font>||<math> r \in S \trel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_RELRAN </font>||<math> r \in S \trel T \;\;\defi\;\; r \in S \rel T \land \ran (r) = T </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_RELDOMRAN </font>||<math> r \in S \strel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S \land \ran (r) = T </math>|| || M | ||
+ | {{RRRow}}|<font size="-2">DEF_IN_FCT</font>||<math>\begin{array}{rcl} | ||
+ | f \in S \pfun T & \defi & f \in S \rel T \\ & \land & (\forall x,y,z \qdot x \mapsto y \in f \land x \mapsto z \in f \limp y = z) \\ \end{array} </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_TFCT </font>||<math> f \in S \tfun T \;\;\defi\;\; f \in S \pfun T \land \dom (f) = S </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_INJ </font>||<math> f \in S \pinj T \;\;\defi\;\; f \in S \pfun T \land f^{-1} \in T \pfun S </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_TINJ </font>||<math> f \in S \tinj T \;\;\defi\;\; f \in S \pinj T \land \dom (f) = S </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DEF_IN_SURJ </font>||<math> f \in S \pfun T \;\;\defi\;\; f \in S \pfun T \land \ran (f) = T </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"> DISTRI_CONVERSE_BUNION </font>||<math> (p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1} </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_L </font>||<math> (q \bunion r) \fcomp p \;\;\defi\;\; (q \fcomp p) \bunion (r \fcomp p) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DPROD_BUNION </font>||<math> r \dprod (s \bunion t) \;\;\defi\;\; (r \dprod s) \bunion (r \dprod t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DPROD_BINTER </font>||<math> r \dprod (s \binter t) \;\;\defi\;\; (r \dprod s) \binter (r \dprod t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DPROD_SETMINUS </font>||<math> r \dprod (s \setminus t) \;\;\defi\;\; (r \dprod s) \setminus (r \dprod t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DPROD_OVERL </font>||<math> r \dprod (s \ovl t) \;\;\defi\;\; (r \dprod s) \ovl (r \dprod t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_PPROD_BUNION </font>||<math> r \pprod (s \bunion t) \;\;\defi\;\; (r \pprod s) \bunion (r \pprod t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_PPROD_BINTER </font>||<math> r \pprod (s \binter t) \;\;\defi\;\; (r \pprod s) \binter (r \pprod t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_PPROD_SETMINUS </font>||<math> r \pprod (s \setminus t) \;\;\defi\;\; (r \pprod s) \setminus (r \pprod t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_PPROD_OVERL </font>||<math> r \pprod (s \ovl t) \;\;\defi\;\; (r \pprod s) \ovl (r \pprod t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_OVERL_BUNION_L </font>||<math> (p \bunion q) \ovl r \;\;\defi\;\; (p \ovl r) \bunion (q \ovl r) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_OVERL_BINTER_L </font>||<math> (p \binter q) \ovl r \;\;\defi\;\; (p \ovl r) \binter (q \ovl r) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMRES_BUNION_R </font>||<math> s \domres (p \bunion q) \;\;\defi\;\; (s \domres p) \bunion (s \domres q) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMRES_BUNION_L </font>||<math> (s \bunion t) \domres r \;\;\defi\;\; (s \domres r) \bunion (t \domres r) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMRES_BINTER_R </font>||<math> s \domres (p \binter q) \;\;\defi\;\; (s \domres p) \binter (s \domres q) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMRES_BINTER_L </font>||<math> (s \binter t) \domres r \;\;\defi\;\; (s \domres r) \binter (t \domres r) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMRES_SETMINUS_R </font>||<math> s \domres (p \setminus q) \;\;\defi\;\; (s \domres p) \setminus (s \domres q) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMRES_SETMINUS_L </font>||<math> (s \setminus t) \domres r \;\;\defi\;\; (s \domres r) \setminus (t \domres r) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMRES_DPROD </font>||<math> s \domres (p \dprod q) \;\;\defi\;\; (s \domres p) \dprod (s \domres q) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMRES_OVERL </font>||<math> s \domres (r \ovl q) \;\;\defi\;\; (s \domres r) \ovl (s \domres q) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMSUB_BUNION_R </font>||<math> s \domsub (p \bunion q) \;\;\defi\;\; (s \domsub p) \bunion (s \domsub q) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMSUB_BUNION_L </font>||<math> (s \bunion t) \domsub r \;\;\defi\;\; (s \domsub r) \bunion (t \domsub r) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMSUB_BINTER_R </font>||<math> s \domsub (p \binter q) \;\;\defi\;\; (s \domsub p) \binter (s \domsub q) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMSUB_BINTER_L </font>||<math> (s \binter t) \domsub r \;\;\defi\;\; (s \domsub r) \binter (t \domsub r) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMSUB_DPROD </font>||<math> A \domsub (r \dprod s) \;\;\defi\;\; (A \domsub r) \dprod (A \domsub s) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOMSUB_OVERL </font>||<math> A \domsub (r \ovl s) \;\;\defi\;\; (A \domsub r) \ovl (A \domsub s) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RANRES_BUNION_R </font>||<math> (r \bunion s) \ranres t \;\;\defi\;\; (r \ranres t) \bunion (s \ranres t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RANRES_BUNION_L </font>||<math> (p \bunion q) \ranres s \;\;\defi\;\; (p \ranres s) \bunion (q \ranres s) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RANRES_BINTER_R </font>||<math> (r \binter s) \ranres t \;\;\defi\;\; (r \ranres t) \binter (s \ranres t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RANRES_BINTER_L </font>||<math> (p \binter q) \ranres s \;\;\defi\;\; (p \ranres s) \binter (q \ranres s) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RANRES_SETMINUS_R </font>||<math> (r \setminus s) \ranres t \;\;\defi\;\; (r \ranres t) \setminus (s \ranres t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RANRES_SETMINUS_L </font>||<math> (p \setminus q) \ranres s \;\;\defi\;\; (p \ranres s) \setminus (q \ranres s) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RANSUB_BUNION_R </font>||<math> (r \bunion s) \ransub t \;\;\defi\;\; (r \ransub t) \bunion (s \ransub t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RANSUB_BUNION_L </font>||<math> (p \bunion q) \ransub s \;\;\defi\;\; (p \ransub s) \bunion (q \ransub s) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RANSUB_BINTER_R </font>||<math> (r \binter s) \ransub t \;\;\defi\;\; (r \ransub t) \binter (s \ransub t) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RANSUB_BINTER_L </font>||<math> (p \binter q) \ransub s \;\;\defi\;\; (p \ransub s) \binter (q \ransub s) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_CONVERSE_BUNION </font>||<math> (p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1} </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_CONVERSE_BINTER </font>||<math> (p \binter q)^{-1} \;\;\defi\;\; p^{-1} \binter q^{-1} </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_CONVERSE_SETMINUS </font>||<math> (r \setminus s)^{-1} \;\;\defi\;\; r^{-1} \setminus s^{-1} </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_CONVERSE_BCOMP </font>||<math> (r \bcomp s)^{-1} \;\;\defi\;\; (s^{-1} \bcomp r^{-1} ) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_CONVERSE_FCOMP </font>||<math> (p \fcomp q)^{-1} \;\;\defi\;\; (q^{-1} \fcomp p^{-1} ) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_CONVERSE_PPROD </font>||<math> (r \pprod s)^{-1} \;\;\defi\;\; r^{-1} \pprod s^{-1} </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_CONVERSE_DOMRES </font>||<math> (s \domres r)^{-1} \;\;\defi\;\; r^{-1} \ranres s </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_CONVERSE_DOMSUB </font>||<math> (s \domsub r)^{-1} \;\;\defi\;\; r^{-1} \ransub s </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_CONVERSE_RANRES </font>||<math> (r \ranres s)^{-1} \;\;\defi\;\; s \domres r^{-1} </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_CONVERSE_RANSUB </font>||<math> (r \ransub s)^{-1} \;\;\defi\;\; s \domsub r^{-1} </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_DOM_BUNION </font>||<math> \dom (r \bunion s) \;\;\defi\;\; \dom (r) \bunion \dom (s) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RAN_BUNION </font>||<math> \ran (r \bunion s) \;\;\defi\;\; \ran (r) \bunion \ran (s) </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RELIMAGE_BUNION_R </font>||<math> r[S \bunion T] \;\;\defi\;\; r[S] \bunion r[T] </math>|| || M | ||
+ | {{RRRow}}|<font size="-2"> DISTRI_RELIMAGE_BUNION_L </font>||<math> (p \bunion q)[S] \;\;\defi\;\; p[S] \bunion q[S] </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_CONVERSE_BUNION </font>||<math> (p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1} </math>|| || M | ||
|} | |} | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | [[User | + | [[Category:User documentation|The Proving Perspective]] |
− | + | [[Category:Rodin Platform|The Proving Perspective]] | |
− | + | [[Category:User manual|The Proving Perspective]] | |
− | |||
− | |||
− | |||
− | |||
− | |||
− | [[ | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− |
Revision as of 10:08, 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_CONVERSE_BUNION | 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 | |||
DISTRI_CONVERSE_BUNION | M |