Difference between revisions of "Relation Rewrite Rules"

From Event-B
Jump to navigationJump to search
imported>Nicolas
m (Corrected SIMP_FUNIMAGE_CONVERSE_FUNIMAGE)
imported>Nicolas
m (Corrected DISTRI_RANRES_BUNION_R; DISTRI_RANRES_BINTER_R; DISTRI_RANRES_SETMINUS_R)
Line 161: Line 161:
 
{{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_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_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_R </font>||<math>  r \ranres (s \bunion t) \;\;\defi\;\;  (r \ranres  s) \bunion  (r \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_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_R </font>||<math>  r \ranres (s \binter t) \;\;\defi\;\;  (r \ranres  s) \binter  (r \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_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_R </font>||<math>  r \ranres  (s \setminus t) \;\;\defi\;\;  (r \ranres  s) \setminus (r \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_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_R </font>||<math>  (r \bunion  s) \ransub  t \;\;\defi\;\;  (r \ransub  t) \bunion  (s \ransub  t) </math>||  ||  M

Revision as of 10:03, 9 June 2009

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