Relation Rewrite Rules: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Frederic
No edit summary
Guillaume (talk | contribs)
Rules DEF_EQUAL_FUN_IMAGE and SIMP_SPECIAL_IN_*ID have been implemented in Rodin 3.9
 
(96 intermediate revisions by 11 users not shown)
Line 1: Line 1:
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
Rules without a <tt>*</tt> are planned to be implemented in future versions.
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
{{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}}|*||{{Rulename|SIMP_DOM_SETENUM}}||<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}}|*||{{Rulename|SIMP_DOM_CONVERSE}}||<math>  \dom (r^{-1} ) \;\;\defi\;\;  \ran (r) </math>||  ||  A
{{RRRow}}|*||
  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}}|*||{{Rulename|DEF_IN_TFCT}}||<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}}|*||{{Rulename|DEF_IN_INJ}}||<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}}|*||{{Rulename|DEF_IN_TINJ}}||<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}}|*||{{Rulename|DEF_IN_SURJ}}||<math>  f \in  S \psur 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}}|*||{{Rulename|DEF_IN_TSURJ}}||<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}}|*||{{Rulename|DEF_IN_BIJ}}||<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}}| ||{{Rulename|DISTRI_BCOMP_BUNION}}||<math> r \bcomp (s \bunion  t) \;\;\defi\;\;  (r \bcomp s) \bunion  (r \bcomp  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}}|*||{{Rulename|DISTRI_FCOMP_BUNION_R}}||<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}}|*||{{Rulename|DISTRI_FCOMP_BUNION_L}}||<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}}|||{{Rulename|DISTRI_DPROD_BUNION}}||<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}}|||{{Rulename|DISTRI_DPROD_BINTER}}||<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}}|||{{Rulename|DISTRI_DPROD_SETMINUS}}||<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}}|||{{Rulename|DISTRI_DPROD_OVERL}}||<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}}|||{{Rulename|DISTRI_PPROD_BUNION}}||<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}}|||{{Rulename|DISTRI_PPROD_BINTER}}||<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}}|||{{Rulename|DISTRI_PPROD_SETMINUS}}||<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}}|||{{Rulename|DISTRI_PPROD_OVERL}}||<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}}|||{{Rulename|DISTRI_OVERL_BUNION_L}}||<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}}|||{{Rulename|DISTRI_OVERL_BINTER_L}}||<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}}|*||{{Rulename|DISTRI_DOMRES_BUNION_R}}||<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}}|*||{{Rulename|DISTRI_DOMRES_BUNION_L}}||<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}}|*||{{Rulename|DISTRI_DOMRES_BINTER_R}}||<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}}|*||{{Rulename|DISTRI_DOMRES_BINTER_L}}||<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}}|||{{Rulename|DISTRI_DOMRES_SETMINUS_R}}||<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}}|||{{Rulename|DISTRI_DOMRES_SETMINUS_L}}||<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}}|||{{Rulename|DISTRI_DOMRES_DPROD}}||<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}}|||{{Rulename|DISTRI_DOMRES_OVERL}}||<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}}|*||{{Rulename|DISTRI_DOMSUB_BUNION_R}}||<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}}|*||{{Rulename|DISTRI_DOMSUB_BUNION_L}}||<math>  (s \bunion t) \domsub r \;\;\defi\;\;  (s \domsub  r) \binter (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}}|*||{{Rulename|DISTRI_DOMSUB_BINTER_R}}||<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}}|*||{{Rulename|DISTRI_DOMSUB_BINTER_L}}||<math(s \binter t) \domsub r \;\;\defi\;\;  (s \domsub  r) \bunion (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}}|||{{Rulename|DISTRI_DOMSUB_DPROD}}||<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}}|||{{Rulename|DISTRI_DOMSUB_OVERL}}||<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}}|*||{{Rulename|DISTRI_RANRES_BUNION_R}}||<math>  r \ranres (s \bunion t) \;\;\defi\;\;  (r \ranres s) \bunion (r \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}}|*||{{Rulename|DISTRI_RANRES_BUNION_L}}||<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}}|*||{{Rulename|DISTRI_RANRES_BINTER_R}}||<math>  r \ranres (s \binter t) \;\;\defi\;\;  (r \ranres  s) \binter (r \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}}|*||{{Rulename|DISTRI_RANRES_BINTER_L}}||<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}}|||{{Rulename|DISTRI_RANRES_SETMINUS_R}}||<math>  r \ranres  (s \setminus t) \;\;\defi\;\;  (r \ranres  s) \setminus (r \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}}|||{{Rulename|DISTRI_RANRES_SETMINUS_L}}||<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}}|*||{{Rulename|DISTRI_RANSUB_BUNION_R}}||<math>  r \ransub (s\bunion t) \;\;\defi\;\;  (r \ransub s) \binter  (r \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}}|*||{{Rulename|DISTRI_RANSUB_BUNION_L}}||<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}}|*||{{Rulename|DISTRI_RANSUB_BINTER_R}}||<math>  r \ransub (s \binter t) \;\;\defi\;\;  (r \ransub  s) \bunion  (r \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}}|*||{{Rulename|DISTRI_RANSUB_BINTER_L}}||<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}}|*||{{Rulename|DISTRI_CONVERSE_BUNION}}||<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}}|||{{Rulename|DISTRI_CONVERSE_BINTER}}||<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}}|||{{Rulename|DISTRI_CONVERSE_SETMINUS}}||<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}}|||{{Rulename|DISTRI_CONVERSE_BCOMP}}||<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}}|||{{Rulename|DISTRI_CONVERSE_FCOMP}}||<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}}|||{{Rulename|DISTRI_CONVERSE_PPROD}}||<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}}|||{{Rulename|DISTRI_CONVERSE_DOMRES}}||<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}}|||{{Rulename|DISTRI_CONVERSE_DOMSUB}}||<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}}|||{{Rulename|DISTRI_CONVERSE_RANRES}}||<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}}|||{{Rulename|DISTRI_CONVERSE_RANSUB}}||<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}}|*||{{Rulename|DISTRI_DOM_BUNION}}||<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}}|*||{{Rulename|DISTRI_RAN_BUNION}}||<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}}|*||{{Rulename|DISTRI_RELIMAGE_BUNION_R}}||<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}}|*||{{Rulename|DISTRI_RELIMAGE_BUNION_L}}||<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}}|*||{{Rulename|DERIV_DOM_TOTALREL}}||<math>  \dom (r) \;\;\defi\;\;  E </math> || with hypothesis <math>r \in E \ \mathit{op}\  F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> || M
{{RRRow}}|<font size="-2"> DISTRI_DOM_BUNION </font>||<math> \dom (p \bunion  q) \;\;\defi\;\; \dom (p) \bunion  \dom (q) </math>||| M
{{RRRow}}| ||{{Rulename|DERIV_RAN_SURJREL}}||<math>  \ran (r) \;\;\defi\;\;  F </math> || with hypothesis <math>r \in E \ \mathit{op}\  F</math>, where <math>\mathit{op}</math> is one of <math>\srel,\strel, \psur, \tsur, \tbij</math> || M
{{RRRow}}|<font size="-2"> DISTRI_RAN_BUNION </font>||<math>  \ran (p \bunion  q) \;\;\defi\;\;  \ran (p) \bunion  \ran (q) </math>|| ||  M
{{RRRow}}|*||{{Rulename|DERIV_PRJ1_SURJ}}||<math>\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> || where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> ||  A
{{RRRow}}|<font size="-2"> DISTRI_CONVERSE_BUNION </font>||<math> (p \bunion  q)^{-1} \;\;\defi\;\; p^{-1} \bunion  q^{-1} </math>|| ||  M
{{RRRow}}|*||{{Rulename|DERIV_PRJ2_SURJ}}||<math>\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue </math> || where <math>\mathit{Ty}_1</math> and <math>\mathit{Ty}_2</math> are types and <math>\mathit{op}</math> is one of <math>\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur </math> ||  A
{{RRRow}}|*||{{Rulename|DERIV_ID_BIJ}}||<math>\id \in\mathit{Ty}\ \mathit{op}\ \mathit{Ty}\;\;\defi\;\; \btrue </math> || where <math>\mathit{Ty}</math> is a type and <math>\mathit{op}</math> is any arrow ||  A
{{RRRow}}|*||{{Rulename|SIMP_MAPSTO_PRJ1_PRJ2}}||<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> ||  ||  A
{{RRRow}}| ||{{Rulename|DERIV_EXPAND_PRJS}}||<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> || ||  M
{{RRRow}}|*||{{Rulename|SIMP_DOM_SUCC}}||<math>\dom(\usucc) \;\;\defi\;\; \intg</math> || ||  A
{{RRRow}}|*||{{Rulename|SIMP_RAN_SUCC}}||<math>\ran(\usucc) \;\;\defi\;\; \intg</math> || ||  A
{{RRRow}}|*||{{Rulename|DERIV_MULTI_IN_BUNION}}||<math> E\in A\bunion\cdots\bunion\left\{\cdots, E,\cdots\right\}\bunion\cdots\bunion B\;\;\defi\;\; \btrue</math> || ||  A
{{RRRow}}|*||{{Rulename|DERIV_MULTI_IN_SETMINUS}}||<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> || ||  A
{{RRRow}}|*||{{Rulename|DEF_PRED}}||<math> \upred\;\;\defi\;\; \usucc^{-1}</math> || ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN_ID}}||<math> E \mapsto E \in \id \;\;\defi\;\; \btrue</math> || ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN_SETMINUS_ID}}||<math>E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse</math> || ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN_DOMRES_ID}}||<math>E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S</math> || ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID}}||<math>E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r</math> || ||  A
 
