Difference between pages "Relation Rewrite Rules" and "Rodin Developer Support"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
(Added rules SIMP_IN_FUNIMAGE*.)
 
imported>Stefan
 
Line 1: Line 1:
−
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
+
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
−
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}}
+
[[Category:Developer Documentation]]
−
{{RRRow}}|*||{{Rulename|SIMP_DOM_COMPSET}}||<math>  \dom (\{ x \mapsto  a, \ldots , y \mapsto  b\} ) \;\;\defi\;\;  \{ x, \ldots , y\} </math>||  ||  A
+
[[Category:Rodin Platform]]
−
{{RRRow}}|||{{Rulename|SIMP_DOM_CONVERSE}}||<math>  \dom (r^{-1} ) \;\;\defi\;\;  \ran (r) </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_RAN_COMPSET}}||<math>  \ran (\{ x \mapsto  a, \ldots , y \mapsto  b\} ) \;\;\defi\;\;  \{ a, \ldots , b\} </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_RAN_CONVERSE}}||<math>  \ran (r^{-1} ) \;\;\defi\;\;  \dom (r) </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OVERL}}||<math>  r \ovl  \ldots  \ovl  \emptyset  \ovl  \ldots  \ovl  s \;\;\defi\;\;  r \ovl  \ldots  \ovl  s </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_MULTI_OVERL}}||<math>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</math>|| there is a <math>j</math> such that <math>1\leq i < j \leq n</math> and <math>r_i</math> and <math>r_j</math> are syntactically equal. ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_TYPE_OVERL_CPROD}}||<math>  r \ovl\dots\ovl  \mathit{Ty} \;\;\defi\;\;  \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMRES_L}}||<math>  \emptyset  \domres  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMRES_R}}||<math>  S \domres  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_DOMRES}}||<math> \mathit{Ty} \domres  r \;\;\defi\;\;  r </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_DOMRES_DOM}}||<math>  \dom (r) \domres  r \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_DOMRES_RAN}}||<math>  \ran (r) \domres  r^{-1}  \;\;\defi\;\;  r^{-1} </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_DOMRES_ID}}||<math>  S \domres  (T \domres \id) \;\;\defi\;\;  (S \binter  T) \domres \id </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANRES_R}}||<math>  r \ranres  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANRES_L}}||<math>  \emptyset  \ranres  S \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_RANRES}}||<math>  r \ranres  \mathit{Ty} \;\;\defi\;\;  r </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_RANRES_RAN}}||<math>  r \ranres  \ran (r) \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_RANRES_DOM}}||<math>  r^{-1}  \ranres  \dom (r) \;\;\defi\;\;  r^{-1} </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_RANRES_ID}}||<math>  (S \domres \id) \ranres  T \;\;\defi\;\;  (S \binter  T) \domres \id </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMSUB_L}}||<math>  \emptyset  \domsub  r \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMSUB_R}}||<math>  S \domsub  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_DOMSUB}}||<math> \mathit{Ty} \domsub  r \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_DOMSUB_DOM}}||<math>  \dom (r) \domsub  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_DOMSUB_ID}}||<math>  S \domsub (T \domres \id ) \;\;\defi\;\;  (T \setminus S) \domres \id </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANSUB_R}}||<math>  r \ransub  \emptyset  \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANSUB_L}}||<math>  \emptyset  \ransub  S \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_RANSUB}}||<math>  r \ransub  \mathit{Ty} \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_RANSUB_RAN}}||<math>  r \ransub  \ran (r) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_RANSUB_ID}}||<math>  (S \domres \id) \ransub  T \;\;\defi\;\;  (S \setminus T) \domres \id </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_FCOMP}}||<math>  r \fcomp \ldots  \fcomp \emptyset  \fcomp \ldots  \fcomp s \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_FCOMP_ID}}||<math>  r \fcomp \ldots  \fcomp \id \fcomp \ldots  \fcomp s \;\;\defi\;\;  r \fcomp \ldots  \fcomp s </math>|| ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_FCOMP_R}}||<math>  r \fcomp \mathit{Ty} \;\;\defi\;\;  \dom (r) \cprod  \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_FCOMP_L}}||<math> \mathit{Ty} \fcomp r \;\;\defi\;\;  \mathit{Ta} \cprod  \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_FCOMP_ID}}||<math>  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 </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_BCOMP}}||<math>  r \bcomp  \ldots  \bcomp  \emptyset  \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_BCOMP_ID}}||<math>  r \bcomp  \ldots  \bcomp  \id \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  r \bcomp  \ldots  \bcomp  s </math>|| ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_BCOMP_L}}||<math> \mathit{Ty} \bcomp  r \;\;\defi\;\;  \dom (r) \cprod  \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_BCOMP_R}}||<math>  r \bcomp  \mathit{Ty} \;\;\defi\;\;  \mathit{Ta} \cprod  \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_BCOMP_ID}}||<math>  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 </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DPROD_R}}||<math>  r \dprod  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DPROD_L}}||<math>  \emptyset  \dprod  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_DPROD_CPROD}}||<math>  (\mathit{S} \cprod \mathit{T})  \dprod  (\mathit{U} \cprod \mathit{V})  \;\;\defi\;\;  \mathit{S}  \binter  \mathit{U}  \cprod  (\mathit{T}  \cprod  \mathit{V}) </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_PPROD_R}}||<math>  r \pprod  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_PPROD_L}}||<math>  \emptyset  \pprod  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_PPROD_CPROD}}||<math>  (\mathit{S} \cprod \mathit{T})  \pprod  (\mathit{U} \cprod \mathit{V}) \;\;\defi\;\;  (\mathit{S} \cprod \mathit{U}) \cprod (\mathit{T} \cprod \mathit{V}) </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RELIMAGE_R}}||<math>  r[\emptyset ] \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RELIMAGE_L}}||<math>  \emptyset [S] \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_RELIMAGE}}||<math>  r[Ty] \;\;\defi\;\;  \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_RELIMAGE_DOM}}||<math>  r[\dom (r)] \;\;\defi\;\;  \ran (r) </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_RELIMAGE_ID}}||<math>  \id[T] \;\;\defi\;\;  T </math>|| ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_RELIMAGE_ID}}||<math>  (S \domres \id)[T] \;\;\defi\;\;  S \binter  T </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_RELIMAGE_CPROD_SING}}||<math>  (\{ E\}  \cprod  S)[\{ E\} ] \;\;\defi\;\;  S </math>|| where <math>E</math> is a single expression ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_RELIMAGE_SING_MAPSTO}}||<math>  \{ E \mapsto  F\} [\{ E\} ] \;\;\defi\;\;  \{ F\} </math>|| where <math>E</math> is a single expression ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB}}||<math>  (r \ransub  S)^{-1} [S] \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_RELIMAGE_CONVERSE_RANRES}}||<math>  (r \ranres  S)^{-1} [S] \;\;\defi\;\;  r^{-1} [S] </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_RELIMAGE_CONVERSE_DOMSUB}}||<math>  (S \domsub  r)^{-1} [T] \;\;\defi\;\;  r^{-1} [T] \setminus S </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|DERIV_RELIMAGE_RANSUB}}||<math>  (r \ransub  S)[T] \;\;\defi\;\;  r[T] \setminus S </math>||  ||  M
 
