Difference between pages "Relation Rewrite Rules" and "Rodin Platform 1.2 Release Notes"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
(Extended rule SIMP_TYPE_OVERL_CPROD.)
 
imported>Pascal
 
Line 1: Line 1:
−
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
+
{{TOCright}}
−
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}}
+
== What's New in Rodin 1.2? ==
−
{{RRRow}}|*||{{Rulename|SIMP_DOM_COMPSET}}||<math>  \dom (\{ x \mapsto  a, \ldots , y \mapsto  b\} ) \;\;\defi\;\;  \{ x, \ldots , y\} </math>||  ||  A
+
{{TODO | List here the new features and improvements.}}
−
{{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\cdots\ovl\mathit{Ty}\ovl\cdots\ovl s;\;\defi\;\; \mathit{Ty}\ovl\cdots\ovl s </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_FUNIMAGE_LAMBDA}}||<math>  (\lambda x \qdot  P(x) \mid  E(x))(y) \;\;\defi\;\;  E(y) </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_DOM_LAMBDA}}||<math>\dom(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid E\}</math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_RAN_LAMBDA}}||<math>\ran(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid F\} </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
 
  
−
|}
+
* [[Generated Model Elements | Generated elements]]
  
 +
* [[Predicate_variables|Predicate variables extension]]
  
 +
* Migration to Eclipse 3.5 (Galileo)
  
−
[[Category:User documentation|The Proving Perspective]]
+
== Requirements ==
−
[[Category:Rodin Platform|The Proving Perspective]]
+
* It is recommended to run the Rodin platform with a Java 1.5 Runtime Environment.
−
[[Category:User manual|The Proving Perspective]]
+
* Only a 32-bit version of the Rodin platform is provided. Some optional libraries dedicated to 32-bit support may be required in order to run it on a 64-bit OS. Moreover, you will have to install a 32-bit Java Virtual Machine (JVM), and then to set the -vm option to make sure that Rodin is run with the correct JVM.
 +
:''eg.'' <tt>/usr/local/rodin/rodin -vm /usr/lib/jvm/ia32-java-1.5.0-sun/bin/java</tt> (You have to adjust paths to your system.)
 +
 
 +
== External plug-ins ==
 +
{{TODO | Describe here the available plug-ins, and the supported versions for this release.}}
 +
 
 +
== Downloading ==
 +
{{TODO | Add here a link to download the platform.}}
 +
 
 +
== Fixed Bugs ==
 +
{{TODO | Add here a list of the fixed bugs.}}
 +
 
 +
== Known Issues ==
 +
* Early releases of XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). More recent releases fix this bug (works fine with xulrunner-1.9.1.7). Alternatively, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:
 +
-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner-1.9.0.14
 +
where "/usr/lib/xulrunner-1.9.0.14" must be replaced with your actual XULRunner 1.9.0 install directory.
 +
 
 +
* Using Rodin on GNOME desktop may result in a situation where buttons lock windows. To avoid this situation, it is needed to launch Rodin with
 +
GDK_NATIVE_WINDOWS=1 /path_to_rodin/rodin
 +
It's a GTK bug, referenced for Eclipse at [[https://bugs.eclipse.org/bugs/show_bug.cgi?id=291257]]<br />See also [[Gnome and broken buttons]].
 +
 
 +
* A warning like the following one is displayed to the standard output when platform starts on GNOME desktop:
 +
(rodin:17254): GLib-WARNING **: g_set_prgname() called multiple times
 +
It's a GNOME bug. Information found there: [[https://issues.foresightlinux.org/browse/FL-2333]]
 +
 
 +
* The error log shows the following problem:
 +
org.osgi.framework.BundleException: The bundle could not be resolved. Reason: Missing Constraint: Import-Package: org.eclipse.equinox.internal.util.event; version="1.0.0"
 +
at org.eclipse.osgi.framework.internal.core.AbstractBundle.getResolverError(AbstractBundle.java:1313)
 +
...
 +
It's an Eclipse 3.5 bug. Information found there: [[http://www.eclipse.org/forums/index.php?t=msg&goto=131264&S=00746ff4ca25d6bd09d287e97ead74ff]]
 +
 
 +
* The list of the currently open bugs is given below:
 +
{{TODO | Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.2).}}
 +
 
 +
[[Category:Rodin Platform Release Notes]]

Revision as of 10:51, 20 January 2010

What's New in Rodin 1.2?

TODO: List here the new features and improvements.

  • Migration to Eclipse 3.5 (Galileo)

Requirements

  • It is recommended to run the Rodin platform with a Java 1.5 Runtime Environment.
  • Only a 32-bit version of the Rodin platform is provided. Some optional libraries dedicated to 32-bit support may be required in order to run it on a 64-bit OS. Moreover, you will have to install a 32-bit Java Virtual Machine (JVM), and then to set the -vm option to make sure that Rodin is run with the correct JVM.
eg. /usr/local/rodin/rodin -vm /usr/lib/jvm/ia32-java-1.5.0-sun/bin/java (You have to adjust paths to your system.)

External plug-ins

TODO: Describe here the available plug-ins, and the supported versions for this release.

Downloading

TODO: Add here a link to download the platform.

Fixed Bugs

TODO: Add here a list of the fixed bugs.

Known Issues

  • Early releases of XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). More recent releases fix this bug (works fine with xulrunner-1.9.1.7). Alternatively, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:
-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner-1.9.0.14

where "/usr/lib/xulrunner-1.9.0.14" must be replaced with your actual XULRunner 1.9.0 install directory.

  • Using Rodin on GNOME desktop may result in a situation where buttons lock windows. To avoid this situation, it is needed to launch Rodin with
GDK_NATIVE_WINDOWS=1 /path_to_rodin/rodin

It's a GTK bug, referenced for Eclipse at [[1]]
See also Gnome and broken buttons.

  • A warning like the following one is displayed to the standard output when platform starts on GNOME desktop:
(rodin:17254): GLib-WARNING **: g_set_prgname() called multiple times

It's a GNOME bug. Information found there: [[2]]

  • The error log shows the following problem:
org.osgi.framework.BundleException: The bundle could not be resolved. Reason: Missing Constraint: Import-Package: org.eclipse.equinox.internal.util.event; version="1.0.0"
at org.eclipse.osgi.framework.internal.core.AbstractBundle.getResolverError(AbstractBundle.java:1313)
...

It's an Eclipse 3.5 bug. Information found there: [[3]]

  • The list of the currently open bugs is given below:

TODO: Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.2).

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