|}
|}



Latest revision as of 15:13, 3 June 2024

Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_Rules.


  Name Rule Side Condition A/M
*
SIMP_DOM_SETENUM
  \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_SETENUM
  \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
r_1 \ovl  \cdots  \ovl r_n \defi r_1 \ovl \cdots \ovl r_{i-1} \ovl r_{i+1} \ovl \cdots \ovl r_n there is a j such that 1\leq i < j \leq n and r_i and r_j are syntactically equal. A
*
SIMP_TYPE_OVERL_CPROD
 r\ovl\cdots\ovl\mathit{Ty}\ovl\cdots\ovl s \;\defi\;\; \mathit{Ty}\ovl\cdots\ovl 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_DOMRES_ID
  S \domres  (T \domres \id) \;\;\defi\;\;  (S \binter  T) \domres \id A
*
SIMP_DOMRES_DOMSUB_ID
  S \domres  (T \domsub \id) \;\;\defi\;\;  (S \setminus  T) \domres \id 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  \ranres  S \;\;\defi\;\;  S  \domres \id A
*
SIMP_RANSUB_ID
  \id  \ransub  S \;\;\defi\;\;  S  \domsub \id A
*
SIMP_RANRES_DOMRES_ID
  (S \domres \id) \ranres  T \;\;\defi\;\;  (S \binter  T) \domres \id A