−
{{RRRow}}|||{{Rulename|DERIV_RELIMAGE_RANRES}}||<math>  (r \ranres  S)[T] \;\;\defi\;\;  r[T] \binter  S </math>||  ||  M
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_RELIMAGE_DOMSUB}}||<math>  (S \domsub  r)[S] \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|DERIV_RELIMAGE_DOMSUB}}||<math>  (S \domsub  r)[T] \;\;\defi\;\;  r[T \setminus S] </math>||  ||  M
 
−
{{RRRow}}|||{{Rulename|DERIV_RELIMAGE_DOMRES}}||<math>  (S \domres  r)[T] \;\;\defi\;\;  r[S \binter  T] </math>||  ||  M
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_CONVERSE}}||<math>  \emptyset ^{-1}  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_CONVERSE_ID}}||<math>  \id^{-1}  \;\;\defi\;\;  \id </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_CONVERSE_CPROD}}||<math>  (\mathit{S} \cprod \mathit{T})^{-1}  \;\;\defi\;\;  \mathit{T} \cprod \mathit{S} </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_CONVERSE_SETENUM}}||<math>  \{ x \mapsto  a, \ldots , y \mapsto  b\} ^{-1}  \;\;\defi\;\;  \{ a \mapsto  x, \ldots , b \mapsto  y\} </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_CONVERSE_COMPSET}}||<math>  \{ X \qdot  P \mid  x\mapsto y\} ^{-1}  \;\;\defi\;\;  \{ X \qdot  P \mid  y\mapsto x\} </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_DOM_ID}}||<math>  \dom (\id) \;\;\defi\;\;  S </math>|| where <math>\id</math> has type <math>\pow(S \cprod S)</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_RAN_ID}}||<math>  \ran (\id) \;\;\defi\;\;  S </math>|| where <math>\id</math> has type <math>\pow(S \cprod S)</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_FCOMP_ID_L}}||<math>  (S \domres \id) \fcomp r \;\;\defi\;\;  S \domres  r </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_FCOMP_ID_R}}||<math>  r \fcomp (S \domres \id) \;\;\defi\;\;  r \ranres  S </math>||  ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_REL_R}}||<math>  S \rel  \emptyset  \;\;\defi\;\;  \{ \emptyset \} </math>|| idem for operators <math>\srel  \pfun  \pinj  \psur</math> ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_REL_L}}||<math>  \emptyset  \rel  S \;\;\defi\;\;  \{ \emptyset \} </math>|| idem for operators <math>\trel  \pfun  \tfun  \pinj  \tinj</math> ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_EQUAL_REL}}||<math>  A \rel  B = \emptyset  \;\;\defi\;\;  \bfalse </math>|| idem for operators <math>\pfun  \pinj</math> ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_EQUAL_RELDOM}}||<math>  A \trel  B = \emptyset  \;\;\defi\;\;  \lnot\, A = \emptyset  \land  B = \emptyset </math>|| idem for operators <math>\tfun  \tinj  \tsur  \tbij</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_FUNIMAGE_PRJ1}}||<math>  \prjone (E \mapsto  F) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_FUNIMAGE_PRJ2}}||<math>  \prjtwo (E \mapsto  F) \;\;\defi\;\;  F </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_DOM_PRJ1}}||<math>  \dom (\prjone) \;\;\defi\;\;  S \cprod T </math>|| where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_DOM_PRJ2}}||<math>  \dom (\prjtwo) \;\;\defi\;\; S \cprod T </math>|| where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_RAN_PRJ1}}||<math>  \ran (\prjone) \;\;\defi\;\;  S </math>|| where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_RAN_PRJ2}}||<math>  \ran (\prjtwo) \;\;\defi\;\;  T </math>|| where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> ||  A
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_LAMBDA}}||<math>  (\lambda x \qdot  \bfalse  \mid  E) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_LAMBDA}}||<math>  (\lambda x \qdot  P(x) \mid  E(x))(y) \;\;\defi\;\;  E(y) </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_DOM_LAMBDA}}||<math>  \dom (\lambda x \qdot  P \mid  E) \;\;\defi\;\;  \{ x\qdot  P \mid  x\} </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_RAN_LAMBDA}}||<math>  \ran (\lambda x \qdot  P \mid  E) \;\;\defi\;\;  \{ x\qdot  P \mid  E\} </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_IN_FUNIMAGE}}||<math>E\mapsto F(E)\in F \;\;\defi\;\; \btrue</math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_IN_FUNIMAGE_CONVERSE_L}}||<math>F^{-1}(E)\mapsto E\in F \;\;\defi\;\; \btrue</math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_IN_FUNIMAGE_CONVERSE_R}}||<math>F(E)\mapsto E\in F^{-1} \;\;\defi\;\; \btrue</math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_FUNIMAGE_SETENUM_LL}}||<math>  \{ A \mapsto  E, \ldots  , B \mapsto  E\} (x) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_FUNIMAGE_SETENUM_LR}}||<math>  \{ A \mapsto  E, \ldots  , x \mapsto  y, \ldots  , B \mapsto  F\} (x) \;\;\defi\;\;  y </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_OVERL_SETENUM}}||<math>  (r \ovl  \ldots  \ovl  \{ A \mapsto  E, \ldots  , x \mapsto  y, \ldots  , B \mapsto  F\} )(x) \;\;\defi\;\;  y </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_FUNIMAGE_BUNION_SETENUM}}||<math>  (r \bunion  \ldots  \bunion  \{ A \mapsto  E, \ldots  , x \mapsto  y, \ldots  , B \mapsto  F\} )(x) \;\;\defi\;\;  y </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_CPROD}}||<math>  (S \cprod  \{ F\} )(x) \;\;\defi\;\;  F </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_FUNIMAGE_ID}}||<math>  \id (x) \;\;\defi\;\;  x </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_FUNIMAGE_CONVERSE}}||<math>  f(f^{-1} (E)) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_CONVERSE_FUNIMAGE}}||<math>  f^{-1}(f(E)) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM}}||<math>  \{x \mapsto a, \ldots, y \mapsto b\}(\{a \mapsto x, \ldots, b \mapsto y\}(E)) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_DOMRES}}||<math>(E \domres F)(G)\;\;\defi\;\;F(G)</math> ||  with hypothesis<math> F \in \mathit{A} \ \mathit{op}\  \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>.  || AM
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_DOMSUB}}||<math>(E \domsub F)(G)\;\;\defi\;\;F(G)</math> ||  with hypothesis<math> F \in \mathit{A} \ \mathit{op}\  \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>.  || AM
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_RANRES}}||<math>(F\ranres E)(G)\;\;\defi\;\;F(G)</math> ||  with hypothesis<math> F \in \mathit{A} \ \mathit{op}\  \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>.  || AM
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_RANSUB}}||<math>(F \ransub E)(G)\;\;\defi\;\;F(G)</math> ||  with hypothesis<math> F \in \mathit{A} \ \mathit{op}\  \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>.  || AM
 
