Relation Rewrite Rules: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>Frederic
No edit summary
imported>Laurent
Added star column
Line 1: Line 1:
{{RRHeader}}
{{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_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\;\;
{{RRRow}}|*||<font size="-2"> SIMP_DOM_CONVERSE </font>||<math>  \dom (r^{-1} ) \;\;
  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
  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_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_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_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_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_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
{{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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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 \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_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 \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_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 \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_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
{{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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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 17:03, 11 February 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(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 \bunion s) \ranres t \;\;\defi\;\; (r \ranres t) \bunion (s \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 \binter s) \ranres t \;\;\defi\;\; (r \ranres t) \binter (s \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 \setminus s) \ranres t \;\;\defi\;\; (r \ranres t) \setminus (s \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
Retrieved from ‘https://wiki.event-b.org/index.php?title=Relation_Rewrite_Rules&oldid=6799’