*
SIMP_RANRES_DOMSUB_ID
  (S \domsub \id) \ranres  T \;\;\defi\;\;  (T \setminus  S) \domres \id 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_MULTI_DOMSUB_RAN
  \ran (r) \domsub  r^{-1} \;\;\defi\;\;  \emptyset A
*
SIMP_DOMSUB_DOMRES_ID
  S \domsub (T \domres \id ) \;\;\defi\;\;  (T \setminus S) \domres \id A
*
SIMP_DOMSUB_DOMSUB_ID
  S \domsub (T \domsub \id ) \;\;\defi\;\;  (S \bunion T) \domsub \id 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_DOM
  r^{-1} \ransub  \dom (r) \;\;\defi\;\;  \emptyset A
*
SIMP_MULTI_RANSUB_RAN
  r \ransub  \ran (r) \;\;\defi\;\;  \emptyset A
*
SIMP_RANSUB_DOMRES_ID
  (S \domres \id) \ransub  T \;\;\defi\;\;  (S \setminus T) \domres \id A
*
SIMP_RANSUB_DOMSUB_ID
  (S \domsub \id) \ransub  T \;\;\defi\;\;  (S \bunion T) \domsub \id 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 \fcomp \ldots  \fcomp s \;\;\defi\;\;  r \fcomp \ldots  \fcomp s 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 S \domres \id \fcomp T \domres \id \fcomp \ldots  s \;\;\defi\;\;  r \fcomp \ldots  \fcomp (S \binter  T) \domres \id \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 \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  r \bcomp  \ldots  \bcomp  s 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 S \domres \id \bcomp T \domres \id \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  r \bcomp  \ldots  \bcomp (S \binter  T) \domres \id \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_DPROD_CPROD
  (\mathit{S} \cprod \mathit{T})  \dprod  (\mathit{U} \cprod \mathit{V})  \;\;\defi\;\;  \mathit{S}  \binter  \mathit{U}  \cprod  (\mathit{T}  \cprod  \mathit{V}) A
*
SIMP_SPECIAL_PPROD_R
  r \pprod  \emptyset  \;\;\defi\;\;  \emptyset A
*
SIMP_SPECIAL_PPROD_L
  \emptyset  \pprod  r \;\;\defi\;\;  \emptyset A
*
SIMP_PPROD_CPROD
  (\mathit{S} \cprod \mathit{T})  \pprod  (\mathit{U} \cprod \mathit{V}) \;\;\defi\;\;  (\mathit{S} \cprod \mathit{U}) \cprod (\mathit{T} \cprod \mathit{V}) 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_RELIMAGE_ID
  \id[T] \;\;\defi\;\;  T A