−
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_SETMINUS}}||<math>(F \setminus E)(G)\;\;\defi\;\;F(G)</math> ||  with hypothesis<math> F \in \mathit{A} \ \mathit{op}\  \mathit{B}</math> where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>.  || AM
 
−
{{RRRow}}|||{{Rulename|DEF_BCOMP}}||<math>  r \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  s \fcomp \ldots  \fcomp r </math>||  ||  M
 
−
{{RRRow}}|||{{Rulename|DERIV_ID_SING}}||<math>  \{ E\} \domres \id \;\;\defi\;\;  \{ E \mapsto  E\} </math>|| where <math>E</math> is a single expression ||  M
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DOM}}||<math>  \dom (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RAN}}||<math>  \ran (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|SIMP_CONVERSE_CONVERSE}}||<math>  r^{-1-1}  \;\;\defi\;\;  r </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_FCOMP}}||<math>  (p \fcomp q)[s] \;\;\defi\;\;  q[p[s]] </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_DOMRES}}||<math>  (s \domres  p) \fcomp q \;\;\defi\;\;  s \domres  (p \fcomp q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_DOMSUB}}||<math>  (s \domsub  p) \fcomp q \;\;\defi\;\;  s \domsub  (p \fcomp q) </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_RANRES}}||<math>  p \fcomp (q \ranres  s) \;\;\defi\;\;  (p \fcomp q) \ranres  s </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_RANSUB}}||<math>  p \fcomp (q \ransub  s) \;\;\defi\;\;  (p \fcomp q) \ransub  s </math>||  ||  M
 
