Relation Rewrite Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Wohuai mNo edit summary |
Rules DEF_EQUAL_FUN_IMAGE and SIMP_SPECIAL_IN_*ID have been implemented in Rodin 3.9 |
||
(53 intermediate revisions by 9 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}}|*||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_DOM_SETENUM}}||<math> \dom (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ x, \ldots , y\} </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_DOM_CONVERSE}}||<math> \dom (r^{-1} ) \;\;\defi\;\; \ran (r) </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_DOM_CONVERSE}}||<math> \dom (r^{-1} ) \;\;\defi\;\; \ran (r) </math>|| || A | ||
{{RRRow}}|*||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_RAN_SETENUM}}||<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_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_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_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> | {{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_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_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_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_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_MULTI_DOMRES_RAN}}||<math> \ran (r) \domres r^{-1} \;\;\defi\;\; r^{-1} </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_DOMRES_DOMRES_ID}}||<math> S \domres (T \domres \id) \;\;\defi\;\; (S \binter T) \domres \id </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_DOMRES_DOMSUB_ID}}||<math> S \domres (T \domsub \id) \;\;\defi\;\; (S \setminus T) \domres \id </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RANRES_R}}||<math> r \ranres \emptyset \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RANRES_L}}||<math> \emptyset \ranres S \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{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| | {{RRRow}}|*||{{Rulename|SIMP_MULTI_RANRES_RAN}}||<math> r \ranres \ran (r) \;\;\defi\;\; r </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_MULTI_RANRES_DOM}}||<math> r^{-1} \ranres \dom (r) \;\;\defi\;\; r^{-1} </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_RANRES_ID}}||<math> \id \ranres S \;\;\defi\;\; S \domres \id </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_RANSUB_ID}}||<math> \id \ransub S \;\;\defi\;\; S \domsub \id </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_RANRES_DOMRES_ID}}||<math> (S \domres \id) \ranres T \;\;\defi\;\; (S \binter T) \domres \id </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_RANRES_DOMSUB_ID}}||<math> (S \domsub \id) \ranres T \;\;\defi\;\; (T \setminus S) \domres \id </math>|| || A | |||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DOMSUB_L}}||<math> \emptyset \domsub r \;\;\defi\;\; r </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DOMSUB_R}}||<math> S \domsub \emptyset \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{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| | {{RRRow}}|*||{{Rulename|SIMP_MULTI_DOMSUB_DOM}}||<math> \dom (r) \domsub r \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_MULTI_DOMSUB_RAN}}||<math> \ran (r) \domsub r^{-1} \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_DOMSUB_DOMRES_ID}}||<math> S \domsub (T \domres \id ) \;\;\defi\;\; (T \setminus S) \domres \id </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_DOMSUB_DOMSUB_ID}}||<math> S \domsub (T \domsub \id ) \;\;\defi\;\; (S \bunion T) \domsub \id </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RANSUB_R}}||<math> r \ransub \emptyset \;\;\defi\;\; r </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RANSUB_L}}||<math> \emptyset \ransub S \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{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_DOM}}||<math> r^{-1} \ransub \dom (r) \;\;\defi\;\; \emptyset </math>|| || A | |||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_MULTI_RANSUB_RAN}}||<math> r \ransub \ran (r) \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_RANSUB_DOMRES_ID}}||<math> (S \domres \id) \ransub T \;\;\defi\;\; (S \setminus T) \domres \id </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_RANSUB_DOMSUB_ID}}||<math> (S \domsub \id) \ransub T \;\;\defi\;\; (S \bunion T) \domsub \id </math>|| || A | ||
{{ | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_FCOMP}}||<math> r \fcomp \ldots \fcomp \emptyset \fcomp \ldots \fcomp s \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{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| | {{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| | {{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| | {{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| | {{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_R}}||<math> r[\emptyset ] \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RELIMAGE_L}}||<math> \emptyset [S] \;\;\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_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_MULTI_RELIMAGE_DOM}}||<math> r[\dom (r)] \;\;\defi\;\; \ran (r) </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_RELIMAGE_ID}}||<math> \id[T] \;\;\defi\;\; T </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_RELIMAGE_DOMRES_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_RELIMAGE_DOMSUB_ID}}||<math> (S \domsub \id)[T] \;\;\defi\;\; T \setminus S </math>|| || 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_CPROD_SING}}||<math> (\{ E\} \cprod S)[\{ E\} ] \;\;\defi\;\; S </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_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_RANRES}}||<math> (r \ranres S)^{-1} [S] \;\;\defi\;\; r^{-1} [S] </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB}}||<math> (r \ransub S)^{-1} [S] \;\;\defi\;\; \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_RELIMAGE_CONVERSE_DOMSUB}}||<math> (S \domsub r)^{-1} [T] \;\;\defi\;\; r^{-1} [T] \setminus S </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_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|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|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_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|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_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_ID}}||<math> \id^{-1} \;\;\defi\;\; \id </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{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_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_CONVERSE_COMPSET}}||<math> \{ X \qdot P \mid x\mapsto y\} ^{-1} \;\;\defi\;\; \{ X \qdot P \mid y\mapsto x\} </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{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| | {{RRRow}}|*||{{Rulename|SIMP_FCOMP_ID_L}}||<math> (S \domres \id) \fcomp r \;\;\defi\;\; S \domres r </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_FCOMP_ID_R}}||<math> r \fcomp (S \domres \id) \;\;\defi\;\; r \ranres S </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{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| | {{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_PRJ1}}||<math> \prjone (E \mapsto F) \;\;\defi\;\; E </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_PRJ2}}||<math> \prjtwo (E \mapsto F) \;\;\defi\;\; F </math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{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| | {{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| | {{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| | {{RRRow}}|*||{{Rulename|SIMP_DOM_LAMBDA}}||<math>\dom(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid E\}</math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_RAN_LAMBDA}}||<math>\ran(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid F\} </math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_IN_FUNIMAGE}}||<math>E\mapsto F(E)\in F \;\;\defi\;\; \btrue</math>|| || A | ||
{{RRRow}}|||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_IN_FUNIMAGE_CONVERSE_L}}||<math>F^{-1}(E)\mapsto E\in F \;\;\defi\;\; \btrue</math>|| || A | ||
{{RRRow}}| ||{{Rulename| | {{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> \{ E, \ldots , x \mapsto y, \ldots , F\} (x) \;\;\defi\;\; y </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_OVERL_SETENUM}}||<math> (r \ovl \ldots \ovl \{ E, \ldots , x \mapsto y, \ldots , F\} )(x) \;\;\defi\;\; y </math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_BUNION_SETENUM}}||<math> (r \bunion \ldots \bunion \{ E, \ldots , x \mapsto y, \ldots , F\} )(x) \;\;\defi\;\; y </math>|| || A | |||
{{RRRow}}|||{{Rulename|SIMP_MULTI_FUNIMAGE_BUNION_SETENUM}}||<math> (r \bunion \ldots \bunion \{ | |||
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_CPROD}}||<math> (S \cprod \{ F\} )(x) \;\;\defi\;\; F </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_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_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_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_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|DEF_BCOMP}}||<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math>|| || M | {{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_EQUAL_FUNIMAGE}}||<math> f(x) = y \;\;\defi\;\; x \mapsto y \in f </math>|| || M | |||
{{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|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_DOM}}||<math> \dom (\emptyset ) \;\;\defi\;\; \emptyset </math>|| || A | ||
Line 106: | Line 122: | ||
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_RANRES}}||<math> p \fcomp (q \ranres s) \;\;\defi\;\; (p \fcomp q) \ranres s </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|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|DERIV_FCOMP_SING}}||<math> \{E\mapsto F\}\fcomp\{F\mapsto G\} \;\;\defi\;\; \{E\mapsto G\} </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} \ | {{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_RAN}}||<math> \ran (\mathit{Ty}) \;\;\defi\;\; \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \ | {{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_MULTI_DOM_CPROD}}||<math> \dom (E \cprod E) \;\;\defi\;\; E </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_RAN_CPROD}}||<math> \ran (E \cprod E) \;\;\defi\;\; E </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|SIMP_MULTI_DOM_DOMRES}}||<math>\dom(A\domres f) \;\;\defi\;\; \dom(f)\binter A</math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DOM_DOMSUB}}||<math>\dom(A\domsub f) \;\;\defi\;\; \dom(f)\setminus A</math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RAN_RANRES}}||<math>\ran(f\ranres A) \;\;\defi\;\; \ran(f)\binter A</math>|| || A | |||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RAN_RANSUB}}||<math>\ran(f\ransub A) \;\;\defi\;\; \ran(f)\setminus A</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_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_RAN}}||<math> F \in \ran (r) \;\;\defi\;\; \exists x \qdot x \mapsto F \in r </math>|| || M | ||
Line 124: | Line 145: | ||
{{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_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_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_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_RELRAN}}||<math> r \in S \srel T \;\;\defi\;\; r \in S \rel T \land \ran (r) = T </math>|| || M | ||
Line 157: | Line 179: | ||
{{RRRow}}|||{{Rulename|DISTRI_DOMRES_OVERL}}||<math> s \domres (r \ovl q) \;\;\defi\;\; (s \domres r) \ovl (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_R}}||<math> s \domsub (p \bunion q) \;\;\defi\;\; (s \domsub p) \bunion (s \domsub q) </math>|| || M | ||
{{RRRow}}| | {{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_R}}||<math> s \domsub (p \binter q) \;\;\defi\;\; (s \domsub p) \binter (s \domsub q) </math>|| || M | ||
{{RRRow}}| | {{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_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_DOMSUB_OVERL}}||<math> A \domsub (r \ovl s) \;\;\defi\;\; (A \domsub r) \ovl (A \domsub s) </math>|| || M | ||
Line 168: | Line 190: | ||
{{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_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_RANRES_SETMINUS_L}}||<math> (p \setminus q) \ranres s \;\;\defi\;\; (p \ranres s) \setminus (q \ranres s) </math>|| || M | ||
{{RRRow}}| | {{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_BUNION_L}}||<math> (p \bunion q) \ransub s \;\;\defi\;\; (p \ransub s) \bunion (q \ransub s) </math>|| || M | ||
{{RRRow}}| | {{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_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_BUNION}}||<math> (p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1} </math>|| || M | ||
Line 186: | Line 208: | ||
{{RRRow}}|*||{{Rulename|DISTRI_RELIMAGE_BUNION_R}}||<math> r[S \bunion T] \;\;\defi\;\; r[S] \bunion r[T] </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|DISTRI_RELIMAGE_BUNION_L}}||<math> (p \bunion q)[S] \;\;\defi\;\; p[S] \bunion q[S] </math>|| || M | ||
{{RRRow}}|*||{{Rulename| | {{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}}| | {{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}}|*||{{Rulename| | {{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}}| ||{{Rulename| | {{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| | {{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|prjtwo | {{RRRow}}|*||{{Rulename|SIMP_MAPSTO_PRJ1_PRJ2}}||<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> || || A | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}| ||{{Rulename|DERIV_EXPAND_PRJS}}||<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> || || M | ||
{{RRRow}}| ||{{Rulename| | {{RRRow}}|*||{{Rulename|SIMP_DOM_SUCC}}||<math>\dom(\usucc) \;\;\defi\;\; \intg</math> || || A | ||
{{RRRow}}| ||{{Rulename| | {{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 |
A | ||
* | SIMP_DOM_CONVERSE |
A | ||
* | SIMP_RAN_SETENUM |
A | ||
* | SIMP_RAN_CONVERSE |
A | ||
* | SIMP_SPECIAL_OVERL |
A | ||
* | SIMP_MULTI_OVERL |
there is a such that and and are syntactically equal. | A | |
* | SIMP_TYPE_OVERL_CPROD |
where is a type expression | A | |
* | SIMP_SPECIAL_DOMRES_L |
A | ||
* | SIMP_SPECIAL_DOMRES_R |
A | ||
* | SIMP_TYPE_DOMRES |
where is a type expression | A | |
* | SIMP_MULTI_DOMRES_DOM |
A | ||
* | SIMP_MULTI_DOMRES_RAN |
A | ||
* | SIMP_DOMRES_DOMRES_ID |
A | ||
* | SIMP_DOMRES_DOMSUB_ID |
A | ||
* | SIMP_SPECIAL_RANRES_R |
A | ||
* | SIMP_SPECIAL_RANRES_L |
A | ||
* | SIMP_TYPE_RANRES |
where is a type expression | A | |
* | SIMP_MULTI_RANRES_RAN |
A | ||
* | SIMP_MULTI_RANRES_DOM |
A | ||
* | SIMP_RANRES_ID |
A | ||
* | SIMP_RANSUB_ID |
A | ||
* | SIMP_RANRES_DOMRES_ID |
A | ||
* | SIMP_RANRES_DOMSUB_ID |
A | ||
* | SIMP_SPECIAL_DOMSUB_L |
A | ||
* | SIMP_SPECIAL_DOMSUB_R |
A | ||
* | SIMP_TYPE_DOMSUB |
where is a type expression | A | |
* | SIMP_MULTI_DOMSUB_DOM |
A | ||
* | SIMP_MULTI_DOMSUB_RAN |
A | ||
* | SIMP_DOMSUB_DOMRES_ID |
A | ||
* | SIMP_DOMSUB_DOMSUB_ID |
A | ||
* | SIMP_SPECIAL_RANSUB_R |
A | ||
* | SIMP_SPECIAL_RANSUB_L |
A | ||
* | SIMP_TYPE_RANSUB |
where is a type expression | A | |
* | SIMP_MULTI_RANSUB_DOM |
A | ||
* | SIMP_MULTI_RANSUB_RAN |
A | ||
* | SIMP_RANSUB_DOMRES_ID |
A | ||
* | SIMP_RANSUB_DOMSUB_ID |
A | ||
* | SIMP_SPECIAL_FCOMP |
A | ||
* | SIMP_TYPE_FCOMP_ID |
A | ||
* | SIMP_TYPE_FCOMP_R |
where is a type expression equal to | A | |
* | SIMP_TYPE_FCOMP_L |
where is a type expression equal to | A | |
* | SIMP_FCOMP_ID |
A | ||
* | SIMP_SPECIAL_BCOMP |
A | ||
* | SIMP_TYPE_BCOMP_ID |
A | ||
* | SIMP_TYPE_BCOMP_L |
where is a type expression equal to | A | |
* | SIMP_TYPE_BCOMP_R |
where is a type expression equal to | A | |
* | SIMP_BCOMP_ID |
A | ||
* | SIMP_SPECIAL_DPROD_R |
A | ||
* | SIMP_SPECIAL_DPROD_L |
A | ||
* | SIMP_DPROD_CPROD |
A | ||
* | SIMP_SPECIAL_PPROD_R |
A | ||
* | SIMP_SPECIAL_PPROD_L |
A | ||
* | SIMP_PPROD_CPROD |
A | ||
* | SIMP_SPECIAL_RELIMAGE_R |
A | ||
* | SIMP_SPECIAL_RELIMAGE_L |
A | ||
* | SIMP_TYPE_RELIMAGE |
where is a type expression | A | |
* | SIMP_MULTI_RELIMAGE_DOM |
A | ||
* | SIMP_RELIMAGE_ID |
A | ||
* | SIMP_RELIMAGE_DOMRES_ID |
A | ||
* | SIMP_RELIMAGE_DOMSUB_ID |
A | ||
* | SIMP_MULTI_RELIMAGE_CPROD_SING |
where is a single expression | A | |
* | SIMP_MULTI_RELIMAGE_SING_MAPSTO |
where is a single expression | A | |
* | SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB |
A | ||
* | SIMP_MULTI_RELIMAGE_CONVERSE_RANRES |
A | ||
* | SIMP_RELIMAGE_CONVERSE_DOMSUB |
A | ||
DERIV_RELIMAGE_RANSUB |
M | |||
DERIV_RELIMAGE_RANRES |
M | |||
* | SIMP_MULTI_RELIMAGE_DOMSUB |
A | ||
DERIV_RELIMAGE_DOMSUB |
M | |||
DERIV_RELIMAGE_DOMRES |
M | |||
* | SIMP_SPECIAL_CONVERSE |
A | ||
* | SIMP_CONVERSE_ID |
A | ||
* | SIMP_CONVERSE_CPROD |
A | ||
* | SIMP_CONVERSE_SETENUM |
A | ||
* | SIMP_CONVERSE_COMPSET |
A | ||
* | SIMP_DOM_ID |
where has type | A | |
* | SIMP_RAN_ID |
where has type | A | |
* | SIMP_FCOMP_ID_L |
A | ||
* | SIMP_FCOMP_ID_R |
A | ||
* | SIMP_SPECIAL_REL_R |
idem for operators | A | |
* | SIMP_SPECIAL_REL_L |
idem for operators | A | |
* | SIMP_FUNIMAGE_PRJ1 |
A | ||
* | SIMP_FUNIMAGE_PRJ2 |
A | ||
* | SIMP_DOM_PRJ1 |
where has type | A | |
* | SIMP_DOM_PRJ2 |
where has type | A | |
* | SIMP_RAN_PRJ1 |
where has type | A | |
* | SIMP_RAN_PRJ2 |
where has type | A | |
* | SIMP_FUNIMAGE_LAMBDA |
A | ||
* | SIMP_DOM_LAMBDA |
A | ||
* | SIMP_RAN_LAMBDA |
A | ||
* | SIMP_IN_FUNIMAGE |
A | ||
* | SIMP_IN_FUNIMAGE_CONVERSE_L |
A | ||
* | SIMP_IN_FUNIMAGE_CONVERSE_R |
A | ||
* | SIMP_MULTI_FUNIMAGE_SETENUM_LL |
A | ||
* | SIMP_MULTI_FUNIMAGE_SETENUM_LR |
A | ||
* | SIMP_MULTI_FUNIMAGE_OVERL_SETENUM |
A | ||
* | SIMP_MULTI_FUNIMAGE_BUNION_SETENUM |
A | ||
* | SIMP_FUNIMAGE_CPROD |
A | ||
* | SIMP_FUNIMAGE_ID |
A | ||
* | SIMP_FUNIMAGE_FUNIMAGE_CONVERSE |
A | ||
* | SIMP_FUNIMAGE_CONVERSE_FUNIMAGE |
A | ||
* | SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM |
A | ||
* | SIMP_FUNIMAGE_DOMRES |
with hypothesis where is one of , , , , , , . | AM | |
* | SIMP_FUNIMAGE_DOMSUB |
with hypothesis where is one of , , , , , , . | AM | |
* | SIMP_FUNIMAGE_RANRES |
with hypothesis where is one of , , , , , , . | AM | |
* | SIMP_FUNIMAGE_RANSUB |
with hypothesis where is one of , , , , , , . | AM | |
* | SIMP_FUNIMAGE_SETMINUS |
with hypothesis where is one of , , , , , , . | AM | |
* | DEF_EQUAL_FUNIMAGE |
M | ||
* | DEF_BCOMP |
M | ||
DERIV_ID_SING |
where is a single expression | M | ||
* | SIMP_SPECIAL_DOM |
A | ||
* | SIMP_SPECIAL_RAN |
A | ||
* | SIMP_CONVERSE_CONVERSE |
A | ||
* | DERIV_RELIMAGE_FCOMP |
M | ||
* | DERIV_FCOMP_DOMRES |
M | ||
* | DERIV_FCOMP_DOMSUB |
M | ||
* | DERIV_FCOMP_RANRES |
M | ||
* | DERIV_FCOMP_RANSUB |
M | ||
DERIV_FCOMP_SING |
A | |||
* | SIMP_SPECIAL_EQUAL_RELDOMRAN |
idem for operators | A | |
* | SIMP_TYPE_DOM |
where is a type expression equal to | A | |
* | SIMP_TYPE_RAN |
where is a type expression equal to | A | |
* | SIMP_MULTI_DOM_CPROD |
A | ||
* | SIMP_MULTI_RAN_CPROD |
A | ||
* | SIMP_MULTI_DOM_DOMRES |
A | ||
* | SIMP_MULTI_DOM_DOMSUB |
A | ||
* | SIMP_MULTI_RAN_RANRES |
A | ||
* | SIMP_MULTI_RAN_RANSUB |
A | ||
* | DEF_IN_DOM |
M | ||
* | DEF_IN_RAN |
M | ||
* | DEF_IN_CONVERSE |
M | ||
* | DEF_IN_DOMRES |
M | ||
* | DEF_IN_RANRES |
M | ||
* | DEF_IN_DOMSUB |
M | ||
* | DEF_IN_RANSUB |
M | ||
* | DEF_IN_RELIMAGE |
M | ||
* | DEF_IN_FCOMP |
M | ||
* | DEF_OVERL |
M | ||
* | DEF_IN_ID |
M | ||
* | DEF_IN_DPROD |
M | ||
* | DEF_IN_PPROD |
M | ||
* | DEF_IN_REL |
M | ||
* | DEF_IN_RELDOM |
M | ||
* | DEF_IN_RELRAN |
M | ||
* | DEF_IN_RELDOMRAN |
M | ||
* | DEF_IN_FCT |
M | ||
* | DEF_IN_TFCT |
M | ||
* | DEF_IN_INJ |
M | ||
* | DEF_IN_TINJ |
M | ||
* | DEF_IN_SURJ |
M | ||
* | DEF_IN_TSURJ |
M | ||
* | DEF_IN_BIJ |
M | ||
DISTRI_BCOMP_BUNION |
M | |||
* | DISTRI_FCOMP_BUNION_R |
M | ||
* | DISTRI_FCOMP_BUNION_L |
M | ||
DISTRI_DPROD_BUNION |
M | |||
DISTRI_DPROD_BINTER |
M | |||
DISTRI_DPROD_SETMINUS |
M | |||
DISTRI_DPROD_OVERL |
M | |||
DISTRI_PPROD_BUNION |
M | |||
DISTRI_PPROD_BINTER |
M | |||
DISTRI_PPROD_SETMINUS |
M | |||
DISTRI_PPROD_OVERL |
M | |||
DISTRI_OVERL_BUNION_L |
M | |||
DISTRI_OVERL_BINTER_L |
M | |||
* | DISTRI_DOMRES_BUNION_R |
M | ||
* | DISTRI_DOMRES_BUNION_L |
M | ||
* | DISTRI_DOMRES_BINTER_R |
M | ||
* | DISTRI_DOMRES_BINTER_L |
M | ||
DISTRI_DOMRES_SETMINUS_R |
M | |||
DISTRI_DOMRES_SETMINUS_L |
M | |||
DISTRI_DOMRES_DPROD |
M | |||
DISTRI_DOMRES_OVERL |
M | |||
* | DISTRI_DOMSUB_BUNION_R |
M | ||
* | DISTRI_DOMSUB_BUNION_L |
M | ||
* | DISTRI_DOMSUB_BINTER_R |
M | ||
* | DISTRI_DOMSUB_BINTER_L |
M | ||
DISTRI_DOMSUB_DPROD |
M | |||
DISTRI_DOMSUB_OVERL |
M | |||
* | DISTRI_RANRES_BUNION_R |
M | ||
* | DISTRI_RANRES_BUNION_L |
M | ||
* | DISTRI_RANRES_BINTER_R |
M | ||
* | DISTRI_RANRES_BINTER_L |
M | ||
DISTRI_RANRES_SETMINUS_R |
M | |||
DISTRI_RANRES_SETMINUS_L |
M | |||
* | DISTRI_RANSUB_BUNION_R |
M | ||
* | DISTRI_RANSUB_BUNION_L |
M | ||
* | DISTRI_RANSUB_BINTER_R |
M | ||
* | DISTRI_RANSUB_BINTER_L |
M | ||
* | DISTRI_CONVERSE_BUNION |
M | ||
DISTRI_CONVERSE_BINTER |
M | |||
DISTRI_CONVERSE_SETMINUS |
M | |||
DISTRI_CONVERSE_BCOMP |
M | |||
DISTRI_CONVERSE_FCOMP |
M | |||
DISTRI_CONVERSE_PPROD |
M | |||
DISTRI_CONVERSE_DOMRES |
M | |||
DISTRI_CONVERSE_DOMSUB |
M | |||
DISTRI_CONVERSE_RANRES |
M | |||
DISTRI_CONVERSE_RANSUB |
M | |||
* | DISTRI_DOM_BUNION |
M | ||
* | DISTRI_RAN_BUNION |
M | ||
* | DISTRI_RELIMAGE_BUNION_R |
M | ||
* | DISTRI_RELIMAGE_BUNION_L |
M | ||
* | DERIV_DOM_TOTALREL |
with hypothesis , where is one of | M | |
DERIV_RAN_SURJREL |
with hypothesis , where is one of | M | ||
* | DERIV_PRJ1_SURJ |
where and are types and is one of | A | |
* | DERIV_PRJ2_SURJ |
where and are types and is one of | A | |
* | DERIV_ID_BIJ |
where is a type and is any arrow | A | |
* | SIMP_MAPSTO_PRJ1_PRJ2 |
A | ||
DERIV_EXPAND_PRJS |
M | |||
* | SIMP_DOM_SUCC |
A | ||
* | SIMP_RAN_SUCC |
A | ||
* | DERIV_MULTI_IN_BUNION |
A | ||
* | DERIV_MULTI_IN_SETMINUS |
A | ||
* | DEF_PRED |
A | ||
* | SIMP_SPECIAL_IN_ID |
A | ||
* | SIMP_SPECIAL_IN_SETMINUS_ID |
A | ||
* | SIMP_SPECIAL_IN_DOMRES_ID |
A | ||
* | SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID |
A |