*
SIMP_RELIMAGE_DOMRES_ID
  (S \domres \id)[T] \;\;\defi\;\;  S \binter  T A
*
SIMP_RELIMAGE_DOMSUB_ID
  (S \domsub \id)[T] \;\;\defi\;\;  T \setminus S 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^{-1}  \;\;\defi\;\;  \id A
*
SIMP_CONVERSE_CPROD
  (\mathit{S} \cprod \mathit{T})^{-1}  \;\;\defi\;\;  \mathit{T} \cprod \mathit{S} 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 \qdot  P \mid  x\mapsto y\} ^{-1}  \;\;\defi\;\;  \{ X \qdot  P \mid  y\mapsto x\} A
*
SIMP_DOM_ID
  \dom (\id) \;\;\defi\;\;  S where \id has type \pow(S \cprod S) A
*
SIMP_RAN_ID
  \ran (\id) \;\;\defi\;\;  S where \id has type \pow(S \cprod S) A
*
SIMP_FCOMP_ID_L
  (S \domres \id) \fcomp r \;\;\defi\;\;  S \domres  r A
*
SIMP_FCOMP_ID_R
  r \fcomp (S \domres \id) \;\;\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_FUNIMAGE_PRJ1
  \prjone (E \mapsto  F) \;\;\defi\;\;  E A
*
SIMP_FUNIMAGE_PRJ2
  \prjtwo (E \mapsto  F) \;\;\defi\;\;  F A
*
SIMP_DOM_PRJ1
  \dom (\prjone) \;\;\defi\;\;  S \cprod T where \prjone has type \pow(S \cprod T \cprod S) A
*
SIMP_DOM_PRJ2
  \dom (\prjtwo) \;\;\defi\;\; S \cprod T where \prjtwo has type \pow(S \cprod T \cprod T) A
*
SIMP_RAN_PRJ1
  \ran (\prjone) \;\;\defi\;\;  S where \prjone has type \pow(S \cprod T \cprod S) A
*
SIMP_RAN_PRJ2
  \ran (\prjtwo) \;\;\defi\;\;  T where \prjtwo has type \pow(S \cprod T \cprod T) A
*
SIMP_FUNIMAGE_LAMBDA
  (\lambda x \qdot  P(x) \mid  E(x))(y) \;\;\defi\;\;  E(y) A
*
SIMP_DOM_LAMBDA
\dom(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid E\} A
*
SIMP_RAN_LAMBDA
\ran(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid F\} A
*
SIMP_IN_FUNIMAGE
E\mapsto F(E)\in F \;\;\defi\;\; \btrue A
*
SIMP_IN_FUNIMAGE_CONVERSE_L
F^{-1}(E)\mapsto E\in F \;\;\defi\;\; \btrue A
*
SIMP_IN_FUNIMAGE_CONVERSE_R
F(E)\mapsto E\in F^{-1} \;\;\defi\;\; \btrue A
*
SIMP_MULTI_FUNIMAGE_SETENUM_LL
  \{ A \mapsto  E, \ldots  , B \mapsto  E\} (x) \;\;\defi\;\;  E A
*
SIMP_MULTI_FUNIMAGE_SETENUM_LR
  \{ E, \ldots  , x \mapsto  y, \ldots  , F\} (x) \;\;\defi\;\;  y A
*
SIMP_MULTI_FUNIMAGE_OVERL_SETENUM
  (r \ovl  \ldots  \ovl  \{ E, \ldots  , x \mapsto  y, \ldots  , F\} )(x) \;\;\defi\;\;  y A
*
SIMP_MULTI_FUNIMAGE_BUNION_SETENUM
  (r \bunion  \ldots  \bunion  \{ E, \ldots  , x \mapsto  y, \ldots  , F\} )(x) \;\;\defi\;\;  y A
*
SIMP_FUNIMAGE_CPROD
  (S \cprod  \{ F\} )(x) \;\;\defi\;\;  F A