−
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_EQUAL_RELDOMRAN}}||<math>  \emptyset  \strel  \emptyset  \;\;\defi\;\;  \{ \emptyset \} </math>|| idem for operators <math>\tsur  \tbij</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_DOM}}||<math>  \dom (\mathit{Ty}) \;\;\defi\;\;  \mathit{Ta} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_TYPE_RAN}}||<math>  \ran (\mathit{Ty}) \;\;\defi\;\;  \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_DOM_CPROD}}||<math>  \dom (E \cprod  E) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_MULTI_RAN_CPROD}}||<math>  \ran (E \cprod  E) \;\;\defi\;\;  E </math>||  ||  A
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_DOM}}||<math>  E \in  \dom (r) \;\;\defi\;\;  \exists y \qdot  E \mapsto  y \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RAN}}||<math>  F \in  \ran (r) \;\;\defi\;\;  \exists x \qdot  x \mapsto  F  \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_CONVERSE}}||<math>  E \mapsto  F \in  r^{-1}  \;\;\defi\;\;  F \mapsto  E \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_DOMRES}}||<math>  E \mapsto  F \in  S \domres  r \;\;\defi\;\;  E \in  S \land  E \mapsto  F \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RANRES}}||<math>  E \mapsto  F \in  r \ranres  T \;\;\defi\;\;  E \mapsto  F \in  r \land  F \in  T </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_DOMSUB}}||<math>  E \mapsto  F \in  S \domsub  r \;\;\defi\;\;  E \notin  S \land  E \mapsto  F \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RANSUB}}||<math>  E \mapsto  F \in  r \ranres  T \;\;\defi\;\;  E \mapsto  F \in  r \land  F \notin  T </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RELIMAGE}}||<math>  F \in  r[w] \;\;\defi\;\;  \exists x \qdot  x \in  w \land  x \mapsto  F \in  r </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_FCOMP}}||<math>  E \mapsto  F \in  (p \fcomp q) \;\;\defi\;\;  \exists x \qdot  E \mapsto  x \in  p \land  x \mapsto  F \in  q </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_OVERL}}||<math>  p \ovl  q \;\;\defi\;\;  (\dom (q) \domsub  p) \bunion  q </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_ID}}||<math>  E \mapsto  F \in  \id \;\;\defi\;\;  E = F </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_DPROD}}||<math>  E \mapsto  (F \mapsto  G) \in  p \dprod  q \;\;\defi\;\;  E \mapsto  F \in  p \land  E \mapsto  G \in  q </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_PPROD}}||<math>  (E \mapsto  G) \mapsto  (F \mapsto  H) \in  p \pprod  q \;\;\defi\;\;  E \mapsto  F \in  p \land  G \mapsto  H \in  q </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_REL}}||<math>  r \in  S \rel  T \;\;\defi\;\;  r\subseteq S\cprod T</math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RELDOM}}||<math>  r \in  S \trel  T \;\;\defi\;\;  r \in  S \rel  T \land  \dom (r) = S </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RELRAN}}||<math>  r \in  S \srel  T \;\;\defi\;\;  r \in  S \rel  T \land  \ran (r) = T </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_RELDOMRAN}}||<math>  r \in  S \strel  T \;\;\defi\;\;  r \in  S \rel  T \land  \dom (r) = S \land  \ran (r) = T </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_FCT}}||<math>\begin{array}{rcl}
 
−
f \in  S \pfun  T & \defi & f \in  S \rel  T  \\  & \land & (\forall x,y,z \qdot  x \mapsto  y \in  f \land  x \mapsto  z \in  f \limp  y = z) \\ \end{array} </math>||  ||  M
 
−
{{RRRow}}|*||{{Rulename|DEF_IN_TFCT}}||<math>  f \in  S \tfun  T \;\;\defi\;\;  f \in  S \pfun  T \land  \dom (f) = 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}}|*||{{Rulename|DEF_IN_TINJ}}||<math>  f \in  S \tinj  T \;\;\defi\;\;  f \in  S \pinj  T \land  \dom (f) = S </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}}|*||{{Rulename|DEF_IN_TSURJ}}||<math>  f \in  S \tsur  T \;\;\defi\;\;  f \in  S \psur  T \land  \dom (f) = S </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}}| ||{{Rulename|DISTRI_BCOMP_BUNION}}||<math>  r \bcomp  (s \bunion  t) \;\;\defi\;\;  (r \bcomp  s) \bunion  (r \bcomp  t) </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}}|*||{{Rulename|DISTRI_FCOMP_BUNION_L}}||<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}}|||{{Rulename|DISTRI_DPROD_BINTER}}||<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}}|||{{Rulename|DISTRI_DPROD_OVERL}}||<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}}|||{{Rulename|DISTRI_PPROD_BINTER}}||<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}}|||{{Rulename|DISTRI_PPROD_OVERL}}||<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}}|||{{Rulename|DISTRI_OVERL_BINTER_L}}||<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}}|*||{{Rulename|DISTRI_DOMRES_BUNION_L}}||<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}}|*||{{Rulename|DISTRI_DOMRES_BINTER_L}}||<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}}|||{{Rulename|DISTRI_DOMRES_SETMINUS_L}}||<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}}|||{{Rulename|DISTRI_DOMRES_OVERL}}||<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}}|*||{{Rulename|DISTRI_DOMSUB_BUNION_L}}||<math>  (s \bunion  t) \domsub  r \;\;\defi\;\;  (s \domsub  r) \binter  (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}}|*||{{Rulename|DISTRI_DOMSUB_BINTER_L}}||<math>  (s \binter  t) \domsub  r \;\;\defi\;\;  (s \domsub  r) \bunion  (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}}|||{{Rulename|DISTRI_DOMSUB_OVERL}}||<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}}|*||{{Rulename|DISTRI_RANRES_BUNION_L}}||<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}}|*||{{Rulename|DISTRI_RANRES_BINTER_L}}||<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}}|||{{Rulename|DISTRI_RANRES_SETMINUS_L}}||<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}}|*||{{Rulename|DISTRI_RANSUB_BUNION_L}}||<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}}|*||{{Rulename|DISTRI_RANSUB_BINTER_L}}||<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}}|||{{Rulename|DISTRI_CONVERSE_BINTER}}||<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}}|||{{Rulename|DISTRI_CONVERSE_BCOMP}}||<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}}|||{{Rulename|DISTRI_CONVERSE_PPROD}}||<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}}|||{{Rulename|DISTRI_CONVERSE_DOMSUB}}||<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}}|||{{Rulename|DISTRI_CONVERSE_RANSUB}}||<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}}|*||{{Rulename|DISTRI_RAN_BUNION}}||<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}}|*||{{Rulename|DISTRI_RELIMAGE_BUNION_L}}||<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}}| ||{{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}}|b||{{Rulename|prjone-functional}}||<math>  \prjone \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue </math> || where <math>\mathit{op}</math> is one of <math> \pfun, \tfun, \trel </math> ||  A
 