*
SIMP_FUNIMAGE_ID
  \id (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
*
SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM
  \{x \mapsto a, \ldots, y \mapsto b\}(\{a \mapsto x, \ldots, b \mapsto y\}(E)) \;\;\defi\;\;  E A
*
SIMP_FUNIMAGE_DOMRES
(E \domres F)(G)\;\;\defi\;\;F(G) with hypothesis F \in \mathit{A} \ \mathit{op}\  \mathit{B} where \mathit{op} is one of \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij. AM
*
SIMP_FUNIMAGE_DOMSUB
(E \domsub F)(G)\;\;\defi\;\;F(G) with hypothesis F \in \mathit{A} \ \mathit{op}\  \mathit{B} where \mathit{op} is one of \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij. AM
*
SIMP_FUNIMAGE_RANRES
(F\ranres E)(G)\;\;\defi\;\;F(G) with hypothesis F \in \mathit{A} \ \mathit{op}\  \mathit{B} where \mathit{op} is one of \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij. AM
*
SIMP_FUNIMAGE_RANSUB
(F \ransub E)(G)\;\;\defi\;\;F(G) with hypothesis F \in \mathit{A} \ \mathit{op}\  \mathit{B} where \mathit{op} is one of \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij. AM
*
SIMP_FUNIMAGE_SETMINUS
(F \setminus E)(G)\;\;\defi\;\;F(G) with hypothesis F \in \mathit{A} \ \mathit{op}\  \mathit{B} where \mathit{op} is one of \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij. AM
*
DEF_EQUAL_FUNIMAGE
 f(x) = y \;\;\defi\;\; x \mapsto y \in f M
*
DEF_BCOMP
  r \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  s \fcomp \ldots  \fcomp r M
DERIV_ID_SING
  \{ E\} \domres \id \;\;\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
DERIV_FCOMP_SING
  \{E\mapsto F\}\fcomp\{F\mapsto G\} \;\;\defi\;\;  \{E\mapsto G\} A
*
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} \cprod \mathit{Tb} A
*
SIMP_TYPE_RAN
  \ran (\mathit{Ty}) \;\;\defi\;\;  \mathit{Tb} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \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
*
SIMP_MULTI_DOM_DOMRES
\dom(A\domres f) \;\;\defi\;\; \dom(f)\binter A A
*
SIMP_MULTI_DOM_DOMSUB
\dom(A\domsub f) \;\;\defi\;\; \dom(f)\setminus A A
*
SIMP_MULTI_RAN_RANRES
\ran(f\ranres A) \;\;\defi\;\; \ran(f)\binter A A
*
SIMP_MULTI_RAN_RANSUB
\ran(f\ransub A) \;\;\defi\;\; \ran(f)\setminus A 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 \;\;\defi\;\;  E = F 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_REL
  r \in  S \rel  T \;\;\defi\;\;  r\subseteq S\cprod T 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 \srel  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 \psur  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  t) 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) \binter  (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) \bunion  (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 \ransub (s\bunion t) \;\;\defi\;\;  (r \ransub  s) \binter  (r \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 \ransub (s \binter t) \;\;\defi\;\;  (r \ransub  s) \bunion  (r \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
*
DERIV_DOM_TOTALREL
  \dom (r) \;\;\defi\;\;  E with hypothesis r \in E \ \mathit{op}\  F, where \mathit{op} is one of \trel, \strel, \tfun, \tinj, \tsur, \tbij M
DERIV_RAN_SURJREL
  \ran (r) \;\;\defi\;\;  F with hypothesis r \in E \ \mathit{op}\  F, where \mathit{op} is one of \srel,\strel, \psur, \tsur, \tbij M
*
DERIV_PRJ1_SURJ
\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue where \mathit{Ty}_1 and \mathit{Ty}_2 are types and \mathit{op} is one of \rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur A
*
DERIV_PRJ2_SURJ
\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue where \mathit{Ty}_1 and \mathit{Ty}_2 are types and \mathit{op} is one of \rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur A
*
DERIV_ID_BIJ
\id \in\mathit{Ty}\ \mathit{op}\ \mathit{Ty}\;\;\defi\;\; \btrue where \mathit{Ty} is a type and \mathit{op} is any arrow A
*
SIMP_MAPSTO_PRJ1_PRJ2
\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E A
DERIV_EXPAND_PRJS
 E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) M
*
SIMP_DOM_SUCC
\dom(\usucc) \;\;\defi\;\; \intg A
*
SIMP_RAN_SUCC
\ran(\usucc) \;\;\defi\;\; \intg A
*
DERIV_MULTI_IN_BUNION
 E\in A\bunion\cdots\bunion\left\{\cdots, E,\cdots\right\}\bunion\cdots\bunion B\;\;\defi\;\; \btrue A
*
DERIV_MULTI_IN_SETMINUS
 E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse A
*
DEF_PRED
 \upred\;\;\defi\;\; \usucc^{-1} A
*
SIMP_SPECIAL_IN_ID
 E \mapsto E \in \id \;\;\defi\;\; \btrue A
*
SIMP_SPECIAL_IN_SETMINUS_ID
E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse A
*
SIMP_SPECIAL_IN_DOMRES_ID
E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S A
*
SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID
E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r A