−
{{RRRow}}|b||{{Rulename|prjtwo-functional}}||<math>  \prjtwo \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue </math> || where <math>\mathit{op}</math> is one of <math> \pfun, \tfun, \trel </math> ||  A
 
−
{{RRRow}}| ||{{Rulename|prj-expand}}||<math> x \;\;\defi\;\; \prjone(x) \mapsto \prjtwo(x) </math> || ||  M
 
  
−
|}
+
== Rodin Platform Overview ==
  
 +
== Architecture of the Rodin Platform ==
  
 +
=== Rodin Platform Core ===
  
−
[[Category:User documentation|The Proving Perspective]]
+
* [[Database]]
−
[[Category:Rodin Platform|The Proving Perspective]]
+
 
−
[[Category:User manual|The Proving Perspective]]
+
* [[Builder]]
 +
 
 +
=== Event-B User Interface ===
 +
 
 +
The Event-B User Interface of the Roding Platform has two major components that are concerned with either '''editing''' Event-B models or '''proving''' properties of models.
 +
 
 +
* [[Editing]]
 +
 
 +
* [[Proving]]
 +
 
 +
=== Event-B Component Library ===
 +
 
 +
Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of of Event-B constructs is verified by a [[static checker|Static Checker]]. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The [[proof obligation generator|Proof Obligation Generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[proof manager|Proof Manager]] attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the [[proving user interface|Proving]]).
 +
 
 +
* [[Abstract Syntax Tree]]
 +
 
 +
* [[Static Checker]]
 +
 
 +
* [[Proof Obligation Generator]]
 +
 
 +
* [[Proof Manager]]
 +
 
 +
== Extending the Rodin Platform ==
 +
 
 +
=== Getting Started ===
 +
 
 +
=== Plug-in Tutorials ===
 +
 
 +
== Useful Hints ==
 +
 
 +
=== Testing ===
 +
 
 +
=== Debugging ===
 +
 
 +
== Rodin Developer FAQ ==

Revision as of 14:56, 4 July 2008

The Developer Support provides resources for developing plug-ins for the Rodin Platform.

Rodin Platform Overview

Architecture of the Rodin Platform

Rodin Platform Core

Event-B User Interface

The Event-B User Interface of the Roding Platform has two major components that are concerned with either editing Event-B models or proving properties of models.

Event-B Component Library

Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an abstract syntax tree. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of of Event-B constructs is verified by a Static Checker. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The Proof Obligation Generator uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the Proof Manager attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the Proving).

Extending the Rodin Platform

Getting Started

Plug-in Tutorials

Useful Hints

Testing

Debugging

Rodin Developer FAQ

Retrieved from ‘https://wiki.event-b.org/index.php?title=Relation_Rewrite_Rules&oldid=7023’